[Agda] Non-termination help!

[Martín]

Hello everyone. I am struggling with Agda's termination checker.

The idea is to define a recursive function like *size* over terms µ S 
for some signature S (definitions are bellow). I can destruct (t : µ S) 
to obtain some symbol and its 'arguments', such arguments should be 
smaller since µ S is strictly positive. Therefore, I should be able to 
recursively call size, right?.

Here is an example where I leave the holes to be filled. I have tried 
different approaches to help the termination checker such as views and 
sized types. Sized types fix these simple functions, but it complicates 
matters in further proofs.

Cheers,

Martín.

----

module Q where

open import Data.Vec
open import Data.Nat

open import Level renaming (zero to lzero ; suc to lsuc)

record Signature : Set (lsuc lzero) where
   constructor sig
   field
     σ : Set
     arity : σ -> ℕ

record Σ (Sig : Signature) (X : Set) : Set where
   constructor _,_
   field
     C : Signature.σ Sig
     as : Vec X (Signature.arity Sig C)

data µ (S : Signature) : Set where
   In : Σ S (µ S) -> µ S

size : {S : Signature} -> µ S -> ℕ
size (In (C , as)) = suc (sum (map {!size!} as))

size' : {S : Signature} -> µ S -> ℕ
size' {sig σ arity} (In (C , as)) with arity C
size' {sig σ arity} (In (C , [])) | zero = 0
size' {sig σ arity} (In (C , (x ∷ as))) | suc arC = suc (sum (map 
{!size'!} (x ∷ as) ))