Haskell's DataKinds and relation of values, types and kinds

Question

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?

Answer 1

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:

• type Animal
• value Dog of type Animal
• value Cat of type Animal
• kind Animal
• type Dog of kind Animal
• type 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