diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean
index cde5794b339a..db51d8d2b2bf 100644
--- a/src/Lean/Elab/Calc.lean
+++ b/src/Lean/Elab/Calc.lean
@@ -144,6 +144,18 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
         throwAbortTerm
   throwTypeMismatchError "'calc' expression" expectedType resultType result
 
+/-!
+Warning! It is *very* tempting to try to improve `calc` so that it makes use of the expected type
+to unify with the LHS and RHS.
+Two people have already re-implemented `elabCalcSteps` trying to do so and then reverted the changes,
+not being aware of examples like https://github.com/leanprover/lean4/issues/2073
+
+The problem is that the expected type might need to be unfolded to get an accurate LHS and RHS.
+(Consider `≤` vs `≥`. Users expect to be able to use `calc` to prove `≥` using chained `≤`!)
+Furthermore, the types of the LHS and RHS do not need to be the same (consider `x ∈ S` as a relation),
+so we also cannot use the expected LHS and RHS as type hints.
+-/
+
 /-- Elaborator for the `calc` term mode variant. -/
 @[builtin_term_elab Lean.calc]
 def elabCalc : TermElab
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 92cd9964c928..5a6eeda9fa7d 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -219,9 +219,13 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
           let mvarDecl ← getMVarDecl mvarId
           unless (← MonadLog.hasErrors) do
             throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}{extraErrorMsg}"
-    | .coe expectedType e mkErrorMsg =>
+    | .coe header expectedType e f? mkErrorMsg? =>
       mvarId.withContext do
-        throwError (← mkErrorMsg mvarId expectedType e)
+        if let some mkErrorMsg := mkErrorMsg? then
+          throwError (← mkErrorMsg mvarId expectedType e)
+        else
+          throwTypeMismatchError header expectedType (← inferType e) e f?
+            m!"failed to create type class instance for{indentExpr (← getMVarDecl mvarId).type}"
     | _ => unreachable! -- TODO handle other cases.
 
 /--
@@ -385,7 +389,7 @@ mutual
     withRef mvarSyntheticDecl.stx do
     match mvarSyntheticDecl.kind with
     | .typeClass extraErrorMsg? => synthesizePendingInstMVar mvarId extraErrorMsg?
-    | .coe expectedType e _ => mvarId.withContext do
+    | .coe _header? expectedType e _f? _ => mvarId.withContext do
       if (← withDefault do isDefEq (← inferType e) expectedType) then
         -- Types may be defeq now due to mvar assignments, type class
         -- defaulting, etc.
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 7b3e320f3cf5..e12a3cf559ec 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -48,9 +48,15 @@ inductive SyntheticMVarKind where
   | typeClass (extraErrorMsg? : Option MessageData)
   /--
   Use coercion to synthesize value for the metavariable.
-  If synthesis fails, then the error `mkErrorMsg expectedType e` is thrown.
-  The `mkErrorMsg` function is allowed to throw an error itself. -/
-  | coe (expectedType : Expr) (e : Expr) (mkErrorMsg : MVarId → Expr → Expr → MetaM MessageData)
+  If synthesis fails, then throws an error.
+  - If `mkErrorMsg?` is provided, then the error `mkErrorMsg expectedType e` is thrown.
+    The `mkErrorMsg` function is allowed to throw an error itself.
+  - Otherwise, throws a default type mismatch error message.
+    If `header?` is not provided, the default header is "type mismatch".
+    If `f?` is provided, then throws an application type mismatch error.
+  -/
+  | coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
+      (mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData))
   /-- Use tactic to synthesize value for metavariable. -/
   | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind)
   /-- Metavariable represents a hole whose elaboration has been postponed. -/
@@ -1077,9 +1083,9 @@ def mkCoeErrorMsg (f? : Option Expr) (errorMsgHeader? : Option String) (mvarId :
   throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
     m!"failed to create type class instance for{indentExpr (← mvarId.getDecl).type}"
 
-def mkCoeWithErrorMsgs (expectedType : Expr) (e : Expr)
-    (mkImmedErrorMsg : (errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData)
-    (mkErrorMsg : MVarId → (expectedType e : Expr) → MetaM MessageData) : TermElabM Expr := do
+def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none)
+    (mkErrorMsg? : Option (MVarId → (expectedType e : Expr) → MetaM MessageData) := none)
+    (mkImmedErrorMsg? : Option ((errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData) := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
   try
     withoutMacroStackAtErr do
@@ -1088,19 +1094,24 @@ def mkCoeWithErrorMsgs (expectedType : Expr) (e : Expr)
       | .none => failure
       | .undef =>
         let mvarAux ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque
-        registerSyntheticMVarWithCurrRef mvarAux.mvarId! (.coe expectedType e mkErrorMsg)
+        registerSyntheticMVarWithCurrRef mvarAux.mvarId! (.coe errorMsgHeader? expectedType e f? mkErrorMsg?)
         return mvarAux
   catch
-    | .error _ msg => throwError (← mkImmedErrorMsg msg expectedType e)
-    | _            => throwError (← mkImmedErrorMsg none expectedType e)
-
-def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
-  mkCoeWithErrorMsgs expectedType e
-    (mkImmedErrorMsg := fun errorMsg? expectedType e => do
-      throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f? errorMsg?)
-    (mkErrorMsg := fun mvarId expectedType e => do
-      throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
-        m!"failed to create type class instance for{indentExpr (← mvarId.getDecl).type}")
+    | .error _ msg =>
+      if let some mkImmedErrorMsg := mkImmedErrorMsg? then
+        throwError (← mkImmedErrorMsg msg expectedType e)
+      else
+        throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f? msg
+    | _            =>
+      if let some mkImmedErrorMsg := mkImmedErrorMsg? then
+        throwError (← mkImmedErrorMsg none expectedType e)
+      else
+        throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
+
+def mkCoeWithErrorMsgs (expectedType : Expr) (e : Expr)
+    (mkImmedErrorMsg : (errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData)
+    (mkErrorMsg : MVarId → (expectedType e : Expr) → MetaM MessageData) : TermElabM Expr := do
+  mkCoe expectedType e (mkImmedErrorMsg? := mkImmedErrorMsg) (mkErrorMsg? := mkErrorMsg)
 
 /--
 If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally equal by inserting a coercion if necessary.