fix: nontermination

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 :=

tests/lean/autoBoundPostponeLoop.lean

@@ -0,0 +1,7 @@
+theorem ex
+     (h₁ : α = β)
+     (as : List α)
+     (bs : List β)
+     (h₂ : (h ▸ as) = bs)
+     : True :=
+  True.intro

tests/lean/autoBoundPostponeLoop.lean.expected.out

@@ -0,0 +1 @@
+autoBoundPostponeLoop.lean:5:12-5:13: error: unknown identifier 'h'