Idris 1.3.3中可构造(Z = S Z)？类型检查异常问询

这是Idris 1类型检查器的已知漏洞，Idris 2对依赖类型的一致性校验做了严格改进，因此不会出现该问题。

问题代码回顾 #

doubleCong: {f: Nat -> Nat -> Nat} -> (prf1: (a1 = a2)) -> (prf2: (b1 = b3)) -> (f a1 b1 = f a2 b2)
doubleCong {f} prf1 prf2 = let intermediate = cong {f = f} prf1 in case intermediate of
                                                                        Refl impossible

zero_equals_1: (Z = S Z)
zero_equals_1 = doubleCong {b2=1} {f = (+)} (Refl {x=0}) (Refl {x=0})


anything: (a: Type) -> a
anything a = case zero_equals_1 of
                  Refl impossible

漏洞原因详解 #

1. 隐式变量约束缺失
   doubleCong的类型签名里，prf2的类型是b1 = b3，但函数返回的是f a1 b1 = f a2 b2——这里b3和b2没有任何绑定关系。Idris 1的类型检查器没有强制要求这两个变量必须一致，允许调用时给b2指定一个和b3完全无关的值（比如这里b3=Z，b2=S Z）。

2. 类型匹配校验漏洞
   doubleCong实现中，cong {f=f} prf1生成的是f a1 b1 = f a2 b1类型的证明，但函数需要返回f a1 b1 = f a2 b2。Idris 1没有检测到这两个类型的差异（因为b1和b2未被约束相等），反而错误地接受了case intermediate of Refl impossible这种逻辑不成立的分支处理——impossible在这里被判定为合法，本质是类型检查器的校验疏漏。

3. 矛盾证明的生成
   调用doubleCong时，传入的prf1是Z=Z，prf2是Z=Z，但显式指定b2=S Z。Idris 1未验证b2必须和prf2中的b3一致，因此生成了Z + Z = Z + S Z的证明，而这个等式等价于Z = S Z，也就是zero_equals_1的类型。

Idris 2的修复 #

Idris 2对依赖类型的变量一致性做了更严格的检查：

• 会发现doubleCong类型签名中b3和b2未绑定的问题，要求两者必须关联（比如修改为prf2: b1 = b2）；
• 在实现阶段会检测到intermediate的类型和函数返回类型不匹配，直接拒绝通过类型检查；
• 从根源上避免了这种逻辑矛盾的证明被构造出来。

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