inductive in macro: invalid `Name.append`, both arguments have macro scopes, consider using `eraseMacroScopes`

The code

macro "foo" x:ident : command =>
  `(inductive Foo where | baz | bar : Nat → Foo
    -- def f (x : Foo) := x matches .baz
    -- theorem $x:ident (x : Foo) : f x || x matches .bar := by simp [f, x.prop]
    )

foo testenum

produces a panic

Error: invalid Name.append, both arguments have macro scopes, consider using eraseMacroScopes
backtrace:
Error: invalid Name.append, both arguments have macro scopes, consider using eraseMacroScopes
backtrace:

and then as a follow up error

cannot define multiple constructors with the same name '[anonymous]'

The problem goes away if I remove the constructors from the inductive.

Context

This did not come up in practice, but when trying to debug the test failure of 793.lean while working on #8037, which I somehow broke. It seems that inductive inside a macro is not well supported anyways.

Versions

Lean 4.20.0-rc5

Impact

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

Start by reproducing the macro and inductive example in the issue, then compare it with the 793.lean test failure referenced in the context and the work from #8037. Done means the example no longer panics with invalid Name.append or reports duplicate anonymous constructors, with the relevant regression behavior covered by the existing test.