手把手教你Lambda式类型推导——纠错：unifyCtx的实现有问题

WARNING

本文纠正了手把手教你Lambda式类型推导，C++老登都能看懂（2）中的一个 bug。如果你看过那篇文章，请务必注意。

对应代码：https://github.com/xiaoshihou514/xingli

问题所在

第2篇中，我给出了如下的 unifyctx 实现：

unifyctx :: TypeCtx -> TypeCtx -> Maybe (PrincipalPair -> PrincipalPair)
unifyctx ctx1 ctx2 = (liftPP . foldr (.) id) <$> sequence subs
  where
    subs = [unify a b | (x, a) <- Map.toList env1, b <- maybeToList $ Map.lookup x env2]
    env1 = env ctx1
    env2 = env ctx2

这个实现是错误的。

问题在于：subs 中每对变量的类型统一是独立进行的——对第一对变量的统一所产生的替换，从未被应用到剩余的变量对上。

举个具体例子，假设两个上下文都给共享变量 x 和 y 赋了类型：

ctx1: x : A -> B,  y : A
ctx2: x : C -> D,  y : C

正确的做法是：

1. 统一 A -> B 和 C -> D，得到 s1 = [A ↦ C, B ↦ D]。
2. 把 s1 应用到剩余变量对上：y 对变成 (s1 A, s1 C) = (C, C)。
3. 统一 C 和 C，得到 s2 = id。
4. 组合：s2 ∘ s1。

而旧代码跳过了第 2 步：它把 A 和 C 独立地统一（不管 s1 已经说了什么），单独产生一个替换 [A ↦ C]，再和 s1 组合。在简单情况下结果可能相同，但一般情况下并不成立——组合后的替换不一定能让所有共同变量的类型真正相等。

我在用Lean形式化证明该算法的可靠性时发现了这个bug。

修复方法

引入一个递归辅助函数 unifyCtx'，将替换顺序穿插传播：

-- 输入：(变量名, ctx1中的类型, ctx2中的类型) 三元组列表
unifyCtx' :: [(Label, CurryType, CurryType)] -> Maybe [CurryType -> CurryType]
unifyCtx' [] = Just []
unifyCtx' ((_, a, b) : rest) = do
    s1   <- unify a b
    -- 先把 s1 应用到所有剩余对，再递归
    exs' <- unifyCtx' (map (\(x, ta, tb) -> (x, s1 ta, s1 tb)) rest)
    return (s1 : exs')

unifyctx :: TypeCtx -> TypeCtx -> Maybe (PrincipalPair -> PrincipalPair)
unifyctx ctx1 ctx2 = do
    exs <- unifyCtx' common
    return $ liftPP (foldl (.) id exs)
  where
    common = [ (x, a, b)
             | (x, a) <- Map.toList env1
             , b      <- maybeToList $ Map.lookup x env2
             ]
    env1 = env ctx1
    env2 = env ctx2

算法的其余部分不变。

---

整个算法（修正 unifyctx 之后）已在 Lean 4 中形式化证明了可靠性，可参考STLC类型推导之证明.pdf。