diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 66bcfba649..3f1a4ec1c5 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -13,10 +13,10 @@ open Term
 
 private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Unit := do
 for preDef in preDefs do
-  trace[Elab.definition]! msg!"processing {preDef.declName}"
+  trace[Elab.definition]! "processing {preDef.declName}"
   forallTelescope preDef.type fun xs type => do
     let inh ← liftM $ mkInhabitantFor preDef.declName xs type
-    trace[Elab.definition]! msg!"inhabitant for {preDef.declName}"
+    trace[Elab.definition]! "inhabitant for {preDef.declName}"
     addNonRec { preDef with
       kind  := DefKind.«opaque»,
       value := inh }
@@ -53,7 +53,7 @@ if ← logUnassignedUsingErrorInfos pendingMVarIds then
 
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do
 for preDef in preDefs do
-  trace[Elab.definition.body]! msg!"{preDef.declName} : {preDef.type} :=\n{preDef.value}"
+  trace[Elab.definition.body]! "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
 for preDef in preDefs do
   ensureNoUnassignedMVarsAtPreDef preDef
 for preDefs in partitionPreDefs preDefs do
diff --git a/src/Lean/Elab/PreDefinition/MkInhabitant.lean b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
index 387d30f125..0355111873 100644
--- a/src/Lean/Elab/PreDefinition/MkInhabitant.lean
+++ b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
@@ -39,6 +39,6 @@ match ← findAssumption? xs type with
 | none   =>
 match ← mkFnInhabitant? xs type with
 | some val => pure val
-| none => throwError msg!"failed to compile partial definition '{declName}', failed to show that type is inhabited"
+| none => throwError! "failed to compile partial definition '{declName}', failed to show that type is inhabited"
 
 end Lean.Elab
diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index eb342ccc74..37953cf12c 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -85,11 +85,11 @@ let rec loop (i : Nat) : MetaM α := do
         let indIndices := indArgs.extract indInfo.nparams indArgs.size
         if !indIndices.all Expr.isFVar then
           orelseMergeErrors
