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 |