fix: hygienic resolution of namespaces

src/Init/Meta.lean

@@ -158,8 +158,6 @@ protected def reprPrec (n : Name) (prec : Nat) : Std.Format :=
 instance : Repr Name where
   reprPrec := Name.reprPrec
 
-deriving instance Repr for Syntax
-
 def capitalize : Name → Name
   | .str p s => .str p s.capitalize
   | n        => n
@@ -257,6 +255,9 @@ instance monadNameGeneratorLift (m n : Type → Type) [MonadLift m n] [MonadName
 
 namespace Syntax
 
+deriving instance Repr for Syntax.Preresolved
+deriving instance Repr for Syntax
+
 abbrev Term := TSyntax `term
 abbrev Command := TSyntax `command
 protected abbrev Level := TSyntax `level
@@ -325,6 +326,9 @@ end TSyntax
 
 namespace Syntax
 
+deriving instance BEq for Syntax.Preresolved
+
+/-- Compare syntax structures modulo source info. -/
 partial def structEq : Syntax → Syntax → Bool
   | Syntax.missing, Syntax.missing => true
   | Syntax.node _ k args, Syntax.node _ k' args' => k == k' && args.isEqv args' structEq
@@ -510,7 +514,7 @@ def mkIdentFromRef [Monad m] [MonadRef m] (val : Name) : m Ident := do
 def mkCIdentFrom (src : Syntax) (c : Name) : Ident :=
   -- Remark: We use the reserved macro scope to make sure there are no accidental collision with our frontend
   let id   := addMacroScope `_internal c reservedMacroScope
-  ⟨Syntax.ident (SourceInfo.fromRef src) (toString id).toSubstring id [(c, [])]⟩
+  ⟨Syntax.ident (SourceInfo.fromRef src) (toString id).toSubstring id [.decl c []]⟩
 
 def mkCIdentFromRef [Monad m] [MonadRef m] (c : Name) : m Syntax := do
   return mkCIdentFrom (← getRef) c

src/Init/Prelude.lean

@@ -3399,6 +3399,17 @@ abbrev SyntaxNodeKind := Name
 
 /-! # Syntax AST -/
 
+/--
+Binding information resolved and stored at compile time of a syntax quotation.
+Note: We do not statically know whether a syntax expects a namespace or term name,
+so a `Syntax.ident` may contain both preresolution kinds.
+-/
+inductive Syntax.Preresolved where
+  | /-- A potential namespace reference -/
+    namespace (ns : Name)
+  | /-- A potential global constant or section variable reference, with additional field accesses -/
+    decl (n : Name) (fields : List String)
+
 /--
 Syntax objects used by the parser, macro expander, delaborator, etc.
 -/
@@ -3435,9 +3446,9 @@ inductive Syntax where
     `rawIdent` parsers.
     * `rawVal` is the literal substring from the input file
     * `val` is the parsed identifier (with hygiene)
-    * `preresolved` is the list of possible constants this could refer to
+    * `preresolved` is the list of possible declarations this could refer to
     -/
-    ident  (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Prod Name (List String))) : Syntax
+    ident  (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Syntax.Preresolved) : Syntax
 
 /-- `SyntaxNodeKinds` is a set of `SyntaxNodeKind` (implemented as a list). -/
 def SyntaxNodeKinds := List SyntaxNodeKind

src/Lean/Elab/BuiltinCommand.lean

@@ -120,22 +120,22 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   | Except.error ex => throwError (ex.toMessageData (← getOptions))
 
 @[builtinCommandElab «export»] def elabExport : CommandElab := fun stx => do
-  -- `stx` is of the form (Command.export "export" <namespace> "(" (null <ids>*) ")")
-  let id  := stx[1].getId
-  let nss ← resolveNamespace id
+  let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax
+  let nss ← resolveNamespace ns
   let currNamespace ← getCurrNamespace
   if nss == [currNamespace] then throwError "invalid 'export', self export"
-  let ids := stx[3].getArgs
   let mut aliases := #[]
   for idStx in ids do
     let id := idStx.getId
     let declName ← resolveNameUsingNamespaces nss idStx
     aliases := aliases.push (currNamespace ++ id, declName)
   modify fun s => { s with env := aliases.foldl (init := s.env) fun env p => addAlias env p.1 p.2 }
 
