diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index a3918d62f3..4ad1e170cc 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -49,7 +49,7 @@ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
   | ⟨i⟩ => RequestM.asTask do
     i.ctx.runMetaM i.info.lctx do
       let type? ← match (← i.info.type?) with
-        | some type => some <$> ppExprTagged type
+        | some type => some <$> (ppExprTagged =<< instantiateMVars type)
         | none => pure none
       let exprExplicit? ← match i.info with
         | Elab.Info.ofTermInfo ti =>