关于Haskell DataKinds升阶类型的三个常见技术问题

你遇到的报错本质上是语法层面的不合法：'Zero本身不是可以承载项的类型，它的Kind是Nat，只有Kind为Type（以及其相关子类）的类型才能作为项的类型签名，所以你直接写undefined :: 'Zero必然会报错。
如果需要把类型层面的升阶构造器和项层级的值做关联，可以用*单例类型（Singleton）*的方案，通过GADT桥接类型层级和项层级：

{-# LANGUAGE GADTs, DataKinds #-}
data SNat :: Nat -> Type where
  SZero :: SNat 'Zero
  SSucc :: SNat n -> SNat ('Succ n)

此时SNat 'Zero就是Kind为Type的合法类型，它的非底居民只有SZero，刚好对应类型层面的'Zero标记，此时你就可以合法写出undefined :: SNat 'Zero或者SZero :: SNat 'Zero。

不是，除了Type之外，还有多类Kind可以承载项层级的值：

• Constraint：类型类约束的Kind就是Constraint，它的居民是类型类的实例字典，只是GHC默认会隐式处理这类值的传递，不会让用户显式书写。
• 未装箱类型对应的Kind：开启底层扩展后可以接触到UnliftedType、BoxedRep r这类Kind，比如GHC原生的未装箱整数Int#的Kind就是UnliftedType，它也有对应的项层级值，只是这类值不支持惰性求值、也不能为底。
• 底层的TYPE rep类Kind：Type本身就是TYPE LiftedRep的别名，所有可以承载项的Kind本质上都是TYPE的不同实例。

是的，升阶得到的、Kind不为Type的类型（比如'Zero、'Succ 'Zero这类Kind为Nat的类型）本身没有任何项层级居民，只能用在类型层面做标记、执行类型级计算。
如果需要在项层面关联这类升阶类型的语义，就需要用到第一个问题提到的单例类型，或者其他带Kind参数的类型构造器（比如长度索引向量Vec :: Nat -> Type -> Type），把升阶类型作为参数传入Kind为Nat -> Type的类型构造器，得到的Kind为Type的类型才会有对应的项层级居民。

内容的提问来源于stack exchange，提问作者wliao