Is there a reason we can't populate types with DataKinds?

Question

With DataKinds, a definition like

data KFoo = TFoo

introduces the kind KFoo :: BOX and the type TFoo :: KFoo. Why can't I then go on to define

data TFoo = CFoo

such that CFoo :: TFoo, TFoo :: KFoo, KFoo :: BOX?

Do all constructors need to belong to a type that belongs to the kind *? If so, why?

Edit: I don't get an error when I do this, because constructors and types share a namespace, but GHC permits conflicts because it disambiguates names as regular types, rather than promoted constructors. The docs say to prefix with a ' to refer to the promoted constructor. When I change that second line to

data 'TFoo = CFoo

I get the error

Malformed head of type or class declaration: TFoo

Bosomed

What error do you get when you try to define data TFoo? – Grafton

Answer 1

Do all constructors need to belong to a type that belongs to the kind *?

Yes. That's exactly what * means: it's the kind of (lifted / boxed, I'm never sure about that part) Haskell types. Indeed all other kinds aren't really kinds of types though they share the type syntax. Rather * is the metatype-level type for types, and all other kinds are metatype-level types for things that aren't types but type constructors or something completely different.

(Again, there's also something about unboxed-type kinds; those certainly are types but I think this isn't possible for a data constructor.)

Ellynellynn

Typically I wouldn't type the word "type" so often in a single post. – Ellynellynn

* is kind of all lifted types and # is unlifted. * and # together encapsulate all types which have values. Boxed just refers to if something is a pointer or not, I believe. – Thermography

Boxed, unboxed types have the kind # which is why you can't use them in polymorphic functions, kind mismatched. There's also ? which is the top of all kinds and ?? which is the lub of * and #. – Kerplunk

Answer 2

Do all constructors need to belong to a type that belongs to the kind *? If so, why?

The most important reason why they must be of type * (or #) is the phase separation employed by GHC: DataKinds get erased during compilation. We can represent them runtime only indirectly, by defining singleton GADT datatypes:

{-# LANGUAGE DataKinds #-}

data Nat = Z | S Nat

data SNat n where
   SZ :: SNat Z
   SS :: SNat n -> SNat (S n)

But the DataKind indices themselves still don't exist runtime. The various kinds offer a simple rule for phase separation, which wouldn't be as straightforward with dependent types (even though it would potentially simplify type level programming greatly).

Cyrillus