-@[builtinCommandElab «open»] def elabOpen : CommandElab := fun n => do
-  let openDecls ← elabOpenDecl n[1]
-  modifyScope fun scope => { scope with openDecls := openDecls }
+@[builtinCommandElab «open»] def elabOpen : CommandElab
+  | `(open $decl:openDecl) => do
+    let openDecls ← elabOpenDecl decl
+    modifyScope fun scope => { scope with openDecls := openDecls }
+  | _ => throwUnsupportedSyntax
 
 private def typelessBinder? : Syntax → Option (Array (TSyntax [`ident, `Lean.Parser.Term.hole]) × Bool)
   | `(bracketedBinder|($ids*)) => some <| (ids, true)

src/Lean/Elab/BuiltinTerm.lean

@@ -268,11 +268,12 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | some msg => elabTermEnsuringType stx[2] expectedType? (errorMsgHeader? := msg)
 
 @[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
+  let `(open $decl in $e) := stx | throwUnsupportedSyntax
   try
     pushScope
-    let openDecls ← elabOpenDecl stx[1]
+    let openDecls ← elabOpenDecl decl
     withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
-      elabTerm stx[3] expectedType?
+      elabTerm e expectedType?
   finally
     popScope
 

src/Lean/Elab/Open.lean

@@ -13,6 +13,10 @@ variable [Monad m] [STWorld IO.RealWorld m] [MonadEnv m]
 variable [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
 variable [AddMessageContext m] [MonadLiftT (ST IO.RealWorld) m] [MonadLog m]
 
+/--
+A local copy of name resolution state that allows us to immediately use new open decls
+in further name resolution as in `open Lean Elab`.
+-/
 structure State where
   openDecls     : List OpenDecl
   currNamespace : Name
@@ -33,19 +37,6 @@ def resolveId (ns : Name) (idStx : Syntax) : M (m := m) Name := do
 private def addOpenDecl (decl : OpenDecl) : M (m:=m) Unit :=
   modify fun s => { s with openDecls := decl :: s.openDecls }
 
-private def elabOpenSimple (n : Syntax) : M (m:=m) Unit :=
-  -- `open` id+
-  for ns in n[0].getArgs do
-    for ns in (← resolveNamespace ns.getId) do
-      addOpenDecl (OpenDecl.simple ns [])
-      activateScoped ns
-
-private def elabOpenScoped (n : Syntax) : M (m:=m) Unit :=
-  -- `open` `scoped` id+
-  for ns in n[1].getArgs do
-    for ns in (← resolveNamespace ns.getId) do
-    activateScoped ns
-
 private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) : M (m:=m) Name := do
   let mut exs := #[]
   let mut result := #[]
@@ -66,56 +57,43 @@ private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) :
   else
     withRef idStx do throwError "ambiguous identifier '{idStx.getId}', possible interpretations: {result.map mkConst}"
 
--- `open` id `(` id+ `)`
-private def elabOpenOnly (n : Syntax) : M (m:=m) Unit := do
-  let nss ← resolveNamespace n[0].getId
-  for idStx in n[2].getArgs do
-    let declName ← resolveNameUsingNamespacesCore nss idStx
-    addOpenDecl (OpenDecl.explicit idStx.getId declName)
-
--- `open` id `hiding` id+
-private def elabOpenHiding (n : Syntax) : M (m:=m) Unit := do
-  let ns ← resolveUniqueNamespace n[0].getId
-  let mut ids : List Name := []
-  for idStx in n[2].getArgs do
-    let _ ← resolveId ns idStx
-    let id := idStx.getId
-    ids := id::ids
-  addOpenDecl (OpenDecl.simple ns ids)
-
--- `open` id `renaming` sepBy (id `->` id) `,`
-private def elabOpenRenaming (n : Syntax) : M (m:=m) Unit := do
-  let ns ← resolveUniqueNamespace n[0].getId
-  for stx in n[2].getSepArgs do
-    let fromStx  := stx[0]
-    let toId     := stx[2].getId
-    let declName ← resolveId ns fromStx
-    addOpenDecl (OpenDecl.explicit toId declName)
-
-def elabOpenDecl [MonadResolveName m] (openDeclStx : Syntax) : m (List OpenDecl) := do
+def elabOpenDecl [MonadResolveName m] (stx : TSyntax ``Parser.Command.openDecl) : m (List OpenDecl) := do
   StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
-    if openDeclStx.getKind == ``Parser.Command.openSimple then
-      elabOpenSimple openDeclStx
-    else if openDeclStx.getKind == ``Parser.Command.openScoped then
-      elabOpenScoped openDeclStx
-    else if openDeclStx.getKind == ``Parser.Command.openOnly then
-      elabOpenOnly openDeclStx
-    else if openDeclStx.getKind == ``Parser.Command.openHiding then
-      elabOpenHiding openDeclStx
-    else
-      elabOpenRenaming openDeclStx
+    match stx with
+    | `(Parser.Command.openDecl| $nss*) =>
+      for ns in nss do
+        for ns in (← resolveNamespace ns) do
+          addOpenDecl (OpenDecl.simple ns [])
+          activateScoped ns
+    | `(Parser.Command.openDecl| scoped $nss*) =>
+      for ns in nss do
+        for ns in (← resolveNamespace ns) do
+          activateScoped ns
+    | `(Parser.Command.openDecl| $ns ($ids*)) =>
+      let nss ← resolveNamespace ns
+      for idStx in ids do
+        let declName ← resolveNameUsingNamespacesCore nss idStx
+        addOpenDecl (OpenDecl.explicit idStx.getId declName)
+    | `(Parser.Command.openDecl| $ns hiding $ids*) =>
+      let ns ← resolveUniqueNamespace ns
+      for id in ids do
+        let _ ← resolveId ns id
+      let ids := ids.map (·.getId) |>.toList
+      addOpenDecl (OpenDecl.simple ns ids)
+    | `(Parser.Command.openDecl| $ns renaming $[$froms -> $tos],*) =>
+      let ns ← resolveUniqueNamespace ns
+      for («from», to) in froms.zip tos do
+        let declName ← resolveId ns «from»
+        addOpenDecl (OpenDecl.explicit to.getId declName)
+    | _ => throwUnsupportedSyntax
     return (← get).openDecls
 
-def resolveOpenDeclId [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name := do
-  StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
-    OpenDecl.resolveId ns idStx
-
-def resolveNameUsingNamespaces [MonadResolveName m] (nss : List Name) (idStx : Syntax) : m Name := do
+def resolveNameUsingNamespaces [MonadResolveName m] (nss : List Name) (idStx : Ident) : m Name := do
   StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
     resolveNameUsingNamespacesCore nss idStx
 
 end OpenDecl
 
-export OpenDecl (elabOpenDecl resolveOpenDeclId resolveNameUsingNamespaces)
+export OpenDecl (elabOpenDecl resolveNameUsingNamespaces)
 
 end Lean.Elab

src/Lean/Elab/Quotation.lean

@@ -99,18 +99,27 @@ def tryAddSyntaxNodeKindInfo (stx : Syntax) (k : SyntaxNodeKind) : TermElabM Uni
     if (← getEnv).contains k then
       addTermInfo' stx (← mkConstWithFreshMVarLevels k)
 
+instance : Quote Syntax.Preresolved where
+  quote
+    | .namespace ns => Unhygienic.run ``(Syntax.Preresolved.namespace $(quote ns))
+    | .decl n fs    => Unhygienic.run ``(Syntax.Preresolved.decl $(quote n) $(quote fs))
+
 /-- Elaborate the content of a syntax quotation term -/
 private partial def quoteSyntax : Syntax → TermElabM Term
   | Syntax.ident _ rawVal val preresolved => do
     if !hygiene.get (← getOptions) then
       return ← `(Syntax.ident info $(quote rawVal) $(quote val) $(quote preresolved))
     -- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
     -- See the paper for details.
-    let r ← resolveGlobalName val
+    let consts ← resolveGlobalName val
     -- extension of the paper algorithm: also store unique section variable names as top-level scopes
     -- so they can be captured and used inside the section, but not outside
-    let r' := resolveSectionVariable (← read).sectionVars val
-    let preresolved := r ++ r' ++ preresolved
+    let sectionVars := resolveSectionVariable (← read).sectionVars val
+    -- extension of the paper algorithm: resolve namespaces as well
+    let namespaces ← resolveNamespaceCore (allowEmpty := true) val
+    let preresolved := (consts ++ sectionVars).map (fun (n, projs) => Preresolved.decl n projs) ++
+      namespaces.map .namespace ++
+      preresolved
     let val := quote val
     -- `scp` is bound in stxQuot.expand
     `(Syntax.ident info $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -99,11 +99,12 @@ private def getOptRotation (stx : Syntax) : Nat :=
   setGoals <| (← getGoals).rotateRight n
 
 @[builtinTactic Parser.Tactic.open] def evalOpen : Tactic := fun stx => do
+  let `(tactic| open $decl in $tac) := stx | throwUnsupportedSyntax
   try
     pushScope
-    let openDecls ← elabOpenDecl stx[1]
+    let openDecls ← elabOpenDecl decl
     withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
-      evalTactic stx[3]
+      evalTactic tac
   finally
     popScope
 

src/Lean/Elab/Term.lean

@@ -1726,12 +1726,15 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
    let const ← mkConst declName explicitLevels
    return (const, projs) :: result
 
-def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
+def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
   addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
   if let some (e, projs) ← resolveLocalName n then
     unless explicitLevels.isEmpty do
       throwError "invalid use of explicit universe parameters, '{e}' is a local"
     return [(e, projs)]
+  let preresolved := preresolved.filterMap fun
+    | .decl n projs => some (n, projs)
+    | _             => none
   -- check for section variable capture by a quotation
   let ctx ← read
   if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then

src/Lean/ResolveName.lean

@@ -204,15 +204,33 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
 def resolveGlobalName [Monad m] [MonadResolveName m] [MonadEnv m] (id : Name) : m (List (Name × List String)) := do
   return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
 
-def resolveNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Name) : m (List Name) := do
-  match ResolveName.resolveNamespace (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with
-  | []  => throwError s!"unknown namespace '{id}'"
-  | nss => return nss
+/--
+Given a namespace name, return a list of possible interpretations.
+Names extracted from syntax should be passed to `resolveNamespace` instead.
+-/
+def resolveNamespaceCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Name) (allowEmpty := false) : m (List Name) := do
+  let nss := ResolveName.resolveNamespace (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
+  if !allowEmpty && nss.isEmpty then
+    throwError s!"unknown namespace '{id}'"
+  return nss
+
+/-- Given a namespace identifier, return a list of possible interpretations. -/
+def resolveNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Ident → m (List Name)
+  | stx@⟨Syntax.ident _ _ n pre⟩ => do
+    let pre := pre.filterMap fun
+      | .namespace ns => some ns
+      | _             => none
+    if pre.isEmpty then
+      withRef stx <| resolveNamespaceCore n
+    else
+      return pre
+  | stx => throwErrorAt stx s!"expected identifier"
 
-def resolveUniqueNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Name) : m Name := do
+/-- Given a namespace identifier, return the unique interpretation or else fail. -/
+def resolveUniqueNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Ident) : m Name := do
   match (← resolveNamespace id) with
   | [ns] => return ns
-  | nss => throwError s!"ambiguous namespace '{id}', possible interpretations: '{nss}'"
+  | nss => throwError s!"ambiguous namespace '{id.getId}', possible interpretations: '{nss}'"
 
 /-- Given a name `n`, return a list of possible interpretations for global constants.
 
@@ -254,7 +272,9 @@ After `open Foo open Boo`, we have
 -/
 def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Syntax → m (List Name)
   | stx@(Syntax.ident _ _ n pre) => do
-    let pre := pre.filterMap fun (n, fields) => if fields.isEmpty then some n else none
+    let pre := pre.filterMap fun
+      | .decl n [] => some n
+      | _          => none
     if pre.isEmpty then
       withRef stx <| resolveGlobalConstCore n
     else