fix: fixes #2000

We now add the macro scope to local syntax declarations.

src/Lean/Elab/ElabRules.lean

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

src/Lean/Elab/Macro.lean

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

@@ -113,11 +113,6 @@ def mkSimpleDelab (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Ma
       | `($lhs $$moreArgs*) => withRef f `($pat $$moreArgs*)
       | _                   => throw ())
 
-private def isLocalAttrKind (attrKind : Syntax) : Bool :=
-  match attrKind with
-  | `(Parser.Term.attrKind| local) => true
-  | _ => false
-
 private def expandNotationAux (ref : Syntax) (currNamespace : Name)
     (doc? : Option (TSyntax ``docComment))
     (attrs? : Option (TSepArray ``attrInstance ","))
@@ -132,6 +127,7 @@ private def expandNotationAux (ref : Syntax) (currNamespace : Name)
     match name? with
     | some name => pure name.getId
     | none => mkNameFromParserSyntax `term (mkNullNode syntaxParts)
+  let name ← addMacroScopeIfLocal name 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

@@ -345,6 +345,20 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
   <|>
   throwError "invalid syntax node kind '{k}'"
 
+def isLocalAttrKind (attrKind : Syntax) : Bool :=
+  match attrKind with
+  | `(Parser.Term.attrKind| local) => true
+  | _ => false
+
+/--
+Add macro scope to `name` if it does not already have them, and `attrKind` is `local`.
+-/
+def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind : Syntax) : m Name := do
+  if isLocalAttrKind attrKind && !name.hasMacroScopes then
+    MonadQuotation.addMacroScope name
+  else
+    return name
+
 @[builtin_command_elab «syntax»] def elabSyntax : CommandElab := fun stx => do
   let `($[$doc?:docComment]? $[ @[ $attrInstances:attrInstance,* ] ]? $attrKind:attrKind
       syntax%$tk $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) := stx
@@ -362,6 +376,8 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
   let name ← match name? with
     | some name => pure name.getId
     | none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser
+  let name ← addMacroScopeIfLocal name attrKind
+  trace[Meta.debug] "name: {name}"
   let prio ← liftMacroM <| evalOptPrio prio?
   let idRef := (name?.map (·.raw)).getD tk
   let stxNodeKind := (← getCurrNamespace) ++ name

tests/pkg/misc/Misc.lean

@@ -1,4 +1,5 @@
 import Misc.Foo
+import Misc.Boo
 import Lean
 
 open Lean Meta

tests/pkg/misc/Misc/Boo.lean

@@ -0,0 +1,3 @@
+local infix:50 " ≺ " => LE.le
+
+#check 1 ≺ 2

tests/pkg/misc/Misc/Foo.lean

@@ -7,3 +7,7 @@ open Lean Meta
   return ()
 
 def foo := 42
+
+local infix:50 " ≺ " => LE.le
+
+#check 1 ≺ 2