Fix lookup Div and Mod GHC >= 9.2

[rowanG077]

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]

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]

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]

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.