experiment: always check types for instance metavariables at instance transparency

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}"

src/Lean/Meta/ExprDefEq.lean

@@ -79,6 +79,11 @@ register_builtin_option backward.isDefEq.implicitBump : Bool := {
   not just instance-implicit ones"
 }
 
+register_builtin_option trace.Meta.isDefEq.printTransparency : Bool := {
+  defValue := false
+  descr    := "if true, prefix `Meta.isDefEq` `=?=` trace messages with the current transparency level"
+}
+
 /--
   Return `true` if `e` is of the form `fun (x_1 ... x_n) => ?m y_1 ... y_k)`, and `?m` is unassigned.
   Remark: `n`, `k` may be 0.
@@ -487,7 +492,20 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
       let mvarType ← inferType mvar
       let vType ← inferType v
       if (← respectTransparencyAtTypes) then
-        withImplicitConfig do
+        -- For instance metavariables — those created for an instance-implicit (`[..]`) parameter,
+        -- identified by `.synthetic` kind together with a class type — cap the transparency at
+        -- exactly `.instances` so an ambient `.default`/`.all` does not let semireducible
+        -- definitions be unfolded while checking the type of an instance assignment. This
+        -- intentionally does not apply to ordinary implicit (`{..}`) metavariables that happen
+        -- to have a class type, which are created with `.natural` kind.
+        let isInstance ←
+          if (← mvar.mvarId!.getKind) matches .synthetic then
+            pure (← isClass? mvarType).isSome
+          else
+            pure false
+        let capInstance (x : MetaM Bool) : MetaM Bool :=
+          if isInstance then withTransparency .instances x else x
+        capInstance <| withImplicitConfig do
           if (← Meta.isExprDefEqAux mvarType vType) then
             mvar.mvarId!.assign v
             return true
@@ -2270,7 +2288,11 @@ private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
 set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
-  withTraceNodeBefore `Meta.isDefEq (fun _ => return m!"{t} =?= {s}") do
+  withTraceNodeBefore `Meta.isDefEq (fun _ => do
+    if trace.Meta.isDefEq.printTransparency.get (← getOptions) then
+      return m!"[{toString (← getTransparency)}] {t} =?= {s}"
+    else
+      return m!"{t} =?= {s}") do
   checkSystem "isDefEq"
   whenUndefDo (isDefEqQuick t s) do
   whenUndefDo (isDefEqProofIrrel t s) do
@@ -2360,5 +2382,6 @@ builtin_initialize
   registerTraceClass `Meta.isDefEq.assign.occursCheck (inherited := true)
   registerTraceClass `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx (inherited := true)
   registerTraceClass `Meta.isDefEq.eta.struct
+  registerTraceClass `Meta.isDefEq.transparency (inherited := true)
 
 end Lean.Meta

src/Lean/Meta/TransparencyMode.lean

@@ -23,6 +23,15 @@ def hash : TransparencyMode → UInt64
 
 instance : Hashable TransparencyMode := ⟨hash⟩
 
+protected def toString : TransparencyMode → String
+  | all       => "all"
+  | default   => "default"
+  | reducible => "reducible"
+  | instances => "instances"
+  | none      => "none"
+
+instance : ToString TransparencyMode := ⟨TransparencyMode.toString⟩
+
 def lt : TransparencyMode → TransparencyMode → Bool
   | _,         none      => false
   | none,      _         => true

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