diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 216b7c057e37a5a6f0ad63304a6d9e1796e3ce9c..b878a5b45b4cf276930cfd3f6061ebeaacb15262 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -6,6 +6,7 @@
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
+{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DisambiguateRecordFields #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
@@ -752,8 +753,7 @@ tc_infer_id id_name
AGlobal (AConLike (RealDataCon con)) -> tcInferDataCon con
AGlobal (AConLike (PatSynCon ps)) -> tcInferPatSyn id_name ps
- AGlobal (ATyCon tc) -> fail_tycon tc
- ATcTyCon tc -> fail_tycon tc
+ (tcTyThingTyCon_maybe -> Just tc) -> fail_tycon tc -- TyCon or TcTyCon
ATyVar name _ -> fail_tyvar name
_ -> failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 6fd2be5b053b92f91740afb75c4349ca316ca345..b5386aa6a79365e10927bf0e8888e3f7af511238 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1536,8 +1536,8 @@ tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
-- application. In particular, for a HsTyVar (which includes type
-- constructors, it does not zoom off into tcInferTyApps and family
-- saturation
-tcInferTyAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
- = tcTyVar mode tv
+tcInferTyAppHead _ (L _ (HsTyVar _ _ (L _ tv)))
+ = tcTyVar tv
tcInferTyAppHead mode ty
= tc_infer_lhs_type mode ty
@@ -1558,7 +1558,7 @@ tcInferTyApps, tcInferTyApps_nosat
-> LHsType GhcRn -- ^ Function (for printing only)
-> TcType -- ^ Function
-> [LHsTypeArg GhcRn] -- ^ Args
- -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
+ -> TcM (TcType, TcKind) -- ^ (f args, result kind)
tcInferTyApps mode hs_ty fun hs_args
= do { (f_args, res_k) <- tcInferTyApps_nosat mode hs_ty fun hs_args
; saturateFamApp f_args res_k }
@@ -1967,24 +1967,19 @@ tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
---------------------------
-tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
+tcTyVar :: Name -> TcM (TcType, TcKind)
-- See Note [Type checking recursive type and class declarations]
-- in GHC.Tc.TyCl
-- This does not instantiate. See Note [Do not always instantiate eagerly in types]
-tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
+tcTyVar name -- Could be a tyvar, a tycon, or a datacon
= do { traceTc "lk1" (ppr name)
; thing <- tcLookup name
; case thing of
ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
-- See Note [Recursion through the kinds]
- ATcTyCon tc_tc
- -> do { check_tc tc_tc
- ; return (mkTyConTy tc_tc, tyConKind tc_tc) }
-
- AGlobal (ATyCon tc)
- -> do { check_tc tc
- ; return (mkTyConTy tc, tyConKind tc) }
+ (tcTyThingTyCon_maybe -> Just tc) -- TyCon or TcTyCon
+ -> return (mkTyConTy tc, tyConKind tc)
AGlobal (AConLike (RealDataCon dc))
-> do { data_kinds <- xoptM LangExt.DataKinds
@@ -2006,13 +2001,6 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
_ -> wrongThingErr "type" thing name }
where
- check_tc :: TyCon -> TcM ()
- check_tc tc = do { data_kinds <- xoptM LangExt.DataKinds
- ; unless (isTypeLevel (mode_tyki mode) ||
- data_kinds ||
- isKindTyCon tc) $
- promotionErr name NoDataKindsTC }
-
-- We cannot promote a data constructor with a context that contains
-- constraints other than equalities, so error if we find one.
-- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
@@ -4279,7 +4267,6 @@ promotionErr name err
-> text "it has an unpromotable context"
<+> quotes (ppr pred)
FamDataConPE -> text "it comes from a data family instance"
- NoDataKindsTC -> text "perhaps you intended to use DataKinds"
NoDataKindsDC -> text "perhaps you intended to use DataKinds"
PatSynPE -> text "pattern synonyms cannot be promoted"
RecDataConPE -> same_rec_group_msg
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index df9384fea2755a7b99ec02d41ad2e5ed6d37b660..2de119b416c45a012f690a762eaf5cc2ab844cec 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -46,7 +46,8 @@ module GHC.Tc.Types(
-- Typechecker types
TcTypeEnv, TcBinderStack, TcBinder(..),
- TcTyThing(..), PromotionErr(..),
+ TcTyThing(..), tcTyThingTyCon_maybe,
+ PromotionErr(..),
IdBindingInfo(..), ClosedTypeId, RhsNames,
IsGroupClosed(..),
SelfBootInfo(..),
@@ -1125,6 +1126,12 @@ data TcTyThing
| APromotionErr PromotionErr
+-- | Matches on either a global 'TyCon' or a 'TcTyCon'.
+tcTyThingTyCon_maybe :: TcTyThing -> Maybe TyCon
+tcTyThingTyCon_maybe (AGlobal (ATyCon tc)) = Just tc
+tcTyThingTyCon_maybe (ATcTyCon tc_tc) = Just tc_tc
+tcTyThingTyCon_maybe _ = Nothing
+
data PromotionErr
= TyConPE -- TyCon used in a kind before we are ready
-- data T :: T -> * where ...
@@ -1142,7 +1149,6 @@ data PromotionErr
| RecDataConPE -- Data constructor in a recursive loop
-- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl
- | NoDataKindsTC -- -XDataKinds not enabled (for a tycon)
| NoDataKindsDC -- -XDataKinds not enabled (for a datacon)
instance Outputable TcTyThing where -- Debugging only
@@ -1337,7 +1343,6 @@ instance Outputable PromotionErr where
ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE"
<+> parens (ppr pred)
ppr RecDataConPE = text "RecDataConPE"
- ppr NoDataKindsTC = text "NoDataKindsTC"
ppr NoDataKindsDC = text "NoDataKindsDC"
--------------
@@ -1362,7 +1367,6 @@ peCategory PatSynPE = "pattern synonym"
peCategory FamDataConPE = "data constructor"
peCategory ConstrainedDataConPE{} = "data constructor"
peCategory RecDataConPE = "data constructor"
-peCategory NoDataKindsTC = "type constructor"
peCategory NoDataKindsDC = "data constructor"
{-
diff --git a/testsuite/tests/typecheck/should_compile/T20873.hs b/testsuite/tests/typecheck/should_compile/T20873.hs
new file mode 100644
index 0000000000000000000000000000000000000000..825b12aece8b2d31b906fa4bf520dd348952a648
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20873.hs
@@ -0,0 +1,23 @@
+
+{-# LANGUAGE GADTSyntax, StandaloneKindSignatures, NoDataKinds #-}
+
+module T20873 where
+
+import Data.Kind ( Type )
+
+type U a = Type
+type V a = a
+
+type MyMaybe1 :: U Type -> U Type
+data MyMaybe1 a = MyJust1 a | MyNothing1
+
+type MyMaybe2 :: V Type -> V Type
+data MyMaybe2 a = MyJust2 a | MyNothing2
+
+data MyMaybe3 (a :: U Type) :: U Type where
+ MyJust3 :: a -> MyMaybe3 a
+ MyNothing3 :: MyMaybe3 a
+
+data MyMaybe4 (a :: V Type) :: V Type where
+ MyJust4 :: a -> MyMaybe4 a
+ MyNothing4 :: MyMaybe4 a
diff --git a/testsuite/tests/typecheck/should_compile/T20873b.hs b/testsuite/tests/typecheck/should_compile/T20873b.hs
new file mode 100644
index 0000000000000000000000000000000000000000..5abe5942a7d728487dff632bc0ddf8d6df138e05
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20873b.hs
@@ -0,0 +1,11 @@
+
+{-# LANGUAGE NoDataKinds #-}
+
+module T20873b where
+
+import T20873b_aux (P)
+
+type Q = P
+ -- P = 'MkA is a promoted data constructor,
+ -- but we should still allow users to use P with -XNoDataKinds,
+ -- to avoid implementation details of M1 leaking.
diff --git a/testsuite/tests/typecheck/should_compile/T20873b_aux.hs b/testsuite/tests/typecheck/should_compile/T20873b_aux.hs
new file mode 100644
index 0000000000000000000000000000000000000000..efd498471af8a9f533b4f08d516dfa522347441d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20873b_aux.hs
@@ -0,0 +1,7 @@
+
+{-# LANGUAGE DataKinds #-}
+
+module T20873b_aux where
+
+data A = MkA
+type P = 'MkA
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a3c89c0ab0c337d9cac00f3dea803dbdda32a56e..8b31c8b3ccb8591be48d611953c6c96057118b33 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -804,3 +804,6 @@ test('T20584b', normal, compile, [''])
test('T20588b', [extra_files(['T20588b.hs', 'T20588b.hs-boot', 'T20588b_aux.hs'])], multimod_compile, ['T20588b_aux.hs', '-v0'])
test('T20588d', [extra_files(['T20588d.hs', 'T20588d.hs-boot', 'T20588d_aux.hs'])], multimod_compile, ['T20588d_aux.hs', '-v0'])
test('T20661', [extra_files(['T20661.hs', 'T20661.hs-boot', 'T20661_aux.hs'])], multimod_compile, ['T20661_aux.hs', '-v0'])
+
+test('T20873', normal, compile, [''])
+test('T20873b', [extra_files(['T20873b_aux.hs'])], multimod_compile, ['T20873b', '-v0'])
diff --git a/testsuite/tests/typecheck/should_fail/T20873c.hs b/testsuite/tests/typecheck/should_fail/T20873c.hs
new file mode 100644
index 0000000000000000000000000000000000000000..776c061f137f3084d1029b89760e4646542ebd39
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20873c.hs
@@ -0,0 +1,11 @@
+
+{-# LANGUAGE GADTSyntax, NoKindSignatures, NoDataKinds #-}
+
+module T20873c where
+
+import Data.Kind ( Type )
+
+type U a = Type
+
+data Foo :: U Int where
+ MkFoo :: Foo
diff --git a/testsuite/tests/typecheck/should_fail/T20873c.stderr b/testsuite/tests/typecheck/should_fail/T20873c.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..972d01c583656e87aabe2a4440e2e2d1ad28f5a6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20873c.stderr
@@ -0,0 +1,5 @@
+
+T20873c.hs:10:1: error:
+ • Illegal kind signature ‘Foo’
+ (Use KindSignatures to allow kind signatures)
+ • In the data declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 908edcfe27a6facbea87637dce08be1f0487dd61..ff092df47885d27da6d71c6b9067357af8f03b43 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -628,3 +628,4 @@ test('T20542', normal, compile_fail, [''])
test('T20588', [extra_files(['T20588.hs', 'T20588.hs-boot', 'T20588_aux.hs'])], multimod_compile_fail, ['T20588_aux.hs', '-v0'])
test('T20588c', [extra_files(['T20588c.hs', 'T20588c.hs-boot', 'T20588c_aux.hs'])], multimod_compile_fail, ['T20588c_aux.hs', '-v0'])
test('T20189', normal, compile_fail, [''])
+test('T20873c', normal, compile_fail, [''])