[Agda] Termination checking with partiality monad

[Brandon Moore]

I don't understand why the following code doesn't pass the termination checker.
Each case of "app" is headed by a constructor, and "eval" only makes
recursive calls on structurally smaller arguments.


module test where
open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Coinduction

data Exp (scope : ℕ) : Set where
  var : Fin scope → Exp scope
  _$_ : Exp scope → Exp scope → Exp scope
  lam : Exp (suc scope) → Exp scope

data Val : Set where
  Closure : {scope : ℕ} → Vec Val scope → Exp (suc scope) → Val

data Trace : Set where
  Call : ∞ Trace → Trace
  Fail : Trace
  Ret : Val → Trace

mutual
  app : Trace → Trace → Trace
  app (Call f) a = Call (♯ (app (♭ f) a))
  app f (Call a) = Call (♯ (app f (♭ a)))
  app Fail _ = Fail
  app _ Fail = Fail
  app (Ret (Closure env body)) (Ret val) = Call (♯ (eval (val ∷ env) body))

  eval : {scope : ℕ} → Vec Val scope → Exp scope → Trace
  eval env (var v) = Ret (lookup v env)
  eval env (f $ a) = app (eval env f) (eval env a)
  eval env (lam body) = Ret (Closure env body)