Idris 中的奇怪错误消息答案

【问题标题】：Strange error message in IdrisIdris 中的奇怪错误消息
【发布时间】：2015-11-11 19:47:11
【问题描述】：

我正在 Idris 中实现 first-order unification by structural recursion 的算法和证明（开发的当前状态可用 here）。

Idris 给了我以下错误信息

`-- UnifyProofs.idr line 130 col 60:
   When checking right hand side of maxEquiv with expected type
           (Max p n f -> Max q n f, Max q n f -> Max p n f)

   When checking argument b to constructor Builtins.MkPair:
           No such variable k

当它尝试键入时检查以下函数

maxEquiv : p .=. q -> Max p .=. Max q 
maxEquiv pr n f = ( \ a => ( fst (pr n f) (fst a) 
                          , \ n1 => \ g => \pr1 => (snd a) n1 g 
                                                   (snd (pr n1 g) pr1))
                  , \ a' => (snd (pr n f) (fst a') 
                          , \ n2 => \ g' => \ pr2 => (snd a') n2 g' 
                                                     (fst (pr n2 g') pr2)))

其中 Max 和 .=。被定义为

Property : (m : Nat) -> Type
Property m = (n : Nat) -> (Fin m -> Term n) -> Type

infix 5 .=.
(.=.) : Property m -> Property m -> Type
(.=.) {m = m} P Q = (n : Nat) -> (f : Fin m -> Term n) -> 
                                 Pair (P n f -> Q n f) 
                                      (Q n f -> P n f)

Max : (p : Property m) -> Property m
Max {m = m} p = \n => \f => (p n f , (k : Nat) -> (f' : Fin m -> Term k) -> 
                                                   p k f' -> f' .< f)

我已尝试显式传递所有函数参数，以避免隐式参数推断出现问题。但错误仍然存在。有人可以给我一些关于如何解决这个问题的提示吗？

【问题讨论】：

能否也包括.<的定义？

标签： dependent-type idris

【解决方案1】：

这是我的问题的解决方案：

Max : (p : Property m) -> Property m
Max {m = m} p = \n => \f => (p n f , (k : Nat) -> (f' : Fin m -> Term k) -> p k f' -> f' .< f)

applySnd : Max {m = m} p n f -> (k : Nat) -> (f' : Fin m -> Term k) -> p k f' -> f' .< f
applySnd = snd

maxEquiv : p .=. q -> Max p .=. Max q 
maxEquiv pr n f = ( \ a => ( fst (pr n f) (fst a) 
                       , \ n1 => \ g => \pr1 => (applySnd a) n1 g (snd (pr n1 g) pr1))
              , \ a' => (snd (pr n f) (fst a
                        , \ n2 => \ g' => \ pr2 => (applySnd a') n2 g' (fst (pr n2 g') pr2)))

我刚刚使用了一个函数 applySnd 来制作与 snd 相同的东西。我不知道为什么这是必要的......可能是一个 Idris 错误......

【讨论】：