From f73615c3d201bdf18460d7985137135cbf8fd1bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 18 Mar 2021 14:23:03 -0700
Subject: [PATCH] fix: nontermination

---
 src/Lean/Elab/SyntheticMVars.lean                  | 6 +++++-
 tests/lean/autoBoundPostponeLoop.lean              | 7 +++++++
 tests/lean/autoBoundPostponeLoop.lean.expected.out | 1 +
 3 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/autoBoundPostponeLoop.lean
 create mode 100644 tests/lean/autoBoundPostponeLoop.lean.expected.out

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'