From 50a34bc1fe2ae2b129dc61299340ed1f2f4a3090 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 20 Oct 2020 14:54:57 -0700
Subject: [PATCH] fix: synthesize pending metavariables before
 `expectedType.hasMVar` test

---
 src/Lean/Elab/BuiltinNotation.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index f84385d6a3..f06e4a7297 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -162,6 +162,7 @@ if arg.isOfKind `Lean.Parser.Term.hole then
   match expectedType? with
   | none => throwError "invalid macro, expected type is not available"
   | some expectedType =>
+    synthesizeSyntheticMVars
     let expectedType ← instantiateMVars expectedType
     if expectedType.hasFVar || expectedType.hasMVar then
       throwError! "expected type must not contain free or meta variables{indentExpr expectedType}"