fix: elaboration of macro-generated defs

src/Init/Lean/Elab/Command.lean

@@ -586,10 +586,16 @@ levelNames      ←
       savedLevelNames
   };
 let ref := declId;
+-- extract (optional) namespace part of id, after decoding macro scopes that would interfere with the check
+let (id, scps) := extractMacroScopes id;
 match id with
-| Name.str pre s _ => withNamespace ref pre $ do
-  modifyScope $ fun scope => { levelNames := levelNames, .. scope };
-  finally (f (mkNameSimple s)) (modifyScope $ fun scope => { levelNames := savedLevelNames, .. scope })
+| Name.str pre s _ =>
+  /- Add back macro scopes. We assume a declaration like `def a.b[1,2] ...` with macro scopes `[1,2]`
+     is always meant to mean `namespace a def b[1,2] ...`. -/
+  let id := addMacroScopes (mkNameSimple s) scps;
+  withNamespace ref pre $ do
+    modifyScope $ fun scope => { levelNames := levelNames, .. scope };
+    finally (f id) (modifyScope $ fun scope => { levelNames := savedLevelNames, .. scope })
 | _                => throwError ref "invalid declaration name"
 
 /--

src/Init/Lean/Hygiene.lean

@@ -38,10 +38,24 @@ class MonadQuotation (m : Type → Type) :=
 (withFreshMacroScope {α : Type} : m α → m α)
 export MonadQuotation
 
-def addMacroScope (n : Name) (scp : MacroScope) : Name :=
 -- TODO: try harder to avoid clashes with other autogenerated names
+def addMacroScope (n : Name) (scp : MacroScope) : Name :=
 mkNameNum n scp
 
+def addMacroScopes (n : Name) (scps : List MacroScope) : Name :=
+scps.foldl addMacroScope n
+
+private def extractMacroScopesAux : Name → List MacroScope → Name × List MacroScope
+| Name.num n scp _, acc => extractMacroScopesAux n (scp::acc)
+| n               , acc => (n, acc.reverse)
+
+/--
+  Revert all `addMacroScope` calls. `(n', scps) = extractMacroScopes n → n = addMacroScopes n' scps`.
+  This operation is useful for analyzing/transforming the original identifiers, then adding back
+  the scopes (via `addMacroScopes`). -/
+def extractMacroScopes (n : Name) : Name × List MacroScope :=
+extractMacroScopesAux n []
+
 /-- Simplistic MonadQuotation that does not guarantee globally fresh names, that
     is, between different runs of this or other MonadQuotation implementations.
     It is only safe if the syntax quotations do not introduce bindings around