Simplify Data.Type.Equality.==

Contrary to previous comments, we can calculate `==` for types
in an extremely general fashion. The approach used here is actually
the one mistakenly rejected as impossible. There will be some cases
when the previous version was able to reduce and this one is not,
particularly for types in `*` that are unknown, but known equal.
However, the new behavior is much more uniform. Within the
established framework of equality testing by pattern matching,
it does a better job than the previous version.

Reviewers: goldfire, austin, hvr, bgamari, RyanGlScott

Reviewed By: RyanGlScott

Subscribers: RyanGlScott, rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3835

6 files changed, 62 insertions, 184 deletions

diff --git a/docs/users_guide/8.4.1-notes.rst b/docs/users_guide/8.4.1-notes.rst
index db573202e2..2d03190663 100644
--- a/docs/users_guide/8.4.1-notes.rst
+++ b/docs/users_guide/8.4.1-notes.rst
@@ -191,6 +191,14 @@ Template Haskell
 - Blank strings can now be used as values for environment variables using the
   System.Environment.Blank module. See :ghc-ticket:`12494`
 
+- ``Data.Type.Equality.==`` is now a closed type family. It works for all kinds
+  out of the box. Any modules that previously declared instances of this family
+  will need to remove them. Whereas the previous definition was somewhat ad
+  hoc, the behavior is now completely uniform. As a result, some applications
+  that used to reduce no longer do, and conversely. Most notably, ``(==)`` no
+  longer treats the ``*``, ``j -> k``, or ``()`` kinds specially; equality is
+  tested structurally in all cases.
+
 Build system
 ~~~~~~~~~~~~
 
diff --git a/libraries/base/Data/Either.hs b/libraries/base/Data/Either.hs
index 58a8020034..c5ff7c0180 100644
--- a/libraries/base/Data/Either.hs
+++ b/libraries/base/Data/Either.hs
@@ -34,8 +34,6 @@ import GHC.Base
 import GHC.Show
 import GHC.Read
 
-import Data.Type.Equality
-
 -- $setup
 -- Allow the use of some Prelude functions in doctests.
 -- >>> import Prelude ( (+), (*), length, putStrLn )
@@ -330,13 +328,6 @@ fromRight :: b -> Either a b -> b
 fromRight _ (Right b) = b
 fromRight b _         = b
 
