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.)

• All other contexts where types can appear are referred to as type contexts.

• The kind type constructors are (see GHC.Core.TyCon.isKindTyCon):

  • TYPE and Type
  • CONSTRAINT and Constraint
  • 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 the TypeData extension, such as the T in type 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)

• 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 in T Int is rejected even though the expansion is just Type. This is consistent with, for example, rejecting T (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.