Declaration `...` must be marked as `meta` error when adding an existing simproc to a custom simp attribute

Description

Adding an existing simproc to a custom simp attribute causes an error "Declaration ... must be marked as meta".

Context

See the discussion on Zulip: #general > How to add simproc to custom simp attribute? @ 💬

Steps to Reproduce

When I try to do

attribute [my_simp] reduceCtorEq

I get the error

error: Cannot add attribute `[my_simp_proc]`: Declaration `reduceCtorEq` must be marked as `meta`

even if I do

public meta import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

I found the following as a workaround, but this seems quite hacky:

simproc [my_simp] reduceCtorEq_copy (_ = _) := reduceCtorEq

Here is a #mwe that does not work on the playground since it needs multiple files:

module

public import Lean
public meta import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

register_simp_attr my_simp

-- in different file:
-- error: Cannot add attribute `[my_simp_proc]`: Declaration `reduceCtorEq` must be marked as `meta`
attribute [my_simp] reduceCtorEq

-- hacky workaround:
simproc [my_simp] reduceCtorEq_copy (_ = _) := reduceCtorEq

Expected behavior: attribute [my_simp] reduceCtorEq succeeds

Actual behavior: attribute [my_simp] reduceCtorEq causes "Declaration reduceCtorEq must be marked as meta"

Impact

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

Start with the multi-file reproducer using register_simp_attr my_simp and attribute [my_simp] reduceCtorEq, then inspect the behavior around Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core. Compare it with the simproc workaround. Done means the direct attribute command succeeds without requiring a copied simproc or producing the meta declaration error.