fix: better defeq error messages

src/Lean/DefEqAttrib.lean

@@ -54,8 +54,11 @@ def validateDefEqAttr (declName : Name) : AttrM Unit := do
   MetaM.run' do withEqLhsRhs info.type fun lhs rhs => do
     let ok ← isDefEqCareful lhs rhs
     unless ok do
-      let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
-        let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
+      let config ← getConfig
+      let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) <| withConfig (fun _ => config) do
+        -- match the `smartUnfolding` setting of `isDefEqCareful`
+        let (lhs, rhs) ← withOptions (smartUnfolding.set · false) <|
+          addPPExplicitToExposeDiff lhs rhs
         let mut msg := m!"Not a definitional equality: the left-hand side{indentExpr lhs}\nis \
           not definitionally equal to the right-hand side{indentExpr rhs}"
         if (← getEnv).isExporting then

src/Lean/Elab/CheckTactic.lean

@@ -42,7 +42,7 @@ def elabCheckTactic : CommandElab := fun stx => do
       | [next] => do
         let (val, _, _) ← matchCheckGoalType stx (←next.getType)
         if !(← Meta.withReducible <| isDefEq val expTerm) then
-          let (val, expTerm) ← addPPExplicitToExposeDiff val expTerm
+          let (val, expTerm) ← Meta.withReducible <| addPPExplicitToExposeDiff val expTerm
           throwErrorAt stx
             m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
       | _ => do

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -447,7 +447,7 @@ where
         let e := (← fvarId.getValue?).get!
         let e' ← Tactic.elabTermEnsuringType v (← fvarId.getType)
         unless ← withAssignableSyntheticOpaque <| isDefEq e e' do
