[Agda] Induction when the argument is wrapped in a constructor?

[Shin-Cheng Mu]

Hi,

Why does this function not pass the termination check,
and is there a work around?

The function f, defined below, is defined inductively
on its input, in principle. The twist is that I would
like to wrap the list in a type constructor Wrap, carrying
some extra information about the list in the type:

   data Wrap : ℕ -> Set where
     W : (xs : [ ℕ ]) -> (bnd : ℕ) -> Wrap bnd

   lemma : ℕ -> ℕ
   lemma = {! !}    -- definition not relevant and omitted

The following (simplified) function f merely returns 0.

   f : forall {i} -> Wrap i -> ℕ
   f {i} (W [] .i) = 0
   f {i} (W (x ∷ xs) .i) with lemma i
   ... | j with f {j} (W xs j)
   ...        | _ = 0

When the argument is x ∷ xs, one recursive call is made
on xs and j, some information computed from i. Although
the argument of f does reduce (from x ∷ xs to xs), Agda
cannot determine its termination. Is it because xs is
wrapped in W?

Is there a work around?

ps. To Nils Anders: if you remember, it is related to
what we discussed a while ago. The function f is what
I would like to use in an unfold. The argument i carries
some size information of xs. In general I would like to
write f of, for example, this type:

    f : forall {i} -> Wrap (suc i) -> ⊤ ⊎ (ℕ × Wrap i)

I ran into trouble when f is defined inductively.

sincerely,
Shin