feat: hint about inaccessible private declaration on dot notation failure (#10803)

This PR improves the error message of generalized field notation if the
issue is that the resolved declaration is not visible in the current
context.

Author: Kha

src/Lean/Elab/App.lean

@@ -1252,8 +1252,11 @@ inductive LValResolution where
   The `baseName` is the base name of the type to search for in the parameter list. -/
   | localRec (baseName : Name) (fvar : Expr)
 
+private def mkLValError (e : Expr) (eType : Expr) (msg : MessageData) : MessageData :=
+  m!"{msg}{indentExpr e}\nhas type{indentExpr eType}"
+
 private def throwLValErrorAt (ref : Syntax) (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
-  throwErrorAt ref "{msg}{indentExpr e}\nhas type{indentExpr eType}"
+  throwErrorAt ref (mkLValError e eType msg)
 
 private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α := do
   throwLValErrorAt (← getRef) e eType msg
@@ -1322,9 +1325,19 @@ where
     | some (_, p2) => prodArity p2 + 1
 
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
-  let throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name) : TermElabM α := do
-    throwLValErrorAt ref e eType <| ← mkUnknownIdentifierMessage (declHint := fullName)
-      m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`"
+  let throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name)
+      (declHint := Name.anonymous) : TermElabM α := do
+    let msg ←
+      -- ordering: put decl hint, if any, last
+      mkUnknownIdentifierMessage (declHint := declHint)
+        (mkLValError e eType
+          m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`")
+    -- HACK: Simulate previous embedding of tagged `mkUnknownIdentifierMessage`.
+    -- The "import unknown identifier" code action requires the tag to be present somewhere in the
+    -- message. But if it is at the root, the tag will also be shown to the user even though the
+    -- current help page does not address field notation, which should likely get its own help page
+    -- (if any).
+    throwErrorAt ref m!"{msg}{.nil}"
   if eType.isForall then
     match lval with
     | LVal.fieldName _ fieldName suffix? fullRef =>
@@ -1390,6 +1403,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
       return LValResolution.const baseStructName structName fullName
     throwInvalidFieldAt fullRef fieldName fullName
+      -- Suggest a potential unreachable private name as hint. This does not cover structure
+      -- inheritance, nor `import all`.
+      (declHint := (mkPrivateName env structName).mkStr fieldName)
   | none, LVal.fieldName _ _ (some suffix) fullRef =>
     -- This may be a function constant whose implicit arguments have already been filled in:
     let c := e.getAppFn

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 (enableLog := false) n then
+      if let [(npriv, _)] ← withoutExporting <| resolveGlobalName (enableLog := false) n then
         throwUnknownIdentifierAt (declHint := npriv) stx m!"Unknown identifier `{.ofConstName n}`"
     if (← read).autoBoundImplicit &&
           !(← read).autoBoundImplicitForbidden n &&

src/Lean/Exception.lean

@@ -105,17 +105,8 @@ function directly.
 protected def «throwNamedErrorAt» [Monad m] [MonadError m] (ref : Syntax) (name : Name) (msg : MessageData) : m α :=
   withRef ref <| Lean.throwNamedError name msg
 
-/--
-Creates a `MessageData` that is tagged with `unknownIdentifierMessageTag`.
-This tag is used by the 'import unknown identifier' code action to detect messages that should
-prompt the code action.
-The end position of the range of an unknown identifier message should always point at the end of the
-unknown identifier.
-
-If `declHint` is specified, a corresponding hint is added to the message in case the name refers to
-a private declaration that is not accessible in the current context.
--/
-def mkUnknownIdentifierMessage [Monad m] [MonadEnv m] [MonadError m] (msg : MessageData)
+/-- Like `mkUnknownIdentifierMessage`, but does not tag the message. -/
+def mkUnknownIdentifierMessageCore [Monad m] [MonadEnv m] [MonadError m] (msg : MessageData)
     (declHint := Name.anonymous) : m MessageData := do
   let mut msg := msg
   let env ← getEnv
@@ -131,6 +122,21 @@ def mkUnknownIdentifierMessage [Monad m] [MonadEnv m] [MonadError m] (msg : Mess
           msg ++ .note m!"A private declaration `{c}` (from `{mod}`) exists but would need to be public to access here."
         else
           msg ++ .note m!"A public declaration `{c}` exists but is imported privately; consider adding `public import {mod}`."
+  return msg
+
+/--
+Creates a `MessageData` that is tagged with `unknownIdentifierMessageTag`.
+This tag is used by the 'import unknown identifier' code action to detect messages that should
+prompt the code action.
+The end position of the range of an unknown identifier message should always point at the end of the
+unknown identifier.
+
+If `declHint` is specified, a corresponding hint is added to the message in case the name refers to
+a private declaration that is not accessible in the current context.
+-/
+def mkUnknownIdentifierMessage [Monad m] [MonadEnv m] [MonadError m] (msg : MessageData)
+    (declHint := Name.anonymous) : m MessageData := do
+  let msg ← mkUnknownIdentifierMessageCore msg declHint
   return MessageData.tagged unknownIdentifierMessageTag msg
 
 /--

tests/pkg/module/Module/Basic.lean

@@ -479,3 +479,20 @@ attribute [simp] f_struct
 /-! `initialize` should be run even if imported IR-only. -/
 
 public initialize initialized : Nat ← pure 5
+
+/-! Error message on private dot notation access. -/
+
+public structure S
+
+def S.s := 1
+
+/--
+error: Invalid field `s`: The environment does not contain `S.s`
+  s
+has type
+  S
+
+Note: A private declaration `S.s` (from the current module) exists but would need to be public to access here.
+-/
+#guard_msgs in
+@[expose] public def useS (s : S) := s.s