diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 83487f13a0..8c0eb1734c 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -294,7 +294,11 @@ mutual
               loop ()
             else
               reportStuckSyntheticMVars
-    loop ()
+    /- Disable `autoBoundImplicit` to avoid nontermination.
+      The postponed terms have a fixed `localContext`, i.e. the context of the metavariable representing the "hole".
+      `throwAutoBoundImplicit` exception will have not effect. -/
+    withReader (fun ctx => { ctx with autoBoundImplicit := false }) do
+      loop ()
 end
 
 def synthesizeSyntheticMVarsNoPostponing : TermElabM Unit :=
diff --git a/tests/lean/autoBoundPostponeLoop.lean b/tests/lean/autoBoundPostponeLoop.lean
new file mode 100644
index 0000000000..24b7a911df
--- /dev/null
+++ b/tests/lean/autoBoundPostponeLoop.lean
@@ -0,0 +1,7 @@
+theorem ex
+     (h₁ : α = β)
+     (as : List α)
+     (bs : List β)
+     (h₂ : (h ▸ as) = bs)
+     : True :=
+  True.intro
diff --git a/tests/lean/autoBoundPostponeLoop.lean.expected.out b/tests/lean/autoBoundPostponeLoop.lean.expected.out
new file mode 100644
index 0000000000..5b7b464206
--- /dev/null
+++ b/tests/lean/autoBoundPostponeLoop.lean.expected.out
@@ -0,0 +1 @@
+autoBoundPostponeLoop.lean:5:12-5:13: error: unknown identifier 'h'