[Git][ghc/ghc][wip/T18831] Make DataKinds the sole arbiter of kind-level literals (and friends)
Ryan Scott
gitlab at gitlab.haskell.org
Tue Oct 13 09:01:08 UTC 2020
Ryan Scott pushed to branch wip/T18831 at Glasgow Haskell Compiler / GHC
Commits:
5b9e529d by Ryan Scott at 2020-10-13T05:00:36-04:00
Make DataKinds the sole arbiter of kind-level literals (and friends)
Previously, the use of kind-level literals, promoted tuples,
and promoted lists required enabling both `DataKinds` and
`PolyKinds`. This made sense back in a `TypeInType` world, but not so
much now that `TypeInType`'s role has been superseded. Nowadays,
`PolyKinds` only controls kind polymorphism, so let's make `DataKinds`
the thing that controls the other aspects of `TypeInType`, which include
literals, promoted tuples and promoted lists.
There are some other things that overzealously required `PolyKinds`,
which this patch fixes as well:
* Previously, using constraints in kinds (e.g., `data T :: () -> Type`)
required `PolyKinds`, despite the fact that this is orthogonal to kind
polymorphism. This now requires `DataKinds` instead.
* Previously, using kind annotations in kinds
(e.g., `data T :: (Type :: Type) -> Type`) required both `KindSignatures`
and `PolyKinds`. This doesn't make much sense, so it only requires
`KindSignatures` now.
Fixes #18831.
- - - - -
6 changed files:
- compiler/GHC/Rename/HsType.hs
- docs/users_guide/exts/data_kinds.rst
- docs/users_guide/exts/poly_kinds.rst
- testsuite/tests/th/T17688b.hs
- + testsuite/tests/typecheck/should_compile/T18831.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -441,9 +441,9 @@ sites. This is less precise, but more accurate.
rnHsType is here because we call it from loadInstDecl, and I didn't
want a gratuitous knot.
-Note [QualTy in kinds]
+Note [HsQualTy in kinds]
~~~~~~~~~~~~~~~~~~~~~~
-I was wondering whether QualTy could occur only at TypeLevel. But no,
+I was wondering whether HsQualTy could occur only at TypeLevel. But no,
we can have a qualified type in a kind too. Here is an example:
type family F a where
@@ -466,9 +466,9 @@ suitable message:
Expected kind: G Bool
Actual kind: F Bool
-However: in a kind, the constraints in the QualTy must all be
+However: in a kind, the constraints in the HsQualTy must all be
equalities; or at least, any kinds with a class constraint are
-uninhabited.
+uninhabited. See Note [Constraints in kinds] in GHC.Core.TyCo.Rep.
-}
data RnTyKiEnv
@@ -574,7 +574,9 @@ rnHsTyKi env ty@(HsForAllTy { hst_tele = tele, hst_body = tau })
, fvs) } }
rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
- = do { checkPolyKinds env ty -- See Note [QualTy in kinds]
+ = do { data_kinds <- xoptM LangExt.DataKinds -- See Note [HsQualTy in kinds]
+ ; when (not data_kinds && isRnKindLevel env)
+ (addErr (dataKindsErr env ty))
; (ctxt', fvs1) <- rnTyKiContext env lctxt
; (tau', fvs2) <- rnLHsTyKi env tau
; return (HsQualTy { hst_xqual = noExtField, hst_ctxt = ctxt'
@@ -636,9 +638,8 @@ rnHsTyKi env listTy@(HsListTy _ ty)
; (ty', fvs) <- rnLHsTyKi env ty
; return (HsListTy noExtField ty', fvs) }
-rnHsTyKi env t@(HsKindSig _ ty k)
- = do { checkPolyKinds env t
- ; kind_sigs_ok <- xoptM LangExt.KindSignatures
+rnHsTyKi env (HsKindSig _ ty k)
+ = do { kind_sigs_ok <- xoptM LangExt.KindSignatures
; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty)
; (ty', lhs_fvs) <- rnLHsTyKi env ty
; (k', sig_fvs) <- rnLHsTyKi (env { rtke_level = KindLevel }) k
@@ -665,7 +666,6 @@ rnHsTyKi env tyLit@(HsTyLit _ t)
= do { data_kinds <- xoptM LangExt.DataKinds
; unless data_kinds (addErr (dataKindsErr env tyLit))
; when (negLit t) (addErr negLitErr)
- ; checkPolyKinds env tyLit
; return (HsTyLit noExtField t, emptyFVs) }
where
negLit (HsStrTy _ _) = False
@@ -705,15 +705,13 @@ rnHsTyKi _ (XHsType (NHsCoreTy ty))
-- but I don't think it matters
rnHsTyKi env ty@(HsExplicitListTy _ ip tys)
- = do { checkPolyKinds env ty
- ; data_kinds <- xoptM LangExt.DataKinds
+ = do { data_kinds <- xoptM LangExt.DataKinds
; unless data_kinds (addErr (dataKindsErr env ty))
; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
; return (HsExplicitListTy noExtField ip tys', fvs) }
rnHsTyKi env ty@(HsExplicitTupleTy _ tys)
- = do { checkPolyKinds env ty
- ; data_kinds <- xoptM LangExt.DataKinds
+ = do { data_kinds <- xoptM LangExt.DataKinds
; unless data_kinds (addErr (dataKindsErr env ty))
; (tys', fvs) <- mapFvRn (rnLHsTyKi env) tys
; return (HsExplicitTupleTy noExtField tys', fvs) }
=====================================
docs/users_guide/exts/data_kinds.rst
=====================================
@@ -134,6 +134,12 @@ promotion quote and the data constructor: ::
type S = 'A' -- ERROR: looks like a character
type R = ' A' -- OK: promoted `A'`
+Type-level literals
+-------------------
+
+:extension:`DataKinds` enables the use of numeric and string literals at the
+type level. For more information, see :ref:`type-level-literals`.
+
.. _promoted-lists-and-tuples:
Promoted list and tuple types
@@ -207,4 +213,8 @@ above code is valid.
See also :ghc-ticket:`7347`.
+Constraints in kinds
+--------------------
+:extension:`DataKinds` enables the use of equality constraints in kinds. For
+more information, see :ref:`constraints-in-kinds`.
=====================================
docs/users_guide/exts/poly_kinds.rst
=====================================
@@ -787,6 +787,8 @@ distinction). GHC does not consider ``forall k. k -> Type`` and
``forall {k}. k -> Type`` to be equal at the kind level, and thus rejects
``Foo Proxy`` as ill-kinded.
+.. _constraints_in_kinds:
+
Constraints in kinds
--------------------
=====================================
testsuite/tests/th/T17688b.hs
=====================================
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
=====================================
testsuite/tests/typecheck/should_compile/T18831.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+module T18831 where
+
+import Data.Kind
+import Data.Proxy
+
+data T1 :: Proxy 0 -> Type
+data T2 :: () => Type
+data T3 :: (Type :: Type) -> Type
+data T4 :: Proxy '[Type,Type] -> Type
+data T5 :: Proxy '(Type,Type) -> Type
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -722,5 +722,6 @@ test('T18412', normal, compile, [''])
test('T18470', normal, compile, [''])
test('T18323', normal, compile, [''])
test('T18585', normal, compile, [''])
+test('T18831', normal, compile, [''])
test('T15942', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5b9e529d01eb1c9d88a3cb4832245f758b479cb9
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5b9e529d01eb1c9d88a3cb4832245f758b479cb9
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/20201013/49424f13/attachment-0001.html>
More information about the ghc-commits
mailing list