diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 4723597925..f04669e224 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -248,10 +248,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
       try
         for c in (← realizeGlobalConstWithInfos term) do
           addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
-          logInfoAt tk <| .ofPPFormat { pp := fun
-            | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
-            | none     => return f!"{c}"  -- should never happen
-          }
+          logInfoAt tk <| .signature c
           return
       catch _ => pure ()  -- identifier might not be a constant but constant + projection
     let e ← Term.elabTerm term none
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
index 1a00994229..1c3e214d0a 100644
--- a/src/Lean/Meta/Tactic/TryThis.lean
+++ b/src/Lean/Meta/Tactic/TryThis.lean
@@ -567,9 +567,10 @@ def addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool))
   -- thus giving more information in the hovers.
   -- Perhaps in future we will have a better way to attach elaboration information to
   -- `Syntax` embedded in a `MessageData`.
+  let toMessageData (e : Expr) : MessageData := if e.isConst then .ofConst e else .ofExpr e
   let mut tacMsg :=
     let rulesMsg := MessageData.sbracket <| MessageData.joinSep
-      (rules.map fun ⟨e, symm⟩ => (if symm then "← " else "") ++ m!"{e}") ", "
+      (rules.map fun ⟨e, symm⟩ => (if symm then "← " else "") ++ toMessageData e) ", "
     if let some loc := loc? then
       m!"rw {rulesMsg} at {loc}"
     else
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index e8ec1515ad..c8e89543c4 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -46,9 +46,6 @@ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (d
     let fmt ← ppTerm stx
     return ⟨fmt, infos⟩
 
-def ppConst (e : Expr) : MetaM Format := do
-  ppUsing e fun e => return (← delabCore e (delab := Delaborator.delabConst)).1
-
 @[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
   Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts, fileName := "<PrettyPrinter>", fileMap := default } { env := env }
@@ -101,4 +98,37 @@ unsafe def registerParserCompilers : IO Unit := do
   ParserCompiler.registerParserCompiler ⟨`formatter, formatterAttribute, combinatorFormatterAttribute⟩
 
 end PrettyPrinter
+
+namespace MessageData
+
+open Lean PrettyPrinter Delaborator
+
+/--
+Turns a `MetaM FormatWithInfos` into a `MessageData` using `.ofPPFormat` and running the monadic value in the given context.
+Uses the `pp.tagAppFns` option to annotate constants with terminfo, which is necessary for seeing the type on mouse hover.
+-/
+def ofFormatWithInfos
+    (fmt : MetaM FormatWithInfos)
+    (noContext : Unit → Format := fun _ => "<no context, could not generate MessageData>") : MessageData :=
+  .ofPPFormat
+  { pp := fun
+      | some ctx => ctx.runMetaM <| withOptions (pp.tagAppFns.set · true) fmt
+      | none => return noContext () }
+
+/-- Pretty print a const expression using `delabConst` and generate terminfo.
+This function avoids inserting `@` if the constant is for a function whose first
+argument is implicit, which is what the default `toMessageData` for `Expr` does.
+Panics if `e` is not a constant. -/
+def ofConst (e : Expr) : MessageData :=
+  if e.isConst then
+    .ofFormatWithInfos (PrettyPrinter.ppExprWithInfos (delab := delabConst) e) fun _ => f!"{e}"
+  else
+    panic! "not a constant"
+
+/-- Generates `MessageData` for a declaration `c` as `c.{<levels>} <params> : <type>`, with terminfo. -/
+def signature (c : Name) : MessageData :=
+  .ofFormatWithInfos (PrettyPrinter.ppSignature c) fun _ => f!"{c}"
+
+end MessageData
+
 end Lean
diff --git a/tests/lean/run/rewrites.lean b/tests/lean/run/rewrites.lean
index df72bb2324..a4f2750d35 100644
--- a/tests/lean/run/rewrites.lean
+++ b/tests/lean/run/rewrites.lean
@@ -4,7 +4,7 @@ private axiom test_sorry : ∀ {α}, α
 -- set_option trace.Tactic.rewrites.lemmas true
 
 /--
-info: Try this: rw [@List.map_append]
+info: Try this: rw [List.map_append]
 -- "no goals"
 -/
 #guard_msgs in