Idris 中的奇怪错误消息

Question

我正在 Idris 中实现 first-order unification by structural recursion (current status of the development available 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)

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

Answer 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 错误...

Idris 中的奇怪错误消息

Strange error message in Idris

dependent-type

idris