Idris - 归纳步骤的证明

Question

考虑以下函数

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber)
tryMove Z from to [] = Nothing
tryMove (S k) from to (smallestDiskPosition :: restOfTheDisposition) =
        map (smallestDiskPosition ::) (tryMove k from to restOfTheDisposition)

尝试编译时出现以下错误：

When checking argument prf to Hanoi.tryMove:
        Type mismatch between
                So True (Type of Oh)
        and
                So (from /= to) (Expected type)

        Specifically:
                Type mismatch between
                        True
                and
                        not (Hanoi.Peg implementation of Prelude.Interfaces.Eq, method == from to)

关于tryMove 的递归调用。 如果我明确地传递{prf}，如

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber)
tryMove Z from to [] = Nothing
tryMove (S k) from to {prf} (smallestDiskPosition :: restOfTheDisposition) =
        map (smallestDiskPosition ::) (tryMove k from to {prf} restOfTheDisposition)

它编译正确。

为什么 Idris 不能在归纳步骤中自动检测证明，而在函数的正常调用中能够做到？

编辑：

这里有一个完整的使用要点：https://gist.github.com/marcosh/d51479ea08e8522560713fd1e5ca9624

Answer 1

您为 prf 提供默认值 (Oh)，因此 Idris 试图将 Oh 传递给递归调用。 Oh 的类型为 So True，Idris 预计 prf 的类型为 So (from /= to)，但由于您不破坏 to 和 from，Idris 无法知道 from /= to 的值，这就是为什么您查看该错误消息。

您可以更改签名以包含{auto prf: So (from /= to)} 或完全删除prf 参数，因为您实际上并没有使用它，您只需将其传递给递归调用而不做任何修改。