From d40821ee33a00e9239c76862ee4dfba95ed09825 Mon Sep 17 00:00:00 2001
From: Ben Gamari <ben@smart-cactus.org>
Date: Mon, 8 Oct 2018 14:29:53 -0400
Subject: [PATCH] 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 | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/GHC/TypeLits/Extra.hs b/src/GHC/TypeLits/Extra.hs
index f28ae2d..2ae8736 100644
--- a/src/GHC/TypeLits/Extra.hs
+++ b/src/GHC/TypeLits/Extra.hs
@@ -106,9 +106,21 @@ 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
@@ -116,7 +128,10 @@ instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Max) x y where
 
 -- | 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