chore: remove @ from rw? suggestions, and enable hover on constants in #check (#3911)

* Replaces the unused `Lean.PrettyPrinter.ppConst` with
`MessageData.ofConst` (which similarly avoids an unnecessary `@`) and
that further generates a hover for the constant

* Uses this in `TryThis.addRewriteSuggestion`, so that `rw?` suggestions
don't have unnecessary `@`s.

* Add `MessageData.signature`, as a wrapper around
`PrettyPrinter.signature`, using the same machinery to generate hovers
for constants, improving the hover behaviour in #check so that we get
second order pop-up for constants in the signature. (Not sure how to
write tests for second order hovers, so there is no test for this.)

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

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

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

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