fix: use eraseMacroScopes on trace classes

src/Init/NotationExtra.lean

@@ -11,11 +11,8 @@ import Init.Data.Array.Subarray
 import Init.Data.ToString
 namespace Lean
 
-syntax "Macro.trace[" ident "]" interpolatedStr(term) : term
-
-macro_rules
-  | `(Macro.trace[$id] $s) => `(Macro.trace $(quote id.getId) (s! $s))
-
+macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
+  `(Macro.trace $(quote id.getId.eraseMacroScopes) (s! $s))
 
 -- Auxiliary parsers and functions for declaring notation with binders
 

src/Lean/Util/Trace.lean

@@ -143,7 +143,7 @@ def registerTraceClass (traceClassName : Name) : IO Unit :=
 macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
   let msg ← if s.getKind == interpolatedStrKind then `(m! $s) else `(($s : MessageData))
   `(doElem| do
-    let cls := $(quote id.getId)
+    let cls := $(quote id.getId.eraseMacroScopes)
     if (← Lean.isTracingEnabledFor cls) then
       Lean.addTrace cls $msg)
 

tests/lean/traceClassScopes.lean

@@ -0,0 +1,19 @@
+import Lean
+
+macro "t" t:interpolatedStr(term) : doElem =>
+  `(Macro.trace[Meta.debug] $t)
+
+macro "tstcmd" : command => do
+  t "hello"
+  `(example : Nat := 1)
+
+set_option trace.Meta.debug true in
+tstcmd
+
+open Lean Meta
+
+macro "r" r:interpolatedStr(term) : doElem =>
+  `(trace[Meta.debug] $r)
+
+set_option trace.Meta.debug true in
+#eval show MetaM _ from do r "world"

tests/lean/traceClassScopes.lean.expected.out

@@ -0,0 +1,2 @@
+[Meta.debug] hello
+[Meta.debug] world