From 08bfc27029d67500ec3372b4dc3d654f05dfa5c3 Mon Sep 17 00:00:00 2001 From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com> Date: Thu, 21 May 2026 17:12:38 +0000 Subject: [PATCH 1/3] experiment: improved 'synthsized type class instance is not definitionally equal' --- src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/SyntheticMVars.lean | 9 +++++- src/Lean/Elab/Term/TermElabM.lean | 30 ++++++++++++++++-- tests/elab_fail/inst_arg_mismatch.lean | 31 +++++++++++++++++++ .../inst_arg_mismatch.lean.out.expected | 7 +++++ 5 files changed, 74 insertions(+), 5 deletions(-) create mode 100644 tests/elab_fail/inst_arg_mismatch.lean create mode 100644 tests/elab_fail/inst_arg_mismatch.lean.out.expected diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 59274eea4886..c0fd09304a66 100644 --- a/src/Lean/Elab/App.lean +++ b/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 diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 7b7f039bfa57..18e149f956f5 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/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! diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index ccd3eda6525e..bab1929c99da 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/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}" diff --git a/tests/elab_fail/inst_arg_mismatch.lean b/tests/elab_fail/inst_arg_mismatch.lean new file mode 100644 index 000000000000..1bbd6437eede --- /dev/null +++ b/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 diff --git a/tests/elab_fail/inst_arg_mismatch.lean.out.expected b/tests/elab_fail/inst_arg_mismatch.lean.out.expected new file mode 100644 index 000000000000..efbf25adcf66 --- /dev/null +++ b/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 From c0bd0c6e3b21accd51da5281c802063d6923fcf8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 18 May 2026 19:21:00 +1000 Subject: [PATCH 2/3] feat: trace transparency level in `Meta.isDefEq` This PR adds two opt-in trace augmentations for debugging definitional equality. Setting `trace.Meta.isDefEq.printTransparency` prefixes each `Meta.isDefEq` `=?=` trace node with the current transparency level (e.g. `[default]`, `[instances]`, `[implicit]`). Enabling the new `Meta.isDefEq.transparency` trace class additionally logs the reason whenever `withInstanceConfig` or `withImplicitConfig` raises the transparency to check an instance-implicit or implicit-value argument. Implementation: adds a `ToString TransparencyMode` instance, registers the option and trace class, and instruments the two wrappers in `ExprDefEq.lean`. Both features are off by default and incur no cost when disabled. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Lean/Meta/ExprDefEq.lean | 12 +++++++++++- src/Lean/Meta/TransparencyMode.lean | 9 +++++++++ 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 43bf97a60cb1..f74e7d059ef7 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/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. @@ -2270,7 +2275,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 +2369,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 diff --git a/src/Lean/Meta/TransparencyMode.lean b/src/Lean/Meta/TransparencyMode.lean index 8f2ca2ff58ec..a1212812388f 100644 --- a/src/Lean/Meta/TransparencyMode.lean +++ b/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 From 2954e802e5cf6f1226c959ec805eb8320e334512 Mon Sep 17 00:00:00 2001 From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com> Date: Mon, 25 May 2026 10:15:46 +0000 Subject: [PATCH 3/3] experiment: always check types for instance metavariables at instances transparency --- src/Lean/Meta/ExprDefEq.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index f74e7d059ef7..92f9dd1d7261 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -492,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