GHC-9.4 accepts "data" in kinds without DataKinds
import GHC.TypeLits (Nat)
import Data.Kind (Type)
data Vector :: Nat -> Type -> Type where
is accepted by GHC-9.4 with just -XHaskell2010 -XGADTSyntax -XKindSignatures
. GHC-9.2 and older require DataKinds
. I cannot find anything in release notes justifying this change.
If it's intentional, please amend release notes.
Here is a specification for what -XDataKinds
allows, or doesn't. First, some definitions:
-
A user-written type (i.e. part of the source text of a program) is in a kind context if it follows a "::" in:
- A standalone kind signature (e.g.
type T :: Nat -> Type
) - A kind signature in a type (e.g.
forall (a :: Nat -> Type). blah
,type F = G :: Nat -> Type
, etc.) - A result kind signature in a type declaration (e.g.
data T a :: Nat -> Type where ...
,type family Fam :: Nat -> Type
, etc.)
- A standalone kind signature (e.g.
-
All other contexts where types can appear are referred to as type contexts.
-
The kind type constructors are (see
GHC.Core.TyCon.isKindTyCon
):-
TYPE
andType
-
CONSTRAINT
andConstraint
LiftedRep
-
RuntimeRep
,Levity
, and their data constructors -
Multiplicity
and its data construtors -
VecCount
,VecElem
, and their data constructors
-
-
A
type data
type constructor is defined using theTypeData
extension, such as theT
intype data T = A | B
. -
The following are rejected in type contexts unless
-XDataKinds
is enabled:- Promoted data constructors (e.g.,
'Just
), except for those data constructors listed under "kind type constructors" - Promoted list or tuple syntax (e.g.,
'[Int, Bool]
or'(Int, Bool)
) - Type-level literals (e.g.,
42
,"hello"
, or'a'
at the type level)
- Promoted data constructors (e.g.,
-
The following are rejected in kind contexts unless
-XDataKinds
is enabled:-
Everything that is rejected in a type context.
-
Any type constructor that is not a kind type constructor or a
type data
type constructor (e.g.,Maybe
,[]
,Char
,Nat
,Symbol
, etc.)Note that this includes rejecting occurrences of non-kind type construtors in type synomym (or type family) applications, even it the expansion would be legal. For example:
type T a = Type f :: forall (x :: T Int). blah
Here the
Int
inT Int
is rejected even though the expansion is justType
. This is consistent with, for example, rejectingT (forall a. a->a)
without-XImpredicativeTypes
.This check only occurs in kind contexts. It is always permissible to mention type synonyms in a type context without enabling
-XDataKinds
, even if the type synonym expands to something that would otherwise require-XDataKinds
.
-