The plugin takes gigabytes for a program with lots of additions

[Mikolaj]

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.