Say I have this:
data Animal = Dog | Cat
:t Dog
Dog :: Animal
Fair enough.
:k Dog
<interactive>:1:1:
Not in scope: type constructor or class ‘Dog’
A data constructor of that name is in scope; did you mean DataKinds?
Wasn't expecting that to work since Dog is a value, not a type. You cannot get a kind of a value, only a kind of a type, right?
But, if I do this:
:set -XDataKinds
data Animal = Dog | Cat
:k Dog
Dog :: Animal
What does this mean that you can get a kind of a value?
Nope. You can only get the kinds of types. What -XDataKinds
does is take data declarations and give them two meanings: first, it declares a new type and some corresponding value constructors; and second, it declares a new kind and some corresponding type constructors. So with DataKinds
on, the following declaration:
data Animal = Dog | Cat
creates all of the following:
Animal
Dog
of type Animal
Cat
of type Animal
Animal
Dog
of kind Animal
Cat
of kind Animal
The three namespaces -- term-level, type-level, and kind-level -- are completely disjoint. In case DataKinds
would define a new type in two different ways, you can use a prefix '
to indicate that you want the lifted version. Thus:
> :set -XDataKinds
> data Animal = Animal
> :k Animal
Animal :: *
> :k 'Animal
'Animal :: Animal