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.

33 files changed, 480 insertions, 0 deletions

diff --git a/testsuite/tests/dependent/Makefile b/testsuite/tests/dependent/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/dependent/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/dependent/should_compile/Dep1.hs b/testsuite/tests/dependent/should_compile/Dep1.hs
new file mode 100644
index 0000000000..6f8fe0720d
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/Dep1.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeInType #-}
+
+module Dep1 where
+
+import Data.Kind
+
+data Proxy k (a :: k) = P
+
+x :: Proxy * Int
+x = P
+
+y :: Proxy Bool True
+y = P
diff --git a/testsuite/tests/dependent/should_compile/Dep2.hs b/testsuite/tests/dependent/should_compile/Dep2.hs
new file mode 100644
index 0000000000..34be3cffc6
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/Dep2.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds, GADTs #-}
+
+module Dep2 where
+
+data G (a :: k) where
+  G1 :: G Int
+  G2 :: G Maybe
diff --git a/testsuite/tests/dependent/should_compile/Dep3.hs b/testsuite/tests/dependent/should_compile/Dep3.hs
new file mode 100644
index 0000000000..cba5043a08
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/Dep3.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE TypeFamilies, TypeInType, GADTs #-}
+
+module Dep3 where
+
+import Data.Kind
+import GHC.Exts ( Constraint )
+
+type Star1 = *
+
+data Id1 (a :: Star1) where
+  Id1 :: a -> Id1 a
+
+data Id1' :: Star1 -> * where
+  Id1' :: a -> Id1' a
+
+type family Star2 x where
+  Star2 x = *
+
+data Id2a (a :: Star2 Constraint) = Id2a a
+
+
+data Id2 (a :: Star2 Constraint) where
+  Id2 :: a -> Id2 a
+
+data Id2' :: Star2 Constraint -> * where
+  Id2' :: a -> Id2' a
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.hs b/testsuite/tests/dependent/should_compile/KindEqualities.hs
new file mode 100644
index 0000000000..1f2e82c302
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE PolyKinds, GADTs, ExplicitForAll #-}
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+
+module KindEqualities where
+
+data TyRep1 :: * -> * where
+  TyInt1 :: TyRep1 Int
+  TyBool1 :: TyRep1 Bool
+
+zero1 :: forall a. TyRep1 a -> a
+zero1 TyInt1 = 0
+zero1 TyBool1 = False
+
+data Proxy (a :: k) = P
+
+data TyRep :: k -> * where
+  TyInt :: TyRep Int
+  TyBool :: TyRep Bool
+  TyMaybe :: TyRep Maybe
+  TyApp :: TyRep a -> TyRep b -> TyRep (a b)
+
+zero :: forall (a :: *). TyRep a -> a
+zero TyInt = 0
+zero TyBool = False
+zero (TyApp TyMaybe _) = Nothing
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities2.hs b/testsuite/tests/dependent/should_compile/KindEqualities2.hs
new file mode 100644
index 0000000000..5a6f60d40b
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/KindEqualities2.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll,
+             TemplateHaskell, UndecidableInstances, ScopedTypeVariables,
+             TypeInType #-}
+
+module KindEqualities2 where
+
+import Data.Kind
+import GHC.Exts ( Any )
+
+data Kind = Star | Arr Kind Kind
+
+data Ty :: Kind -> * where
+  TInt :: Ty Star
+  TBool :: Ty Star
+  TMaybe :: Ty (Arr Star Star)
+  TApp :: Ty (Arr k1 k2) -> Ty k1 -> Ty k2
+
+
+data TyRep (k :: Kind) (t :: Ty k) where
+  TyInt :: TyRep Star TInt
+  TyBool :: TyRep Star TBool
+  TyMaybe :: TyRep (Arr Star Star) TMaybe
+  TyApp :: TyRep (Arr k1 k2) a -> TyRep k1 b -> TyRep k2 (TApp a b)
+
+type family IK (k :: Kind)
+type instance IK Star = *
+type instance IK (Arr k1 k2) = IK k1 -> IK k2
+
+$(return [])  -- necessary because the following instances depend on the
+              -- previous ones.
+
+type family I (t :: Ty k) :: IK k
+type instance I TInt = Int
+type instance I TBool = Bool
+type instance I TMaybe = Maybe
+type instance I (TApp a b) = (I a) (I b)
+
+zero :: forall (a :: Ty 'Star). TyRep Star a -> I a
+zero TyInt = 0
+zero TyBool = False
+zero (TyApp TyMaybe TyInt) = Nothing
+
+main = print $ zero (TyApp TyMaybe TyInt)
diff --git a/testsuite/tests/dependent/should_compile/KindLevels.hs b/testsuite/tests/dependent/should_compile/KindLevels.hs
new file mode 100644
index 0000000000..80762978b2
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/KindLevels.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds, PolyKinds #-}
+
+module KindLevels where
+
+data A
+data B :: A -> *
+data C :: B a -> *
+data D :: C b -> *
+data E :: D c -> *
diff --git a/testsuite/tests/dependent/should_compile/Makefile b/testsuite/tests/dependent/should_compile/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/dependent/should_compile/RAE_T32b.hs b/testsuite/tests/dependent/should_compile/RAE_T32b.hs
new file mode 100644
index 0000000000..7e067099c9
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/RAE_T32b.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, DataKinds, PolyKinds,
+             RankNTypes, TypeOperators, TypeInType #-}
+
+module RAE_T32b where
+
+import Data.Kind
+
+data family Sing (k :: *) :: k -> *
+
+data TyArr (a :: *) (b :: *) :: *
+type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2
+$(return [])
+
+data Sigma (p :: *) (r :: TyArr p * -> *) :: * where
+  Sigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a).
+           Sing * p -> Sing (TyArr p * -> *) r -> Sing p a -> Sing (r @@ a) b -> Sigma p r
+$(return [])
+
+data instance Sing (Sigma p r) (x :: Sigma p r) :: * where
+  SSigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a)
+            (sp :: Sing * p) (sr :: Sing (TyArr 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)
diff --git a/testsuite/tests/dependent/should_compile/Rae31.hs b/testsuite/tests/dependent/should_compile/Rae31.hs
new file mode 100644
index 0000000000..cedc019cf3
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/Rae31.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TemplateHaskell, TypeOperators, PolyKinds, DataKinds,
+             TypeFamilies, TypeInType #-}
+
+module A where
+
+import Data.Kind
+
+data family Sing (k :: *) :: k -> *
+type Sing' (x :: k) = Sing k x
+data TyFun' (a :: *) (b :: *) :: *
+type TyFun (a :: *) (b :: *) = TyFun' a b -> *
+type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2
+data TyPi' (a :: *) (b :: TyFun a *) :: *
+type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> *
+type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
+$(return [])
+
+data A (a :: *) (b :: a) (c :: TyFun' a *) -- A :: forall a -> a -> a ~> *
+type instance (@@) (A a b) c = *
+$(return [])
+data B (a :: *) (b :: TyFun' a *) -- B :: forall a -> a ~> *
+type instance (@@) (B a) b = TyPi a (A a b)
+$(return [])
+data C (a :: *) (b :: TyPi a (B a)) (c :: a) (d :: a) (e :: TyFun' (b @@@ c @@@ d) *)
diff --git a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
new file mode 100644
index 0000000000..e99c7b5dd5
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies,
+             TypeInType #-}
+{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
+
+module RaeBlogPost where
+
+import Data.Kind
+
+-- a Proxy type with an explicit kind
+data Proxy k (a :: k) = P
+prox :: Proxy * Bool
+prox = P
+
+prox2 :: Proxy Bool 'True
+prox2 = P
+
+-- implicit kinds still work
+data A
+data B :: A -> *
+data C :: B a -> *
+data D :: C b -> *
+data E :: D c -> *
+-- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> *
+
+-- a kind-indexed GADT
+data TypeRep (a :: k) where
+  TInt   :: TypeRep Int
+  TMaybe :: TypeRep Maybe
+  TApp   :: TypeRep a -> TypeRep b -> TypeRep (a b)
+
+zero :: TypeRep a -> a
+zero TInt            = 0
+zero (TApp TMaybe _) = Nothing
+
+data Nat = Zero | Succ Nat
+type family a + b where
+  'Zero     + b = b
+  ('Succ a) + b = 'Succ (a + b)
+
+data Vec :: * -> Nat -> * where
+  Nil  :: Vec a 'Zero
+  (:>) :: a -> Vec a n -> Vec a ('Succ n)
+infixr 5 :>
+
+-- promoted GADT, and using + as a "kind family":
+type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where
+  'Nil      ++ y = y
+  (h ':> t) ++ y = h ':> (t ++ y)
+
+-- datatype that mentions *
+data U = Star (*)
+       | Bool Bool
+
+-- kind synonym
+type Monadish = * -> *
+class MonadTrans (t :: Monadish -> Monadish) where
+  lift :: Monad m => m a -> t m a
+data Free :: Monadish where
+  Return :: a -> Free a
+  Bind   :: Free a -> (a -> Free b) -> Free b
+
+-- yes, * really does have type *.
+type Star = (* :: (* :: (* :: *)))
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
new file mode 100644
index 0000000000..0f231db699
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -0,0 +1,10 @@
+test('Dep1', only_ways('normal'), compile, [''])
+test('Dep2', only_ways('normal'), compile, [''])
+test('Dep3', only_ways('normal'), compile, [''])
+test('KindEqualities', only_ways('normal'), compile, [''])
+test('KindEqualities2', only_ways('normal'), compile, [''])
+test('Rae31', only_ways('normal'), compile, [''])
+test('RAE_T32b', only_ways('normal'), compile, [''])
+test('KindLevels', normal, compile, [''])
+test('RaeBlogPost', normal, compile, [''])
+test('mkGADTVars', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_compile/mkGADTVars.hs b/testsuite/tests/dependent/should_compile/mkGADTVars.hs
new file mode 100644
index 0000000000..1e74c6980a
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/mkGADTVars.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs, TypeInType #-}
+
+module GADTVars where
+
+import Data.Kind
+import Data.Proxy
+
+data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where
+  MkT :: T x1 * (Proxy (y :: x1), z) z
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, [''])