From 9715bc773803d3e02f4fda0e6ec7acff78fb0315 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Dec 2019 06:57:50 -0800
Subject: [PATCH] fix: missing `instantiateMVars`

---
 src/Init/Lean/Meta/SynthInstance.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean
index 799ff92ed7..198d30cdc9 100644
--- a/src/Init/Lean/Meta/SynthInstance.lean
+++ b/src/Init/Lean/Meta/SynthInstance.lean
@@ -194,6 +194,7 @@ def newSubgoal (mctx : MetavarContext) (key : Expr) (mvar : Expr) (waiter : Wait
 withMCtx mctx $ do
   trace `Meta.synthInstance.newSubgoal $ fun _ => key;
   mvarType  ← inferType mvar;
+  mvarType  ← instantiateMVars mvarType;
   instances ← getInstances mvarType;
   mctx      ← getMCtx;
   if instances.isEmpty then pure ()