Allow defining kinds alone, without a datatype

Sometimes we want to define a kind alone, and we are not interested in the datatype. In principle having an extra datatype around is not a big problem, but the constructor names will be taken, so they cannot be used somewhere else. A contrived example:

data Code = Unit | Prod Code Code

data family Interprt (c :: Code) :: *
data instance Interprt Unit       = Unit1
data instance Interprt (Prod a b) = Prod1 (Interprt a) (Interprt b)

We're only interested in the constructors of the data family Interprt, but we cannot use the names Unit and Prod because they are constructors of Code.

The suggestion is to allow defining:

data kind Code = Unit | Prod Code Code

Such that Code is a kind, and not a type, and Unit and Prod are types, and not constructors.

Note that using "data kind" instead of just "kind" means the word "kind" does not have to be a reserved keyword.

You could also think you would want to have datatypes that should not be promoted:

data K

data type T = K

But I don't see a need for this, as the fact that the K constructor is promoted to a type does not prevent you from having a datatype named K.

Trac metadata

Trac field	Value
Version	7.5
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture