Termination checking of a function fails in Agda

Question

I'm currently writing the following incomplete function for this project:

  extend : ∀ o asc (s : CSet (suc k) o) → SC asc → SC (add s asc)
  extend 0 asc s rewrite l≡0 s Eq.refl =
    restrict (add (empty _) asc) asc (add-∈ asc (empty∈asc asc))
  extend 1 asc s = restrict (add s asc) asc (add-∈ asc (asc .hasAllPoints s))
  extend {k} (suc (suc o)) asc s with has asc (_ , s) in eq
  ... | true = restrict (add s asc) asc (add-∈ asc (pser T eq tt))
  ... | false = result
    module Extend where      
      extendAll : ∀ bsc (ss : Fin m → CSet (suc k) (suc o)) → SC bsc → SC (addAll ss bsc)
      extendAll {zero} _ _ sc = sc
      extendAll {suc _} bsc ss sc =
        let head-ss = ss zero
            tail-ss i = ss (suc i)
        in extendAll (add head-ss bsc) tail-ss (extend (suc o) bsc head-ss sc)

      faces : SC asc → SC (addAll (except s) asc)
      faces = extendAll asc (except s)

      cycl : SC asc → Cycle P o
      cycl sc .face i = faces sc .for (∈-addAll (except s) asc i)
      cycl sc .compatible i j =
        P.proj (punchIn i) (cycl sc .face j) ≈˘⟨ P.map-cong (embed-except (except s j) Eq.refl _) _ ⟩
        P.proj (embed (except⊂s (except s j) i)) (cycl sc .face j) ≡⟨⟩
        P.proj (embed (except⊂s (except s j) i)) (faces sc .for (∈-addAll (except s) asc j)) ≈˘⟨ faces sc .compat (∈-addAll (except s) asc _) _ ⟩
        faces sc .for (Has-⊆ (addAll (except s) asc) (except⊂s (except s j) i) (∈-addAll (except s) asc j)) ≡˘⟨ for-resp (faces sc) _ _ ⟩
        faces sc .for (resp (_∈ addAll (except s) asc) (except-except s Eq.refl j i) (Has-⊆ (addAll (except s) asc) (except⊂s (except s j) i) (∈-addAll (except s) asc j))) ≡⟨ faces sc .for =$= T-irrel ⟩
        faces sc .for (Has-⊆ (addAll (except s) asc) (except⊂s (except s (punchIn j i)) (pinch i j)) (∈-addAll (except s) asc (punchIn j i))) ≈⟨ faces sc .compat _ _ ⟩
        P.proj (embed (except⊂s (except s (punchIn j i)) (pinch i j))) (faces sc  .for (∈-addAll (except s) asc (punchIn j i))) ≡⟨⟩
        P.proj (embed (except⊂s (except s (punchIn j i)) (pinch i j))) (cycl sc .face (punchIn j i)) ≈⟨ P.map-cong (embed-except (except s (punchIn j i)) Eq.refl _) _ ⟩
        P.proj (punchIn (pinch i j)) (cycl sc .face (punchIn j i)) ∎
        where open Relation.Reasoning (P._≃_)
              open Equiv (refl (P.Space _)) (trig (P.Space _))

      result : SC asc → SC (add s asc)
      result sc .for {s = t} t∈added with add-⊂ {s = t} {s} {asc} t∈added
      ... | inj₂ t∈asc = sc .for t∈asc
      ... | inj₁ t⊂s with ⊂-except t⊂s Eq.refl
      ... | inj₂ (i , t⊂except) = faces sc .for (Has-⊆ (addAll (except s) asc) t⊂except (∈-addAll (except s) asc i))
      ... | inj₁ (Eq.refl , Eq.refl) = ?
      result sc .compat = ?

As we can see, the only recursive call of extend to itself is in the final branch, where the first explicit argument o (which is a natural number) is pattern matched against suc (suc o), and the recursive call itself passes suc o as the first explicit argument, so it is strictly smaller than the one pattern matched against.

Yet, Agda 2.6.4.1 rejects this definition and complains about failed termination checking. Am I missing something here or is this possibly a bug?

Btw, sorry for not including all the definitions used in this function, as there are simply too many. If you want to experiment with it yourself, a slightly modified version of this function can be found in the aforementioned project under here, where the decreasing argument (named l there instead of o) is implicit instead of explicit (as originally intended), and extendAll is moved outside of extend.

Answer 1

I have no idea whether this will help, and in any case your code fragment is much too complicated for me to think about digging into the details... but what happens if you change the pattern suc (suc o), with subsequent use of suc o below, instead to suc o@(suc _), and all subsequent occurrences of suc o now simply to o itself?

As far as I can tell, you make no use of the additional sub-term o of suc (suc o) in any call, so use of the @-pattern would both be more precise, and simplify the subsequent code. One might hope...

... but having said that, the termination checker is notoriously sensitive to recursive calls in the scope of an intermediate with, and that may be the real reason for your troubles. Is such behaviour a 'bug'? Surely not, except that we might hope for better. The 'usual' solution here is to write the auxiliary function by hand, mutually with the main one, but in your case, that looks... challenging!

Mind you, the with concerned is doing case analysis on a boolean... which for me at least, falls under the code smell of 'redundant uses of with', so I would consider refactoring to avoid that... which again in your case, would also involve refactoring away the use of the equation eq, but equations of the form b ≡ true etc. aren't really working hard enough to earn their place to begin with, are they?

Answer 2

So, I have solved my problem and I think I'd shared the things I've tried in case it helps others:

1. I replaced the pattern suc (suc o) with suc o@(suc _) and every occurrence of suc o with o as James McKinna suggested. Didn't work.
2. I removed the unnecessary with-abstractions as James McKinna pointed out. It made my code cleaner but still didn't solve the problem.
3. I moved everything in the named where-block into a separate module (also called Extend), mutually recursive with the extend function. So now instead of having just one recursive definition that calls itself in the where-clause, I had 4 mutually dependent definitions. Didn't work.
4. I added an additional parameter to the now separate module Extend that receives the recursive call to extend, such that the extend function, having neither with-abstractions nor where-blocks at this point, would pass a recursive call to itself to the Extend module directly in the RHS. This finally worked.

So, I guess the conclusion is perhaps that Agda's termination checker can't deal with four mutually recursive definitions?