Add kind equalities to GHC.

This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

13 files changed, 146 insertions, 75 deletions

diff --git a/libraries/base/Data/Coerce.hs b/libraries/base/Data/Coerce.hs
index 23c37967df..bb98393210 100644
--- a/libraries/base/Data/Coerce.hs
+++ b/libraries/base/Data/Coerce.hs
@@ -26,5 +26,4 @@ module Data.Coerce
 import GHC.Prim (coerce)
 import GHC.Types (Coercible)
 
-import GHC.Base () -- for build ordering
-
+import GHC.Base () -- for build ordering; see Notes in GHC.Base for more info
diff --git a/libraries/base/Data/Kind.hs b/libraries/base/Data/Kind.hs
new file mode 100644
index 0000000000..348301347c
--- /dev/null
+++ b/libraries/base/Data/Kind.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE Trustworthy, ExplicitNamespaces #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Kind
+-- License     :  BSD-style (see the LICENSE file in the distribution)
+--
+-- Maintainer  :  libraries@haskell.org
+-- Stability   :  experimental
+-- Portability :  not portable
+--
+-- Basic kinds
+--
+-- @since 4.9.0.0
+-----------------------------------------------------------------------------
+
+module Data.Kind ( Type, Constraint, type (*), type (★) ) where
+
+import GHC.Types
diff --git a/libraries/base/Data/Monoid.hs b/libraries/base/Data/Monoid.hs
index f60a15fb58..0a33c27cac 100644
--- a/libraries/base/Data/Monoid.hs
+++ b/libraries/base/Data/Monoid.hs
@@ -235,4 +235,3 @@ prop_mconcatLast x =
         where listLastToMaybe [] = Nothing
               listLastToMaybe lst = Just (last lst)
 -- -}
-
diff --git a/libraries/base/Data/Type/Coercion.hs b/libraries/base/Data/Type/Coercion.hs
index f9f64c1439..c85af5b282 100644
--- a/libraries/base/Data/Type/Coercion.hs
+++ b/libraries/base/Data/Type/Coercion.hs
@@ -52,19 +52,17 @@ data Coercion a b where
 -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif
 -- for 'type-eq'
 
-newtype Sym a b = Sym { unsym :: Coercion b a }
-
 -- | Type-safe cast, using representational equality
 coerceWith :: Coercion a b -> a -> b
 coerceWith Coercion x = coerce x
 
 -- | Symmetry of representational equality
-sym :: forall a b. Coercion a b -> Coercion b a
-sym Coercion = unsym (coerce (Sym Coercion :: Sym a a))
+sym :: Coercion a b -> Coercion b a
+sym Coercion = Coercion
 
 -- | Transitivity of representational equality
 trans :: Coercion a b -> Coercion b c -> Coercion a c
-trans c Coercion = coerce c
+trans Coercion Coercion = Coercion
 
 -- | Convert propositional (nominal) equality to representational equality
 repr :: (a Eq.:~: b) -> Coercion a b
@@ -98,4 +96,4 @@ instance TestCoercion ((Eq.:~:) a) where
   testCoercion Eq.Refl Eq.Refl = Just Coercion
 
 instance TestCoercion (Coercion a) where
