From ba4bfe26f2bf851a5f06c26c8b686ccc95079c73 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Mon, 26 Jun 2023 15:36:49 -0700
Subject: [PATCH] fix: add missing instantiateMVars

---
 src/Lean/Server/FileWorker/WidgetRequests.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 =>