Drop equality cases from Min/Max

I've recently been playing around with the
[Thoralf](https://github.com/Divesh-Otwani/the-thoralf-plugin) plugin for
more sophisticated solving. Unfortunately, it gets a bit confused with the
equality case in `Min` and `Max`.

I've included CPP guards for earlier GHC versions, which don't support
ghc-typelits-knownnat's KnownBool solver.

src/GHC/TypeLits/Extra.hs

@@ -106,17 +106,32 @@ intToNumber x = smallInteger x
 #endif
 {-# INLINE intToNumber #-}
 
+-- Note [Reflexive equations]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~
+--
+-- Both Min and Max include equations for the reflexive case for GHC < 8.6.
+-- This is because with versions after 8.6 the ghc-typelits-knownnat solver is
+-- smart enough to solve in the presence of If applications using the KnownBool
+-- solver.
+--
+
 -- | Type-level 'max'
 type family Max (x :: Nat) (y :: Nat) :: Nat where
+#if !MIN_VERSION_ghc(8,6,0)
+  -- See Note [Reflexive equations] above
   Max n n = n
+#endif
   Max x y = If (x <=? y) y x
 
 instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Max) x y where
   natSing2 = SNatKn (max (N.natVal (Proxy @x)) (N.natVal (Proxy @y)))
 
 -- | Type-level 'min'
 type family Min (x :: Nat) (y :: Nat) :: Nat where
+#if !MIN_VERSION_ghc(8,6,0)
+  -- See Note [Reflexive equations] above
   Min n n = n
+#endif
   Min x y = If (x <=? y) x y
 
 instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Min) x y where