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

Fix lookup `Div` and `Mod` GHC >= 9.2 #52

Closed rowanG077 closed 5 months ago

rowanG077 commented 5 months ago

While implementing reduction Mod n p <= q -> p <= q + 1 I noticed that the lookups for Div and Mod were wrong post GHC 9.2.

I have fixed that and also added the reduction. If you want I can split this up into two PRs. One for the lookup fix and one for the reduction. But since the each change is so small I didn't feel like the overhead is worth it.

leonschoorl commented 5 months ago

This maybe unavoidable with the way type checker plugins work, but I don't think this reduction is always a good thing to do.

While p <= q + 1 implies Mod n p <= q. The opposite isn't necessarily true.

For example Mod 1 (a+3) <= 1 holds, but this now gets reduced to (a+3) <= 2, which does not hold. If there happens to be some other (hypothetical) plugin that could have solved the original Mod 1 (a+2) <= 2, and this plugin happens gets called first by GHC then type checking will fail because we now reduced it to an unsolvable form.

error: [GHC-83865]
    • Couldn't match type ‘Data.Type.Ord.OrdCond
                             (CmpNat (a + 3) 2) True True False’
                     with ‘True’
      Expected: Proxy True
        Actual: Proxy (Mod 1 (a + 3) <=? 1)
rowanG077 commented 5 months ago

Yes. You ideally want to reduce Mod n p <= q to 1 <= p && (n <= q || p <= q + 1) but I don't think type level disjunction exists? Or could you simply write a || type family?

rowanG077 commented 5 months ago

Since it's more controversial then expected I have removed the reduction from this PR. If you are oke with doing the reduction I will open a seperate PR.