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.

5 files changed, 55 insertions, 55 deletions

diff --git a/testsuite/tests/gadt/T3163.stderr b/testsuite/tests/gadt/T3163.stderr
index 095378b540..c6b6a976da 100644
--- a/testsuite/tests/gadt/T3163.stderr
+++ b/testsuite/tests/gadt/T3163.stderr
@@ -1,5 +1,5 @@
-

-T3163.hs:8:5: error:

-    Illegal polymorphic or qualified type: forall s. s

-    In the definition of data constructor ‘Unreached’

-    In the data type declaration for ‘Taker’

+
+T3163.hs:8:5: error:
+    Illegal polymorphic or qualified type: forall s1. s1
+    In the definition of data constructor ‘Unreached’
+    In the data type declaration for ‘Taker’
diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index 39d736adb8..829dfa0e2b 100644
--- a/testsuite/tests/gadt/gadt-escape1.stderr
+++ b/testsuite/tests/gadt/gadt-escape1.stderr
@@ -1,17 +1,17 @@
 
-gadt-escape1.hs:19:58:
-    Couldn't match type ‘t’ with ‘ExpGADT Int’
-      ‘t’ is untouchable
-        inside the constraints: t1 ~ Int
-        bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int,
-                 in a case alternative
-        at gadt-escape1.hs:19:43-50
-      ‘t’ is a rigid type variable bound by
-          the inferred type of weird1 :: t at gadt-escape1.hs:19:1
-    Possible fix: add a type signature for ‘weird1’
-    Expected type: t
-      Actual type: ExpGADT t1
-    In the expression: a
-    In a case alternative: Hidden (ExpInt _) a -> a
-    Relevant bindings include
-      weird1 :: t (bound at gadt-escape1.hs:19:1)
+gadt-escape1.hs:19:58: error:
+    • Couldn't match type ‘r’ with ‘ExpGADT Int’
+        ‘r’ is untouchable
+          inside the constraints: t ~ Int
+          bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int,
+                   in a case alternative
+          at gadt-escape1.hs:19:43-50
+      ‘r’ is a rigid type variable bound by
+        the inferred type of weird1 :: r at gadt-escape1.hs:19:1
+      Possible fix: add a type signature for ‘weird1’
+      Expected type: r
+      Actual type: ExpGADT t
+    • In the expression: a
+      In a case alternative: Hidden (ExpInt _) a -> a
+    • Relevant bindings include
+        weird1 :: r (bound at gadt-escape1.hs:19:1)
diff --git a/testsuite/tests/gadt/gadt10.stderr b/testsuite/tests/gadt/gadt10.stderr
index cc5230e2f2..97bd197a2a 100644
--- a/testsuite/tests/gadt/gadt10.stderr
+++ b/testsuite/tests/gadt/gadt10.stderr
@@ -1,7 +1,7 @@
 
-gadt10.hs:6:24:
+gadt10.hs:6:24: error:
     Expecting one more argument to ‘RInt’
-    Expected kind ‘*’, but ‘RInt’ has kind ‘k0 -> *’
+    Expected a type, but ‘RInt’ has kind ‘k0 -> *’
     In the type ‘RInt’
     In the definition of data constructor ‘R’
     In the data declaration for ‘RInt’
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index ce56fe838e..44b100b059 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -1,16 +1,16 @@
 
-gadt13.hs:15:13:
-    Couldn't match expected type ‘t’
-                with actual type ‘String -> [Char]’
-      ‘t’ is untouchable
-        inside the constraints: t1 ~ Int
-        bound by a pattern with constructor: I :: Int -> Term Int,
-                 in an equation for ‘shw’
-        at gadt13.hs:15:6-8
-      ‘t’ is a rigid type variable bound by
-          the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1
-    Possible fix: add a type signature for ‘shw’
-    In the expression: ("I " ++) . shows t
-    In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
-    Relevant bindings include
-      shw :: Term t1 -> t (bound at gadt13.hs:15:1)
+gadt13.hs:15:13: error:
+    • Couldn't match expected type ‘r’
+                  with actual type ‘String -> [Char]’
+        ‘r’ is untouchable
+          inside the constraints: r1 ~ Int
+          bound by a pattern with constructor: I :: Int -> Term Int,
+                   in an equation for ‘shw’
+          at gadt13.hs:15:6-8
+      ‘r’ is a rigid type variable bound by
+        the inferred type of shw :: Term r1 -> r at gadt13.hs:15:1
+      Possible fix: add a type signature for ‘shw’
+    • In the expression: ("I " ++) . shows t
+      In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
+    • Relevant bindings include
+        shw :: Term r1 -> r (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index e49cac1577..8720d7fe10 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,19 +1,19 @@
 
-gadt7.hs:16:38:
-    Couldn't match expected type ‘t’ with actual type ‘r’
-      ‘r’ is untouchable
-        inside the constraints: t1 ~ Int
-        bound by a pattern with constructor: K :: T Int,
-                 in a case alternative
-        at gadt7.hs:16:33
+gadt7.hs:16:38: error:
+    • Couldn't match expected type ‘r’ with actual type ‘r1’
+        ‘r’ is untouchable
+          inside the constraints: t ~ Int
+          bound by a pattern with constructor: K :: T Int,
+                   in a case alternative
+          at gadt7.hs:16:33
       ‘r’ is a rigid type variable bound by
-          the inferred type of i1b :: T t1 -> r -> t at gadt7.hs:16:1
-      ‘t’ is a rigid type variable bound by
-          the inferred type of i1b :: T t1 -> r -> t at gadt7.hs:16:1
-    Possible fix: add a type signature for ‘i1b’
-    In the expression: y1
-    In a case alternative: K -> y1
-    Relevant bindings include
-      y1 :: r (bound at gadt7.hs:16:16)
-      y :: r (bound at gadt7.hs:16:7)
-      i1b :: T t1 -> r -> t (bound at gadt7.hs:16:1)
+        the inferred type of i1b :: T t -> r1 -> r at gadt7.hs:16:1
+      ‘r1’ is a rigid type variable bound by
+        the inferred type of i1b :: T t -> r1 -> r at gadt7.hs:16:1
+      Possible fix: add a type signature for ‘i1b’
+    • In the expression: y1
+      In a case alternative: K -> y1
+    • Relevant bindings include
+        y1 :: r1 (bound at gadt7.hs:16:16)
+        y :: r1 (bound at gadt7.hs:16:7)
+        i1b :: T t -> r1 -> r (bound at gadt7.hs:16:1)