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.

16 files changed, 109 insertions, 110 deletions

diff --git a/testsuite/tests/ghci.debugger/scripts/break001.stdout b/testsuite/tests/ghci.debugger/scripts/break001.stdout
index c3146e2351..02ba1bbe93 100644
--- a/testsuite/tests/ghci.debugger/scripts/break001.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break001.stdout
@@ -1,12 +1,12 @@
 Breakpoint 0 activated at ../Test2.hs:3:1-9
 Breakpoint 1 activated at ../Test2.hs:5:1-7
 Stopped at ../Test2.hs:3:1-9
-_result :: t = _
+_result :: r = _
 Stopped at ../Test2.hs:3:7-9
 _result :: Integer = _
 x :: Integer = 1
 Stopped at ../Test2.hs:5:1-7
-_result :: t = _
+_result :: r = _
 Stopped at ../Test2.hs:5:7
 _result :: Integer = _
 y :: Integer = 1
diff --git a/testsuite/tests/ghci.debugger/scripts/break003.stderr b/testsuite/tests/ghci.debugger/scripts/break003.stderr
index bf3d2ef5a4..c19e8b45ce 100644
--- a/testsuite/tests/ghci.debugger/scripts/break003.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/break003.stderr
@@ -1,5 +1,5 @@
 
 <interactive>:4:1: error:
