我不能告诉你发生这种情况的确切原因，但我可以告诉你如何治愈这些症状。在我开始之前：这是终止检查器的一个已知问题。如果您精通 Haskell，可以查看源代码。
一种可能的解决方案是将函数分成两个：第一个用于第一个参数变小的情况，第二个用于第二个：
mutual
merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes _ = x ∷ merge xs (y ∷ ys)
... | no _ = y ∷ merge′ x xs ys
merge xs ys = xs ++ ys
merge′ : ℕ → List ℕ → List ℕ → List ℕ
merge′ x xs (y ∷ ys) with x ≤? y
... | yes _ = x ∷ merge xs (y ∷ ys)
... | no _ = y ∷ merge′ x xs ys
merge′ x xs [] = x ∷ xs
所以，第一个函数xs会砍掉，一旦我们必须砍掉ys，我们就切换到第二个函数，反之亦然。
问题报告中也提到的另一个（可能令人惊讶的）选项是通过以下方式引入递归结果with：
merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y | merge xs (y ∷ ys) | merge (x ∷ xs) ys
... | yes _ | r | _ = x ∷ r
... | no _ | _ | r = y ∷ r
merge xs ys = xs ++ ys
最后，我们可以对 tors 执行递归Vec，然后转换回List：
open import Data.Vec as V
using (Vec; []; _∷_)
merge : List ℕ → List ℕ → List ℕ
merge xs ys = V.toList (go (V.fromList xs) (V.fromList ys))
where
go : ∀ {n m} → Vec ℕ n → Vec ℕ m → Vec ℕ (n + m)
go {suc n} {suc m} (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes _ = x ∷ go xs (y ∷ ys)
... | no _ rewrite lem n m = y ∷ go (x ∷ xs) ys
go xs ys = xs V.++ ys
但是，这里我们需要一个简单的引理：
open import Relation.Binary.PropositionalEquality
lem : ∀ n m → n + suc m ≡ suc (n + m)
lem zero m = refl
lem (suc n) m rewrite lem n m = refl
我们也可以直接go返回List并完全避免引理：
merge : List ℕ → List ℕ → List ℕ
merge xs ys = go (V.fromList xs) (V.fromList ys)
where
go : ∀ {n m} → Vec ℕ n → Vec ℕ m → List ℕ
go (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes _ = x ∷ go xs (y ∷ ys)
... | no _ = y ∷ go (x ∷ xs) ys
go xs ys = V.toList xs ++ V.toList ys
第一个技巧（即将函数拆分为几个相互递归的函数）实际上非常好记。由于终止检查器不会查看您使用的其他函数的定义，因此它会拒绝大量完美的程序，请考虑：
data Rose {a} (A : Set a) : Set a where
[] : Rose A
node : A → List (Rose A) → Rose A
现在，我们要实现mapRose：
mapRose : ∀ {a b} {A : Set a} {B : Set b} →
(A → B) → Rose A → Rose B
mapRose f [] = []
mapRose f (node t ts) = node (f t) (map (mapRose f) ts)
然而，终止检查器不会查看内部map以查看它是否没有对元素做任何时髦的事情，而只是拒绝这个定义。我们必须内联定义map并编写一对相互递归的函数：
mutual
mapRose : ∀ {a b} {A : Set a} {B : Set b} →
(A → B) → Rose A → Rose B
mapRose f [] = []
mapRose f (node t ts) = node (f t) (mapRose′ f ts)
mapRose′ : ∀ {a b} {A : Set a} {B : Set b} →
(A → B) → List (Rose A) → List (Rose B)
mapRose′ f [] = []
mapRose′ f (t ∷ ts) = mapRose f t ∷ mapRose′ f ts
where通常，您可以在声明中隐藏大部分混乱：
mapRose : ∀ {a b} {A : Set a} {B : Set b} →
(A → B) → Rose A → Rose B
mapRose {A = A} {B = B} f = go
where
go : Rose A → Rose B
go-list : List (Rose A) → List (Rose B)
go [] = []
go (node t ts) = node (f t) (go-list ts)
go-list [] = []
go-list (t ∷ ts) = go t ∷ go-list ts
注意：可以在定义两个函数之前声明它们的签名，而不是mutual在较新版本的 Agda 中使用。
更新：Agda 的开发版本对终止检查器进行了更新，我将让提交消息和发布说明自己说话：
- 可以处理任意终止深度的调用图完成的修订。这个算法在 MiniAgda 中已经存在了一段时间，等待它的伟大的一天。现在就在这里！选项 --termination-depth 现在可以停用。
从发行说明中：
'with' 定义的函数的终止检查已得到改进。
以前需要 --termination-depth（现在已过时！）通过终止检查器（由于使用 'with'）的情况不再
需要该标志。例如
merge : List A → List A → List A
merge [] ys = ys
merge xs [] = xs
merge (x ∷ xs) (y ∷ ys) with x ≤ y
merge (x ∷ xs) (y ∷ ys) | false = y ∷ merge (x ∷ xs) ys
merge (x ∷ xs) (y ∷ ys) | true = x ∷ merge xs (y ∷ ys)
这之前未能终止检查，因为“with”扩展为辅助函数 merge-aux：
merge-aux x y xs ys false = y ∷ merge (x ∷ xs) ys
merge-aux x y xs ys true = x ∷ merge xs (y ∷ ys)
此函数调用合并，其中一个参数的大小正在增加。为了使它通过，终止检查器现在在检查之前内联合并辅助的定义，从而有效地终止检查原始源程序。
由于这种转换，对变量执行“with”不再保留终止。例如，这不会终止检查：
bad : Nat → Nat
bad n with n
... | zero = zero
... | suc m = bad m
事实上，您的原始函数现在通过了终止检查！