-  testCoercion c Coercion = Just $ coerce (sym c)
+  testCoercion Coercion Coercion = Just Coercion
diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs
index 59d4ea3455..a021fa7b9a 100644
--- a/libraries/base/Data/Type/Equality.hs
+++ b/libraries/base/Data/Type/Equality.hs
@@ -1,15 +1,17 @@
-{-# LANGUAGE DeriveGeneric        #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE StandaloneDeriving   #-}
-{-# LANGUAGE NoImplicitPrelude    #-}
-{-# LANGUAGE PolyKinds            #-}
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE ExplicitNamespaces   #-}
+{-# LANGUAGE DeriveGeneric          #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE StandaloneDeriving     #-}
+{-# LANGUAGE NoImplicitPrelude      #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE ExplicitNamespaces     #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FunctionalDependencies #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -29,9 +31,9 @@
 
 
 module Data.Type.Equality (
-  -- * The equality type
-  (:~:)(..),
-  
+  -- * The equality types
+  (:~:)(..), type (~~),
+
   -- * Working with equality
   sym, trans, castWith, gcastWith, apply, inner, outer,
 
@@ -49,6 +51,16 @@ import GHC.Read
 import GHC.Base
 import Data.Type.Bool
 
+-- | Lifted, homogeneous equality. By lifted, we mean that it can be
+-- bogus (deferred type error). By homogeneous, the two types @a@
+-- and @b@ must have the same kind.
+class a ~~ b => (a :: k) ~ (b :: k) | a -> b, b -> a
+  -- NB: Not exported, as (~) is magical syntax. That's also why there's
+  -- no fixity.
+instance {-# INCOHERENT #-} a ~~ b => a ~ b
+  -- incoherent because we want to use this instance eagerly, even when
+  -- the tyvars are partially unknown.
+
 infix 4 :~:
 
 -- | Propositional equality. If @a :~: b@ is inhabited by some terminating
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 4379155c57..86ced96b12 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -44,9 +44,10 @@ module Data.Typeable.Internal (
     tcBool, tc'True, tc'False,
     tcOrdering, tc'LT, tc'EQ, tc'GT,
     tcChar, tcInt, tcWord, tcFloat, tcDouble, tcFun,
-    tcIO, tcSPEC, tcTyCon, tcModule,
-    tcCoercible, tcList, tcEq,
-    tcLiftedKind, tcUnliftedKind, tcOpenKind, tcBOX, tcConstraint, tcAnyK,
+    tcIO, tcSPEC, tcTyCon, tcModule, tcTrName,
+    tcCoercible, tcList, tcHEq,
+    tcConstraint,
+    tcTYPE, tcLevity, tc'Lifted, tc'Unlifted,
 
     funTc,  -- ToDo
 
@@ -403,8 +404,8 @@ mkGhcTypesTyCon name = mkTyCon3# "ghc-prim"# "GHC.Types"# name
 tcBool, tc'True, tc'False,
   tcOrdering, tc'GT, tc'EQ, tc'LT,
   tcChar, tcInt, tcWord, tcFloat, tcDouble, tcFun,
-  tcIO, tcSPEC, tcTyCon, tcModule,
-  tcCoercible, tcEq, tcList :: TyCon
+  tcIO, tcSPEC, tcTyCon, tcModule, tcTrName,
+  tcCoercible, tcHEq, tcList :: TyCon
 
 tcBool      = mkGhcTypesTyCon "Bool"#      -- Bool is promotable
 tc'True     = mkGhcTypesTyCon "'True"#
@@ -415,28 +416,28 @@ tc'EQ       = mkGhcTypesTyCon "'EQ"#
 tc'LT       = mkGhcTypesTyCon "'LT"#
 
 -- None of the rest are promotable (see TysWiredIn)
-tcChar      = mkGhcTypesTyCon "Char"#
-tcInt       = mkGhcTypesTyCon "Int"#
-tcWord      = mkGhcTypesTyCon "Word"#
-tcFloat     = mkGhcTypesTyCon "Float"#
-tcDouble    = mkGhcTypesTyCon "Double"#
-tcSPEC      = mkGhcTypesTyCon "SPEC"#
-tcIO        = mkGhcTypesTyCon "IO"#
-tcTyCon     = mkGhcTypesTyCon "TyCon"#
-tcModule    = mkGhcTypesTyCon "Module"#
-tcCoercible = mkGhcTypesTyCon "Coercible"#
+tcChar       = mkGhcTypesTyCon "Char"#
+tcInt        = mkGhcTypesTyCon "Int"#
+tcWord       = mkGhcTypesTyCon "Word"#
+tcFloat      = mkGhcTypesTyCon "Float"#
+tcDouble     = mkGhcTypesTyCon "Double"#
+tcSPEC       = mkGhcTypesTyCon "SPEC"#
+tcIO         = mkGhcTypesTyCon "IO"#
+tcTyCon      = mkGhcTypesTyCon "TyCon"#
+tcModule     = mkGhcTypesTyCon "Module"#
+tcTrName     = mkGhcTypesTyCon "TrName"#
+tcCoercible  = mkGhcTypesTyCon "Coercible"#
 
 tcFun       = mkGhcTypesTyCon "->"#
 tcList      = mkGhcTypesTyCon "[]"#   -- Type rep for the list type constructor
-tcEq        = mkGhcTypesTyCon "~"#    -- Type rep for the (~) type constructor
-
-tcLiftedKind, tcUnliftedKind, tcOpenKind, tcBOX, tcConstraint, tcAnyK :: TyCon
-tcLiftedKind   = mkGhcTypesTyCon "*"#
-tcUnliftedKind = mkGhcTypesTyCon "#"#
-tcOpenKind     = mkGhcTypesTyCon "#"#
-tcBOX          = mkGhcTypesTyCon "BOX"#
-tcAnyK         = mkGhcTypesTyCon "AnyK"#
+tcHEq       = mkGhcTypesTyCon "~~"#   -- Type rep for the (~~) type constructor
+
+tcConstraint, tcTYPE, tcLevity, tc'Lifted, tc'Unlifted :: TyCon
 tcConstraint   = mkGhcTypesTyCon "Constraint"#
+tcTYPE         = mkGhcTypesTyCon "TYPE"#
+tcLevity       = mkGhcTypesTyCon "Levity"#
+tc'Lifted      = mkGhcTypesTyCon "'Lifted"#
+tc'Unlifted    = mkGhcTypesTyCon "'Unlifted"#
 
 funTc :: TyCon
 funTc = tcFun   -- Legacy
@@ -463,4 +464,3 @@ typeSymbolTypeRep p = typeLitTypeRep (show (symbolVal' p))
 -- | An internal function, to make representations for type literals.
 typeLitTypeRep :: String -> TypeRep
 typeLitTypeRep nm = mkTyConApp (mkTypeLitTyCon nm) []
-
diff --git a/libraries/base/GHC/Base.hs b/libraries/base/GHC/Base.hs
index 199664d9db..90eaaf0a1e 100644
--- a/libraries/base/GHC/Base.hs
+++ b/libraries/base/GHC/Base.hs
@@ -1,4 +1,17 @@
 {-
+
+NOTA BENE: Do NOT use ($) anywhere in this module! The type of ($) is
+slightly magical (it can return unlifted types), and it is wired in.
+But, it is also *defined* in this module, with a non-magical type.
+GHC gets terribly confused (and *hangs*) if you try to use ($) in this
+module, because it has different types in different scenarios.
+
+This is not a problem in general, because the type ($), being wired in, is not
+written out to the interface file, so importing files don't get confused.
+The problem is only if ($) is used here. So don't!
+
+---------------------------------------------
+
 The overall structure of the GHC Prelude is a bit tricky.
 
   a) We want to avoid "orphan modules", i.e. ones with instance
@@ -1086,13 +1099,13 @@ instance Alternative IO where
 instance MonadPlus IO
 
 returnIO :: a -> IO a
-returnIO x = IO $ \ s -> (# s, x #)
+returnIO x = IO (\ s -> (# s, x #))
 
 bindIO :: IO a -> (a -> IO b) -> IO b
-bindIO (IO m) k = IO $ \ s -> case m s of (# new_s, a #) -> unIO (k a) new_s
+bindIO (IO m) k = IO (\ s -> case m s of (# new_s, a #) -> unIO (k a) new_s)
 
 thenIO :: IO a -> IO b -> IO b
-thenIO (IO m) k = IO $ \ s -> case m s of (# new_s, _ #) -> unIO k new_s
+thenIO (IO m) k = IO (\ s -> case m s of (# new_s, _ #) -> unIO k new_s)
 
 unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #))
 unIO (IO a) = a
diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs
index ffc27d11eb..032e650c1e 100755
--- a/libraries/base/GHC/Exts.hs
+++ b/libraries/base/GHC/Exts.hs
@@ -53,6 +53,12 @@ module GHC.Exts
         -- @since 4.7.0.0
         Data.Coerce.coerce, Data.Coerce.Coercible,
 
+        -- * Equality
+        type (~~),
+
+        -- * Levity polymorphism
+        GHC.Prim.TYPE, Levity(..),
+
         -- * Transform comprehensions
         Down(..), groupWith, sortWith, the,
 
@@ -72,8 +78,9 @@ module GHC.Exts
         IsList(..)
        ) where
 
-import GHC.Prim hiding (coerce, Constraint)
-import GHC.Base hiding (coerce) -- implicitly comes from GHC.Prim
+import GHC.Prim hiding ( coerce, TYPE )
+import qualified GHC.Prim
+import GHC.Base hiding ( coerce )
 import GHC.Word
 import GHC.Int
 import GHC.Ptr
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 0d9f4fe61f..a51ba910e0 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -284,5 +284,3 @@ withSNat f x y = magicDict (WrapN f) x y
 withSSymbol :: (KnownSymbol a => Proxy a -> b)
             -> SSymbol a      -> Proxy a -> b
 withSSymbol f x y = magicDict (WrapS f) x y
-
-
diff --git a/libraries/base/base.cabal b/libraries/base/base.cabal
index 684fabb14e..6261c446b8 100644
--- a/libraries/base/base.cabal
+++ b/libraries/base/base.cabal
@@ -148,6 +148,7 @@ Library
         Data.IORef
         Data.Int
         Data.Ix
+        Data.Kind
         Data.List
         Data.List.NonEmpty
         Data.Maybe
diff --git a/libraries/base/tests/CatEntail.hs b/libraries/base/tests/CatEntail.hs
index bc2d8d2f55..c980a2db73 100644
--- a/libraries/base/tests/CatEntail.hs
+++ b/libraries/base/tests/CatEntail.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE TypeOperators, KindSignatures #-}
 module CatEntail where
 import Prelude hiding (id, (.))
-import GHC.Prim (Constraint)
+import GHC.Exts (Constraint)
 import Control.Category
 
 -- One dictionary to rule them all.
diff --git a/libraries/ghc-prim/GHC/Classes.hs b/libraries/ghc-prim/GHC/Classes.hs
index 12fe65f322..d4c6697652 100644
--- a/libraries/ghc-prim/GHC/Classes.hs
+++ b/libraries/ghc-prim/GHC/Classes.hs
@@ -678,4 +678,3 @@ class (c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16,
        c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44,
        c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58,
        c59, c60, c61, c62)
-
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index 63b4f0508f..04aecbf37f 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE MagicHash, NoImplicitPrelude, TypeFamilies, UnboxedTuples,
-             MultiParamTypeClasses, RoleAnnotations, CPP #-}
+             MultiParamTypeClasses, RoleAnnotations, CPP, TypeOperators #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  GHC.Types
@@ -29,7 +29,12 @@ module GHC.Types (
         isTrue#,
         SPEC(..),
         Nat, Symbol,
-        Coercible,
+        type (~~), Coercible,
+        TYPE, Levity(..), Type, type (*), type (★), Constraint,
+          -- The historical type * should ideally be written as
+          -- `type *`, without the parentheses. But that's a true
+          -- pain to parse, and for little gain.
+
         -- * Runtime type representation
         Module(..), TrName(..), TyCon(..)
     ) where
@@ -40,6 +45,24 @@ infixr 5 :
 
 {- *********************************************************************
 *                                                                      *
+                  Kinds
+*                                                                      *
+********************************************************************* -}
+
+-- | The kind of constraints, like @Show a@
+data Constraint
+
+-- | The kind of types with values. For example @Int :: Type@.
+type Type = TYPE 'Lifted
+
+-- | A backward-compatible (pre-GHC 8.0) synonym for 'Type'
+type * = TYPE 'Lifted
+
+-- | A unicode backward-compatible (pre-GHC 8.0) synonym for 'Type'
+type ★ = TYPE 'Lifted
+
+{- *********************************************************************
+*                                                                      *
                   Nat and Symbol
 *                                                                      *
 ********************************************************************* -}
@@ -51,7 +74,6 @@ data Nat
 -- Declared here because class IP needs it
 data Symbol
 
-
 {- *********************************************************************
 *                                                                      *
                   Lists
@@ -164,12 +186,10 @@ inside GHC, to change the kind and type.
 -}
 
 
--- | A data constructor used to box up all unlifted equalities
---
--- The type constructor is special in that GHC pretends that it
--- has kind (? -> ? -> Fact) rather than (* -> * -> *)
-data (~) a b = Eq# ((~#) a b)
-
+-- | Lifted, heterogeneous equality. By lifted, we mean that it
+-- can be bogus (deferred type error). By heterogeneous, the two
+-- types @a@ and @b@ might have different kinds.
+class a ~~ b
 
 -- | This two-parameter class has instances for types @a@ and @b@ if
 --      the compiler can infer that they have the same representation. This class
@@ -218,15 +238,7 @@ data (~) a b = Eq# ((~#) a b)
 --      by Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones and Stephanie Weirich.
 --
 --      @since 4.7.0.0
-data Coercible a b = MkCoercible ((~#) a b)
--- It's really ~R# (representational equality), not ~#,
--- but  * we don't yet have syntax for ~R#,
---      * the compiled code is the same either way
---      * TysWiredIn has the truthful types
--- Also see Note [Kind-changing of (~) and Coercible]
-
--- | Alias for 'tagToEnum#'. Returns True if its parameter is 1# and False
---   if it is 0#.
+class Coercible a b
 
 {- *********************************************************************
 *                                                                      *
@@ -237,6 +249,8 @@ data Coercible a b = MkCoercible ((~#) a b)
 data {-# CTYPE "HsBool" #-} Bool = False | True
 
 {-# INLINE isTrue# #-}
+-- | Alias for 'tagToEnum#'. Returns True if its parameter is 1# and False
+--   if it is 0#.
 isTrue# :: Int# -> Bool   -- See Note [Optimizing isTrue#]
 isTrue# x = tagToEnum# x
 
@@ -310,6 +324,18 @@ you're reading this in 2023 then things went wrong). See #8326.
 -- loops should be aggressively specialized.
 data SPEC = SPEC | SPEC2
 
+-- | GHC divides all proper types (that is, types that can perhaps be
+-- inhabited, as distinct from type constructors or type-level data)
+-- into two worlds: lifted types and unlifted types. For example,
+-- @Int@ is lifted while @Int#@ is unlifted. Certain operations need
+-- to be polymorphic in this distinction. A classic example is 'unsafeCoerce#',
+-- which needs to be able to coerce between lifted and unlifted types.
+-- To achieve this, we use kind polymorphism: lifted types have kind
+-- @TYPE Lifted@ and unlifted ones have kind @TYPE Unlifted@. 'Levity'
+-- is the kind of 'Lifted' and 'Unlifted'. @*@ is a synonym for @TYPE Lifted@
+-- and @#@ is a synonym for @TYPE Unlifted@.
+data Levity = Lifted | Unlifted
+
 {- *********************************************************************
 *                                                                      *
              Runtime represntation of TyCon