From a7fcb7a07cdf633c6cd7656fa5917bf5ee5a84aa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 20 Oct 2020 15:49:51 -0700
Subject: [PATCH] feat: improve type ascription elaboration function

---
 src/Lean/Elab/BuiltinNotation.lean |  2 +-
 src/Lean/Elab/SyntheticMVars.lean  | 14 ++++++++++----
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index d9afa904ea..6d0339cd39 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -321,7 +321,7 @@ fun stx expectedType? =>
   match_syntax stx with
   | `(())           => pure $ Lean.mkConst `Unit.unit
   | `(($e : $type)) => do
-    let type ← withSynthesize $ elabType type
+    let type ← withSynthesize (mayPostpone := true) $ elabType type
     let e ← elabCDot e type
     ensureHasType type e
   | `(($e))         => elabCDot e expectedType?
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index a339a6d193..6263d50c5e 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -232,16 +232,22 @@ let rec loop (u : Unit) : TermElabM Unit := do
 loop ()
 
 def synthesizeSyntheticMVarsNoPostponing : TermElabM Unit :=
-synthesizeSyntheticMVars false
+synthesizeSyntheticMVars (mayPostpone := false)
 
-/-- Execute `k`, and make sure all pending synthetic metavariables created while executing `k` are solved. -/
-def withSynthesize {α} (k : TermElabM α) : TermElabM α := do
+/--
+  Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
+  If `mayPostpone == false`, then all of them must be synthesized.
+  Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
+def withSynthesize {α} (k : TermElabM α) (mayPostpone := false) : TermElabM α := do
 let s ← get
 let syntheticMVarsSaved := s.syntheticMVars
 modify fun s => { s with syntheticMVars := [] }
 try
   let a ← k
-  synthesizeSyntheticMVarsNoPostponing
+  synthesizeSyntheticMVars mayPostpone
+  if mayPostpone then
+    if (← synthesizeUsingDefault) then
+      synthesizeSyntheticMVars mayPostpone
   pure a
 finally
   modify fun s => { s with syntheticMVars := s.syntheticMVars ++ syntheticMVarsSaved }