Embrace -XTypeInType, add -XStarIsType

Summary:
Implement the "Embrace Type :: Type" GHC proposal,
.../ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst

GHC 8.0 included a major change to GHC's type system: the Type :: Type
axiom. Though casual users were protected from this by hiding its
features behind the -XTypeInType extension, all programs written in GHC
8+ have the axiom behind the scenes. In order to preserve backward
compatibility, various legacy features were left unchanged. For example,
with -XDataKinds but not -XTypeInType, GADTs could not be used in types.
Now these restrictions are lifted and -XTypeInType becomes a redundant
flag that will be eventually deprecated.

* Incorporate the features currently in -XTypeInType into the
  -XPolyKinds and -XDataKinds extensions.
* Introduce a new extension -XStarIsType to control how to parse * in
  code and whether to print it in error messages.

Test Plan: Validate

Reviewers: goldfire, hvr, bgamari, alanz, simonpj

Reviewed By: goldfire, simonpj

Subscribers: rwbarton, thomie, mpickering, carter

GHC Trac Issues: #15195

Differential Revision: https://phabricator.haskell.org/D4748

36 files changed, 76 insertions, 72 deletions

diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.hs b/testsuite/tests/dependent/should_fail/BadTelescope.hs
index acabffec54..11b52f36e2 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module BadTelescope where
 
diff --git a/testsuite/tests/dependent/should_fail/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/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/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/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/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/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/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 046a1e1aa4..41f5d7cd4c 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
@@ -1,10 +1,10 @@
 
-RAE_T32a.hs:28:1: error:
+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:
+RAE_T32a.hs:29:20: error:
     • Expecting two more arguments to ‘Sigma’
       Expected a type, but
       ‘Sigma’ has kind
@@ -12,7 +12,7 @@ RAE_T32a.hs:28:20: error:
     • In the first argument of ‘Sing’, namely ‘Sigma’
       In the data instance declaration for ‘Sing’
 
-RAE_T32a.hs:28:27: error:
+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/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 772ac78bfa..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)
diff --git a/testsuite/tests/dependent/should_fail/T13601.hs b/testsuite/tests/dependent/should_fail/T13601.hs
index 5e98c7a657..a8fa34d4a0 100644
--- a/testsuite/tests/dependent/should_fail/T13601.hs
+++ b/testsuite/tests/dependent/should_fail/T13601.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, DataKinds, TypeInType #-}
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
 
 import GHC.Exts
 import Prelude (Bool(True,False),Integer,Ordering,undefined)
diff --git a/testsuite/tests/dependent/should_fail/T13780a.hs b/testsuite/tests/dependent/should_fail/T13780a.hs
index 1f7c95c40a..b7e1510672 100644
--- a/testsuite/tests/dependent/should_fail/T13780a.hs
+++ b/testsuite/tests/dependent/should_fail/T13780a.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 module T13780a where
 
 data family Sing (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T13780b.hs b/testsuite/tests/dependent/should_fail/T13780b.hs
index 238e7a1af9..dc6ac89c08 100644
--- a/testsuite/tests/dependent/should_fail/T13780b.hs
+++ b/testsuite/tests/dependent/should_fail/T13780b.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 module T13780b where
 
 data family Sing (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T13780c.hs b/testsuite/tests/dependent/should_fail/T13780c.hs
index eee6436237..78e09f5ef1 100644
--- a/testsuite/tests/dependent/should_fail/T13780c.hs
+++ b/testsuite/tests/dependent/should_fail/T13780c.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 module T13780c where
 
 import Data.Kind
diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr
index 065c700dfc..9a196f4bd7 100644
--- a/testsuite/tests/dependent/should_fail/T13780c.stderr
+++ b/testsuite/tests/dependent/should_fail/T13780c.stderr
@@ -2,11 +2,13 @@
 [2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
 
 T13780c.hs:11:16: error:
-    • Expected kind ‘Sing _1’, but ‘SFalse’ has kind ‘Sing 'False’
+    • 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:
-    • Expected kind ‘Sing _1’, but ‘STrue’ has kind ‘Sing 'True’
+    • 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/T14066.hs b/testsuite/tests/dependent/should_fail/T14066.hs
index 58396df591..709d507a34 100644
--- a/testsuite/tests/dependent/should_fail/T14066.hs
+++ b/testsuite/tests/dependent/should_fail/T14066.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeInType #-}
-{-# LANGUAGE KindSignatures #-}
+
+
 
 module T14066 where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066c.hs b/testsuite/tests/dependent/should_fail/T14066c.hs
index b4597d2cec..4dd6f41973 100644
--- a/testsuite/tests/dependent/should_fail/T14066c.hs
+++ b/testsuite/tests/dependent/should_fail/T14066c.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, TypeInType, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, UndecidableInstances #-}
 
 module T14066c where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066d.hs b/testsuite/tests/dependent/should_fail/T14066d.hs
index ea47644688..dd5676826d 100644
--- a/testsuite/tests/dependent/should_fail/T14066d.hs
+++ b/testsuite/tests/dependent/should_fail/T14066d.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeInType #-}
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, PolyKinds #-}
 
 module T14066d where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066e.hs b/testsuite/tests/dependent/should_fail/T14066e.hs
index 9b799e542c..9bce332527 100644
--- a/testsuite/tests/dependent/should_fail/T14066e.hs
+++ b/testsuite/tests/dependent/should_fail/T14066e.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MonoLocalBinds, TypeInType, ScopedTypeVariables #-}
+{-# LANGUAGE MonoLocalBinds, PolyKinds, ScopedTypeVariables #-}
 
 module T14066e where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066f.hs b/testsuite/tests/dependent/should_fail/T14066f.hs
index ccb7ceac0e..b2035f2c3d 100644
--- a/testsuite/tests/dependent/should_fail/T14066f.hs
+++ b/testsuite/tests/dependent/should_fail/T14066f.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
 
 module T14066f where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066g.hs b/testsuite/tests/dependent/should_fail/T14066g.hs
index df0e03b173..b07a2c36a9 100644
--- a/testsuite/tests/dependent/should_fail/T14066g.hs
+++ b/testsuite/tests/dependent/should_fail/T14066g.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
 
 module T14066g where
 
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs
index 7e7ecd31c9..a20ae30958 100644
--- a/testsuite/tests/dependent/should_fail/T14066h.hs
+++ b/testsuite/tests/dependent/should_fail/T14066h.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ScopedTypeVariables, TypeInType, MonoLocalBinds #-}
+{-# LANGUAGE ScopedTypeVariables, PolyKinds, MonoLocalBinds #-}
 
 module T14066h where
 
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/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
index 02b7737499..1f958de426 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
@@ -1,4 +1,4 @@
-{-# 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/all.T b/testsuite/tests/dependent/should_fail/all.T
index 7273445548..5ae037dc54 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -10,7 +10,6 @@ test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334b', normal, compile_fail, [''])
-test('KindLevelsB', normal, compile_fail, [''])
 test('T11473', normal, compile_fail, [''])
 test('T11471', normal, compile_fail, [''])
 test('T12174', normal, compile_fail, [''])
@@ -28,3 +27,4 @@ test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
 test('T14066h', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
+test('T15245', normal, compile_fail, [''])