In GHC's type-level subtraction, the term 0 - 1 will never be reduced.
As a ad-hoc workaround, we have to add constraints n :- m :>= 0 whenever n :- m appears as subterm.

It at least compiles with GHC 8.2, but panics at compile-time.

natLeqZero :: (n <= 0) => proxy n -> n :~: 0
natLeqZero _ = Refl

generates:

ghc: panic! (the 'impossible' happened)
  (GHC version 8.2.1 for x86_64-apple-darwin):
	kindPrimRep
  Bool
  typePrimRep (fsk0_a3Vp[fsk] :: Bool)
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
        pprPanic, called at compiler/simplStg/RepType.hs:344:5 in ghc:RepType

The plugin's handling of type families is very strange and unsound. For one thing, it treats type families that output natural numbers as constant, which is obviously unsound:

type family Simple (n :: Bool) :: Nat where
    Simple 'False = 0
    Simple 'True = 1

invalid :: forall x y. Simple x :~: Simple y
invalid = Refl

And here is the (trivial) proof of unsoundness:

type family RevSimple (n :: Nat) :: Bool where
    RevSimple 0 = 'False
    RevSimple 1 = 'True

absurdity :: 'True :~: 'False
absurdity = applyRev $ invalid @'True @'False where
    applyRev :: forall x y. x :~: y -> RevSimple x :~: RevSimple y
    applyRev Refl = Refl

It appears to also equate even distinct type families, as long as they have the same number of arguments applied, even cases like:

type family Simple (n :: Bool) :: Nat where
    Simple 'False = 0
    Simple 'True = 1

type family Weird :: Nat -> Nat where

invalid :: forall x y. Simple x :~: Weird y
invalid = Refl

However, this doesn't work if y is replaced with a constant.

invalid :: forall x. Simple x :~: Weird 0
invalid = Refl

doesn't typecheck, and neither does:

invalid :: forall x y. Simple x :~: Weird (y + 1)
invalid = Refl

However, this does:

type family Simple (n :: Nat) :: Nat where
    Simple 0 = 0
    Simple 1 = 1

type family Weird :: Nat -> Nat where

invalid :: forall x y. Simple (x + 1) :~: Weird (y + 1)
invalid = Refl

First, thank you very much for your plugin, It managed to solve one inequality with it that GHC.TypeLits.Normalise was not able to solve.

However, the ghc-typelits-presburger plugin takes gigabytes of memory (20G) when confronted with the following program fragment

projectGatherN
  :: forall k1 k2 k3 m1 m2 p n r.
     ( Show r, Numeric r
     , KnownNat k1, KnownNat k2, KnownNat k3
     , KnownNat m1, KnownNat m2, KnownNat p, KnownNat n )
  => Permutation -> AstIndex (k1 + k2 + k3) r
  -> (AstVarList (m1 + k1), AstVarList (m2 + k2), AstIndex p r)
  -> Ast (p + n + k3) r -> ShapeInt (m1 + k1 + m2 + k2 + n + k3)
  -> [Permutation]
  -> Ast (m1 + m2 + n) r
projectGatherN perm0 ix@(i1 :. rest1) (varsRev, var2 ::: vars, ix4) v sh@(_ :$ sh') permsOuter = undefined

taken from https://github.com/Mikolaj/horde-ad, though eventually it accepts it.

If the last line is changed to

projectGatherN _ _ _ _ _ _ = undefined

it accepts the program quickly.

I apologise for a lack of a standalone reproducer. If you every find time to work on these things again, let me know, and I can try to produce an example easier to work with.

The GHC plugin requires equational-reasoning to be installed when the plugin is used, but this doesn't appear to be documented. My issue was solved by adding build-inputs: equational-reasoning to my package.

natLeqZero', leqSucc and leqEquiv won't compile properly anymore in GHC 8.6.3.

ghc-typelits-presburger depends on generic-unification, which isn't on Hackage. As a result, I can't build this repo.

Consider the following example:

data Vec (n :: Nat) a where
  Nil :: Vec 0 a
  (:-) :: a -> Vec n a -> Vec (n + 1) a

infixr 9 :-

zipMVec :: Vec n a -> Vec n b -> Vec n (a, b)
zipMVec Nil Nil = Nil
zipMVec zs@(a :- as) (b :- bs) = (a, b) :- zipMVec zs bs

This must fail because zs has length n+1 and bs n.
If no solver is invoked, it is rejected as expected;
but if the plugin is enabeld, it is silently get accepted!

An invalid inference rule is made when handling comparisons and subtraction. I believe similar issues also occur around strict less than, but less than or equal proved the easiest to minimize:

invalid :: forall x y n. (x - n <=? y - n) :~: 'True -> (x <=? y) :~: 'True
invalid Refl = Refl

As demonstrated below, this is unsound:

absurdity :: 'True :~: 'False
absurdity = makeProof @5 @0 (allLe @5 @0) Refl where
    makeProof :: forall x y. (x <=? y) :~: 'True -> (x <=? y) :~: 'False -> 'True :~: 'False
    makeProof = worker where
        worker :: forall a' b'. (x <=? y) :~: a' -> (x <=? y) :~: b' -> a' :~: b'
        worker Refl Refl = Refl
    allLe :: forall x y. (x <=? y) :~: 'True
    allLe = worker where
        worker :: (x <=? y) :~: 'True
        worker = invalid @x @y @x worker'
        worker' :: (x - x <=? y - x) :~: 'True
        worker' = worker'' @(x - x) @(y - x) Refl
        worker'' :: forall n m. n :~: 0 -> (n <=? m) :~: 'True
        worker'' Refl = Refl

The fundamental problem is that the subtraction may reduce the left hand side to zero, and the rule forall x. 0 <= x then triggers even if x itself can't reduce, resulting in assertions like 0 <= 2 - 5 which should never be turned into 5 <= 2.