GHC2024中ADTs与GADTs的语法及定义差异问询

我对数据类型声明的细节理解不够透彻，在多种定义方式中感到困惑：是否该用GADT语法？是否需要写出类型构造器的kind签名或其类型参数的kind？

下面的示例让我产生了**这些语法到底有何差异？**的疑问：

一篇singletons教程里的带幻影类型参数的数据类型声明：

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

之后又给出了GADT语法的替代写法：

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

我目前能理解的是这两种形式都表达了：

• Door是Type构造器
  • 后者通过-> Type显式声明了这一点
  • 前者则是通过构造器能生成属于Type的项，间接体现这一点
• Door是一元类型构造器，接受一个DoorState kind的类型参数

但我还写出了这种介于两者之间的形式：

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

这种写法用了GADT语法的where，但又像非GADT语法那样显式指定了Door的类型参数s并标注了:: DoorState。

关键疑问是：这里的s和前两种写法里的s是否是同一指代？这种定义Door的方式和前两种有没有本质差异？

我知道查看ADTs和GADTs的语法规范会有帮助，但不确定该找哪里。之前了解到Haskell2010报告是规范，但上面这些代码依赖的扩展都超出了Haskell2010的范围，所以想知道GHC2024中ADTs与GADTs的语法细节。

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