chore: move MessageData.ofConstName earlier (#5877)

Makes `MessageData.ofConstName` available without needing to import the
pretty printer. Any code making use of `MessageData` can write `m!" ...
{.ofConstName n} ... "` to have the name print with hover information.
More error messages now have hover information.

* Now `.ofConstName` also has a boolean flag to make names print fully
qualified. Default: false.
* Now `.ofConstName` will sanitize names that aren't constants. It is OK
to use it in `"unknown constant '{.ofConstName constName}'"` errors.

Usability note: it is more user-friendly to have "has already been
declared" errors report the fully qualified name. For this, write
`m!"{.ofConstName n true} has already been declared"`.

src/Lean/Class.lean

@@ -87,7 +87,7 @@ def hasOutParams (env : Environment) (declName : Name) : Bool :=
   incorrect. This transformation would be counterintuitive to users since
   we would implicitly treat these regular parameters as `outParam`s.
 -/
-private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except String (Array Nat) :=
+private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except MessageData (Array Nat) :=
   match type with
   | .forallE _ d b bi =>
     let addOutParam (_ : Unit) :=
@@ -102,7 +102,7 @@ private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (ou
         /- See issue #1852 for a motivation for `bi.isInstImplicit` -/
         addOutParam ()
       else
-        Except.error s!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`"
+        Except.error m!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`"
     else
       checkOutParam (i+1) outParamFVarIds outParams b
   | _ => return outParams
@@ -149,13 +149,13 @@ and it must be the name of constant in `env`.
 `declName` must be a inductive datatype or axiom.
 Recall that all structures are inductive datatypes.
 -/
-def addClass (env : Environment) (clsName : Name) : Except String Environment := do
+def addClass (env : Environment) (clsName : Name) : Except MessageData Environment := do
   if isClass env clsName then
-    throw s!"class has already been declared '{clsName}'"
+    throw m!"class has already been declared '{.ofConstName clsName true}'"
   let some decl := env.find? clsName
-    | throw s!"unknown declaration '{clsName}'"
+    | throw m!"unknown declaration '{clsName}'"
   unless decl matches .inductInfo .. | .axiomInfo .. do
-    throw s!"invalid 'class', declaration '{clsName}' must be inductive datatype, structure, or constant"
+    throw m!"invalid 'class', declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant"
   let outParams ← checkOutParam 0 #[] #[] decl.type
   return classExtension.addEntry env { name := clsName, outParams }
 

src/Lean/Elab/DeclModifiers.lean

@@ -25,19 +25,19 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
   if env.contains declName then
     addInfo declName
     match privateToUserName? declName with
-    | none          => throwError "'{declName}' has already been declared"
-    | some declName => throwError "private declaration '{declName}' has already been declared"
+    | none          => throwError "'{.ofConstName declName true}' has already been declared"
+    | some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared"
   if isReservedName env declName then
     throwError "'{declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)
-    throwError "a private declaration '{declName}' has already been declared"
+    throwError "a private declaration '{.ofConstName declName true}' has already been declared"
   match privateToUserName? declName with
   | none => pure ()
   | some declName =>
     if env.contains declName then
       addInfo declName
-      throwError "a non-private declaration '{declName}' has already been declared"
+      throwError "a non-private declaration '{.ofConstName declName true}' has already been declared"
 
 /-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/
 inductive Visibility where

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!"{.ofConstName 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/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 '{.ofConstName id}'"
 
 private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
   match levelParams with

src/Lean/Elab/Structure.lean

@@ -318,7 +318,7 @@ where
     if h : i < subfieldNames.size then
       let subfieldName := subfieldNames.get ⟨i, h⟩
       if containsFieldName infos subfieldName then
-        throwError "field '{subfieldName}' from '{parentStructName}' has already been declared"
+        throwError "field '{subfieldName}' from '{.ofConstName parentStructName}' has already been declared"
       let val  ← mkProjection parentFVar subfieldName
       let type ← inferType val
       withLetDecl subfieldName type val fun subfieldFVar => do
@@ -428,7 +428,7 @@ private partial def copyDefaultValue? (fieldMap : FieldMap) (expandedStructNames
     go? (← instantiateValueLevelParams cinfo us)
 where
   failed : TermElabM (Option Expr) := do
-    logWarning s!"ignoring default value for field '{fieldName}' defined at '{structName}'"
+    logWarning m!"ignoring default value for field '{fieldName}' defined at '{.ofConstName structName}'"
     return none
 
   go? (e : Expr) : TermElabM (Option Expr) := do
@@ -464,7 +464,7 @@ where
         | some existingFieldInfo =>
           let existingFieldType ← inferType existingFieldInfo.fvar
           unless (← isDefEq fieldType existingFieldType) do
-            throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
+            throwError "parent field type mismatch, field '{fieldName}' from parent '{.ofConstName parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
           /- Remark: if structure has a default value for this field, it will be set at the `processOveriddenDefaultValues` below. -/
           copy (i+1) infos (fieldMap.insert fieldName existingFieldInfo.fvar) expandedStructNames
         | none =>
@@ -543,10 +543,10 @@ where
       let parentType ← whnf type
       let parentStructName ← getStructureName parentType
       if parents.any (fun info => info.structName == parentStructName) then
-        logWarningAt parent m!"duplicate parent structure '{parentStructName}'"
+        logWarningAt parent m!"duplicate parent structure '{.ofConstName parentStructName}'"
       if let some existingFieldName ← findExistingField? infos parentStructName then
         if structureDiamondWarning.get (← getOptions) then
-          logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared"
+          logWarning m!"field '{existingFieldName}' from '{.ofConstName parentStructName}' has already been declared"
         let parents := parents.push { ref := parent, fvar? := none, subobject := false, structName := parentStructName, type := parentType }
         copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos parents
         -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure`

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 '{.ofConstName 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
@@ -81,10 +81,10 @@ protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : Messag
 Convert an `Except` into a `m` monadic action, where `m` is any monad that
 implements `MonadError`.
 -/
-def ofExcept [Monad m] [MonadError m] [ToString ε] (x : Except ε α) : m α :=
+def ofExcept [Monad m] [MonadError m] [ToMessageData ε] (x : Except ε α) : m α :=
   match x with
   | .ok a    => return a
-  | .error e => Lean.throwError <| toString e
+  | .error e => Lean.throwError <| toMessageData e
 
 /--
 Throw an error exception for the given kernel exception.

src/Lean/Message.lean

@@ -168,8 +168,31 @@ 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, but sanitized if it is a hygienic name.
+Use `MessageData.ofName` if hovers are undesired.
+
+If `fullNames` is true, then pretty prints as if `pp.fullNames` is true.
+Otherwise, pretty prints using the current user setting for `pp.fullNames`.
+-/
+def ofConstName (constName : Name) (fullNames : Bool := false) : MessageData :=
+  .ofLazy
+    (fun ctx? => do
+      let msg ← ofFormatWithInfos <$> match ctx? with
+        | .none => pure (format constName)
+        | .some ctx =>
+          let ctx := if fullNames then { ctx with opts := ctx.opts.insert `pp.fullNames fullNames } else ctx
+          ppConstNameWithInfos ctx constName
+      return Dynamic.mk msg)
+    (fun _ => false)
+
 partial def hasSyntheticSorry (msg : MessageData) : Bool :=
   visit none msg
 where
@@ -490,7 +513,7 @@ private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (ms
 def toMessageData (e : KernelException) (opts : Options) : MessageData :=
   match e with
   | unknownConstant env constName       => mkCtx env {} opts m!"(kernel) unknown constant '{constName}'"
-  | alreadyDeclared env constName       => mkCtx env {} opts m!"(kernel) constant has already been declared '{constName}'"
+  | alreadyDeclared env constName       => mkCtx env {} opts m!"(kernel) constant has already been declared '{.ofConstName constName true}'"
   | declTypeMismatch env decl givenType =>
     mkCtx env {} opts <|
     let process (n : Name) (expectedType : Expr) : MessageData :=
@@ -499,16 +522,16 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
     | Declaration.defnDecl { name := n, type := type, .. } => process n type
     | Declaration.thmDecl { name := n, type := type, .. }  => process n type
     | _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information
-  | declHasMVars env constName _        => mkCtx env {} opts m!"(kernel) declaration has metavariables '{constName}'"
-  | declHasFVars env constName _        => mkCtx env {} opts m!"(kernel) declaration has free variables '{constName}'"
+  | declHasMVars env constName _        => mkCtx env {} opts m!"(kernel) declaration has metavariables '{.ofConstName constName true}'"
+  | declHasFVars env constName _        => mkCtx env {} opts m!"(kernel) declaration has free variables '{.ofConstName constName true}'"
   | funExpected env lctx e              => mkCtx env lctx opts m!"(kernel) function expected{indentExpr e}"
   | typeExpected env lctx e             => mkCtx env lctx opts m!"(kernel) type expected{indentExpr e}"
   | letTypeMismatch  env lctx n _ _     => mkCtx env lctx opts m!"(kernel) let-declaration type mismatch '{n}'"
   | exprTypeMismatch env lctx e _       => mkCtx env lctx opts m!"(kernel) type mismatch at{indentExpr e}"
   | appTypeMismatch  env lctx e fnType argType =>
     mkCtx env lctx opts m!"application type mismatch{indentExpr e}\nargument has type{indentExpr argType}\nbut function has type{indentExpr fnType}"
   | invalidProj env lctx e              => mkCtx env lctx opts m!"(kernel) invalid projection{indentExpr e}"
-  | thmTypeIsNotProp env constName type => mkCtx env {} opts m!"(kernel) type of theorem '{constName}' is not a proposition{indentExpr type}"
+  | thmTypeIsNotProp env constName type => mkCtx env {} opts m!"(kernel) type of theorem '{.ofConstName constName true}' is not a proposition{indentExpr type}"
   | other msg                           => m!"(kernel) {msg}"
   | deterministicTimeout                => "(kernel) deterministic timeout"
   | excessiveMemory                     => "(kernel) excessive memory consumption detected"

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!"({.ofConstName ctorName}{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/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 {.ofConst e.getAppFn}, {e} ==> {e'}"
     recordSimpTheorem (.decl e.getAppFn.constName!)
     return e'
   | none => foldRawNatLit e

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 {.ofConstName 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 '{.ofConstName 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 "'{.ofConstName 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 "'{.ofConstName 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 "'{.ofConstName 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 "'{.ofConstName 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

src/Lean/PrettyPrinter.lean

@@ -63,6 +63,17 @@ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (d
     let fmt ← ppTerm stx >>= maybePrependExprSizes e
     return ⟨fmt, infos⟩
 
+open Delaborator in
+def ppConstNameWithInfos (constName : Name) : MetaM FormatWithInfos := do
+  if let some info := (← getEnv).find? constName then
+    let delab := withOptionAtCurrPos `pp.tagAppFns true <| delabConst
+    PrettyPrinter.ppExprWithInfos (delab := delab) (.const constName <| info.levelParams.map mkLevelParam)
+  else
+    -- Still, let's sanitize the name.
+    let stx := mkIdent constName
+    let stx := (sanitizeSyntax stx).run' { options := (← getOptions) }
+    formatCategory `term stx
+
 @[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
   Prod.fst <$> ((withOptions (fun _ => opts) <| ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO
@@ -103,9 +114,10 @@ private def withoutContext {m} [MonadExcept Exception m] (x : m α) : m α :=
 
 builtin_initialize
   ppFnsRef.set {
-    ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e,
-    ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx,
-    ppLevel := fun ctx l => return l.format (mvars := getPPMVarsLevels ctx.opts),
+    ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e
+    ppConstNameWithInfos := fun ctx n => ctx.runMetaM <| withoutContext <| ppConstNameWithInfos n
+    ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx
+    ppLevel := fun ctx l => return l.format (mvars := getPPMVarsLevels ctx.opts)
     ppGoal := fun ctx mvarId => ctx.runMetaM <| withoutContext <| Meta.ppGoal mvarId
   }
 
@@ -155,19 +167,6 @@ def ofConst (e : Expr) : MessageData :=
   else
     panic! "not a constant"
 
-/--
-Pretty print a constant given its name, similar to `Lean.MessageData.ofConst`.
-Uses the constant's universe level parameters when pretty printing.
-If there is no such constant in the environment, the name is simply formatted.
--/
-def ofConstName (constName : Name) : MessageData :=
-  .ofFormatWithInfosM do
-    if let some info := (← getEnv).find? constName then
-      let delab : Delab := withOptionAtCurrPos `pp.tagAppFns true delabConst
-      PrettyPrinter.ppExprWithInfos (delab := delab) (.const constName <| info.levelParams.map mkLevelParam)
-    else
-      return format constName
-
 /-- Generates `MessageData` for a declaration `c` as `c.{<levels>} <params> : <type>`, with terminfo. -/
 def signature (c : Name) : MessageData :=
   .ofFormatWithInfosM (PrettyPrinter.ppSignature c)

src/Lean/ResolveName.lean

@@ -20,7 +20,7 @@ For example, give a definition `foo`, we flag `foo.def` as reserved symbol.
 -/
 
 def throwReservedNameNotAvailable [Monad m] [MonadError m] (declName : Name) (reservedName : Name) : m Unit := do
-  throwError "failed to declare `{declName}` because `{reservedName}` has already been declared"
+  throwError "failed to declare `{declName}` because `{.ofConstName reservedName true}` has already been declared"
 
 def ensureReservedNameAvailable [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (suffix : String) : m Unit := do
   let reservedName := .str declName suffix