diff git a/docs/users_guide/8.4.1notes.rst b/docs/users_guide/8.4.1notes.rst
 a/docs/users_guide/8.4.1notes.rst
+++ b/docs/users_guide/8.4.1notes.rst
@@ 191,6 +191,14 @@
 Blank strings can now be used as values for environment variables using the
System.Environment.Blank module. See :ghcticket:`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
 a/libraries/base/Data/Either.hs
+++ b/libraries/base/Data/Either.hs
@@ 34,8 +34,6 @@
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 _ (Right b) = b
fromRight b _ = b
 instance for the == Boolean typelevel 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
 a/libraries/base/Data/Type/Equality.hs
+++ b/libraries/base/Data/Type/Equality.hs
@@ 179,164 +179,47 @@
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 polykinded 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 polykinded instance for (==) is
not provided. To be concrete, here would be the polykinded 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 typecheck with the polykinded 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` typechecks 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 Natspecific instance allows strictly more reductions, and is thus
preferable to the polykinded instance. But, if we introduce the polykinded
instance, we are barred from writing the Natspecific 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 typecheck 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
 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 @@
) 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.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 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 typelevel symbols, as a function.
diff git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
 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,15 +36,15 @@
) 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(..))
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 @@
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
 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`