Agda中函数终止检查失败问题求助

我正在编写以下未完成的extend函数：

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 = ?

extend唯一的自递归调用在最后一个分支中：第一个显式参数o（自然数）被模式匹配为suc (suc o)，递归调用传入的第一个显式参数是suc o，严格小于匹配的参数。但Agda 2.6.4.1仍拒绝该定义，提示终止检查失败。我是否忽略了什么？这可能是一个bug吗？

抱歉未包含函数中使用的所有定义，数量太多。若要自行测试，可在项目的对应文件中找到该函数的稍作修改版本：其中递减参数（命名为l而非o）为隐式参数，extendAll被移至extend外部。

内容的提问来源于stack exchange，提问作者XiaohuWang