diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index fd4d0350c4b32f5676f600f6129855bcc993cb09..c191f98244b0fc7432519f07c8e64ce7ec178b4f 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -56,7 +56,7 @@ module GHC.Core.TyCon(
         tyConMustBeSaturated,
         isPromotedDataCon, isPromotedDataCon_maybe,
         isDataKindsPromotedDataCon,
-        isKindTyCon, isLiftedTypeKindTyConName,
+        isKindTyCon, isKindName, isLiftedTypeKindTyConName,
         isTauTyCon, isFamFreeTyCon, isForgetfulSynTyCon,
 
         isDataTyCon,
@@ -2284,16 +2284,32 @@ isDataKindsPromotedDataCon (TyCon { tyConDetails = details })
               = not (isTypeDataCon dc)
   | otherwise = False
 
--- | Is this tycon really meant for use at the kind level? That is,
--- should it be permitted without -XDataKinds?
+-- | Is this 'TyCon' really meant for use at the kind level? That is,
+-- should it be permitted without @DataKinds@?
 isKindTyCon :: TyCon -> Bool
-isKindTyCon tc = getUnique tc `elementOfUniqSet` kindTyConKeys
+isKindTyCon = isKindUniquable
+
+-- | This is 'Name' really meant for use at the kind level? That is,
+-- should it be permitted wihout @DataKinds@?
+isKindName :: Name -> Bool
+isKindName = isKindUniquable
+
+-- | The workhorse for 'isKindTyCon' and 'isKindName'.
+isKindUniquable :: Uniquable a => a -> Bool
+isKindUniquable thing = getUnique thing `elementOfUniqSet` kindTyConKeys
 
 -- | These TyCons should be allowed at the kind level, even without
 -- -XDataKinds.
 kindTyConKeys :: UniqSet Unique
 kindTyConKeys = unionManyUniqSets
-  ( mkUniqSet [ liftedTypeKindTyConKey, liftedRepTyConKey, constraintKindTyConKey, tYPETyConKey ]
+  -- Make sure to keep this in sync with the following:
+  --
+  -- - The Overview section in docs/users_guide/exts/data_kinds.rst in the GHC
+  --   User's Guide.
+  --
+  -- - The typecheck/should_compile/T22141f.hs test case, which ensures that all
+  --   of these can successfully be used without DataKinds.
+  ( mkUniqSet [ liftedTypeKindTyConKey, liftedRepTyConKey, constraintKindTyConKey, tYPETyConKey, cONSTRAINTTyConKey ]
   : map (mkUniqSet . tycon_with_datacons) [ runtimeRepTyCon, levityTyCon
                                           , multiplicityTyCon
                                           , vecCountTyCon, vecElemTyCon ] )
diff --git a/compiler/GHC/Driver/Flags.hs b/compiler/GHC/Driver/Flags.hs
index d078255b4494dedc35d5616798d33679f9f02d3f..577b015d61489e523ee3ba7be6ec74607fa342bf 100644
--- a/compiler/GHC/Driver/Flags.hs
+++ b/compiler/GHC/Driver/Flags.hs
@@ -696,6 +696,7 @@ data WarningFlag =
    | Opt_WarnIncompleteRecordSelectors               -- Since 9.10
    | Opt_WarnBadlyStagedTypes                        -- Since 9.10
    | Opt_WarnInconsistentFlags                       -- Since 9.8
+   | Opt_WarnDataKindsTC                             -- Since 9.10
    deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Return the names of a WarningFlag
@@ -809,6 +810,7 @@ warnFlagNames wflag = case wflag of
   Opt_WarnIncompleteRecordSelectors               -> "incomplete-record-selectors" :| []
   Opt_WarnBadlyStagedTypes                        -> "badly-staged-types" :| []
   Opt_WarnInconsistentFlags                       -> "inconsistent-flags" :| []
+  Opt_WarnDataKindsTC                             -> "data-kinds-tc" :| []
 
 -- -----------------------------------------------------------------------------
 -- Standard sets of warning options
@@ -949,7 +951,8 @@ standardWarnings -- see Note [Documenting warning flags]
         Opt_WarnLoopySuperclassSolve,
         Opt_WarnBadlyStagedTypes,
         Opt_WarnTypeEqualityRequiresOperators,
-        Opt_WarnInconsistentFlags
+        Opt_WarnInconsistentFlags,
+        Opt_WarnDataKindsTC
       ]
 
 -- | Things you get with -W
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index d4cae261016680422de25a62994d80722cdf9f94..800bd321a15a6e3403dc9ec4dde8f5b60c5cd4d2 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -2284,6 +2284,7 @@ wWarningFlagsDeps = [minBound..maxBound] >>= \x -> case x of
   Opt_WarnImplicitRhsQuantification -> warnSpec x
   Opt_WarnIncompleteExportWarnings -> warnSpec x
   Opt_WarnIncompleteRecordSelectors -> warnSpec x
+  Opt_WarnDataKindsTC -> warnSpec x
 
 warningGroupsDeps :: [(Deprecation, FlagSpec WarningGroup)]
 warningGroupsDeps = map mk warningGroups
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index 6cf5387bddb09710be7cb3ac3ee3b0e0131c5ac5..e380b86f5ace24340385a69f1d4cf57281a6aa78 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -48,6 +48,7 @@ import GHC.Prelude
 import {-# SOURCE #-} GHC.Rename.Splice( rnSpliceType, checkThLocalTyName )
 
 import GHC.Core.TyCo.FVs ( tyCoVarsOfTypeList )
+import GHC.Core.TyCon    ( isKindName )
 import GHC.Hs
 import GHC.Rename.Env
 import GHC.Rename.Doc
@@ -528,7 +529,7 @@ rnHsTyKi env (HsQualTy { hst_ctxt = lctxt, hst_body = tau })
                           , hst_body =  tau' }
                 , fvs1 `plusFV` fvs2) }
 
-rnHsTyKi env (HsTyVar _ ip (L loc rdr_name))
+rnHsTyKi env tv@(HsTyVar _ ip (L loc rdr_name))
   = do { when (isRnKindLevel env && isRdrTyVar rdr_name) $
          unlessXOptM LangExt.PolyKinds $ addErr $
          TcRnWithHsDocContext (rtke_ctxt env) $
@@ -539,6 +540,12 @@ rnHsTyKi env (HsTyVar _ ip (L loc rdr_name))
        ; this_mod <- getModule
        ; when (nameIsLocalOrFrom this_mod name) $
          checkThLocalTyName name
+       ; when (isDataConName name && not (isKindName name)) $
+           -- Any use of a promoted data constructor name (that is not
+           -- specifically exempted by isKindName) is illegal without the use
+           -- of DataKinds. See Note [Checking for DataKinds] in
+           -- GHC.Tc.Validity.
+           checkDataKinds env tv
        ; when (isDataConName name && not (isPromoted ip)) $
          -- NB: a prefix symbolic operator such as (:) is represented as HsTyVar.
             addDiagnostic (TcRnUntickedPromotedThing $ UntickedConstructor Prefix name)
@@ -593,9 +600,8 @@ rnHsTyKi env (HsFunTy u mult ty1 ty2)
                 , plusFVs [fvs1, fvs2, w_fvs]) }
 
 rnHsTyKi env listTy@(HsListTy x ty)
