Haskell GADT中为何函数f可被推断为T a -> a -> a类型？

示例代码如下：

data T a where
  T1 :: Bool -> T Bool
  T2 :: T a

f x y = case x of
  T1 _ -> True
  T2   -> y

觉得函数返回值必须是Bool，问题出在没搞清楚GADT的局部类型细化规则，错把分支内的局部约束当成了整个函数的全局约束：

• GADT构造器携带的类型约束，仅在匹配到该构造器的case分支内部生效，不会溢出到分支外影响全局类型推断。
• 匹配T1的分支里，构造器T1 :: Bool -> T Bool会把当前分支内的类型参数a局部约束为Bool，此时分支返回的True是Bool类型，刚好和局部约束下的a类型匹配，完全符合返回a类型的要求。
• 匹配T2的分支里，没有任何额外的类型约束，a保持多态状态，分支返回的y本身就是a类型，自然也满足返回要求。

两个分支的返回值在各自的局部作用域里都符合a类型的要求，因此函数能推断出的最通用类型就是T a -> a -> a，实际调用也完全符合这个签名：

• 传入T2和整数3，f T2 3会返回Int类型的3
• 传入T1 True和布尔值False，f (T1 True) False会返回Bool类型的True

如果把T2分支的返回值也改成True，此时因为T2分支不存在a ~ Bool的局部约束，返回Bool值才会把整个函数的返回类型固定为T a -> Bool。

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