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.

12 files changed, 46 insertions, 62 deletions

diff --git a/testsuite/tests/ghc-api/annotations/T10307.stdout b/testsuite/tests/ghc-api/annotations/T10307.stdout
index 26a255dca9..48cbca6cd0 100644
--- a/testsuite/tests/ghc-api/annotations/T10307.stdout
+++ b/testsuite/tests/ghc-api/annotations/T10307.stdout
@@ -12,7 +12,6 @@
 ((Test10307.hs:5:3-34,AnnDcolon), [Test10307.hs:5:31-32]),
 ((Test10307.hs:5:3-34,AnnSemi), [Test10307.hs:6:3]),
 ((Test10307.hs:5:3-34,AnnType), [Test10307.hs:5:3-6]),
-((Test10307.hs:5:34,AnnStar), [Test10307.hs:5:34]),
 ((Test10307.hs:6:3-34,AnnEqual), [Test10307.hs:6:31]),
 ((Test10307.hs:6:3-34,AnnType), [Test10307.hs:6:3-6]),
 ((Test10307.hs:6:8-34,AnnEqual), [Test10307.hs:6:31]),
diff --git a/testsuite/tests/ghc-api/annotations/T10312.stderr b/testsuite/tests/ghc-api/annotations/T10312.stderr
index 8fc7a0c0bf..e5c16948f2 100644
--- a/testsuite/tests/ghc-api/annotations/T10312.stderr
+++ b/testsuite/tests/ghc-api/annotations/T10312.stderr
@@ -1,2 +1,2 @@
-

-Test10312.hs:77:38: error: Not in scope: data constructor ‘Fixity’

+
+Test10312.hs:77:38: error: Not in scope: data constructor ‘Fixity’
diff --git a/testsuite/tests/ghc-api/annotations/T10312.stdout b/testsuite/tests/ghc-api/annotations/T10312.stdout
index 61fea45a33..00f25444cc 100644
--- a/testsuite/tests/ghc-api/annotations/T10312.stdout
+++ b/testsuite/tests/ghc-api/annotations/T10312.stdout
@@ -33,7 +33,6 @@
 ((Test10312.hs:(16,19)-(20,19),AnnVbar), [Test10312.hs:17:19]),
 ((Test10312.hs:16:21-25,AnnVal), [Test10312.hs:16:23]),
 ((Test10312.hs:16:21-29,AnnVal), [Test10312.hs:16:27]),
-((Test10312.hs:16:27,AnnStar), [Test10312.hs:16:27]),
 ((Test10312.hs:17:21-32,AnnComma), [Test10312.hs:18:19]),
 ((Test10312.hs:17:21-32,AnnLarrow), [Test10312.hs:17:23-24]),
 ((Test10312.hs:17:26-32,AnnCloseS), [Test10312.hs:17:32]),
@@ -60,7 +59,6 @@
 ((Test10312.hs:(23,20)-(27,20),AnnVbar), [Test10312.hs:24:20]),
 ((Test10312.hs:23:22-26,AnnVal), [Test10312.hs:23:24]),
 ((Test10312.hs:23:22-30,AnnVal), [Test10312.hs:23:28]),
-((Test10312.hs:23:28,AnnStar), [Test10312.hs:23:28]),
 ((Test10312.hs:24:22-33,AnnLarrow), [Test10312.hs:24:24-25]),
 ((Test10312.hs:24:22-33,AnnVbar), [Test10312.hs:25:20]),
 ((Test10312.hs:24:27-33,AnnCloseS), [Test10312.hs:24:33]),
diff --git a/testsuite/tests/ghc-api/annotations/T10357.stderr b/testsuite/tests/ghc-api/annotations/T10357.stderr
index b394ffa49b..09f29ddfb8 100644
--- a/testsuite/tests/ghc-api/annotations/T10357.stderr
+++ b/testsuite/tests/ghc-api/annotations/T10357.stderr
@@ -1,37 +1,37 @@
-

-Test10357.hs:4:13: error: Variable not in scope: one

-

-Test10357.hs:4:19: error: Variable not in scope: x

-

-Test10357.hs:5:7: error:

-    Variable not in scope: multPoly :: t3 -> t4 -> t

-

-Test10357.hs:6:10: error:

-    Variable not in scope: poly :: t0 -> [Double] -> t3

-

-Test10357.hs:6:15: error:

-    Data constructor not in scope: LE

-    Perhaps you meant ‘LT’ (imported from Prelude)

-

-Test10357.hs:7:10: error:

-    Variable not in scope: addPoly :: t5 -> t6 -> t4

-

-Test10357.hs:7:19: error:

-    Variable not in scope: poly :: t1 -> [Double] -> t7

-

-Test10357.hs:7:24: error:

-    Data constructor not in scope: LE

-    Perhaps you meant ‘LT’ (imported from Prelude)

-

-Test10357.hs:7:43: error:

-    Variable not in scope: multPoly :: t7 -> t -> t5

-

-Test10357.hs:8:19: error:

-    Variable not in scope: poly :: t2 -> [Double] -> t8

-

-Test10357.hs:8:24: error:

-    Data constructor not in scope: LE

-    Perhaps you meant ‘LT’ (imported from Prelude)

-

-Test10357.hs:8:43: error:

-    Variable not in scope: multPoly :: t8 -> t -> t6

+
+Test10357.hs:4:13: error: Variable not in scope: one
+
+Test10357.hs:4:19: error: Variable not in scope: x
+
+Test10357.hs:5:7: error:
+    Variable not in scope: multPoly :: t0 -> t1 -> t
+
+Test10357.hs:6:10: error:
+    Variable not in scope: poly :: t2 -> [Double] -> t0
+
+Test10357.hs:6:15: error:
+    Data constructor not in scope: LE
+    Perhaps you meant ‘LT’ (imported from Prelude)
+
+Test10357.hs:7:10: error:
+    Variable not in scope: addPoly :: t3 -> t4 -> t1
+
+Test10357.hs:7:19: error:
+    Variable not in scope: poly :: t6 -> [Double] -> t5
+
+Test10357.hs:7:24: error:
+    Data constructor not in scope: LE
+    Perhaps you meant ‘LT’ (imported from Prelude)
+
+Test10357.hs:7:43: error:
+    Variable not in scope: multPoly :: t5 -> t -> t3
+
+Test10357.hs:8:19: error:
+    Variable not in scope: poly :: t8 -> [Double] -> t7
+
+Test10357.hs:8:24: error:
+    Data constructor not in scope: LE
+    Perhaps you meant ‘LT’ (imported from Prelude)
+
+Test10357.hs:8:43: error:
+    Variable not in scope: multPoly :: t7 -> t -> t4
diff --git a/testsuite/tests/ghc-api/annotations/T10357.stdout b/testsuite/tests/ghc-api/annotations/T10357.stdout
index cbbb84e2ee..15d5139be5 100644
--- a/testsuite/tests/ghc-api/annotations/T10357.stdout
+++ b/testsuite/tests/ghc-api/annotations/T10357.stdout
@@ -31,7 +31,6 @@
 ((Test10357.hs:7:28,AnnComma), [Test10357.hs:7:29]),
 ((Test10357.hs:7:31-36,AnnVal), [Test10357.hs:7:33]),
 ((Test10357.hs:7:31-40,AnnVal), [Test10357.hs:7:38]),
-((Test10357.hs:7:33,AnnStar), [Test10357.hs:7:33]),
 ((Test10357.hs:7:43-52,AnnBackquote), [Test10357.hs:7:43, Test10357.hs:7:52]),
 ((Test10357.hs:7:43-52,AnnVal), [Test10357.hs:7:44-51]),
 ((Test10357.hs:8:18-59,AnnCloseP), [Test10357.hs:8:59]),
diff --git a/testsuite/tests/ghc-api/annotations/T10358.stdout b/testsuite/tests/ghc-api/annotations/T10358.stdout
index 2bcbf68c09..ae1ec8587f 100644
--- a/testsuite/tests/ghc-api/annotations/T10358.stdout
+++ b/testsuite/tests/ghc-api/annotations/T10358.stdout
@@ -15,23 +15,18 @@
 ((Test10358.hs:5:7-16,AnnEqual), [Test10358.hs:5:12]),
 ((Test10358.hs:5:7-16,AnnSemi), [Test10358.hs:5:17]),
 ((Test10358.hs:5:14-16,AnnVal), [Test10358.hs:5:15]),
-((Test10358.hs:5:15,AnnStar), [Test10358.hs:5:15]),
 ((Test10358.hs:5:19-22,AnnBang), [Test10358.hs:5:19]),
 ((Test10358.hs:5:19-32,AnnEqual), [Test10358.hs:5:24]),
 ((Test10358.hs:5:19-32,AnnSemi), [Test10358.hs:6:7]),
 ((Test10358.hs:5:26-32,AnnVal), [Test10358.hs:5:29]),
