fix: global name resolution of macro-introduced idents

src/Init/Lean/Elab/ResolveName.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
+import Init.Lean.Hygiene
 import Init.Lean.Modifiers
 import Init.Lean.Elab.Alias
 
@@ -65,8 +66,10 @@ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl →
   let resolvedIds := if id == openedId then resolvedId :: resolvedIds else resolvedIds;
   resolveOpenDecls openDecls resolvedIds
 
-private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : List OpenDecl) : Name → List String → List (Name × List String)
+private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : List OpenDecl) (scps : List MacroScope) : Name → List String → List (Name × List String)
 | id@(Name.str p s _), projs =>
+  -- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
+  let id := addMacroScopes id scps;
   match resolveUsingNamespace env id ns with
   | resolvedIds@(_ :: _) => resolvedIds.eraseDups.map $ fun id => (id, projs)
   | [] =>
@@ -82,7 +85,9 @@ private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : Li
 | _, _ => []
 
 def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) :=
-resolveGlobalNameAux env ns openDecls id []
+-- decode macro scopes from name before recursion
+let (id, scps) := extractMacroScopes id;
+resolveGlobalNameAux env ns openDecls scps id []
 
 /- Namespace resolution -/