update to current master againwip/T13904

67 files changed, 574 insertions, 109 deletions

diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.hs b/testsuite/tests/dependent/should_fail/BadTelescope.hs
index acabffec54..11b52f36e2 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module BadTelescope where
 
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.stderr b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
index 2fbc35a9ba..5fa8efd502 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
@@ -1,9 +1,6 @@
 
 BadTelescope.hs:9:1: error:
-    • These kind and type variables: (a :: k)
-                                     k
-                                     (b :: k)
-                                     (c :: SameKind a b)
+    • These kind and type variables: a 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
index 6237df4488..b12adbd8e3 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, ExplicitForAll #-}
+{-# LANGUAGE DataKinds, PolyKinds, ExplicitForAll #-}
 
 module BadTelescope2 where
 
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index 2a9dc76310..55a484910c 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -3,14 +3,11 @@ 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
+    • 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:
+BadTelescope2.hs:13:70: error:
+    • Expected kind ‘k0’, but ‘d’ has kind ‘Proxy a’
+    • In the second argument of ‘SameKind’, namely ‘d’
+      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
index 807479f634..470f5fb9fe 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope3.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope3.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, ExplicitForAll #-}
+{-# LANGUAGE PolyKinds, ExplicitForAll #-}
 
 module BadTelescope3 where
 
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
index 4ea7458bb2..1137f28c4d 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
@@ -1,6 +1,6 @@
 
 BadTelescope3.hs:9:1: error:
-    • These kind and type variables: (a :: k) k (b :: k)
+    • 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 synonym declaration for ‘S’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.hs b/testsuite/tests/dependent/should_fail/BadTelescope4.hs
index 566922a4a0..bdaf674c2f 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope4.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope4.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ExistentialQuantification, TypeInType #-}
+{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds #-}
 module BadTelescope4 where
 
 import Data.Proxy
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
index 2394f896ad..f7c281e983 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
@@ -1,6 +1,6 @@
 
 BadTelescope4.hs:9:1: error:
-    • These kind and type variables: (a :: k)
+    • These kind and type variables: a
                                      (c :: Proxy b)
                                      (d :: Proxy a)
                                      (x :: SameKind b d)
@@ -11,5 +11,5 @@ BadTelescope4.hs:9:1: error:
         (c :: Proxy b)
         (d :: Proxy a)
         (x :: SameKind b d)
-      NB: Implicitly declared kind variables are put first.
+      NB: Implicitly declared variables come before others.
     • 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
index 425a8159c4..26e5d46832 100644
--- a/testsuite/tests/dependent/should_fail/DepFail1.hs
+++ b/testsuite/tests/dependent/should_fail/DepFail1.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 
 module DepFail1 where
 
diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr
index 630f010fa3..a8e64d4e0c 100644
--- a/testsuite/tests/dependent/should_fail/DepFail1.stderr
+++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr
@@ -2,11 +2,25 @@
 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
+    • In the type signature: z :: Proxy Bool
+
+DepFail1.hs:8:5: error:
+    • Couldn't match expected type ‘Proxy Bool’
+                  with actual type ‘Proxy k0 a1’
+    • In the expression: P
+      In an equation for ‘z’: z = P
 
 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
+      In the type signature: a :: Proxy Int Bool
+
+DepFail1.hs:11:5: error:
+    • Couldn't match kind ‘*’ with ‘Int’
+      When matching types
+        a0 :: Int
+        Bool :: *
+      Expected type: Proxy Int Bool
+        Actual type: Proxy Int a0
+    • In the expression: P
+      In an equation for ‘a’: a = P
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.hs b/testsuite/tests/dependent/should_fail/InferDependency.hs
index 47957d47d6..c2bec19d44 100644
--- a/testsuite/tests/dependent/should_fail/InferDependency.hs
+++ b/testsuite/tests/dependent/should_fail/InferDependency.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 
 module InferDependency where
 
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.stderr b/testsuite/tests/dependent/should_fail/InferDependency.stderr
index 7fa900a889..cc852ee58c 100644
--- a/testsuite/tests/dependent/should_fail/InferDependency.stderr
+++ b/testsuite/tests/dependent/should_fail/InferDependency.stderr
@@ -1,8 +1,10 @@
 
-InferDependency.hs:6:1: error:
-    • Invalid declaration for ‘Proxy2’; you must explicitly
-      declare which variables are dependent on which others.
-      Inferred variable kinds:
+InferDependency.hs:6:13: error:
+    • Type constructor argument ‘k’ is used dependently.
+      Any dependent arguments must be obviously so, not inferred
+      by the type-checker.
+      Inferred argument kinds:
         k :: *
         a :: k
+      Suggestion: use ‘k’ in a kind to make the dependency clearer.
     • In the data type declaration for ‘Proxy2’
diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.hs b/testsuite/tests/dependent/should_fail/KindLevelsB.hs
deleted file mode 100644
index 80762978b2..0000000000
--- a/testsuite/tests/dependent/should_fail/KindLevelsB.hs
+++ /dev/null
@@ -1,9 +0,0 @@
-{-# 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_fail/KindLevelsB.stderr b/testsuite/tests/dependent/should_fail/KindLevelsB.stderr
deleted file mode 100644
index 587eb97bfa..0000000000
--- a/testsuite/tests/dependent/should_fail/KindLevelsB.stderr
+++ /dev/null
@@ -1,5 +0,0 @@
-
-KindLevelsB.hs:7:13: error:
-    • Expected kind ‘A’, but ‘a’ has kind ‘*’
-    • In the first argument of ‘B’, namely ‘a’
-      In the kind ‘B a -> *’
diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.hs b/testsuite/tests/dependent/should_fail/PromotedClass.hs
index 6c3f415e5d..53d581015d 100644
--- a/testsuite/tests/dependent/should_fail/PromotedClass.hs
+++ b/testsuite/tests/dependent/should_fail/PromotedClass.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, GADTs #-}
+{-# LANGUAGE DataKinds, GADTs #-}
 
 module PromotedClass where
 
diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.stderr b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
index f0683309bc..4da1a32fca 100644
--- a/testsuite/tests/dependent/should_fail/PromotedClass.stderr
+++ b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
@@ -1,5 +1,6 @@
 
 PromotedClass.hs:10:15: error:
-    • Illegal constraint in a type: Show a0
+    • Data constructor ‘MkX’ cannot be used here
+        (it has an unpromotable context ‘Show a’)
     • 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
index 08a4ad78a8..d71b863f02 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.hs
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.hs
@@ -1,34 +1,36 @@
 {-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, DataKinds,
-             PolyKinds, TypeFamilies, GADTs, TypeInType #-}
+             PolyKinds, TypeFamilies, GADTs #-}
 
 module RAE_T32a where
 
 import Data.Kind
 
-data family Sing (k :: *) :: k -> *
+data family Sing (k :: Type) :: k -> Type
 
-data TyArr' (a :: *) (b :: *) :: *
-type TyArr (a :: *) (b :: *) = TyArr' a b -> *
+data TyArr' (a :: Type) (b :: Type) :: Type
+type TyArr (a :: Type) (b :: Type) = TyArr' a b -> Type
 type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2
-data TyPi' (a :: *) (b :: TyArr a *) :: *
-type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> *
+data TyPi' (a :: Type) (b :: TyArr a Type) :: Type
+type TyPi (a :: Type) (b :: TyArr a Type) = TyPi' a b -> Type
 type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
 $(return [])
 
-data MkStar (p :: *) (x :: TyArr' p *)
-type instance MkStar p @@ x = *
+data MkStar (p :: Type) (x :: TyArr' p Type)
+type instance MkStar p @@ x = Type
 $(return [])
 
-data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where
+data Sigma (p :: Type) (r :: TyPi p (MkStar p)) :: Type 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
+    forall (p :: Type) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a).
+    Sing Type 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).
+    forall (p :: Type) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a)
+           (sp :: Sing Type 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)
 
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
index cb94dd2854..41f5d7cd4c 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
@@ -1,19 +1,18 @@
 
-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:29:1: error:
+    • Expected kind ‘k0 -> *’,
+        but ‘Sing Sigma (Sigma p r)’ has kind ‘*’
+    • 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:29: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’
+RAE_T32a.hs:29: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/RenamingStar.hs b/testsuite/tests/dependent/should_fail/RenamingStar.hs
index 255021c8d9..f9344b0fd9 100644
--- a/testsuite/tests/dependent/should_fail/RenamingStar.hs
+++ b/testsuite/tests/dependent/should_fail/RenamingStar.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE KindSignatures, NoStarIsType #-}
 
 module RenamingStar where
 
diff --git a/testsuite/tests/dependent/should_fail/RenamingStar.stderr b/testsuite/tests/dependent/should_fail/RenamingStar.stderr
index 5efda699fd..4001811f1f 100644
--- a/testsuite/tests/dependent/should_fail/RenamingStar.stderr
+++ b/testsuite/tests/dependent/should_fail/RenamingStar.stderr
@@ -1,11 +1,5 @@
 
 RenamingStar.hs:5:13: error:
-    Not in scope: type constructor or class ‘*’
-    NB: With TypeInType, you must import * from Data.Kind
-
-RenamingStar.hs:5:13: error:
-    Illegal operator ‘*’ in type ‘*’
-      Use TypeOperators to allow operators in types
-
-RenamingStar.hs:5:13: error:
     Operator applied to too few arguments: *
+    With NoStarIsType, ‘*’ is treated as a regular type operator. 
+    Did you mean to use ‘Type’ from Data.Kind instead?
diff --git a/testsuite/tests/dependent/should_fail/SelfDep.hs b/testsuite/tests/dependent/should_fail/SelfDep.hs
index f54b92752b..22ac9ede98 100644
--- a/testsuite/tests/dependent/should_fail/SelfDep.hs
+++ b/testsuite/tests/dependent/should_fail/SelfDep.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE KindSignatures #-}
+
 module SelfDep where
 
 data T :: T -> *
diff --git a/testsuite/tests/dependent/should_fail/SelfDep.stderr b/testsuite/tests/dependent/should_fail/SelfDep.stderr
index f4014f7277..8ac4be8c0c 100644
--- a/testsuite/tests/dependent/should_fail/SelfDep.stderr
+++ b/testsuite/tests/dependent/should_fail/SelfDep.stderr
@@ -1,5 +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 -> *’
+SelfDep.hs:5: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/T11407.hs b/testsuite/tests/dependent/should_fail/T11407.hs
index 533870f94b..e94eaba1e7 100644
--- a/testsuite/tests/dependent/should_fail/T11407.hs
+++ b/testsuite/tests/dependent/should_fail/T11407.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 module T11407 where
 
 import Data.Kind
diff --git a/testsuite/tests/dependent/should_fail/T11471.hs b/testsuite/tests/dependent/should_fail/T11471.hs
index 19025db22b..ae09ae07bb 100644
--- a/testsuite/tests/dependent/should_fail/T11471.hs
+++ b/testsuite/tests/dependent/should_fail/T11471.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies #-}
+{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies, AllowAmbiguousTypes #-}
 
 module T11471 where
 
diff --git a/testsuite/tests/dependent/should_fail/T11471.stderr b/testsuite/tests/dependent/should_fail/T11471.stderr
index 80c5fc606c..640ae6c754 100644
--- a/testsuite/tests/dependent/should_fail/T11471.stderr
+++ b/testsuite/tests/dependent/should_fail/T11471.stderr
@@ -1,19 +1,22 @@
 
 T11471.hs:15:10: error:
     • Couldn't match a lifted type with an unlifted type
-      Expected type: Proxy Int#
+      When matching types
+        a :: *
+        Int# :: TYPE 'IntRep
+      Expected type: Proxy a
         Actual type: Proxy Int#
-      Use -fprint-explicit-kinds to see the kind arguments
     • In the first argument of ‘f’, namely ‘(undefined :: Proxy Int#)’
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
+    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
 
 T11471.hs:15:35: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
-        F Int# :: *
+        F a :: *
         Int# :: TYPE 'IntRep
     • In the second argument of ‘f’, namely ‘3#’
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
-    • Relevant bindings include bad :: F Int# (bound at T11471.hs:15:1)
+    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/T11473.hs b/testsuite/tests/dependent/should_fail/T11473.hs
index 12d95caac6..ebfeeb8a13 100644
--- a/testsuite/tests/dependent/should_fail/T11473.hs
+++ b/testsuite/tests/dependent/should_fail/T11473.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-}
+{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, RankNTypes #-}
 
 module T11473 where
 
diff --git a/testsuite/tests/dependent/should_fail/T12081.hs b/testsuite/tests/dependent/should_fail/T12081.hs
index f68de420cb..0bf03b1950 100644
--- a/testsuite/tests/dependent/should_fail/T12081.hs
+++ b/testsuite/tests/dependent/should_fail/T12081.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module T12081 where
 
diff --git a/testsuite/tests/dependent/should_fail/T12174.hs b/testsuite/tests/dependent/should_fail/T12174.hs
index 29064d6a96..800759d690 100644
--- a/testsuite/tests/dependent/should_fail/T12174.hs
+++ b/testsuite/tests/dependent/should_fail/T12174.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeInType #-}
 module T12174 where
 
 data V a
diff --git a/testsuite/tests/dependent/should_fail/T13135.hs b/testsuite/tests/dependent/should_fail/T13135.hs
index c39b3f5842..8f78ccbfb1 100644
--- a/testsuite/tests/dependent/should_fail/T13135.hs
+++ b/testsuite/tests/dependent/should_fail/T13135.hs
@@ -8,11 +8,11 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 
 
-module T12135 where
+
+module T13135 where
 
 
 import Data.Kind (Type)
@@ -62,7 +62,7 @@ arrLen = smartSym sym where
 
 
 
-{- The original bug was a familure to subsitute
+{- The original bug was a failure to substitute
    properly during type-function improvement.
 
 --------------------------------------
diff --git a/testsuite/tests/dependent/should_fail/T13601.hs b/testsuite/tests/dependent/should_fail/T13601.hs
new file mode 100644
index 0000000000..a8fa34d4a0
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13601.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
+
+import GHC.Exts
+import Prelude (Bool(True,False),Integer,Ordering,undefined)
+import qualified Prelude
+import Data.Kind
+
+--------------------
+-- class hierarchy
+
+type family
+  Rep (rep :: RuntimeRep) :: RuntimeRep where
+  -- Rep IntRep         = IntRep
+  -- Rep DoubleRep      = IntRep
+  -- Rep PtrRepUnlifted = IntRep
+  -- Rep PtrRepLifted   = PtrRepLifted
+
+class Boolean (Logic a) => Eq (a :: TYPE rep) where
+  type Logic (a :: TYPE rep) :: TYPE (Rep rep)
+  (==) :: a -> a -> Logic a
+
+class Eq a => POrd (a :: TYPE rep) where
+  inf :: a -> a -> a
+
+class POrd a => MinBound (a :: TYPE rep) where
+  minBound :: () -> a
+
+class POrd a => Lattice (a :: TYPE rep) where
+  sup :: a -> a -> a
+
+class (Lattice a, MinBound a) => Bounded (a :: TYPE rep) where
+  maxBound :: () -> a
+
+class Bounded a => Complemented (a :: TYPE rep) where
+  not :: a -> a
+
+class Bounded a => Heyting (a :: TYPE rep) where
+  infixr 3 ==>
+  (==>) :: a -> a -> a
+
+class (Complemented a, Heyting a) => Boolean a
+
+(||) :: Boolean a => a -> a -> a
+(||) = sup
+
+(&&) :: Boolean a => a -> a -> a
+(&&) = inf
diff --git a/testsuite/tests/dependent/should_fail/T13601.stderr b/testsuite/tests/dependent/should_fail/T13601.stderr
new file mode 100644
index 0000000000..bc2877c3e6
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13601.stderr
@@ -0,0 +1,5 @@
+
+T13601.hs:18:16: error:
+    • Expected a type, but ‘Logic a’ has kind ‘TYPE (Rep rep)’
+    • In the first argument of ‘Boolean’, namely ‘(Logic a)’
+      In the class declaration for ‘Eq’
diff --git a/testsuite/tests/dependent/should_fail/T13780a.hs b/testsuite/tests/dependent/should_fail/T13780a.hs
new file mode 100644
index 0000000000..b7e1510672
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
+module T13780a where
+
+data family Sing (a :: k)
+
+data Foo a = a ~ Bool => MkFoo
+data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr
new file mode 100644
index 0000000000..3b113bd89e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780a.stderr
@@ -0,0 +1,6 @@
+
+T13780a.hs:9:40: error:
+    • Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’
+    • In the second argument of ‘(~)’, namely ‘MkFoo’
+      In the definition of data constructor ‘SMkFoo’
+      In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/T13780b.hs b/testsuite/tests/dependent/should_fail/T13780b.hs
new file mode 100644
index 0000000000..dc6ac89c08
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780b.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+module T13780b where
+
+data family Sing (a :: k)
+
+data instance Sing (z :: Bool) =
+    z ~ False => SFalse
+  | z ~ True  => STrue
diff --git a/testsuite/tests/dependent/should_fail/T13780c.hs b/testsuite/tests/dependent/should_fail/T13780c.hs
new file mode 100644
index 0000000000..78e09f5ef1
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780c.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
+module T13780c where
+
+import Data.Kind
+import T13780b
+
+type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b)
+                     (pFalse :: p False) (pTrue :: p True) :: p b where
+  ElimBool _ _ SFalse pFalse _ = pFalse
+  ElimBool _ _ STrue  _ pTrue  = pTrue
diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr
new file mode 100644
index 0000000000..9a196f4bd7
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13780c.stderr
@@ -0,0 +1,14 @@
+[1 of 2] Compiling T13780b          ( T13780b.hs, T13780b.o )
+[2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
+
+T13780c.hs:11:16: error:
+    • Data constructor ‘SFalse’ cannot be used here
+        (it comes from a data family instance)
+    • In the third argument of ‘ElimBool’, namely ‘SFalse’
+      In the type family declaration for ‘ElimBool’
+
+T13780c.hs:12:16: error:
+    • Data constructor ‘STrue’ cannot be used here
+        (it comes from a data family instance)
+    • In the third argument of ‘ElimBool’, namely ‘STrue’
+      In the type family declaration for ‘ElimBool’
diff --git a/testsuite/tests/dependent/should_fail/T13895.hs b/testsuite/tests/dependent/should_fail/T13895.hs
new file mode 100644
index 0000000000..5897cd8149
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13895.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module T13895 where
+
+import Data.Data (Data, Typeable)
+import Data.Kind
+
+dataCast1 :: forall (a :: Type).
+             Data a
+          => forall (c :: Type -> Type)
+                    (t :: forall (k :: Type). Typeable k => k -> Type).
+             Typeable t
+          => (forall d. Data d => c (t d))
+          -> Maybe (c a)
+dataCast1 _ = undefined
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
new file mode 100644
index 0000000000..3e8bef6858
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -0,0 +1,44 @@
+
+T13895.hs:8:14: error:
+    • Could not deduce (Typeable (t dict0))
+      from the context: (Data a, Typeable (t dict))
+        bound by the type signature for:
+                   dataCast1 :: forall k (dict :: Typeable k) (dict1 :: Typeable
+                                                                          *) a (c :: *
+                                                                                     -> *) (t :: forall k1.
+                                                                                                 Typeable
+                                                                                                   k1 =>
+                                                                                                 k1
+                                                                                                 -> *).
+                                (Data a, Typeable (t dict)) =>
+                                (forall d. Data d => c (t dict1 d)) -> Maybe (c a)
+        at T13895.hs:(8,14)-(14,24)
+      The type variable ‘dict0’ is ambiguous
+    • In the ambiguity check for ‘dataCast1’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
+T13895.hs:12:23: error:
+    • Illegal constraint in a kind: Typeable k0
+    • In the first argument of ‘Typeable’, namely ‘t’
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
+T13895.hs:13:38: error:
+    • Illegal constraint in a kind: Typeable k0
+    • In the first argument of ‘c’, namely ‘(t d)’
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
diff --git a/testsuite/tests/dependent/should_fail/T14066.hs b/testsuite/tests/dependent/should_fail/T14066.hs
new file mode 100644
index 0000000000..709d507a34
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+
+
+
+module T14066 where
+
+import Data.Kind ( Type )
+import Data.Type.Equality
+import Data.Proxy
+import GHC.Exts
+
+data SameKind :: k -> k -> Type
+
+f (x :: Proxy a) = let g :: forall k (b :: k). SameKind a b
+                       g = undefined
+                   in ()
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
new file mode 100644
index 0000000000..e5179e510b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -0,0 +1,13 @@
+
+T14066.hs:15:59: error:
+    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the type signature: g :: forall k (b :: k). SameKind a b
+      In the expression:
+        let
+          g :: forall k (b :: k). SameKind a b
+          g = undefined
+        in ()
+    • Relevant bindings include
+        x :: Proxy a (bound at T14066.hs:15:4)
+        f :: Proxy a -> () (bound at T14066.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066c.hs b/testsuite/tests/dependent/should_fail/T14066c.hs
new file mode 100644
index 0000000000..4dd6f41973
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066c.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, UndecidableInstances #-}
+
+module T14066c where
+
+type family H a b where
+  H a b = H b a
+
+type X = H True Nothing  -- this should fail to kind-check.
+                         -- if it's accepted, then we've inferred polymorphic recursion for H
diff --git a/testsuite/tests/dependent/should_fail/T14066c.stderr b/testsuite/tests/dependent/should_fail/T14066c.stderr
new file mode 100644
index 0000000000..dc5ba30a4f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066c.stderr
@@ -0,0 +1,6 @@
+
+T14066c.hs:8:17: error:
+    • Expected kind ‘Bool’, but ‘Nothing’ has kind ‘Maybe a0’
+    • In the second argument of ‘H’, namely ‘Nothing’
+      In the type ‘H True Nothing’
+      In the type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/T14066d.hs b/testsuite/tests/dependent/should_fail/T14066d.hs
new file mode 100644
index 0000000000..dd5676826d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066d.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, PolyKinds #-}
+
+module T14066d where
+
+import Data.Proxy
+
+g :: (forall c b (a :: c). (Proxy a, Proxy c, b)) -> ()
+g _ = ()
+
+f :: forall b. b -> (Proxy Maybe, ())
+f x = (fstOf3 y :: Proxy Maybe, g y)
+  where
+    y :: (Proxy a, Proxy c, b)  -- this should NOT generalize over b
+                                -- meaning the call to g is ill-typed
+    y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
new file mode 100644
index 0000000000..8ece51029b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -0,0 +1,21 @@
+
+T14066d.hs:11:35: error:
+    • Couldn't match type ‘b1’ with ‘b’
+      ‘b1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall c b1 (a :: c). (Proxy a, Proxy c, b1)
+        at T14066d.hs:11:35
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall b. b -> (Proxy Maybe, ())
+        at T14066d.hs:10:1-37
+      Expected type: (Proxy a, Proxy c, b1)
+        Actual type: (Proxy a, Proxy c, b)
+    • In the first argument of ‘g’, namely ‘y’
+      In the expression: g y
+      In the expression: (fstOf3 y :: Proxy Maybe, g y)
+    • Relevant bindings include
+        y :: forall k1 k2 (a :: k2) (c :: k1). (Proxy a, Proxy c, b)
+          (bound at T14066d.hs:15:5)
+        x :: b (bound at T14066d.hs:11:3)
+        f :: b -> (Proxy Maybe, ()) (bound at T14066d.hs:11:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.hs b/testsuite/tests/dependent/should_fail/T14066e.hs
new file mode 100644
index 0000000000..9bce332527
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066e.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MonoLocalBinds, PolyKinds, ScopedTypeVariables #-}
+
+module T14066e where
+
+import Data.Proxy
+
+-- this should fail because the dependency between b and c can't be
+-- determined in the type signature
+h :: forall a. a -> ()
+h x = ()
+  where
+    j :: forall c b. Proxy a -> Proxy b -> Proxy c -> Proxy b
+    j _ (p1 :: Proxy b') (p2 :: Proxy c') = (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
new file mode 100644
index 0000000000..193c74d193
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -0,0 +1,20 @@
+
+T14066e.hs:13:59: error:
+    • Couldn't match kind ‘k1’ with ‘*’
+      ‘k1’ is a rigid type variable bound by
+        the type signature for:
+          j :: forall k k1 (c :: k1) (b :: k).
+               Proxy a -> Proxy b -> Proxy c -> Proxy b
+        at T14066e.hs:12:5-61
+      When matching kinds
+        k :: *
+        c :: k1
+      Expected kind ‘c’, but ‘b'’ has kind ‘k’
+    • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
+      In an expression type signature: Proxy (b' :: c')
+      In the expression: (p1 :: Proxy (b' :: c'))
+    • Relevant bindings include
+        p2 :: Proxy c (bound at T14066e.hs:13:27)
+        p1 :: Proxy b (bound at T14066e.hs:13:10)
+        j :: Proxy a -> Proxy b -> Proxy c -> Proxy b
+          (bound at T14066e.hs:13:5)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.hs b/testsuite/tests/dependent/should_fail/T14066f.hs
new file mode 100644
index 0000000000..b2035f2c3d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066f.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE PolyKinds #-}
+
+module T14066f where
+
+import Data.Proxy
+
+-- a can't come before k.
+type P a k = Proxy (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.stderr b/testsuite/tests/dependent/should_fail/T14066f.stderr
new file mode 100644
index 0000000000..44c4ed293c
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066f.stderr
@@ -0,0 +1,6 @@
+
+T14066f.hs:8:1: error:
+    • These kind and type variables: a k
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k)
+    • In the type synonym declaration for ‘P’
diff --git a/testsuite/tests/dependent/should_fail/T14066g.hs b/testsuite/tests/dependent/should_fail/T14066g.hs
new file mode 100644
index 0000000000..b07a2c36a9
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066g.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds, PolyKinds #-}
+
+module T14066g where
+
+import Data.Kind
+
+data SameKind :: k -> k -> Type
+
+data Q a (b :: a) (d :: SameKind c b)
diff --git a/testsuite/tests/dependent/should_fail/T14066g.stderr b/testsuite/tests/dependent/should_fail/T14066g.stderr
new file mode 100644
index 0000000000..22ca786343
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066g.stderr
@@ -0,0 +1,7 @@
+
+T14066g.hs:9:1: error:
+    • These kind and type variables: a (b :: a) (d :: SameKind c b)
+      are out of dependency order. Perhaps try this ordering:
+        a (c :: a) (b :: a) (d :: SameKind c b)
+      NB: Implicitly declared variables come before others.
+    • In the data type declaration for ‘Q’
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail1.hs b/testsuite/tests/dependent/should_fail/T14845_fail1.hs
new file mode 100644
index 0000000000..46c1351027
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail1.hs
@@ -0,0 +1,10 @@
+{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
+module T14845_fail1 where
+
+import Data.Kind
+
+data Struct :: (k -> Constraint) -> (k -> Type) where
+  S :: cls a => Struct cls a
+
+data Foo a where
+  F :: Foo (S::Struct Eq a)
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail1.stderr b/testsuite/tests/dependent/should_fail/T14845_fail1.stderr
new file mode 100644
index 0000000000..c1f1c8605d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail1.stderr
@@ -0,0 +1,7 @@
+
+T14845_fail1.hs:10:13: error:
+    • Data constructor ‘S’ cannot be used here
+        (it has an unpromotable context ‘cls a’)
+    • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
+      In the type ‘Foo (S :: Struct Eq a)’
+      In the definition of data constructor ‘F’
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail2.hs b/testsuite/tests/dependent/should_fail/T14845_fail2.hs
new file mode 100644
index 0000000000..4c5dac730f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T14845_fail2 where
+
+import Data.Coerce
+import Data.Kind
+
+data A :: Type -> Type where
+  MkA :: Coercible a Int => A a
+
+data SA :: forall a. A a -> Type where
+  SMkA :: SA MkA
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail2.stderr b/testsuite/tests/dependent/should_fail/T14845_fail2.stderr
new file mode 100644
index 0000000000..9fe733f374
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail2.stderr
@@ -0,0 +1,7 @@
+
+T14845_fail2.hs:14:14: error:
+    • Data constructor ‘MkA’ cannot be used here
+        (it has an unpromotable context ‘Coercible a Int’)
+    • In the first argument of ‘SA’, namely ‘MkA’
+      In the type ‘SA MkA’
+      In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/T15215.hs b/testsuite/tests/dependent/should_fail/T15215.hs
new file mode 100644
index 0000000000..96fe04385b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15215.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T15215 where
+
+import Data.Kind
+
+data A :: Type -> Type where
+  MkA :: Show (Maybe a) => A a
+
+data SA :: forall a. A a -> Type where
+  SMkA :: SA MkA
diff --git a/testsuite/tests/dependent/should_fail/T15215.stderr b/testsuite/tests/dependent/should_fail/T15215.stderr
new file mode 100644
index 0000000000..53aff765a3
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15215.stderr
@@ -0,0 +1,12 @@
+
+T15215.hs:9:3: error:
+    • Non type-variable argument in the constraint: Show (Maybe a)
+      (Use FlexibleContexts to permit this)
+    • In the definition of data constructor ‘MkA’
+      In the data type declaration for ‘A’
+
+T15215.hs:12:14: error:
+    • Illegal constraint in a kind: Show (Maybe a0)
+    • In the first argument of ‘SA’, namely ‘MkA’
+      In the type ‘SA MkA’
+      In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/T15245.hs b/testsuite/tests/dependent/should_fail/T15245.hs
new file mode 100644
index 0000000000..86d9c221e0
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15245.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeApplications #-}
+
+module T15245 where
+
+import Type.Reflection
+
+data family K
+data instance K = MkK
+
+main = print (typeRep @'MkK)
diff --git a/testsuite/tests/dependent/should_fail/T15245.stderr b/testsuite/tests/dependent/should_fail/T15245.stderr
new file mode 100644
index 0000000000..b41076636f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15245.stderr
@@ -0,0 +1,7 @@
+
+T15245.hs:10:24: error:
+    • Data constructor ‘MkK’ cannot be used here
+        (it comes from a data family instance)
+    • In the type ‘ 'MkK’
+      In the first argument of ‘print’, namely ‘(typeRep @ 'MkK)’
+      In the expression: print (typeRep @ 'MkK)
diff --git a/testsuite/tests/dependent/should_fail/T15308.hs b/testsuite/tests/dependent/should_fail/T15308.hs
new file mode 100644
index 0000000000..b49fe1f75b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15308.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T15308 where
+
+import Data.Kind
+
+data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where
+  MkFoo :: Foo a f
+
+f :: Foo a f -> String
+f = show
diff --git a/testsuite/tests/dependent/should_fail/T15308.stderr b/testsuite/tests/dependent/should_fail/T15308.stderr
new file mode 100644
index 0000000000..a4bdbd5ab6
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15308.stderr
@@ -0,0 +1,5 @@
+
+T15308.hs:12:5: error:
+    • No instance for (Show (Foo a f)) arising from a use of ‘show’
+    • In the expression: show
+      In an equation for ‘f’: f = show
diff --git a/testsuite/tests/dependent/should_fail/T15343.hs b/testsuite/tests/dependent/should_fail/T15343.hs
new file mode 100644
index 0000000000..9bb59c807a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15343.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeInType #-}
+module T15343 where
+
+import Data.Kind
+
+elimSing :: forall (p :: forall z. z). p
+elimSing = undefined
+
+data WhySym :: Type -> Type
+
+hsym = elimSing @WhySym
diff --git a/testsuite/tests/dependent/should_fail/T15343.stderr b/testsuite/tests/dependent/should_fail/T15343.stderr
new file mode 100644
index 0000000000..79d81e5772
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15343.stderr
@@ -0,0 +1,7 @@
+
+T15343.hs:14:18: error:
+    • Expecting one more argument to ‘WhySym’
+      Expected kind ‘forall z. z’, but ‘WhySym’ has kind ‘* -> *’
+    • In the type ‘WhySym’
+      In the expression: elimSing @WhySym
+      In an equation for ‘hsym’: hsym = elimSing @WhySym
diff --git a/testsuite/tests/dependent/should_fail/T15380.hs b/testsuite/tests/dependent/should_fail/T15380.hs
new file mode 100644
index 0000000000..32ea8ec724
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15380.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T15380 where
+
+import Data.Kind
+
+class Generic a where
+  type Rep a :: Type
+
+class PGeneric a where
+  type To a (x :: Rep a) :: a
+
+type family MDefault (x :: a) :: a where
+  MDefault x = To (M x)
+
+class C a where
+  type M (x :: a) :: a
+  type M (x :: a) = MDefault x
diff --git a/testsuite/tests/dependent/should_fail/T15380.stderr b/testsuite/tests/dependent/should_fail/T15380.stderr
new file mode 100644
index 0000000000..9b30078c64
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15380.stderr
@@ -0,0 +1,6 @@
+
+T15380.hs:16:16: error:
+    • Expecting one more argument to ‘To (M x)’
+      Expected a type, but ‘To (M x)’ has kind ‘Rep (M x) -> M x’
+    • In the type ‘To (M x)’
+      In the type family declaration for ‘MDefault’
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
index bbec037487..1f958de426 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-}
+{-# LANGUAGE RankNTypes, PolyKinds #-}
+-- NB: -fprint-explicit-runtime-reps enabled in all.T
 
 module TypeSkolEscape where
 
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
index 88539858cf..e2ef266914 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
@@ -1,7 +1,5 @@
 
-TypeSkolEscape.hs:8:1: error:
-    • Quantified type's kind mentions quantified type variable
-      (skolem escape)
-           type: forall (a1 :: TYPE v1). a1
-        of kind: TYPE v
-    • In the type synonym declaration for ‘Bad’
+TypeSkolEscape.hs:9:52: error:
+    • Expected kind ‘k0’, but ‘a’ has kind ‘TYPE v’
+    • In the type ‘forall (v :: RuntimeRep) (a :: TYPE v). a’
+      In the type declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index c648f9ed1d..0f7129020e 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,6 +1,6 @@
 test('DepFail1', normal, compile_fail, [''])
 test('RAE_T32a', normal, compile_fail, [''])
-test('TypeSkolEscape', normal, compile_fail, [''])
+test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
 test('BadTelescope3', normal, compile_fail, [''])
@@ -10,10 +10,27 @@ test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334b', normal, compile_fail, [''])
-test('InferDependency', normal, compile_fail, [''])
-test('KindLevelsB', normal, compile_fail, [''])
 test('T11473', normal, compile_fail, [''])
 test('T11471', normal, compile_fail, [''])
 test('T12174', normal, compile_fail, [''])
 test('T12081', normal, compile_fail, [''])
 test('T13135', normal, compile_fail, [''])
+test('T13601', normal, compile_fail, [''])
+test('T13780a', normal, compile_fail, [''])
+test('T13780c', [extra_files(['T13780b.hs'])],
+                multimod_compile_fail, ['T13780c', ''])
+test('T13895', normal, compile_fail, [''])
+test('T14066', normal, compile_fail, [''])
+test('T14066c', normal, compile_fail, [''])
+test('T14066d', normal, compile_fail, [''])
+test('T14066e', normal, compile_fail, [''])
+test('T14066f', normal, compile_fail, [''])
+test('T14066g', normal, compile_fail, [''])
+test('T14845_fail1', normal, compile_fail, [''])
+test('T14845_fail2', normal, compile_fail, [''])
+test('InferDependency', normal, compile_fail, [''])
+test('T15245', normal, compile_fail, [''])
+test('T15215', normal, compile_fail, [''])
+test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
+test('T15343', normal, compile_fail, [''])
+test('T15380', normal, compile_fail, [''])