feat: make MessageData.ofConstName be the default coercion from Name to MessageData

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -136,7 +136,7 @@ private def mkFormat (e : Expr) : MetaM Expr := do
     if eval.derive.repr.get (← getOptions) then
       if let .const name _ := (← whnf (← inferType e)).getAppFn then
         try
-          trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{MessageData.ofConstName name}'"
+          trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{name}'"
           liftCommandElabM do applyDerivingHandlers ``Repr #[name] none
           resetSynthInstanceCache
           return ← mkRepr e
@@ -201,9 +201,9 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
           discard <| withLocalDeclD `x ty fun x => mkT x
         catch _ =>
           throw ex
-        throwError m!"unable to synthesize '{MessageData.ofConstName ``MonadEval}' instance \
+        throwError m!"unable to synthesize '{``MonadEval}' instance \
           to adapt{indentExpr (← inferType e)}\n\
-          to '{MessageData.ofConstName ``IO}' or '{MessageData.ofConstName ``CommandElabM}'."
+          to '{``IO}' or '{``CommandElabM}'."
       addAndCompileExprForEval declName r (allowSorry := bang)
       -- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below.
       let r ← toMessageData <$> evalConst t declName

src/Lean/Elab/Deriving/TypeName.lean

@@ -14,7 +14,7 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool
   for declName in declNames do
     let cinfo ← getConstInfo declName
     unless cinfo.levelParams.isEmpty do
-      throwError m!"{mkConst declName} has universe level parameters"
+      throwError m!"{declName} has universe level parameters"
     elabCommand <| ← withFreshMacroScope `(
       unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
       @[implemented_by instImpl] opaque inst : TypeName @$(mkCIdent declName)

src/Lean/Elab/PreDefinition/Basic.lean

@@ -125,7 +125,7 @@ private def reportTheoremDiag (d : TheoremVal) : TermElabM Unit := do
     if proofSize > diagnostics.threshold.proofSize.get (← getOptions) then
       let sizeMsg := MessageData.trace { cls := `size } m!"{proofSize}" #[]
       let constOccs ← d.value.numApps (threshold := diagnostics.threshold.get (← getOptions))
-      let constOccsMsg ← constOccs.mapM fun (declName, numOccs) => return MessageData.trace { cls := `occs } m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {numOccs}" #[]
+      let constOccsMsg ← constOccs.mapM fun (declName, numOccs) => return MessageData.trace { cls := `occs } m!"{declName} ↦ {numOccs}" #[]
       -- let info
       logInfo <| MessageData.trace { cls := `theorem } m!"{d.name}" (#[sizeMsg] ++ constOccsMsg)
 

src/Lean/Elab/Print.lean

@@ -11,7 +11,7 @@ import Lean.Elab.Command
 namespace Lean.Elab.Command
 
 private def throwUnknownId (id : Name) : CommandElabM Unit :=
-  throwError "unknown identifier '{mkConst id}'"
+  throwError "unknown identifier '{format id}'"
 
 private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
   match levelParams with
@@ -38,7 +38,7 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   let (m, id) := match privateToUserName? id with
     | some id => (m ++ "private ", id)
     | none    => (m, id)
-  let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type
+  let m := m ++ kind ++ " " ++ format id ++ levelParamsToMessageData levelParams ++ " : " ++ type
   pure m
 
 private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=

src/Lean/Elab/StructInst.lean

@@ -434,7 +434,7 @@ private def expandParentFields (s : Struct) : TermElabM Struct := do
     | { lhs := .fieldName ref fieldName :: _,    .. } =>
       addCompletionInfo <| CompletionInfo.fieldId ref fieldName (← getLCtx) s.structName
       match findField? env s.structName fieldName with
-      | none => throwErrorAt ref "'{fieldName}' is not a field of structure '{MessageData.ofConstName s.structName}'"
+      | none => throwErrorAt ref "'{fieldName}' is not a field of structure '{s.structName}'"
       | some baseStructName =>
         if baseStructName == s.structName then pure field
         else match getPathToBaseStructure? env baseStructName s.structName with

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -452,7 +452,7 @@ where
       if r.isAppOf ``isTrue then
         return m!"\
           tactic '{tacticName}' failed. internal error: the elaborator is able to reduce the \
-          '{MessageData.ofConstName ``Decidable}' instance, but the kernel is not able to"
+          '{``Decidable}' instance, but the kernel is not able to"
       else if r.isAppOf ``isFalse then
         return m!"\
           tactic '{tacticName}' proved that the proposition\
@@ -466,42 +466,42 @@ where
         let unfoldedInsts ← unfolded |>.qsort Name.lt |>.filterMapM fun n => do
           let e ← mkConstWithLevelParams n
           if (← Meta.isClass? (← inferType e)) == ``Decidable then
-            return m!"'{MessageData.ofConst e}'"
+            return m!"'{n}'"
           else
             return none
         return (reason, unfoldedInsts)
       let stuckMsg :=
         if unfoldedInsts.isEmpty then
-          m!"Reduction got stuck at the '{MessageData.ofConstName ``Decidable}' instance{indentExpr reason}"
+          m!"Reduction got stuck at the '{``Decidable}' instance{indentExpr reason}"
         else
           let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
           m!"After unfolding the {instances} {MessageData.andList unfoldedInsts.toList}, \
-          reduction got stuck at the '{MessageData.ofConstName ``Decidable}' instance{indentExpr reason}"
+          reduction got stuck at the '{``Decidable}' instance{indentExpr reason}"
       let hint :=
         if reason.isAppOf ``Eq.rec then
           m!"\n\n\
-          Hint: Reduction got stuck on '▸' ({MessageData.ofConstName ``Eq.rec}), \
-          which suggests that one of the '{MessageData.ofConstName ``Decidable}' instances is defined using tactics such as 'rw' or 'simp'. \
+          Hint: Reduction got stuck on '▸' ({``Eq.rec}), \
+          which suggests that one of the '{``Decidable}' instances is defined using tactics such as 'rw' or 'simp'. \
           To avoid tactics, make use of functions such as \
-          '{MessageData.ofConstName ``inferInstanceAs}' or '{MessageData.ofConstName ``decidable_of_decidable_of_iff}' \
+          '{``inferInstanceAs}' or '{``decidable_of_decidable_of_iff}' \
           to alter a proposition."
         else if reason.isAppOf ``Classical.choice then
           m!"\n\n\
-          Hint: Reduction got stuck on '{MessageData.ofConstName ``Classical.choice}', \
-          which indicates that a '{MessageData.ofConstName ``Decidable}' instance \
+          Hint: Reduction got stuck on '{``Classical.choice}', \
+          which indicates that a '{``Decidable}' instance \
           is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
           The '{tacticName}' tactic works by evaluating a decision procedure via reduction, \
           and it cannot make progress with such instances. \
           This can occur due to the 'opened scoped Classical' command, which enables the instance \
-          '{MessageData.ofConstName ``Classical.propDecidable}'."
+          '{``Classical.propDecidable}'."
         else
           MessageData.nil
       return m!"\
         tactic '{tacticName}' failed for proposition\
         {indentExpr expectedType}\n\
-        since its '{MessageData.ofConstName ``Decidable}' instance\
+        since its '{``Decidable}' instance\
         {indentExpr s}\n\
-        did not reduce to '{MessageData.ofConstName ``isTrue}' or '{MessageData.ofConstName ``isFalse}'.\n\n\
+        did not reduce to '{``isTrue}' or '{``isFalse}'.\n\n\
         {stuckMsg}{hint}"
 
 @[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>

src/Lean/Elab/Tactic/Ext.lean

@@ -126,7 +126,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
         addAuxDeclarationRanges extName (← getRef) (← getRef)
     catch e =>
       throwError m!"\
-        Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
+        Failed to generate an 'ext' theorem for '{structName}': {e.toMessageData}"
   return extName
 
 /--
@@ -164,7 +164,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
         addAuxDeclarationRanges extName (← getRef) (← getRef)
     catch e =>
       throwError m!"\
-        Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\
+        Failed to generate an 'ext_iff' theorem from '{extName}': {e.toMessageData}\n\
         \n\
         Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem."
   return extIffName

src/Lean/Exception.lean

@@ -71,7 +71,7 @@ protected def throwError [Monad m] [MonadError m] (msg : MessageData) : m α :=
 
 /-- Throw an unknown constant error message. -/
 def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α :=
-  Lean.throwError m!"unknown constant '{mkConst constName}'"
+  Lean.throwError m!"unknown constant '{constName}'"
 
 /-- Throw an error exception using the given message data and reference syntax. -/
 protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α := do

src/Lean/Message.lean

@@ -12,6 +12,7 @@ import Lean.MetavarContext
 import Lean.Environment
 import Lean.Util.PPExt
 import Lean.Util.Sorry
+import Lean.Modifiers
 
 namespace Lean
 
@@ -168,8 +169,30 @@ def ofLevel (l : Level) : MessageData :=
       return Dynamic.mk msg)
     (fun _ => false)
 
+/--
+Simply formats the name.
+
+See `MessageData.ofConstName` for richer messages.
+-/
 def ofName (n : Name) : MessageData := ofFormat (format n)
 
+/--
+Represents a constant name such that hovering and "go to definition" works.
+If there is no such constant in the environment, the name is simply formatted.
+
+This function is used for the default `Name`-to-`MessageData` coercion.
+
+Use `MessageData.ofName` to prevent hovers.
+-/
+def ofConstName (constName : Name) (fullNames : Bool := true) : MessageData :=
+  .ofLazy
+    (fun ctx? => do
+      let msg ← ofFormatWithInfos <$> match ctx? with
+        | .none => pure (format constName)
+        | .some ctx => ppConstNameWithInfos { ctx with opts := ctx.opts.insert `pp.fullNames fullNames } constName
+      return Dynamic.mk msg)
+    (fun _ => false)
+
 partial def hasSyntheticSorry (msg : MessageData) : Bool :=
   visit none msg
 where
@@ -220,7 +243,7 @@ instance : Coe String MessageData := ⟨ofFormat ∘ format⟩
 instance : Coe Format MessageData := ⟨ofFormat⟩
 instance : Coe Level MessageData  := ⟨ofLevel⟩
 instance : Coe Expr MessageData   := ⟨ofExpr⟩
-instance : Coe Name MessageData   := ⟨ofName⟩
+instance : Coe Name MessageData   := ⟨ofConstName⟩
 instance : Coe Syntax MessageData := ⟨ofSyntax⟩
 instance : Coe MVarId MessageData := ⟨ofGoal⟩
 instance : Coe (Option Expr) MessageData := ⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
@@ -458,7 +481,7 @@ def stringToMessageData (str : String) : MessageData :=
 instance [ToFormat α] : ToMessageData α := ⟨MessageData.ofFormat ∘ format⟩
 instance : ToMessageData Expr          := ⟨MessageData.ofExpr⟩
 instance : ToMessageData Level         := ⟨MessageData.ofLevel⟩
-instance : ToMessageData Name          := ⟨MessageData.ofName⟩
+instance : ToMessageData Name          := ⟨MessageData.ofConstName⟩
 instance : ToMessageData String        := ⟨stringToMessageData⟩
 instance : ToMessageData Syntax        := ⟨MessageData.ofSyntax⟩
 instance : ToMessageData (TSyntax k)   := ⟨(MessageData.ofSyntax ·)⟩

src/Lean/Meta/Diagnostics.lean

@@ -43,7 +43,7 @@ def mkDiagSummary (cls : Name) (counters : PHashMap Name Nat) (p : Name → Bool
   else
     let mut data := #[]
     for (declName, counter) in entries do
-      data := data.push <| .trace { cls } m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
+      data := data.push <| .trace { cls } m!"{declName} ↦ {counter}" #[]
     return { data, max := entries[0]!.2 }
 
 def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do

src/Lean/Meta/Match/Basic.lean

@@ -280,7 +280,7 @@ partial def varsToUnderscore : Example → Example
 partial def toMessageData : Example → MessageData
   | var fvarId        => mkFVar fvarId
   | ctor ctorName []  => mkConst ctorName
-  | ctor ctorName exs => m!"({mkConst ctorName}{exs.foldl (fun msg pat => m!"{msg} {toMessageData pat}") Format.nil})"
+  | ctor ctorName exs => m!"({MessageData.ofConstName ctorName false}{exs.foldl (fun msg pat => m!"{msg} {toMessageData pat}") Format.nil})"
   | arrayLit exs      => "#" ++ MessageData.ofList (exs.map toMessageData)
   | val e             => e
   | underscore        => "_"

src/Lean/Meta/Tactic/Simp/Diagnostics.lean

@@ -13,7 +13,7 @@ private def originToKey (thmId : Origin) : MetaM MessageData := do
   match thmId with
   | .decl declName _ _ =>
     if (← getEnv).contains declName then
-      pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}"
+      pure m!"{declName}"
     else
       pure m!"{declName} (builtin simproc)"
   | .fvar fvarId => pure m!"{mkFVar fvarId}"

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -200,7 +200,7 @@ private def reduceStep (e : Expr) : SimpM Expr := do
       return e.letBody!.instantiate1 e.letValue!
   match (← unfold? e) with
   | some e' =>
-    trace[Meta.Tactic.simp.rewrite] "unfold {mkConst e.getAppFn.constName!}, {e} ==> {e'}"
+    trace[Meta.Tactic.simp.rewrite] "unfold {e.getAppFn.constName!}, {e} ==> {e'}"
     recordSimpTheorem (.decl e.getAppFn.constName!)
     return e'
   | none => foldRawNatLit e

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -165,12 +165,11 @@ instance : ToFormat SimpTheorem where
 
 def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
   | .decl n post inv => do
-    let r := MessageData.ofConst (← mkConstWithLevelParams n)
     match post, inv with
-    | true,  true  => return m!"← {r}"
-    | true,  false => return r
-    | false, true  => return m!"↓ ← {r}"
-    | false, false => return m!"↓ {r}"
+    | true,  true  => return m!"← {n}"
+    | true,  false => return n
+    | false, true  => return m!"↓ ← {n}"
+    | false, false => return m!"↓ {n}"
   | .fvar n => return mkFVar n
   | .stx _ ref => return ref
   | .other n => return n

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -116,7 +116,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
             else
               match caseName? with
               | none => throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}"
-              | some caseName => throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}\nat case {mkConst caseName}"
+              | some caseName => throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}\nat case {format caseName}"
         let a ← instantiateMVars a
         let b ← instantiateMVars b
         match a, b with

src/Lean/MonadEnv.lean

@@ -92,7 +92,7 @@ def mkAuxName [Monad m] [MonadEnv m] (baseName : Name) (idx : Nat) : m Name := d
 def getConstInfo [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m ConstantInfo := do
   match (← getEnv).find? constName with
   | some info => pure info
-  | none      => throwError "unknown constant '{mkConst constName}'"
+  | none      => throwError "unknown constant '{constName}'"
 
 def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Expr := do
   let info ← getConstInfo constName
@@ -101,22 +101,22 @@ def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Na
 def getConstInfoDefn [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m DefinitionVal := do
   match (← getConstInfo constName) with
   | ConstantInfo.defnInfo v => pure v
-  | _                       => throwError "'{mkConst constName}' is not a definition"
+  | _                       => throwError "'{constName}' is not a definition"
 
 def getConstInfoInduct [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m InductiveVal := do
   match (← getConstInfo constName) with
   | ConstantInfo.inductInfo v => pure v
-  | _                         => throwError "'{mkConst constName}' is not a inductive type"
+  | _                         => throwError "'{constName}' is not a inductive type"
 
 def getConstInfoCtor [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m ConstructorVal := do
   match (← getConstInfo constName) with
   | ConstantInfo.ctorInfo v => pure v
-  | _                       => throwError "'{mkConst constName}' is not a constructor"
+  | _                       => throwError "'{constName}' is not a constructor"
 
 def getConstInfoRec [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m RecursorVal := do
   match (← getConstInfo constName) with
   | ConstantInfo.recInfo v => pure v
-  | _                      => throwError "'{mkConst constName}' is not a recursor"
+  | _                      => throwError "'{constName}' is not a recursor"
 
 @[inline] def matchConstStruct [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → ConstructorVal → m α) : m α :=
   matchConstInduct e failK fun ival us => do