strange deep recursion error when using `rw` with `match`

Stream: lean4

[Devon Tuma]

Working with BitVec and EStateM, I've come across a very strange error that I cannot figure out the reason for. In particular using certain lemmas with rw causes "(kernel) deep recursion detected" issues that only happen in very specific cases. This is the best MWE I could come up with:

import Init.Data.BitVec

variable {ε σ α β : Type}

theorem EStateM.run_bind (x : EStateM ε σ α) (f : α → EStateM ε σ β) (s : σ) :
    (x >>= f).run s = match x.run s with
    | .ok a s => (f a).run s
    | .error e s => .error e s := rfl

theorem EStateM.run_bind' (x : EStateM ε σ α) (f : α → EStateM ε σ β) (s : σ) :
    (x >>= f).run s = (x.run s).rec (fun a s => (f a).run s) (fun e s => .error e s) := by
  show (match x.run s with
    | .ok a s => (f a).run s
    | .error e s => .error e s) = _
  cases x.run s <;> rfl

theorem EStateM.run_pure (x : α) :
    (pure x : EStateM ε σ α).run s = EStateM.Result.ok x s := rfl

example (n : Fin _) (s : Unit) :
    EStateM.run (do
      let _ ←
        (match
          (match ((BitVec.ofNat 1 (n * 30292 : Fin 30293)))[0]'Nat.one_pos with
          | true => true
          | false => true) with
        | true => pure ()
        | false => pure () : EStateM Unit Unit Unit)
      return ()) s = EStateM.Result.ok () s := by
  rw [EStateM.run_bind] -- (kernel) deep recursion detected
  -- rw [EStateM.run_bind'] -- no errors
  -- simp [EStateM.run_bind] -- no errors

  cases (BitVec.ofNat 1 (n * _).val)[0]
  · simp only [EStateM.run_pure]
  · simp only [EStateM.run_pure]

My first thought was that maybe lemma statements that contain match expressions are not meant to be supported, but the conditions to reproduce this are actually very specific. For example even changing 30292 to 30291 will solve the problem. And so will changing the match expressions in the example statement to have a single default case instead of two specific cases.