feat: backward.privateInPublic option (#10807)

This PR introduces the `backward.privateInPublic` option to aid in
porting projects to the module system by temporarily allowing access to
private declarations from the public scope, even across modules. A
warning will be generated by such accesses unless
`backward.privateInPublic.warn` is disabled.

Author: Kha

src/Lean/AddDecl.lean

@@ -128,7 +128,7 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit := do
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
     | _ => return (← doAdd)
 
-  if decl.getTopLevelNames.all isPrivateName then
+  if decl.getTopLevelNames.all isPrivateName && !(← ResolveName.backward.privateInPublic.getM) then
     exportedInfo? := none
   else
     -- preserve original constant kind in extension if different from exported one

src/Lean/Data/Options.lean

@@ -121,6 +121,9 @@ protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Op
 protected def get [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : α :=
   opts.get opt.name opt.defValue
 
+protected def getM [Monad m] [MonadOptions m] [KVMap.Value α] (opt : Lean.Option α) : m α :=
+  return opt.get (← getOptions)
+
 protected def set [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options :=
   opts.set opt.name val
 

src/Lean/Elab/App.lean

@@ -1267,7 +1267,9 @@ private partial def findMethod? (structName fieldName : Name) : MetaM (Option (N
   let find? structName' : MetaM (Option (Name × Name)) := do
     let fullName := privateToUserName structName' ++ fieldName
     -- We do not want to make use of the current namespace for resolution.
-    let candidates := ResolveName.resolveGlobalName (← getEnv) Name.anonymous (← getOpenDecls) fullName
+    let candidates :=
+      (← withTheReader Core.Context ({ · with currNamespace := .anonymous }) do
+        resolveGlobalName fullName)
       |>.filter (fun (_, fieldList) => fieldList.isEmpty)
       |>.map Prod.fst
     match candidates with
@@ -1737,7 +1739,7 @@ where
         -- Recall that the namespace for private declarations is non-private.
         let fullName := privateToUserName declName ++ id
         -- Resolve the name without making use of the current namespace, like in `findMethod?`.
-        let candidates := ResolveName.resolveGlobalName env Name.anonymous (← getOpenDecls) fullName
+        let candidates := ResolveName.resolveGlobalName env (← getOptions) Name.anonymous (← getOpenDecls) fullName
           |>.filter (fun (_, fieldList) => fieldList.isEmpty)
           |>.map Prod.fst
         if !candidates.isEmpty then

src/Lean/Elab/Open.lean

@@ -33,7 +33,7 @@ instance : MonadResolveName (M (m := m)) where
   getCurrNamespace   := return (← get).currNamespace
   getOpenDecls       := return (← get).openDecls
 
-def resolveId [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name := do
+def resolveId [MonadOptions m] [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name := do
   let declName := ns ++ idStx.getId
   if (← getEnv).contains declName then
     return declName
@@ -48,7 +48,7 @@ Uniquely resolves the identifier `idStx` in the provided namespaces `nss`.
 
 If the identifier does not indicate a name in exactly one of the namespaces, an exception is thrown.
 -/
-def resolveNameUsingNamespacesCore [MonadResolveName m]
+def resolveNameUsingNamespacesCore [MonadOptions m] [MonadResolveName m]
     (nss : List Name) (idStx : Syntax) : m Name := do
   let mut exs := #[]
   let mut result := #[]
@@ -69,7 +69,7 @@ def resolveNameUsingNamespacesCore [MonadResolveName m]
   else
     withRef idStx do throwError "ambiguous identifier `{idStx.getId}`, possible interpretations: {result.map mkConst}"
 
-def elabOpenDecl [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax ``Parser.Command.openDecl) : m (List OpenDecl) := do
+def elabOpenDecl [MonadOptions m] [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax ``Parser.Command.openDecl) : m (List OpenDecl) := do
   StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
     match stx with
     | `(Parser.Command.openDecl| $nss*) =>
@@ -108,7 +108,7 @@ def elabOpenDecl [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax ``Parser.
     | _ => throwUnsupportedSyntax
     return (← get).openDecls
 
-def resolveNameUsingNamespaces [MonadResolveName m] (nss : List Name) (idStx : Ident) : m Name := do
+def resolveNameUsingNamespaces [MonadOptions m] [MonadResolveName m] (nss : List Name) (idStx : Ident) : m Name := do
   StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
     resolveNameUsingNamespacesCore (m := M) nss idStx
 

src/Lean/Elab/Term/TermElabM.lean

@@ -1971,7 +1971,7 @@ where
     let env ← getEnv
     -- check for scope errors before trying auto implicits
     if env.isExporting then
-      if let [(npriv, _)] ← withEnv (env.setExporting false) <| resolveGlobalName n then
+      if let [(npriv, _)] ← withEnv (env.setExporting false) <| resolveGlobalName (enableLog := false) n then
         throwUnknownIdentifierAt (declHint := npriv) stx m!"Unknown identifier `{.ofConstName n}`"
     if (← read).autoBoundImplicit &&
           !(← read).autoBoundImplicitForbidden n &&

src/Lean/Elab/Util.lean

@@ -178,6 +178,7 @@ instance (m n) [MonadLift m n] [MonadQuotation n] [MonadMacroAdapter m] : MonadM
 
 def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : MacroM α) : m α := do
   let env  ← getEnv
+  let opts ← getOptions
   let currNamespace ← getCurrNamespace
   let openDecls ← getOpenDecls
   let methods := Macro.mkMethods {
@@ -189,7 +190,7 @@ def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [M
     hasDecl          := fun declName => return env.contains declName
     getCurrNamespace := return currNamespace
     resolveNamespace := fun n => return ResolveName.resolveNamespace env currNamespace openDecls n
-    resolveGlobalName := fun n => return ResolveName.resolveGlobalName env currNamespace openDecls n
+    resolveGlobalName := fun n => return ResolveName.resolveGlobalName env opts currNamespace openDecls n
   }
   match x { methods        := methods
             ref            := ← getRef

src/Lean/Parser/Extension.lean

@@ -663,7 +663,7 @@ inductive ParserResolution where
   | alias (p : ParserAliasValue)
 
 /-- Resolve the given parser name and return a list of candidates. -/
-def resolveParserNameCore (env : Environment) (currNamespace : Name)
+private def resolveParserNameCore (env : Environment) (opts : Options) (currNamespace : Name)
     (openDecls : List OpenDecl) (ident : Ident) : List ParserResolution := Id.run do
   let ⟨.ident (val := val) (preresolved := pre) ..⟩ := ident | return []
 
@@ -684,7 +684,7 @@ def resolveParserNameCore (env : Environment) (currNamespace : Name)
   if isParserCategory env erased then
     return [.category erased]
 
-  let resolved ← ResolveName.resolveGlobalName env currNamespace openDecls val |>.filterMap fun
+  let resolved ← ResolveName.resolveGlobalName env opts currNamespace openDecls val |>.filterMap fun
     | (name, []) => (isParser name).map fun isDescr => .parser name isDescr
     | _ => none
   unless resolved.isEmpty do
@@ -698,11 +698,11 @@ def resolveParserNameCore (env : Environment) (currNamespace : Name)
 
 /-- Resolve the given parser name and return a list of candidates. -/
 def ParserContext.resolveParserName (ctx : ParserContext) (id : Ident) : List ParserResolution :=
-  Parser.resolveParserNameCore ctx.env ctx.currNamespace ctx.openDecls id
+  Parser.resolveParserNameCore ctx.env ctx.options ctx.currNamespace ctx.openDecls id
 
 /-- Resolve the given parser name and return a list of candidates. -/
 def resolveParserName (id : Ident) : CoreM (List ParserResolution) :=
-  return resolveParserNameCore (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
+  return resolveParserNameCore (← getEnv) (← getOptions) (← getCurrNamespace) (← getOpenDecls) id
 
 def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do
   let stack := s.stxStack