diff --git a/src/Init/Data/ToString/Macro.lean b/src/Init/Data/ToString/Macro.lean
index e87f96b527..eb113feaf7 100644
--- a/src/Init/Data/ToString/Macro.lean
+++ b/src/Init/Data/ToString/Macro.lean
@@ -10,7 +10,4 @@ import Init.Data.ToString.Basic
 syntax:max "s!" interpolatedStr(term) : term
 
 macro_rules
-  | `(s! $interpStr) => do
-    let chunks := interpStr.getArgs
-    let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toString $a))
-    `(($r : String))
+  | `(s! $interpStr) => do interpStr.expandInterpolatedStr (← `(String)) (← `(toString))
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index ce21990ce2..1670ed91a8 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -664,6 +664,11 @@ def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → S
     i := i+1
   return result
 
+def expandInterpolatedStr (interpStr : Syntax) (type : Syntax) (toTypeFn : Syntax) : MacroM Syntax := do
+  let ref := interpStr
+  let r ← expandInterpolatedStrChunks interpStr.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
+  `(($r : $type))
+
 def getSepArgs (stx : Syntax) : Array Syntax :=
   stx.getArgs.getSepElems
 
diff --git a/src/Lean/Data/FormatMacro.lean b/src/Lean/Data/FormatMacro.lean
index cc1b1473a1..bd30c8ba6c 100644
--- a/src/Lean/Data/FormatMacro.lean
+++ b/src/Lean/Data/FormatMacro.lean
@@ -9,9 +9,6 @@ namespace Lean
 syntax:max "f!" interpolatedStr(term) : term
 
 macro_rules
-  | `(f! $interpStr) => do
-    let chunks := interpStr.getArgs
-    let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(fmt $a))
-    `(($r : Format))
+  | `(f! $interpStr) => do interpStr.expandInterpolatedStr (← `(Format)) (← `(fmt))
 
 end Lean
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index b914811980..d8b889c766 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -492,7 +492,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
            So, we don't projection functions for it. Thus, we use `Expr.proj` -/
         pure $ LValResolution.projIdx structName (idx - 1)
     else
-      throwLValError e eType msg!"invalid projection, structure has only {fieldNames.size} field(s)"
+      throwLValError e eType m!"invalid projection, structure has only {fieldNames.size} field(s)"
   | Expr.const structName _ _, LVal.fieldName fieldName =>
     let env ← getEnv
     let searchEnv : Unit → TermElabM LValResolution := fun _ => do
@@ -500,7 +500,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       | some (baseStructName, fullName) => pure $ LValResolution.const baseStructName structName fullName
       | none   =>
         throwLValError e eType
-          msg!"invalid field notation, '{fieldName}' is not a valid \"field\" because environment does not contain '{Name.mkStr structName fieldName}'"
+          m!"invalid field notation, '{fieldName}' is not a valid \"field\" because environment does not contain '{Name.mkStr structName fieldName}'"
     -- search local context first, then environment
     let searchCtx : Unit → TermElabM LValResolution := fun _ => do
       let fullName := Name.mkStr structName fieldName
@@ -526,7 +526,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     let fullName := Name.mkStr structName "getOp"
     match env.find? fullName with
     | some _ => pure $ LValResolution.getOp fullName idx
-    | none   => throwLValError e eType msg!"invalid [..] notation because environment does not contain '{fullName}'"
+    | none   => throwLValError e eType m!"invalid [..] notation because environment does not contain '{fullName}'"
   | _, LVal.getOp idx =>
     throwLValError e eType "invalid [..] notation, type is not of the form (C ...) where C is a constant"
   | _, _ =>
@@ -791,7 +791,7 @@ private def toMessageData (ex : Exception) : TermElabM MessageData := do
     else
       let fileMap ← MonadLog.getFileMap -- Remove `MonadLog.` it is a workaround for old frontend
       let exPosition := fileMap.toPosition exPos
-      pure msg!"{exPosition.line}:{exPosition.column} {ex.toMessageData}"
+      pure m!"{exPosition.line}:{exPosition.column} {ex.toMessageData}"
 
 private def toMessageList (msgs : Array MessageData) : MessageData :=
   indentD (MessageData.joinSep msgs.toList (Format.line ++ Format.line))
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 46542a97b0..88658c853b 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -211,7 +211,7 @@ instance : MonadRecDepth CommandElabM := {
         pure ()
       else
         let idName ← liftIO $ id.getName;
-        logError msg!"internal exception {idName}"
+        logError m!"internal exception {idName}"
 
 builtin_initialize registerTraceClass `Elab.command
 
@@ -412,7 +412,7 @@ partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM Unit :=
     throwError (ex.toMessageData opts)
 
 def logUnknownDecl (declName : Name) : CommandElabM Unit :=
-  logError msg!"unknown declaration '{declName}'"
+  logError m!"unknown declaration '{declName}'"
 
 @[builtinCommandElab «export»] def elabExport : CommandElab := fun stx => do
   -- `stx` is of the form (Command.export "export" <namespace> "(" (null <ids>*) ")")
@@ -522,7 +522,7 @@ open Meta
     let e ← Term.elabTerm term none
     Term.synthesizeSyntheticMVarsNoPostponing
     let type ← inferType e
-    logInfo msg!"{e} : {type}"
+    logInfo m!"{e} : {type}"
 
 def hasNoErrorMessages : CommandElabM Bool := do
   return !(← get).messages.hasErrors
@@ -630,7 +630,7 @@ def setOption (optionName : Name) (val : DataValue) : CommandElabM Unit := do
   match val with
   | Syntax.atom _ "true"  => setOption optionName (DataValue.ofBool true)
   | Syntax.atom _ "false" => setOption optionName (DataValue.ofBool false)
-  | _ => logErrorAt val msg!"unexpected set_option value {val}"
+  | _ => logErrorAt val m!"unexpected set_option value {val}"
 
 @[builtinMacro Lean.Parser.Command.«in»] def expandInCmd : Macro := fun stx => do
   let cmd₁ := stx[0]
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 5dd8a6deb6..e7017f1e33 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -163,19 +163,19 @@ private def varsToMessageData (vars : Array Name) : MessageData :=
 partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
   let us := MessageData.ofList $ (nameSetToArray codeBlock.uvars).toList.map MessageData.ofName
   let rec loop : Code → MessageData
-    | Code.decl xs _ k            => msg!"let {varsToMessageData xs} := ...\n{loop k}"
-    | Code.reassign xs _ k        => msg!"{varsToMessageData xs} := ...\n{loop k}"
-    | Code.joinpoint n ps body k  => msg!"let {n.simpMacroScopes} {varsToMessageData (ps.map Prod.fst)} := {indentD (loop body)}\n{loop k}"
-    | Code.seq e k                => msg!"{e}\n{loop k}"
+    | Code.decl xs _ k            => m!"let {varsToMessageData xs} := ...\n{loop k}"
+    | Code.reassign xs _ k        => m!"{varsToMessageData xs} := ...\n{loop k}"
+    | Code.joinpoint n ps body k  => m!"let {n.simpMacroScopes} {varsToMessageData (ps.map Prod.fst)} := {indentD (loop body)}\n{loop k}"
+    | Code.seq e k                => m!"{e}\n{loop k}"
     | Code.action e               => e
-    | Code.ite _ _ _ c t e        => msg!"if {c} then {indentD (loop t)}\nelse{loop e}"
-    | Code.jmp _ j xs             => msg!"jmp {j.simpMacroScopes} {xs.toList}"
-    | Code.«break» _              => msg!"break {us}"
-    | Code.«continue» _           => msg!"continue {us}"
-    | Code.«return» _ v           => msg!"return {v} {us}"
+    | Code.ite _ _ _ c t e        => m!"if {c} then {indentD (loop t)}\nelse{loop e}"
+    | Code.jmp _ j xs             => m!"jmp {j.simpMacroScopes} {xs.toList}"
+    | Code.«break» _              => m!"break {us}"
+    | Code.«continue» _           => m!"continue {us}"
+    | Code.«return» _ v           => m!"return {v} {us}"
     | Code.«match» _ ds t alts    =>
-      msg!"match {ds} with"
-      ++ alts.foldl (init := "") fun acc alt => acc ++ msg!"\n| {alt.patterns} => {loop alt.rhs}"
+      m!"match {ds} with"
+      ++ alts.foldl (init := "") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}"
   loop codeBlock.code
 
 /- Return true if the give code contains an exit point that satisfies `p` -/
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 0061ee5aa4..7eb53ed12b 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -138,7 +138,7 @@ private partial def checkParamsAndResultType (type firstType : Expr) (numParams
     | _ =>
       throwError "unexpected inductive resulting type"
   catch
-    | Exception.error ref msg => throw (Exception.error ref msg!"invalid mutually inductive types, {msg}")
+    | Exception.error ref msg => throw (Exception.error ref m!"invalid mutually inductive types, {msg}")
     | ex => throw ex
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 33d9613cfe..caa22cbfaa 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -65,7 +65,7 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl
       checkModifiers newHeader.modifiers firstHeader.modifiers
       checkKinds newHeader.kind firstHeader.kind
     catch
-       | Exception.error ref msg => throw (Exception.error ref msg!"invalid mutually recursive definitions, {msg}")
+       | Exception.error ref msg => throw (Exception.error ref m!"invalid mutually recursive definitions, {msg}")
        | ex => throw ex
   else
     pure ()
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 2577f3fd4d..3b7429851c 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -75,6 +75,6 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do
           (WFRecursion preDefs))
         (fun msg =>
           let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
-          msg!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
+          m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
 
 end Lean.Elab
diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index 6bcdc4ce30..57239530ce 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -117,7 +117,7 @@ private partial def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecA
                        indParams   := indParams,
                        indIndices  := indIndices,
                        reflexive := indInfo.isReflexive })
