chore: fix test

src/Lean/Attributes.lean

@@ -139,7 +139,7 @@ def throwAttrNotInAsyncCtx (attrName declName : Name) (asyncPrefix? : Option Nam
   throwError "Cannot add attribute `[{attrName}]` to declaration `{.ofConstName declName}` because it is not from the present async context{asyncPrefix}"
 
 def throwAttrDeclNotOfExpectedType (attrName declName : Name) (givenType expectedType : Expr) : m α :=
-  throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{declName}` has type{indentExpr givenType}\n\
+  throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` has type{indentExpr givenType}\n\
     but `[{attrName}]` can only be added to declarations of type{indentExpr expectedType}"
 end
 
@@ -383,7 +383,7 @@ unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options)
   | some info =>
     match info.type with
     | Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName
-    | _ => throw s!"Unexpected attribute implementation type: `{declName}` is not of type `Lean.AttributeImpl`"
+    | _ => throw "Unexpected attribute implementation type: `{.ofConstName declName}` is not of type `Lean.AttributeImpl`"
 
 @[implemented_by mkAttributeImplOfConstantUnsafe]
 opaque mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl

src/Lean/Compiler/IR/Checker.lean

@@ -41,7 +41,7 @@ abbrev M := ReaderT CheckerContext <| StateRefT CheckerState CompilerM
 
 def throwCheckerError {α : Type} (msg : String) : M α := do
   let declName := (← read).currentDecl.name
-  throwError s!"failed to compile definition, compiler IR check failed at '{declName}'. Error: {msg}"
+  throwError "failed to compile definition, compiler IR check failed at `{.ofConstName declName}`. Error: {msg}"
 
 def markIndex (i : Index) : M Unit := do
   let s ← get

src/Lean/Compiler/ImplementedByAttr.lean

@@ -58,11 +58,11 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
       let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
       let fnDecl ← getConstVal fnName
       unless decl.levelParams.length == fnDecl.levelParams.length do
-        throwError "Invalid `implemented_by` argument `{fnName}`: `{fnName}` has {fnDecl.levelParams.length} universe level parameter(s), but `{declName}` has {decl.levelParams.length}"
+        throwError "Invalid `implemented_by` argument `{fnName}`: `{fnName}` has {fnDecl.levelParams.length} universe level parameter(s), but `{.ofConstName declName}` has {decl.levelParams.length}"
       let declType := decl.type
       let fnType ← Core.instantiateTypeLevelParams fnDecl (decl.levelParams.map mkLevelParam)
       unless declType == fnType do
-        throwError "Invalid `implemented_by` argument `{fnName}`: `{fnName}` has type{indentExpr fnType}\nbut `{declName}` has type{indentExpr declType}"
+        throwError "Invalid `implemented_by` argument `{fnName}`: `{fnName}` has type{indentExpr fnType}\nbut `{.ofConstName declName}` has type{indentExpr declType}"
       if decl.name == fnDecl.name then
         throwError "Invalid `implemented_by` argument `{fnName}`: Definition cannot be implemented by itself"
       return fnName

src/Lean/Compiler/InlineAttrs.lean

@@ -76,10 +76,10 @@ builtin_initialize inlineAttrs : EnumAttributes InlineAttributeKind ←
         s!"Cannot add attribute `[{kind.toAttrString}]`: {e}"
       if kind matches .macroInline then
         unless (← isValidMacroInline declName) do
-          throwError "Cannot add `[macro_inline]` attribute to `{declName}`: This attribute does not support this kind of declaration; only non-recursive definitions are supported"
+          throwError "Cannot add `[macro_inline]` attribute to `{.ofConstName declName}`: This attribute does not support this kind of declaration; only non-recursive definitions are supported"
         withExporting (isExporting := !isPrivateName declName) do
           if !(← getConstInfo declName).isDefinition then
-            throwError "invalid `[macro_inline]` attribute, '{declName}' must be an exposed definition"
+            throwError "invalid `[macro_inline]` attribute, '{.ofConstName declName}' must be an exposed definition"
 
 def setInlineAttribute (env : Environment) (declName : Name) (kind : InlineAttributeKind) : Except String Environment :=
   inlineAttrs.setValue env declName kind

src/Lean/Compiler/LCNF/Check.lean