--- instance for the == Boolean type-level equality operator
-type family EqEither a b where
-  EqEither ('Left x)  ('Left y)  = x == y
-  EqEither ('Right x) ('Right y) = x == y
-  EqEither a          b          = 'False
-type instance a == b = EqEither a b
-
 {-
 {--------------------------------------------------------------------
   Testing
diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs
index 09999b021d..64bb5556cf 100644
--- a/libraries/base/Data/Type/Equality.hs
+++ b/libraries/base/Data/Type/Equality.hs
@@ -179,164 +179,47 @@ instance TestEquality ((:~:) a) where
 instance TestEquality ((:~~:) a) where
   testEquality HRefl HRefl = Just Refl
 
--- | A type family to compute Boolean equality. Instances are provided
--- only for /open/ kinds, such as @*@ and function kinds. Instances are
--- also provided for datatypes exported from base. A poly-kinded instance
--- is /not/ provided, as a recursive definition for algebraic kinds is
--- generally more useful.
-type family (a :: k) == (b :: k) :: Bool
 infix 4 ==
 
-{-
-This comment explains more about why a poly-kinded instance for (==) is
-not provided. To be concrete, here would be the poly-kinded instance:
-
-type family EqPoly (a :: k) (b :: k) where
- EqPoly a a = True
- EqPoly a b = False
-type instance (a :: k) == (b :: k) = EqPoly a b
-
-Note that this overlaps with every other instance -- if this were defined,
-it would be the only instance for (==).
-
-Now, consider
-data Nat = Zero | Succ Nat
-
-Suppose I want
-foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)
-foo = Refl
-
-This would not type-check with the poly-kinded instance. `Succ n == Succ m`
-quickly becomes `EqPoly (Succ n) (Succ m)` but then is stuck. We don't know
-enough about `n` and `m` to reduce further.
-
-On the other hand, consider this:
-
-type family EqNat (a :: Nat) (b :: Nat) where
- EqNat Zero     Zero     = True
- EqNat (Succ n) (Succ m) = EqNat n m
- EqNat n        m        = False
-type instance (a :: Nat) == (b :: Nat) = EqNat a b
-
-With this instance, `foo` type-checks fine. `Succ n == Succ m` becomes `EqNat
-(Succ n) (Succ m)` which becomes `EqNat n m`. Thus, we can conclude `(n == m)
-~ True` as desired.
-
-So, the Nat-specific instance allows strictly more reductions, and is thus
-preferable to the poly-kinded instance. But, if we introduce the poly-kinded
-instance, we are barred from writing the Nat-specific instance, due to
-overlap.
-
-Even better than the current instance for * would be one that does this sort
-of recursion for all datatypes, something like this:
-
-type family EqStar (a :: *) (b :: *) where
- EqStar Bool Bool = True
- EqStar (a,b) (c,d) = a == c && b == d
- EqStar (Maybe a) (Maybe b) = a == b
- ...
- EqStar a b = False
-
-The problem is the (...) is extensible -- we would want to add new cases for
-all datatypes in scope. This is not currently possible for closed type
-families.
--}
-
--- all of the following closed type families are local to this module
-type family EqStar (a :: *) (b :: *) where
-  EqStar a a = 'True
-  EqStar a b = 'False
-
--- This looks dangerous, but it isn't. This allows == to be defined
--- over arbitrary type constructors.
-type family EqArrow (a :: k1 -> k2) (b :: k1 -> k2) where
-  EqArrow a a = 'True
-  EqArrow a b = 'False
-
-type family EqBool a b where
-  EqBool 'True  'True  = 'True
-  EqBool 'False 'False = 'True
-  EqBool a      b      = 'False
-
-type family EqOrdering a b where
-  EqOrdering 'LT 'LT = 'True
-  EqOrdering 'EQ 'EQ = 'True
-  EqOrdering 'GT 'GT = 'True
-  EqOrdering a   b   = 'False
-
-type EqUnit (a :: ()) (b :: ()) = 'True
-
-type family EqList a b where
-  EqList '[]        '[]        = 'True
-  EqList (h1 ': t1) (h2 ': t2) = (h1 == h2) && (t1 == t2)
-  EqList a          b          = 'False
-
-type family EqMaybe a b where
-  EqMaybe 'Nothing   'Nothing  = 'True
-  EqMaybe ('Just x) ('Just y)  = x == y
-  EqMaybe a         b          = 'False
-
-type family Eq2 a b where
-  Eq2 '(a1, b1) '(a2, b2) = a1 == a2 && b1 == b2
-
-type family Eq3 a b where
-  Eq3 '(a1, b1, c1) '(a2, b2, c2) = a1 == a2 && b1 == b2 && c1 == c2
-
-type family Eq4 a b where
-  Eq4 '(a1, b1, c1, d1) '(a2, b2, c2, d2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2
-
-type family Eq5 a b where
-  Eq5 '(a1, b1, c1, d1, e1) '(a2, b2, c2, d2, e2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2
-
-type family Eq6 a b where
-  Eq6 '(a1, b1, c1, d1, e1, f1) '(a2, b2, c2, d2, e2, f2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2
-
-type family Eq7 a b where
-  Eq7 '(a1, b1, c1, d1, e1, f1, g1) '(a2, b2, c2, d2, e2, f2, g2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2
-
-type family Eq8 a b where
-  Eq8 '(a1, b1, c1, d1, e1, f1, g1, h1) '(a2, b2, c2, d2, e2, f2, g2, h2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2
-
-type family Eq9 a b where
-  Eq9 '(a1, b1, c1, d1, e1, f1, g1, h1, i1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2
-
-type family Eq10 a b where
-  Eq10 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2
-
-type family Eq11 a b where
-  Eq11 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2
-
-type family Eq12 a b where
-  Eq12 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2
-
-type family Eq13 a b where
-  Eq13 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2
-
-type family Eq14 a b where
-  Eq14 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2 && n1 == n2
-
-type family Eq15 a b where
-  Eq15 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2 && n1 == n2 && o1 == o2
-
--- these all look to be overlapping, but they are differentiated by their kinds
-type instance a == b = EqStar a b
-type instance a == b = EqArrow a b
-type instance a == b = EqBool a b
-type instance a == b = EqOrdering a b
-type instance a == b = EqUnit a b
-type instance a == b = EqList a b
-type instance a == b = EqMaybe a b
-type instance a == b = Eq2 a b
-type instance a == b = Eq3 a b
-type instance a == b = Eq4 a b
-type instance a == b = Eq5 a b
-type instance a == b = Eq6 a b
-type instance a == b = Eq7 a b
-type instance a == b = Eq8 a b
-type instance a == b = Eq9 a b
-type instance a == b = Eq10 a b
-type instance a == b = Eq11 a b
-type instance a == b = Eq12 a b
-type instance a == b = Eq13 a b
-type instance a == b = Eq14 a b
-type instance a == b = Eq15 a b
+-- | A type family to compute Boolean equality.
+type family (a :: k) == (b :: k) :: Bool where
+  f a == g b = f == g && a == b
+  a == a = 'True
+  _ == _ = 'False
+
+-- The idea here is to recognize equality of *applications* using
+-- the first case, and of *constructors* using the second and third
+-- ones. It would be wonderful if GHC recognized that the
+-- first and second cases are compatible, which would allow us to
+-- prove
+--
+-- a ~ b => a == b
+--
+-- but it (understandably) does not.
+--
+-- It is absolutely critical that the three cases occur in precisely
+-- this order. In particular, if
+--
+-- a == a = 'True
+--
+-- came first, then the type application case would only be reached
+-- (uselessly) when GHC discovered that the types were not equal.
+--
+-- One might reasonably ask what's wrong with a simpler version:
+--
+-- type family (a :: k) == (b :: k) where
+--  a == a = True
+--  a == b = False
+--
+-- Consider
+-- data Nat = Zero | Succ Nat
+--
+-- Suppose I want
+-- foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)
+-- foo = Refl
+--
+-- This would not type-check with the simple version. `Succ n == Succ m`
+-- is stuck. We don't know enough about `n` and `m` to reduce the family.
+-- With the recursive version, `Succ n == Succ m` reduces to
+-- `Succ == Succ && n == m`, which can reduce to `'True && n == m` and
+-- finally to `n == m`.
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 0964db98ba..0ea866a5bb 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -9,7 +9,6 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE UndecidableInstances #-}  -- for compiling instances of (==)
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PolyKinds #-}
@@ -44,7 +43,7 @@ module GHC.TypeLits
 
   ) where
 
-import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise)
+import GHC.Base(Eq(..), Ord(..), Ordering(..), otherwise)
 import GHC.Types( Nat, Symbol )
 import GHC.Num(Integer, fromInteger)
 import GHC.Base(String)
@@ -54,7 +53,7 @@ import GHC.Real(toInteger)
 import GHC.Prim(magicDict, Proxy#)
 import Data.Maybe(Maybe(..))
 import Data.Proxy (Proxy(..))
-import Data.Type.Equality(type (==), (:~:)(Refl))
+import Data.Type.Equality((:~:)(Refl))
 import Unsafe.Coerce(unsafeCoerce)
 
 import GHC.TypeNats (KnownNat)
@@ -122,11 +121,6 @@ instance Show SomeSymbol where
 instance Read SomeSymbol where
   readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
 
-type family EqSymbol (a :: Symbol) (b :: Symbol) where
-  EqSymbol a a = 'True
-  EqSymbol a b = 'False
-type instance a == b = EqSymbol a b
-
 --------------------------------------------------------------------------------
 
 -- | Comparison of type-level symbols, as a function.
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index cb75367ac8..7d9ca0d8e4 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/libraries/base/GHC/TypeNats.hs
@@ -9,7 +9,6 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE UndecidableInstances #-}  -- for compiling instances of (==)
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PolyKinds #-}
@@ -37,7 +36,7 @@ module GHC.TypeNats
 
   ) where
 
-import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise)
+import GHC.Base(Eq(..), Ord(..), Bool(True), Ordering(..), otherwise)
 import GHC.Types( Nat )
 import GHC.Natural(Natural)
 import GHC.Show(Show(..))
@@ -45,7 +44,7 @@ import GHC.Read(Read(..))
 import GHC.Prim(magicDict, Proxy#)
 import Data.Maybe(Maybe(..))
 import Data.Proxy (Proxy(..))
-import Data.Type.Equality(type (==), (:~:)(Refl))
+import Data.Type.Equality((:~:)(Refl))
 import Unsafe.Coerce(unsafeCoerce)
 
 --------------------------------------------------------------------------------
@@ -95,11 +94,6 @@ instance Read SomeNat where
   readsPrec p xs = do (a,ys) <- readsPrec p xs
                       [(someNatVal a, ys)]
 
-type family EqNat (a :: Nat) (b :: Nat) where
-  EqNat a a = 'True
-  EqNat a b = 'False
-type instance a == b = EqNat a b
-
 --------------------------------------------------------------------------------
 
 infix  4 <=?, <=
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index 047f6d9f5b..0ef50731bf 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -20,6 +20,14 @@
 
   * Remove the deprecated `Typeable{1..7}` type synonyms (#14047)
 
+  * Make `Data.Type.Equality.==` a closed type family. It now works for all
+  kinds out of the box. Any modules that previously declared instances of this
+  family will need to remove them. Whereas the previous definition was somewhat
+  ad hoc, the behavior is now completely uniform. As a result, some applications
+  that used to reduce no longer do, and conversely. Most notably, `(==)` no
+  longer treats the `*`, `j -> k`, or `()` kinds specially; equality is
+  tested structurally in all cases.
+
   * Add instances `Semigroup` and `Monoid` for `Control.Monad.ST` (#14107).
 
   * The `Read` instances for `Proxy`, `Coercion`, `(:~:)`, `(:~~:)`, and `U1`