-                    (fun msg => msg!"argument #{i+1} was not used for structural recursion{indentD msg}"))
+                    (fun msg => m!"argument #{i+1} was not used for structural recursion{indentD msg}"))
                   (loop (i+1))
     else
       throwStructuralFailed
@@ -352,7 +352,7 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
     throwError "structural recursion does not handle mutually recursive functions"
   else do
     let preDefNonRec ← elimRecursion preDefs[0]
-    mapError (addNonRec preDefNonRec) (fun msg => msg!"structural recursion failed, produced type incorrect term{indentD msg}")
+    mapError (addNonRec preDefNonRec) (fun msg => m!"structural recursion failed, produced type incorrect term{indentD msg}")
     addAndCompileUnsafeRec preDefs
 
 builtin_initialize
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 72a82c060e..9b52a32e0b 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -109,9 +109,9 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
   let env ← getEnv
   let (_, s) := ((CollectAxioms.collect constName).run env).run {}
   if s.axioms.isEmpty then
-    logInfo msg!"'{constName}' does not depend on any axioms"
+    logInfo m!"'{constName}' does not depend on any axioms"
   else
-    logInfo msg!"'{constName}' depends on axioms: {s.axioms.toList}"
+    logInfo m!"'{constName}' depends on axioms: {s.axioms.toList}"
 
 @[builtinCommandElab «printAxioms»] def elabPrintAxioms : CommandElab := fun stx => do
   let id := stx[2].getId
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 292bd23cbc..68ad597ba2 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -531,7 +531,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
           | some val => cont val { field with val := FieldVal.term (mkHole field.ref) }
           | none     => do let (val, sNew) ← elabStruct s (some d); let val ← ensureHasType d val; cont val { field with val := FieldVal.nested sNew }
         | FieldVal.default  => do let val ← withRef field.ref $ mkFreshExprMVar (some d); cont (markDefaultMissing val) field
