chore: avoid turning accesses to private decs from public signatures into auto implicits (#9961)

src/Lean/Elab/Term.lean

@@ -1994,9 +1994,12 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
 where
   process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
     if candidates.isEmpty then
+      let env ← getEnv
       if (← read).autoBoundImplicit &&
            !(← read).autoBoundImplicitForbidden n &&
-           isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
+           isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) &&
+           -- do not turn a scope error into an auto implicit
+           !(env.isExporting && (env.setExporting false).contains n) then
         throwAutoBoundImplicitLocal n
       else
         throwUnknownIdentifierAt (declHint := n) stx m!"Unknown identifier `{.ofConstName n}`"

tests/pkg/module/Module/PrivateImported.lean

@@ -12,7 +12,6 @@ error: Unknown identifier `f`
 Note: A private declaration `f` exists but is not accessible in the current context.
 -/
 #guard_msgs in
-set_option autoImplicit false in
 public theorem t2 : f = 1 := sorry
 
 /--