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

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

Solution

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.)