-      | _ => withRef field.ref $ throwFailedToElabField fieldName s.structName msg!"unexpected constructor type{indentExpr type}"
+      | _ => withRef field.ref $ throwFailedToElabField fieldName s.structName m!"unexpected constructor type{indentExpr type}"
     | _ => throwErrorAt field.ref "unexpected unexpanded structure field"
   pure (e, s.setFields fields.reverse)
 
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 6ec7d8da81..157620f057 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -129,7 +129,7 @@ private def synthesizeSyntheticMVarsStep (postponeOnError : Bool) (runTactics :
   -- It would not be incorrect to use `filterM`.
   let remainingSyntheticMVars ← syntheticMVars.filterRevM fun mvarDecl => do
      -- We use `traceM` because we want to make sure the metavar local context is used to trace the message
-     traceM `Elab.postpone (withMVarContext mvarDecl.mvarId do addMessageContext msg!"resuming {mkMVar mvarDecl.mvarId}")
+     traceM `Elab.postpone (withMVarContext mvarDecl.mvarId do addMessageContext m!"resuming {mkMVar mvarDecl.mvarId}")
      let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics
      trace[Elab.postpone]! if succeeded then fmt "succeeded" else fmt "not ready yet"
      pure !succeeded
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 9bb076bbce..c374496ed9 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -279,7 +279,7 @@ def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
     let majorType ← inferType major
     let majorType ← whnf majorType
     matchConstInduct majorType.getAppFn
-      (fun _ => Meta.throwTacticEx `induction mvarId msg!"major premise type is not an inductive type {indentExpr majorType}")
+      (fun _ => Meta.throwTacticEx `induction mvarId m!"major premise type is not an inductive type {indentExpr majorType}")
       (fun val _ => pure val)
 
 private partial def getRecFromUsingLoop (baseRecName : Name) (majorType : Expr) : TacticM (Option Meta.RecursorInfo) := do
diff --git a/src/Lean/Elab/Tactic/Injection.lean b/src/Lean/Elab/Tactic/Injection.lean
index 92c28c240b..5e60eb6a05 100644
--- a/src/Lean/Elab/Tactic/Injection.lean
+++ b/src/Lean/Elab/Tactic/Injection.lean
@@ -16,7 +16,7 @@ private def getInjectionNewIds (stx : Syntax) : List Name :=
 
 private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Unit :=
   unless unusedIds.isEmpty do
-    Meta.throwTacticEx `injection mvarId msg!"too many identifiers provided, unused: {unusedIds}"
+    Meta.throwTacticEx `injection mvarId m!"too many identifiers provided, unused: {unusedIds}"
 
 @[builtinTactic «injection»] def evalInjection : Tactic := fun stx => do
   -- parser! nonReservedSymbol "injection " >> termParser >> withIds
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 768ae6fa4e..6c7f7b10c2 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -364,7 +364,7 @@ def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit := d
         msg ++ " " ++ arg.getAppFn
       else
         msg ++ " …"
-    let msg : MessageData := msg!"don't know how to synthesize implicit argument{indentD msg}"
+    let msg : MessageData := m!"don't know how to synthesize implicit argument{indentD msg}"
     let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId
     logErrorAt mvarErrorInfo.ref msg
   | MVarErrorKind.hole => do
@@ -480,9 +480,9 @@ def applyAttributes (declName : Name) (attrs : Array Attribute) (persistent : Bo
 
 def mkTypeMismatchError (header? : Option String) (e : Expr) (eType : Expr) (expectedType : Expr) : MessageData :=
   let header : MessageData := match header? with
-    | some header => msg!"{header} has type"
-    | none        => msg!"type mismatch{indentExpr e}\nhas type"
-  msg!"{header}{indentExpr eType}\nbut is expected to have type{indentExpr expectedType}"
+    | some header => m!"{header} has type"
+    | none        => m!"type mismatch{indentExpr e}\nhas type"
+  m!"{header}{indentExpr eType}\nbut is expected to have type{indentExpr expectedType}"
 
 def throwTypeMismatchError {α} (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr)
     (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α :=
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index 5e146b4915..a9d2d5934e 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -47,7 +47,7 @@ def throwError {α} (msg : MessageData) : m α := do
   throw $ Exception.error ref msg
 
 def throwUnknownConstant {α} (constName : Name) : m α :=
-  throwError msg!"unknown constant '{mkConst constName}'"
+  throwError m!"unknown constant '{mkConst constName}'"
 
 def throwErrorAt {α} (ref : Syntax) (msg : MessageData) : m α := do
   withRef ref $ throwError msg
@@ -89,14 +89,14 @@ syntax "throwErrorAt! " term:max (interpolatedStr(term) <|> term) : term
 macro_rules
   | `(throwError! $msg) =>
     if msg.getKind == interpolatedStrKind then
-      `(throwError (msg! $msg))
+      `(throwError (m! $msg))
     else
       `(throwError $msg)
 
 macro_rules
   | `(throwErrorAt! $ref $msg) =>
     if msg.getKind == interpolatedStrKind then
-      `(throwErrorAt $ref (msg! $msg))
+      `(throwErrorAt $ref (m! $msg))
     else
       `(throwErrorAt $ref $msg)
 
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 062edb8fcc..22935b8399 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -290,12 +290,9 @@ instance {α} [ToMessageData α] : ToMessageData (Array α) := ⟨fun as => toMe
 instance {α} [ToMessageData α] : ToMessageData (Option α) := ⟨fun | none => "none" | some e => "some (" ++ toMessageData e ++ ")"⟩
 instance : ToMessageData (Option Expr) := ⟨fun | none => "<not-available>" | some e => toMessageData e⟩
 
-syntax:max "msg!" interpolatedStr(term) : term
+syntax:max "m!" interpolatedStr(term) : term
 
 macro_rules
-  | `(msg! $interpStr) => do
-    let chunks := interpStr.getArgs
-    let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toMessageData $a))
-    `(($r : MessageData))
+  | `(m! $interpStr) => do interpStr.expandInterpolatedStr (← `(MessageData)) (← `(toMessageData))
 
 end Lean
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index a3fb5aaf1e..cd766b2e5f 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -62,7 +62,7 @@ private def infer (h : Expr) : MetaM Expr := do
   whnfD hType
 
 private def hasTypeMsg (e type : Expr) : MessageData :=
-  msg!"{indentExpr e}\nhas type{indentExpr type}"
+  m!"{indentExpr e}\nhas type{indentExpr type}"
 
 private def throwAppBuilderException {α} (op : Name) (msg : MessageData) : MetaM α :=
   throwError! "AppBuilder for '{op}', {msg}"
@@ -121,11 +121,11 @@ private def mkEqOfHEqImp (h : Expr) : MetaM Expr := do
   match hType.heq? with
   | some (α, a, β, b) =>
     unless (← isDefEq α β) do
-      throwAppBuilderException `eqOfHEq msg!"heterogeneous equality types are not definitionally equal{indentExpr α}\nis not definitionally equal to{indentExpr β}"
+      throwAppBuilderException `eqOfHEq m!"heterogeneous equality types are not definitionally equal{indentExpr α}\nis not definitionally equal to{indentExpr β}"
     let u ← getLevel α
     pure $ mkApp4 (mkConst `eqOfHEq [u]) α a b h
   | _ =>
-    throwAppBuilderException `HEq.trans msg!"heterogeneous equality proof expected{indentExpr h}"
+    throwAppBuilderException `HEq.trans m!"heterogeneous equality proof expected{indentExpr h}"
 def mkEqOfHEq (h : Expr) : m Expr :=
   liftMetaM $ mkEqOfHEqImp h
 
@@ -209,7 +209,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
         if type.isForall then
           loop type i args.size args instMVars
         else
-          throwAppBuilderException `mkAppM msg!"too many explicit arguments provided to{indentExpr f}\narguments{indentD xs}"
+          throwAppBuilderException `mkAppM m!"too many explicit arguments provided to{indentExpr f}\narguments{indentD xs}"
   loop fType 0 0 #[] #[]
 
 private def mkFun (constName : Name) : MetaM (Expr × Expr) := do
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 55c7dbff38..cc3f6ed03f 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -437,7 +437,7 @@ instance : MonadCache Expr Expr CheckAssignmentM := {
 
 private def addAssignmentInfo (msg : MessageData) : CheckAssignmentM MessageData := do
   let ctx ← read
-  return msg!" @ {mkMVar ctx.mvarId} {ctx.fvars} := {ctx.rhs}"
+  return m!" @ {mkMVar ctx.mvarId} {ctx.fvars} := {ctx.rhs}"
 
 @[specialize] def checkFVar (check : Expr → CheckAssignmentM Expr) (fvar : Expr) : CheckAssignmentM Expr := do
   let ctxMeta ← readThe Meta.Context
diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index 3e03e5ca10..7f4ccab8a6 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -227,7 +227,7 @@ private def restore (env : Environment) (mctx : MetavarContext) (postponed : Per
 private def postponedToMessageData (ps : PersistentArray PostponedEntry) : MessageData := do
   let mut r := MessageData.nil
   for p in ps do
-    r := msg!"{r}\n{p.lhs} =?= {p.rhs}"
+    r := m!"{r}\n{p.lhs} =?= {p.rhs}"
   pure r
 
 @[specialize] def withoutPostponingUniverseConstraintsImp {α} (x : MetaM α) : MetaM α := do
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index b91a7939b6..ed774bd01b 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -29,13 +29,13 @@ namespace Pattern
 instance : Inhabited Pattern := ⟨Pattern.inaccessible (arbitrary _)⟩
 
 partial def toMessageData : Pattern → MessageData
-  | inaccessible e         => msg!".({e})"
+  | inaccessible e         => m!".({e})"
   | var varId              => mkFVar varId
   | ctor ctorName _ _ []   => ctorName
-  | ctor ctorName _ _ pats => msg!"({ctorName}{pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil})"
+  | ctor ctorName _ _ pats => m!"({ctorName}{pats.foldl (fun (msg : MessageData) pat => msg ++ " " ++ toMessageData pat) Format.nil})"
   | val e                  => e
-  | arrayLit _ pats        => msg!"#[{MessageData.joinSep (pats.map toMessageData) ", "}]"
-  | as varId p             => msg!"{mkFVar varId}@{toMessageData p}"
+  | arrayLit _ pats        => m!"#[{MessageData.joinSep (pats.map toMessageData) ", "}]"
+  | as varId p             => m!"{mkFVar varId}@{toMessageData p}"
 
 partial def toExpr : Pattern → MetaM Expr
   | inaccessible e                 => pure e
@@ -176,7 +176,7 @@ def checkAndReplaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : MetaM Alt :
     unless (← isDefEqGuarded fvarDecl.type vType) do
       withExistingLocalDecls alt.fvarDecls do
         throwErrorAt alt.ref $
-          msg!"type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr fvarDecl.type}\nexpected type{indentExpr vType}"
+          m!"type mismatch during dependent match-elimination at pattern variable '{mkFVar fvarDecl.fvarId}' with type{indentExpr fvarDecl.type}\nexpected type{indentExpr vType}"
     pure $ replaceFVarId fvarId v alt
 
 end Alt
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index 3a037737c9..ba8bd84275 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -24,7 +24,7 @@ private def getExpectedNumArgs (e : Expr) : MetaM Nat := do
   pure numArgs
 
 private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α :=
-  throwTacticEx `apply mvarId msg!"failed to unify{indentExpr eType}\nwith{indentExpr targetType}"
+  throwTacticEx `apply mvarId m!"failed to unify{indentExpr eType}\nwith{indentExpr targetType}"
 
 def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit :=
   newMVars.size.forM fun i => do
diff --git a/src/Lean/Meta/Tactic/Clear.lean b/src/Lean/Meta/Tactic/Clear.lean
index 4fa0f7e3c7..fcb972baf8 100644
--- a/src/Lean/Meta/Tactic/Clear.lean
+++ b/src/Lean/Meta/Tactic/Clear.lean
@@ -12,16 +12,16 @@ def clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
     checkNotAssigned mvarId `clear
     let lctx ← getLCtx
     unless lctx.contains fvarId do
-      throwTacticEx `clear mvarId msg!"unknown variable '{mkFVar fvarId}'"
+      throwTacticEx `clear mvarId m!"unknown variable '{mkFVar fvarId}'"
     let tag ← getMVarTag mvarId
     let mctx ← getMCtx
     lctx.forM fun localDecl => do
       unless localDecl.fvarId == fvarId do
         if mctx.localDeclDependsOn localDecl fvarId then
-          throwTacticEx `clear mvarId msg!"variable '{localDecl.toExpr}' depends on '{mkFVar fvarId}'"
+          throwTacticEx `clear mvarId m!"variable '{localDecl.toExpr}' depends on '{mkFVar fvarId}'"
     let mvarDecl ← getMVarDecl mvarId
     if mctx.exprDependsOn mvarDecl.type fvarId then
-      throwTacticEx `clear mvarId msg!"taget depends on '{mkFVar fvarId}'"
+      throwTacticEx `clear mvarId m!"taget depends on '{mkFVar fvarId}'"
     let lctx := lctx.erase fvarId
     let localInsts ← getLocalInstances
     let localInsts := match localInsts.findIdx? $ fun localInst => localInst.fvar.fvarId! == fvarId with
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index e3182050c1..32ac1b3134 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -116,7 +116,7 @@ private partial def finalize
   loop (recursorInfo.paramsPos.length + 1) 0 recursor recursorType false #[]
 
 private def throwUnexpectedMajorType {α} (mvarId : MVarId) (majorType : Expr) : MetaM α :=
-  throwTacticEx `induction mvarId msg!"unexpected major premise type{indentExpr majorType}"
+  throwTacticEx `induction mvarId m!"unexpected major premise type{indentExpr majorType}"
 
 def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array (List Name) := #[]) (useUnusedNames := false) :
     MetaM (Array InductionSubgoal) :=
@@ -129,28 +129,28 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
       recursorInfo.paramsPos.forM fun paramPos? => do
         match paramPos? with
         | none          => pure ()
-        | some paramPos => if paramPos ≥ majorTypeArgs.size then throwTacticEx `induction mvarId msg!"major premise type is ill-formed{indentExpr majorType}"
+        | some paramPos => if paramPos ≥ majorTypeArgs.size then throwTacticEx `induction mvarId m!"major premise type is ill-formed{indentExpr majorType}"
       let mctx ← getMCtx
       let indices ← recursorInfo.indicesPos.toArray.mapM fun idxPos => do
-        if idxPos ≥ majorTypeArgs.size then throwTacticEx `induction mvarId msg!"major premise type is ill-formed{indentExpr majorType}"
+        if idxPos ≥ majorTypeArgs.size then throwTacticEx `induction mvarId m!"major premise type is ill-formed{indentExpr majorType}"
         let idx := majorTypeArgs.get! idxPos
-        unless idx.isFVar do throwTacticEx `induction mvarId msg!"major premise type index {idx} is not a variable{indentExpr majorType}"
+        unless idx.isFVar do throwTacticEx `induction mvarId m!"major premise type index {idx} is not a variable{indentExpr majorType}"
         majorTypeArgs.size.forM fun i => do
           let arg := majorTypeArgs[i]
           if i != idxPos && arg == idx then
-            throwTacticEx `induction mvarId msg!"'{idx}' is an index in major premise, but it occurs more than once{indentExpr majorType}"
+            throwTacticEx `induction mvarId m!"'{idx}' is an index in major premise, but it occurs more than once{indentExpr majorType}"
           if i < idxPos && mctx.exprDependsOn arg idx.fvarId! then
-            throwTacticEx `induction mvarId msg!"'{idx}' is an index in major premise, but it occurs in previous arguments{indentExpr majorType}"
+            throwTacticEx `induction mvarId m!"'{idx}' is an index in major premise, but it occurs in previous arguments{indentExpr majorType}"
           -- If arg is also and index and a variable occurring after `idx`, we need to make sure it doesn't depend on `idx`.
           -- Note that if `arg` is not a variable, we will fail anyway when we visit it.
           if i > idxPos && recursorInfo.indicesPos.contains i && arg.isFVar then
             let idxDecl ← getLocalDecl idx.fvarId!
             if mctx.localDeclDependsOn idxDecl arg.fvarId! then
-              throwTacticEx `induction mvarId msg!"'{idx}' is an index in major premise, but it depends on index occurring at position #{i+1}"
+              throwTacticEx `induction mvarId m!"'{idx}' is an index in major premise, but it depends on index occurring at position #{i+1}"
         pure idx
       let target ← getMVarType mvarId
       if !recursorInfo.depElim && mctx.exprDependsOn target majorFVarId then
-        throwTacticEx `induction mvarId msg!"recursor '{recursorName}' does not support dependent elimination, but conclusion depends on major premise"
+        throwTacticEx `induction mvarId m!"recursor '{recursorName}' does not support dependent elimination, but conclusion depends on major premise"
       -- Revert indices and major premise preserving variable order
       let (reverted, mvarId) ← revert mvarId ((indices.map Expr.fvarId!).push majorFVarId) true
       -- Re-introduce indices and major
@@ -187,7 +187,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
                     if idx ≥ majorTypeFnLevels.size then throwTacticEx `induction mvarId "ill-formed recursor"
                     pure (recursorLevels.push (majorTypeFnLevels.get! idx), foundTargetLevel)
             if !foundTargetLevel && !targetLevel.isZero then
-              throwTacticEx `induction mvarId msg!"recursor '{recursorName}' can only eliminate into Prop"
+              throwTacticEx `induction mvarId m!"recursor '{recursorName}' can only eliminate into Prop"
             let recursor := mkConst recursorName recursorLevels.toList
             let recursor ← addRecParams mvarId majorTypeArgs recursorInfo.paramsPos recursor
             -- Compute motive
diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean
index 41a58315bc..79cc44b127 100644
--- a/src/Lean/Meta/Tactic/Replace.lean
+++ b/src/Lean/Meta/Tactic/Replace.lean
@@ -66,7 +66,7 @@ def replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqPro
 def change (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId := withMVarContext mvarId do
   let target ← getMVarType mvarId
   unless (← isDefEq target targetNew) do
-    throwTacticEx `change mvarId msg!"given type{indentExpr targetNew}\nis not definitionally equal to{indentExpr target}"
+    throwTacticEx `change mvarId m!"given type{indentExpr targetNew}\nis not definitionally equal to{indentExpr target}"
   replaceTargetDefEq mvarId targetNew
 
 def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do
@@ -77,7 +77,7 @@ def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM
     let target ← getMVarType mvarId
     let checkDefEq (typeOld : Expr) : MetaM Unit := do
       unless (← isDefEq typeNew typeOld) do
-        throwTacticEx `changeHypothesis mvarId msg!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
+        throwTacticEx `changeHypothesis mvarId m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
     let finalize (targetNew : Expr) : MetaM MVarId := do
       let mvarId ← replaceTargetDefEq mvarId targetNew
       let (_, mvarId) ← introNP mvarId (numReverted-1)
diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index dd9b2d68aa..3d23dce63a 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -24,15 +24,15 @@ def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) (symm : Bool := false) (oc
     let heq := mkAppN heq newMVars
     let cont (heq heqType : Expr) : MetaM RewriteResult := do
       match (← matchEq? heqType) with
-      | none => throwTacticEx `rewrite mvarId msg!"equality or iff proof expected{indentExpr heqType}"
+      | none => throwTacticEx `rewrite mvarId m!"equality or iff proof expected{indentExpr heqType}"
       | some (α, lhs, rhs) =>
         let cont (heq heqType lhs rhs : Expr) : MetaM RewriteResult := do
           if lhs.getAppFn.isMVar then
-            throwTacticEx `rewrite mvarId msg!"pattern is a metavariable{indentExpr lhs}\nfrom equation{indentExpr heqType}"
+            throwTacticEx `rewrite mvarId m!"pattern is a metavariable{indentExpr lhs}\nfrom equation{indentExpr heqType}"
           let e ← instantiateMVars e
           let eAbst ← kabstract e lhs occs
           unless eAbst.hasLooseBVars do
-            throwTacticEx `rewrite mvarId msg!"did not find instance of the pattern in the target expression{indentExpr lhs}"
+            throwTacticEx `rewrite mvarId m!"did not find instance of the pattern in the target expression{indentExpr lhs}"
           -- construct rewrite proof
           let eNew := eAbst.instantiate1 rhs
           let eNew ← instantiateMVars eNew
diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index 950fb439f2..715843dddc 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -31,7 +31,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
         trace[Meta.Tactic.subst]! "substituting {a} (id: {aFVarId} with {b}"
         let mctx ← getMCtx
         if mctx.exprDependsOn b aFVarId then
-          throwTacticEx `subst mvarId msg!"'{a}' occurs at{indentExpr b}"
+          throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}"
         let aLocalDecl ← getLocalDecl aFVarId
         let (vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true
         let (twoVars, mvarId) ← introNP mvarId 2
@@ -98,7 +98,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
       | _ =>
         let eqMsg := if symm then "(t = x)" else "(x = t)"
         throwTacticEx `subst mvarId
-          msg!"invalid equality proof, it is not of the form {eqMsg}{indentExpr hLocalDecl.type}\nafter WHNF, variable expected, but obtained{indentExpr a}"
+          m!"invalid equality proof, it is not of the form {eqMsg}{indentExpr hLocalDecl.type}\nafter WHNF, variable expected, but obtained{indentExpr a}"
 
 def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId :=
   withMVarContext mvarId do
@@ -113,7 +113,7 @@ def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId :=
         if lhs.isFVar then
           (·.2) <$> substCore mvarId hFVarId
         else do
-          throwTacticEx `subst mvarId msg!"invalid equality proof, it is not of the form (x = t) or (t = x){indentExpr hLocalDecl.type}"
+          throwTacticEx `subst mvarId m!"invalid equality proof, it is not of the form (x = t) or (t = x){indentExpr hLocalDecl.type}"
     | none =>
       let mctx ← getMCtx
       let lctx ← getLCtx
@@ -130,7 +130,7 @@ def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId :=
              else
                pure none
            | _ => pure none
-        | throwTacticEx `subst mvarId msg!"did not find equation for eliminating '{mkFVar hFVarId}'"
+        | throwTacticEx `subst mvarId m!"did not find equation for eliminating '{mkFVar hFVarId}'"
       (·.2) <$> substCore mvarId fvarId symm
 
 builtin_initialize registerTraceClass `Meta.Tactic.subst
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 5aab893d4c..dc2d956bfc 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -212,7 +212,7 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
   x
   let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get
     | panic! "maybeParenthesize: visited a syntax tree without precedences?!"
-  trace[PrettyPrinter.parenthesize]! ("...precedences are {prec} >? {minPrec}" ++ if canJuxtapose then msg!", {(trailPrec, trailCat)} <=? {(st.contPrec, st.contCat)}" else "")
+  trace[PrettyPrinter.parenthesize]! ("...precedences are {prec} >? {minPrec}" ++ if canJuxtapose then m!", {(trailPrec, trailCat)} <=? {(st.contPrec, st.contCat)}" else "")
   -- Should we parenthesize?
   if (prec > minPrec || canJuxtapose && match trailPrec, st.contPrec with some trailPrec, some contPrec => trailCat == st.contCat && trailPrec <= contPrec | _, _ => false) then
       -- The recursive `visit` call, by the invariant, has moved to the preceding node. In order to parenthesize
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 4556b5e6a9..f678dc7fe0 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -146,7 +146,7 @@ syntax "trace[" ident "]!" (interpolatedStr(term) <|> term) : term
 macro_rules
   | `(trace[$id]! $s) =>
     if s.getKind == interpolatedStrKind then
-      `(Lean.trace $(quote id.getId) fun _ => msg! $s)
+      `(Lean.trace $(quote id.getId) fun _ => m! $s)
     else
       `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
 
@@ -170,7 +170,7 @@ def withNestedTraces [MonadFinally m] (x : m α) : m α := do
           currTraces ++ traces -- No nest of nest
         else
           let d := traces.foldl (init := MessageData.nil) fun d elem =>
-            if d.isNil then elem.msg else msg!"{d}\n{elem.msg}"
+            if d.isNil then elem.msg else m!"{d}\n{elem.msg}"
           currTraces.push { ref := ref, msg := MessageData.nestD d }
 
 end Lean
diff --git a/tests/lean/run/catchThe.lean b/tests/lean/run/catchThe.lean
index f4ce6cdddc..0c90f08c61 100644
--- a/tests/lean/run/catchThe.lean
+++ b/tests/lean/run/catchThe.lean
@@ -10,8 +10,8 @@ abbrev M := ExceptT String $ MetaM
 def testM {α} [BEq α] [ToString α] (x : M α) (expected : α)  : MetaM Unit := do
 let r ← x;
 match r with
-| Except.ok a    => unless a == expected do throwError msg!"unexpected result {a}"
-| Except.error e => throwError msg!"FAILED: {e}"
+| Except.ok a    => unless a == expected do throwError m!"unexpected result {a}"
+| Except.error e => throwError m!"FAILED: {e}"
 
 @[noinline] def act1 : M Nat :=
 throwThe Exception $ Exception.error Syntax.missing "Error at act1"
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index de31858848..e28e0a49e5 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -165,10 +165,10 @@ generalizeTelescope majors.toArray fun majors => do
 def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
 withDepElimFrom ex numPats fun majors alts => do
   let majors := majors.map mkFVar
-  trace[Meta.debug]! msg!"majors: {majors.toArray}"
+  trace[Meta.debug]! m!"majors: {majors.toArray}"
   let r ← mkTester elimName majors alts inProp
   unless r.counterExamples.isEmpty do
-    throwError msg!"missing cases:\n{counterExamplesToMessageData r.counterExamples}"
+    throwError m!"missing cases:\n{counterExamplesToMessageData r.counterExamples}"
   unless r.unusedAltIdxs.isEmpty do
     throwError ("unused alternatives: " ++ toString (r.unusedAltIdxs.map fun idx => "#" ++ toString (idx+1)))
   let cinfo ← getConstInfo elimName
diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean
index 0664ae994d..0bd4783959 100644
--- a/tests/lean/run/meta5.lean
+++ b/tests/lean/run/meta5.lean
@@ -16,7 +16,7 @@ withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
   trace[Meta.debug]! r;
   let mctx ← getMCtx;
   mctx.decls.forM fun mvarId mvarDecl => do
-    trace[Meta.debug]! msg!"?{mvarId} : {mvarDecl.type}"
+    trace[Meta.debug]! m!"?{mvarId} : {mvarDecl.type}"
 }
 
 set_option trace.Meta.debug true