attribute [-simp] cannot be undone

This seems like a bug, and not a feature: Once a theorem is attribute [-simp] a_eq_b’ed, it cannot be made [simp] again:

axiom a : Nat
axiom b : Nat
axiom a_eq_b : a = b

axiom P : Nat → Nat → Prop
@[simp] axiom P_b : P b b

/-- error: simp made no progress -/
#guard_msgs in example : P a b := by simp

attribute [simp] a_eq_b

example : P a b := by simp

attribute [-simp] a_eq_b

/-- error: simp made no progress -/
#guard_msgs in example : P a b := by simp

attribute [simp] a_eq_b
/-- error: simp made no progress -/
#guard_msgs in example : P a b := by simp

I stumbled over this while testing changes for #5828.

I wonder how complicated it will be to describe the intended semantics of these attributes, also with regard to local and scoped. But it seems that one cannot even use local and scoped with [-simp]?

Versions

Lean 4.12.0-nightly-2024-10-28
Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the attribute [simp], attribute [-simp], and #guard_msgs reproducer from the issue on the stated Lean nightly version. Trace how simp attributes are registered and removed, then verify that re-adding a_eq_b restores the original proof and clarify expected behavior for local and scoped attributes.