[Git][ghc/ghc][master] More robust checking for DataKinds

[Marge Bot (@marge-bot)]

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
9f9c9227 by Ryan Scott at 2023-11-01T09:19:12-04:00
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.

- - - - -


30 changed files:

- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Driver/Flags.hs
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Rename/Pat.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Errors/Types/PromotionErr.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Validity.hs
- compiler/GHC/Types/Error/Codes.hs
- docs/users_guide/9.10.1-notes.rst
- docs/users_guide/exts/data_kinds.rst
- docs/users_guide/using-warnings.rst
- testsuite/tests/polykinds/T7433.stderr
- testsuite/tests/rename/should_fail/T22478e.hs
- testsuite/tests/rename/should_fail/T22478e.stderr
- + testsuite/tests/typecheck/should_compile/T22141a.hs
- + testsuite/tests/typecheck/should_compile/T22141a.stderr
- + testsuite/tests/typecheck/should_compile/T22141b.hs
- + testsuite/tests/typecheck/should_compile/T22141b.stderr
- + testsuite/tests/typecheck/should_compile/T22141c.hs
- + testsuite/tests/typecheck/should_compile/T22141c.stderr
- + testsuite/tests/typecheck/should_compile/T22141d.hs
- + testsuite/tests/typecheck/should_compile/T22141d.stderr
- + testsuite/tests/typecheck/should_compile/T22141e.hs
- + testsuite/tests/typecheck/should_compile/T22141e.stderr
- + testsuite/tests/typecheck/should_compile/T22141e_Aux.hs
- + testsuite/tests/typecheck/should_compile/T22141f.hs
- + testsuite/tests/typecheck/should_compile/T22141g.hs


The diff was not included because it is too large.


View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9f9c92272b3ca11d54331cea83ad5e82e17fa062

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9f9c92272b3ca11d54331cea83ad5e82e17fa062
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20231101/91f03b33/attachment.html>