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.

20 files changed, 222 insertions, 0 deletions

diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.hs b/testsuite/tests/dependent/should_fail/BadTelescope.hs
new file mode 100644
index 0000000000..acabffec54
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeInType #-}
+
+module BadTelescope where
+
+import Data.Kind
+
+data SameKind :: k -> k -> *
+
+data X a k (b :: k) (c :: SameKind a b)
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.stderr b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
new file mode 100644
index 0000000000..2fbc35a9ba
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
@@ -0,0 +1,9 @@
+
+BadTelescope.hs:9:1: error:
+    • These kind and type variables: (a :: k)
+                                     k
+                                     (b :: k)
+                                     (c :: SameKind a b)
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k) (b :: k) (c :: SameKind a b)
+    • In the data type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
new file mode 100644
index 0000000000..6237df4488
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeInType, ExplicitForAll #-}
+
+module BadTelescope2 where
+
+import Data.Kind
+import Data.Proxy
+
+data SameKind :: k -> k -> *
+
+foo :: forall a k (b :: k). SameKind a b
+foo = undefined
+
+bar :: forall a (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
+bar = undefined
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
new file mode 100644
index 0000000000..2a9dc76310
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -0,0 +1,16 @@
+
+BadTelescope2.hs:10:8: error:
+    • These kind and type variables: a k (b :: k)
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k) (b :: k)
+    • In the type signature:
+        foo :: forall a k (b :: k). SameKind a b
+
+BadTelescope2.hs:13:8: error:
+    • The kind of variable ‘b’, namely ‘Proxy a’,
+      depends on variable ‘a’ from an inner scope
+      Perhaps bind ‘b’ sometime after binding ‘a’
+      NB: Implicitly-bound variables always come before other ones.
+    • In the type signature:
+        bar :: forall a (c :: Proxy b) (d :: Proxy a).
+               Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.hs b/testsuite/tests/dependent/should_fail/BadTelescope3.hs
new file mode 100644
index 0000000000..807479f634
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope3.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeInType, ExplicitForAll #-}
+
+module BadTelescope3 where
+
+import Data.Kind
+
+data SameKind :: k -> k -> *
+
+type S a k (b :: k) = SameKind a b
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
new file mode 100644
index 0000000000..4ea7458bb2
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
@@ -0,0 +1,6 @@
+
+BadTelescope3.hs:9:1: error:
+    • These kind and type variables: (a :: k) k (b :: k)
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k) (b :: k)
+    • In the type synonym declaration for ‘S’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.hs b/testsuite/tests/dependent/should_fail/BadTelescope4.hs
new file mode 100644
index 0000000000..566922a4a0
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope4.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE ExistentialQuantification, TypeInType #-}
+module BadTelescope4 where
+
+import Data.Proxy
+import Data.Kind
+
+data SameKind :: k -> k -> *
+
+data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
+
+data Borked a (b :: k) = forall (c :: k). B (Proxy c)
+  -- this last one is OK. But there was a bug involving renaming
+  -- that failed here, so the test case remains.
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
new file mode 100644
index 0000000000..158aec650d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
@@ -0,0 +1,15 @@
+
+BadTelescope4.hs:9:1: error:
+    • These kind and type variables: (a :: k1)
+                                     (c :: Proxy b)
+                                     (d :: Proxy a)
+                                     (x :: SameKind b d)
+      are out of dependency order. Perhaps try this ordering:
+        k1
+        (a :: k1)
+        (b :: Proxy a)
+        (c :: Proxy b)
+        (d :: Proxy a)
+        (x :: SameKind b d)
+      NB: Implicitly declared kind variables are put first.
+    • In the data type declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/DepFail1.hs b/testsuite/tests/dependent/should_fail/DepFail1.hs
new file mode 100644
index 0000000000..425a8159c4
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/DepFail1.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeInType #-}
+
+module DepFail1 where
+
+data Proxy k (a :: k) = P
+
+z :: Proxy Bool
+z = P
+
+a :: Proxy Int Bool
+a = P
diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr
new file mode 100644
index 0000000000..630f010fa3
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr
@@ -0,0 +1,12 @@
+
+DepFail1.hs:7:6: error:
+    • Expecting one more argument to ‘Proxy Bool’
+      Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’
+    • In the type signature:
+        z :: Proxy Bool
+
+DepFail1.hs:10:16: error:
+    • Expected kind ‘Int’, but ‘Bool’ has kind ‘*’
+    • In the second argument of ‘Proxy’, namely ‘Bool’
+      In the type signature:
+        a :: Proxy Int Bool
diff --git a/testsuite/tests/dependent/should_fail/Makefile b/testsuite/tests/dependent/should_fail/Makefile
new file mode 100644
index 0000000000..13938e423d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/Makefile
@@ -0,0 +1,5 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
+
+
diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.hs b/testsuite/tests/dependent/should_fail/PromotedClass.hs
new file mode 100644
index 0000000000..6c3f415e5d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/PromotedClass.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeInType, GADTs #-}
+
+module PromotedClass where
+
+import Data.Proxy
+
+data X a where
+  MkX :: Show a => a -> X a
+
+foo :: Proxy ('MkX 'True)
+foo = Proxy
diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.stderr b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
new file mode 100644
index 0000000000..544124ed07
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
@@ -0,0 +1,6 @@
+
+PromotedClass.hs:10:15: error:
+    • Illegal constraint in a type: Show a0
+    • In the first argument of ‘Proxy’, namely ‘MkX True’
+      In the type signature:
+        foo :: Proxy (MkX True)
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.hs b/testsuite/tests/dependent/should_fail/RAE_T32a.hs
new file mode 100644
index 0000000000..08a4ad78a8
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, DataKinds,
+             PolyKinds, TypeFamilies, GADTs, TypeInType #-}
+
+module RAE_T32a where
+
+import Data.Kind
+
+data family Sing (k :: *) :: k -> *
+
+data TyArr' (a :: *) (b :: *) :: *
+type TyArr (a :: *) (b :: *) = TyArr' a b -> *
+type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2
+data TyPi' (a :: *) (b :: TyArr a *) :: *
+type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> *
+type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
+$(return [])
+
+data MkStar (p :: *) (x :: TyArr' p *)
+type instance MkStar p @@ x = *
+$(return [])
+
+data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where
+  Sigma ::
+    forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a).
+    Sing * p -> Sing (TyPi p (MkStar p)) r -> Sing p a -> Sing (r @@@ a) b -> Sigma p r
+$(return [])
+
+data instance Sing Sigma (Sigma p r) x where
+  SSigma ::
+    forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a)
+    (sp :: Sing * p) (sr :: Sing (TyPi p (MkStar p)) r) (sa :: Sing p a) (sb :: Sing (r @@@ a) b).
+    Sing (Sing (r @@@ a) b) sb ->
+    Sing (Sigma p r) ('Sigma sp sr sa sb)
+
+-- I (RAE) believe this last definition is ill-typed.
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
new file mode 100644
index 0000000000..1a54c7d53b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
@@ -0,0 +1,19 @@
+
+RAE_T32a.hs:28:1: error:
+    Too many parameters to Sing:
+      x is unexpected;
+      expected only two parameters
+    In the data instance declaration for ‘Sing’
+
+RAE_T32a.hs:28:20: error:
+    Expecting two more arguments to ‘Sigma’
+    Expected a type, but
+    ‘Sigma’ has kind
+    ‘forall p -> TyPi p (MkStar p) -> *’
+    In the first argument of ‘Sing’, namely ‘Sigma’
+    In the data instance declaration for ‘Sing’
+
+RAE_T32a.hs:28:27: error:
+    Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
+    In the second argument of ‘Sing’, namely ‘Sigma p r’
+    In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/SelfDep.hs b/testsuite/tests/dependent/should_fail/SelfDep.hs
new file mode 100644
index 0000000000..f54b92752b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/SelfDep.hs
@@ -0,0 +1,3 @@
+module SelfDep where
+
+data T :: T -> *
diff --git a/testsuite/tests/dependent/should_fail/SelfDep.stderr b/testsuite/tests/dependent/should_fail/SelfDep.stderr
new file mode 100644
index 0000000000..f4014f7277
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/SelfDep.stderr
@@ -0,0 +1,5 @@
+
+SelfDep.hs:3:11: error:
+    Type constructor ‘T’ cannot be used here
+      (it is defined and used in the same recursive group)
+    In the kind ‘T -> *’
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
new file mode 100644
index 0000000000..09845ed87e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-}
+
+module TypeSkolEscape where
+
+import GHC.Types
+import GHC.Exts
+
+type Bad = forall (v :: Levity) (a :: TYPE v). a
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
new file mode 100644
index 0000000000..1574c017ce
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
@@ -0,0 +1,7 @@
+
+TypeSkolEscape.hs:8:1: error:
+    Quantified type's kind mentions quantified type variable
+    (skolem escape)
+         type: forall (v1 :: Levity) (a1 :: TYPE v1). a1
+      of kind: TYPE v
+    In the type synonym declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
new file mode 100644
index 0000000000..8d4b288e96
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -0,0 +1,9 @@
+test('DepFail1', normal, compile_fail, [''])
+test('RAE_T32a', normal, compile_fail, [''])
+test('TypeSkolEscape', normal, compile_fail, [''])
+test('BadTelescope', normal, compile_fail, [''])
+test('BadTelescope2', normal, compile_fail, [''])
+test('BadTelescope3', normal, compile_fail, [''])
+test('PromotedClass', normal, compile_fail, [''])
+test('SelfDep', normal, compile_fail, [''])
+test('BadTelescope4', normal, compile_fail, [''])