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

[RFC] Drop equality cases from Min/Max #16

Open bgamari opened 5 years ago

bgamari commented 5 years ago

I've recently been playing around with the Thoralf plugin for more sophisticated solving. Unfortunately, it gets a bit confused with the equality case in Min and Max. However, if I'm not mistaken it is redundant anyways.

bgamari commented 5 years ago

Actually, it seems that this breaks the ghc-typelits-knownnat solver for reasons I haven't yet pieced together.

christiaanb commented 5 years ago

Ah, so single clause closed type families are sorta treated like type synonyms, and so the KnownNat2 instance used by ghc-typelits-knownnat will no longer work. As it won’t see a KnownNat (Max x y), but KnownNat (If (x <=? y) y x)

bgamari commented 5 years ago

I have updated this to keep the reflexive cases for GHC < 8.6, since these compilers don't support the KnownBool solver recently introduced in ghc-typelits-knownnat.

christiaanb commented 4 years ago

I applied these changes manually, but it seems the test suite would no longer pass since we added more "reasoning-about-max/min" capabilities to the solver, and so the solver itself now needs min/max not to be a type-synonym.... I guess we could fix this internally by treating If (X <=? Y) X Y as Min and If (X <=? Y) Y X as Max.