{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ Nat

DataKinds according to GHC User Guide, promotes datatype to a kind and constructors to type constructors.

Nat :: Type
'Zero :: Nat
'Succ :: Nat -> Nat

Q1. Types are sets of values, but how can I get term-level values of the promoted types?

In ghci, for example, bottom is even not inhabitants of type `'Zero'.

λ: undefined :: 'Zero

<interactive>:3:14: error:
    • Expected a type, but ‘'Zero’ has kind ‘Nat’
    • In an expression type signature: 'Zero
      In the expression: undefined :: 'Zero
      In an equation for ‘it’: it = undefined :: 'Zero

Q2. Is type of kind Type the only kind where term-level values can inhabit?

Q3. If there is no inhabitants in the promoted types, does this also mean the promoted types `'Zero' ''Succ' can only be used at type-level?

CodePudding user response：

1. No values inhabit promoted types.
2. Yes, Type is the only kind with types inhabited by terms.
3. Yes, 'Zero and 'Succ can only be used at the type-level. But I think this is not so interesting an observation; it is also true that, say, Int can only be used at the type-level.