remove defeqhint

src/Lean/Elab/SyntheticMVars.lean

@@ -226,9 +226,6 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
         else
           throwTypeMismatchError header expectedType (← inferType e) e f?
             m!"failed to create type class instance for{indentExpr (← getMVarDecl mvarId).type}"
-    | .defeqHint .. =>
-      -- This is just a hint, so we simply forget about it.
-      pure ()
     | _ => unreachable! -- TODO handle other cases.
 
 /--
@@ -413,13 +410,6 @@ mutual
           return true
         else
           return false
-    | .defeqHint e t => mvarId.withContext do
-      try
-        withTransparency t <| isDefEq (.mvar mvarId) e
-      catch _ =>
-        -- If isDefEq throws an error, assume that isDefEq will never succeed.
-        -- This can happen for example if expressions are not type correct at the given transparency level.
-        return true
   /--
     Try to synthesize the current list of pending synthetic metavariables.
     Return `true` if at least one of them was synthesized. -/

src/Lean/Elab/Tactic/Change.lean

@@ -21,7 +21,14 @@ Unlike `(show p from ?m : e)`, this can assign synthetic opaque metavariables ap
 def elabChange (e : Expr) (p : Term) : TacticM Expr := do
   let p ← runTermElab do
     let p ← Term.elabTermEnsuringType p (← inferType e)
-    Term.registerDefeqHint p e
+    unless ← isDefEq p e do
+      /-
+      Sometimes isDefEq can fail due to postponed elaboration problems.
+      We synthesize pending synthetic mvars while allowing typeclass instances to be postponed,
+      which might enable solving for them with an additional `isDefEq`.
+      -/
+      Term.synthesizeSyntheticMVars (postpone := .partial)
+      discard <| isDefEq p e
     pure p
   withAssignableSyntheticOpaque do
     unless ← isDefEq p e do

src/Lean/Elab/Term.lean

@@ -61,8 +61,6 @@ inductive SyntheticMVarKind where
   | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind)
   /-- Metavariable represents a hole whose elaboration has been postponed. -/
   | postponed (ctx : SavedContext)
-  /-- A hint that the metavariable is ideally defeq to `e`. -/
-  | defeqHint (e : Expr) (t : Meta.TransparencyMode)
   deriving Inhabited
 
 /--
@@ -77,7 +75,6 @@ instance : ToString SyntheticMVarKind where
     | .coe ..       => "coe"
     | .tactic ..    => "tactic"
     | .postponed .. => "postponed"
-    | .defeqHint .. => "defeq hint"
 
 structure SyntheticMVarDecl where
   stx : Syntax
@@ -1134,16 +1131,6 @@ def ensureHasTypeWithErrorMsgs (expectedType? : Option Expr) (e : Expr)
   else
     mkCoeWithErrorMsgs expectedType e mkImmedErrorMsg mkErrorMsg
 
-/--
-Registers a hint that `e` and `e'` are ideally defeq if they are not already defeq.
-This hint gets interleaved between elaboration tasks.
--/
-def registerDefeqHint (e e' : Expr) : TermElabM Unit := do
-  unless ← isDefEq e e' do
-    let mvar ← mkFreshExprMVar (← inferType e)
-    mvar.mvarId!.assign e
-    registerSyntheticMVarWithCurrRef mvar.mvarId! (.defeqHint e' (← getTransparency))
-
 /--
   Create a synthetic sorry for the given expected type. If `expectedType? = none`, then a fresh
   metavariable is created to represent the type.

tests/lean/run/change.lean

@@ -41,8 +41,8 @@ noncomputable example : Nat := by
 def foo (a b c : Nat) := if a < b then c else 0
 
 /-!
-The first `change` would fail with `typeclass instance problem is stuck`
-if there weren't defeq hints in the elaborator (`SyntheticMVarKind.defeqHint`)
+The first `change` would fail with `typeclass instance problem is stuck` if we did not have
+the `Term.synthesizeSyntheticMVars (postpone := .partial); discard <| isDefEq p e` hint
 -/
 example : foo 1 2 3 = 3 := by
   change (if _ then _ else _) = _