diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 7b7f039bfa57..56a1d9b4150e 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -76,8 +76,19 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
 /--
   Similar to `synthesizeInstMVarCore`, but makes sure that `instMVar` local context and instances
   are used. It also logs any error message produced. -/
+register_builtin_option Elab.tcSkipUnchanged : Bool := {
+  defValue := false
+  descr := "skip re-attempting a pending typeclass metavariable whose instantiated goal     type is unchanged since its last failed attempt (the outcome is deterministic in the     goal, so re-attempting is wasted work; the resumption loop is otherwise quadratic in     the number of chained pending instances)"
+}
+
 private def synthesizePendingInstMVar (instMVar : MVarId) (extraErrorMsg? : Option MessageData := none): TermElabM Bool :=
   instMVar.withContext do
+    if Elab.tcSkipUnchanged.get (← getOptions) then
+      let type ← instantiateMVars (← instMVar.getType)
+      if let some prev := (← get).tcSynthAttempt.get? instMVar then
+        if prev == type then
+          return false
+      modify fun s => { s with tcSynthAttempt := s.tcSynthAttempt.insert instMVar type }
     try
       synthesizeInstMVarCore instMVar (extraErrorMsg? := extraErrorMsg?)
     catch
diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean
index 4d848e0860a2..dc0c25bfcb4e 100644
--- a/src/Lean/Elab/Term/TermElabM.lean
+++ b/src/Lean/Elab/Term/TermElabM.lean
@@ -181,6 +181,11 @@ structure State where
   levelNames        : List Name       := []
   syntheticMVars    : MVarIdMap SyntheticMVarDecl := {}
   pendingMVars      : List MVarId := {}
+  /-- Last instantiated goal type per still-pending `.typeClass` mvar whose synthesis
+  attempt failed; used (option `Elab.tcSkipUnchanged`) to skip re-attempts when the
+  goal is unchanged — the resumption loop otherwise re-tries every pending TC mvar
+  after each single success, which is quadratic in chained-literal statements. -/
+  tcSynthAttempt    : MVarIdMap Expr := {}
   /-- List of errors associated to a metavariable that are shown to the user if the metavariable could not be fully instantiated -/
   mvarErrorInfos    : List MVarErrorInfo := []
   /-- List of data to be able to localize universe level metavariable errors to particular expressions. -/