Skip to content

More robust checking for DataKinds

Ryan Scott requested to merge wip/T22141 into master

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. 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 (closed).

Merge request reports