-    No instance for (Show (t -> t1)) arising from a use of ‘print’
+    No instance for (Show (t1 -> t)) arising from a use of ‘print’
       (maybe you haven't applied a function to enough arguments?)
     In a stmt of an interactive GHCi command: print it
diff --git a/testsuite/tests/ghci.debugger/scripts/break003.stdout b/testsuite/tests/ghci.debugger/scripts/break003.stdout
index a48f74c4c3..b1aa8ba2d2 100644
--- a/testsuite/tests/ghci.debugger/scripts/break003.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break003.stdout
@@ -1,6 +1,6 @@
 Breakpoint 0 activated at ../Test3.hs:2:18-31
 Stopped at ../Test3.hs:2:18-31
-_result :: [t1] = _
-f :: t -> t1 = _
-x :: t = _
-xs :: [t] = [_]
+_result :: [t] = _
+f :: t1 -> t = _
+x :: t1 = _
+xs :: [t1] = [_]
diff --git a/testsuite/tests/ghci.debugger/scripts/break006.stderr b/testsuite/tests/ghci.debugger/scripts/break006.stderr
index 56f40f2b21..f1567ed7ff 100644
--- a/testsuite/tests/ghci.debugger/scripts/break006.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/break006.stderr
@@ -1,14 +1,14 @@
 
 <interactive>:5:1: error:
-    No instance for (Show t1) arising from a use of ‘print’
-    Cannot resolve unknown runtime type ‘t1’
+    No instance for (Show t) arising from a use of ‘print’
+    Cannot resolve unknown runtime type ‘t’
     Use :print or :force to determine these types
-    Relevant bindings include it :: t1 (bound at <interactive>:5:1)
+    Relevant bindings include it :: t (bound at <interactive>:5:1)
     These potential instances exist:
       instance (Show a, Show b) => Show (Either a b)
         -- Defined in ‘Data.Either’
       instance Show All -- Defined in ‘Data.Monoid’
-      instance forall (k :: BOX) (f :: k -> *) (a :: k).
+      instance forall k (f :: k -> *) (a :: k).
                Show (f a) =>
                Show (Alt f a)
         -- Defined in ‘Data.Monoid’
@@ -17,15 +17,15 @@
     In a stmt of an interactive GHCi command: print it
 
 <interactive>:7:1: error:
-    No instance for (Show t1) arising from a use of ‘print’
-    Cannot resolve unknown runtime type ‘t1’
+    No instance for (Show t) arising from a use of ‘print’
+    Cannot resolve unknown runtime type ‘t’
     Use :print or :force to determine these types
-    Relevant bindings include it :: t1 (bound at <interactive>:7:1)
+    Relevant bindings include it :: t (bound at <interactive>:7:1)
     These potential instances exist:
       instance (Show a, Show b) => Show (Either a b)
         -- Defined in ‘Data.Either’
       instance Show All -- Defined in ‘Data.Monoid’
-      instance forall (k :: BOX) (f :: k -> *) (a :: k).
+      instance forall k (f :: k -> *) (a :: k).
                Show (f a) =>
                Show (Alt f a)
         -- Defined in ‘Data.Monoid’
diff --git a/testsuite/tests/ghci.debugger/scripts/break006.stdout b/testsuite/tests/ghci.debugger/scripts/break006.stdout
index 7e5edbf9d2..374fffd29a 100644
--- a/testsuite/tests/ghci.debugger/scripts/break006.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break006.stdout
@@ -1,15 +1,15 @@
 Stopped at ../Test3.hs:(1,1)-(2,31)
-_result :: [t1] = _
+_result :: [t] = _
 Stopped at ../Test3.hs:2:18-31
-_result :: [t1] = _
-f :: Integer -> t1 = _
+_result :: [t] = _
+f :: Integer -> t = _
 x :: Integer = 1
 xs :: [Integer] = [2,3]
 xs :: [Integer] = [2,3]
 x :: Integer = 1
-f :: Integer -> t1 = _
-_result :: [t1] = _
-y = (_t1::t1)
+f :: Integer -> t = _
+_result :: [t] = _
+y = (_t1::t)
 y = 2
 xs :: [Integer] = [2,3]
 x :: Integer = 1
diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout
index 88e8b3ee71..6b023718dc 100644
--- a/testsuite/tests/ghci.debugger/scripts/break012.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout
@@ -1,16 +1,16 @@
 Stopped at break012.hs:(1,1)-(5,18)
-_result :: (t, a3 -> a3, (), a2 -> a2 -> a2) = _
+_result :: (r, a3 -> a3, (), a2 -> a2 -> a2) = _
 Stopped at break012.hs:5:10-18
-_result :: (t, a3 -> a3, (), a2 -> a2 -> a2) = _
-a :: t = _
+_result :: (r, a3 -> a3, (), a2 -> a2 -> a2) = _
+a :: r = _
 b :: a4 -> a4 = _
 c :: () = _
 d :: a2 -> a2 -> a2 = _
-a :: t
+a :: r
 b :: a4 -> a4
 c :: ()
 d :: a2 -> a2 -> a2
-a = (_t1::t)
+a = (_t1::r)
 b = (_t2::a4 -> a4)
 c = (_t3::())
 d = (_t4::a2 -> a2 -> a2)
diff --git a/testsuite/tests/ghci.debugger/scripts/break018.stdout b/testsuite/tests/ghci.debugger/scripts/break018.stdout
index 11ef5476b5..d9c6b6e06a 100644
--- a/testsuite/tests/ghci.debugger/scripts/break018.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break018.stdout
@@ -1,5 +1,5 @@
 Stopped at ../mdo.hs:(30,1)-(32,27)
-_result :: IO (N a6) = _
+_result :: IO (N a7) = _
 Stopped at ../mdo.hs:(30,16)-(32,27)
 _result :: IO (N Char) = _
 x :: Char = 'h'
@@ -10,4 +10,4 @@ f :: N Char = _
 l :: N Char = _
 x :: Char = 'h'
 Stopped at ../mdo.hs:(8,1)-(9,42)
-_result :: IO (N a6) = _
+_result :: IO (N a7) = _
diff --git a/testsuite/tests/ghci.debugger/scripts/break022/break022.stdout b/testsuite/tests/ghci.debugger/scripts/break022/break022.stdout
index a87ffce942..f4b804296f 100644
--- a/testsuite/tests/ghci.debugger/scripts/break022/break022.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break022/break022.stdout
@@ -5,4 +5,4 @@ Stopped at A.hs:4:7-9
 _result :: () = _
 x :: () = ()
 Stopped at B.hs:5:1-7
-_result :: t = _
+_result :: r = _
diff --git a/testsuite/tests/ghci.debugger/scripts/break026.stdout b/testsuite/tests/ghci.debugger/scripts/break026.stdout
index 8d81867044..9afc3f470e 100644
--- a/testsuite/tests/ghci.debugger/scripts/break026.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break026.stdout
@@ -1,58 +1,58 @@
-Stopped at break026.hs:(5,1)-(7,35)

-_result :: t1 = _

-Stopped at break026.hs:5:16-22

-_result :: Integer = _

-c :: Integer = 0

-go :: Integer -> [t] -> Integer = _

-xs :: [t] = _

-Stopped at break026.hs:(6,9)-(7,35)

-_result :: t1 = _

-f :: t1 -> t -> t1 = _

-Stopped at break026.hs:7:23-35

-_result :: Integer = _

-c :: Integer = 0

-f :: Integer -> Integer -> Integer = _

-x :: Integer = 1

-xs :: [Integer] = _

-Stopped at break026.hs:(6,9)-(7,35)

-_result :: t1 = _

-f :: t1 -> t -> t1 = _

-Stopped at break026.hs:7:23-35

-_result :: t1 = _

-c :: t1 = _

-f :: t1 -> Integer -> t1 = _

-x :: Integer = 2

-xs :: [Integer] = _

-c = 1

-Stopped at break026.hs:(5,1)-(7,35)

-_result :: t1 = _

-Stopped at break026.hs:5:16-22

-_result :: Integer = _

-c :: Integer = 0

-go :: Integer -> [t] -> Integer = _

-xs :: [t] = _

-Stopped at break026.hs:(6,9)-(7,35)

-_result :: t1 = _

-f :: t1 -> t -> t1 = _

-Stopped at break026.hs:7:23-35

-_result :: Integer = _

-c :: Integer = 0

-f :: Integer -> Integer -> Integer = _

-x :: Integer = 1

-xs :: [Integer] = _

-Stopped at break026.hs:(6,9)-(7,35)

-_result :: t1 = _

-f :: t1 -> t -> t1 = _

-Stopped at break026.hs:7:23-35

-_result :: t1 = _

-c :: t1 = _

-f :: t1 -> Integer -> t1 = _

-x :: Integer = 2

-xs :: [Integer] = _

-Stopped at break026.hs:7:27-31

-_result :: Integer = _

-c :: Integer = 0

-f :: Integer -> Integer -> Integer = _

-x :: Integer = 1

-()

-1

+Stopped at break026.hs:(5,1)-(7,35)
+_result :: t = _
+Stopped at break026.hs:5:16-22
+_result :: Integer = _
+c :: Integer = 0
+go :: Integer -> [t1] -> Integer = _
+xs :: [t1] = _
+Stopped at break026.hs:(6,9)-(7,35)
+_result :: t = _
+f :: t -> t1 -> t = _
+Stopped at break026.hs:7:23-35
+_result :: Integer = _
+c :: Integer = 0
+f :: Integer -> Integer -> Integer = _
+x :: Integer = 1
+xs :: [Integer] = _
+Stopped at break026.hs:(6,9)-(7,35)
+_result :: t = _
+f :: t -> t1 -> t = _
+Stopped at break026.hs:7:23-35
+_result :: t = _
+c :: t = _
+f :: t -> Integer -> t = _
+x :: Integer = 2
+xs :: [Integer] = _
+c = 1
+Stopped at break026.hs:(5,1)-(7,35)
+_result :: t = _
+Stopped at break026.hs:5:16-22
+_result :: Integer = _
+c :: Integer = 0
+go :: Integer -> [t1] -> Integer = _
+xs :: [t1] = _
+Stopped at break026.hs:(6,9)-(7,35)
+_result :: t = _
+f :: t -> t1 -> t = _
+Stopped at break026.hs:7:23-35
+_result :: Integer = _
+c :: Integer = 0
+f :: Integer -> Integer -> Integer = _
+x :: Integer = 1
+xs :: [Integer] = _
+Stopped at break026.hs:(6,9)-(7,35)
+_result :: t = _
+f :: t -> t1 -> t = _
+Stopped at break026.hs:7:23-35
+_result :: t = _
+c :: t = _
+f :: t -> Integer -> t = _
+x :: Integer = 2
+xs :: [Integer] = _
+Stopped at break026.hs:7:27-31
+_result :: Integer = _
+c :: Integer = 0
+f :: Integer -> Integer -> Integer = _
+x :: Integer = 1
+()
+1
diff --git a/testsuite/tests/ghci.debugger/scripts/break028.stdout b/testsuite/tests/ghci.debugger/scripts/break028.stdout
index 896a2416ef..bbe47267b0 100644
--- a/testsuite/tests/ghci.debugger/scripts/break028.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break028.stdout
@@ -1,5 +1,5 @@
 Stopped at break028.hs:15:1-24
-_result :: Id a3 = _
+_result :: Id a4 = _
 Stopped at break028.hs:15:23-24
-_result :: Id a3 = _
-x' :: Id a3 = _
+_result :: Id a4 = _
+x' :: Id a4 = _
diff --git a/testsuite/tests/ghci.debugger/scripts/hist001.stdout b/testsuite/tests/ghci.debugger/scripts/hist001.stdout
index 0b58b8fcb7..3a70f6aa1e 100644
--- a/testsuite/tests/ghci.debugger/scripts/hist001.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/hist001.stdout
@@ -12,20 +12,20 @@ _result :: [a] = _
 -9  : mymap (../Test3.hs:(1,1)-(2,31))
 <end of history>
 Logged breakpoint at ../Test3.hs:(1,1)-(2,31)
-_result :: [t1]
-_result :: [t1] = _
+_result :: [t]
+_result :: [t] = _
 Logged breakpoint at ../Test3.hs:2:22-31
-_result :: [t1]
-f :: t -> t1
-xs :: [t]
-xs :: [t] = []
-f :: t -> t1 = _
-_result :: [t1] = _
+_result :: [t]
+f :: t1 -> t
+xs :: [t1]
+xs :: [t1] = []
+f :: t1 -> t = _
+_result :: [t] = _
 *** Ignoring breakpoint
 _result = []
 Logged breakpoint at ../Test3.hs:2:18-20
-_result :: t1
-f :: Integer -> t1
+_result :: t
+f :: Integer -> t
 x :: Integer
 Logged breakpoint at ../Test3.hs:2:22-31
-_result :: [t1]
+_result :: [t]
diff --git a/testsuite/tests/ghci.debugger/scripts/print018.stdout b/testsuite/tests/ghci.debugger/scripts/print018.stdout
index a00d5374dd..614b7d3657 100644
--- a/testsuite/tests/ghci.debugger/scripts/print018.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print018.stdout
@@ -3,9 +3,9 @@ Stopped at ../Test.hs:40:1-17
 _result :: () = _
 Stopped at ../Test.hs:40:10-17
 _result :: () = _
-x :: a36 = _
-x = (_t1::a36)
-x :: a36
+x :: a41 = _
+x = (_t1::a41)
+x :: a41
 ()
 x = Unary
 x :: Unary
diff --git a/testsuite/tests/ghci.debugger/scripts/print022.stdout b/testsuite/tests/ghci.debugger/scripts/print022.stdout
index 8aa539418a..85111a2c7e 100644
--- a/testsuite/tests/ghci.debugger/scripts/print022.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print022.stdout
@@ -2,9 +2,9 @@
 test = C 1 32 1.2 1.23 'x' 1 1.2 1.23
 Breakpoint 0 activated at print022.hs:11:1-7
 Stopped at print022.hs:11:1-7
-_result :: t = _
+_result :: r = _
 Stopped at print022.hs:11:7
-_result :: t = _
-x :: t = _
+_result :: r = _
+x :: r = _
 x = C2 1 (W# 32) (TwoFields 'a' 3)
 x :: T2
diff --git a/testsuite/tests/ghci.debugger/scripts/print025.stdout b/testsuite/tests/ghci.debugger/scripts/print025.stdout
index b2fcf65b1b..3936640210 100644
--- a/testsuite/tests/ghci.debugger/scripts/print025.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print025.stdout
@@ -1,7 +1,7 @@
 T 1
 Breakpoint 0 activated at print025.hs:2:1-7
 Stopped at print025.hs:2:1-7
-_result :: t = _
+_result :: r = _
 Stopped at print025.hs:2:7
 _result :: T Int s = _
 x :: T Int s = T 1
diff --git a/testsuite/tests/ghci.debugger/scripts/print031.stdout b/testsuite/tests/ghci.debugger/scripts/print031.stdout
index da3e14238d..81a2518a31 100644
--- a/testsuite/tests/ghci.debugger/scripts/print031.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print031.stdout
@@ -4,5 +4,5 @@ Stopped at print031.hs:7:1-19
 _result :: Bool = _
 Stopped at print031.hs:7:7-19
 _result :: Bool = _
-x :: t (Phantom a5) = [Just (Phantom 1)]
+x :: t (Phantom a6) = [Just (Phantom 1)]
 x = [Just (Phantom 1)]
diff --git a/testsuite/tests/ghci.debugger/scripts/print036.stdout b/testsuite/tests/ghci.debugger/scripts/print036.stdout
index d932b467a5..b9862354ab 100644
--- a/testsuite/tests/ghci.debugger/scripts/print036.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print036.stdout
@@ -1,2 +1 @@
 read = (_t1::Read a => String -> a)
-_t1 :: Read a => String -> a