GADTs与GADTSyntax的区别及GADT启用必要性与类型推断疑问

核心差异：构造器的类型签名约束 #

普通代数数据类型（ADT）的构造器，其返回类型必须是类型名+统一的类型参数。比如定义列表类型：

data List a = Nil | Cons a (List a)

这里Nil的类型是List a，Cons的类型是a -> List a -> List a——所有构造器返回的List的类型参数都是同一个变量a，构造器的参数类型也只能基于这个统一的a。

而广义代数数据类型（GADT）允许构造器返回类型参数被实例化到具体类型或更复杂约束的类型。比如定义表达式类型：

data Expr a where
  LitInt  :: Int -> Expr Int
  LitBool :: Bool -> Expr Bool
  Add     :: Expr Int -> Expr Int -> Expr Int

这里每个构造器的返回类型都是Expr的具体实例：LitInt返回Expr Int，LitBool返回Expr Bool，甚至可以让构造器的参数类型和返回类型的参数形成约束（比如Add要求两个参数都是Expr Int，返回也是Expr Int）。简单来说，GADT打破了“所有构造器共享同一套类型参数变量”的限制，让构造器可以自由指定返回类型的实例化形式。

为何必须显式启用GADTs？ #

• 类型推断复杂度飙升：GADT引入了依赖模式匹配的类型细化，这会让传统的Hindley-Milner类型推断算法无法在有限步骤内完成推导，甚至变得不可判定。默认关闭可以保证核心语言的类型推断效率和可预测性。
• 语言设计的保守性：GADT是对核心类型系统的扩展，它允许更精细的类型约束和类型级编程，这超出了普通ADT的设计目标。显式启用可以让开发者明确知晓自己在使用非核心特性，避免意外引入复杂的类型问题。
• 类型系统性质改变：GADT会让类型系统支持“等式约束”（比如匹配LitInt时，能推导出a ~ Int），这会打破普通ADT类型系统的一些简单性质（比如参数化多态的参数不变性），需要显式启用以区分两种类型系统的行为。

为什么不能把GADT构造器当普通函数做类型推断？ #

普通函数的类型推断基于Hindley-Milner算法，核心是统一化（unification）——通过匹配类型变量和具体类型来推导最一般的类型。但GADT构造器的特殊之处在于：
当你对GADT值做模式匹配时，会产生类型等式约束（比如匹配LitInt n时，当前上下文的Expr a会被细化为Expr Int，即a ~ Int）。这类约束不是简单的变量替换，而是依赖于模式匹配的分支，会导致统一化过程出现递归或无法解决的冲突，最终让类型推断变得不可判定。

普通函数的类型推断不需要处理这种“分支依赖的类型细化”，而GADT的构造器本质上是带有类型约束的函数，这种约束无法被Hindley-Milner的原有框架处理，因此不能直接纳入普通类型推断流程。

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