Haskell如何检测冗余约束？基于GHC的可行性与现有设施问询

逻辑层面的可行性 #

这类冗余约束检测的本质是经典逻辑下的约束蕴含关系判定：即拿到类型签名头部的完整约束集合，逐一验证每个约束是否可以被集合内的其他约束通过已有的类定义、实例规则逻辑推导出来；如果推导成立，这个约束就是可以安全移除的重言式冗余项。

先以上述场景的示例代码作为分析基础：

class    (A a, B a) => C1 a -- C1 ~ A AND B
instance (A a, B a) => C1 a

class    (A a, B a, C a) => C2 a
instance (A a, B a, C a) => C2 a

f :: (C1 a, C2 a) => a
f = ...

从可判定性边界看，这类场景的冗余检测完全没有逻辑层面的障碍：

• 示例中C2 a的约束经过超类展开，可以直接得到A a、B a、C a三个已知前提；而C1 a的成立仅需要A a、B a两个前提，属于已知前提可以完全覆盖的推导关系，不存在无法证明的逻辑盲区。
• 仅当检测场景涉及不受控的递归实例、非终止的类型族归约时，才可能出现蕴含判定无法停机的问题；但GHC本身已经对这类场景做了强制的无环校验、类型族终止性检查，把这类不可判定的输入拦在了类型检查阶段，因此所有正常可编译的代码范围内，冗余约束检测都是可落地的。

GHC现有底层基础设施的支撑能力 #

GHC的编译管线已经覆盖了冗余约束检测需要的全部核心能力，不存在需要从零搭建的技术缺口：

• GHC内置的类型约束求解器，在处理类型签名约束时会自动完成全量超类展开、实例上下文匹配、约束归约的全流程，天然就能计算出任意约束的可推导前提闭包。比如你写上述f的类型签名时，求解器已经默默完成了所有超类展开，明确知道C2 a已经覆盖了C1 a的成立前提。
• GHC从8.0版本开始就内置了-Wredundant-constraints警告开关，已经能覆盖一部分基础场景的冗余检测：比如重复书写的相同约束、通过直接超类关联蕴含的约束（比如有Ord a约束时重复写Eq a），这类场景下编译器会直接抛出冗余提示。
• 示例中提到的“跨类的非直接超类关联冗余”目前没有被默认警告规则覆盖，本质不是能力缺失，而是现有告警规则过于保守导致的：
  • 现在的-Wredundant-constraints只会在求解过程中完全不触发实例匹配、纯靠直接超类展开就可以证明约束冗余的场景下触发提示；对于示例中C2和C1没有直接继承关系、需要计算两个类的超类闭包做集合包含判断的场景，虽然求解器可以轻松完成计算，但现有逻辑没有把这部分闭包计算结果传递给告警模块。
• 所有实现更激进冗余检测需要的编译钩子、底层数据结构（比如类的超类闭包表、约束求解的推导路径记录）GHC都已经对外暴露，只需要在现有管线上把已有的能力串接，就可以实现覆盖全场景的冗余约束检测。

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