From 14de4e69656b45f0f758610fc911d8951f63cf30 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Dec 2019 18:52:31 -0800
Subject: [PATCH] feat: add `trySynthInstance`

---
 src/Init/Lean/LOption.lean            |  3 +++
 src/Init/Lean/Meta/SynthInstance.lean | 20 +++++++++++++++++---
 2 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/LOption.lean b/src/Init/Lean/LOption.lean
index 790d45842a..c5ab751788 100644
--- a/src/Init/Lean/LOption.lean
+++ b/src/Init/Lean/LOption.lean
@@ -36,3 +36,6 @@ end Lean
 def Option.toLOption {α : Type u} : Option α → Lean.LOption α
 | none   => Lean.LOption.none
 | some a => Lean.LOption.some a
+
+@[inline] def toLOptionM {α} {m : Type → Type} [Monad m] (x : m (Option α)) : m (Lean.LOption α) :=
+do b ← x; pure b.toLOption
diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean
index 93e32da3e2..a3f5995a37 100644
--- a/src/Init/Lean/Meta/SynthInstance.lean
+++ b/src/Init/Lean/Meta/SynthInstance.lean
@@ -157,12 +157,14 @@ forallTelescope type $ fun xs typeBody =>
   | _ => pure (type, {})
 
 private def resolveReplacements (r : Replacements) : MetaM Bool :=
-r.levelReplacements.allM (fun ⟨u, u'⟩ => isLevelDefEqAux u u')
-<&&>
-r.exprReplacements.allM (fun ⟨e, e'⟩ => isExprDefEqAux e e')
+try $
+  r.levelReplacements.allM (fun ⟨u, u'⟩ => isLevelDefEqAux u u')
+  <&&>
+  r.exprReplacements.allM (fun ⟨e, e'⟩ => isExprDefEqAux e e')
 
 def synthInstance (type : Expr) : MetaM (Option Expr) :=
 usingTransparency TransparencyMode.reducible $ do
+  type ← instantiateMVars type;
   type ← preprocess type;
   s ← get;
   match s.cache.synthInstance.find type with
@@ -188,5 +190,17 @@ usingTransparency TransparencyMode.reducible $ do
     else
       pure result
 
+/--
+  Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if
+  instance cannot be synthesized right now because `type` contains metavariables. -/
+def trySynthInstance (type : Expr) : MetaM (LOption Expr) :=
+adaptReader (fun (ctx : Context) => { config := { isDefEqStuckEx := true, .. ctx.config }, .. ctx }) $
+  catch
+    (toLOptionM $ synthInstance type)
+    (fun ex => match ex with
+      | Exception.isExprDefEqStuck _ _ _  => pure LOption.undef
+      | Exception.isLevelDefEqStuck _ _ _ => pure LOption.undef
+      | _                                 => throw ex)
+
 end Meta
 end Lean