-  = do { data_kinds <- xoptM LangExt.DataKinds
-       ; when (not data_kinds && isRnKindLevel env)
-              (addErr (dataKindsErr env listTy))
+  = do { when (isRnKindLevel env) $
+           checkDataKinds env listTy
        ; (ty', fvs) <- rnLHsTyKi env ty
        ; return (HsListTy x ty', fvs) }
 
@@ -610,23 +616,20 @@ rnHsTyKi env (HsKindSig x ty k)
 -- Unboxed tuples are allowed to have poly-typed arguments.  These
 -- sometimes crop up as a result of CPR worker-wrappering dictionaries.
 rnHsTyKi env tupleTy@(HsTupleTy x tup_con tys)
-  = do { data_kinds <- xoptM LangExt.DataKinds
-       ; when (not data_kinds && isRnKindLevel env)
-              (addErr (dataKindsErr env tupleTy))
+  = do { when (isRnKindLevel env) $
+           checkDataKinds env tupleTy
        ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
        ; return (HsTupleTy x tup_con tys', fvs) }
 
 rnHsTyKi env sumTy@(HsSumTy x tys)
-  = do { data_kinds <- xoptM LangExt.DataKinds
-       ; when (not data_kinds && isRnKindLevel env)
-              (addErr (dataKindsErr env sumTy))
+  = do { when (isRnKindLevel env) $
+           checkDataKinds env sumTy
        ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
        ; return (HsSumTy x tys', fvs) }
 
 -- Ensure that a type-level integer is nonnegative (#8306, #8412)
 rnHsTyKi env tyLit@(HsTyLit src t)
-  = do { data_kinds <- xoptM LangExt.DataKinds
-       ; unless data_kinds (addErr (dataKindsErr env tyLit))
+  = do { checkDataKinds env tyLit
        ; t' <- rnHsTyLit t
        ; return (HsTyLit src t', emptyFVs) }
 
@@ -675,16 +678,14 @@ rnHsTyKi env (XHsType ty)
             TcRnNotInScope (notInScopeErr WL_LocalOnly rdr_name) rdr_name [] []
 
 rnHsTyKi env ty@(HsExplicitListTy _ ip tys)
-  = do { data_kinds <- xoptM LangExt.DataKinds
-       ; unless data_kinds (addErr (dataKindsErr env ty))
+  = do { checkDataKinds env ty
        ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
        ; unless (isPromoted ip) $
            addDiagnostic (TcRnUntickedPromotedThing $ UntickedExplicitList)
        ; return (HsExplicitListTy noExtField ip tys', fvs) }
 
 rnHsTyKi env ty@(HsExplicitTupleTy _ tys)
-  = do { data_kinds <- xoptM LangExt.DataKinds
-       ; unless data_kinds (addErr (dataKindsErr env ty))
+  = do { checkDataKinds env ty
        ; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
        ; return (HsExplicitTupleTy noExtField tys', fvs) }
 
@@ -1631,11 +1632,16 @@ badKindSigErr doc (L loc ty)
     TcRnWithHsDocContext doc $
     TcRnKindSignaturesDisabled (Left ty)
 
-dataKindsErr :: RnTyKiEnv -> HsType GhcPs -> TcRnMessage
-dataKindsErr env thing
-  = TcRnDataKindsError type_or_Kind thing
+-- | Check for DataKinds violations in a type context, as well as \"obvious\"
+-- violations in kind contexts.
+-- See @Note [Checking for DataKinds]@ in "GHC.Tc.Validity" for more on this.
+checkDataKinds :: RnTyKiEnv -> HsType GhcPs -> TcM ()
+checkDataKinds env thing
+  = do data_kinds <- xoptM LangExt.DataKinds
+       unless data_kinds $
+         addErr $ TcRnDataKindsError type_or_kind $ Left thing
   where
-    type_or_Kind | isRnKindLevel env = KindLevel
+    type_or_kind | isRnKindLevel env = KindLevel
                  | otherwise         = TypeLevel
 
 warnUnusedForAll :: OutputableBndrFlag flag 'Renamed
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index d9519c18a99f5ed76e1e068ca83783b2d463d872..81b3b3b19ad29288f8a161a18d0f9441d989930c 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -79,6 +79,7 @@ import GHC.Types.Literal   ( inCharRange )
 import GHC.Types.GREInfo   ( ConInfo(..), conInfoFields )
 import GHC.Builtin.Types   ( nilDataCon )
 import GHC.Core.DataCon
+import GHC.Core.TyCon      ( isKindName )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad       ( when, ap, guard, unless )
@@ -1255,9 +1256,14 @@ rn_ty_pat_var lrdr@(L l rdr) = do
 -- For the difference between `rn_ty_pat` and `rnHsTyKi` see Note [CpsRn monad]
 -- and Note [Implicit and explicit type variable binders]
 rn_ty_pat :: HsType GhcPs -> TPRnM (HsType GhcRn)
-rn_ty_pat (HsTyVar an prom lrdr) = do
-  name <- rn_ty_pat_var lrdr
-  pure (HsTyVar an prom name)
+rn_ty_pat tv@(HsTyVar an prom lrdr) = do
+  lname@(L _ name) <- rn_ty_pat_var lrdr
+  when (isDataConName name && not (isKindName name)) $
+    -- Any use of a promoted data constructor name (that is not specifically
+    -- exempted by isKindName) is illegal without the use of DataKinds.
+    -- See Note [Checking for DataKinds] in GHC.Tc.Validity.
+    check_data_kinds tv
+  pure (HsTyVar an prom lname)
 
 rn_ty_pat (HsForAllTy an tele body) = liftTPRnRaw $ \ctxt locals thing_inside ->
   bindHsForAllTelescope ctxt tele $ \tele' -> do
@@ -1331,8 +1337,7 @@ rn_ty_pat (HsDocTy an ty haddock_doc) = do
   pure (HsDocTy an ty' haddock_doc')
 
 rn_ty_pat ty@(HsExplicitListTy _ prom tys) = do
-  data_kinds <- liftRn $ xoptM LangExt.DataKinds
-  unless data_kinds (liftRn $ addErr (TcRnDataKindsError TypeLevel ty))
+  check_data_kinds ty
 
   unless (isPromoted prom) $
     liftRn $ addDiagnostic (TcRnUntickedPromotedThing $ UntickedExplicitList)
@@ -1341,14 +1346,12 @@ rn_ty_pat ty@(HsExplicitListTy _ prom tys) = do
   pure (HsExplicitListTy noExtField prom tys')
 
 rn_ty_pat ty@(HsExplicitTupleTy _ tys) = do
-  data_kinds <- liftRn $ xoptM LangExt.DataKinds
-  unless data_kinds (liftRn $ addErr (TcRnDataKindsError TypeLevel ty))
+  check_data_kinds ty
   tys' <- mapM rn_lty_pat tys
   pure (HsExplicitTupleTy noExtField tys')
 
 rn_ty_pat tyLit@(HsTyLit src t) = do
-  data_kinds <- liftRn $ xoptM LangExt.DataKinds
-  unless data_kinds (liftRn $ addErr (TcRnDataKindsError TypeLevel tyLit))
+  check_data_kinds tyLit
   t' <- liftRn $ rnHsTyLit t
   pure (HsTyLit src t')
 
@@ -1405,6 +1408,11 @@ rn_ty_pat_arrow (HsLinearArrow (HsLolly arr)) = pure (HsLinearArrow (HsLolly arr
 rn_ty_pat_arrow (HsExplicitMult pct p arr)
   = rn_lty_pat p <&> (\mult -> HsExplicitMult pct mult arr)
 
+check_data_kinds :: HsType GhcPs -> TPRnM ()
+check_data_kinds thing = liftRn $ do
+  data_kinds <- xoptM LangExt.DataKinds
+  unless data_kinds $
+    addErr $ TcRnDataKindsError TypeLevel $ Left thing
 
 {- Note [Locally bound names in type patterns]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index c23c5e1ef91d1006a3b87020ba6de0e96719e641..74190ad02960e869c38bf53d0c5cf1e5f1d06cd9 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1025,7 +1025,6 @@ instance Diagnostic TcRnMessage where
                                        <+> quotes (pprTheta theta)
 
                      FamDataConPE   -> text "it comes from a data family instance"
-                     NoDataKindsDC  -> text "perhaps you intended to use DataKinds"
                      PatSynPE       -> text "pattern synonyms cannot be promoted"
                      RecDataConPE   -> same_rec_group_msg
                      ClassPE        -> same_rec_group_msg
@@ -1655,8 +1654,21 @@ instance Diagnostic TcRnMessage where
                 , inHsDocContext doc ]
 
     TcRnDataKindsError typeOrKind thing
-      -> mkSimpleDecorated $
-           text "Illegal" <+> (text $ levelString typeOrKind) <> colon <+> quotes (ppr thing)
+      -- See Note [Checking for DataKinds] (Wrinkle: Migration story for
+      -- DataKinds typechecker errors) in GHC.Tc.Validity for why we give
+      -- different diagnostic messages below.
+      -> case thing of
+           Left renamer_thing ->
+             mkSimpleDecorated $
+               text "Illegal" <+> ppr_level <> colon <+> quotes (ppr renamer_thing)
+           Right typechecker_thing ->
+             mkSimpleDecorated $ vcat
+               [ text "An occurrence of" <+> quotes (ppr typechecker_thing) <+>
+                 text "in a" <+> ppr_level <+> text "requires DataKinds."
+               , text "Future versions of GHC will turn this warning into an error."
+               ]
+      where
+        ppr_level = text $ levelString typeOrKind
 
     TcRnTypeSynonymCycle decl_or_tcs
       -> mkSimpleDecorated $
@@ -2401,8 +2413,17 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnUnusedQuantifiedTypeVar{}
       -> WarningWithFlag Opt_WarnUnusedForalls
-    TcRnDataKindsError{}
-      -> ErrorWithoutFlag
+    TcRnDataKindsError _ thing
+      -- DataKinds errors can arise from either the renamer (Left) or the
+      -- typechecker (Right). The latter category of DataKinds errors are a
+      -- fairly recent addition to GHC (introduced in GHC 9.10), and in order
+      -- to prevent these new errors from breaking users' code, we temporarily
+      -- downgrade these errors to warnings. See Note [Checking for DataKinds]
+      -- (Wrinkle: Migration story for DataKinds typechecker errors)
+      -- in GHC.Tc.Validity.
+      -> case thing of
+           Left  _ -> ErrorWithoutFlag
+           Right _ -> WarningWithFlag Opt_WarnDataKindsTC
     TcRnTypeSynonymCycle{}
       -> ErrorWithoutFlag
     TcRnZonkerMessage msg
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 9c1f8a2fb879a30cd92086f3d6e6f76a6b51b9c2..614e00a3b89ad2a9a4f87fc87f5a85d96846592d 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -2380,6 +2380,12 @@ data TcRnMessage where
       an illegal type or kind, probably required -XDataKinds
       and is used without the enabled extension.
 
+      This error can occur in both the renamer and the typechecker. The field
+      of type @'Either' ('HsType' 'GhcPs') 'Type'@ reflects this: this field
+      will contain a 'Left' value if the error occurred in the renamer, and this
+      field will contain a 'Right' value if the error occurred in the
+      typechecker.
+
       Examples:
 
         type Foo = [Nat, Char]
@@ -2387,11 +2393,24 @@ data TcRnMessage where
         type Bar = [Int, String]
 
       Test cases: linear/should_fail/T18888
+                  parser/should_fail/readFail001
                   polykinds/T7151
+                  polykinds/T7433
+                  rename/should_fail/T13568
+                  rename/should_fail/T22478e
                   th/TH_Promoted1Tuple
-                  typecheck/should_fail/tcfail094
-  -}
-  TcRnDataKindsError :: TypeOrKind -> HsType GhcPs -> TcRnMessage
+                  typecheck/should_compile/tcfail094
+                  typecheck/should_compile/T22141a
+                  typecheck/should_compile/T22141b
+                  typecheck/should_compile/T22141c
+                  typecheck/should_compile/T22141d
+                  typecheck/should_compile/T22141e
+                  typecheck/should_compile/T22141f
+                  typecheck/should_compile/T22141g
+                  typecheck/should_fail/T20873c
+                  typecheck/should_fail/T20873d
+  -}
+  TcRnDataKindsError :: TypeOrKind -> Either (HsType GhcPs) Type -> TcRnMessage
 
   {-| TcRnCannotBindScopedTyVarInPatSig is an error stating that scoped type
      variables cannot be used in pattern bindings.
diff --git a/compiler/GHC/Tc/Errors/Types/PromotionErr.hs b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
index 809b3898686aaab614ec9cb581dc45bfeb226c18..47e49a5933e43b375ecf312ecc77f78afc286290 100644
--- a/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
+++ b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
@@ -26,7 +26,6 @@ data PromotionErr
   | RecDataConPE     -- Data constructor in a recursive loop
                      -- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl
   | TermVariablePE   -- See Note [Promoted variables in types]
-  | NoDataKindsDC    -- -XDataKinds not enabled (for a datacon)
   | TypeVariablePE   -- See Note [Type variable scoping errors during typechecking]
   deriving (Generic)
 
@@ -37,7 +36,6 @@ instance Outputable PromotionErr where
   ppr FamDataConPE         = text "FamDataConPE"
   ppr (ConstrainedDataConPE theta) = text "ConstrainedDataConPE" <+> parens (ppr theta)
   ppr RecDataConPE         = text "RecDataConPE"
-  ppr NoDataKindsDC        = text "NoDataKindsDC"
   ppr TermVariablePE       = text "TermVariablePE"
   ppr TypeVariablePE       = text "TypeVariablePE"
 
@@ -51,7 +49,6 @@ peCategory PatSynPE             = "pattern synonym"
 peCategory FamDataConPE         = "data constructor"
 peCategory ConstrainedDataConPE{} = "data constructor"
 peCategory RecDataConPE         = "data constructor"
-peCategory NoDataKindsDC        = "data constructor"
 peCategory TermVariablePE       = "term variable"
 peCategory TypeVariablePE       = "type variable"
 
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 465a73f7e2181e327796fe36407f3b4ae64b5d75..6f1d9545d236b940d7f31bdb4672016c1a33479b 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1993,10 +1993,7 @@ tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
              -> return (mkTyConTy tc, tyConKind tc)
 
            AGlobal (AConLike (RealDataCon dc))
-             -> do { data_kinds <- xoptM LangExt.DataKinds
-                   ; unless (data_kinds || specialPromotedDc dc) $
-                       promotionErr name NoDataKindsDC
-                   ; when (isFamInstTyCon (dataConTyCon dc)) $
+             -> do { when (isFamInstTyCon (dataConTyCon dc)) $
                        -- see #15245
                        promotionErr name FamDataConPE
                    ; let (_, _, _, theta, _, _) = dataConFullSig dc
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 797ee56e61466384b88de6b17d8bbdcd9429a848..b66103af540bfd34da142a0cf36fa26a45c81ba2 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -60,7 +60,8 @@ import GHC.Driver.Session
 import qualified GHC.LanguageExtensions as LangExt
 
 import GHC.Types.Error
-import GHC.Types.Basic   ( UnboxedTupleOrSum(..), unboxedTupleOrSumExtension )
+import GHC.Types.Basic   ( TypeOrKind(..), UnboxedTupleOrSum(..)
+                         , unboxedTupleOrSumExtension )
 import GHC.Types.Name
 import GHC.Types.Var.Env
 import GHC.Types.Var.Set
@@ -779,9 +780,18 @@ check_type ve ty@(TyConApp tc tys)
   = check_ubx_tuple_or_sum UnboxedSumType   ve ty tys
 
   | otherwise
-  = mapM_ (check_arg_type False ve) tys
-
-check_type _ (LitTy {}) = return ()
+  = do { -- We require DataKinds to use a type constructor in a kind, unless it
+         -- is exempted (e.g., Type, TYPE, etc., which is checked by
+         -- isKindTyCon) or a `type data` type constructor.
+         -- See Note [Checking for DataKinds].
+         unless (isKindTyCon tc || isTypeDataTyCon tc) $
+         checkDataKinds ve ty
+       ; mapM_ (check_arg_type False ve) tys }
+
+check_type ve ty@(LitTy {}) =
+  -- Type-level literals are forbidden from appearing in kinds unless DataKinds
+  -- is enabled. See Note [Checking for DataKinds].
+  checkDataKinds ve ty
 
 check_type ve (CastTy ty _) = check_type ve ty
 
@@ -929,6 +939,10 @@ check_ubx_tuple_or_sum tup_or_sum (ve@ValidityEnv{ve_tidy_env = env}) ty tys
         ; checkTcM ub_thing_allowed
             (env, TcRnUnboxedTupleOrSumTypeFuncArg tup_or_sum (tidyType env ty))
 
+          -- Unboxed tuples and sums are forbidden from appearing in kinds
+          -- unless DataKinds is enabled. See Note [Checking for DataKinds].
+        ; checkDataKinds ve ty
+
         ; impred <- xoptM LangExt.ImpredicativeTypes
         ; let rank' = if impred then ArbitraryRank else MonoTypeTyConArg
                 -- c.f. check_arg_type
@@ -1004,6 +1018,22 @@ checkVdqOK ve tvbs ty = do
     no_vdq = all (isInvisibleForAllTyFlag . binderFlag) tvbs
     ValidityEnv{ve_tidy_env = env, ve_ctxt = ctxt} = ve
 
+-- | Check for a DataKinds violation in a kind context.
+-- See @Note [Checking for DataKinds]@.
+--
+-- Note that emitting DataKinds errors from the typechecker is a fairly recent
+-- addition to GHC (introduced in GHC 9.10), and in order to prevent these new
+-- errors from breaking users' code, we temporarily downgrade these errors to
+-- warnings. (This is why we use 'diagnosticTcM' below.) See
+-- @Note [Checking for DataKinds] (Wrinkle: Migration story for DataKinds
+-- typechecker errors)@.
+checkDataKinds :: ValidityEnv -> Type -> TcM ()
+checkDataKinds (ValidityEnv{ ve_ctxt = ctxt, ve_tidy_env = env }) ty = do
+  data_kinds <- xoptM LangExt.DataKinds
+  diagnosticTcM
+    (not (data_kinds || typeLevelUserTypeCtxt ctxt)) $
+    (env, TcRnDataKindsError KindLevel (Right (tidyType env ty)))
+
 {- Note [No constraints in kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 GHC does not allow constraints in kinds. Equality constraints
@@ -1077,6 +1107,104 @@ as the FunTy case must came after the rank-n case. Otherwise, something like
 (Eq a => Int) would be treated as a function type (FunTy), which just
 wouldn't do.
 
+Note [Checking for DataKinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Checking whether a piece of code requires -XDataKinds or not is surprisingly
+complicated, so here is a specification (adapted from #22141) for what
+-XDataKinds does and does not allow. First, some definitions:
+
+* A user-written type (i.e. part of the source text of a program) is in a
+  /kind context/ if it follows a `::` in:
+  * A standalone kind signature, e.g.,
+      type T :: Nat -> Type
+  * A kind signature in a type, e.g.:
+    - forall (a :: Nat -> Type). blah
+    - type F = G :: Nat -> Type
+    - etc.
+  * A result kind signature in a type declaration, e.g.:
+    - data T a :: Nat -> Type where ...
+    - type family Fam :: Nat -> Type
+    - etc.
+
+* All other contexts where types can appear are referred to as /type contexts/.
+
+* The /kind type constructors/ are (see GHC.Core.TyCon.isKindTyCon):
+  * TYPE and Type
+  * CONSTRAINT and Constraint
+  * LiftedRep
+  * RuntimeRep, Levity, and their data constructors
+  * Multiplicity and its data construtors
+  * VecCount, VecElem, and their data constructors
+
+* A `type data` type constructor is defined using the -XTypeData extension, such
+  as the T in `type data T = A | B`.
+
+* The following are rejected in type contexts unless -XDataKinds is enabled:
+  * Promoted data constructors (e.g., 'Just), except for those data constructors
+    listed under /kind type constructors/
+  * Promoted list or tuple syntax (e.g., '[Int, Bool] or '(Int, Bool))
+  * Type-level literals (e.g., 42, "hello", or 'a' at the type level)
+
+* The following are rejected in kind contexts unless -XDataKinds is enabled:
+  * Everything that is rejected in a type context.
+  * Any type constructor that is not a kind type constructor or a `type data`
+    type constructor (e.g., Maybe, [], Char, Nat, Symbol, etc.)
+
+    Note that this includes rejecting occurrences of non-kind type construtors
+    in type synomym (or type family) applications, even it the expansion would
+    be legal. For example:
+
+      type T a = Type
+      f :: forall (x :: T Int). blah
+
+    Here the `Int` in `T Int` is rejected even though the expansion is just
+    `Type`. This is consistent with, for example, rejecting `T (forall a. a->a)`
+    without -XImpredicativeTypes.
+
+    This check only occurs in kind contexts. It is always permissible to mention
+    type synonyms in a type context without enabling -XDataKinds, even if the
+    type synonym expands to something that would otherwise require -XDataKinds.
+
+Because checking for DataKinds in a kind context requires looking beneath type
+synonyms, it is natural to implement these checks in checkValidType, which has
+the necessary machinery to check for language extensions in the presence of
+type synonyms. For the exact same reason, checkValidType is *not* a good place
+to check for DataKinds in a type context, since we deliberately do not want to
+look beneath type synonyms there. As a result, we check for DataKinds in two
+different places in the code:
+
+* We check for DataKinds violations in kind contexts in the typechecker. See
+  checkDataKinds in this module.
+* We check for DataKinds violations in type contexts in the renamer. See
+  checkDataKinds in GHC.Rename.HsType and check_data_kinds in GHC.Rename.Pat.
+
+  Note that the renamer can also catch "obvious" kind-level violations such as
+  `data Dat :: Proxy 42 -> Type` (where 42 is not hidden beneath a type
+  synonym), so we also catch a subset of kind-level violations in the renamer
+  to allow for earlier reporting of these errors.
+
+-----
+-- Wrinkle: Migration story for DataKinds typechecker errors
+-----
+
+As mentioned above, DataKinds is checked in two different places: the renamer
+and the typechecker. The checks in the renamer have been around since DataKinds
+was introduced. The checks in the typechecker, on the other hand, are a fairly
+recent addition, having been introduced in GHC 9.10. As such, it is possible
+that there are some programs in the wild that (1) do not enable DataKinds, and
+(2) were accepted by a previous GHC version, but would now be rejected by the
+new DataKinds checks in the typechecker.
+
+To prevent the new DataKinds checks in the typechecker from breaking users'
+code, we temporarily allow programs to compile if they violate a DataKinds
+check in the typechecker, but GHC will emit a warning if such a violation
+occurs. Users can then silence the warning by enabling DataKinds in the module
+where the affected code lives. It is fairly straightforward to distinguish
+between DataKinds violations arising from the renamer versus the typechecker,
+as TcRnDataKindsError (the error message type classifying all DataKinds errors)
+stores an Either field that is Left when the error comes from the renamer and
+Right when the error comes from the typechecker.
+
 ************************************************************************
 *                                                                      *
 \subsection{Checking a theta or source type}
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index 990e268f19b19322dd2d350987ea33c8e664d81b..9905ec5a1be3fdd93197df4b7009a4b2e3b63203 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -869,7 +869,6 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "FamDataConPE"                                  = 64578
   GhcDiagnosticCode "ConstrainedDataConPE"                          = 28374
   GhcDiagnosticCode "RecDataConPE"                                  = 56753
-  GhcDiagnosticCode "NoDataKindsDC"                                 = 71015
   GhcDiagnosticCode "TermVariablePE"                                = 45510
   GhcDiagnosticCode "TypeVariablePE"                                = 47557
 
diff --git a/docs/users_guide/9.10.1-notes.rst b/docs/users_guide/9.10.1-notes.rst
index 77d51e173e5ddcb2a51a939166e3a6f96e7b2c4f..804609f3f63d66908b428f501a844c771448903a 100644
--- a/docs/users_guide/9.10.1-notes.rst
+++ b/docs/users_guide/9.10.1-notes.rst
@@ -18,6 +18,25 @@ Language
 
   This feature is guarded behind :extension:`RequiredTypeArguments` and :extension:`ExplicitNamespaces`.
 
+- Due to an oversight, previous GHC releases (starting from 9.4) allowed the use
+  of promoted data types in kinds, even when :extension:`DataKinds` was not
+  enabled. That is, GHC would erroneously accept the following code: ::
+
+    {-# LANGUAGE NoDataKinds #-}
+
+    import Data.Kind (Type)
+    import GHC.TypeNats (Nat)
+
+    -- Nat shouldn't be allowed here without DataKinds
+    data Vec :: Nat -> Type -> Type
+
+  This oversight has now been fixed. If you wrote code that took advantage of
+  this oversight, you may need to enable :extension:`DataKinds` in your code to
+  allow it to compile with GHC 9.10.
+
+  For more information on what types are allowed in kinds, see the
+  :ref:`promotion` section.
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/data_kinds.rst b/docs/users_guide/exts/data_kinds.rst
index 8194e1f7aeb826937d59d0303f4be9ea4b0bc78b..49e248a64552bae2d3bb4752683851f6cd67e2cb 100644
--- a/docs/users_guide/exts/data_kinds.rst
+++ b/docs/users_guide/exts/data_kinds.rst
@@ -96,6 +96,23 @@ There are only a couple of exceptions to this rule:
      data Foo :: Type -> Type where
        MkFoo :: Show a => Foo a    -- not promotable
 
+The following kinds and promoted data constructors can be used even when
+:extension:`DataKinds` is not enabled:
+
+- ``Type``
+- ``TYPE`` (see :ref:`_runtime-rep`)
+- ``Constraint`` (see :ref:`constraint-kind`)
+- ``CONSTRAINT``
+- ``Multiplicity`` and its promoted data constructors (see :extension:`LinearTypes`)
+- ``LiftedRep`` (see :ref:`_runtime-rep`)
+- ``RuntimeRep`` and its promoted data constructors (see :ref:`_runtime-rep`)
+- ``Levity`` and its promoted data constructors (see :ref:`_runtime-rep`)
+- ``VecCount`` and its promoted data constructors
+- ``VecElem`` and its promoted data constructors
+
+It is also possible to use kinds declared with ``type data`` (see
+:extension:`TypeData`) without enabling :extension:`DataKinds`.
+
 .. _promotion-syntax:
 
 Distinguishing between types and constructors
@@ -208,3 +225,71 @@ parameter to ``UnEx``, the kind is not escaping the existential, and the
 above code is valid.
 
 See also :ghc-ticket:`7347`.
+
+.. _promotion-type-synonyms:
+
+:extension:`DataKinds` and type synonyms
+----------------------------------------
+
+The :extensions:`DataKinds` extension interacts with type synonyms in the
+following ways:
+
+1. In a *type* context: :extension:`DataKinds` is not required to use a type
+   synonym that expands to a type that would otherwise require the extension.
+   For example: ::
+
+     {-# LANGUAGE DataKinds #-}
+     module A where
+
+       type MyTrue = 'True
+
+     {-# LANGUAGE NoDataKinds #-}
+     module B where
+
+       import A
+       import Data.Proxy
+
+       f :: Proxy MyTrue
+       f = Proxy
+
+   GHC will accept the type signature for ``f`` even though
+   :extension:`DataKinds` is not enabled, as the promoted data constructor
+   ``True`` is tucked underneath the ``MyTrue`` type synonym. If the user
+   had written ``Proxy 'True`` directly, however, then :extension:`DataKinds`
+   would be required.
+
+2. In a *kind* context: :extension:`DataKinds` applies to all types mentioned
+   in the kind, *including the expansions of type synonyms*. For instance,
+   given this module: ::
+
+     module C where
+
+       type MyType = Type
+       type MySymbol = Symbol
+
+   We would accept or reject the following definitions in this module, which
+   makes use of :ref:`standalone-kind-signatures`: ::
+
+     {-# LANGUAGE NoDataKinds #-}
+     module D where
+
+       import C
+
+       -- ACCEPTED: The kind only mentions Type, which doesn't require DataKinds
+       type D1 :: Type -> Type
+       data D1 a
+
+       -- REJECTED: The kind mentions Symbol, which requires DataKinds to use in
+       -- a kind position
+       data D2 :: Symbol -> Type
+       data D2 a
+
+       -- ACCEPTED: The kind mentions a type synonym MyType that expands to
+       -- Type, which doesn't require DataKinds
+       data D3 :: MyType -> Type
+       data D3 a
+
+       -- REJECTED: The kind mentions a type synonym MySymbol that expands to
+       -- Symbol, which requires DataKinds to use in a kind position
+       data D4 :: MySymbol -> Type
+       data D4 a
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index 839140bcd65c15c5f0a45b0c8ee2798348cd5909..84dcd6721c54132d16df557abb7d6d8bfcac6858 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -2566,6 +2566,26 @@ of ``-W(no-)*``.
     issued. Another example is :ghc-flag:`-dynamic` is ignored when :ghc-flag:`-dynamic-too`
     is passed.
 
+.. ghc-flag:: -Wdata-kinds-tc
+    :shortdesc: warn when an illegal use of a type or kind without
+                :extension:`DataKinds` is caught by the typechecker
+    :type: dynamic
+    :reverse: -Wno-data-kinds-tc
+
+    :since: 9.10.1
+
+    Introduced in GHC 9.10.1, this warns when an illegal use of a type or kind
+    (without having enabled the :extension:`DataKinds` extension) is caught in
+    the typechecker (hence the ``-tc`` suffix). These warnings complement the
+    existing :extensions:`DataKinds` checks (that have existed since
+    :extension:`DataKinds` was first introduced), which result in errors
+    instead of warnings.
+
+    This warning is scheduled to be changed to an error in a future GHC
+    version, at which point the :ghc-flag:`-Wdata-kinds-tc` flag will be
+    removed. Users can enable the :extension:`DataKinds` extension to avoid
+    issues (thus silencing the warning).
+
 If you're feeling really paranoid, the :ghc-flag:`-dcore-lint` option is a good choice.
 It turns on heavyweight intra-pass sanity-checking within GHC. (It checks GHC's
 sanity, not yours.)
diff --git a/testsuite/tests/polykinds/T7433.stderr b/testsuite/tests/polykinds/T7433.stderr
index b1f4d52a9ba9be82ec02ae3e32051218ec1edb57..347d510adac46ebac3340c7cd20009b98208227f 100644
--- a/testsuite/tests/polykinds/T7433.stderr
+++ b/testsuite/tests/polykinds/T7433.stderr
@@ -1,6 +1,4 @@
 
-T7433.hs:2:10: error: [GHC-71015]
-    • Data constructor ‘Z’ cannot be used here
-        (perhaps you intended to use DataKinds)
-    • In the type ‘'Z’
-      In the type declaration for ‘T’
+T7433.hs:2:10: error: [GHC-68567]
+    Illegal type: ‘'Z’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/rename/should_fail/T22478e.hs b/testsuite/tests/rename/should_fail/T22478e.hs
index 0d90014b5b693ee00afb06bc93ce48331dd75b58..10c621ddd16028399b60da1b0b130c78505c6003 100644
--- a/testsuite/tests/rename/should_fail/T22478e.hs
+++ b/testsuite/tests/rename/should_fail/T22478e.hs
@@ -10,3 +10,4 @@ j (P @(t :: k)) = ()
 k (P @('(a,b))) = ()
 l (P @"str")    = ()
 d (P @'c')      = ()
+e (P @'True)    = ()
diff --git a/testsuite/tests/rename/should_fail/T22478e.stderr b/testsuite/tests/rename/should_fail/T22478e.stderr
index 2a2c79d719ff58df526ef452d1a3fd41532b53a4..dbd2a9845fce17b4bee27bd711d3c4b3ea561b2e 100644
--- a/testsuite/tests/rename/should_fail/T22478e.stderr
+++ b/testsuite/tests/rename/should_fail/T22478e.stderr
@@ -55,3 +55,11 @@ T22478e.hs:12:4: error: [GHC-68567]
 T22478e.hs:12:4: error: [GHC-17916]
     Illegal visible type application in a pattern: @'c'
     Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T22478e.hs:13:4: error: [GHC-68567]
+    Illegal type: ‘'True’
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22478e.hs:13:4: error: [GHC-17916]
+    Illegal visible type application in a pattern: @'True
+    Suggested fix: Perhaps you intended to use TypeAbstractions
diff --git a/testsuite/tests/typecheck/should_compile/T22141a.hs b/testsuite/tests/typecheck/should_compile/T22141a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..5c1f43a42bdb3711c1c3a232a419252e4aaaa51f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141a.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE NoDataKinds #-}
+module T22141a where
+
+import GHC.TypeLits (Nat)
+import Data.Kind (Type)
+
+data Vector :: Nat -> Type -> Type where
diff --git a/testsuite/tests/typecheck/should_compile/T22141a.stderr b/testsuite/tests/typecheck/should_compile/T22141a.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..8c26dea1d10ecb9af0fe81633124884ef16aa1ad
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141a.stderr
@@ -0,0 +1,7 @@
+
+T22141a.hs:8:1: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘GHC.Num.Natural.Natural’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In the expansion of type synonym ‘Nat’
+      In the data type declaration for ‘Vector’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_compile/T22141b.hs b/testsuite/tests/typecheck/should_compile/T22141b.hs
new file mode 100644
index 0000000000000000000000000000000000000000..199885c6d7a13379295b84cd98a8ba271ebedf04
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE NoDataKinds #-}
+module T22141b where
+
+import GHC.TypeLits (Nat)
+import Data.Kind (Type)
+
+type MyNat = Nat
+
+data Vector :: MyNat -> Type -> Type
diff --git a/testsuite/tests/typecheck/should_compile/T22141b.stderr b/testsuite/tests/typecheck/should_compile/T22141b.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..f3d2471bbaf903851d32ab39687fa5c57143e89e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141b.stderr
@@ -0,0 +1,8 @@
+
+T22141b.hs:10:1: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘GHC.Num.Natural.Natural’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In the expansion of type synonym ‘Nat’
+      In the expansion of type synonym ‘MyNat’
+      In the data type declaration for ‘Vector’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_compile/T22141c.hs b/testsuite/tests/typecheck/should_compile/T22141c.hs
new file mode 100644
index 0000000000000000000000000000000000000000..40168014d8fb1451db5dff8c8bea2c38f083bed5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141c.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE NoDataKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+module T22141c where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy)
+
+type T = (# Type, Type #)
+
+type D :: Proxy T -> Type
+data D a
diff --git a/testsuite/tests/typecheck/should_compile/T22141c.stderr b/testsuite/tests/typecheck/should_compile/T22141c.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..e82c57fd3ef7effe5b3c0877386f798c2acff551
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141c.stderr
@@ -0,0 +1,32 @@
+
+T22141c.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘(# *, * #)’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In the expansion of type synonym ‘T’
+      In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141c.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘'[]’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141c.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘'[GHC.Types.LiftedRep]’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141c.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘[GHC.Types.LiftedRep,
+                         GHC.Types.LiftedRep]’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141c.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘Proxy T’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_compile/T22141d.hs b/testsuite/tests/typecheck/should_compile/T22141d.hs
new file mode 100644
index 0000000000000000000000000000000000000000..994fdfcb863c9e2c3a722e2b411645bccbd82944
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141d.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE NoDataKinds #-}
+{-# LANGUAGE UnboxedSums #-}
+module T22141d where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy)
+
+type T = (# Type | Type #)
+
+type D :: Proxy T -> Type
+data D a
diff --git a/testsuite/tests/typecheck/should_compile/T22141d.stderr b/testsuite/tests/typecheck/should_compile/T22141d.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..d3f57e4304be8f6456288fc3a37f79797d522160
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141d.stderr
@@ -0,0 +1,32 @@
+
+T22141d.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘(# * | * #)’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In the expansion of type synonym ‘T’
+      In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141d.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘'[]’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141d.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘'[GHC.Types.LiftedRep]’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141d.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘[GHC.Types.LiftedRep,
+                         GHC.Types.LiftedRep]’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141d.hs:10:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘Proxy T’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_compile/T22141e.hs b/testsuite/tests/typecheck/should_compile/T22141e.hs
new file mode 100644
index 0000000000000000000000000000000000000000..1f4f4b182b9e8527d6d1b73a065c32e8e07d1fa2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141e.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE NoDataKinds #-}
+module T22141e where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy)
+import T22141e_Aux
+
+type D :: Proxy T -> Type
+data D a
diff --git a/testsuite/tests/typecheck/should_compile/T22141e.stderr b/testsuite/tests/typecheck/should_compile/T22141e.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..94b1ccc126c1ce3df0d18db8bb93fac404f72285
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141e.stderr
@@ -0,0 +1,19 @@
+
+T22141e.hs:8:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘42’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In the expansion of type synonym ‘T’
+      In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141e.hs:8:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘GHC.Num.Natural.Natural’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22141e.hs:8:11: warning: [GHC-68567] [-Wdata-kinds-tc (in -Wdefault)]
+    • An occurrence of ‘Proxy T’ in a kind requires DataKinds.
+      Future versions of GHC will turn this warning into an error.
+    • In a standalone kind signature for ‘D’: Proxy T -> Type
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_compile/T22141e_Aux.hs b/testsuite/tests/typecheck/should_compile/T22141e_Aux.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a8f6d9f711873199f0e32dadb94fd969d0e1d7ab
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141e_Aux.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE DataKinds #-}
+module T22141e_Aux where
+
+type T = 42
diff --git a/testsuite/tests/typecheck/should_compile/T22141f.hs b/testsuite/tests/typecheck/should_compile/T22141f.hs
new file mode 100644
index 0000000000000000000000000000000000000000..2a976f31035a59030bd3705d8837c09e1046c358
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141f.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE NoDataKinds #-}
+{-# LANGUAGE LinearTypes #-}
+module T22141f where
+
+import Data.Kind (Constraint, Type)
+import GHC.Exts ( CONSTRAINT, Levity(..), LiftedRep, Multiplicity(..)
+                , RuntimeRep(..), TYPE, VecCount(..), VecElem(..) )
+
+-- All of the following should be accepted without DataKinds.
+
+type A :: Type
+data A
+
+type B :: TYPE LiftedRep
+data B
+
+type C :: Type -> Constraint
+class C a
+
+type D :: TYPE LiftedRep -> CONSTRAINT LiftedRep
+class D a
+
+type E :: Multiplicity -> Type
+data E a
+
+type E1 = Int %'One  -> Int
+type E2 = Int %'Many -> Int
+
+type F1      = TYPE 'IntRep
+type F2      = TYPE 'Int8Rep
+type F3      = TYPE 'Int16Rep
+type F4      = TYPE 'Int32Rep
+type F5      = TYPE 'Int64Rep
+type F6      = TYPE 'WordRep
+type F7      = TYPE 'Word8Rep
+type F8      = TYPE 'Word16Rep
+type F9      = TYPE 'Word32Rep
+type F10     = TYPE 'Word64Rep
+type F11     = TYPE 'AddrRep
+type F12     = TYPE 'FloatRep
+type F13     = TYPE 'DoubleRep
+type F14 x   = TYPE ('TupleRep x)
+type F15 x   = TYPE ('SumRep x)
+type F16 x y = TYPE ('VecRep x y)
+type F17 x   = TYPE ('BoxedRep x)
+
+type G :: Levity -> Type
+data G a
+
+type G1 = 'BoxedRep 'Lifted
+type G2 = 'BoxedRep 'Unlifted
+
+type H :: VecCount -> Type
+data H a
+
+type H1 x = 'VecRep 'Vec2 x
+type H2 x = 'VecRep 'Vec4 x
+type H3 x = 'VecRep 'Vec8 x
+type H4 x = 'VecRep 'Vec16 x
+type H5 x = 'VecRep 'Vec32 x
+type H6 x = 'VecRep 'Vec64 x
+
+type I :: VecElem -> Type
+data I a
+
+type I1  x = 'VecRep x 'Int8ElemRep
+type I2  x = 'VecRep x 'Int16ElemRep
+type I3  x = 'VecRep x 'Int32ElemRep
+type I4  x = 'VecRep x 'Int64ElemRep
+type I5  x = 'VecRep x 'Word8ElemRep
+type I6  x = 'VecRep x 'Word16ElemRep
+type I7  x = 'VecRep x 'Word32ElemRep
+type I8  x = 'VecRep x 'Word64ElemRep
+type I9  x = 'VecRep x 'FloatElemRep
+type I10 x = 'VecRep x 'DoubleElemRep
diff --git a/testsuite/tests/typecheck/should_compile/T22141g.hs b/testsuite/tests/typecheck/should_compile/T22141g.hs
new file mode 100644
index 0000000000000000000000000000000000000000..693d7de44d0e0b42c40bd4d03ea10bd735c3397e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22141g.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE NoDataKinds #-}
+{-# LANGUAGE TypeData #-}
+module T22141g where
+
+import Data.Kind (Type)
+
+-- `type data` type constructors should be able to be used without DataKinds.
+
+type data Letter = A | B | C
+
+type F :: Letter -> Type
+data F l
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index e5f5c0ec86767ed18773444cc9bf4b1b19f13fa0..5e13e55a84fde15b23ef24a2808298d1a7be4b78 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -851,6 +851,13 @@ test('T21765', normal, compile, [''])
 test('T21951a', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21550', normal, compile, [''])
+test('T22141a', normal, compile, [''])
+test('T22141b', normal, compile, [''])
+test('T22141c', normal, compile, [''])
+test('T22141d', normal, compile, [''])
+test('T22141e', [extra_files(['T22141e_Aux.hs'])], multimod_compile, ['T22141e.hs', '-v0'])
+test('T22141f', normal, compile, [''])
+test('T22141g', normal, compile, [''])
 test('T22310', normal, compile, [''])
 test('T22331', normal, compile, [''])
 test('T22516', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T20873d.hs b/testsuite/tests/typecheck/should_fail/T20873d.hs
new file mode 100644
index 0000000000000000000000000000000000000000..862fe3b9828f29fbdf56bdaf0abbb5221fd271e4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20873d.hs
@@ -0,0 +1,11 @@
+
+{-# LANGUAGE GADTSyntax, NoKindSignatures, NoDataKinds #-}
+
+module T20873d where
+
+import Data.Kind ( Type )
+
+type U a = Type
+
+data Foo :: U Type where
+  MkFoo :: Foo
diff --git a/testsuite/tests/typecheck/should_fail/T20873d.stderr b/testsuite/tests/typecheck/should_fail/T20873d.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..8511e460712785de63af8562501492e8630c1842
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20873d.stderr
@@ -0,0 +1,5 @@
+
+T20873d.hs:10:1: error: [GHC-49378]
+    • Illegal kind signature ‘Foo :: U Type’
+    • In the data declaration for ‘Foo’
+    Suggested fix: Perhaps you intended to use KindSignatures
diff --git a/testsuite/tests/typecheck/should_fail/T22141a.stderr b/testsuite/tests/typecheck/should_fail/T22141a.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..719e678e645af6ee02d03a48bdda0fa927d91028
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22141a.stderr
@@ -0,0 +1,6 @@
+
+T22141a.hs:8:1: error: [GHC-68567]
+    • Illegal kind: ‘GHC.Num.Natural.Natural’
+    • In the expansion of type synonym ‘Nat’
+      In the data type declaration for ‘Vector’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_fail/T22141b.stderr b/testsuite/tests/typecheck/should_fail/T22141b.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..74f8670a1401e93d06f28e0fbed5a78c4be68f64
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22141b.stderr
@@ -0,0 +1,7 @@
+
+T22141b.hs:10:1: error: [GHC-68567]
+    • Illegal kind: ‘GHC.Num.Natural.Natural’
+    • In the expansion of type synonym ‘Nat’
+      In the expansion of type synonym ‘MyNat’
+      In the data type declaration for ‘Vector’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_fail/T22141c.stderr b/testsuite/tests/typecheck/should_fail/T22141c.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..3dcc2941617079a12fba9702789d308cd4556bf2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22141c.stderr
@@ -0,0 +1,4 @@
+
+T22141c.hs:8:17: error: [GHC-68567]
+    Illegal kind: ‘(# Type, Type #)’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_fail/T22141d.stderr b/testsuite/tests/typecheck/should_fail/T22141d.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..f9e1206c215b2e50b7707dc6e36ca57d2af62630
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22141d.stderr
@@ -0,0 +1,4 @@
+
+T22141d.hs:8:17: error: [GHC-68567]
+    Illegal kind: ‘(# Type | Type #)’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_fail/T22141e.stderr b/testsuite/tests/typecheck/should_fail/T22141e.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..8311a08ab46dc956cc126ed7f6204c57db6a34be
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22141e.stderr
@@ -0,0 +1,4 @@
+
+T22141e.hs:7:17: error: [GHC-68567]
+    Illegal kind: ‘42’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 7db8f53be6e38eae994f09108d1038ff6101e8ef..852e23ba43c36745f9b9b6ae989550d83476b55c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -647,6 +647,7 @@ test('T20588', [extra_files(['T20588.hs', 'T20588.hs-boot', 'T20588_aux.hs'])],
 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, [''])
+test('T20873d', normal, compile_fail, [''])
 test('FunDepOrigin1b', normal, compile_fail, [''])
 test('FD1', normal, compile_fail, [''])
 test('FD2', normal, compile_fail, [''])