From 9f9c92272b3ca11d54331cea83ad5e82e17fa062 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Fri, 22 Sep 2023 06:42:54 -0400
Subject: [PATCH] More robust checking for DataKinds
As observed in #22141, GHC was not doing its due diligence in catching code
that should require `DataKinds` in order to use. Most notably, it was allowing
the use of arbitrary data types in kind contexts without `DataKinds`, e.g.,
```hs
data Vector :: Nat -> Type -> Type where
```
This patch revamps how GHC tracks `DataKinds`. The full specification is
written out in the `DataKinds` section of the GHC User's Guide, and the
implementation thereof is described in `Note [Checking for DataKinds]` in
`GHC.Tc.Validity`. In brief:
* We catch _type_-level `DataKinds` violations in the renamer. See
`checkDataKinds` in `GHC.Rename.HsType` and `check_data_kinds` in
`GHC.Rename.Pat`.
* We catch _kind_-level `DataKinds` violations in the typechecker, as this
allows us to catch things that appear beneath type synonyms. (We do *not*
want to do this in type-level contexts, as it is perfectly fine for a type
synonym to mention something that requires DataKinds while still using the
type synonym in a module that doesn't enable DataKinds.) See `checkValidType`
in `GHC.Tc.Validity`.
* There is now a single `TcRnDataKindsError` that classifies all manner of
`DataKinds` violations, both in the renamer and the typechecker. The
`NoDataKindsDC` error has been removed, as it has been subsumed by
`TcRnDataKindsError`.
* I have added `CONSTRAINT` is `isKindTyCon`, which is what checks for illicit
uses of data types at the kind level without `DataKinds`. Previously,
`isKindTyCon` checked for `Constraint` but not `CONSTRAINT`. This is
inconsistent, given that both `Type` and `TYPE` were checked by `isKindTyCon`.
Moreover, it thwarted the implementation of the `DataKinds` check in
`checkValidType`, since we would expand `Constraint` (which was OK without
`DataKinds`) to `CONSTRAINT` (which was _not_ OK without `DataKinds`) and
reject it. Now both are allowed.
* I have added a flurry of additional test cases that test various corners of
`DataKinds` checking.
Fixes #22141.
---
compiler/GHC/Core/TyCon.hs | 26 +++-
compiler/GHC/Driver/Flags.hs | 5 +-
compiler/GHC/Driver/Session.hs | 1 +
compiler/GHC/Rename/HsType.hs | 46 +++---
compiler/GHC/Rename/Pat.hs | 26 ++--
compiler/GHC/Tc/Errors/Ppr.hs | 31 +++-
compiler/GHC/Tc/Errors/Types.hs | 25 +++-
compiler/GHC/Tc/Errors/Types/PromotionErr.hs | 3 -
compiler/GHC/Tc/Gen/HsType.hs | 5 +-
compiler/GHC/Tc/Validity.hs | 136 +++++++++++++++++-
compiler/GHC/Types/Error/Codes.hs | 1 -
docs/users_guide/9.10.1-notes.rst | 19 +++
docs/users_guide/exts/data_kinds.rst | 85 +++++++++++
docs/users_guide/using-warnings.rst | 20 +++
testsuite/tests/polykinds/T7433.stderr | 8 +-
testsuite/tests/rename/should_fail/T22478e.hs | 1 +
.../tests/rename/should_fail/T22478e.stderr | 8 ++
.../tests/typecheck/should_compile/T22141a.hs | 8 ++
.../typecheck/should_compile/T22141a.stderr | 7 +
.../tests/typecheck/should_compile/T22141b.hs | 10 ++
.../typecheck/should_compile/T22141b.stderr | 8 ++
.../tests/typecheck/should_compile/T22141c.hs | 11 ++
.../typecheck/should_compile/T22141c.stderr | 32 +++++
.../tests/typecheck/should_compile/T22141d.hs | 11 ++
.../typecheck/should_compile/T22141d.stderr | 32 +++++
.../tests/typecheck/should_compile/T22141e.hs | 9 ++
.../typecheck/should_compile/T22141e.stderr | 19 +++
.../typecheck/should_compile/T22141e_Aux.hs | 4 +
.../tests/typecheck/should_compile/T22141f.hs | 75 ++++++++++
.../tests/typecheck/should_compile/T22141g.hs | 12 ++
.../tests/typecheck/should_compile/all.T | 7 +
.../tests/typecheck/should_fail/T20873d.hs | 11 ++
.../typecheck/should_fail/T20873d.stderr | 5 +
.../typecheck/should_fail/T22141a.stderr | 6 +
.../typecheck/should_fail/T22141b.stderr | 7 +
.../typecheck/should_fail/T22141c.stderr | 4 +
.../typecheck/should_fail/T22141d.stderr | 4 +
.../typecheck/should_fail/T22141e.stderr | 4 +
testsuite/tests/typecheck/should_fail/all.T | 1 +
39 files changed, 673 insertions(+), 60 deletions(-)
create mode 100644 testsuite/tests/typecheck/should_compile/T22141a.hs
create mode 100644 testsuite/tests/typecheck/should_compile/T22141a.stderr
create mode 100644 testsuite/tests/typecheck/should_compile/T22141b.hs
create mode 100644 testsuite/tests/typecheck/should_compile/T22141b.stderr
create mode 100644 testsuite/tests/typecheck/should_compile/T22141c.hs
create mode 100644 testsuite/tests/typecheck/should_compile/T22141c.stderr
create mode 100644 testsuite/tests/typecheck/should_compile/T22141d.hs
create mode 100644 testsuite/tests/typecheck/should_compile/T22141d.stderr
create mode 100644 testsuite/tests/typecheck/should_compile/T22141e.hs
create mode 100644 testsuite/tests/typecheck/should_compile/T22141e.stderr
create mode 100644 testsuite/tests/typecheck/should_compile/T22141e_Aux.hs
create mode 100644 testsuite/tests/typecheck/should_compile/T22141f.hs
create mode 100644 testsuite/tests/typecheck/should_compile/T22141g.hs
create mode 100644 testsuite/tests/typecheck/should_fail/T20873d.hs
create mode 100644 testsuite/tests/typecheck/should_fail/T20873d.stderr
create mode 100644 testsuite/tests/typecheck/should_fail/T22141a.stderr
create mode 100644 testsuite/tests/typecheck/should_fail/T22141b.stderr
create mode 100644 testsuite/tests/typecheck/should_fail/T22141c.stderr
create mode 100644 testsuite/tests/typecheck/should_fail/T22141d.stderr
create mode 100644 testsuite/tests/typecheck/should_fail/T22141e.stderr
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index fd4d0350c4b3..c191f98244b0 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 d078255b4494..577b015d6148 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 d4cae2610166..800bd321a15a 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 6cf5387bddb0..e380b86f5ace 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 d9519c18a99f..81b3b3b19ad2 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 c23c5e1ef91d..74190ad02960 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 9c1f8a2fb879..614e00a3b89a 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 809b3898686a..47e49a5933e4 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 465a73f7e218..6f1d9545d236 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 797ee56e6146..b66103af540b 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 990e268f19b1..9905ec5a1be3 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 77d51e173e5d..804609f3f63d 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 8194e1f7aeb8..49e248a64552 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 839140bcd65c..84dcd6721c54 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 b1f4d52a9ba9..347d510adac4 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 0d90014b5b69..10c621ddd160 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 2a2c79d719ff..dbd2a9845fce 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 000000000000..5c1f43a42bdb
--- /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 000000000000..8c26dea1d10e
--- /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 000000000000..199885c6d7a1
--- /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 000000000000..f3d2471bbaf9
--- /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 000000000000..40168014d8fb
--- /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 000000000000..e82c57fd3ef7
--- /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 000000000000..994fdfcb863c
--- /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 000000000000..d3f57e4304be
--- /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 000000000000..1f4f4b182b9e
--- /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 000000000000..94b1ccc126c1
--- /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 000000000000..a8f6d9f71187
--- /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 000000000000..2a976f31035a
--- /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 000000000000..693d7de44d0e
--- /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 e5f5c0ec8676..5e13e55a84fd 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 000000000000..862fe3b9828f
--- /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 000000000000..8511e4607127
--- /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 000000000000..719e678e645a
--- /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 000000000000..74f8670a1401
--- /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 000000000000..3dcc29416170
--- /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 000000000000..f9e1206c215b
--- /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 000000000000..8311a08ab46d
--- /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 7db8f53be6e3..852e23ba43c3 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, [''])
--
GitLab