feat: hint about inaccessible private declaration on dot notation failure

Author: Kha

src/Lean/Elab/App.lean

@@ -1261,8 +1261,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
@@ -1329,9 +1332,13 @@ 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
+    throwErrorAt ref (←
+      -- ordering: put decl hint, if any, last
+      mkUnknownIdentifierMessage (declHint := declHint)
+        (mkLValError e eType
+          m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`"))
   if eType.isForall then
     match lval with
     | LVal.fieldName _ fieldName suffix? fullRef =>
@@ -1397,6 +1404,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

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

tests/pkg/module/Module/Basic.lean

@@ -469,3 +469,20 @@ info: @[expose] meta def msecexp : Nat :=
 #print msecexp
 
 attribute [simp] f_struct
+
+/-! 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