Having trouble automatically showing function terminates

Stream: lean4

[Ben]

I have the following. The definition Expression.specialize is throwing fail to show termination ... using structural recursion

inductive Placeholder where
| x : Placeholder
| y : Placeholder
| z : Placeholder
deriving BEq

inductive Expression where
  | call (on: Expression) (arg: Expression) : Expression
  | function (param: Placeholder) (body: Expression) : Expression
  | unit (value: Placeholder) : Expression

def Expression.specialize (on: Expression) (arg: Placeholder × Expression) : Expression := match on with
| unit v => if v == arg.fst then arg.snd else unit v
| function p b => function p (b.specialize arg)
| call on arg2 =>
  let ons := on.specialize arg
  let args := arg2.specialize arg
  match ons with
  -- Offending statement
  | function p sb => sb.specialize (p, args)
  | on => Expression.call on args

Is there a example application where this infinitely recurses? Maybe just a fail of the automatic termination thing, if so is there a simple way to show it does terminate?

[Scott Morrison]

It's the sb.specialize call that is not obvious, and I think you should expect that to require a non-automatic proof.