Haskell为何无法为此GADT推断类型？
问题背景
首先定义如下简单GADT：
data GADT a where MkGADT :: Int -> GADT Int
现象1：无类型签名定义函数报错
在GHCi中执行以下函数定义：
inferGADT (MkGADT n) = "123"
会触发类型错误，提示无法推导p ~ String。此时GHC推断出的函数骨架为inferGADT :: GADT a -> p，其中a已通过模式匹配确定为Int（即a ~ Int），但p是刚性类型变量，无法自动关联到返回值的String类型。
现象2：添加类型注解后正常运行
为模式匹配的参数添加类型注解后，函数可正常定义：
inferGADT ((MkGADT n)::(GADT Int)) = "123"
执行:t inferGADT查看类型，结果为：
inferGADT :: GADT Int -> String
现象3：直接构造值可自动推断类型
直接构造GADT值时，GHC能正确推断出具体类型：
ghci> :t (MkGADT 1) (MkGADT 1) :: GADT Int
核心疑问
- 既然
MkGADT构造函数明确标注了Int -> GADT Int，为何模式匹配时无法自动推断出函数的参数类型是GADT Int？ - 错误信息中已确定
a ~ Int，为何无法进一步推导返回值类型p ~ String？ - 该场景下GHC的类型推断具体流程是怎样的？
问题解析
1. 类型推断的初始阶段：函数骨架生成
当你定义inferGADT (MkGADT n) = "123"时，GHC首先会生成最通用的函数类型骨架：inferGADT :: GADT a -> p。这里的a和p都是刚性类型变量——它们是尚未绑定到具体类型的占位符，但GHC不会随意修改它们的绑定关系，除非有明确约束。
2. GADT模式匹配的约束传递
匹配MkGADT n时，GHC确实能从构造函数的类型Int -> GADT Int推导出a ~ Int，这个约束会被记录下来，但此时的类型骨架仍为GADT a -> p，只是附加了a ~ Int的约束。
3. 返回值类型无法关联的原因
问题出在返回值"123"的String类型无法传递给刚性变量p。Haskell类型推断遵循让函数尽可能通用的原则：如果没有明确的类型注解，GHC会假设函数可能接受任意GADT a类型的参数（即使当前模式只匹配了GADT Int），并返回任意p类型的值——但当前实现只能处理GADT Int并返回String，这就产生了矛盾。
换句话说，GHC不会因为你写了一个匹配GADT Int的模式，就自动缩小函数的参数类型范围，也不会因为返回值是String就直接绑定p到String——它需要明确的类型注解来打破这种“通用性假设”。
4. 类型注解的作用
当你为参数添加:: GADT Int的注解时，相当于明确告诉GHC：这个函数只接受GADT Int类型的参数。此时类型骨架中的a被固定为Int，同时返回值"123"的String类型可以直接绑定到p，最终得到明确的类型GADT Int -> String。
5. 直接构造值的推断逻辑
直接构造MkGADT 1时，不存在“通用性假设”——GHC只需要根据构造函数的类型，直接推导出结果是GADT Int，不需要考虑函数的通用性，所以推断过程简单直接。
内容的提问来源于stack exchange，提问作者Evg
