failed to generate equality theorems when using @[simp]

Stream: lean4

[Paul Mure]

Here's an example:

inductive Ty
  | bv : Nat → Ty

@[reducible]
def Ty.denote : Ty → Type
  | bv w => BitVec w

inductive BinOp : Ty → Ty → Ty → Type
  | add : {w : Nat} → BinOp (.bv w) (.bv w) (.bv w)
  | eq : BinOp α α (.bv 1)

@[simp]
def BinOp.eval : BinOp α β γ → (α.denote → β.denote → γ.denote)
  | add => BitVec.add
  | eq => λ a b => if a == b then ⟨1⟩ else ⟨0⟩

example : ∀α x y (op : BinOp α α α), op.eval x y = op.eval x y := by
  simp

This fails unless I remove the @[simp] from BinOp.eval.