I cannot give you a reason why this is happening, but I can show you how to cure the symptoms. Before you begin: this is a known issue using completion checking. If you are good at Haskell, you can take a look at the source.
One of the possible solutions is to divide the function into two: first, for the case when the first argument becomes smaller, and the second for the second:
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
So, the first function discards xs , and as soon as we have to split ys , we switch to the second function and vice versa.
Another (possibly unexpected) option, which is also mentioned in the release report, is to present the result of the recursion through 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
And finally, we can recurs to Vec tors and then convert back to 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 : ∀ {nm} → 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 nm = y ∷ go (x ∷ xs) ys go xs ys = xs V.++ ys
However, here we need a simple lemma:
open import Relation.Binary.PropositionalEquality lem : ∀ nm → n + suc m ≡ suc (n + m) lem zero m = refl lem (suc n) m rewrite lem nm = refl
We could also have a go return List directly and avoid the lemma altogether:
merge : List ℕ → List ℕ → List ℕ merge xs ys = go (V.fromList xs) (V.fromList ys) where go : ∀ {nm} → 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
The first trick (i.e., dividing a function into several mutually recursive ones) is actually nice to remember. Since checking completion does not find the definition of other functions that you use, it rejects many great programs, consider:
data Rose {a} (A : Set a) : Set a where [] : Rose A node : A → List (Rose A) → Rose A
And now we would like to implement mapRose :
mapRose : ∀ {ab} {A : Set a} {B : Set b} → (A → B) → Rose A → Rose B mapRose f [] = [] mapRose f (node t ts) = node (ft) (map (mapRose f) ts)
The completion controller, however, does not look inside the map to make sure that it does not do anything funky with the elements and simply rejects this definition. We need to establish a map definition and write a couple of mutually recursive functions:
mutual mapRose : ∀ {ab} {A : Set a} {B : Set b} → (A → B) → Rose A → Rose B mapRose f [] = [] mapRose f (node t ts) = node (ft) (mapRose′ f ts) mapRose′ : ∀ {ab} {A : Set a} {B : Set b} → (A → B) → List (Rose A) → List (Rose B) mapRose′ f [] = [] mapRose′ f (t ∷ ts) = mapRose ft ∷ mapRose′ f ts
You can usually hide most of the clutter in a where declaration:
mapRose : ∀ {ab} {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 (ft) (go-list ts) go-list [] = [] go-list (t ∷ ts) = go t ∷ go-list ts
Note. Declaring signatures of both functions before defining them can be used instead of mutual in new versions of Agda.
Update: The development version of Agda has received an update to verify the end of the session, I will let the message and commit messages speak for themselves:
- Revision of the completion of the call graph, which may deal with arbitrary completion depths. This algorithm sat for a while in MiniAgda, waiting for its great day. It is now! Now the -termination-depth option can be removed.
And from the release notes:
Improved verification of the completion of functions defined with "c".
Cases that previously required - depth-depth (now obsolete!) To pass the completion check (due to the use of "c") no longer need a flag. for instance
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)
This failed to complete the check earlier, since 'with' expands to the helper function merge-aux:
merge-aux xy xs ys false = y ∷ merge (x ∷ xs) ys merge-aux xy xs ys true = x ∷ merge xs (y ∷ ys)
This function makes a merge call in which the size of one of the arguments grows. To do this, complete the completion check now inserts the definition of merge-aux before checking, thus effectively completing the verification of the original source program.
As a result of this conversion doing “c” on the variable no, longer storage is terminated. For example, this is not a completion check:
bad : Nat → Nat bad n with n ... | zero = zero ... | suc m = bad m
Indeed, your original function now passes the completion check!