id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
6024	Allow defining kinds alone, without a datatype	dreixel		"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`."	feature request	new	normal	7.8.1	Compiler (Type checker)	7.5			ross@…	Unknown/Multiple	Unknown/Multiple	None/Unknown	Unknown