maximum recursion depth

Stream: lean4

[Marcus Rossel]

I'm hitting a maximum recursion depth has been reached error in a scenario where I don't understand it.
The following example is reduced, so it might look a bit strange:

inductive Term
  | bool (b : Bool)
  | nat (n : Nat)
  | ite (cond pos neg : Term)

def eval₁ (t : Term) : Option Term :=
  match t with
  | bool _ => t
  | nat _ => t
  | ite .. => t

def evalₙ (t : Term) : Option Term :=
  match h : t.eval₁ with
  | none => none
  | some (.bool b) => some (.bool b)
  | some (.nat n) => some (.nat n)
  | some (.ite cond pos neg) => evalₙ (.ite cond pos neg)
termination_by evalₙ t => t
decreasing_by sorry

I'm aware that evalₙ doesn't actually terminate, and this might be related to the issue.
The error arises on the last simp in:

theorem same_evaluation : evalₙ = evalₙ := by
  apply funext ?_
  intro t
  induction t
  case bool b =>
    simp [evalₙ]

I have no idea how simp works, but as far as I can tell, unfolding/reducing the definitions of evalₙ and eval₁ should simply yield some (.bool b) in this case. So I don't understand where the recursion is coming from.

Interestingly, rewriting evalₙ as:

def evalₙ (t : Term) : Option Term :=
  match h : some t with
  ...

fixes the problem.