experiment: improved 'synthsized type class instance is not definitio…

src/Lean/Elab/App.lean

@@ -74,7 +74,7 @@ private def mkProjAndCheck (structName : Name) (idx : Nat) (e : Expr) : MetaM Ex
 
 def synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) : TermElabM Unit :=
   for mvarId in instMVars do
-    unless (← synthesizeInstMVarCore mvarId) do
+    unless (← synthesizeInstMVarCore mvarId (app? := app)) do
       registerSyntheticMVarWithCurrRef mvarId (.typeClass none)
       registerMVarErrorImplicitArgInfo mvarId (← getRef) app
 

src/Lean/Elab/SyntheticMVars.lean

@@ -78,8 +78,15 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
   are used. It also logs any error message produced. -/
 private def synthesizePendingInstMVar (instMVar : MVarId) (extraErrorMsg? : Option MessageData := none): TermElabM Bool :=
   instMVar.withContext do
+    -- Recover the parent application registered by `synthesizeAppInstMVars` for richer errors.
+    let app? := (← get).mvarErrorInfos.findSome? fun info =>
+      if info.mvarId == instMVar then
+        match info.kind with
+        | .implicitArg _ app => some app
+        | _ => none
+      else none
     try
-      synthesizeInstMVarCore instMVar (extraErrorMsg? := extraErrorMsg?)
+      synthesizeInstMVarCore instMVar (extraErrorMsg? := extraErrorMsg?) (app? := app?)
     catch
       | ex@(.error ..) => logException ex; return true
       | _              => unreachable!

src/Lean/Elab/Term/TermElabM.lean

@@ -1191,6 +1191,22 @@ Returns whether `className` has a `deriving` handler installed.
 def hasDerivingHandler (className : Name) : IO Bool := do
   return (← derivableRef.get).contains className
 
+/--
+Build a `MessageData` describing the application context for an instance-argument mismatch:
+shows the (explicit) application and identifies which positional argument is the instance,
+falling back gracefully when the mvar cannot be located in the application's argument list.
+-/
+private def mkInstAppContextMsg (instMVar : MVarId) (app : Expr) : TermElabM MessageData := do
+  let argIdx? := app.getAppArgs.findIdx? fun a => a.isMVar && a.mvarId! == instMVar
+  let argName? := (← get).mvarArgNames.get? instMVar |>.filter (!·.hasMacroScopes)
+  let argDescr : MessageData := match argName?, argIdx? with
+    | some n, some i => m!"`{n}` (#{i+1})"
+    | some n, none   => m!"`{n}`"
+    | none,   some i => m!"#{i+1}"
+    | none,   none   => m!"of unknown position"
+  let appInst ← instantiateMVars app
+  return m!"\nwhile elaborating instance argument {argDescr} of{indentExpr appInst.setAppPPExplicit}"
+
 /--
   Try to synthesize metavariable using type class resolution.
   This method assumes the local context and local instances of `instMVar` coincide
@@ -1201,8 +1217,12 @@ def hasDerivingHandler (className : Name) : IO Bool := do
 
   If `extraErrorMsg?` is not none, it contains additional information that should be attached
   to type class synthesis failures.
+
+  If `app?` is `some app`, the parent application is included in mismatch error messages,
+  together with an indicator pointing at the instance argument inside it.
 -/
-def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := none) (extraErrorMsg? : Option MessageData := none): TermElabM Bool := do
+def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := none)
+    (extraErrorMsg? : Option MessageData := none) (app? : Option Expr := none) : TermElabM Bool := do
   let extraErrorMsg := extraMsgToMsg extraErrorMsg?
   let instMVarDecl ← getMVarDecl instMVar
   let type := instMVarDecl.type
@@ -1233,13 +1253,17 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
              `p` has not been elaborated yet.
            -/
           return false -- we will try again later
+        let appCtx? ← app?.mapM (mkInstAppContextMsg instMVar ·)
+        let (sep, ctx) := match appCtx? with
+          | some ctx => ("\n", ctx)
+          | none     => (", ", MessageData.nil)
         let oldValType ← inferType oldVal
         let valType ← inferType val
         unless (← isDefEq oldValType valType) do
           let (oldValType, valType) ← addPPExplicitToExposeDiff oldValType valType
-          throwError "synthesized type class instance type is not definitionally equal to expected type, synthesized{indentExpr val}\nhas type{indentExpr valType}\nexpected{indentExpr oldValType}{extraErrorMsg}"
+          throwError "synthesized type class instance type is not definitionally equal to expected type{ctx}{sep}synthesized{indentExpr val}\nhas type{indentExpr valType}\nexpected{indentExpr oldValType}{extraErrorMsg}"
         let (oldVal, val) ← addPPExplicitToExposeDiff oldVal val
-        throwError "synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized{indentExpr val}\ninferred{indentExpr oldVal}{extraErrorMsg}"
+        throwError "synthesized type class instance is not definitionally equal to expression inferred by typing rules{ctx}{sep}synthesized{indentExpr val}\ninferred{indentExpr oldVal}{extraErrorMsg}"
     else
       unless (← isDefEq (mkMVar instMVar) val) do
         throwError "failed to assign synthesized type class instance{indentExpr val}{extraErrorMsg}"

tests/elab_fail/inst_arg_mismatch.lean

@@ -0,0 +1,31 @@
+import Lean.Elab.Term
+
+/-!
+Test the "synthesized type class instance is not definitionally equal" error message.
+
+When type-class resolution produces an instance that disagrees with the value already
+assigned to the instance metavariable by other typing constraints, the error should
+include the surrounding application and a clear indicator of which argument is the
+problematic instance.
+-/
+
+class C (α : Type) where
+  v : Nat
+
+instance ic1 : C Nat := ⟨0⟩
+instance ic2 : C Nat := ⟨1⟩
+
+def myFn (α : Type) [c : C α] (x : Nat) : Nat := x + c.v
+
+open Lean Meta Elab Term in
+elab "test_mismatch" : term => do
+  let type ← elabTerm (← `(C Nat)) none
+  let mvar ← mkFreshExprMVar type (kind := .synthetic)
+  -- Pre-assign the instance mvar to `ic1`, then trigger type-class synthesis,
+  -- which (with `ic2` defined later and higher priority) produces a different value.
+  mvar.mvarId!.assign (Lean.mkConst ``ic1 [])
+  let app := mkAppN (Lean.mkConst ``myFn []) #[Lean.mkConst ``Nat [], mvar, Lean.mkNatLit 5]
+  let _ ← synthesizeInstMVarCore mvar.mvarId! (app? := app)
+  return app
+
+#check test_mismatch

tests/elab_fail/inst_arg_mismatch.lean.out.expected

@@ -0,0 +1,7 @@
+inst_arg_mismatch.lean:31:7-31:20: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules
+while elaborating instance argument #2 of
+  @myFn Nat ic1 5
+synthesized
+  ic2
+inferred
+  ic1