search

clash-lang / ghc-typelits-extra

Extra type-level operations on GHC.TypeLits.Nat and a custom solver
Other
16 stars 9 forks source link

Various KnownNat and solver issues #15

Open augustss opened 6 years ago

augustss commented 6 years ago

Some examples

Bug.hs.gz

christiaanb commented 6 years ago

  1. The superfluous constraints in bug2 should be solved by moving the KnownNat2 instances defined in ghc-typelits-extra for Div and Mod to the ghc-typelits-knownnat package. As a work-around, you can import GHC.TypeLits.Extra for now, so that the KnownNat2 instances will be in scope.

  2. I have yet to solve the other superfluous constraints; the inequality constraints in particular will take some time, because ghc-typelits-natnormalise inequality solver is really crude, and can only handle solving wanted inequalities using a single given inequality at a time. And in order to solve the wanted inequalities in your example it'll have to use multiple given inequalities at a time. I'll have to see how far the current brute-force approach will get...