Skip to content
Snippets Groups Projects
Commit 9f9c9227 authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot
Browse files

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.
parent 5b0392e0
No related branches found
No related tags found
No related merge requests found
Showing
with 411 additions and 60 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment