为什么Idris 2中cong无法通过类型检查，如何解决该问题？

Idris 2 的 Prelude 中内置的cong函数签名与 Idris 1 存在关键差异：

• Idris 1 中的cong会自动推导需要应用到相等性证明两端的函数，调用时只需传入相等性证明参数即可
• Idris 2 中的cong签名为 cong : (f : a -> b) -> x = y -> f x = f y，要求显式传入第一个参数——即要作用在相等两端的函数

你原来的代码中直接写cong e时，编译器会把你传入的相等性证明e识别为第一个参数f，自然会出现类型不匹配的报错。你自己实现的cong'已经固定了要应用的函数是S构造器，不需要额外传参，因此可以正常通过检查。

有两种无需自定义cong'的轻量化修改方式，任选其一即可：

方案1：显式给cong传入函数参数S #

修改后的完整代码如下：

sameNat : (n : Nat) -> (m : Nat) -> Maybe (n = m)
sameNat Z Z = Just Refl
sameNat (S n) (S m) = case sameNat n m of
                        Just e => Just (cong S e)
                        Nothing => Nothing
sameNat _ _ = Nothing

方案2：使用Idris 2内置的congS工具 #

Idris 2 标准库中已经预置了专门针对S构造器的相等性证明映射函数congS，可以直接替换：

sameNat : (n : Nat) -> (m : Nat) -> Maybe (n = m)
sameNat Z Z = Just Refl
sameNat (S n) (S m) = case sameNat n m of
                        Just e => Just (congS e)
                        Nothing => Nothing
sameNat _ _ = Nothing

你原本自定义cong'替换的方案也完全可用。

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