update to current master againwip/T13904

117 files changed, 1499 insertions, 188 deletions

diff --git a/testsuite/tests/dependent/ghci/T11549.script b/testsuite/tests/dependent/ghci/T11549.script
index bb35589671..3e0811f921 100644
--- a/testsuite/tests/dependent/ghci/T11549.script
+++ b/testsuite/tests/dependent/ghci/T11549.script
@@ -1,14 +1,18 @@
-:set -XTypeInType
+:set -XPolyKinds
 import GHC.Exts
 
 putStrLn "-fno-print-explicit-runtime-reps"
 :set -fno-print-explicit-runtime-reps
+:type ($)
 :info ($)
 :kind TYPE
+:type error
 :info error
 
 putStrLn "\n-fprint-explicit-runtime-reps"
 :set -fprint-explicit-runtime-reps
+:type ($)
 :info ($)
 :kind TYPE
+:type error
 :info error
diff --git a/testsuite/tests/dependent/ghci/T11549.stdout b/testsuite/tests/dependent/ghci/T11549.stdout
index c8449ba09f..5e23c0da99 100644
--- a/testsuite/tests/dependent/ghci/T11549.stdout
+++ b/testsuite/tests/dependent/ghci/T11549.stdout
@@ -1,12 +1,21 @@
 -fno-print-explicit-runtime-reps
 ($) :: (a -> b) -> a -> b
+($) :: (a -> b) -> a -> b 	-- Defined in ‘GHC.Base’
+infixr 0 $
 TYPE :: RuntimeRep -> *
+error :: [Char] -> a
 error :: GHC.Stack.Types.HasCallStack => [Char] -> a
+  	-- Defined in ‘GHC.Err’
 
 -fprint-explicit-runtime-reps
+($) :: (a -> b) -> a -> b
 ($) :: forall (r :: RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b
+  	-- Defined in ‘GHC.Base’
+infixr 0 $
 TYPE :: RuntimeRep -> *
-error
-  :: forall (r :: RuntimeRep) (a :: TYPE r).
-     GHC.Stack.Types.HasCallStack =>
-     [Char] -> a
+error :: [Char] -> a
+error ::
+  forall (r :: RuntimeRep) (a :: TYPE r).
+  GHC.Stack.Types.HasCallStack =>
+  [Char] -> a
+  	-- Defined in ‘GHC.Err’
diff --git a/testsuite/tests/dependent/ghci/T11786.script b/testsuite/tests/dependent/ghci/T11786.script
new file mode 100644
index 0000000000..61e3141843
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T11786.script
@@ -0,0 +1,11 @@
+:set -fno-print-explicit-runtime-reps
+:t ($)
+:t (($))
+:t +v ($)
+:i ($)
+
+:set -fprint-explicit-runtime-reps
+:t ($)
+:t (($))
+:t +v ($)
+:i ($)
diff --git a/testsuite/tests/dependent/ghci/T11786.stdout b/testsuite/tests/dependent/ghci/T11786.stdout
new file mode 100644
index 0000000000..93616ed750
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T11786.stdout
@@ -0,0 +1,15 @@
+($) :: (a -> b) -> a -> b
+(($)) :: (a -> b) -> a -> b
+($) :: (a -> b) -> a -> b
+($) :: (a -> b) -> a -> b 	-- Defined in ‘GHC.Base’
+infixr 0 $
+($) :: (a -> b) -> a -> b
+(($)) :: (a -> b) -> a -> b
+($)
+  :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
+     (a -> b) -> a -> b
+($) ::
+  forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
+  (a -> b) -> a -> b
+  	-- Defined in ‘GHC.Base’
+infixr 0 $
diff --git a/testsuite/tests/dependent/ghci/T14238.script b/testsuite/tests/dependent/ghci/T14238.script
new file mode 100644
index 0000000000..7c27123e00
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T14238.script
@@ -0,0 +1,4 @@
+:set -XTypeInType
+:m + Data.Kind
+data Foo (k :: Type) :: k -> Type
+:kind Foo
diff --git a/testsuite/tests/dependent/ghci/T14238.stdout b/testsuite/tests/dependent/ghci/T14238.stdout
new file mode 100644
index 0000000000..fddbc0de54
--- /dev/null
+++ b/testsuite/tests/dependent/ghci/T14238.stdout
@@ -0,0 +1 @@
+Foo :: forall k -> k -> *
diff --git a/testsuite/tests/dependent/ghci/all.T b/testsuite/tests/dependent/ghci/all.T
index 956272fa55..89ebab0e44 100644
--- a/testsuite/tests/dependent/ghci/all.T
+++ b/testsuite/tests/dependent/ghci/all.T
@@ -1,4 +1,3 @@
-test('T11549',
-     [ expect_broken( 11787 ),
-       expect_broken( 11786 ) ],
-     ghci_script, ['T11549.script'])
+test('T11549', normal, ghci_script, ['T11549.script'])
+test('T11786', normal, ghci_script, ['T11786.script'])
+test('T14238', normal, ghci_script, ['T14238.script'])
diff --git a/testsuite/tests/dependent/should_compile/Dep1.hs b/testsuite/tests/dependent/should_compile/Dep1.hs
index 6f8fe0720d..086d759bbe 100644
--- a/testsuite/tests/dependent/should_compile/Dep1.hs
+++ b/testsuite/tests/dependent/should_compile/Dep1.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module Dep1 where
 
diff --git a/testsuite/tests/dependent/should_compile/Dep3.hs b/testsuite/tests/dependent/should_compile/Dep3.hs
index cba5043a08..db10d2a8c6 100644
--- a/testsuite/tests/dependent/should_compile/Dep3.hs
+++ b/testsuite/tests/dependent/should_compile/Dep3.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeInType, GADTs #-}
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, GADTs #-}
 
 module Dep3 where
 
diff --git a/testsuite/tests/dependent/should_compile/DkNameRes.hs b/testsuite/tests/dependent/should_compile/DkNameRes.hs
new file mode 100644
index 0000000000..4110b33882
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/DkNameRes.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
+
+module DkNameRes where
+
+import Data.Proxy
+import Data.Kind
+
+type family IfK (e :: Proxy (j :: Bool)) :: Type where
+   IfK (_ :: Proxy True) = ()
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.hs b/testsuite/tests/dependent/should_compile/KindEqualities.hs
index 1f2e82c302..1caa46f7c3 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.hs
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.hs
@@ -3,6 +3,8 @@
 
 module KindEqualities where
 
+import Data.Kind
+
 data TyRep1 :: * -> * where
   TyInt1 :: TyRep1 Int
   TyBool1 :: TyRep1 Bool
@@ -13,7 +15,7 @@ zero1 TyBool1 = False
 
 data Proxy (a :: k) = P
 
-data TyRep :: k -> * where
+data TyRep :: forall k. k -> * where
   TyInt :: TyRep Int
   TyBool :: TyRep Bool
   TyMaybe :: TyRep Maybe
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.stderr b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
index af429d106b..ad9562eae8 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.stderr
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
@@ -1,5 +1,5 @@
 
-KindEqualities.hs:23:1: warning: [-Wincomplete-patterns (in -Wextra)]
+KindEqualities.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘zero’:
         Patterns not matched: (TyApp (TyApp _ _) _)
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities2.hs b/testsuite/tests/dependent/should_compile/KindEqualities2.hs
index 5a6f60d40b..0bdfcfa034 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities2.hs
+++ b/testsuite/tests/dependent/should_compile/KindEqualities2.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll,
-             TemplateHaskell, UndecidableInstances, ScopedTypeVariables,
-             TypeInType #-}
+             TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}
 
 module KindEqualities2 where
 
