Can't use `attribute [semireducible]` on well-founded definitions.

Description

While we can make a well-founded definition (which is irreducible by default) semireducible using @[semireducible], we can't make it semireducible with attribute [semireducible], even immediately afterwards.

Steps to Reproduce

abbrev F (α : Type _) := (Nat → α) → α

inductive Circuit (α : Type _) (γ : List (F α))
| input : Nat → Circuit α γ
| gate : (g : F α) → (_ : g ∈ γ) → List (Circuit α γ) → Circuit α γ

namespace Circuit

variable {α : Type _} [Inhabited α] {γ : List (F α)}

-- @[semireducible] -- This works!
def eval (c : Circuit α γ) (input : Nat → α) : α :=
  match c with
  | .input n => input n
  | .gate g _ cs => g fun n => match h : cs[n]? with
    | some c =>
      have : c ∈ cs := List.getElem?_mem h
      eval c input
    | none => default

attribute [semireducible] eval -- But this doesn't. Fails with:
-- failed to set `[semireducible]` for `Circuit.eval`, declarations are `[semireducible]` by default

end Circuit

Impact

Relatively minor. I wouldn't even mind if it was still disallowed, but with an actionable error message.

Start by running the reproducer for Circuit.eval and compare the inline @[semireducible] declaration with the later attribute [semireducible] command. Trace the handling of the semireducible attribute for well-founded definitions. Done means the command works consistently or reports an actionable error explaining why it is disallowed.