I'm a heavy user of ghc-typelits-natnormalise. I can feel your pain that it sometimes isn't able to solve seemingly "simple" constraints. But not all is lost in those cases. The `constraints` package allows one to solve `Nat` constraints out of thin air, provided you go through a function to do it. nLEZeroIsZeroRule :: (n <= 0) :- (n ~ 0) nLEZeroIsZeroRule = Sub (unsafeCoerce (Dict :: Dict (a ~ a))) foo :: (n ~ 0) => Int foo = 10 bar :: forall (n :: Nat). (n <= 0) => Int bar = case nLEZeroIsZeroRule @n of { Sub Dict -> foo @n } If you can hide your contraints behind this for users of your library it might not such a bad option. I don't need very many of these since natnormalise does by far the most work for me. This just fills the gaps. Rowan Goemans On 1/12/23 19:10, Henning Thielemann wrote:
On Fri, 13 Jan 2023, 石井大海 wrote:
Just a shameless plug: I deviced ghc-typelits-presburger exactly to solve such problems, and applying in conjunction with ghc-typelits-natnormalise in production code:
https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger
Formally, this augments GHC's type checker with Presburger Arithmetic Solver.
This sounds promising!
I know that Iavor Diatchki implemented a Presburger Arithmetic Solver for GHC type checking many years ago, but when I asked last time, he recommended ghc-typelits-natnormalise.
Although there indeed be some propositions that this plugin cannot solve, but together with ghc-typelits-natnormalise and ghc-typelits-knownnat, relatively wide range of propositions can be solved automatically in my experiences.
It is good to know that I can combine different type checker plugins.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.