为什么 Idris 的 Refl 有时不进行类型检查？

Question

我正在阅读 Idris 的书，并且正在做第一个证明练习。

通过证明same_lists 的练习，我能够像这样实现它，因为匹配Refl 强制x 和y 统一：

total same_lists : {xs : List a} -> {ys : List a} ->
    x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

但是，当我尝试以相同的方式证明其他事情时，我会遇到不匹配的情况。例如：

total allSame2 : (x, y : Nat) -> x = y -> S x = S y
allSame2 x y Refl = Refl

编译器说：

Type mismatch between
   y = y (Type of Refl)
and
   x = y (Expected type)

如果我在 = 之后进行大小写匹配，无论是显式还是使用 lambda，它都会按预期工作：

total allSame2 : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
allSame2 x y = \Refl => Refl

这里有什么不同？

另一个有效的修改是隐含有问题的参数：

total allSame2 : {x : Nat} -> {y : Nat} -> x = y -> S x = S y
allSame2 Refl = Refl

Answer 1

我不知道所有细节，但我可以给你一个粗略的想法。在 Idris 中，命名函数的参数列表是特殊的，因为它是依赖模式匹配的一部分。当您进行模式匹配时，它还会重写其他参数。

same_lists x y Refl = Refl 无效，我大致猜想，因为 Idris 将 x 和 y 重写为相同，并且您不能再给这个单一的值起不同的名字——我希望有人能给更好地解释这种机制。相反，您可以使用 same_lists x x Refl = Refl — 请注意，名称 x 并不重要，只是在两个站点中使用相同的名称。

lambda 参数与命名参数列表不同。因此，由于您在 lambda 中进行匹配，Idris 只会在此时重写其他参数。关键是，在第一个示例中，Idris 想要一次完成所有操作，因为它是同一个参数列表的一部分。

对于最后一个示例，唯一的变化是您没有为参数指定不同的名称。使用all_same _ _ Refl = Refl 也是有效的。当参数为隐式时，Idris 会为您正确填写。

最后你可以考虑same_lists = \x, y, Refl => Refl，它也可以。这是因为 Idris 不会重写未命名的参数列表（即 lambda 参数）。