@@ -200,7 +200,7 @@ partial def checkFunDeclCore (declName : Name) (params : Array Param) (type : Ex
     if (← checkTypes) then
       let valueType ← mkForallParams params (← value.inferType)
       unless (← InferType.compatibleTypes type valueType) do
-        throwError "type mismatch at `{declName}`, value has type{indentExpr valueType}\nbut is expected to have type{indentExpr type}"
+        throwError "type mismatch at `{.ofConstName declName}`, value has type{indentExpr valueType}\nbut is expected to have type{indentExpr type}"
 
 partial def checkFunDecl (funDecl : FunDecl) : CheckM Unit := do
   checkFunDeclCore funDecl.binderName funDecl.params funDecl.type funDecl.value

src/Lean/Compiler/LCNF/Simp/SimpM.lean

@@ -135,12 +135,12 @@ Otherwise, do not change the `inlineStack`.
     x
 where
   check (declName : Name) : SimpM Nat := do
-    trace[Compiler.simp.inline] "{declName}"
+    trace[Compiler.simp.inline] "{.ofConstName declName}"
     let numOccs := (← read).inlineStackOccs.find? declName |>.getD 0
     let numOccs := numOccs + 1
     let inlineIfReduce ← if let some decl ← getDecl? declName then pure decl.inlineIfReduceAttr else pure false
     if recursive && inlineIfReduce && numOccs > (← getConfig).maxRecInlineIfReduce then
-      throwError "function `{declName}` has been recursively inlined more than #{(← getConfig).maxRecInlineIfReduce}, consider removing the attribute `[inline_if_reduce]` from this declaration or increasing the limit using `set_option compiler.maxRecInlineIfReduce <num>`"
+      throwError "function `{.ofConstName declName}` has been recursively inlined more than #{(← getConfig).maxRecInlineIfReduce}, consider removing the attribute `[inline_if_reduce]` from this declaration or increasing the limit using `set_option compiler.maxRecInlineIfReduce <num>`"
     return numOccs
 
 /--
@@ -158,7 +158,7 @@ where
     match (← read).inlineStack with
     | [] => throwError maxRecDepthErrorMessage
     | declName :: stack =>
-      let mut fmt  := f!"{declName}\n"
+      let mut fmt  := m!"{.ofConstName declName}\n"
       let mut prev := declName
       let mut ellipsis := false
       for declName in stack do
@@ -167,7 +167,7 @@ where
             ellipsis := true
             fmt := fmt ++ "...\n"
         else
-          fmt := fmt ++ f!"{declName}\n"
+          fmt := fmt ++ m!"{.ofConstName declName}\n"
           prev := declName
           ellipsis := false
       throwError "maximum recursion depth reached in the code generator\nfunction inline stack:\n{fmt}"

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -101,7 +101,7 @@ The steps for this are roughly:
 -/
 def toDecl (declName : Name) : CompilerM Decl := do
   let declName := if let some name := isUnsafeRecName? declName then name else declName
-  let some info ← getDeclInfo? declName | throwError "declaration `{declName}` not found"
+  let some info ← getDeclInfo? declName | throwError "declaration `{.ofConstName declName}` not found"
   let safe := !info.isPartial && !info.isUnsafe
   let env ← getEnv
   let inlineAttr? := getInlineAttribute? env declName
@@ -125,7 +125,7 @@ def toDecl (declName : Name) : CompilerM Decl := do
     let params ← paramsFromTypeBinders type
     return { name := declName, params, type, value := .extern { entries := [] }, levelParams := info.levelParams, safe, inlineAttr? }
   else
-    let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value"
+    let some value := info.value? (allowOpaque := true) | throwError "declaration `{.ofConstName declName}` does not have a value"
     let (type, value) ← Meta.MetaM.run' do
       let type  ← toLCNFType info.type
       let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body)

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -686,7 +686,7 @@ where
           let type ← toLCNFType (← liftMetaM <| Meta.inferType e)
           mkUnreachable type
       | _, _ =>
-        throwError "code generator failed, unsupported occurrence of `{declName}`"
+        throwError "code generator failed, unsupported occurrence of `{.ofConstName declName}`"
 
   expandNoConfusionMajor (major : Expr) (numFields : Nat) : M Expr := do
     match numFields with

src/Lean/CoreM.lean

@@ -674,7 +674,7 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla
         && !supportedRecursors.contains declName
       | _ => false
     match unsupportedRecursor? with
-    | some (Expr.const declName ..) => throwError "code generator does not support recursor '{declName}' yet, consider using 'match ... with' and/or structural recursion"
+    | some (Expr.const declName ..) => throwError "code generator does not support recursor '{.ofConstName declName}' yet, consider using 'match ... with' and/or structural recursion"
     | _ => pure ()
 
 /--

src/Lean/DocString/Add.lean

