diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 033e9cea05d7..193c311b2711 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -107,7 +107,8 @@ def lazy (f : PPContext → IO MessageData)
     (hasSyntheticSorry : MetavarContext → Bool := fun _ => false) : MessageData :=
   .ofLazy (hasSyntheticSorry := hasSyntheticSorry) fun ctx? => do
     let msg ← match ctx? with
-      | .none => pure (.ofFormat "(invalid MessageData.lazy, missing context)")
+      | .none =>
+        pure (.ofFormat "(invalid MessageData.lazy, missing context)") -- see `addMessageContext`
       | .some ctx => f ctx
     return Dynamic.mk msg
 
@@ -141,14 +142,31 @@ def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
 def ofSyntax (stx : Syntax) : MessageData :=
   -- discard leading/trailing whitespace
   let stx := stx.copyHeadTailInfoFrom .missing
-  .lazy fun ctx => ofFormat <$> ppTerm ctx ⟨stx⟩ -- HACK: might not be a term
+  .ofLazy
+    (fun ctx? => do
+      let msg ← ofFormat <$> match ctx? with
+        | .none => pure stx.formatStx
+        | .some ctx => ppTerm ctx ⟨stx⟩ -- HACK: might not be a term
+      return Dynamic.mk msg)
+    (fun _ => false)
 
 def ofExpr (e : Expr) : MessageData :=
-  .lazy (fun ctx => ofFormatWithInfos <$> ppExprWithInfos ctx e)
-        (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry)
+  .ofLazy
+    (fun ctx? => do
+      let msg ← ofFormatWithInfos <$> match ctx? with
+        | .none => pure (format (toString e))
+        | .some ctx => ppExprWithInfos ctx e
+      return Dynamic.mk msg)
+    (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry)
 
 def ofLevel (l : Level) : MessageData :=
-  .lazy fun ctx => ofFormat <$> ppLevel ctx l
+  .ofLazy
+    (fun ctx? => do
+      let msg ← ofFormat <$> match ctx? with
+        | .none => pure (format l)
+        | .some ctx => ppLevel ctx l
+      return Dynamic.mk msg)
+    (fun _ => false)
 
 def ofName (n : Name) : MessageData := ofFormat (format n)
 
@@ -385,6 +403,13 @@ def indentExpr (e : Expr) : MessageData :=
   indentD e
 
 class AddMessageContext (m : Type → Type) where
+  /-- 
+  Without context, a `MessageData` object may be be missing information
+  (e.g. hover info) for pretty printing, or may print an error. Hence,
+  `addMessageContext` should be called on all constructed `MessageData`
+  (e.g. via `m!`) before taking it out of context (e.g. leaving `MetaM` or
+  `CoreM`).
+  -/
   addMessageContext : MessageData → m MessageData
 
 export AddMessageContext (addMessageContext)