feat: make it possible to use dot notation in m! strings

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 '{.ofConstName 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 '{.ofConstName ``MonadEval}' instance \
           to adapt{indentExpr (← inferType e)}\n\
-          to '{MessageData.ofConstName ``IO}' or '{MessageData.ofConstName ``CommandElabM}'."
+          to '{.ofConstName ``IO}' or '{.ofConstName ``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/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!"{.ofConstName declName} ↦ {numOccs}" #[]
       -- let info
       logInfo <| MessageData.trace { cls := `theorem } m!"{d.name}" (#[sizeMsg] ++ constOccsMsg)
 

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -62,8 +62,8 @@ def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Ex
         \n\
         This process uses multiple strategies:\n\
         - It looks for a parameter that matches the return type.\n\
-        - It tries synthesizing '{MessageData.ofConstName ``Inhabited}' and '{MessageData.ofConstName ``Nonempty}' \
-          instances for the return type, while making every parameter into a local '{MessageData.ofConstName ``Inhabited}' instance.\n\
+        - It tries synthesizing '{.ofConstName ``Inhabited}' and '{.ofConstName ``Nonempty}' \
+          instances for the return type, while making every parameter into a local '{.ofConstName ``Inhabited}' instance.\n\
         - It tries unfolding the return type.\n\
         \n\
         If the return type is defined using the 'structure' or 'inductive' command, \

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 '{.ofConstName 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"
+          '{.ofConstName ``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!"'{.ofConst e}'"
           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 '{.ofConstName ``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}"
+          m!"After unfolding the {instances} {.andList unfoldedInsts.toList}, \
+          reduction got stuck at the '{.ofConstName ``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 '▸' ({.ofConstName ``Eq.rec}), \
+          which suggests that one of the '{.ofConstName ``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}' \
+          '{.ofConstName ``inferInstanceAs}' or '{.ofConstName ``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 '{.ofConstName ``Classical.choice}', \
+          which indicates that a '{.ofConstName ``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}'."
+          '{.ofConstName ``Classical.propDecidable}'."
         else
           MessageData.nil
       return m!"\
         tactic '{tacticName}' failed for proposition\
         {indentExpr expectedType}\n\
-        since its '{MessageData.ofConstName ``Decidable}' instance\
+        since its '{.ofConstName ``Decidable}' instance\
         {indentExpr s}\n\
-        did not reduce to '{MessageData.ofConstName ``isTrue}' or '{MessageData.ofConstName ``isFalse}'.\n\n\
+        did not reduce to '{.ofConstName ``isTrue}' or '{.ofConstName ``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
         addDeclarationRangesFromSyntax extName (← getRef)
     catch e =>
       throwError m!"\
-        Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
+        Failed to generate an 'ext' theorem for '{.ofConstName structName}': {e.toMessageData}"
   return extName
 
 /--
@@ -164,7 +164,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
         addDeclarationRangesFromSyntax extName (← 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 '{.ofConstName extName}': {e.toMessageData}\n\
         \n\
         Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem."
   return extIffName

src/Lean/Message.lean

@@ -464,6 +464,7 @@ instance : ToMessageData Syntax        := ⟨MessageData.ofSyntax⟩
 instance : ToMessageData (TSyntax k)   := ⟨(MessageData.ofSyntax ·)⟩
 instance : ToMessageData Format        := ⟨MessageData.ofFormat⟩
 instance : ToMessageData MVarId        := ⟨MessageData.ofGoal⟩
+@[default_instance]
 instance : ToMessageData MessageData   := ⟨id⟩
 instance [ToMessageData α] : ToMessageData (List α)  := ⟨fun as => MessageData.ofList <| as.map toMessageData⟩
 instance [ToMessageData α] : ToMessageData (Array α) := ⟨fun as => toMessageData as.toList⟩

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!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
     return { data, max := entries[0]!.2 }
 
 def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do

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!"{.ofConstName declName}"
     else
       pure m!"{declName} (builtin simproc)"
   | .fvar fvarId => pure m!"{mkFVar fvarId}"

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

@@ -63,15 +63,15 @@ def mkSimpCongrTheorem (declName : Name) (prio : Nat) : MetaM SimpCongrTheorem :
       for lhsArg in lhsArgs do
         for mvarId in (lhsArg.collectMVars {}).result do
           foundMVars := foundMVars.insert mvarId
-      let mut i := 0
+      let mut i : Nat := 0
       let mut hypothesesPos := #[]
       for x in xs, bi in bis do
         if bi.isExplicit && !foundMVars.contains x.mvarId! then
           let rhsFn? ← forallTelescopeReducing (← inferType x) fun ys xType => do
             match xType.eqOrIff? with
             | none => pure none -- skip
             | some (xLhs, xRhs) =>
-              let mut j := 0
+              let mut j : Nat := 0
               for y in ys do
                 let yType ← inferType y
                 unless onlyMVarsAt yType foundMVars do

tests/lean/run/panicAtCheckAssignment.lean

@@ -8,5 +8,5 @@ def bug : MetaM Unit := do
   forallTelescopeReducing default fun ys _ => do
     let mut j := 0
     for y in ys do
-      throwError "#{i+1}"
+      throwError "#{(i+1 : Nat)}"
       j := j + 1