使用DataKinds，定义如
data KFoo = TFoo
介绍那种 KFoo :: BOX 和类型 TFoo :: KFoo。为什么我不能继续定义
data TFoo = CFoo
这样的 CFoo :: TFoo， TFoo :: KFoo， KFoo :: BOX？
所有构造函数都需要属于属于该类型的类型 *？如果是这样，为什么？
编辑：当我这样做时，我没有收到错误，因为构造函数和类型共享一个命名空间，但GHC允许冲突，因为它将名称消歧为常规类型，而不是提升构造函数。文档说前缀为 ' 引用提升的构造函数。当我改变第二行时
data 'TFoo = CFoo
我收到了错误
格式错误的类型或类声明：TFoo
所有构造函数都需要属于属于该类型的类型
*？
是。那正是如此 * 意思是：它是那种（提升/盒装，我从来不确定那部分）Haskell类型。事实上，除了共享之外，所有其他种类都不是真正的种类 type 句法。宁 * 是类型的元类型级别类型，所有其他类型是元类型级别类型，用于非类型但类型构造函数或完全不同的东西。
（同样，还有一些关于未装箱类型的东西;那些肯定是类型，但我认为这是不可能的 data 构造函数）。
所有构造函数都需要属于属于那种*的类型吗？如果是这样，为什么？
他们必须属于类型的最重要原因 * （要么 #）是GHC采用的相分离： DataKinds 在编译期间被删除。我们可以通过定义单例GADT数据类型来间接表示它们的运行时：
{-# LANGUAGE DataKinds #-}
data Nat = Z | S Nat
data SNat n where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
但是 DataKind 索引本身仍然不存在运行时。各种类型为相位分离提供了一个简单的规则，对于依赖类型来说这并不是那么简单（即使它可能会极大地简化类型级编程）。