-((Test10358.hs:5:29,AnnStar), [Test10358.hs:5:29]),
 ((Test10358.hs:6:7-16,AnnEqual), [Test10358.hs:6:10]),
 ((Test10358.hs:6:7-16,AnnFunId), [Test10358.hs:6:7-8]),
 ((Test10358.hs:6:7-16,AnnSemi), [Test10358.hs:7:7]),
 ((Test10358.hs:6:12-14,AnnVal), [Test10358.hs:6:13]),
 ((Test10358.hs:6:12-16,AnnVal), [Test10358.hs:6:15]),
-((Test10358.hs:6:13,AnnStar), [Test10358.hs:6:13]),
-((Test10358.hs:6:15,AnnStar), [Test10358.hs:6:15]),
 ((Test10358.hs:7:7-17,AnnEqual), [Test10358.hs:7:10]),
 ((Test10358.hs:7:7-17,AnnFunId), [Test10358.hs:7:7-8]),
 ((Test10358.hs:7:12-17,AnnVal), [Test10358.hs:7:14]),
-((Test10358.hs:7:14,AnnStar), [Test10358.hs:7:14]),
 ((<no location info>,AnnEofPos), [Test10358.hs:9:1])
 ]
 
diff --git a/testsuite/tests/ghc-api/annotations/T11018.stderr b/testsuite/tests/ghc-api/annotations/T11018.stderr
index c58942f4c7..86d30ec5ed 100644
--- a/testsuite/tests/ghc-api/annotations/T11018.stderr
+++ b/testsuite/tests/ghc-api/annotations/T11018.stderr
@@ -20,7 +20,7 @@ Test11018.hs:26:7: error:
     Not in scope: type constructor or class ‘ArrowApply’
 
 Test11018.hs:37:27: error:
-    Illegal kind signature: ‘* -> *’
+    Illegal kind signature: ‘★ -> ★’
       Perhaps you intended to use KindSignatures
     In the data type declaration for ‘RecorderU’
 
diff --git a/testsuite/tests/ghc-api/annotations/T11018.stdout b/testsuite/tests/ghc-api/annotations/T11018.stdout
index d05c13f213..ac32549858 100644
--- a/testsuite/tests/ghc-api/annotations/T11018.stdout
+++ b/testsuite/tests/ghc-api/annotations/T11018.stdout
@@ -23,9 +23,8 @@
 ((Test11018.hs:12:21-32,AnnCloseP), [Test11018.hs:12:32]),
 ((Test11018.hs:12:21-32,AnnDcolonU), [Test11018.hs:12:24]),
 ((Test11018.hs:12:21-32,AnnOpenP), [Test11018.hs:12:21]),
-((Test11018.hs:12:26,AnnStar), [Test11018.hs:12:26]),
+((Test11018.hs:12:26,AnnRarrow), [Test11018.hs:12:28-29]),
 ((Test11018.hs:12:26-31,AnnRarrow), [Test11018.hs:12:28-29]),
-((Test11018.hs:12:31,AnnStar), [Test11018.hs:12:31]),
 ((Test11018.hs:(13,16)-(15,7),AnnCloseC), [Test11018.hs:15:7]),
 ((Test11018.hs:(13,16)-(15,7),AnnOpenC), [Test11018.hs:13:16]),
 ((Test11018.hs:14:9-40,AnnDcolon), [Test11018.hs:14:18-19]),
@@ -119,9 +118,8 @@
 ((Test11018.hs:37:22-32,AnnCloseP), [Test11018.hs:37:32]),
 ((Test11018.hs:37:22-32,AnnDcolonU), [Test11018.hs:37:25]),
 ((Test11018.hs:37:22-32,AnnOpenP), [Test11018.hs:37:22]),
-((Test11018.hs:37:27,AnnStarU), [Test11018.hs:37:27]),
+((Test11018.hs:37:27,AnnRarrowU), [Test11018.hs:37:29]),
 ((Test11018.hs:37:27-31,AnnRarrowU), [Test11018.hs:37:29]),
-((Test11018.hs:37:31,AnnStarU), [Test11018.hs:37:31]),
 ((Test11018.hs:(38,17)-(40,7),AnnCloseC), [Test11018.hs:40:7]),
 ((Test11018.hs:(38,17)-(40,7),AnnOpenC), [Test11018.hs:38:17]),
 ((Test11018.hs:39:9-40,AnnDcolonU), [Test11018.hs:39:19]),
