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