Failing termination check with a with-abstraction

Question

I'm surprised to see the following function fail the termination check. y ∷ ys is structurally smaller than x ∷ y ∷ ys, isn't it?

open import Data.List using (List ; [] ; _∷_)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Nat.Properties using (<-cmp)

foo : List ℕ → ℕ
foo [] = 0
foo (x ∷ []) = 1
foo (x ∷ y ∷ ys) with <-cmp x y
... | _ = suc (foo (y ∷ ys))

Doing either (or both) of the following two things seems to make the termination checker see the light:

Removing the with-abstraction.
Changing the last clause to match with y ∷ ys instead of x ∷ y ∷ ys and recurse with ys instead of y ∷ ys. (And also changing <-cmp x y to <-cmp y y for a lack of xs.)

Now I am even more confused than I usually am and I'm wondering: What's going on, how does the with-abstraction (and its helper function) factor into all of this, and what do I do about it?

I've seen the other questions and answers concerning termination, but - unlike those more complicated cases - the case at hand seems to be about basic structural recursion, no?

Update

I just found an answer to the question, but if anybody would like to shed more light on what exactly is going on, e.g., how exactly the with-abstraction interferes with termination checking, then I'd be more than happy to accept that answer instead.

user_13595001 · Answer

Turns out that this is a known limitation of the termination checker since 2.6.1. See the Termination checking section in the change log for 2.6.1: https://github.com/agda/agda/blob/v2.6.1/CHANGELOG.md

The pattern match and the recursive call won't work with a with-abstraction between them. A workaround is to also abstract over the recursive call in order to pull it up into the with-abstraction (from its original location after the with-abstraction).

open import Data.List using (List ; [] ; _∷_)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Nat.Properties using (<-cmp)

foo : List ℕ → ℕ
foo [] = 0
foo (x ∷ []) = 1
foo (x ∷ y ∷ ys) with foo (y ∷ ys) | <-cmp x y
... | rec | _ = suc rec

In the above code, the pattern match x ∷ y ∷ ys and the recursive call foo (y ∷ ys) don't straddle the with-abstraction any longer and the termination check succeeds.

The above fixes my issue, but the change log describes more delicate cases that require a little more care.

This issue is tracked in Agda issue #59 (!), which contains more details and a history of the problem: https://github.com/agda/agda/issues/59

Failing termination check with a with-abstraction

1 Answers