fix: fixes #2009

src/Lean/Elab/ElabRules.lean

@@ -95,8 +95,7 @@ def elabElab : CommandElab
     -- name
     let name ← match name? with
       | some name => pure name.getId
-      | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-    let name ← addMacroScopeIfLocal name attrKind
+      | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)) attrKind
     let nameId := name?.getD (mkIdentFrom tk name (canonical := true))
     let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
     elabCommand <|← `(

src/Lean/Elab/Macro.lean

@@ -20,8 +20,7 @@ open Lean.Parser.Command
       -- name
       let name ← match name? with
         | some name => pure name.getId
-        | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-      let name ← addMacroScopeIfLocal name attrKind
+        | 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⟩

src/Lean/Elab/Notation.lean

@@ -126,8 +126,7 @@ private def expandNotationAux (ref : Syntax) (currNamespace : Name)
   let name ←
     match name? with
     | some name => pure name.getId
-    | none => mkNameFromParserSyntax `term (mkNullNode syntaxParts)
-  let name ← addMacroScopeIfLocal name attrKind
+    | none => addMacroScopeIfLocal (← mkNameFromParserSyntax `term (mkNullNode syntaxParts)) attrKind
   -- build macro rules
   let vars := items.filter fun item => item.raw.getKind == ``identPrec
   let vars := vars.map fun var => var.raw[0]

src/Lean/Elab/Syntax.lean

@@ -375,8 +375,7 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
     | none      => pure precDefault
   let name ← match name? with
     | some name => pure name.getId
-    | none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser
-  let name ← addMacroScopeIfLocal name attrKind
+    | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat syntaxParser) attrKind
   trace[Meta.debug] "name: {name}"
   let prio ← liftMacroM <| evalOptPrio prio?
   let idRef := (name?.map (·.raw)).getD tk

tests/lean/run/2009.lean

@@ -0,0 +1 @@
+local notation (name := foo) "foo" => 42