diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2020-10-12 19:51:57 -0400 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-10-14 12:04:34 -0400 |
commit | 716385c90f2f89ac45e256cdb7cdada1981b31ad (patch) | |
tree | a21daa10665856b228dab2df4a69a6e47d52bbbc | |
parent | 89f4d8e950a1ed2a3ffab424233d3bcd243b1771 (diff) | |
download | haskell-716385c90f2f89ac45e256cdb7cdada1981b31ad.tar.gz |
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.
-rw-r--r-- | compiler/GHC/Rename/HsType.hs | 24 | ||||
-rw-r--r-- | docs/users_guide/exts/data_kinds.rst | 29 | ||||
-rw-r--r-- | docs/users_guide/exts/poly_kinds.rst | 23 | ||||
-rw-r--r-- | testsuite/tests/th/T17688b.hs | 1 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T18831.hs | 12 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
6 files changed, 54 insertions, 36 deletions
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs index 9bd1fa64ac..77ece61c14 100644 --- a/compiler/GHC/Rename/HsType.hs +++ b/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) } diff --git a/docs/users_guide/exts/data_kinds.rst b/docs/users_guide/exts/data_kinds.rst index 7105b1adc8..86bd8832f5 100644 --- a/docs/users_guide/exts/data_kinds.rst +++ b/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,27 @@ above code is valid. See also :ghc-ticket:`7347`. +.. _constraints_in_kinds: + +Constraints in kinds +-------------------- + +Kinds can (with :extension:`DataKinds`) contain type constraints. However, +only equality constraints are supported. + +Here is an example of a constrained kind: :: + + type family IsTypeLit a where + IsTypeLit Nat = 'True + IsTypeLit Symbol = 'True + IsTypeLit a = 'False + + data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where + MkNat :: T 42 + MkSymbol :: T "Don't panic!" +The declarations above are accepted. However, if we add ``MkOther :: T Int``, +we get an error that the equality constraint is not satisfied; ``Int`` is +not a type literal. Note that explicitly quantifying with ``forall a`` is +necessary in order for ``T`` to typecheck +(see :ref:`complete-kind-signatures`). diff --git a/docs/users_guide/exts/poly_kinds.rst b/docs/users_guide/exts/poly_kinds.rst index 39bd6e6f49..58800d47cb 100644 --- a/docs/users_guide/exts/poly_kinds.rst +++ b/docs/users_guide/exts/poly_kinds.rst @@ -787,29 +787,6 @@ 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 --------------------- - -As kinds and types are the same, kinds can (with :extension:`TypeInType`) -contain type constraints. However, only equality constraints are supported. - -Here is an example of a constrained kind: :: - - type family IsTypeLit a where - IsTypeLit Nat = 'True - IsTypeLit Symbol = 'True - IsTypeLit a = 'False - - data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where - MkNat :: T 42 - MkSymbol :: T "Don't panic!" - -The declarations above are accepted. However, if we add ``MkOther :: T Int``, -we get an error that the equality constraint is not satisfied; ``Int`` is -not a type literal. Note that explicitly quantifying with ``forall a`` is -necessary in order for ``T`` to typecheck -(see :ref:`complete-kind-signatures`). - The kind ``Type`` ----------------- diff --git a/testsuite/tests/th/T17688b.hs b/testsuite/tests/th/T17688b.hs index f78cf0266a..f6252b79a4 100644 --- a/testsuite/tests/th/T17688b.hs +++ b/testsuite/tests/th/T17688b.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneKindSignatures #-} diff --git a/testsuite/tests/typecheck/should_compile/T18831.hs b/testsuite/tests/typecheck/should_compile/T18831.hs new file mode 100644 index 0000000000..f717aa911a --- /dev/null +++ b/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 diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index a74a84f461..ad682924e2 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/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, ['']) |