clash-lang / ghc-typelits-natnormalise

Normalise GHC.TypeLits.Nat equations
Other
43 stars 15 forks source link

WIP: Fix `n <= 0` constrained being reported as impossible. #83

Open rowanG077 opened 3 months ago

rowanG077 commented 3 months ago

The problem is in:

https://github.com/clash-lang/ghc-typelits-natnormalise/blob/84f500a9735675e96253181939c3473a567f6f7a/src-ghc-9.4/GHC/TypeLits/Normalise.hs#L506-L524

Given a constraint of a <= 0 then subtractIneq will turn that into -a and isNatural will report it as not a natural. The approach in this PR obviously doesn't work. There is a ton of fallout in the other plugins... So I need to think of something else.

The first commit tried a "proper" fix but there is fallout of tests failing on old GHCs and I tried to compile clash-compiler with it and a ton of breakage occured in ghc-typelits-extra. The second commit added a hack which does not have the problem of fallout. But doesn't work on older GHC due to a <= 0 turning up as a wanted.

Pinging the guru @christiaanb.