diff --git a/testsuite/tests/ghc-api/annotations/exampleTest.stdout b/testsuite/tests/ghc-api/annotations/exampleTest.stdout
index 9ae9f2300a..a884f56a32 100644
--- a/testsuite/tests/ghc-api/annotations/exampleTest.stdout
+++ b/testsuite/tests/ghc-api/annotations/exampleTest.stdout
@@ -65,9 +65,8 @@
 ((AnnotationTuple.hs:18:1-28,AnnDcolon), [AnnotationTuple.hs:18:20-21]),
 ((AnnotationTuple.hs:18:1-28,AnnFamily), [AnnotationTuple.hs:18:6-11]),
 ((AnnotationTuple.hs:18:1-28,AnnSemi), [AnnotationTuple.hs:19:1]),
-((AnnotationTuple.hs:18:23,AnnStar), [AnnotationTuple.hs:18:23]),
+((AnnotationTuple.hs:18:23,AnnRarrow), [AnnotationTuple.hs:18:25-26]),
 ((AnnotationTuple.hs:18:23-28,AnnRarrow), [AnnotationTuple.hs:18:25-26]),
-((AnnotationTuple.hs:18:28,AnnStar), [AnnotationTuple.hs:18:28]),
 ((AnnotationTuple.hs:(20,1)-(24,14),AnnFunId), [AnnotationTuple.hs:20:1-5]),
 ((AnnotationTuple.hs:(20,1)-(24,14),AnnSemi), [AnnotationTuple.hs:25:1]),
 ((AnnotationTuple.hs:(21,7)-(24,14),AnnEqual), [AnnotationTuple.hs:24:7]),
diff --git a/testsuite/tests/ghc-api/annotations/listcomps.stdout b/testsuite/tests/ghc-api/annotations/listcomps.stdout
index 754c170f39..1c0b8e5ce4 100644
--- a/testsuite/tests/ghc-api/annotations/listcomps.stdout
+++ b/testsuite/tests/ghc-api/annotations/listcomps.stdout
@@ -97,8 +97,6 @@
 
 (AK ListComprehensions.hs:18:22-30 AnnVal = [ListComprehensions.hs:18:28])
 
-(AK ListComprehensions.hs:18:28 AnnStar = [ListComprehensions.hs:18:28])
-
 (AK ListComprehensions.hs:19:22-33 AnnLarrow = [ListComprehensions.hs:19:24-25])
 
 (AK ListComprehensions.hs:19:22-33 AnnVbar = [ListComprehensions.hs:20:20])
diff --git a/testsuite/tests/ghc-api/annotations/parseTree.stdout b/testsuite/tests/ghc-api/annotations/parseTree.stdout
index d3e1a5a7dd..46b1c4fbb4 100644
--- a/testsuite/tests/ghc-api/annotations/parseTree.stdout
+++ b/testsuite/tests/ghc-api/annotations/parseTree.stdout
@@ -132,12 +132,10 @@
 
 (AK AnnotationTuple.hs:18:1-28 AnnSemi = [AnnotationTuple.hs:19:1])
 
-(AK AnnotationTuple.hs:18:23 AnnStar = [AnnotationTuple.hs:18:23])
+(AK AnnotationTuple.hs:18:23 AnnRarrow = [AnnotationTuple.hs:18:25-26])
 
 (AK AnnotationTuple.hs:18:23-28 AnnRarrow = [AnnotationTuple.hs:18:25-26])
 
-(AK AnnotationTuple.hs:18:28 AnnStar = [AnnotationTuple.hs:18:28])
-
 (AK AnnotationTuple.hs:(20,1)-(24,14) AnnFunId = [AnnotationTuple.hs:20:1-5])
 
 (AK AnnotationTuple.hs:(20,1)-(24,14) AnnSemi = [AnnotationTuple.hs:25:1])
diff --git a/testsuite/tests/ghc-api/landmines/landmines.stdout b/testsuite/tests/ghc-api/landmines/landmines.stdout
index 551b2cf8d7..ccb6b3107e 100644
--- a/testsuite/tests/ghc-api/landmines/landmines.stdout
+++ b/testsuite/tests/ghc-api/landmines/landmines.stdout
@@ -1,4 +1,4 @@
 (12,12,7)
-(63,63,0)
-(13,13,7)
+(70,63,0)
+(14,13,7)
 (10,10,7)