-            (throwError msg!"argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
+            (throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
             (loop (i+1))
         else if !indIndices.allDiff then
           orelseMergeErrors
-            (throwError msg!"argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
+            (throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
             (loop (i+1))
         else
           let indexMinPos := getIndexMinPos xs indIndices
@@ -99,13 +99,13 @@ let rec loop (i : Nat) : MetaM α := do
           match ← hasBadIndexDep? ys indIndices with
           | some (index, y) =>
             orelseMergeErrors
-              (throwError msg!"argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
+              (throwError! "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
               (loop (i+1))
           | none =>
             match ← hasBadParamDep? ys indParams with
             | some (indParam, y) =>
               orelseMergeErrors
-                (throwError msg!"argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
+                (throwError! "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
                 (loop (i+1))
             | none =>
               let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
@@ -129,7 +129,7 @@ private def ensureNoRecFn (recFnName : Name) (e : Expr) : MetaM Expr := do
 if containsRecFn recFnName e then
   Meta.forEachExpr e fun e => do
     if e.isAppOf recFnName then
-      throwError msg!"unexpected occurrence of recursive application{indentExpr e}"
+      throwError! "unexpected occurrence of recursive application{indentExpr e}"
   pure e
 else
   pure e
@@ -141,7 +141,7 @@ throwError "toBelow failed"
 private partial def toBelowAux (C : Expr) : Expr → Expr → Expr → MetaM Expr
 | belowDict, arg, F => do
   belowDict ← whnf belowDict
-  trace[Elab.definition.structural]! msg!"belowDict: {belowDict}, arg: {arg}"
+  trace[Elab.definition.structural]! "belowDict: {belowDict}, arg: {arg}"
   match belowDict with
   | Expr.app (Expr.app (Expr.const `PProd _ _) d1 _) d2 _ =>
     (do toBelowAux C d1 arg (← mkAppM `PProd.fst #[F]))
@@ -167,10 +167,10 @@ private partial def toBelowAux (C : Expr) : Expr → Expr → Expr → MetaM Exp
 /- See toBelow -/
 private def withBelowDict {α} (below : Expr) (numIndParams : Nat) (k : Expr → Expr → MetaM α) : MetaM α := do
 let belowType ← inferType below
-trace[Elab.definition.structural]! msg!"belowType: {belowType}"
+trace[Elab.definition.structural]! "belowType: {belowType}"
 belowType.withApp fun f args => do
   let motivePos := numIndParams + 1
-  unless motivePos < args.size do throwError msg!"unexpected 'below' type{indentExpr belowType}"
+  unless motivePos < args.size do throwError! "unexpected 'below' type{indentExpr belowType}"
   let pre := mkAppN f (args.extract 0 numIndParams)
   let preType ← inferType pre
   forallBoundedTelescope preType (some 1) fun x _ => do
@@ -225,9 +225,9 @@ let rec loop : Expr → Expr → MetaM Expr
           let numFixed  := recArgInfo.fixedParams.size
           let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos
           if recArgPos >= args.size then
-            throwError msg!"insufficient number of parameters at recursive application {indentExpr e}"
+            throwError! "insufficient number of parameters at recursive application {indentExpr e}"
           let recArg := args[recArgPos]
-          let f ← try toBelow below recArgInfo.indParams.size recArg catch  _ => throwError msg!"failed to eliminate recursive application{indentExpr e}"
+          let f ← try toBelow below recArgInfo.indParams.size recArg catch  _ => throwError! "failed to eliminate recursive application{indentExpr e}"
           -- Recall that the fixed parameters are not in the scope of the `brecOn`. So, we skip them.
           let argsNonFixed := args.extract numFixed args.size
           -- The function `f` does not explicitly take `recArg` and its indices as arguments. So, we skip them too.
@@ -279,9 +279,9 @@ let rec loop : Expr → Expr → MetaM Expr
         do let matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
            let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
             lambdaTelescope alt fun xs altBody => do
-              trace[Elab.definition.structural]! msg!"altNumParams: {numParams}, xs: {xs}"
+              trace[Elab.definition.structural]! "altNumParams: {numParams}, xs: {xs}"
               unless xs.size >= numParams do
-                throwError msg!"unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
+                throwError! "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
               let belowForAlt := xs[numParams - 1]
               mkLambdaFVars xs (← loop belowForAlt altBody)
            pure { matcherApp with alts := altsNew }.toExpr
@@ -295,12 +295,12 @@ let major := recArgInfo.ys[recArgInfo.pos]
 let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
 let motive ← mkForallFVars otherArgs type
 let brecOnUniv ← getLevel motive
-trace[Elab.definition.structural]! msg!"brecOn univ: {brecOnUniv}"
+trace[Elab.definition.structural]! "brecOn univ: {brecOnUniv}"
 let useBInductionOn := recArgInfo.reflexive && brecOnUniv == levelZero
 if recArgInfo.reflexive && brecOnUniv != levelZero then
   brecOnUniv ← decLevel brecOnUniv
 let motive ← mkLambdaFVars (recArgInfo.indIndices.push major) motive
-trace[Elab.definition.structural]! msg!"brecOn motive: {motive}"
+trace[Elab.definition.structural]! "brecOn motive: {motive}"
 let brecOn :=
   if useBInductionOn then
     Lean.mkConst (mkBInductionOnFor recArgInfo.indName) recArgInfo.indLevels
@@ -312,8 +312,8 @@ let brecOn := mkAppN brecOn recArgInfo.indIndices
 let brecOn := mkApp brecOn major
 check brecOn
 let brecOnType ← inferType brecOn
-trace[Elab.definition.structural]! msg!"brecOn     {brecOn}"
-trace[Elab.definition.structural]! msg!"brecOnType {brecOnType}"
+trace[Elab.definition.structural]! "brecOn     {brecOn}"
+trace[Elab.definition.structural]! "brecOnType {brecOnType}"
 forallBoundedTelescope brecOnType (some 1) fun F _ => do
   let F := F[0]
   let FType ← inferType F
@@ -334,13 +334,13 @@ forallBoundedTelescope brecOnType (some 1) fun F _ => do
 private def elimRecursion (preDef : PreDefinition) : MetaM PreDefinition :=
 withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
   addAsAxiom preDef
-  trace[Elab.definition.structural]! msg!"{preDef.declName} {xs} :=\n{value}"
+  trace[Elab.definition.structural]! "{preDef.declName} {xs} :=\n{value}"
   let numFixed := getFixedPrefix preDef.declName xs value
   findRecArg numFixed xs fun recArgInfo => do
     -- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
     let valueNew ← mkBRecOn preDef.declName recArgInfo value
     let valueNew ← mkLambdaFVars xs valueNew
-    trace[Elab.definition.structural]! msg!"result: {valueNew}"
+    trace[Elab.definition.structural]! "result: {valueNew}"
     -- Recursive applications may still occur in expressions that were not visited by replaceRecApps (e.g., in types)
     let valueNew ← ensureNoRecFn preDef.declName valueNew
     pure { preDef with value := valueNew }
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 0930f8061a..889cad478a 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -20,7 +20,7 @@ def goalsToMessageData (goals : List MVarId) : MessageData :=
 MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
 
 def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
-throwError msg!"unsolved goals\n{goalsToMessageData goals}"
+throwError! "unsolved goals\n{goalsToMessageData goals}"
 
 namespace Tactic
 
@@ -93,7 +93,7 @@ mkElabAttribute Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tac
 
 private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tactic) : TacticM Unit := do
 let rec loop : List Tactic → TacticM Unit
-  | []              => throwErrorAt stx msg!"unexpected syntax {indentD stx}"
+  | []              => throwErrorAt! stx "unexpected syntax {indentD stx}"
   | evalFn::evalFns => do
     try
       evalFn stx
@@ -117,7 +117,7 @@ mutual
 
 partial def expandTacticMacroFns (stx : Syntax) (macros : List Macro) : TacticM Unit :=
 let rec loop : List Macro → TacticM Unit
-  | []    => throwErrorAt stx msg!"tactic '{stx.getKind}' has not been implemented"
+  | []    => throwErrorAt! stx "tactic '{stx.getKind}' has not been implemented"
   | m::ms => do
     let scp ← getCurrMacroScope
     try
@@ -177,7 +177,7 @@ let e ← instantiateMVars e
 let pendingMVars ← getMVars e
 Term.logUnassignedUsingErrorInfos pendingMVars
 if e.hasExprMVar then
-  throwError msg!"tactic failed, resulting expression contains metavariables{indentExpr e}"
+  throwError! "tactic failed, resulting expression contains metavariables{indentExpr e}"
 
 def withMainMVarContext {α} (x : TacticM α) : TacticM α := do
 let (mvarId, _) ← getMainGoal
@@ -286,7 +286,7 @@ fun stx => pure ()
 fun stx => do
   let tactic := stx.getArg 1
   if (← do try evalTactic tactic; pure true catch _ => pure false) then
-    throwError ("tactic succeeded")
+    throwError "tactic succeeded"
 
 @[builtinTactic traceState] def evalTraceState : Tactic :=
 fun stx => do
@@ -345,7 +345,7 @@ withRef id do
 let fvar? ← liftTermElabM $ Term.isLocalIdent? id;
 match fvar? with
 | some fvar => pure fvar.fvarId!
-| none      => throwError msg!"unknown variable '{id.getId}'"
+| none      => throwError! "unknown variable '{id.getId}'"
 
 def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do
 withMainMVarContext $ ids.mapM getFVarId
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 58f69dd7ed..98a7249bc8 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -96,9 +96,9 @@ private def getAltRHS (alt : Syntax) : Syntax := alt.getArg 3
 private def checkAltCtorNames (alts : Array Syntax) (ctorNames : List Name) : TacticM Unit := do
 for alt in alts do
   let n := getAltName alt
-  withRef alt $ trace[Elab.checkAlt]! msg!"{n} , {alt}"
+  withRef alt $ trace[Elab.checkAlt]! "{n} , {alt}"
   unless n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName) do
-    throwErrorAt (alt.getArg 0) msg!"invalid constructor name '{n}'"
+    throwErrorAt! (alt.getArg 0) "invalid constructor name '{n}'"
 
 structure RecInfo :=
 (recName : Name)
@@ -143,7 +143,7 @@ match ← getRecFromUsingLoop baseRecName (← inferType major) with
   try
     liftMetaMAtMain fun _ => Meta.mkRecursorInfo recName
   catch _ =>
-    throwError msg!"invalid recursor name '{baseRecName}'"
+    throwError! "invalid recursor name '{baseRecName}'"
 
 /- Create `RecInfo` assuming builtin recursor -/
 private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAlts : Bool) : TacticM (RecInfo × Array Name) := do
@@ -183,7 +183,7 @@ else
               altVars := altVars.push []
               altRHSs := altRHSs.push Syntax.missing
             else
-              throwError msg!"alternative for constructor '{ctorName}' is missing"
+              throwError! "alternative for constructor '{ctorName}' is missing"
   unless remainingAlts.isEmpty do
     throwErrorAt remainingAlts[0] "unused alternative"
   pure ({ recName := recName, altVars := altVars, altRHSs := altRHSs }, ctorNames.toArray)
@@ -238,7 +238,7 @@ else
               altVars := altVars.push (getAltVarNames alt).toList
               altRHSs := altRHSs.push (getAltRHS alt)
             | none     =>
-              throwError msg!"alternative for minor premise '{paramName}' is missing"
+              throwError! "alternative for minor premise '{paramName}' is missing"
     unless remainingAlts.isEmpty do
       throwErrorAt remainingAlts[0] "unused alternative"
     pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
@@ -252,7 +252,7 @@ if altRHSs.isEmpty then
   setGoals $ result.toList.map fun s => s.mvarId
 else
   unless altRHSs.size == result.size do
-    throwError msg!"mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})"
+    throwError! "mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})"
   let gs := []
   for i in [:result.size] do
     let subgoal := result[i]
@@ -299,12 +299,12 @@ let rec loop (i j : Nat) : TacticM Unit :=
         if ctorName == subgoal.ctorName then
           loop (i+1) (j+1)
         else
-          throwError msg!"alternative for '{subgoal.ctorName}' has not been provided"
+          throwError! "alternative for '{subgoal.ctorName}' has not been provided"
       else
-        throwError msg!"alternative for '{ctorName}' is not needed"
+        throwError! "alternative for '{ctorName}' is not needed"
   else if h : i < casesResult.size then
     let subgoal := casesResult.get ⟨i, h⟩
-    throwError msg!"alternative for '{subgoal.ctorName}' has not been provided"
+    throwError! "alternative for '{subgoal.ctorName}' has not been provided"
   else
     pure ()
 unless altRHSs.isEmpty do
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index ef8941fbf0..c772b3b29f 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -103,3 +103,26 @@ when (curr == max) $ throwError maxRecDepthErrorMessage;
 MonadRecDepth.withRecDepth (curr+1) x
 
 end Lean
+
+new_frontend
+
+namespace Lean
+
+syntax "throwError! " ((interpolatedStr term) <|> term) : term
+syntax "throwErrorAt! " term:max ((interpolatedStr term) <|> term) : term
+
+macro_rules
+| `(throwError! $msg) =>
+  if msg.getKind == interpolatedStrKind then
+    `(throwError (msg! $msg))
+  else
+    `(throwError $msg)
+
+macro_rules
+| `(throwErrorAt! $ref $msg) =>
+  if msg.getKind == interpolatedStrKind then
+    `(throwErrorAt $ref (msg! $msg))
+  else
+    `(throwErrorAt $ref $msg)
+
+end Lean
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index d7327cec84..143c2b5b9c 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -135,9 +135,13 @@ namespace Lean
 
 macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData))
 
-syntax "trace[" ident "]!" term : term
+syntax "trace[" ident "]!" ((interpolatedStr term) <|> term) : term
 
 macro_rules
-| `(trace[$id]! $s) => `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
+| `(trace[$id]! $s) =>
+  if s.getKind == interpolatedStrKind then
+    `(Lean.trace $(quote id.getId) fun _ => msg! $s)
+  else
+    `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
 
 end Lean