`private` and `protected` interact strangely

import Lean
open Lean
macro "test" x:ident : command => do
  let [(name, _)] ← Macro.resolveGlobalName x.getId | Macro.throwUnsupported
  `(protected theorem $(mkIdent (name.mkStr "ext")):ident : True := trivial)

inductive A : Type
test A
#print A.ext -- ok

private inductive B : Type
test B 
-- invalid scope
-- protected declarations must be in a namespace
-- invalid 'end', insufficient scopes
#print B.ext -- fail

namespace Ns
private inductive C : Type
test C 
-- invalid scope
-- invalid 'end', insufficient scopes
#print C.ext -- fail, but...
#print Ns.ext -- ok

This is a simplified version of an issue with the ext attribute from mathlib, which attempts to create a protected declaration in the same namespace as the input type name. (It would also be nice to implement this as a macro; I think I know how to work around this as an elab.) When the type is private, this essentially amounts to elaborating a command like:

protected theorem _private.Test.0.B.ext : True := trivial

and the declaration parser gets very confused by this identifier. Ideally, this would just work and create a private declaration which is also protected, in the sense that you can refer to it by the name B.ext but not ext. I believe the knock-on error about invalid scope is because the declaration elaborator expanded to a namespace 0 which isn't valid.