diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Util/Message.lean
index 0f25102843..1d9d7ded86 100644
--- a/src/Init/Lean/Util/Message.lean
+++ b/src/Init/Lean/Util/Message.lean
@@ -49,7 +49,7 @@ partial def formatAux : Option (Environment × MetavarContext × LocalContext) 
 | _, ofLevel u                     => fmt u
 | _, ofName n                      => fmt n
 | none, ofExpr e                   => format (toString e)
-| some (env, mctx, lctx), ofExpr e => format (toString e) -- TODO: invoke pretty printer
+| some (env, mctx, lctx), ofExpr e => format (toString (mctx.instantiateMVars e).1) -- TODO: invoke pretty printer
 | _, context env mctx lctx d       => formatAux (some (env, mctx, lctx)) d
 | ctx, tagged cls d                => Format.sbracket (format cls) ++ " " ++ formatAux ctx d
 | ctx, nest n d                    => Format.nest n (formatAux ctx d)