More robust checking for DataKinds
As observed in #22141 (closed), 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.,
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. SeecheckDataKinds
inGHC.Rename.HsType
andcheck_data_kinds
inGHC.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.) SeecheckValidType
inGHC.Tc.Validity
. -
There is now a single
TcRnDataKindsError
that classifies all manner ofDataKinds
violations, both in the renamer and the typechecker. TheNoDataKindsDC
error has been removed, as it has been subsumed byTcRnDataKindsError
. -
I have added
CONSTRAINT
isisKindTyCon
, which is what checks for illicit uses of data types at the kind level withoutDataKinds
. Previously,isKindTyCon
checked forConstraint
but notCONSTRAINT
. This is inconsistent, given that bothType
andTYPE
were checked byisKindTyCon
. Moreover, it thwarted the implementation of theDataKinds
check incheckValidType
, since we would expandConstraint
(which was OK withoutDataKinds
) toCONSTRAINT
(which was not OK withoutDataKinds
) 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 (closed).