fix: store local context for 'don't know how to synthesize implicit a…

…rgument' errors (#5658)

When named arguments introduce eta arguments, the full application
contains fvars for these eta arguments, so `MVarErrorKind.implicitArg`
needs to keep a local context for its error messages. This is because
the local context of the mvar associated to the `MVarErrorKind` is not
sufficient, since when an eta argument come after an implicit argument,
the implicit argument's mvar doesn't contain the eta argument's fvar in
its local context.

Closes #5475

src/Lean/Elab/Term.lean

@@ -80,8 +80,9 @@ structure SyntheticMVarDecl where
   We have three different kinds of error context.
 -/
 inductive MVarErrorKind where
-  /-- Metavariable for implicit arguments. `ctx` is the parent application. -/
-  | implicitArg (ctx : Expr)
+  /-- Metavariable for implicit arguments. `ctx` is the parent application,
+  `lctx` is a local context where it is valid (necessary for eta feature for named arguments). -/
+  | implicitArg (lctx : LocalContext) (ctx : Expr)
   /-- Metavariable for explicit holes provided by the user (e.g., `_` and `?m`) -/
   | hole
   /-- "Custom", `msgData` stores the additional error messages. -/
@@ -90,7 +91,7 @@ inductive MVarErrorKind where
 
 instance : ToString MVarErrorKind where
   toString
-    | .implicitArg _   => "implicitArg"
+    | .implicitArg _ _ => "implicitArg"
     | .hole            => "hole"
     | .custom _        => "custom"
 
@@ -735,7 +736,7 @@ def registerMVarErrorHoleInfo (mvarId : MVarId) (ref : Syntax) : TermElabM Unit
   registerMVarErrorInfo { mvarId, ref, kind := .hole }
 
 def registerMVarErrorImplicitArgInfo (mvarId : MVarId) (ref : Syntax) (app : Expr) : TermElabM Unit := do
-  registerMVarErrorInfo { mvarId, ref, kind := .implicitArg app }
+  registerMVarErrorInfo { mvarId, ref, kind := .implicitArg (← getLCtx) app }
 
 def registerMVarErrorCustomInfo (mvarId : MVarId) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := do
   registerMVarErrorInfo { mvarId, ref, kind := .custom msgData }
@@ -761,7 +762,7 @@ def throwMVarError (m : MessageData) : TermElabM α := do
 
 def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) (extraMsg? : Option MessageData) : TermElabM Unit := do
   match mvarErrorInfo.kind with
-  | MVarErrorKind.implicitArg app => do
+  | MVarErrorKind.implicitArg lctx app => withLCtx lctx {} do
     let app ← instantiateMVars app
     let msg ← addArgName "don't know how to synthesize implicit argument"
     let msg := msg ++ m!"{indentExpr app.setAppPPExplicitForExposingMVars}" ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId

tests/lean/run/5475.lean

@@ -0,0 +1,23 @@
+/-!
+# Eta arguments had wrong context in "don't know how to synthesize implicit" errors
+https://github.com/leanprover/lean4/issues/5475
+-/
+
+set_option pp.mvars false
+
+/-!
+Formerly, argument `x` appeared as `_fvar.123`
+-/
+
+def f {α β : Type} (x: α) (y: β) : α := x
+/--
+error: don't know how to synthesize implicit argument 'α'
+  @f ?_ Nat x Nat.zero
+context:
+⊢ Type
+---
+error: failed to infer definition type
+-/
+#guard_msgs in
+example :=
+  f (y := Nat.zero)