Commit 716385c9 authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

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.
parent 89f4d8e9
Pipeline #26293 passed with stages
in 341 minutes and 50 seconds
......@@ -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) }
......
......@@ -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`).
......@@ -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``
-----------------
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
......
{-# 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
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment