[Agda] Compositional termination

[Karn Kallio]

My first encounter with noncompositional termination was while writing some 
parser combinators while threading a termination counter so as to escape from
proof obligations.  Looking at the resulting definitions along the lines of

loop₁ : Char → ℕ → Maybe Char
loop₁ x zero    = nothing
loop₁ x (suc n) = loop₁ x n

zig : Char → ℕ → Maybe Char
zag : Char → ℕ → Maybe Char

zig x zero    = nothing
zig x (suc n) = zag x n

zag x zero    = nothing
zag x (suc n) = zig x n

I wanted to have a termination counter weak or quasi monad (the left and right 
unit laws fail, so not a monad)

M : Set → Set
M A = ℕ → Maybe A

q-return : ∀ {A} → A → M A
q-return x = λ n → just x

_q->>=_ : ∀ {A B} → M A → (A → M B) → M B
_q->>=_ m f zero    = nothing
_q->>=_ m f (suc n) = m n >>= λ x → f x n
  where open RawMonad monad

But then the termination checker does not "see through" applications of 
quasibind, so [loop] below does not terminate:

loop : Char → M Char
loop x = q-return x q->>= loop

so I was stuck with expanding out quasibind manually.