diff --git a/testsuite/tests/dependent/should_compile/KindLevels.hs b/testsuite/tests/dependent/should_compile/KindLevels.hs
index 1aad299df3..5540ce40cd 100644
--- a/testsuite/tests/dependent/should_compile/KindLevels.hs
+++ b/testsuite/tests/dependent/should_compile/KindLevels.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module KindLevels where
 
diff --git a/testsuite/tests/dependent/should_compile/Makefile b/testsuite/tests/dependent/should_compile/Makefile
index 9101fbd40a..0f855180c0 100644
--- a/testsuite/tests/dependent/should_compile/Makefile
+++ b/testsuite/tests/dependent/should_compile/Makefile
@@ -1,3 +1,8 @@
 TOP=../../..
 include $(TOP)/mk/boilerplate.mk
 include $(TOP)/mk/test.mk
+
+T13938:
+	$(RM) T13938a.hi T13938a.o T13938.hi T13938.o
+	'$(TEST_HC)' $(TEST_HC_OPTS) -O -c T13938a.hs
+	'$(TEST_HC)' $(TEST_HC_OPTS) -O -c T13938.hs
diff --git a/testsuite/tests/dependent/should_compile/RAE_T32b.hs b/testsuite/tests/dependent/should_compile/RAE_T32b.hs
index 7e067099c9..ddd21db18d 100644
--- a/testsuite/tests/dependent/should_compile/RAE_T32b.hs
+++ b/testsuite/tests/dependent/should_compile/RAE_T32b.hs
@@ -1,23 +1,27 @@
 {-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, DataKinds, PolyKinds,
-             RankNTypes, TypeOperators, TypeInType #-}
+             RankNTypes, TypeOperators #-}
 
 module RAE_T32b where
 
 import Data.Kind
 
-data family Sing (k :: *) :: k -> *
+data family Sing (k :: Type) :: k -> Type
 
-data TyArr (a :: *) (b :: *) :: *
-type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2
+data TyArr (a :: Type) (b :: Type) :: Type
+type family (a :: TyArr k1 k2 -> Type) @@ (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
+data Sigma (p :: Type) (r :: TyArr p Type -> Type) :: Type where
+  Sigma :: forall (p :: Type) (r :: TyArr p Type -> Type)
+                  (a :: p) (b :: r @@ a).
+           Sing Type p -> Sing (TyArr p Type -> Type) 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).
+data instance Sing (Sigma p r) (x :: Sigma p r) :: Type where
+  SSigma :: forall (p :: Type) (r :: TyArr p Type -> Type)
+                   (a :: p) (b :: r @@ a)
+                   (sp :: Sing Type p) (sr :: Sing (TyArr p Type -> Type) 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
index cedc019cf3..7a50b606ee 100644
--- a/testsuite/tests/dependent/should_compile/Rae31.hs
+++ b/testsuite/tests/dependent/should_compile/Rae31.hs
@@ -1,24 +1,27 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators, PolyKinds, DataKinds,
-             TypeFamilies, TypeInType #-}
+             TypeFamilies #-}
 
 module A where
 
 import Data.Kind
 
-data family Sing (k :: *) :: k -> *
+data family Sing (k :: Type) :: k -> Type
 type Sing' (x :: k) = Sing k x
-data TyFun' (a :: *) (b :: *) :: *
-type TyFun (a :: *) (b :: *) = TyFun' a b -> *
+data TyFun' (a :: Type) (b :: Type) :: Type
+type TyFun (a :: Type) (b :: Type) = TyFun' a b -> Type
 type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2
-data TyPi' (a :: *) (b :: TyFun a *) :: *
-type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> *
+data TyPi' (a :: Type) (b :: TyFun a Type) :: Type
+type TyPi (a :: Type) (b :: TyFun a Type) = TyPi' a b -> Type
 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 = *
+data A (a :: Type) (b :: a) (c :: TyFun' a Type)
+  -- A :: forall a -> a -> a ~> Type
+type instance (@@) (A a b) c = Type
 $(return [])
-data B (a :: *) (b :: TyFun' a *) -- B :: forall a -> a ~> *
+data B (a :: Type) (b :: TyFun' a Type)
+  -- B :: forall a -> a ~> Type
 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) *)
+data C (a :: Type) (b :: TyPi a (B a)) (c :: a) (d :: a)
+       (e :: TyFun' (b @@@ c @@@ d) Type)
diff --git a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
index e99c7b5dd5..b048a49e44 100644
--- a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
+++ b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs
@@ -1,5 +1,4 @@
-{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies,
-             TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies #-}
 {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
 
 module RaeBlogPost where
@@ -8,7 +7,7 @@ import Data.Kind
 
 -- a Proxy type with an explicit kind
 data Proxy k (a :: k) = P
-prox :: Proxy * Bool
+prox :: Proxy Type Bool
 prox = P
 
 prox2 :: Proxy Bool 'True
@@ -16,11 +15,11 @@ 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 -> *
+data B :: A -> Type
+data C :: B a -> Type
+data D :: C b -> Type
+data E :: D c -> Type
+-- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> Type
 
 -- a kind-indexed GADT
 data TypeRep (a :: k) where
@@ -37,7 +36,7 @@ type family a + b where
   'Zero     + b = b
   ('Succ a) + b = 'Succ (a + b)
 
-data Vec :: * -> Nat -> * where
+data Vec :: Type -> Nat -> Type where
   Nil  :: Vec a 'Zero
   (:>) :: a -> Vec a n -> Vec a ('Succ n)
 infixr 5 :>
@@ -47,17 +46,17 @@ 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 (*)
+-- datatype that mentions Type
+data U = Star (Type)
        | Bool Bool
 
 -- kind synonym
-type Monadish = * -> *
+type Monadish = Type -> Type
 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 = (* :: (* :: (* :: *)))
+-- yes, Type really does have type Type.
+type Star = (Type :: (Type :: (Type :: Type)))
diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
index 480db090c3..1a22573109 100644
--- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
+++ b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
@@ -3,7 +3,7 @@
 
 {-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications, AllowAmbiguousTypes,
              ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies,
-             TypeInType, ConstraintKinds, UndecidableInstances,
+             DataKinds, PolyKinds , ConstraintKinds, UndecidableInstances,
              FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies,
              FlexibleContexts, StandaloneDeriving, InstanceSigs,
              RankNTypes, UndecidableSuperClasses #-}
diff --git a/testsuite/tests/dependent/should_compile/T11405.hs b/testsuite/tests/dependent/should_compile/T11405.hs
index cdb713f118..5fdd7baed1 100644
--- a/testsuite/tests/dependent/should_compile/T11405.hs
+++ b/testsuite/tests/dependent/should_compile/T11405.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ImplicitParams, TypeInType, ExplicitForAll #-}
+{-# LANGUAGE ImplicitParams, PolyKinds, ExplicitForAll #-}
 
 module T11405 where
 
diff --git a/testsuite/tests/dependent/should_compile/T11635.hs b/testsuite/tests/dependent/should_compile/T11635.hs
index 1cbdbafb90..61d9978e55 100644
--- a/testsuite/tests/dependent/should_compile/T11635.hs
+++ b/testsuite/tests/dependent/should_compile/T11635.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-}
+{-# LANGUAGE PolyKinds, KindSignatures, ExplicitForAll, RankNTypes #-}
 
 module T11635 where
 
diff --git a/testsuite/tests/dependent/should_compile/T11711.hs b/testsuite/tests/dependent/should_compile/T11711.hs
index 0cd4dceb42..814b2a4a68 100644
--- a/testsuite/tests/dependent/should_compile/T11711.hs
+++ b/testsuite/tests/dependent/should_compile/T11711.hs
@@ -5,7 +5,6 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 
diff --git a/testsuite/tests/dependent/should_compile/T11719.hs b/testsuite/tests/dependent/should_compile/T11719.hs
index ba4d7c9db4..e4c2a89bf2 100644
--- a/testsuite/tests/dependent/should_compile/T11719.hs
+++ b/testsuite/tests/dependent/should_compile/T11719.hs
@@ -1,12 +1,12 @@
-{-# LANGUAGE RankNTypes, TypeFamilies, TypeInType, TypeOperators,
+{-# LANGUAGE RankNTypes, TypeFamilies, TypeOperators, DataKinds, PolyKinds,
              UndecidableInstances #-}
 
 module T11719 where
 
 import Data.Kind
 
-data TyFun :: * -> * -> *
-type a ~> b = TyFun a b -> *
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
 
 type family (f :: a ~> b) @@ (x :: a) :: b
 
diff --git a/testsuite/tests/dependent/should_compile/T11966.hs b/testsuite/tests/dependent/should_compile/T11966.hs
index 0262a0aed3..daad450f13 100644
--- a/testsuite/tests/dependent/should_compile/T11966.hs
+++ b/testsuite/tests/dependent/should_compile/T11966.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 
 module T11966 where
diff --git a/testsuite/tests/dependent/should_compile/T12176.hs b/testsuite/tests/dependent/should_compile/T12176.hs
new file mode 100644
index 0000000000..a11c151567
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T12176.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies #-}
+
+module T12176 where
+
+import Data.Kind
+
+data Proxy :: forall k. k -> Type where
+  MkProxy :: forall k (a :: k). Proxy a
+
+data X where
+  MkX :: forall (k :: Type) (a :: k). Proxy a -> X
+
+type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
+
+type family Foo (x :: forall (a :: k). Proxy a -> X) where
+  Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
+
+type Bug = Foo Expr  -- this failed with #12176
diff --git a/testsuite/tests/dependent/should_compile/T12442.hs b/testsuite/tests/dependent/should_compile/T12442.hs
index f9dbf0a486..c76dfb962e 100644
--- a/testsuite/tests/dependent/should_compile/T12442.hs
+++ b/testsuite/tests/dependent/should_compile/T12442.hs
@@ -1,7 +1,7 @@
 -- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr
 
-{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeOperators, TypeApplications,
-             GADTs, TypeFamilies, AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds, PolyKinds, ScopedTypeVariables, TypeOperators,
+             TypeApplications, GADTs, TypeFamilies, AllowAmbiguousTypes #-}
 
 module T12442 where
 
diff --git a/testsuite/tests/dependent/should_compile/T12742.hs b/testsuite/tests/dependent/should_compile/T12742.hs
new file mode 100644
index 0000000000..988d7c318a
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T12742.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds, PolyKinds, RankNTypes, TypeFamilies #-}
+
+module T12742 where
+
+import Data.Kind
+
+type family F :: forall k2. (k1, k2)
+
+data T :: (forall k2. (Bool, k2)) -> Type
+
+type S = T F
diff --git a/testsuite/tests/dependent/should_compile/T13910.hs b/testsuite/tests/dependent/should_compile/T13910.hs
new file mode 100644
index 0000000000..b3707dd365
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T13910.hs
@@ -0,0 +1,148 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module T13910 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data family Sing (a :: k)
+
+class SingKind k where
+  type Demote k = (r :: Type) | r -> k
+  fromSing :: Sing (a :: k) -> Demote k
+  toSing   :: Demote k -> SomeSing k
+
+data SomeSing k where
+  SomeSing :: Sing (a :: k) -> SomeSing k
+
+withSomeSing :: forall k r
+              . SingKind k
+             => Demote k
+             -> (forall (a :: k). Sing a -> r)
+             -> r
+withSomeSing x f =
+  case toSing x of
+    SomeSing x' -> f x'
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) | (:~>)
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+$(return [])
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+data instance Sing (z :: a :~: b) where
+  SRefl :: Sing Refl
+
+instance SingKind (a :~: b) where
+  type Demote (a :~: b) = a :~: b
+  fromSing SRefl = Refl
+  toSing Refl = SomeSing SRefl
+
+(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
+           Sing r
+        -> p @@ Refl
+        -> p @@ r
+(~>:~:) SRefl pRefl = pRefl
+
+type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
+                    (y :: t) (e :: from :~: y) = App t arr Type p y
+data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
+  :: forall (y :: t). from :~: y ~> Type
+type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
+  = WhyReplacePoly arr from p y x
+
+replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
+           p from
+        -> from :~: to
+        -> p to
+replace = replacePoly @(:->)
+
+replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
+                p @@ from
+             -> from :~: to
+             -> p @@ to
+replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p
+
+replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
+                      (p :: (t -?> Type) arr).
+               FunApp arr
+            => App t arr Type p from
+            -> from :~: to
+            -> App t arr Type p to
+replacePoly from eq =
+  withSomeSing eq $ \(singEq :: Sing r) ->
+    (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from
+
+type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)
+  = App t arr Type f a -> App t arr Type f z
+data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
+  :: t ~> Type
+type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z
+
+leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)
+                      (a :: t) (b :: t).
+               FunApp arr
+            => a :~: b
+            -> App t arr Type f a
+            -> App t arr Type f b
+leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id
+
+leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
+           a :~: b
+        -> f a
+        -> f b
+leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id
+-- The line above is what you get if you inline the definition of leibnizPoly.
+-- It causes a panic, however.
+--
+-- An equivalent implementation is commented out below, which does *not*
+-- cause GHC to panic.
+--
+-- leibniz = leibnizPoly @(:->)
+
+leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
+                a :~: b
+             -> f @@ a
+             -> f @@ b
+leibnizTyFun = leibnizPoly @(:~>) @_ @f
diff --git a/testsuite/tests/dependent/should_compile/T13938.hs b/testsuite/tests/dependent/should_compile/T13938.hs
new file mode 100644
index 0000000000..1ce77d194f
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T13938.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T13938 where
+
+import T13938a
+import Data.Kind
+import Data.Type.Equality
+import GHC.TypeLits
+
+type family Length (l :: [a]) :: Nat where {}
+type family Map (f :: a ~> b) (l :: [a]) :: [b] where {}
+
+type WhyMapPreservesLength (f :: x ~> y) (l :: [x])
+  = Length l :~: Length (Map f l)
+data WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type
+type instance Apply (WhyMapPreservesLengthSym1 f) l = WhyMapPreservesLength f l
+
+mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).
+                      Length l :~: Length (Map f l)
+mapPreservesLength
+  = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined undefined
diff --git a/testsuite/tests/dependent/should_compile/T13938a.hs b/testsuite/tests/dependent/should_compile/T13938a.hs
new file mode 100644
index 0000000000..5197747e87
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T13938a.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module T13938a where
+
+import Data.Kind (Type)
+
+data family Sing (a :: k)
+data instance Sing (z :: [a]) where
+  SNil  :: Sing '[]
+  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) -- ^ '(->)'
+              | (:~>) -- ^ '(~>)'
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+$(return [])
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
+            Sing l
+         -> p '[]
+         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
+         -> p l
+elimList = elimListPoly @(:->)
+
+elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
+                 Sing l
+              -> p @@ '[]
+              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
+              -> p @@ l
+elimListTyFun = elimListPoly @(:~>) @_ @p
+
+elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
+                FunApp arr
+             => Sing l
+             -> App [a] arr Type p '[]
+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
+             -> App [a] arr Type p l
+elimListPoly SNil                      pNil _     = pNil
+elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
diff --git a/testsuite/tests/dependent/should_compile/T14038.hs b/testsuite/tests/dependent/should_compile/T14038.hs
new file mode 100644
index 0000000000..04b24b9f9e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14038.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module T14038 where
+
+import Data.Kind (Type)
+
+data family Sing (a :: k)
+data instance Sing (z :: [a]) where
+  SNil  :: Sing '[]
+  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+data FunArrow = (:->) -- ^ '(->)'
+              | (:~>) -- ^ '(~>)'
+
+class FunType (arr :: FunArrow) where
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+class FunType arr => AppType (arr :: FunArrow) where
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
+            Sing l
+         -> p '[]
+         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
+         -> p l
+elimList = elimListPoly @(:->)
+
+elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
+                 Sing l
+              -> p @@ '[]
+              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
+              -> p @@ l
+elimListTyFun = elimListPoly @(:~>) @_ @p
+
+elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
+                FunApp arr
+             => Sing l
+             -> App [a] arr Type p '[]
+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
+             -> App [a] arr Type p l
+elimListPoly SNil                      pNil _     = pNil
+elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs
new file mode 100644
index 0000000000..1d6b72491e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14066a.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs,
+             UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+
+module T14066a where
+
+import Data.Proxy
+import Data.Kind
+import Data.Type.Bool
+
+
+type family Bar x y where
+  Bar (x :: a) (y :: b) = Int
+  Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be TyVarTvs and unify appropriately
+
+
+  -- the two k's, even though they have different scopes, should unify in the
+  -- kind-check and then work in the type-check because Prox3 has been generalized
+
+data Prox3 a where
+  MkProx3a :: Prox3 (a :: k1)
+  MkProx3b :: Prox3 (a :: k2)
+
+  -- This probably should be rejected, as it's polymorphic recursion without a CUSK.
+  -- But GHC accepts it because the polymorphic occurrence is at a type variable.
+data T0 a = forall k (b :: k). MkT0 (T0 b) Int
+
+  -- k and j should unify
+type family G x a where
+  G Int (b :: k) = Int
+  G Bool (c :: j) = Bool
+
+-- this last example just checks that GADT pattern-matching on kinds still works.
+-- nothing new here.
+data T (a :: k) where
+  MkT :: T (a :: Type -> Type)
+
+data S (a :: Type -> Type) where
+  MkS :: S a
+
+f :: forall k (a :: k). Proxy a -> T a -> ()
+f _ MkT = let y :: S a
+              y = MkS
+          in ()
+
+-- This is questionable. Should we use the RHS to determine dependency? It works
+-- now, but if it stops working in the future, that's not a deal-breaker.
+type P k a = Proxy (a :: k)
+
+
+-- This is a challenge. It should be accepted, but only because c's kind is learned
+-- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind,
+-- then GHC would need to be convinced that If (c's kind) b d always has kind `a`.
+-- Naively, we don't know about c's kind early enough.
+
+data SameKind :: forall k. k -> k -> Type
+type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
+   IfK (_ :: Proxy True)  f _ = f
+   IfK (_ :: Proxy False) _ g = g
+x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True))
+x _ = Proxy
+
+
+f2 :: forall b. b -> Proxy Maybe
+f2 x = fstOf3 y :: Proxy Maybe
+  where
+    y :: (Proxy a, Proxy c, b)
+    y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
+
+f3 :: forall b. b -> Proxy Maybe
+f3 x = fst y :: Proxy Maybe
+  where
+    y :: (Proxy a, b)
+    y = (Proxy, x)
+
+-- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables,
+-- so it is generalized, even with MonoLocalBinds.
+f4 x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+  where
+    y :: (Proxy a, Int)
+    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
new file mode 100644
index 0000000000..610e434d6c
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14066a.stderr
@@ -0,0 +1,5 @@
+
+T14066a.hs:13:3: warning:
+    Type family instance equation is overlapped:
+      forall d c (x :: c) (y :: d).
+        Bar x y = Bool -- Defined at T14066a.hs:13:3
diff --git a/testsuite/tests/dependent/should_compile/T14066h.hs b/testsuite/tests/dependent/should_compile/T14066h.hs
new file mode 100644
index 0000000000..df3db1c15d
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14066h.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ScopedTypeVariables, PolyKinds, MonoLocalBinds #-}
+
+module T14066h where
+
+import Data.Proxy
+
+f :: forall b. b -> (Proxy Int, Proxy Maybe)
+f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+  where
+    y :: (Proxy a, b)  -- this generalizes over the kind of a
+    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/T14556.hs b/testsuite/tests/dependent/should_compile/T14556.hs
new file mode 100644
index 0000000000..133a9e6a44
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14556.hs
@@ -0,0 +1,39 @@
+{-# Language UndecidableInstances, DataKinds, TypeOperators, PolyKinds,
+             TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
+
+module T14556 where
+
+import Data.Kind
+import Data.Proxy
+
+data Fn a b where
+  IdSym :: Fn Type Type
+
+type family
+  (@@) (f::Fn k k') (a::k)::k' where
+  IdSym @@ a = a
+
+data KIND = X | FNARR KIND KIND
+
+data TY :: KIND -> Type where
+  ID    :: TY (FNARR X X)
+  FNAPP :: TY (FNARR k k') -> TY k -> TY k'
+
+data TyRep (kind::KIND) :: TY kind -> Type where
+  TID    :: TyRep (FNARR X X)  ID
+  TFnApp :: TyRep (FNARR k k') f
+         -> TyRep k            a
+         -> TyRep k'           (FNAPP f a)
+
+type family
+  IK (kind::KIND) :: Type where
+  IK X            = Type
+  IK (FNARR k k') = Fn (IK k) (IK k')
+
+type family
+  IT (ty::TY kind) :: IK kind where
+  IT ID          = IdSym
+  IT (FNAPP f x) = IT f @@ IT x
+
+zero :: TyRep X a -> IT a
+zero = undefined
diff --git a/testsuite/tests/dependent/should_compile/T14720.hs b/testsuite/tests/dependent/should_compile/T14720.hs
new file mode 100644
index 0000000000..0f053756f5
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14720.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module T14720 where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..), sym, trans)
+import Data.Void
+
+data family Sing (z :: k)
+
+class Generic (a :: Type) where
+    type Rep a :: Type
+    from :: a -> Rep a
+    to :: Rep a -> a
+
+class PGeneric (a :: Type) where
+  type PFrom (x :: a)     :: Rep a
+  type PTo   (x :: Rep a) :: a
+
+class SGeneric k where
+  sFrom :: forall (a :: k).     Sing a -> Sing (PFrom a)
+  sTo   :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+class (PGeneric k, SGeneric k) => VGeneric k where
+  sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
+  sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
+
+data Decision a = Proved a
+                | Disproved (a -> Void)
+
+class SDecide k where
+  (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
+  default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
+               => Sing a -> Sing b -> Decision (a :~: b)
+  s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
+    Proved (Refl :: PFrom a :~: PFrom b) ->
+      case (sTof s1, sTof s2) of
+          (Refl, Refl) -> Proved Refl
+    Disproved contra -> Disproved (\Refl -> contra Refl)
diff --git a/testsuite/tests/dependent/should_compile/T14749.hs b/testsuite/tests/dependent/should_compile/T14749.hs
new file mode 100644
index 0000000000..c4480fad0f
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14749.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, PolyKinds #-}
+
+module T14749 where
+
+import Data.Kind
+
+data KIND = STAR | KIND :> KIND
+
+data Ty :: KIND -> Type where
+  TMaybe :: Ty (STAR :> STAR)
+  TApp   :: Ty (a :> b) -> (Ty a -> Ty b)
+
+type family IK (k :: KIND) = (res :: Type) where
+  IK STAR   = Type
+  IK (a:>b) = IK a -> IK b
+
+type family I (t :: Ty k) = (res :: IK k)  where
+  I TMaybe     = Maybe
+  I (TApp f a) = (I f) (I a)
+
+data TyRep (k :: KIND) (t :: Ty k) where
+  TyMaybe :: TyRep (STAR:>STAR) TMaybe
+  TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
+
+zero :: TyRep STAR a -> I a
+zero x = case x of
+            TyApp TyMaybe _ -> Nothing
diff --git a/testsuite/tests/dependent/should_compile/T14845_compile.hs b/testsuite/tests/dependent/should_compile/T14845_compile.hs
new file mode 100644
index 0000000000..04f50189b8
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14845_compile.hs
@@ -0,0 +1,16 @@
+{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
+{-# Language FlexibleContexts #-}
+{-# Language RankNTypes #-}
+{-# Language TypeOperators #-}
+module T14845 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data A :: Type -> Type where
+  MkA1 :: a ~  Int => A a
+  MkA2 :: a ~~ Int => A a
+
+data SA :: forall a. A a -> Type where
+  SMkA1 :: SA MkA1
+  SMkA2 :: SA MkA2
diff --git a/testsuite/tests/dependent/should_compile/T14991.hs b/testsuite/tests/dependent/should_compile/T14991.hs
new file mode 100644
index 0000000000..b2f5642ec5
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14991.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14991 where
+
+import Data.Kind
+
+type family Promote (k :: Type) :: Type
+type family PromoteX (a :: k) :: Promote k
+
+type family Demote (k :: Type) :: Type
+type family DemoteX (a :: k) :: Demote k
+
+-----
+-- Type
+-----
+
+type instance Demote Type = Type
+type instance Promote Type = Type
+
+type instance DemoteX (a :: Type) = Demote a
+type instance PromoteX (a :: Type) = Promote a
+
+-----
+-- Arrows
+-----
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type instance Demote  (a ~> b) = DemoteX  a -> DemoteX  b
+type instance Promote (a -> b) = PromoteX a ~> PromoteX b
diff --git a/testsuite/tests/dependent/should_compile/T15264.hs b/testsuite/tests/dependent/should_compile/T15264.hs
new file mode 100644
index 0000000000..a03cf4346e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15264.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE ExplicitForAll, PolyKinds #-}
+{-# OPTIONS -Wcompat #-}
+
+module T15264 where
+
+import Data.Proxy
+
+bad1 :: forall (a :: k). Proxy a -> ()
+bad1 _ = ()
+
+bad2 :: forall (a :: k1) (b :: k2). Proxy a -> ()
+bad2 _ = ()
+
+good :: forall k (a :: k). Proxy a -> ()
+good _ = ()
diff --git a/testsuite/tests/dependent/should_compile/T15264.stderr b/testsuite/tests/dependent/should_compile/T15264.stderr
new file mode 100644
index 0000000000..222d686513
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15264.stderr
@@ -0,0 +1,10 @@
+
+T15264.hs:8:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
+    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k’
+    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
+    Suggested fix: add ‘forall k.’
+
+T15264.hs:11:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
+    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k1’, ‘k2’
+    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
+    Suggested fix: add ‘forall k1 k2.’
diff --git a/testsuite/tests/dependent/should_compile/T15346.hs b/testsuite/tests/dependent/should_compile/T15346.hs
new file mode 100644
index 0000000000..3d8d49b9d2
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15346.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeApplications #-}
+module T15346 where
+
+import Data.Kind
+import Data.Proxy
+
+-----
+
+type family Rep (a :: Type) :: Type
+type instance Rep () = ()
+
+type family PFrom (x :: a) :: Rep a
+
+-----
+
+class SDecide k where
+  test :: forall (a :: k). Proxy a
+
+instance SDecide () where
+  test = undefined
+
+test1 :: forall (a :: k). SDecide (Rep k) => Proxy a
+test1 = seq (test @_ @(PFrom a)) Proxy
+
+test2 :: forall (a :: ()). Proxy a
+test2 = test1
diff --git a/testsuite/tests/dependent/should_compile/T15419.hs b/testsuite/tests/dependent/should_compile/T15419.hs
new file mode 100644
index 0000000000..68f20e5604
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15419.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T15419 where
+
+import Data.Kind
+
+data Prod a b
+data Proxy p = Proxy
+
+-----
+
+data family Sing :: forall k. k -> Type
+data instance Sing x = STuple
+
+-----
+
+type family Rep1 (f :: k -> Type) :: k -> Type
+type instance Rep1 ((,) a) = Prod a
+
+type family From1 (f :: Type -> Type) a (z :: f a) :: Rep1 f a
+type family To1 (f :: Type -> Type) a (z :: Rep1 f a) :: f a
+
+class Generic1 (f :: Type -> Type) where
+  sFrom1 :: forall (a :: Type) (z :: f a).      Proxy z -> Sing (From1 f a z)
+  sTo1   :: forall (a :: Type) (r :: Rep1 f a). Proxy r -> Proxy (To1 f a r :: f a)
+
+instance Generic1 ((,) a) where
+  sFrom1 Proxy = undefined
+  sTo1   Proxy = undefined
+
+-----
+
+type family Fmap (g :: b) (x :: f a) :: f b
+type instance Fmap (g :: b) (x :: (u, a)) = To1 ((,) u) b (Fmap g (From1 ((,) u) a x))
+
+class PFunctor (f :: Type -> Type) where
+  sFmap         :: forall a b (g :: b) (x :: f a).
+                   Proxy g -> Sing x -> Proxy (Fmap g x)
+
+instance PFunctor (Prod a) where
+  sFmap _ STuple = undefined
+
+sFmap1 :: forall (f :: Type -> Type) (u :: Type) (b :: Type) (g :: b) (x :: f u).
+                 (Generic1 f,
+                  PFunctor (Rep1 f),
+                  Fmap g x ~ To1 f b (Fmap g (From1 f u x)) )
+              => Proxy g -> Proxy x -> Proxy (Fmap g x)
+sFmap1 sg sx = sTo1 (sFmap sg (sFrom1 sx))
+
+sFmap2  :: forall (p :: Type) (a :: Type) (b :: Type) (g :: b) (x :: (p, a)).
+          Proxy g -> Proxy x -> Proxy (Fmap g x)
+sFmap2 = sFmap1
diff --git a/testsuite/tests/dependent/should_compile/T9632.hs b/testsuite/tests/dependent/should_compile/T9632.hs
index bea468fff3..f2099aa22b 100644
--- a/testsuite/tests/dependent/should_compile/T9632.hs
+++ b/testsuite/tests/dependent/should_compile/T9632.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module T9632 where
 
diff --git a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs
index 19f605c8cd..0e2f0c7744 100644
--- a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs
+++ b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType, UnicodeSyntax, GADTs, NoImplicitPrelude,
+{-# LANGUAGE DataKinds, PolyKinds, UnicodeSyntax, GADTs, NoImplicitPrelude,
              TypeOperators, TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
 
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 8a9b221a4e..418fba2d85 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -10,10 +10,14 @@ test('RaeBlogPost', normal, compile, [''])
 test('mkGADTVars', normal, compile, [''])
 test('TypeLevelVec',normal,compile, [''])
 test('T9632', normal, compile, [''])
-# Simon says in #11330: The "simplifier ticks exhausted" error is expected;
-# see Section 7 of the paper:
-# http://research.microsoft.com/en-us/um/people/simonpj/papers/haskell-dynamic/
-test('dynamic-paper', expect_fail_for(['optasm', 'optllvm']), compile, [''])
+# The dynamic-paper test fails in the profasm way if we don't increase
+# the simplifier tick limit. If we do, we run out of stack
+# space. If we increase the stack size enough with -K,
+# we run out of simplifier ticks again. This is
+# discussed in #11330.
+test('dynamic-paper',
+     expect_broken_for(11330, ['profasm']),
+     compile_fail, [''])
 test('T11311', normal, compile, [''])
 test('T11405', normal, compile, [''])
 test('T11241', normal, compile, [''])
@@ -24,3 +28,29 @@ test('T11719', normal, compile, [''])
 test('T11966', normal, compile, [''])
 test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
+test('T12176', normal, compile, [''])
+test('T14038', normal, compile, [''])
+test('T12742', normal, compile, [''])
+# we omit profasm because it doesn't bring much to the table but
+# introduces its share of complexity, as the test as it is fails with
+# profasm:
+# T13910.hs:6:5: fatal:
+#     Cannot load -prof objects when GHC is built with -dynamic
+#     To fix this, either:
+#       (1) Use -fexternal-interpreter, or
+#       (2) Build the program twice: once with -dynamic, and then
+#           with -prof using -osuf to set a different object file suffix.
+test('T13910', omit_ways(['profasm']), compile, [''])
+test('T13938', [extra_files(['T13938a.hs'])], run_command,
+     ['$MAKE -s --no-print-directory T13938'])
+test('T14556', normal, compile, [''])
+test('T14720', normal, compile, [''])
+test('T14066a', normal, compile, [''])
+test('T14749', normal, compile, [''])
+test('T14845_compile', normal, compile, [''])
+test('T14991', normal, compile, [''])
+test('T15264', normal, compile, [''])
+test('DkNameRes', normal, compile, [''])
+test('T15346', normal, compile, [''])
+test('T15419', normal, compile, [''])
+test('T14066h', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
index 1aa4ee54d9..c998f0967c 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
@@ -7,7 +7,7 @@ Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -}
 {-#  LANGUAGE RankNTypes, PolyKinds, TypeOperators,
              ScopedTypeVariables, GADTs, FlexibleInstances,
              UndecidableInstances, RebindableSyntax,
-             DataKinds, MagicHash, AutoDeriveTypeable, TypeInType  #-}
+             DataKinds, MagicHash #-}
 {-# OPTIONS_GHC -Wno-missing-methods -Wno-redundant-constraints #-}
 {-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
   -- Because we define a local Typeable class and have
@@ -127,7 +127,7 @@ gcast x = do  Refl <- eqT  (typeRep :: TypeRep a)
                            (typeRep :: TypeRep b)
               return x
 
-data SameKind :: k -> k -> *
+data SameKind :: k -> k -> Type
 type CheckAppResult = SameKind AppResult AppResultNoKind
   --  not the most thorough check
 foo :: AppResult x -> AppResultNoKind x
@@ -170,17 +170,20 @@ dynFst :: Dynamic -> Maybe Dynamic
 dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))
 
   = do  App (rpa  :: TypeRep pa ) (rb :: TypeRep b)  <- splitApp rpab
-            --  introduces kind |k2|, and types |pa :: k2 -> *|, |b :: k2|
+            --  introduces kind |k2|, and types |pa :: k2 -> Type|, |b :: k2|
 
         App (rp   :: TypeRep p  ) (ra :: TypeRep a)  <- splitApp rpa
-            --  introduces kind |k1|, and types |p :: k1 -> k2 -> *|, |a :: k1|
+            --  introduces kind |k1|, and types |p :: k1 -> k2 -> Type|,
+            --                                  |a :: k1|
 
         Refl       <- eqT rp (typeRep :: TypeRep (,))
-            --  introduces |p ~ (,)| and |(k1 -> k2 -> *) ~ (* -> * -> *)|
+            --  introduces |p ~ (,)| and
+            --             |(k1 -> k2 -> Type) ~ (Type -> Type -> Type)|
 
         return (Dyn ra (fst x))
 
-eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~: b)
+eqT :: forall k1 k2 (a :: k1) (b :: k2).
+       TypeRep a -> TypeRep b -> Maybe (a :~: b)
 
 data (a :: k1) :~: (b :: k2) where
   Refl :: forall k (a :: k). a :~: a
@@ -201,11 +204,13 @@ data SomeTypeRep where
 
 type TyMapLessTyped = Map SomeTypeRep Dynamic
 
-insertLessTyped    ::  forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
-insertLessTyped x  =   Map.insert (SomeTypeRep (typeRep :: TypeRep a)) (toDynamic x)
+insertLessTyped :: forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
+insertLessTyped x
+  = Map.insert (SomeTypeRep (typeRep :: TypeRep a)) (toDynamic x)
 
-lookupLessTyped  ::  forall a. Typeable a => TyMapLessTyped -> Maybe a
-lookupLessTyped  =   fromDynamic <=< Map.lookup (SomeTypeRep (typeRep :: TypeRep a))
+lookupLessTyped :: forall a. Typeable a => TyMapLessTyped -> Maybe a
+lookupLessTyped
+  = fromDynamic <=< Map.lookup (SomeTypeRep (typeRep :: TypeRep a))
 
 instance Ord SomeTypeRep where
   compare (SomeTypeRep tr1) (SomeTypeRep tr2) = compareTypeRep tr1 tr2
@@ -329,7 +334,7 @@ dynApplyOld (DynOld trf f) (DynOld trx x) =
 data DynamicClosed where
   DynClosed :: TypeRepClosed a -> a -> DynamicClosed
 
-data TypeRepClosed (a :: *) where
+data TypeRepClosed (a :: Type) where
   TBool  :: TypeRepClosed Bool
   TFun   :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a -> b)
   TProd  :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a, b)
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
new file mode 100644
index 0000000000..3ba4db2219
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
@@ -0,0 +1,15 @@
+Simplifier ticks exhausted
+  When trying UnfoldingDone delta1
+  To increase the limit, use -fsimpl-tick-factor=N (default 100).
+   
+  If you need to increase the limit substantially, please file a
+  bug report and indicate the factor you needed.
+   
+  If GHC was unable to complete compilation even with a very large factor
+  (a thousand or more), please consult the "Known bugs or infelicities"
+  section in the Users Guide before filing a report. There are a
+  few situations unlikely to occur in practical programs for which
+  simplifier non-termination has been judged acceptable.
+   
+  To see detailed counts use -ddump-simpl-stats
+  Total ticks: 140004
diff --git a/testsuite/tests/dependent/should_compile/mkGADTVars.hs b/testsuite/tests/dependent/should_compile/mkGADTVars.hs
index 1e74c6980a..9b48e8c395 100644
--- a/testsuite/tests/dependent/should_compile/mkGADTVars.hs
+++ b/testsuite/tests/dependent/should_compile/mkGADTVars.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, TypeInType #-}
+{-# LANGUAGE GADTs, PolyKinds #-}
 
 module GADTVars where
 
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, [''])
diff --git a/testsuite/tests/dependent/should_run/T11964a.hs b/testsuite/tests/dependent/should_run/T11964a.hs
index f0576542b6..2c6993fef0 100644
--- a/testsuite/tests/dependent/should_run/T11964a.hs
+++ b/testsuite/tests/dependent/should_run/T11964a.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 module T11964a where
 import Data.Kind
 type Star = Type