[RFC] Drop equality cases from Min/Max

[bgamari]

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]

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

[christiaanb]

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]

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]

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.