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.

8 files changed, 78 insertions, 137 deletions

diff --git a/testsuite/tests/roles/should_compile/Roles1.stderr b/testsuite/tests/roles/should_compile/Roles1.stderr
index 839d04d692..1759bab776 100644
--- a/testsuite/tests/roles/should_compile/Roles1.stderr
+++ b/testsuite/tests/roles/should_compile/Roles1.stderr
@@ -2,84 +2,42 @@ TYPE SIGNATURES
 TYPE CONSTRUCTORS
   type role T1 nominal
   data T1 a = K1 a
-    Promotable
+    Kind: * -> *
   data T2 a = K2 a
-    Promotable
+    Kind: * -> *
   type role T3 phantom
   data T3 (a :: k) = K3
+    Kind: forall k1. k1 -> *
   type role T4 nominal nominal
   data T4 (a :: * -> *) b = K4 (a b)
+    Kind: (* -> *) -> * -> *
   data T5 a = K5 a
-    Promotable
+    Kind: * -> *
   type role T6 phantom
   data T6 (a :: k) = K6
+    Kind: forall k1. k1 -> *
   type role T7 phantom representational
   data T7 (a :: k) b = K7 b
+    Kind: forall k1. k1 -> * -> *
 COERCION AXIOMS
 Dependent modules: []
 Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
                      integer-gmp-1.0.0.0]
 
 ==================== Typechecker ====================
