From 27be7e681247a0806ba8ac6224b03bf32e955fcf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Sep 2020 18:41:17 -0700
Subject: [PATCH] fix: leaking `isDefEqStuckExceptionId`

---
 src/Lean/Meta/SynthInstance.lean | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 9f3e9236c8..8c6ed27519 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -579,11 +579,14 @@ catchInternalId isDefEqStuckExceptionId
   (toLOptionM $ synthInstanceImp? type)
   (fun _ => pure LOption.undef)
 
-private def synthInstanceImp (type : Expr) : MetaM Expr := do
-result? ← synthInstanceImp? type;
-match result? with
-| some result => pure result
-| none        => throwError $ "failed to synthesize" ++ indentExpr type
+private def synthInstanceImp (type : Expr) : MetaM Expr :=
+catchInternalId isDefEqStuckExceptionId
+  (do
+    result? ← synthInstanceImp? type;
+    match result? with
+    | some result => pure result
+    | none        => throwError $ "failed to synthesize" ++ indentExpr type)
+  (fun _ => throwError $ "failed to synthesize" ++ indentExpr type)
 
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := do
 mvarDecl ← getMVarDecl mvarId;
@@ -593,7 +596,7 @@ match mvarDecl.kind with
   match c? with
   | none   => pure false
   | some _ => do
-    val? ← synthInstanceImp? mvarDecl.type;
+    val? ← catchInternalId isDefEqStuckExceptionId (synthInstanceImp? mvarDecl.type) (fun _ => pure none);
     match val? with
     | none     => pure false
     | some val =>