From 72e7bf49998e3a8314a4e180673be37f676f371c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 4 Aug 2021 19:34:46 -0700
Subject: [PATCH] fix: `synthPending` bug

---
 src/Lean/Meta/SynthInstance.lean    |  2 +-
 tests/lean/run/synthPendingBug.lean | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/synthPendingBug.lean

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index c983ab7ec8..c090d430af 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -644,7 +644,7 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
     (fun _ => throwError "failed to synthesize{indentExpr type}")
 
 @[export lean_synth_pending]
-private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth do
+private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| withMVarContext mvarId do
   let mvarDecl ← getMVarDecl mvarId
   match mvarDecl.kind with
   | MetavarKind.synthetic =>
diff --git a/tests/lean/run/synthPendingBug.lean b/tests/lean/run/synthPendingBug.lean
new file mode 100644
index 0000000000..17c9dd730e
--- /dev/null
+++ b/tests/lean/run/synthPendingBug.lean
@@ -0,0 +1,15 @@
+inductive Nested
+| nest (a : Array Nested) : Nested
+
+class OfUnit (α : Type) where
+  ofUnit : Unit → Except String α
+
+instance myArrayInst [OfUnit α] : OfUnit (Array α) where
+  ofUnit _ := Except.error ""
+open OfUnit
+
+partial def ofUnitNested (_ : Unit) : Except String Nested := do
+  let localinst : OfUnit Nested := ⟨ofUnitNested⟩
+  let units : Array Unit ← Except.ok #[]
+  let a ← ofUnit ()
+  return Nested.nest a