Agda循环索引函数编译报错`.A !=< .A₁ of type Set`原因咨询

首先，你的错误根源在于辅助函数go重复声明了隐式参数{A : Set}，导致它和外部roundIndex的A成为了两个完全独立的类型参数，Agda无法统一这两个不同的A实例，从而抛出类型不兼容的错误。

错误原因详解 #

你在where块里定义的go函数自己加了{A : Set}隐式参数，这意味着每次调用go时，Agda都会重新推断一个全新的A类型。比如在go (suc n) [] = go n xs这一行：

• 左边的go对应的隐式参数是.A₁（Agda自动生成的名称）
• 右边调用go时传入的xs是外部roundIndex参数里的xs，它的类型是List A（外部的A）
  此时Agda发现.A（外部）和.A₁（go自己的）无法统一，于是抛出了.A !=< .A₁的错误。

!=<符号的含义 #

这个符号是Agda的类型检查错误提示，翻译过来就是：左边的类型不能被当作右边类型的子类型（或兼容类型）。简单说就是两个类型完全不匹配，无法统一。在这里，Agda期望得到.A₁类型的值，但你提供的是.A类型的值，两者是不同的隐式参数实例，自然无法兼容。

修正后的代码 #

解决方法很简单：让go继承外部roundIndex的隐式A参数，不要自己声明。另外，原代码里go的参数x和外部的x重名，容易混淆，我改成了y：

module Test where
open import Prelude.Nat
open import Prelude.List

roundIndex : {A : Set} -> Nat -> A -> List A -> A
roundIndex n x xs = go n xs
  where
    -- 去掉独立的隐式参数，直接使用外部的A
    go : Nat -> List A -> A
    go (suc n) (y ∷ ys) = go n ys
    go (suc n) [] = go n xs  -- 现在xs的类型List A和go的List A完全匹配
    go zero (y ∷ ys) = y
    go zero [] = x  -- x的类型A也和返回类型匹配

这样修改后，所有的类型参数都统一为外部的A，Agda就能正确推断类型，编译通过了。

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