Agda项目中嵌套隐藏`with`子句的模式匹配问题分析

问题背景

在Agda类型检查器的开发过程中，发现了一个与嵌套with子句相关的模式匹配问题。这个问题特别出现在使用隐藏参数（hidden arguments）的情况下，会导致类型检查器错误地处理模式匹配参数。

问题重现

考虑以下Agda代码示例：

open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

infixr 5 _∷_ _++_

_++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys

T : ∀ {A n} → Vec A n → Set
T [] = Nat
T (x ∷ xs) = Vec Nat 0

foo : ∀ {A} m n (xs : Vec A m) (ys : Vec A n) → T (xs ++ ys)
foo m n xs ys with {m + n} | xs ++ ys
foo m n xs ys | [] = 0
foo m n xs ys | z ∷ zs with {m + n} | xs ++ ys
foo m n xs ys | z ∷ zs | v ∷ vs = []

这段代码会被Agda拒绝，并显示错误信息："Too many arguments given in with-clause"。

技术分析

根本原因

问题的根源在于Agda类型检查器在处理嵌套with子句时，特别是当with子句包含隐藏参数时，对模式匹配参数的计算出现了错误。

具体来说，在类型检查器的实现中，当处理嵌套的with子句时，代码会计算父级子句的with表达式数量（包括隐藏的with表达式）。然后使用这个数量来分割当前with子句的模式参数。然而，由于这个数量包含了隐藏的with表达式，导致分割过早，从而错误地处理了模式匹配参数。

影响范围

这个问题主要影响以下场景：

1. 使用嵌套的with子句
2. 其中至少一个with子句包含隐藏参数（使用{}语法）
3. 模式匹配涉及多个参数

相关案例

另一个类似的案例展示了相同的问题：

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

postulate
  com : ∀ n m → n + m ≡ m + n

thm : ∀ a b c → a + (b + c) ≡ (c + b) + a
thm a b c with {b + c} | com b c
... | refl with c + b
... | cb with com a cb
... | p rewrite p = refl

这个例子同样会触发"Too many arguments given in with-clause"错误，并展示了类型检查器在处理重写规则时的类似问题。

解决方案

修复这个问题的正确方法是：

1. 在处理with子句的模式匹配时，只计算显式的with表达式数量
2. 确保隐藏的with表达式不会影响模式参数的分割逻辑
3. 在类型检查器中正确跟踪隐藏参数的位置信息

总结

这个bug揭示了Agda类型检查器在处理复杂模式匹配场景时的一个边界情况。它特别强调了在处理嵌套结构和隐藏参数组合时的潜在陷阱。对于Agda用户来说，了解这个限制可以帮助他们避免在编写涉及复杂模式匹配的代码时遇到类似问题。对于Agda开发者而言，这个案例提供了关于如何改进类型检查器处理模式匹配逻辑的重要见解。