attribute [-simp] cannot be undone

[nomeata]

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.