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
DataKindsviolations in the renamer. SeecheckDataKindsinGHC.Rename.HsTypeandcheck_data_kindsinGHC.Rename.Pat. -
We catch kind-level
DataKindsviolations 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.) SeecheckValidTypeinGHC.Tc.Validity. -
There is now a single
TcRnDataKindsErrorthat classifies all manner ofDataKindsviolations, both in the renamer and the typechecker. TheNoDataKindsDCerror has been removed, as it has been subsumed byTcRnDataKindsError. -
I have added
CONSTRAINTisisKindTyCon, which is what checks for illicit uses of data types at the kind level withoutDataKinds. Previously,isKindTyConchecked forConstraintbut notCONSTRAINT. This is inconsistent, given that bothTypeandTYPEwere checked byisKindTyCon. Moreover, it thwarted the implementation of theDataKindscheck 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
DataKindschecking.
Fixes #22141 (closed).