Haskell中GADT绑定时Functional dependency无法统一问题

核心问题是GHC的类型检查器默认不会跨类型量化作用域自动应用函数依赖（Functional Dependency，下称FD）的等价推导规则，两个冲突的类型变量b/b1属于完全独立的量化作用域：

• Foo构造器的类型为forall a b. FD a b => b -> Foo a，对Foo x做模式匹配时，构造器自带的b是全新的刚性类型变量（即报错信息中的b1），仅和构造器上下文内的a满足FD a b1约束。
• unFoo签名中的b是函数顶层量化的另一个独立刚性类型变量，仅和函数签名中的a满足FD a b约束。

虽然FD规则约定了同一个a可以唯一确定对应的b，但GHC并不会主动将两个不同作用域下的FD约束关联推导，没有显式证据的前提下不会判定b和b1等价，因此抛出类型不匹配错误。

如果需要保留FD写法，可以开启GHC扩展UndecidableInstances+QuantifiedConstraints满足推导要求；更简单的方式是将FD替换为类型家族实现等价逻辑，不会出现类型匹配问题，示例代码如下：

class FD a where
  type B a :: *

data Foo a where
  Foo :: B a -> Foo a

unFoo :: Foo a -> B a
unFoo (Foo x) = x

该写法中关联类型B a对同一个a全局唯一，GHC可以直接判定类型等价。

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