我的问题在于我还没有完全理解声明数据类型的细微差别。我觉得在外面那些自由度里容易迷失： 我应该使用GADT语法吗？我该把类型构造子的kind签名写清楚，还是把类型构造子的类型参数的kind写清楚？

下面有一个例子，在那里自然会问“这些语法之间有什么区别？”

这个关于单子（单例）类型的教程 展示了这段代码，演示如何声明一个带有虚拟类型参数的数据类型：

data Door (s :: DoorState) = UnsafeMkDoor { doorMaterial :: String }

稍后给出另一种写法，使用GADT语法：

data Door :: DoorState -> Type where
    UnsafeMkDoor :: { doorMaterial :: String } -> Door s

据我的理解，这两种形式都传达了

• Door 是一个 Type 构造子

• 后者通过 -> Type 明确地表达，

• 前者通过提供一个数据构造子来形成一个 项（terms），如果有什么有一个 项，那么它就是一个 Type；
• Door 类型构造子是单参的，接收一个kind为 DoorState 的类型。

但我也可以像下面这样重写上面的内容：

data Door (s :: DoorState) where
  UnsafeMkDoor :: { doorMaterial :: String } -> Door s

这感觉像介于两者之间，因为它使用了 where，就像GADT语法一样，但它明确提到了 Door 的类型参数，给它命名为 s 并用 :: DoorState 标注，就像非GADT的语法一样。

关键在于，后者的 s 并不指向前者，但这样定义 Door 的方式在本质上还有没有什么根本性的区别？

我想看到ADT与 GADT的语法规则应该会很有帮助，但我也不确定去哪里查找。曾经 我无意中问过，答案是 [Haskell报告（The Haskell Report）] 是权威的规范，但那只在使用Haskell2010时成立，而上面的代码片段所假设的扩展并非如此。

解决方案

据我所知，这三种变体之间没有差别。

GADT语法在GHC用户手册中有一个语法规则： https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/gadt_syntax.html#formal-syntax-for-gadts