高阶多态类型推断中，是否存在计算两类型最大下界的算法？

你提到的场景属于高阶子类型化中求类型的最大下界（Greatest Lower Bound, GLB）——也就是你所说的“最小公共类型”：即同时是两个目标类型子类型的最宽泛（最大）类型。你的初步思路方向完全正确，这类问题已有成熟的理论和算法支撑：

核心思路：基于类型结构的协变/逆变换算 #

函数类型的子类型遵循逆变-协变规则：T₁ → T₂ <: S₁ → S₂ 当且仅当 S₁ <: T₁（参数位置逆变）且 T₂ <: S₂（返回值位置协变）。求两个函数类型的GLB时，需对各部分分别处理：

• 参数部分：由于逆变特性，需要计算两个参数类型的最小上界（LUB）
• 返回值部分：直接计算两个返回值类型的GLB

对应你给出的案例：

1. 对于 forall a. a → Int 和 forall a. a → Bool：
   两者结构统一为 forall a. (a → R)，参数都是a（LUB为自身），返回值Int和Bool无简单GLB，因此将差异抽象为全称量化变量，得到forall a. a → a——该类型可通过实例化返回值变量分别匹配Int和Bool，满足子类型关系。
2. 对于 (forall a. a) → Int 和 (forall a. a) → Bool：
   参数部分的LUB是forall a. a（自身），返回值部分的GLB抽象为forall a. a，因此组合得到(forall a. a) → (forall a. a)。

成熟算法体系 #

在任意秩多态场景下，这类GLB求解算法已被深入研究，核心组件包括：

• 结构递归遍历：递归拆解类型结构（函数、全称量化类型等），对每个子节点分别计算GLB/LUB
• 量化变量抽象：当遇到无法直接统一的具体类型时，将差异部分抽象为全称量化变量，确保生成的类型具备足够多态性以适配原类型
• 约束集求解：将子类型关系转化为约束集合，通过约束求解器推导满足所有条件的最一般化类型（即GLB）

这类算法正是《Practical Type Inference for Arbitrary-Rank Types》所讨论的类型推断体系的扩展部分，相关逻辑也已在工业级编译器中落地——比如Haskell的GHC编译器，其高阶多态子类型处理就基于上述思路实现。

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