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 ()