-Roles1.$tcT7
-  = TyCon
-      12795488517584970699##
-      6852268802866176810##
-      Roles1.$trModule
-      (TrNameS "T7"#)
-Roles1.$tcT6
-  = TyCon
-      1052116432298682626##
-      4782516991847719023##
-      Roles1.$trModule
-      (TrNameS "T6"#)
-Roles1.$tcT5
-  = TyCon
-      10855726709479635304##
-      5574528370049939204##
-      Roles1.$trModule
-      (TrNameS "T5"#)
-Roles1.$tc'K5
-  = TyCon
-      17986294396600628264##
-      15784122741796850983##
-      Roles1.$trModule
-      (TrNameS "'K5"#)
-Roles1.$tcT4
-  = TyCon
-      5809060867006837344##
-      8795972313583150301##
-      Roles1.$trModule
-      (TrNameS "T4"#)
-Roles1.$tcT3
-  = TyCon
-      17827258502042208248##
-      10404219359416482652##
-      Roles1.$trModule
-      (TrNameS "T3"#)
-Roles1.$tcT2
-  = TyCon
-      14324923875690440398##
-      17626224477681351106##
-      Roles1.$trModule
-      (TrNameS "T2"#)
-Roles1.$tc'K2
-  = TyCon
-      17795591238510508397##
-      10155757471958311507##
-      Roles1.$trModule
-      (TrNameS "'K2"#)
-Roles1.$tcT1
-  = TyCon
-      12633763300352597178##
-      11103726621424210926##
-      Roles1.$trModule
-      (TrNameS "T1"#)
-Roles1.$tc'K1
-  = TyCon
-      1949157551035372857##
-      3576433963139282451##
-      Roles1.$trModule
-      (TrNameS "'K1"#)
+Roles1.$tcT7 = TyCon 0## 0## Roles1.$trModule (TrNameS "T7"#)
+Roles1.$tc'K7 = TyCon 0## 0## Roles1.$trModule (TrNameS "'K7"#)
+Roles1.$tcT6 = TyCon 0## 0## Roles1.$trModule (TrNameS "T6"#)
+Roles1.$tc'K6 = TyCon 0## 0## Roles1.$trModule (TrNameS "'K6"#)
+Roles1.$tcT5 = TyCon 0## 0## Roles1.$trModule (TrNameS "T5"#)
+Roles1.$tc'K5 = TyCon 0## 0## Roles1.$trModule (TrNameS "'K5"#)
+Roles1.$tcT4 = TyCon 0## 0## Roles1.$trModule (TrNameS "T4"#)
+Roles1.$tc'K4 = TyCon 0## 0## Roles1.$trModule (TrNameS "'K4"#)
+Roles1.$tcT3 = TyCon 0## 0## Roles1.$trModule (TrNameS "T3"#)
+Roles1.$tc'K3 = TyCon 0## 0## Roles1.$trModule (TrNameS "'K3"#)
+Roles1.$tcT2 = TyCon 0## 0## Roles1.$trModule (TrNameS "T2"#)
+Roles1.$tc'K2 = TyCon 0## 0## Roles1.$trModule (TrNameS "'K2"#)
+Roles1.$tcT1 = TyCon 0## 0## Roles1.$trModule (TrNameS "T1"#)
+Roles1.$tc'K1 = TyCon 0## 0## Roles1.$trModule (TrNameS "'K1"#)
 Roles1.$trModule = Module (TrNameS "main"#) (TrNameS "Roles1"#)
 
diff --git a/testsuite/tests/roles/should_compile/Roles13.stderr b/testsuite/tests/roles/should_compile/Roles13.stderr
index 4b7b2cb18d..0af9862d2d 100644
--- a/testsuite/tests/roles/should_compile/Roles13.stderr
+++ b/testsuite/tests/roles/should_compile/Roles13.stderr
@@ -1,6 +1,6 @@
 
 ==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 42, types: 18, coercions: 5}
+Result size of Tidy Core = {terms: 51, types: 20, coercions: 5}
 
 -- RHS size: {terms: 2, types: 0, coercions: 0}
 a :: TrName
@@ -20,43 +20,53 @@ Roles13.$trModule = Module a a1
 -- RHS size: {terms: 2, types: 0, coercions: 0}
 a2 :: TrName
 [GblId, Caf=NoCafRefs, Str=DmdType]
-a2 = TrNameS "Age"#
+a2 = TrNameS "'MkAge"#
 
 -- RHS size: {terms: 5, types: 0, coercions: 0}
-Roles13.$tcAge :: TyCon
+Roles13.$tc'MkAge :: TyCon
 [GblId[ReflectionId], Caf=NoCafRefs, Str=DmdType]
-Roles13.$tcAge = TyCon 0## 0## Roles13.$trModule a2
+Roles13.$tc'MkAge = TyCon 0## 0## Roles13.$trModule a2
 
 -- RHS size: {terms: 2, types: 0, coercions: 0}
 a3 :: TrName
 [GblId, Caf=NoCafRefs, Str=DmdType]
-a3 = TrNameS "'MkWrap"#
+a3 = TrNameS "Age"#
 
 -- RHS size: {terms: 5, types: 0, coercions: 0}
-Roles13.$tc'MkWrap :: TyCon
+Roles13.$tcAge :: TyCon
 [GblId[ReflectionId], Caf=NoCafRefs, Str=DmdType]
-Roles13.$tc'MkWrap = TyCon 0## 0## Roles13.$trModule a3
+Roles13.$tcAge = TyCon 0## 0## Roles13.$trModule a3
 
 -- RHS size: {terms: 2, types: 0, coercions: 0}
 a4 :: TrName
 [GblId, Caf=NoCafRefs, Str=DmdType]
-a4 = TrNameS "Wrap"#
+a4 = TrNameS "'MkWrap"#
+
+-- RHS size: {terms: 5, types: 0, coercions: 0}
+Roles13.$tc'MkWrap :: TyCon
+[GblId[ReflectionId], Caf=NoCafRefs, Str=DmdType]
+Roles13.$tc'MkWrap = TyCon 0## 0## Roles13.$trModule a4
+
+-- RHS size: {terms: 2, types: 0, coercions: 0}
+a5 :: TrName
+[GblId, Caf=NoCafRefs, Str=DmdType]
+a5 = TrNameS "Wrap"#
 
 -- RHS size: {terms: 5, types: 0, coercions: 0}
 Roles13.$tcWrap :: TyCon
 [GblId[ReflectionId], Caf=NoCafRefs, Str=DmdType]
-Roles13.$tcWrap = TyCon 0## 0## Roles13.$trModule a4
+Roles13.$tcWrap = TyCon 0## 0## Roles13.$trModule a5
 
 -- RHS size: {terms: 2, types: 2, coercions: 0}
-a5 :: Wrap Age -> Wrap Age
+a6 :: Wrap Age -> Wrap Age
 [GblId, Arity=1, Caf=NoCafRefs, Str=DmdType]
-a5 = \ (ds :: Wrap Age) -> ds
+a6 = \ (ds :: Wrap Age) -> ds
 
 -- RHS size: {terms: 1, types: 0, coercions: 5}
 convert :: Wrap Age -> Int
 [GblId, Arity=1, Caf=NoCafRefs, Str=DmdType]
 convert =
-  a5
+  a6
   `cast` (<Wrap Age>_R -> Roles13.NTCo:Wrap[0] Roles13.NTCo:Age[0]
           :: (Wrap Age -> Wrap Age) ~R# (Wrap Age -> Int))
 
diff --git a/testsuite/tests/roles/should_compile/Roles14.stderr b/testsuite/tests/roles/should_compile/Roles14.stderr
index 08e3b8c504..52333753da 100644
--- a/testsuite/tests/roles/should_compile/Roles14.stderr
+++ b/testsuite/tests/roles/should_compile/Roles14.stderr
@@ -11,11 +11,8 @@ Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
                      integer-gmp-1.0.0.0]
 
 ==================== Typechecker ====================
-Roles12.$tcC2
-  = TyCon
-      4006088231579841122##
-      4783761708993822739##
-      Roles12.$trModule
-      (TrNameS "C2"#)
+Roles12.$tcC2 = TyCon 0## 0## Roles12.$trModule (TrNameS "C2"#)
+Roles12.$tc'D:C2
+  = TyCon 0## 0## Roles12.$trModule (TrNameS "'D:C2"#)
 Roles12.$trModule = Module (TrNameS "main"#) (TrNameS "Roles12"#)
 
diff --git a/testsuite/tests/roles/should_compile/Roles2.stderr b/testsuite/tests/roles/should_compile/Roles2.stderr
index d885534a8d..0b8a8e0336 100644
--- a/testsuite/tests/roles/should_compile/Roles2.stderr
+++ b/testsuite/tests/roles/should_compile/Roles2.stderr
@@ -1,25 +1,19 @@
 TYPE SIGNATURES
 TYPE CONSTRUCTORS
   data T1 a = K1 (IO a)
+    Kind: * -> *
   type role T2 phantom
   data T2 a = K2 (FunPtr a)
+    Kind: * -> *
 COERCION AXIOMS
 Dependent modules: []
 Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
                      integer-gmp-1.0.0.0]
 
 ==================== Typechecker ====================
-Roles2.$tcT2
-  = TyCon
-      5934726586329293381##
-      1923031187495159753##
-      Roles2.$trModule
-      (TrNameS "T2"#)
-Roles2.$tcT1
-  = TyCon
-      13879106829711353992##
-      15151456821588362072##
-      Roles2.$trModule
-      (TrNameS "T1"#)
+Roles2.$tcT2 = TyCon 0## 0## Roles2.$trModule (TrNameS "T2"#)
+Roles2.$tc'K2 = TyCon 0## 0## Roles2.$trModule (TrNameS "'K2"#)
+Roles2.$tcT1 = TyCon 0## 0## Roles2.$trModule (TrNameS "T1"#)
+Roles2.$tc'K1 = TyCon 0## 0## Roles2.$trModule (TrNameS "'K1"#)
 Roles2.$trModule = Module (TrNameS "main"#) (TrNameS "Roles2"#)
 
diff --git a/testsuite/tests/roles/should_compile/Roles3.stderr b/testsuite/tests/roles/should_compile/Roles3.stderr
index f09760224a..e2f304dc56 100644
--- a/testsuite/tests/roles/should_compile/Roles3.stderr
+++ b/testsuite/tests/roles/should_compile/Roles3.stderr
@@ -7,13 +7,15 @@ TYPE CONSTRUCTORS
     meth2 :: a ~ b => a -> b
     {-# MINIMAL meth2 #-}
   class C3 a b where
-    type family F3 b :: * open
+    type family F3 b open
+      Kind: * -> *
     meth3 :: a -> F3 b -> F3 b
     {-# MINIMAL meth3 #-}
   class C4 a b where
     meth4 :: a -> F4 b -> F4 b
     {-# MINIMAL meth4 #-}
-  type family F4 a :: * open
+  type family F4 a open
+    Kind: * -> *
   type Syn1 a = F4 a
   type Syn2 a = [a]
 COERCION AXIOMS
@@ -29,29 +31,13 @@ Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
                      integer-gmp-1.0.0.0]
 
 ==================== Typechecker ====================
-Roles3.$tcC4
-  = TyCon
-      12861862461396457184##
-      6389612623460961504##
-      Roles3.$trModule
-      (TrNameS "C4"#)
-Roles3.$tcC3
-  = TyCon
-      5998139369941479154##
-      6816352641934636458##
-      Roles3.$trModule
-      (TrNameS "C3"#)
-Roles3.$tcC2
-  = TyCon
-      8833962732139387711##
-      7891126688522429937##
-      Roles3.$trModule
-      (TrNameS "C2"#)
-Roles3.$tcC1
-  = TyCon
-      16242970448469140073##
-      10229725431456576413##
-      Roles3.$trModule
-      (TrNameS "C1"#)
+Roles3.$tcC4 = TyCon 0## 0## Roles3.$trModule (TrNameS "C4"#)
+Roles3.$tc'D:C4 = TyCon 0## 0## Roles3.$trModule (TrNameS "'D:C4"#)
+Roles3.$tcC3 = TyCon 0## 0## Roles3.$trModule (TrNameS "C3"#)
+Roles3.$tc'D:C3 = TyCon 0## 0## Roles3.$trModule (TrNameS "'D:C3"#)
+Roles3.$tcC2 = TyCon 0## 0## Roles3.$trModule (TrNameS "C2"#)
+Roles3.$tc'D:C2 = TyCon 0## 0## Roles3.$trModule (TrNameS "'D:C2"#)
+Roles3.$tcC1 = TyCon 0## 0## Roles3.$trModule (TrNameS "C1"#)
+Roles3.$tc'D:C1 = TyCon 0## 0## Roles3.$trModule (TrNameS "'D:C1"#)
 Roles3.$trModule = Module (TrNameS "main"#) (TrNameS "Roles3"#)
 
diff --git a/testsuite/tests/roles/should_compile/Roles4.stderr b/testsuite/tests/roles/should_compile/Roles4.stderr
index 67b75cde86..fb6e88a597 100644
--- a/testsuite/tests/roles/should_compile/Roles4.stderr
+++ b/testsuite/tests/roles/should_compile/Roles4.stderr
@@ -16,17 +16,9 @@ Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
                      integer-gmp-1.0.0.0]
 
 ==================== Typechecker ====================
-Roles4.$tcC3
-  = TyCon
-      16502190608089501863##
-      13971441568961069854##
-      Roles4.$trModule
-      (TrNameS "C3"#)
-Roles4.$tcC1
-  = TyCon
-      11951908835899020229##
-      6518430686554778113##
-      Roles4.$trModule
-      (TrNameS "C1"#)
+Roles4.$tcC3 = TyCon 0## 0## Roles4.$trModule (TrNameS "C3"#)
+Roles4.$tc'D:C3 = TyCon 0## 0## Roles4.$trModule (TrNameS "'D:C3"#)
+Roles4.$tcC1 = TyCon 0## 0## Roles4.$trModule (TrNameS "C1"#)
+Roles4.$tc'D:C1 = TyCon 0## 0## Roles4.$trModule (TrNameS "'D:C1"#)
 Roles4.$trModule = Module (TrNameS "main"#) (TrNameS "Roles4"#)
 
diff --git a/testsuite/tests/roles/should_compile/T8958.stderr b/testsuite/tests/roles/should_compile/T8958.stderr
index efb7488564..9ffe72ad16 100644
--- a/testsuite/tests/roles/should_compile/T8958.stderr
+++ b/testsuite/tests/roles/should_compile/T8958.stderr
@@ -5,7 +5,7 @@ TYPE SIGNATURES
 TYPE CONSTRUCTORS
   type role Map nominal representational
   newtype (Nominal k, Representational v) => Map k v = MkMap [(k, v)]
-    Promotable
+    Kind: * -> * -> *
   class Nominal a
   type role Representational representational
   class Representational a
@@ -25,8 +25,12 @@ T8958.$tcMap = TyCon 0## 0## T8958.$trModule (TrNameS "Map"#)
 T8958.$tc'MkMap = TyCon 0## 0## T8958.$trModule (TrNameS "'MkMap"#)
 T8958.$tcRepresentational
   = TyCon 0## 0## T8958.$trModule (TrNameS "Representational"#)
+T8958.$tc'D:Representational
+  = TyCon 0## 0## T8958.$trModule (TrNameS "'D:Representational"#)
 T8958.$tcNominal
   = TyCon 0## 0## T8958.$trModule (TrNameS "Nominal"#)
+T8958.$tc'D:Nominal
+  = TyCon 0## 0## T8958.$trModule (TrNameS "'D:Nominal"#)
 T8958.$trModule = Module (TrNameS "main"#) (TrNameS "T8958"#)
 AbsBinds [a] []
   {Exports: [T8958.$fRepresentationala <= $dRepresentational
diff --git a/testsuite/tests/roles/should_compile/all.T b/testsuite/tests/roles/should_compile/all.T
index b740d8ad3e..25a4a37272 100644
--- a/testsuite/tests/roles/should_compile/all.T
+++ b/testsuite/tests/roles/should_compile/all.T
@@ -1,9 +1,9 @@
-test('Roles1', only_ways('normal'), compile, ['-ddump-tc -fprint-explicit-foralls'])
-test('Roles2', only_ways('normal'), compile, ['-ddump-tc -fprint-explicit-foralls'])
-test('Roles3', only_ways('normal'), compile, ['-ddump-tc'])
-test('Roles4', only_ways('normal'), compile, ['-ddump-tc'])
+test('Roles1', only_ways('normal'), compile, ['-ddump-tc -fprint-explicit-foralls -dsuppress-uniques'])
+test('Roles2', only_ways('normal'), compile, ['-ddump-tc -fprint-explicit-foralls -dsuppress-uniques'])
+test('Roles3', only_ways('normal'), compile, ['-ddump-tc -dsuppress-uniques'])
+test('Roles4', only_ways('normal'), compile, ['-ddump-tc -dsuppress-uniques'])
 test('Roles13', only_ways('normal'), compile, ['-ddump-simpl -dsuppress-uniques'])
-test('Roles14', only_ways('normal'), compile, ['-ddump-tc'])
+test('Roles14', only_ways('normal'), compile, ['-ddump-tc -dsuppress-uniques'])
 test('T8958', [normalise_fun(normalise_errmsg), only_ways('normal')], compile, ['-ddump-tc -dsuppress-uniques'])
 test('T10263', normal, compile, [''])
 test('T9204b', extra_clean(['T9204b.o-boot', 'T9204b.hi-boot', 'T9204b2.hi', 'T9204b2.o']), multimod_compile, ['T9204b', '-v0'])