Agda中通过函数返回构造器类型报错的问题咨询

问题代码 #

尝试自定义对应List Set的Tuple类型，编写的代码如下：

open import Agda.Builtin.List

mutual
  f : List Set -> Set
  f T = g T T where
    g : List Set -> List Set -> Set
    g [] T = Tuple T
    g (t ∷ rest) T = t -> g rest T

  data Tuple (A : List Set) : Set where
    MkTPL : f A

报错信息 #

Agda编译器持续报错：

The target of a constructor must be the datatype applied to its
parameters, playground.g A A A isn't
when checking the constructor MkTPL in the declaration of Tuple

错误原因与解决方法 #

核心问题 #

构造器的类型必须最终指向Tuple A，但你的代码通过mutual块+局部g函数形成循环依赖，导致Agda无法正确推断f A的最终目标类型是Tuple A；同时局部where子句中的g函数在mutual上下文里的类型解析出现混淆。

正确写法 #

可以通过独立辅助函数生成构造器所需的函数类型，彻底避免循环依赖：

open import Agda.Builtin.List

-- 辅助函数：生成从元素到目标类型的嵌套函数类型
TupleArgs : List Set -> Set -> Set
TupleArgs [] T = T
TupleArgs (t ∷ ts) T = t -> TupleArgs ts T

data Tuple (A : List Set) : Set where
  MkTPL : TupleArgs A (Tuple A)

这个写法的逻辑：

• 当A为空列表时，TupleArgs [] (Tuple []) = Tuple []，构造器MkTPL直接对应空Tuple；
• 当A为[t₁, t₂, ..., tₙ]时，TupleArgs A (Tuple A)会展开为t₁ → t₂ → ... → tₙ → Tuple A，完全符合依赖Tuple的构造需求。

关于报错信息中g A A A的疑问 #

报错里出现g A A A是循环依赖下的类型推断混乱导致的：
你的g函数仅接受两个List Set参数，但Agda在解析g T T时，错误地将Tuple的参数A也混入了g的参数列表，导致出现三个参数的非法应用。将g从where子句移出或改用独立辅助函数即可避免这类问题。

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