-          let (e, e') ← addPPExplicitToExposeDiff e e'
+          let (e, e') ← withAssignableSyntheticOpaque <| addPPExplicitToExposeDiff e e'
           throwErrorAt v "Provided term{indentExpr e'}\n\
             is not definitionally equal to{indentD m!"{Expr.fvar fvarId} := {e}"}"
         let mvars ← filterOldMVars (← getMVars e') mvarCounterSaved

src/Lean/Elab/Tactic/Change.lean

@@ -42,7 +42,8 @@ def elabChange (e : Expr) (p : Term) (mkDefeqError : Expr → Expr → MetaM Mes
     pure p
   withAssignableSyntheticOpaque do
     unless ← isDefEq p e do
-      throwError MessageData.ofLazyM (es := #[p, e]) do
+      let config ← getConfig
+      throwError MessageData.ofLazyM (es := #[p, e]) <| withConfig (fun _ => config) do
         let (p, tgt) ← addPPExplicitToExposeDiff p e
         mkDefeqError p tgt
     instantiateMVars p

src/Lean/Meta/Check.lean

@@ -78,7 +78,10 @@ partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
     -- but we don't want these assignments to leak out of the function.
     -- Note: we shouldn't instantiate mvars in `visit` to prevent leakage.
     withoutModifyingState do
-      visit (← instantiateMVars a) (← instantiateMVars b)
+      let traceState ← getTraceState
+      let r ← visit (← instantiateMVars a) (← instantiateMVars b)
+      setTraceState traceState
+      return r
 where
   visit (a b : Expr) : MetaM (Expr × Expr) := do
     try
@@ -224,7 +227,9 @@ function. Any expressions appearing in the trailing message should be included i
 def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr)
     (trailing? : Option MessageData := none) (trailingExprs : Array Expr := #[])
     : MetaM MessageData := do
-  return MessageData.ofLazyM (es := #[givenType, expectedType] ++ trailingExprs) do
+  let config ← getConfig
+  return MessageData.ofLazyM (es := #[givenType, expectedType] ++ trailingExprs) <|
+      withConfig (fun _ => config) do
     let mut msg ← (try
       let givenTypeType ← inferType givenType
       let expectedTypeType ← inferType expectedType

src/Lean/Meta/Tactic/Apply.lean

@@ -28,8 +28,10 @@ def getExpectedNumArgs (e : Expr) : MetaM Nat := do
 
 private def throwApplyError {α} (mvarId : MVarId)
     (eType : Expr) (conclusionType? : Option Expr) (targetType : Expr)
-    (term? : Option MessageData) : MetaM α := do
-  throwTacticEx `apply mvarId <| MessageData.ofLazyM (es := #[eType, targetType]) do
+    (term? : Option MessageData) (approx : Bool) : MetaM α := do
+  let config ← if approx then approxDefEq getConfig else getConfig
+  throwTacticEx `apply mvarId <| MessageData.ofLazyM (es := #[eType, targetType]) <|
+      withConfig (fun _ => config) do
     let conclusionType := conclusionType?.getD eType
     let note := if conclusionType?.isSome then .note m!"The full type of {term?.getD "the term"} is{indentExpr eType}" else m!""
     let (conclusionType, targetType) ← addPPExplicitToExposeDiff conclusionType targetType
@@ -215,7 +217,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
         else
           let (_, _, r) ← forallMetaTelescopeReducing eType (some rangeNumArgs.lower)
           pure (some r)
-        throwApplyError mvarId eType conclusionType? targetType term?
+        throwApplyError mvarId eType conclusionType? targetType term? cfg.approx
       termination_by rangeNumArgs.upper - i
     let (newMVars, binderInfos) ← go rangeNumArgs.lower
     postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances cfg.allowSynthFailures

src/Lean/Meta/Tactic/Rewrite.lean

@@ -46,7 +46,8 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let e ← instantiateMVars e
           let eAbst ← withConfig (fun oldConfig => { config, oldConfig with }) <| kabstract e lhs config.occs
           unless eAbst.hasLooseBVars do
-            let (tgt, pat) ← addPPExplicitToExposeDiff e lhs
+            let (tgt, pat) ← withConfig (fun oldConfig => { config, oldConfig with }) <|
+              addPPExplicitToExposeDiff e lhs
             throwTacticEx `rewrite mvarId m!"Did not find an occurrence of the pattern{indentExpr pat}\nin the target expression{indentExpr tgt}"
           -- construct rewrite proof
           let eNew := eAbst.instantiate1 rhs

src/Lean/Meta/Tactic/Rfl.lean

@@ -85,7 +85,8 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
 
   let success ← approxDefEq <| isDefEqGuarded lhs rhs
   unless success do
-    let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
+    let config ← approxDefEq getConfig
+    let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) <| withConfig (fun _ => config) do
       let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
       return m!"The left-hand side{indentExpr lhs}\nis not definitionally equal to the right-hand side{indentExpr rhs}"
     throwTacticEx `rfl goal explanation

tests/elab/addPPExplicitToExposeDiff.lean

@@ -64,6 +64,26 @@ but is expected to have type
 example : @f 1 2 := by
   exact (sorry : @f 0 _)
 
+def myId {x : Nat} : Nat := x
+def one : Nat := 1
+
+/-!
+Exposes an implicit argument nested inside an outer implicit argument because
+the out explicit arguments can be unified, but the outer implicit argument
+cannot, and its nested explicit arguments can be unified.
+-/
+/--
+error: Type mismatch
+  sorry
+has type
+  @f (@myId 1) 2
+but is expected to have type
+  @f (@myId one) 2
+-/
+#guard_msgs in
+example : @f (myId (x := one)) 2 := by
+  with_implicit exact (sorry : @f (myId (x := 1)) 2)
+
 /-!
 Add type ascriptions for numerals if they have different types.
 -/
@@ -162,3 +182,106 @@ but is expected to have type
 #guard_msgs in example (p : Nat → Prop) (d1 d2 : DecidablePred p) :
     {x : Nat // @decide _ (d1 x) = true} :=
   (sorry : {x : Nat // @decide _ (d2 x) = true})
+
+/-!
+`change` diagnoses at the transparency of the failed check.
+-/
+/--
+error: 'change' tactic failed, pattern
+  @f (@myId 1) 2
+is not definitionally equal to target
+  @f (@myId one) 2
+-/
+#guard_msgs in
+example : @f (myId (x := one)) 2 := by
+  with_reducible change @f (myId (x := 1)) 2
+
+/-!
+`#check_tactic` diagnoses at the reducible transparency of its check.
+-/
+/--
+error: Term reduces to
+  @myId one
+but is expected to reduce to ⏎
+  @myId 1
+-/
+#guard_msgs in
+#check_tactic (myId (x := one)) ~> myId (x := 1) by skip
+
+/-!
+`#check_tactic` diagnoses at the reducible transparency of its check.
+-/
+/--
+error: Term reduces to
+  @f (@myId one) 2
+but is expected to reduce to ⏎
+  @f (@myId 1) 2
+-/
+#guard_msgs in
+#check_tactic @f (myId (x := one)) 2 ~> @f (myId (x := 1)) 2 by skip
+
+/-!
+`rewrite` diagnoses at the transparency `kabstract` matched at.
+-/
+/--
+error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
+  @f (@myId 1) 2
+in the target expression
+  @f (@myId one) 2
+
+h : f 2 = True
+⊢ f 2
+-/
+#guard_msgs in
+example (h : @f (@myId 1) 2 = True) : @f (myId (x := one)) 2 := by
+  rewrite [h]
+
+/-!
+`apply` diagnoses at the configuration of the failed check.
+-/
+/--
+error: Tactic `apply` failed: could not unify the type of `h`
+  @f (@myId 1) 2
+with the goal
+  @f (@myId one) 2
+
+h : f 2
+⊢ f 2
+-/
+#guard_msgs in
+example (h : @f (@myId 1) 2) : @f (myId (x := one)) 2 := by
+  with_reducible apply h
+
+/-!
+`@[defeq]` diagnoses at the configuration of its defeq check (transparency `.all`), so the
+diff is not attributed to `one'` vs. `1`, which are defeq at that transparency.
+-/
+axiom testSorry : α
+@[irreducible] def one' : Nat := 1
+opaque a : Nat
+opaque b : Nat
+opaque g : {_ : Nat} → Nat → Nat
+
+/--
+error: Not a definitional equality: the left-hand side
+  @g a one'
+is not definitionally equal to the right-hand side
+  @g b 1
+-/
+#guard_msgs in
+@[defeq] theorem gEq : @g a one' = @g b 1 := testSorry
+
+/-!
+`clear_value` diagnoses with assignable synthetic opaque metavariables, matching its check, so
+the diff is attributed to `a` vs. `b` rather than to the assignable `?_`.
+-/
+/--
+error: Provided term
+  f ?_ ∧ @f b 2
+is not definitionally equal to
+  x := f 1 ∧ @f a 2
+-/
+#guard_msgs in
+example : True := by
+  let x : Prop := @f 1 1 ∧ @f a 2
+  clear_value (h : x = (@f 1 ?_ ∧ @f b 2))

tests/elab/implicitReducibleFunctorComp.lean

@@ -145,9 +145,9 @@ Full error:
   Application type mismatch: The argument
     G.map (F.map f)
   has type
-    @Quiver.Hom E inst✝.toQuiver (G.obj (F.obj X)) (G.obj (F.obj Y))
+    G.obj (F.obj X) ⟶ G.obj (F.obj Y)
   but is expected to have type
-    @Quiver.Hom E inst✝.toQuiver ((F ⋙ G).obj X) ((F ⋙ G).obj Y)
+    (F ⋙ G).obj X ⟶ (F ⋙ G).obj Y
   in the application
     Category.comp (G.map (F.map f))
 -/

tests/elab/linterTacticCheckInstances.lean

@@ -35,9 +35,9 @@ Full error:
   Application type mismatch: The argument
     h2
   has type
-    @LT.lt Nat instLTNat idx (composed s a b).s.decls.size
+    idx < (composed s a b).s.decls.size
   but is expected to have type
-    @LT.lt Nat instLTNat idx
+    idx <
       (have res := myF s { x := a };
             myF res.s { x := b }).s.decls.size
   in the application
@@ -62,9 +62,9 @@ Full error:
   Application type mismatch: The argument
     h1
   has type
-    @LT.lt Nat instLTNat idx s.decls.size
+    idx < s.decls.size
   but is expected to have type
-    @LT.lt Nat instLTNat idx (composed s a b).s.decls.size
+    idx < (composed s a b).s.decls.size
   in the application
     (composed s a b).s.decls[idx]
 

tests/elab/rflTacticErrors.lean

@@ -238,9 +238,9 @@ example : true'' = true   := by with_reducible apply_rfl -- Error
 
 /--
 error: Tactic `apply` failed: could not unify the conclusion of 'HEq.refl'
-  @HEq ?α ?a ?α ?a
+  ?a ≍ ?a
 with the goal
-  @HEq Bool true'' Bool true
+  true'' ≍ true
 
 Note: The full type of 'HEq.refl' is
   ∀ {α : Sort _} (a : α), a ≍ a

tests/elab/typeCheckNote.lean

@@ -97,9 +97,9 @@ Full error:
   Application type mismatch: The argument
     h2
   has type
-    @LT.lt Nat instLTNat idx (composed s a b).s.decls.size
+    idx < (composed s a b).s.decls.size
   but is expected to have type
-    @LT.lt Nat instLTNat idx
+    idx <
       (have res := myF s { x := a };
             myF res.s { x := b }).s.decls.size
   in the application