@@ -49,7 +49,7 @@ def addDocString
     [Monad m] [MonadError m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
     (declName : Name) (docComment : TSyntax `Lean.Parser.Command.docComment) : m Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+    throwError "invalid doc string, declaration '{.ofConstName declName}' is in an imported module"
   validateDocComment docComment
   let docString : String ← getDocStringText docComment
   modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces

src/Lean/DocString/Extension.lean

@@ -34,7 +34,7 @@ def addBuiltinDocString (declName : Name) (docString : String) : IO Unit := do
 
 def addDocStringCore [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+    throwError "invalid doc string, declaration '{.ofConstName declName}' is in an imported module"
   modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
 
 def addDocStringCore' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=

src/Lean/Elab/DeclModifiers.lean

@@ -38,7 +38,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadFina
     | none          => throwError "'{.ofConstName declName true}' has already been declared"
     | some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared"
   if isReservedName env (privateToUserName declName) || isReservedName env (mkPrivateName (← getEnv) declName) then
-    throwError "'{declName}' is a reserved name"
+    throwError "'{.ofConstName declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)
     throwError "a private declaration '{.ofConstName declName true}' has already been declared"
@@ -225,7 +225,7 @@ def checkIfShadowingStructureField (declName : Name) : m Unit := do
       let fieldNames := getStructureFieldsFlattened (← getEnv) pre
       for fieldName in fieldNames do
         if pre ++ fieldName == declName then
-          throwError "invalid declaration name '{declName}', structure '{pre}' has field '{fieldName}'"
+          throwError "invalid declaration name '{.ofConstName declName}', structure '{pre}' has field '{fieldName}'"
   | _ => pure ()
 
 def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) : m (Name × Name) := do

src/Lean/Elab/Deriving/Basic.lean

@@ -168,7 +168,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) : TermElabM Unit
   -- and we make sure to put the instance in the private scope.
   withoutExporting (when := isPrivateName declName) do
   let ConstantInfo.defnInfo info ← getConstInfo declName
-    | throwError "Failed to delta derive instance, `{declName}` is not a definition."
+    | throwError "Failed to delta derive instance, `{.ofConstName declName}` is not a definition."
   let value := info.value.beta decl.getAppArgs
   let result : Closure.MkValueTypeClosureResult ←
     -- Assumption: users intend delta deriving to apply to the body of a definition, even if in the source code

src/Lean/Elab/Deriving/Inhabited.lean

@@ -121,7 +121,7 @@ private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do
         return true
     return false
   unless (← doIt false <||> doIt true) do
-    throwError "failed to generate 'Inhabited' instance for '{declName}'"
+    throwError "failed to generate 'Inhabited' instance for '{.ofConstName declName}'"
 
 def mkInhabitedInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
   if (← declNames.allM isInductive) then

src/Lean/Elab/LetRec.lean

@@ -53,7 +53,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       let declName := parentName?.getD Name.anonymous ++ shortDeclName
       if decls.any fun decl => decl.declName == declName then
         withRef declId do
-          throwError "'{declName}' has already been declared"
+          throwError "'{.ofConstName declName}' has already been declared"
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
       addDocString' declName docStr?

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -394,7 +394,7 @@ private partial def mkEqnProof (declName : Name) (type : Expr) (tryRefl : Bool)
         else if let some mvarIds ← splitTarget? mvarId (useNewSemantics := true) then
           mvarIds.forM go
         else
-          throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
+          throwError "failed to generate equational theorem for '{.ofConstName declName}'\n{MessageData.ofGoal mvarId}"
 
 
 /--
@@ -408,7 +408,7 @@ This is currently used for non-recursive functions, well-founded recursion and p
 but not for structural recursion.
 -/
 def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (Array Name) := do
-  trace[Elab.definition.eqns] "mkEqns: {declName}"
+  trace[Elab.definition.eqns] "mkEqns: {.ofConstName declName}"
   let info ← getConstInfoDefn declName
   let us := info.levelParams.map mkLevelParam
   withOptions (tactic.hygienic.set · false) do
@@ -449,7 +449,7 @@ where
   until one of the equational theorems is applicable.
 -/
 partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
-  let some eqs ← getEqnsFor? declName | throwError "failed to generate equations for '{declName}'"
+  let some eqs ← getEqnsFor? declName | throwError "failed to generate equations for '{.ofConstName declName}'"
   let tryEqns (mvarId : MVarId) : MetaM Bool :=
     eqs.anyM fun eq => commitWhen do checkpointDefEq (mayPostpone := false) do
       try
@@ -475,7 +475,7 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
     if (← tryContradiction mvarId) then
       return ()
 
-    throwError "failed to generate unfold theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
+    throwError "failed to generate unfold theorem for '{.ofConstName declName}'\n{MessageData.ofGoal mvarId}"
   go mvarId
 
 builtin_initialize

src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean

@@ -99,7 +99,7 @@ where
           trace[Elab.definition.partialFixpoint] "mkUnfoldEq rfl succeeded"
           instantiateMVars goal
         catch e =>
-          throwError "failed to generate unfold theorem for '{declName}':\n{e.toMessageData}"
+          throwError "failed to generate unfold theorem for '{.ofConstName declName}':\n{e.toMessageData}"
       let type ← mkForallFVars xs type
       let type ← letToHave type
       let value ← mkLambdaFVars xs goal

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -74,7 +74,7 @@ where
             trace[Elab.definition.structural.eqns] "splitTarget? succeeded"
             mvarIds.forM go
           else
-            throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
+            throwError "failed to generate equational theorem for '{.ofConstName declName}'\n{MessageData.ofGoal mvarId}"
 
 def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean

@@ -52,9 +52,9 @@ def getEnumToBitVecFor (declName : Name) : MetaM Name := do
   let enumToBitVecName := Name.str declName enumToBitVecSuffix
   realizeConst declName enumToBitVecName do
     let env ← getEnv
-    let .inductInfo inductiveInfo ← getConstInfo declName | throwError m!"{declName} is not an inductive."
+    let .inductInfo inductiveInfo ← getConstInfo declName | throwError m!"{.ofConstName declName} is not an inductive."
     if !(← isEnumType declName) then
-      throwError m!"{declName} is not an enum inductive."
+      throwError m!"{.ofConstName declName} is not an enum inductive."
     let domainSize := inductiveInfo.ctors.length
     let bvSize := getBitVecSize domainSize
     let bvType := mkApp (mkConst ``BitVec) (toExpr bvSize)
@@ -348,7 +348,7 @@ def getMatchEqCondFor (declName : Name) : MetaM Name := do
   if let some kind ← isSupportedMatch declName then
     return (← getMatchEqCondForAux declName kind)
   else
-    throwError m!"{matchEqCondSuffix} lemma could not be established for {declName}"
+    throwError m!"{matchEqCondSuffix} lemma could not be established for {.ofConstName declName}"
 
 builtin_initialize
   registerReservedNamePredicate fun env name => Id.run do

src/Lean/Elab/Tactic/Rewrite.lean

@@ -65,7 +65,7 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
             let hint := if eqThms.size = 1 then m!"" else
               .hint' m!"Try rewriting with `{Name.str declName unfoldThmSuffix}`"
             let rec go : List Name →  TacticM Unit
-              | [] => throwError m!"Failed to rewrite using equation theorems for `{declName}`" ++ hint
+              | [] => throwError m!"Failed to rewrite using equation theorems for `{.ofConstName declName}`" ++ hint
               | eqThm::eqThms => (x symm (mkCIdentFrom id eqThm)) <|> go eqThms
             discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
             go eqThms.toList

src/Lean/Elab/Tactic/Simp.lean

@@ -178,9 +178,9 @@ private def elabDeclToUnfoldOrTheorem (config : Meta.ConfigWithKey) (id : Origin
       return .addEntries <| thms.map (SimpEntry.thm ·)
     else
       if inv then
-        throwError m!"Invalid `←` modifier: `{declName}` is a declaration name to be unfolded"
+        throwError m!"Invalid `←` modifier: `{.ofConstName declName}` is a declaration name to be unfolded"
           ++ .hint' m!"The simplifier cannot \"refold\" definitions by name. Use `rw` for this instead,
-                      or use the `←` simp modifier with an equational lemma for `{declName}`."
+                      or use the `←` simp modifier with an equational lemma for `{.ofConstName declName}`."
       if kind == .dsimp then
         return .addEntries #[.toUnfold declName]
       else

src/Lean/KeyedDeclsAttribute.lean

@@ -105,7 +105,7 @@ def mkStateOfTable (table : Table γ) : ExtensionState γ := {
 
 def ExtensionState.erase (s : ExtensionState γ) (attrName : Name) (declName : Name) : CoreM (ExtensionState γ) := do
   unless s.declNames.contains declName do
-    throwError "Cannot erase attribute `{attrName}`: `{declName}` does not have this attribute"
+    throwError "Cannot erase attribute `{attrName}`: `{.ofConstName declName}` does not have this attribute"
   return { s with erased := s.erased.insert declName, declNames := s.declNames.erase declName }
 
 protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute γ) := do

src/Lean/Meta/Instances.lean

@@ -87,7 +87,7 @@ def Instances.eraseCore (d : Instances) (declName : Name) : Instances :=
 
 def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) : m Instances := do
   unless d.instanceNames.contains declName do
-    throwError "'{declName}' does not have [instance] attribute"
+    throwError "'{.ofConstName declName}' does not have [instance] attribute"
   return d.eraseCore declName
 
 builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances ←
@@ -311,15 +311,15 @@ builtin_initialize defaultInstanceExtension : SimplePersistentEnvExtension Defau
 
 def addDefaultInstance (declName : Name) (prio : Nat := 0) : MetaM Unit := do
   match (← getEnv).find? declName with
-  | none => throwError "Unknown constant `{declName}`"
+  | none => throwError "Unknown constant `{.ofConstName declName}`"
   | some info =>
     forallTelescopeReducing info.type fun _ type => do
       match type.getAppFn with
       | Expr.const className _ =>
         unless isClass (← getEnv) className do
-          throwError "invalid default instance '{declName}', it has type '({className} ...)', but {className}' is not a type class"
+          throwError "invalid default instance '{.ofConstName declName}', it has type '({className} ...)', but {className}' is not a type class"
         setEnv <| defaultInstanceExtension.addEntry (← getEnv) { className := className, instanceName := declName, priority := prio }
-      | _ => throwError "invalid default instance '{declName}', type must be of the form '(C ...)' where 'C' is a type class"
+      | _ => throwError "invalid default instance '{.ofConstName declName}', type must be of the form '(C ...)' where 'C' is a type class"
 
 builtin_initialize
   registerBuiltinAttribute {

src/Lean/Meta/Match/MatchPatternAttr.lean

@@ -36,7 +36,7 @@ builtin_initialize matchPatternAttr : TagAttribute ←
     (validate := fun declName => do
       withExporting (isExporting := !isPrivateName declName) do
         if !(← getConstInfo declName).isDefinition then
-          throwError "invalid `@[match_pattern]` attribute, '{declName}' is not an exposed definition")
+          throwError "invalid `@[match_pattern]` attribute, '{.ofConstName declName}' is not an exposed definition")
 
 @[export lean_has_match_pattern_attribute]
 def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool :=

src/Lean/Meta/RecursorInfo.lean

@@ -87,7 +87,7 @@ private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat)
 
 private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit :=
   unless motive.isFVar && motiveArgs.all Expr.isFVar do
-    throwError "invalid user defined recursor '{declName}', result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables"
+    throwError "invalid user defined recursor '{.ofConstName declName}', result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables"
 
 /-- Compute number of parameters for (user-defined) recursor.
    We assume a parameter is anything that occurs before the motive -/
@@ -109,11 +109,11 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
     else throwError "invalid major premise position for user defined recursor, recursor has only {xs.size} arguments"
   | none => do
     if motiveArgs.isEmpty then
-      throwError "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
+      throwError "invalid user defined recursor, '{.ofConstName declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
     let major := motiveArgs.back!
     match xs.idxOf? major with
     | some majorPos => pure (major, majorPos, true)
-    | none          => throwError "ill-formed recursor '{declName}'"
+    | none          => throwError "ill-formed recursor '{.ofConstName declName}'"
 
 private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (Iargs : Array Expr) : MetaM (List (Option Nat)) := do
   let mut paramsPos := #[]
@@ -126,7 +126,7 @@ private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (
       if localDecl.binderInfo.isInstImplicit then
         paramsPos := paramsPos.push none
       else
-        throwError"invalid user defined recursor '{declName}', type of the major premise does not contain the recursor parameter"
+        throwError"invalid user defined recursor '{.ofConstName declName}', type of the major premise does not contain the recursor parameter"
   pure paramsPos.toList
 
 private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndices : Nat) (Iargs : Array Expr) : MetaM (List Nat) := do
@@ -136,7 +136,7 @@ private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndic
     let x := xs[i]!
     match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with
     | some j => indicesPos := indicesPos.push j
-    | none   => throwError "invalid user defined recursor '{declName}', type of the major premise does not contain the recursor index"
+    | none   => throwError "invalid user defined recursor '{.ofConstName declName}', type of the major premise does not contain the recursor index"
   pure indicesPos.toList
 
 private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM Level :=
@@ -144,7 +144,7 @@ private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM L
   | Expr.sort u@(Level.zero)    => pure u
   | Expr.sort u@(Level.param _) => pure u
   | _                           =>
-    throwError "invalid user defined recursor '{declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter"
+    throwError "invalid user defined recursor '{.ofConstName declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter"
 
 private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : Level) (Ilevels : List Level) : MetaM (List RecursorUnivLevelPos) := do
   let Ilevels := Ilevels.toArray
@@ -156,7 +156,7 @@ private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl :
       match Ilevels.findIdx? fun u => u == mkLevelParam p with
       | some i => univLevelPos := univLevelPos.push (RecursorUnivLevelPos.majorType i)
       | none   =>
-        throwError "invalid user defined recursor '{declName}', major premise type does not contain universe level parameter '{p}'"
+        throwError "invalid user defined recursor '{.ofConstName declName}', major premise type does not contain universe level parameter '{p}'"
   pure univLevelPos.toList
 
 private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do
@@ -180,7 +180,7 @@ private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices
 
 private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (motiveResultType : Expr) (motiveTypeParams : Array Expr) : MetaM Unit := do
   if !motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size then
-    throwError "invalid user defined recursor '{declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant"
+    throwError "invalid user defined recursor '{.ofConstName declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant"
 
 private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : MetaM RecursorInfo := do
   let cinfo ← getConstInfo declName
@@ -191,7 +191,7 @@ private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : Meta
     let (major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motiveArgs
     let numIndices := if depElim then motiveArgs.size - 1 else motiveArgs.size
     if majorPos < numIndices then
-      throwError "invalid user defined recursor '{declName}', indices must occur before major premise"
+      throwError "invalid user defined recursor '{.ofConstName declName}', indices must occur before major premise"
     let majorType ← inferType major
     majorType.withApp fun I Iargs =>
     match I with
@@ -216,7 +216,7 @@ private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : Meta
           indicesPos    := indicesPos,
           numArgs       := xs.size
         }
-    | _ => throwError "invalid user defined recursor '{declName}', type of the major premise must be of the form (I ...), where I is a constant"
+    | _ => throwError "invalid user defined recursor '{.ofConstName declName}', type of the major premise must be of the form (I ...), where I is a constant"
 
 /-
 @[builtin_attr_parser] def «recursor» := leading_parser "recursor " >> numLit

src/Lean/Meta/Structure.lean

@@ -26,7 +26,7 @@ def getStructureName (struct : Expr) : MetaM Name :=
   match struct.getAppFn with
   | Expr.const declName .. => do
     unless isStructure (← getEnv) declName do
-      throwError "'{declName}' is not a structure"
+      throwError "'{.ofConstName declName}' is not a structure"
     return declName
   | _ => throwError "expected structure"
 

src/Lean/Meta/Tactic/Ext.lean

@@ -83,7 +83,7 @@ found somewhere in the state's tree, and is not erased.
 def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) :
     m ExtTheorems := do
   unless d.contains declName do
-    throwError "Cannot erase `[ext]` attribute from `{declName}`: It does not have this attribute"
+    throwError "Cannot erase `[ext]` attribute from `{.ofConstName declName}`: It does not have this attribute"
   return d.eraseCore declName
 
 end Lean.Meta.Ext

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

@@ -36,7 +36,7 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
             addSimpTheorem ext declName post (inv := inv) attrKind prio
           else if info.kind matches .defn then
             if inv then
-              throwError m!"Invalid `←` modifier: `{declName}` is a declaration name to be unfolded"
+              throwError m!"Invalid `←` modifier: `{.ofConstName declName}` is a declaration name to be unfolded"
                 ++ .note m!"The simplifier will automatically unfold definitions marked with the `[simp]` \
                             attribute, but it will not \"refold\" them"
             if (← Simp.ignoreEquations declName) then
@@ -50,7 +50,7 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
             else
               ext.add (SimpEntry.toUnfold declName) attrKind
           else
-            throwError m!"Cannot add `simp` attribute to `{declName}`: It is not a proposition nor a definition (to unfold)"
+            throwError m!"Cannot add `simp` attribute to `{.ofConstName declName}`: It is not a proposition nor a definition (to unfold)"
               ++ .note m!"The `[simp]` attribute can be added to lemmas that should be automatically used by the simplifier \
                           and to definitions that the simplifier should automatically unfold"
         discard <| go.run {} {}

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

@@ -87,7 +87,7 @@ def registerBuiltinSimprocCore (declName : Name) (key : Array SimpTheoremKey) (p
   unless (← initializing) do
     throw (IO.userError s!"Invalid builtin simproc declaration: It can only be registered during initialization")
   if (← builtinSimprocDeclsRef.get).keys.contains declName then
-    throw (IO.userError s!"Invalid builtin simproc declaration `{declName}`: This builtin simproc has already been declared")
+    throw (IO.userError s!"Invalid builtin simproc declaration `{privateToUserName declName}`: This builtin simproc has already been declared")
   builtinSimprocDeclsRef.modify fun { keys, procs } =>
     { keys := keys.insert declName key, procs := procs.insert declName proc }
 
@@ -100,9 +100,9 @@ def registerBuiltinDSimproc (declName : Name) (key : Array SimpTheoremKey) (proc
 def registerSimproc (declName : Name) (keys : Array SimpTheoremKey) : CoreM Unit := do
   let env ← getEnv
   unless (env.getModuleIdxFor? declName).isNone do
-    throwError "Invalid simproc declaration `{declName}`: This function is declared in an imported module"
+    throwError "Invalid simproc declaration `{.ofConstName declName}`: This function is declared in an imported module"
   if (← isSimproc declName) then
-    throwError "Invalid simproc declaration `{declName}`: This simproc has already been declared"
+    throwError "Invalid simproc declaration `{.ofConstName declName}`: This simproc has already been declared"
   modifyEnv fun env => simprocDeclExt.modifyState env fun s => { s with newEntries := s.newEntries.insert declName keys }
 
 instance : BEq SimprocEntry where
@@ -132,7 +132,7 @@ unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM (Sum Simproc DSimp
       return .inl (← IO.ofExcept <| ctx.env.evalConst Simproc ctx.opts declName)
     | .const ``DSimproc _ =>
       return .inr (← IO.ofExcept <| ctx.env.evalConst DSimproc ctx.opts declName)
-    | _ => throw <| IO.userError s!"Simproc `{declName}` has an unexpected type: Expected `Simproc` or `DSimproc`, but found `{info.type}`"
+    | _ => throw <| IO.userError s!"Simproc `{privateToUserName declName}` has an unexpected type: Expected `Simproc` or `DSimproc`, but found `{info.type}`"
 
 @[implemented_by getSimprocFromDeclImpl]
 opaque getSimprocFromDecl (declName: Name) : ImportM (Sum Simproc DSimproc)
@@ -143,13 +143,13 @@ def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do
 def eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit := do
   let s := ext.getState (← getEnv)
   unless s.simprocNames.contains declName do
-    throwError "`{declName}` does not have a [simproc] attribute"
+    throwError "`{.ofConstName declName}` does not have a [simproc] attribute"
   modifyEnv fun env => ext.modifyState env fun s => s.erase declName
 
 def addSimprocAttrCore (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
   let proc ← getSimprocFromDecl declName
   let some keys ← getSimprocDeclKeys? declName |
-    throwError "Invalid `[simproc]` attribute: `{declName}` is not a simproc"
+    throwError "Invalid `[simproc]` attribute: `{.ofConstName declName}` is not a simproc"
   ext.add { declName, post, keys, proc } kind
 
 def Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : Simprocs :=
@@ -164,7 +164,7 @@ Implements attributes `builtin_simproc` and `builtin_sevalproc`.
 -/
 def addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : IO Unit := do
   let some keys := (← builtinSimprocDeclsRef.get).keys[declName]? |
-    throw (IO.userError s!"Invalid `[builtin_simproc]` attribute: `{declName}` is not a builtin simproc")
+    throw (IO.userError s!"Invalid `[builtin_simproc]` attribute: `{privateToUserName declName}` is not a builtin simproc")
   ref.modify fun s => s.addCore keys declName post proc
 
 def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : IO Unit :=
@@ -180,12 +180,12 @@ def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs
     catch e =>
       if (← isBuiltinSimproc declName) then
         let some proc := (← builtinSimprocDeclsRef.get).procs[declName]?
-          | throwError "Invalid `[simproc]` attribute: `{declName}` is not a simproc"
+          | throwError "Invalid `[simproc]` attribute: `{.ofConstName declName}` is not a simproc"
         pure proc
       else
         throw e
   let some keys ← getSimprocDeclKeys? declName |
-    throwError "Invalid `[simproc]` attribute: `{declName}` is not a simproc"
+    throwError "Invalid `[simproc]` attribute: `{.ofConstName declName}` is not a simproc"
   return s.addCore keys declName post proc
 
 def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM Step := do
@@ -409,7 +409,7 @@ private def addBuiltin (declName : Name) (stx : Syntax) (addDeclName : Name) : A
       | .const ``Simproc _  => pure <| mkApp3 (mkConst ``Sum.inl [0, 0]) (mkConst ``Simproc) (mkConst ``DSimproc) (mkConst declName)
       | .const ``DSimproc _ => pure <| mkApp3 (mkConst ``Sum.inr [0, 0]) (mkConst ``Simproc) (mkConst ``DSimproc) (mkConst declName)
       | tp => throwError "Unexpected simproc type: Expected {.ofConstName ``Lean.Meta.Simp.Simproc} or {.ofConstName ``Lean.Meta.Simp.DSimproc}, \
-                but `{declName}` has type{indentExpr tp}"
+                but `{.ofConstName declName}` has type{indentExpr tp}"
     let val := mkAppN (mkConst addDeclName) #[toExpr declName, toExpr post, procExpr]
     let initDeclName ← mkFreshUserName (declName ++ `declare)
     declareBuiltin initDeclName val

src/Lean/Meta/Tactic/Unfold.lean

@@ -36,13 +36,13 @@ where
 def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := mvarId.withContext do
   let target ← instantiateMVars (← mvarId.getType)
   let r ← unfold target declName
-  if r.expr == target then throwError "Tactic `unfold` failed to unfold `{declName}` in{indentExpr target}"
+  if r.expr == target then throwError "Tactic `unfold` failed to unfold `{.ofConstName declName}` in{indentExpr target}"
   applySimpResultToTarget mvarId target r
 
 def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : MetaM MVarId := mvarId.withContext do
   let type ← fvarId.getType
   let r ← unfold (← instantiateMVars type) declName
-  if r.expr == type then throwError "Tactic `unfold` failed to unfold `{declName}` in{indentExpr type}"
+  if r.expr == type then throwError "Tactic `unfold` failed to unfold `{.ofConstName declName}` in{indentExpr type}"
   let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r (mayCloseGoal := false) | unreachable!
   return mvarId
 

src/Lean/Parser/Extension.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Parser.Basic
 public import Lean.ScopedEnvExtension
+import Lean.PrivateName
 import Lean.BuiltinDocAttr
 
 public section
@@ -153,7 +154,7 @@ private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit
   let tokenTable ← builtinTokenTable.swap {}
   match addParserTokens tokenTable info with
   | Except.ok tokenTable => builtinTokenTable.set tokenTable
-  | Except.error msg     => throw (IO.userError s!"invalid builtin parser '{declName}', {msg}")
+  | Except.error msg     => throw (IO.userError s!"invalid builtin parser `{privateToUserName declName}`, {msg}")
 
 def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
   match e with
@@ -509,7 +510,7 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
   | Expr.const `Lean.Parser.Parser _ =>
     declareLeadingBuiltinParser catName declName prio
   | _ => throwError "Unexpected type for parser declaration: Parsers must have type `Parser` or \
-    `TrailingParser`, but `{declName}` has type{indentExpr decl.type}"
+    `TrailingParser`, but `{.ofConstName declName}` has type{indentExpr decl.type}"
   declareBuiltinDocStringAndRanges declName
   runParserAttributeHooks catName declName (builtin := true)
 
@@ -542,7 +543,7 @@ private def ParserAttribute.add (_attrName : Name) (catName : Name) (declName :
     try
       addToken token attrKind
     catch
-      | Exception.error _   msg => throwError "invalid parser '{declName}', {msg}"
+      | Exception.error _   msg => throwError "invalid parser '{.ofConstName declName}', {msg}"
       | ex => throw ex
   let kinds := parser.info.collectKinds {}
   kinds.forM fun kind _ => modifyEnv fun env => addSyntaxNodeKind env kind

src/Lean/Parser/Tactic/Doc.lean

@@ -283,12 +283,12 @@ def tacticDocsOnTactics : ParserAttributeHook where
     if catName == `tactic then
       return
     if alternativeOfTactic (← getEnv) declName |>.isSome then
-      throwError m!"`{declName}` is not a tactic"
+      throwError m!"`{.ofConstName declName}` is not a tactic"
     -- It's sufficient to look in the state (and not the imported entries) because this validation
     -- only needs to check tags added in the current module
     if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then
       if !tags.isEmpty then
-        throwError m!"`{declName}` is not a tactic"
+        throwError m!"`{.ofConstName declName}` is not a tactic"
 
 builtin_initialize
   registerParserAttributeHook tacticDocsOnTactics

src/Lean/ReducibilityAttrs.lean

@@ -108,30 +108,30 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind :
       let statusOld := getReducibilityStatusCore (← getEnv) declName
       match attrKind with
       | .scoped =>
-        throwError "failed to set reducibility status for `{declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}"
+        throwError "failed to set reducibility status for `{.ofConstName declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}"
       | .global =>
         if (← getEnv).getModuleIdxFor? declName matches some _ then
-          throwError "failed to set reducibility status, `{declName}` has not been defined in this file, consider using the `local` modifier{suffix}"
+          throwError "failed to set reducibility status, `{.ofConstName declName}` has not been defined in this file, consider using the `local` modifier{suffix}"
         match status with
         | .reducible =>
           unless statusOld matches .semireducible do
-            throwError "failed to set `[reducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
+            throwError "failed to set `[reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
         | .irreducible =>
           unless statusOld matches .semireducible do
-            throwError "failed to set `[irreducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
+            throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
         | .semireducible =>
-          throwError "failed to set `[semireducible]` for `{declName}`, declarations are `[semireducible]` by default{suffix}"
+          throwError "failed to set `[semireducible]` for `{.ofConstName declName}`, declarations are `[semireducible]` by default{suffix}"
       | .local =>
         match status with
         | .reducible =>
-          throwError "failed to set `[local reducible]` for `{declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}"
+          throwError "failed to set `[local reducible]` for `{.ofConstName declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}"
         | .irreducible =>
           unless statusOld matches .semireducible do
-            throwError "failed to set `[local irreducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
+            throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
         | .semireducible =>
           unless statusOld matches .irreducible do
-            throwError "failed to set `[local semireducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}"
-    | _ => throwError "failed to set reducibility status, `{declName}` is not a definition{suffix}"
+            throwError "failed to set `[local semireducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}"
+    | _ => throwError "failed to set reducibility status, `{.ofConstName declName}` is not a definition{suffix}"
 
 private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
   Attribute.Builtin.ensureNoArgs stx

src/Lean/ResolveName.lean

@@ -25,7 +25,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 `{.ofConstName reservedName true}` has already been declared"
+  throwError "failed to declare `{.ofConstName 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

tests/lean/implementedByIssue.lean.expected.out

@@ -1,5 +1,5 @@
-implementedByIssue.lean:15:11-15:31: error: Invalid `implemented_by` argument `Hidden.get_2`: `Hidden.get_2` has 0 universe level parameter(s), but `Hidden.Array.data` has 1
+implementedByIssue.lean:15:11-15:31: error: Invalid `implemented_by` argument `Hidden.get_2`: `Hidden.get_2` has 0 universe level parameter(s), but `Array.data` has 1
 implementedByIssue.lean:19:11-19:31: error: Invalid `implemented_by` argument `Hidden.get_3`: `Hidden.get_3` has type
   {α : Type u} → {n : Nat} → Fin n → Array α n → α
-but `Hidden.Array.data` has type
+but `Array.data` has type
   {α : Type u} → {n : Nat} → Array α n → Fin n → α