fix: resolve _root_ in macro, syntax, elab

src/Lean/Elab/ElabRules.lean

@@ -97,7 +97,11 @@ def elabElab : CommandElab
       | some name => pure name.getId
       | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)) attrKind
     let nameId := name?.getD (mkIdentFrom tk name (canonical := true))
-    let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
+    let stxNodeKind := if (`_root_).isPrefixOf name then
+      name.replacePrefix `_root_ Name.anonymous
+    else
+      (← getCurrNamespace) ++ name
+    let pat := ⟨mkNode stxNodeKind patArgs⟩
     elabCommand <|← `(
       $[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
       syntax%$tk$[:$prec?]? (name := $nameId) (priority := $(quote prio):num) $[$stxParts]* : $cat

src/Lean/Elab/Macro.lean

@@ -23,7 +23,11 @@ open Lean.Parser.Command
         | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)) attrKind
       /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
         So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
-      let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
+      let stxNodeKind := if (`_root_).isPrefixOf name then
+        name.replacePrefix `_root_ Name.anonymous
+      else
+        (← getCurrNamespace) ++ name
+      let pat := ⟨mkNode stxNodeKind patArgs⟩
       let stxCmd ← `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
         syntax$[:$prec?]?
           (name := $(name?.getD (mkIdentFrom tk name (canonical := true))))

src/Lean/Elab/Syntax.lean

@@ -381,10 +381,12 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
   let name ← match name? with
     | some name => pure name.getId
     | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat syntaxParser) attrKind
-  trace[Meta.debug] "name: {name}"
   let prio ← liftMacroM <| evalOptPrio prio?
   let idRef := (name?.map (·.raw)).getD tk
-  let stxNodeKind := (← getCurrNamespace) ++ name
+  let stxNodeKind := if (`_root_).isPrefixOf name then
+    name.replacePrefix `_root_ Name.anonymous
+  else
+    (← getCurrNamespace) ++ name
   let catParserId := mkIdentFrom idRef (cat.appendAfter "_parser")
   let (val, lhsPrec?) ← runTermElabM fun _ => Term.toParserDescr syntaxParser cat
   let declName := name?.getD (mkIdentFrom idRef name (canonical := true))
@@ -404,8 +406,13 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
   let `($[$doc?:docComment]? syntax $declName:ident := $[$ps:stx]*) ← pure stx | throwUnsupportedSyntax
   -- TODO: nonatomic names
   let (val, _) ← runTermElabM fun _ => Term.toParserDescr (mkNullNode ps) Name.anonymous
-  let stxNodeKind := (← getCurrNamespace) ++ declName.getId
-  let stx' ← `($[$doc?:docComment]? def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
+  let name := declName.getId
+  let stxNodeKind := if (`_root_).isPrefixOf name then
+    name.replacePrefix `_root_ Name.anonymous
+  else
+    (← getCurrNamespace) ++ name
+  let stx' ← `($[$doc?:docComment]? def $declName:ident : Lean.ParserDescr :=
+    ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
   withMacroExpansion stx stx' <| elabCommand stx'
 
 def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=