diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 6d6caeb989..9022129c48 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -292,13 +292,13 @@ private def propagateExpectedType (arg : Arg) : M Unit := do
           modify fun s => { s with propagateExpected := false }
         else
           let numRemainingArgs := s.args.length
-          trace[Elab.app.propagateExpectedType]! "etaArgs.size: {s.etaArgs.size}, numRemainingArgs: {numRemainingArgs}, fType: {s.fType}"
+          trace[Elab.app.propagateExpectedType] "etaArgs.size: {s.etaArgs.size}, numRemainingArgs: {numRemainingArgs}, fType: {s.fType}"
           match getForallBody s.explicit numRemainingArgs s.namedArgs s.fType with
           | none           => pure ()
           | some fTypeBody =>
             unless fTypeBody.hasLooseBVars do
               unless (← hasOptAutoParams fTypeBody) do
-                trace[Elab.app.propagateExpectedType]! "{expectedType} =?= {fTypeBody}"
+                trace[Elab.app.propagateExpectedType] "{expectedType} =?= {fTypeBody}"
                 if (← isDefEq expectedType fTypeBody) then
                   /- Note that we only set `propagateExpected := false` when propagation has succeeded. -/
                   modify fun s => { s with propagateExpected := false }
@@ -319,7 +319,7 @@ private def finalize : M Expr := do
   let s ← get
   let mut e := s.f
   -- all user explicit arguments have been consumed
-  trace[Elab.app.finalize]! e
+  trace[Elab.app.finalize] e
   let ref ← getRef
   -- Register the error context of implicits
   for mvarId in s.toSetErrorCtx do
@@ -331,11 +331,11 @@ private def finalize : M Expr := do
     `s.etaArgs.isEmpty`. Reason: it may have been unfolded.
   -/
   let eType ← inferType e
-  trace[Elab.app.finalize]! "after etaArgs, {e} : {eType}"
+  trace[Elab.app.finalize] "after etaArgs, {e} : {eType}"
   match s.expectedType? with
   | none              => pure ()
   | some expectedType =>
-     trace[Elab.app.finalize]! "expected type: {expectedType}"
+     trace[Elab.app.finalize] "expected type: {expectedType}"
      -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
      discard <| isDefEq expectedType eType
   synthesizeAppInstMVars
@@ -485,7 +485,7 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
     (expectedType? : Option Expr) (explicit ellipsis : Bool) : TermElabM Expr := do
   let fType ← inferType f
   let fType ← instantiateMVars fType
-  trace[Elab.app.args]! "explicit: {explicit}, {f} : {fType}"
+  trace[Elab.app.args] "explicit: {explicit}, {f} : {fType}"
   unless namedArgs.isEmpty && args.isEmpty do
     tryPostponeIfMVar fType
   ElabAppArgs.main.run' {
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 0da728b456..e0287d4159 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -64,7 +64,7 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
     let tactic ← quoteAutoTactic tactic
     let val ← elabTerm tactic type
     let val ← instantiateMVars val
-    trace[Elab.autoParam]! val
+    trace[Elab.autoParam] val
     let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque,
                                        safety := DefinitionSafety.safe }
     addDecl decl
@@ -518,7 +518,7 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
       let type ← mkForallFVars xs type
       let val  ← mkLambdaFVars xs val
       pure (type, val, xs.size)
-  trace[Elab.let.decl]! "{id.getId} : {type} := {val}"
+  trace[Elab.let.decl] "{id.getId} : {type} := {val}"
   let result ←
     if useLetExpr then
       withLetDecl id.getId type val fun x => do
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 87b1cf1e7e..3711e4d4b1 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -154,7 +154,6 @@ private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
 
 @[builtinTermElab Lean.Parser.Term.decide] def elabDecide : TermElab := fun stx expectedType? => do
   let p ← getPropToDecide expectedType?
-  trace[Meta.debug]! "elabDecide: {p}"
   let d ← mkDecide p
   let d ← instantiateMVars d
   let r ← withDefault <| whnf d
diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index 58105bb064..7357f952f7 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -94,7 +94,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
 private def mkBEqInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
   let ctx ← mkContext "beq" declNames[0]
   let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq declNames)
-  trace[Elab.Deriving.beq]! "\n{cmds}"
+  trace[Elab.Deriving.beq] "\n{cmds}"
   return cmds
 
 open Command
diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 1f661652ee..676824da7f 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -90,7 +90,7 @@ def mkAuxFunction (ctx : Context) : TermElabM Syntax := do
 def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do
   let ctx ← mkContext "decEq" indVal.name
   let cmds := #[← mkAuxFunction ctx] ++ (← mkInstanceCmds ctx `DecidableEq #[indVal.name] (useAnonCtor := false))
-  trace[Elab.Deriving.decEq]! "\n{cmds}"
+  trace[Elab.Deriving.decEq] "\n{cmds}"
   return cmds
 
 open Command
diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean
index 80083a91a7..ff386ffc3c 100644
--- a/src/Lean/Elab/Deriving/Inhabited.lean
+++ b/src/Lean/Elab/Deriving/Inhabited.lean
@@ -30,7 +30,7 @@ where
         let instType ← mkAppM `Inhabited #[x]
         if (← isTypeCorrect instType) then
           withLocalDeclD (← mkFreshUserName `inst) instType fun inst => do
-            trace[Elab.Deriving.inhabited]! "adding local instance {instType}"
+            trace[Elab.Deriving.inhabited] "adding local instance {instType}"
             addLocalInstancesForParamsAux k xs (i+1) (map.insert inst.fvarId! i)
         else
           addLocalInstancesForParamsAux k xs (i+1) map
@@ -89,20 +89,20 @@ where
         for i in [ctorVal.numParams:xs.size] do
           let x := xs[i]
           let instType ← mkAppM `Inhabited #[(← inferType x)]
-          trace[Elab.Deriving.inhabited]! "checking {instType} for '{ctorName}'"
+          trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'"
           match (← trySynthInstance instType) with
           | LOption.some e =>
             usedInstIdxs ← collectUsedLocalsInsts usedInstIdxs localInst2Index e
           | _ =>
-            trace[Elab.Deriving.inhabited]! "failed to generate instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
+            trace[Elab.Deriving.inhabited] "failed to generate instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
             ok := false
             break
         if !ok then
           return none
         else
-          trace[Elab.Deriving.inhabited]! "inhabited instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
+          trace[Elab.Deriving.inhabited] "inhabited instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
           let cmd ← mkInstanceCmdWith usedInstIdxs
-          trace[Elab.Deriving.inhabited]! "\n{cmd}"
+          trace[Elab.Deriving.inhabited] "\n{cmd}"
           return some cmd
 
 private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do
diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 3f2a3950ee..a2b70237e3 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -108,7 +108,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
 private def mkReprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
   let ctx ← mkContext "repr" declNames[0]
   let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr declNames)
-  trace[Elab.Deriving.repr]! "\n{cmds}"
+  trace[Elab.Deriving.repr] "\n{cmds}"
   return cmds
 
 open Command
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index 3c4ef885aa..0b8240ea15 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -61,7 +61,7 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
     match typeName.eraseMacroScopes with
     | Name.str _ t _ => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
     | _              => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
-  trace[Elab.Deriving.beq]! "{auxFunNames}"
+  trace[Elab.Deriving.beq] "{auxFunNames}"
   let usePartial := indVal.isNested || typeInfos.size > 1
   return {
     typeInfos   := typeInfos
@@ -104,7 +104,6 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
       let type         ← `($(mkIdent className) $indType)
       let val          ← if useAnonCtor then `(⟨$(mkIdent auxFunName)⟩) else pure <| mkIdent auxFunName
       let instCmd ← `(instance $binders:implicitBinder* : $type := $val)
-      trace[Meta.debug]! "\n{instCmd}"
       instances := instances.push instCmd
   return instances
 
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 7248cff342..c40bac67bf 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1541,7 +1541,7 @@ def elabDo : TermElab := fun stx expectedType? => do
   let m ← mkMonadAlias bindInfo.m
   let codeBlock ← ToCodeBlock.run stx m
   let stxNew ← liftMacroM $ ToTerm.run codeBlock.code m
-  trace[Elab.do]! stxNew
+  trace[Elab.do] stxNew
   withMacroExpansion stx stxNew $ elabTermEnsuringType stxNew bindInfo.expectedType
 
 end Do
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 1fee1b8b8e..51ae332744 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -215,7 +215,6 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
           let ctorParams ← Term.addAutoBoundImplicits ctorParams
           let type ← mkForallFVars ctorParams type
           let type ← mkForallFVars params type
-          trace[Meta.debug]! "{ctorView.declName} : {type}"
           return { name := ctorView.declName, type := type }
 where
   checkParamOccs (ctorType : Expr) : MetaM Expr :=
@@ -339,7 +338,7 @@ private def updateResultingUniverse (numParams : Nat) (indTypes : List Inductive
   unless r.isParam do
     throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly"
   let us ← collectUniverses r rOffset numParams indTypes
-  trace[Elab.inductive]! "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
+  trace[Elab.inductive] "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
   let rNew := mkResultUniverse us rOffset
   let updateLevel (e : Expr) : Expr := e.replaceLevel fun u => if u == tmpIndParam then some rNew else none
   return indTypes.map fun indType =>
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 575304f383..e26927a2c5 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -47,7 +47,7 @@ private def elabDiscrsWitMatchType (discrStxs : Array Syntax) (matchType : Expr)
     match matchType with
     | Expr.forallE _ d b _ =>
       let discr ← fullApproxDefEq <| elabTermEnsuringType discrStx[1] d
-      trace[Elab.match]! "discr #{i} {discr} : {d}"
+      trace[Elab.match] "discr #{i} {discr} : {d}"
       if b.hasLooseBVars then
         isDep := true
       matchType ← b.instantiate1 discr
@@ -473,7 +473,7 @@ where
 
 def main (alt : MatchAltView) : M MatchAltView := do
   let patterns ← alt.patterns.mapM fun p => do
-    trace[Elab.match]! "collecting variables at pattern: {p}"
+    trace[Elab.match] "collecting variables at pattern: {p}"
     collect p
   return { alt with patterns := patterns }
 
@@ -552,13 +552,13 @@ def finalizePatternDecls (patternVarDecls : Array PatternVarDecl) : TermElabM (A
       decls := decls.push decl
     | PatternVarDecl.anonymousVar mvarId fvarId =>
        let e ← instantiateMVars (mkMVar mvarId);
-       trace[Elab.match]! "finalizePatternDecls: mvarId: {mvarId} := {e}, fvar: {mkFVar fvarId}"
+       trace[Elab.match] "finalizePatternDecls: mvarId: {mvarId} := {e}, fvar: {mkFVar fvarId}"
        match e with
        | Expr.mvar newMVarId _ =>
          /- Metavariable was not assigned, or assigned to another metavariable. So,
             we assign to the auxiliary free variable we created at `withPatternVars` to `newMVarId`. -/
          assignExprMVar newMVarId (mkFVar fvarId)
-         trace[Elab.match]! "finalizePatternDecls: {mkMVar newMVarId} := {mkFVar fvarId}"
+         trace[Elab.match] "finalizePatternDecls: {mkMVar newMVarId} := {mkFVar fvarId}"
          let decl ← getLocalDecl fvarId
          let decl ← instantiateLocalDeclMVars decl
          decls := decls.push decl
@@ -683,13 +683,13 @@ private def withElaboratedLHS {α} (ref : Syntax) (patternVarDecls : Array Patte
 
 def elabMatchAltView (alt : MatchAltView) (matchType : Expr) : TermElabM (AltLHS × Expr) := withRef alt.ref do
   let (patternVars, alt) ← collectPatternVars alt
-  trace[Elab.match]! "patternVars: {patternVars}"
+  trace[Elab.match] "patternVars: {patternVars}"
   withPatternVars patternVars fun patternVarDecls => do
     withElaboratedLHS alt.ref patternVarDecls alt.patterns matchType fun altLHS matchType => do
       let rhs ← elabTermEnsuringType alt.rhs matchType
       let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr
       let rhs ← if xs.isEmpty then pure <| mkSimpleThunk rhs else mkLambdaFVars xs rhs
-      trace[Elab.match]! "rhs: {rhs}"
+      trace[Elab.match] "rhs: {rhs}"
       return (altLHS, rhs)
 
 def mkMatcher (elimName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : TermElabM MatcherResult :=
@@ -730,7 +730,7 @@ private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltVi
   let (discrs, matchType, altLHSS, isDep, rhss) ← commitIfDidNotPostpone do
     let ⟨discrs, matchType, isDep, altViews⟩ ← elabMatchTypeAndDiscrs discrStxs matchOptType altViews expectedType
     let matchAlts ← liftMacroM <| expandMacrosInPatterns altViews
-    trace[Elab.match]! "matchType: {matchType}"
+    trace[Elab.match] "matchType: {matchType}"
     let alts ← matchAlts.mapM fun alt => elabMatchAltView alt matchType
     /-
      We should not use `synthesizeSyntheticMVarsNoPostponing` here. Otherwise, we will not be
@@ -796,7 +796,7 @@ private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltVi
     let r := mkApp matcherResult.matcher motive
     let r := mkAppN r discrs
     let r := mkAppN r rhss
-    trace[Elab.match]! "result: {r}"
+    trace[Elab.match] "result: {r}"
     return r
 
 private def getDiscrs (matchStx : Syntax) : Array Syntax :=
@@ -852,7 +852,7 @@ private def tryPostponeIfDiscrTypeIsMVar (matchStx : Syntax) : TermElabM Unit :=
       | none   => throwErrorAt discr "unexpected discriminant" -- see `expandNonAtomicDiscrs?
       | some d =>
         let dType ← inferType d
-        trace[Elab.match]! "discr {d} : {dType}"
+        trace[Elab.match] "discr {d} : {dType}"
         tryPostponeIfMVar dType
 
 /-
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 79510a8037..1358f0754d 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -438,7 +438,7 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
   match pickMaxFVar? lctx toProcess with
   | none        => pure ()
   | some fvarId =>
-    trace[Elab.definition.mkClosure]! "toProcess: {toProcess.map mkFVar}, maxVar: {mkFVar fvarId}"
+    trace[Elab.definition.mkClosure] "toProcess: {toProcess.map mkFVar}, maxVar: {mkFVar fvarId}"
     let toProcess := toProcess.erase fvarId
     let localDecl ← getLocalDecl fvarId
     match localDecl with
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 5abd5fbd44..ae3b3b5774 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -12,10 +12,10 @@ open Term
 
 private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
-    trace[Elab.definition]! "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]! "inhabitant for {preDef.declName}"
+      trace[Elab.definition] "inhabitant for {preDef.declName}"
       addNonRec { preDef with
         kind  := DefKind.«opaque»,
         value := inh
@@ -53,11 +53,11 @@ private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM
 
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
-    trace[Elab.definition.body]! "{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
-    trace[Elab.definition.scc]! "{preDefs.map (·.declName)}"
+    trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
     if preDefs.size == 1 && isNonRecursive preDefs[0] then
       let preDef := preDefs[0]
       if preDef.modifiers.isNoncomputable then
diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index 87897a85f6..c404fa4b37 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -183,7 +183,7 @@ private def throwToBelowFailed {α} : MetaM α :=
 private partial def toBelowAux (C : Expr) : Expr → Expr → Expr → MetaM Expr
   | belowDict, arg, F => do
     let belowDict ← whnf belowDict
-    trace[Elab.definition.structural]! "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]))
@@ -209,7 +209,7 @@ 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]! "belowType: {belowType}"
+  trace[Elab.definition.structural] "belowType: {belowType}"
   belowType.withApp fun f args => do
     let motivePos := numIndParams + 1
     unless motivePos < args.size do throwError! "unexpected 'below' type{indentExpr belowType}"
@@ -321,12 +321,12 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
              To make it work, users have to write the third alternative as `| zs => g zs + 2`
              If this is too annoying in practice, we may replace `ys` with the matching term, but
              this may generate weird error messages, when it doesn't work. -/
-          trace[Elab.definition.structural]! "below before matcherApp.addArg: {below} : {← inferType below}"
+          trace[Elab.definition.structural] "below before matcherApp.addArg: {below} : {← inferType below}"
           let matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
           modify fun s => { s with matcherBelowDep := s.matcherBelowDep.insert matcherApp.matcherName }
           let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
             lambdaTelescope alt fun xs altBody => do
-              trace[Elab.definition.structural]! "altNumParams: {numParams}, xs: {xs}"
+              trace[Elab.definition.structural] "altNumParams: {numParams}, xs: {xs}"
               unless xs.size >= numParams do
                 throwError! "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
               let belowForAlt := xs[numParams - 1]
@@ -340,15 +340,15 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
   let type  := (← inferType value).headBeta
   let major := recArgInfo.ys[recArgInfo.pos]
   let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
-  trace[Elab.definition.structural]! "fixedParams: {recArgInfo.fixedParams}, otherArgs: {otherArgs}"
+  trace[Elab.definition.structural] "fixedParams: {recArgInfo.fixedParams}, otherArgs: {otherArgs}"
   let motive ← mkForallFVars otherArgs type
   let mut brecOnUniv ← getLevel motive
-  trace[Elab.definition.structural]! "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]! "brecOn motive: {motive}"
+  trace[Elab.definition.structural] "brecOn motive: {motive}"
   let brecOn :=
     if useBInductionOn then
       Lean.mkConst (mkBInductionOnName recArgInfo.indName) recArgInfo.indLevels
@@ -360,12 +360,12 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
   let brecOn := mkApp brecOn major
   check brecOn
   let brecOnType ← inferType brecOn
-  trace[Elab.definition.structural]! "brecOn     {brecOn}"
-  trace[Elab.definition.structural]! "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
-    trace[Elab.definition.structural]! "FType: {FType}"
+    trace[Elab.definition.structural] "FType: {FType}"
     let FType ← instantiateForall FType recArgInfo.indIndices
     let FType ← instantiateForall FType #[major]
     forallBoundedTelescope FType (some 1) fun below _ => do
@@ -378,14 +378,14 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
 private def elimRecursion (preDef : PreDefinition) : M PreDefinition :=
   withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
     addAsAxiom preDef
-    trace[Elab.definition.structural]! "{preDef.declName} {xs} :=\n{value}"
+    trace[Elab.definition.structural] "{preDef.declName} {xs} :=\n{value}"
     let numFixed ← getFixedPrefix preDef.declName xs value
-    trace[Elab.definition.structural]! "numFixed: {numFixed}"
+    trace[Elab.definition.structural] "numFixed: {numFixed}"
     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]! "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/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 64c2c00d80..a092d6aa4b 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -403,7 +403,7 @@ private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Ar
         (floatedLetDecls.push (← `(letDecl|rhs $vars:ident* := $rhs)), (pats, rhs'))
 
 private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : TermElabM Syntax := do
-  trace[Elab.match_syntax]! "match {discrs} with {alts}"
+  trace[Elab.match_syntax] "match {discrs} with {alts}"
   match discrs, alts with
   | [],            ([], rhs)::_ => pure rhs  -- nothing left to match
   | _,             []           => throwError "non-exhaustive 'match_syntax'"
@@ -461,7 +461,7 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
       -- no quotations => fall back to regular `match`
       throwUnsupportedSyntax
     let stx ← compileStxMatch discrs.toList (patss.map (·.toList) |>.zip rhss).toList
-    trace[Elab.match_syntax.result]! "{stx}"
+    trace[Elab.match_syntax.result] "{stx}"
     stx
   | _ => throwUnsupportedSyntax
 
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 47e9d0c186..328fa2ccd6 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -127,9 +127,9 @@ private def elabModifyOp (stx modifyOp source : Syntax) (expectedType? : Option
     let idx  := lval[1]
     let self := source[0]
     let stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val))
-    trace[Elab.struct.modifyOp]! "{stx}\n===>\n{stxNew}"
+    trace[Elab.struct.modifyOp] "{stx}\n===>\n{stxNew}"
     withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
-  trace[Elab.struct.modifyOp]! "{modifyOp}\nSource: {source}"
+  trace[Elab.struct.modifyOp] "{modifyOp}\nSource: {source}"
   let rest := modifyOp[0][1]
   if rest.isNone then
     cont modifyOp[2]
@@ -143,7 +143,7 @@ private def elabModifyOp (stx modifyOp source : Syntax) (expectedType? : Option
     let valSource := source.modifyArg 0 fun _ => s
     let val       := stx.setArg 1 valSource
     let val       := val.setArg 2 <| mkNullNode #[mkNullNode #[valField, mkNullNode]]
-    trace[Elab.struct.modifyOp]! "{stx}\nval: {val}"
+    trace[Elab.struct.modifyOp] "{stx}\nval: {val}"
     cont val
 
 /- Get structure name and elaborate explicit source (if available) -/
@@ -789,7 +789,7 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
   | Except.error ex  => throwError ex
   | Except.ok struct =>
     let struct ← expandStruct struct
-    trace[Elab.struct]! "{struct}"
+    trace[Elab.struct] "{struct}"
     let (r, struct) ← elabStruct struct expectedType?
     DefaultFields.propagate struct
     pure r
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 4ce8761636..5942766b96 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -431,7 +431,6 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
   let type ← addCtorFields fieldInfos fieldInfos.size type
   let type ← mkForallFVars params type
   let type ← instantiateMVars type
-  trace[Meta.debug]! "ctor type: {type}"
   let type := type.inferImplicit params.size !view.ctor.inferMod
   pure { name := view.ctor.declName, type := type }
 
@@ -488,7 +487,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
         else
           checkResultingUniverse (← getResultUniverse type)
           pure type
-      trace[Elab.structure]! "type: {type}"
+      trace[Elab.structure] "type: {type}"
       let usedLevelNames ← collectLevelParamsInStructure type scopeVars view.params fieldInfos
       match sortDeclLevelParams view.scopeLevelNames view.allUserLevelNames usedLevelNames with
       | Except.error msg      => withRef view.ref <| throwError msg
@@ -497,7 +496,6 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
         let ctor ← mkCtor view levelParams params fieldInfos
         let type ← mkForallFVars params type
         let type ← instantiateMVars type
-        trace[Meta.debug]! "type: {type}"
         let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType }
         let decl    := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe
         Term.ensureNoUnassignedMVars decl
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 024abbbdf2..32290c1f8e 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -101,14 +101,14 @@ private def tryToSynthesizeUsingDefaultInstance (mvarId : MVarId) (defaultInstan
     let candidate := Lean.mkConst defaultInstance (← mkFreshLevelMVars constInfo.levelParams.length)
     let (mvars, bis, _) ← forallMetaTelescopeReducing (← inferType candidate)
     let candidate := mkAppN candidate mvars
-    trace[Elab.resume]! "trying default instance for {mkMVar mvarId} := {candidate}"
+    trace[Elab.resume] "trying default instance for {mkMVar mvarId} := {candidate}"
     if (← isDefEqGuarded (mkMVar mvarId) candidate) then
       -- Succeeded. Collect new TC problems
       let mut result := []
       for i in [:bis.size] do
         if bis[i] == BinderInfo.instImplicit then
            result := { mvarId := mvars[i].mvarId!, stx := (← getRef), kind := SyntheticMVarKind.typeClass } :: result
-      trace[Elab.resume]! "worked"
+      trace[Elab.resume] "worked"
       return some result
     else
       return none
@@ -239,7 +239,7 @@ mutual
        -- 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 m!"resuming {mkMVar mvarDecl.mvarId}")
        let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics
-       trace[Elab.postpone]! if succeeded then fmt "succeeded" else fmt "not ready yet"
+       trace[Elab.postpone] if succeeded then fmt "succeeded" else fmt "not ready yet"
        pure !succeeded
     -- Merge new synthetic metavariables with `remainingSyntheticMVars`, i.e., metavariables that still couldn't be synthesized
     modify fun s => { s with syntheticMVars := s.syntheticMVars ++ remainingSyntheticMVars }
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index acb5729a18..dfb241e453 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -876,7 +876,7 @@ def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermEla
   pure expectedType
 
 private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
-  trace[Elab.postpone]! "{stx} : {expectedType?}"
+  trace[Elab.postpone] "{stx} : {expectedType?}"
   let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque
   let ctx ← read
   registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack ctx.declName?)
@@ -980,7 +980,7 @@ private def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expec
   let body ← elabUsingElabFns stx expectedType catchExPostpone
   let body ← ensureHasType expectedType body
   let r ← mkLambdaFVars fvars body
-  trace[Elab.implicitForall]! r
+  trace[Elab.implicitForall] r
   pure r
 
 private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) : Expr → Array Expr → TermElabM Expr
@@ -998,7 +998,7 @@ private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) :
 /- Main loop for `elabTerm` -/
 private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : Bool) (implicitLambda : Bool) : Syntax → TermElabM Expr
   | stx => withFreshMacroScope <| withIncRecDepth do
-    trace[Elab.step]! "expected type: {expectedType?}, term\n{stx}"
+    trace[Elab.step] "expected type: {expectedType?}, term\n{stx}"
     checkMaxHeartbeats "elaborator"
     withNestedTraces do
     let env ← getEnv
@@ -1157,9 +1157,9 @@ builtin_initialize registerTraceClass `Elab.letrec
 /- Return true if mvarId is an auxiliary metavariable created for compiling `let rec` or it
    is delayed assigned to one. -/
 def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
-  trace[Elab.letrec]! "mvarId: {mkMVar mvarId} letrecMVars: {(← get).letRecsToLift.map (mkMVar $ ·.mvarId)}"
+  trace[Elab.letrec] "mvarId: {mkMVar mvarId} letrecMVars: {(← get).letRecsToLift.map (mkMVar $ ·.mvarId)}"
   let mvarId := (← getMCtx).getDelayedRoot mvarId
-  trace[Elab.letrec]! "mvarId root: {mkMVar mvarId}"
+  trace[Elab.letrec] "mvarId root: {mkMVar mvarId}"
   return (← get).letRecsToLift.any (·.mvarId == mvarId)
 
 /- =======================================
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 8547b95c35..6122d6965c 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -51,14 +51,14 @@ def mkHEqRefl (a : Expr) : MetaM Expr := do
   return mkApp2 (mkConst ``HEq.refl [u]) aType a
 
 def mkAbsurd (e : Expr) (hp hnp : Expr) : MetaM Expr := do
-  let p ← inferType hp 
-  let u ← getLevel e 
-  return mkApp4 (mkConst ``absurd [u]) p e hp hnp 
+  let p ← inferType hp
+  let u ← getLevel e
+  return mkApp4 (mkConst ``absurd [u]) p e hp hnp
 
 def mkFalseElim (e : Expr) (h : Expr) : MetaM Expr := do
   let u ← getLevel e
   return mkApp2 (mkConst ``False.elim [u]) e h
-  
+
 private def infer (h : Expr) : MetaM Expr := do
   let hType ← inferType h
   whnfD hType
@@ -243,7 +243,7 @@ def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := do
   traceCtx `Meta.appBuilder <| withNewMCtxDepth do
     let (f, fType) ← mkFun constName
     let r ← mkAppMArgs f fType xs
-    trace[Meta.appBuilder]! "constName: {constName}, xs: {xs}, result: {r}"
+    trace[Meta.appBuilder] "constName: {constName}, xs: {xs}, result: {r}"
     return r
 
 private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat → Array Expr → Nat → Array MVarId → Expr → MetaM Expr
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index af14a06179..30fd32ee19 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -186,7 +186,7 @@ def isTypeCorrect (e : Expr) : MetaM Bool := do
     check e
     pure true
   catch ex =>
-    trace[Meta.typeError]! ex.toMessageData
+    trace[Meta.typeError] ex.toMessageData
     pure false
 
 builtin_initialize
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 1c1c36d510..cbc8622f8f 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -347,7 +347,7 @@ end Closure
   returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
   and `t_j`s are free and meta variables `type` and `value` depend on. -/
 def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) (compile : Bool := true) : MetaM Expr := do
-  trace[Meta.debug]! "{name} : {type} := {value}"
+  trace[Meta.debug] "{name} : {type} := {value}"
   let result ← Closure.mkValueTypeClosure type value zeta
   let env ← getEnv
   let decl := Declaration.defnDecl {
@@ -358,7 +358,7 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f
     hints       := ReducibilityHints.regular (getMaxHeight env result.value + 1),
     safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
   }
-  trace[Meta.debug]! "{name} : {result.type} := {result.value}"
+  trace[Meta.debug] "{name} : {result.type} := {result.value}"
   addDecl decl
   if compile then
     compileDecl decl
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index eb1f6a9cff..c3f1fa0322 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -229,18 +229,18 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
   traceCtx `Meta.isDefEq.assign.checkTypes do
     if !mvar.isMVar then
-      trace[Meta.isDefEq.assign.final]! "metavariable expected at {mvar} := {v}"
+      trace[Meta.isDefEq.assign.final] "metavariable expected at {mvar} := {v}"
       return false
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
       let vType ← inferType v
       if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then
-        trace[Meta.isDefEq.assign.final]! "{mvar} := {v}"
+        trace[Meta.isDefEq.assign.final] "{mvar} := {v}"
         assignExprMVar mvar.mvarId! v
         pure true
       else
-        trace[Meta.isDefEq.assign.typeMismatch]! "{mvar} : {mvarType} := {v} : {vType}"
+        trace[Meta.isDefEq.assign.typeMismatch] "{mvar} : {mvarType} := {v} : {vType}"
         pure false
 
 /--
@@ -278,7 +278,7 @@ private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : Meta
     mkLambdaFVars xs v
   else
     let ys ← addLetDeps
-    trace[Meta.debug]! "ys: {ys}, v: {v}"
+    trace[Meta.debug] "ys: {ys}, v: {v}"
     mkLambdaFVars ys v
 
 where
@@ -834,7 +834,7 @@ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr)
     if !cfg.foApprox then
       pure false
     else
-      trace[Meta.isDefEq.foApprox]! "{mvar} {args} := {v}"
+      trace[Meta.isDefEq.foApprox] "{mvar} {args} := {v}"
       let v := v.headBeta
       if (← commitWhen <| processAssignmentFOApproxAux mvar args v) then
         pure true
@@ -872,7 +872,7 @@ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool :=
       match (← checkAssignment mvar.mvarId! #[] v) with
       | none   => pure false
       | some v =>
-        trace[Meta.isDefEq.constApprox]! "{mvar} := {v}"
+        trace[Meta.isDefEq.constApprox] "{mvar} := {v}"
         checkTypesAndAssign mvar v
 
 private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
@@ -888,7 +888,7 @@ private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM
     It assumes `?m` is unassigned. -/
 private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :=
   traceCtx `Meta.isDefEq.assign do
-    trace[Meta.isDefEq.assign]! "{mvarApp} := {v}"
+    trace[Meta.isDefEq.assign] "{mvarApp} := {v}"
     let mvar := mvarApp.getAppFn
     let mvarDecl ← getMVarDecl mvar.mvarId!
     let rec process (i : Nat) (args : Array Expr) (v : Expr) := do
@@ -919,7 +919,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
           match (← checkAssignment mvarId args v) with
           | none   => useFOApprox args
           | some v => do
-            trace[Meta.isDefEq.assign.beforeMkLambda]! "{mvar} {args} := {v}"
+            trace[Meta.isDefEq.assign.beforeMkLambda] "{mvar} {args} := {v}"
             let some v ← mkLambdaFVarsWithLetDeps args v | return false
             if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then
               /- We need to type check `v` because abstraction using `mkLambdaFVars` may have produced
@@ -927,7 +927,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
               if (← isTypeCorrect v) then
                 checkTypesAndAssign mvar v
               else
-                trace[Meta.isDefEq.assign.typeError]! "{mvar} := {v}"
+                trace[Meta.isDefEq.assign.typeError] "{mvar} := {v}"
                 useFOApprox args
             else
               checkTypesAndAssign mvar v
@@ -968,17 +968,17 @@ private def isListLevelDefEq (us vs : List Level) : MetaM LBool :=
 
 /-- Auxiliary method for isDefEqDelta -/
 private def isDefEqLeft (fn : Name) (t s : Expr) : MetaM LBool := do
-  trace[Meta.isDefEq.delta.unfoldLeft]! fn
+  trace[Meta.isDefEq.delta.unfoldLeft] fn
   toLBoolM <| Meta.isExprDefEqAux t s
 
 /-- Auxiliary method for isDefEqDelta -/
 private def isDefEqRight (fn : Name) (t s : Expr) : MetaM LBool := do
-  trace[Meta.isDefEq.delta.unfoldRight]! fn
+  trace[Meta.isDefEq.delta.unfoldRight] fn
   toLBoolM <| Meta.isExprDefEqAux t s
 
 /-- Auxiliary method for isDefEqDelta -/
 private def isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := do
-  trace[Meta.isDefEq.delta.unfoldLeftRight]! fn
+  trace[Meta.isDefEq.delta.unfoldLeftRight] fn
   toLBoolM <| Meta.isExprDefEqAux t s
 
 /-- Try to solve `f a₁ ... aₙ =?= f b₁ ... bₙ` by solving `a₁ =?= b₁, ..., aₙ =?= bₙ`.
@@ -1012,7 +1012,7 @@ private def tryHeuristic (t s : Expr) : MetaM Bool :=
               <&&>
               isListLevelDefEqAux tFn.constLevels! sFn.constLevels!
       unless b do
-        trace[Meta.isDefEq.delta]! "heuristic failed {t} =?= {s}"
+        trace[Meta.isDefEq.delta] "heuristic failed {t} =?= {s}"
       pure b
 
 /-- Auxiliary method for isDefEqDelta -/
@@ -1288,7 +1288,7 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
       let tAssign? ← isAssignable tFn
       let sAssign? ← isAssignable sFn
       let assignableMsg (b : Bool) := if b then "[assignable]" else "[nonassignable]"
-      trace[Meta.isDefEq]! "{t} {assignableMsg tAssign?} =?= {s} {assignableMsg sAssign?}"
+      trace[Meta.isDefEq] "{t} {assignableMsg tAssign?} =?= {s} {assignableMsg sAssign?}"
       if tAssign? && !sAssign? then
         toLBoolM <| processAssignment' t s
       else if !tAssign? && sAssign? then
@@ -1297,7 +1297,7 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
         if tFn.isMVar || sFn.isMVar then
           let ctx ← read
           if ctx.config.isDefEqStuckEx then do
-            trace[Meta.isDefEq.stuck]! "{t} =?= {s}"
+            trace[Meta.isDefEq.stuck] "{t} =?= {s}"
             Meta.throwIsDefEqStuck
           else
             pure LBool.false
@@ -1337,7 +1337,7 @@ end
 @[specialize] private def unstuckMVar (e : Expr) (successK : Expr → MetaM Bool) (failK : MetaM Bool): MetaM Bool := do
   match (← getStuckMVar? e) with
   | some mvarId =>
-    trace[Meta.isDefEq.stuckMVar]! "found stuck MVar {mkMVar mvarId} : {← inferType (mkMVar mvarId)}"
+    trace[Meta.isDefEq.stuckMVar] "found stuck MVar {mkMVar mvarId} : {← inferType (mkMVar mvarId)}"
     if (← Meta.synthPending mvarId) then
       let e ← instantiateMVars e
       successK e
@@ -1373,7 +1373,7 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do
     isDefEqOnFailure t s
 
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := do
-  trace[Meta.isDefEq.step]! "{t} =?= {s}"
+  trace[Meta.isDefEq.step] "{t} =?= {s}"
   checkMaxHeartbeats "isDefEq"
   withNestedTraces do
   whenUndefDo (isDefEqQuick t s) do
diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index 44d176e4c4..32e3f1d7e2 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -119,7 +119,7 @@ mutual
       if lhs.getLevelOffset == rhs.getLevelOffset then
         return lhs.getOffset == rhs.getOffset
       else
-        trace[Meta.isLevelDefEq.step]! "{lhs} =?= {rhs}"
+        trace[Meta.isLevelDefEq.step] "{lhs} =?= {rhs}"
         let lhs' ← instantiateLevelMVars lhs
         let lhs' := lhs'.normalize
         let rhs' ← instantiateLevelMVars rhs
@@ -139,7 +139,7 @@ mutual
               if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then
                 let ctx ← read
                 if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
-                  trace[Meta.isLevelDefEq.stuck]! "{lhs} =?= {rhs}"
+                  trace[Meta.isLevelDefEq.stuck] "{lhs} =?= {rhs}"
                   Meta.throwIsDefEqStuck
                 else
                   return false
@@ -181,7 +181,7 @@ else
       if numPostponed == 0 then
         return true
       else
-        trace[Meta.isLevelDefEq.postponed]! "processing #{numPostponed} postponed is-def-eq level constraints"
+        trace[Meta.isLevelDefEq.postponed] "processing #{numPostponed} postponed is-def-eq level constraints"
         if !(← processPostponedStep) then
           return false
         else
@@ -191,7 +191,7 @@ else
           else if numPostponed' < numPostponed then
             loop
           else
-            trace[Meta.isLevelDefEq.postponed]! "no progress solving pending is-def-eq level constraints"
+            trace[Meta.isLevelDefEq.postponed] "no progress solving pending is-def-eq level constraints"
             return mayPostpone
     loop
 
@@ -257,13 +257,13 @@ private def postponedToMessageData (ps : PersistentArray PostponedEntry) : Messa
 def isLevelDefEq (u v : Level) : MetaM Bool :=
   traceCtx `Meta.isLevelDefEq do
     let b ← commitWhen (mayPostpone := true) <| Meta.isLevelDefEqAux u v
-    trace[Meta.isLevelDefEq]! "{u} =?= {v} ... {if b then "success" else "failure"}"
+    trace[Meta.isLevelDefEq] "{u} =?= {v} ... {if b then "success" else "failure"}"
     return b
 
 def isExprDefEq (t s : Expr) : MetaM Bool :=
   traceCtx `Meta.isDefEq do
     let b ← commitWhen (mayPostpone := true) <| Meta.isExprDefEqAux t s
-    trace[Meta.isDefEq]! "{t} =?= {s} ... {if b then "success" else "failure"}"
+    trace[Meta.isDefEq] "{t} =?= {s} ... {if b then "success" else "failure"}"
     return b
 
 abbrev isDefEq (t s : Expr) : MetaM Bool :=
diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean
index d2e05fe82a..b50ca198de 100644
--- a/src/Lean/Meta/Match/CaseValues.lean
+++ b/src/Lean/Meta/Match/CaseValues.lean
@@ -45,11 +45,11 @@ def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Nam
     let clearH := false
     let (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH
     withMVarContext thenMVarId do
-      trace[Meta]! "subst domain: {thenSubst.domain}"
+      trace[Meta] "subst domain: {thenSubst.domain}"
       let thenH := (thenSubst.get thenH).fvarId!
-      trace[Meta]! "searching for decl"
+      trace[Meta] "searching for decl"
       let decl ← getLocalDecl thenH
-      trace[Meta]! "found decl"
+      trace[Meta] "found decl"
     let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal }
     pure (thenSubgoal, elseSubgoal)
 
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 4cefdbc983..fe2e29e1a4 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -41,7 +41,7 @@ where
       let (minorType, minorNumParams) := if !xs.isEmpty then (minorType, xs.size) else (mkSimpleThunkType minorType, 1)
       let idx       := alts.length
       let minorName := (`h).appendIndexAfter (idx+1)
-      trace[Meta.Match.debug]! "minor premise {minorName} : {minorType}"
+      trace[Meta.Match.debug] "minor premise {minorName} : {minorType}"
       withLocalDeclD minorName minorType fun minor => do
         let rhs    := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs
         let minors := minors.push (minor, minorNumParams)
@@ -202,20 +202,20 @@ def occurs (fvarId : FVarId) (v : Expr) : Bool :=
 
 def assign (fvarId : FVarId) (v : Expr) : M Bool := do
   if occurs fvarId v then
-    trace[Meta.Match.unify]! "assign occurs check failed, {mkFVar fvarId} := {v}"
+    trace[Meta.Match.unify] "assign occurs check failed, {mkFVar fvarId} := {v}"
     pure false
   else
     let ctx ← read
     if (← isAltVar fvarId) then
-      trace[Meta.Match.unify]! "{mkFVar fvarId} := {v}"
+      trace[Meta.Match.unify] "{mkFVar fvarId} := {v}"
       modify fun s => { s with fvarSubst := s.fvarSubst.insert fvarId v }
       pure true
     else
-      trace[Meta.Match.unify]! "assign failed variable is not local, {mkFVar fvarId} := {v}"
+      trace[Meta.Match.unify] "assign failed variable is not local, {mkFVar fvarId} := {v}"
       pure false
 
 partial def unify (a : Expr) (b : Expr) : M Bool := do
-  trace[Meta.Match.unify]! "{a} =?= {b}"
+  trace[Meta.Match.unify] "{a} =?= {b}"
   if (← isDefEq a b) then
     pure true
   else
@@ -292,7 +292,7 @@ def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt)
   let env ← getEnv
   match alt.patterns with
   | p@(Pattern.inaccessible e) :: ps =>
-    trace[Meta.Match.match]! "inaccessible in ctor step {e}"
+    trace[Meta.Match.match] "inaccessible in ctor step {e}"
     withExistingLocalDecls alt.fvarDecls do
       -- Try to push inaccessible annotations.
       let e ← whnfD e
@@ -308,7 +308,7 @@ def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt)
   | _ => unreachable!
 
 private def processConstructor (p : Problem) : MetaM (Array Problem) := do
-  trace[Meta.Match.match]! "constructor step"
+  trace[Meta.Match.match] "constructor step"
   let env ← getEnv
   match p.vars with
   | []      => unreachable!
@@ -395,7 +395,7 @@ private def isFirstPatternVar (alt : Alt) : Bool :=
   | _                  => false
 
 private def processValue (p : Problem) : MetaM (Array Problem) := do
-  trace[Meta.Match.match]! "value step"
+  trace[Meta.Match.match] "value step"
   match p.vars with
   | []      => unreachable!
   | x :: xs => do
@@ -449,7 +449,7 @@ private def expandVarIntoArrayLit (alt : Alt) (fvarId : FVarId) (arrayElemType :
     loop arraySize #[]
 
 private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
-  trace[Meta.Match.match]! "array literal step"
+  trace[Meta.Match.match] "array literal step"
   match p.vars with
   | []      => unreachable!
   | x :: xs => do
@@ -490,7 +490,7 @@ private def expandNatValuePattern (p : Problem) : Problem := do
   { p with alts := alts }
 
 private def traceStep (msg : String) : StateRefT State MetaM Unit :=
-  trace[Meta.Match.match]! "{msg} step"
+  trace[Meta.Match.match] "{msg} step"
 
 private def traceState (p : Problem) : MetaM Unit :=
   withGoalOf p (traceM `Meta.Match.match p.toMessageData)
@@ -579,7 +579,7 @@ builtin_initialize matcherExt : EnvExtension (Std.PHashMap (Expr × Bool) Name)
 /- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`.
    It also returns an Boolean that indicates whether a new matcher function was added to the environment or not. -/
 def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Bool × Expr) := do
-  trace[Meta.debug]! "{name} : {type} := {value}"
+  trace[Meta.debug] "{name} : {type} := {value}"
   let compile := bootstrap.genMatcherCode.get (← getOptions)
   let result ← Closure.mkValueTypeClosure type value (zeta := false)
   let env ← getEnv
@@ -594,7 +594,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (B
       hints       := ReducibilityHints.regular (getMaxHeight env result.value + 1),
       safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
     }
-    trace[Meta.debug]! "{name} : {result.type} := {result.value}"
+    trace[Meta.debug] "{name} : {result.type} := {result.value}"
     addDecl decl
     if compile then
       compileDecl decl
@@ -621,9 +621,9 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
   let motiveType ← mkForallFVars majors (mkSort uElimGen)
   withLocalDeclD `motive motiveType fun motive => do
-  trace[Meta.Match.debug]! "motiveType: {motiveType}"
+  trace[Meta.Match.debug] "motiveType: {motiveType}"
   let mvarType  := mkAppN motive majors
-  trace[Meta.Match.debug]! "target: {mvarType}"
+  trace[Meta.Match.debug] "target: {mvarType}"
   withAlts motive lhss fun alts minors => do
     let mvar ← mkFreshExprMVar mvarType
     let examples := majors.toList.map fun major => Example.var major.fvarId!
@@ -631,7 +631,7 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
     let args := #[motive] ++ majors ++ minors.map Prod.fst
     let type ← mkForallFVars args mvarType
     let val  ← mkLambdaFVars args mvar
-    trace[Meta.Match.debug]! "matcher value: {val}\ntype: {type}"
+    trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
        for compiling `src/Init/Data/Int`. It is needed because the compiler uses `Int.decLt`
        for generating code for `Int.casesOn` applications, but `Int.casesOn` is used to
@@ -644,13 +644,13 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
        ```
        which is defined **before** `Int.decLt` -/
     let (isNewMatcher, matcher) ← mkMatcherAuxDefinition matcherName type val
-    trace[Meta.Match.debug]! "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
+    trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen
     discard <| isLevelDefEq uElimGen uElim
     if isNewMatcher then
       addMatcherInfo matcherName { numParams := matcher.getAppNumArgs, numDiscrs := numDiscrs, altNumParams := minors.map Prod.snd, uElimPos? := uElimPos? }
       setInlineAttribute matcherName
-    trace[Meta.Match.debug]! "matcher: {matcher}"
+    trace[Meta.Match.debug] "matcher: {matcher}"
     let unusedAltIdxs := lhss.length.fold (init := []) fun i r =>
       if s.used.contains i then r else i::r
     pure { matcher := matcher, counterExamples := s.counterExamples, unusedAltIdxs := unusedAltIdxs.reverse }
@@ -709,7 +709,6 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
     let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params
     let aux := mkApp aux motive
     let aux := mkAppN aux matcherApp.discrs
-    trace! `Meta.debug aux
     check aux
     unless (← isTypeCorrect aux) do
       throwError "failed to add argument to matcher application, type error when constructing the new motive"
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index 3baab742c2..c177f8317f 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -68,7 +68,7 @@ where
       let type ← inferType motiveFVars[i]
       let motive ← forallTelescopeReducing type fun xs _ => do
         mkLambdaFVars xs <| mkConst ``Nat
-      trace[Meta.sizeOf]! "motive: {motive}"
+      trace[Meta.sizeOf] "motive: {motive}"
       loop (i+1) (motives.push motive)
     else
       k motives
@@ -89,7 +89,7 @@ where
             | some idx => minor ← mkAdd minor xs'[idx]
             | none     => minor ← mkAdd minor (← mkAppM ``SizeOf.sizeOf #[x'])
         minor ← mkLambdaFVars xs' minor
-        trace[Meta.sizeOf]! "minor: {minor}"
+        trace[Meta.sizeOf] "minor: {minor}"
         loop (i+1) (minors.push minor)
     else
       k minors
@@ -98,7 +98,7 @@ where
   Create a "sizeOf" function with name `declName` using the recursor `recName`.
 -/
 partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
-  trace[Meta.sizeOf]! "recName: {recName}"
+  trace[Meta.sizeOf] "recName: {recName}"
   let recInfo : RecursorVal ← getConstInfoRec recName
   forallTelescopeReducing recInfo.type fun xs type =>
     let levelParams := recInfo.levelParams.tail! -- universe parameters for declaration being defined
@@ -118,7 +118,7 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
         let sizeOfParams := params ++ localInsts ++ indices ++ #[major]
         let sizeOfType ← mkForallFVars sizeOfParams nat
         let val := mkAppN val (minors ++ indices ++ #[major])
-        trace[Meta.sizeOf]! "val: {val}"
+        trace[Meta.sizeOf] "val: {val}"
         let sizeOfValue ← mkLambdaFVars sizeOfParams val
         addDecl <| Declaration.defnDecl {
           name        := declName
@@ -205,7 +205,7 @@ private def recToSizeOf (e : Expr) : M Expr := do
 mutual
   /-- Construct minor premise proof for `mkSizeOfAuxLemmaProof`. `ys` contains fields and inductive hypotheses for the minor premise. -/
   private partial def mkMinorProof (ys : Array Expr) (lhs rhs : Expr) : M Expr := do
-    trace[Meta.sizeOf.minor]! "{lhs} =?= {rhs}"
+    trace[Meta.sizeOf.minor] "{lhs} =?= {rhs}"
     if (← isDefEq lhs rhs) then
       mkEqRefl rhs
     else
@@ -228,7 +228,7 @@ mutual
       mkEqRefl rhs
     else
       let lhs ← recToSizeOf lhs
-      trace[Meta.sizeOf.minor.step]! "{lhs} =?= {rhs}"
+      trace[Meta.sizeOf.minor.step] "{lhs} =?= {rhs}"
       let target ← mkEq lhs rhs
       for y in ys do
         if (← isDefEq (← inferType y) target) then
@@ -317,7 +317,7 @@ mutual
     `Expr._sizeOf_1 args` is **not** definitionally equal to `sizeOf args`. We need a proof by induction.
   -/
   private partial def mkSizeOfAuxLemma (lhs rhs : Expr) : M Expr := do
-    trace[Meta.sizeOf.aux]! "{lhs} =?= {rhs}"
+    trace[Meta.sizeOf.aux] "{lhs} =?= {rhs}"
     match lhs.getAppFn.const? with
     | none => throwFailed
     | some (fName, us) =>
@@ -347,7 +347,7 @@ mutual
               let thmType ← mkForallFVars thmParams eq
               let thmValue ← mkSizeOfAuxLemmaProof info lhsNew rhsNew
               let thmValue ← mkLambdaFVars thmParams thmValue
-              trace[Meta.sizeOf]! "thmValue: {thmValue}"
+              trace[Meta.sizeOf] "thmValue: {thmValue}"
               addDecl <| Declaration.thmDecl {
                 name        := thmName
                 levelParams := thmLevelParams
@@ -369,7 +369,7 @@ partial def main (lhs rhs : Expr) : M Expr := do
     loop lhs rhs
 where
   loop (lhs rhs : Expr) : M Expr := do
-    trace[Meta.sizeOf.loop]! "{lhs} =?= {rhs}"
+    trace[Meta.sizeOf.loop] "{lhs} =?= {rhs}"
     if (← isDefEq lhs rhs) then
       mkEqRefl rhs
     else
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 22fa9f38cd..b3b0f91da7 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -199,7 +199,7 @@ def getInstances (type : Expr) : MetaM (Array Expr) := do
       let result ← result.mapM fun e => match e.val with
         | Expr.const constName us _ => return e.val.updateConst! (← us.mapM (fun _ => mkFreshLevelMVar))
         | _ => panic! "global instance is not a constant"
-      trace[Meta.synthInstance.globalInstances]! "{type}, {result}"
+      trace[Meta.synthInstance.globalInstances] "{type}, {result}"
       let result := localInstances.foldl (init := result) fun (result : Array Expr) linst =>
         if linst.className == className then result.push linst.fvar else result
       pure result
@@ -224,7 +224,7 @@ def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do
     `key` must be `mkTableKey mctx mvarType`. -/
 def newSubgoal (mctx : MetavarContext) (key : Expr) (mvar : Expr) (waiter : Waiter) : SynthM Unit :=
   withMCtx mctx do
-    trace[Meta.synthInstance.newSubgoal]! key
+    trace[Meta.synthInstance.newSubgoal] key
     match (← mkGeneratorNode? key mvar) with
     | none      => pure ()
     | some node =>
@@ -316,17 +316,17 @@ def tryResolveCore (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext 
   let localInsts ← getLocalInstances
   forallTelescopeReducing mvarType fun xs mvarTypeBody => do
     let ⟨subgoals, instVal, instTypeBody⟩ ← getSubgoals lctx localInsts xs inst
-    trace[Meta.synthInstance.tryResolve]! "{mvarTypeBody} =?= {instTypeBody}"
+    trace[Meta.synthInstance.tryResolve] "{mvarTypeBody} =?= {instTypeBody}"
     if (← isDefEq mvarTypeBody instTypeBody) then
       let instVal ← mkLambdaFVars xs instVal
       if (← isDefEq mvar instVal) then
-        trace[Meta.synthInstance.tryResolve]! "success"
+        trace[Meta.synthInstance.tryResolve] "success"
         pure (some ((← getMCtx), subgoals))
       else
-        trace[Meta.synthInstance.tryResolve]! "failure assigning"
+        trace[Meta.synthInstance.tryResolve] "failure assigning"
         pure none
     else
-      trace[Meta.synthInstance.tryResolve]! "failure"
+      trace[Meta.synthInstance.tryResolve] "failure"
       pure none
 
 /--
@@ -355,7 +355,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
       modify fun s => { s with result := answer.result.expr }
     else
       let (_, _, answerExpr) ← openAbstractMVarsResult answer.result
-      trace[Meta.synthInstance]! "skip answer containing metavariables {answerExpr}"
+      trace[Meta.synthInstance] "skip answer containing metavariables {answerExpr}"
       pure ()
   | Waiter.consumerNode cNode =>
     modify fun s => { s with resumeStack := s.resumeStack.push (cNode, answer) }
@@ -370,7 +370,7 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
   withMCtx cNode.mctx do
     traceM `Meta.synthInstance.newAnswer do m!"size: {cNode.size}, {← inferType cNode.mvar}"
     let val ← instantiateMVars cNode.mvar
-    trace[Meta.synthInstance.newAnswer]! "val: {val}"
+    trace[Meta.synthInstance.newAnswer] "val: {val}"
     let result ← abstractMVars val -- assignable metavariables become parameters
     let resultType ← inferType result.expr
     pure { result := result, resultType := resultType, size := cNode.size + 1 }
@@ -425,7 +425,7 @@ def generate : SynthM Unit := do
     let inst := gNode.instances.get! idx
     let mctx := gNode.mctx
     let mvar := gNode.mvar
-    trace[Meta.synthInstance.generate]! "instance {inst}"
+    trace[Meta.synthInstance.generate] "instance {inst}"
     modifyTop fun gNode => { gNode with currInstanceIdx := idx }
     match (← tryResolve mctx mvar inst) with
     | none                  => pure ()
@@ -475,12 +475,12 @@ partial def synth : SynthM (Option Expr) := do
     | none        => synth
     | some result => pure result
   else
-    trace[Meta.synthInstance]! "failed"
+    trace[Meta.synthInstance] "failed"
     pure none
 
 def main (type : Expr) (maxResultSize : Nat) : MetaM (Option Expr) :=
   withCurrHeartbeats <| traceCtx `Meta.synthInstance do
-     trace[Meta.synthInstance]! "main goal {type}"
+     trace[Meta.synthInstance] "main goal {type}"
      let mvar ← mkFreshExprMVar type
      let mctx ← getMCtx
      let key    := mkTableKey mctx type
@@ -577,27 +577,27 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     | none        =>
       let result? ← withNewMCtxDepth do
         let normType ← preprocessOutParam type
-        trace[Meta.synthInstance]! "{type} ==> {normType}"
+        trace[Meta.synthInstance] "{type} ==> {normType}"
         match (← SynthInstance.main normType maxResultSize) with
         | none        => pure none
         | some result =>
-          trace[Meta.synthInstance]! "FOUND result {result}"
+          trace[Meta.synthInstance] "FOUND result {result}"
           let result ← instantiateMVars result
           if (← hasAssignableMVar result) then
-            trace[Meta.synthInstance]! "Failed has assignable mvar {result.setOption `pp.all true}"
+            trace[Meta.synthInstance] "Failed has assignable mvar {result.setOption `pp.all true}"
             pure none
           else
             pure (some result)
       let result? ← match result? with
         | none        => pure none
         | some result => do
-          trace[Meta.synthInstance]! "result {result}"
+          trace[Meta.synthInstance] "result {result}"
           let resultType ← inferType result
           if (← withConfig (fun _ => inputConfig) <| isDefEq type resultType) then
             let result ← instantiateMVars result
             pure (some result)
           else
-            trace[Meta.synthInstance]! "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
+            trace[Meta.synthInstance] "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
             pure none
       if type.hasMVar then
         pure result?
diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean
index acdb7eed15..2a3f2dc577 100644
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/src/Lean/Meta/Tactic/Cases.lean
@@ -296,7 +296,7 @@ def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNam
         inductionCasesOn mvarId majorFVarId givenNames ctx
       else
         let s₁ ← generalizeIndices mvarId majorFVarId
-        trace[Meta.Tactic.cases]! "after generalizeIndices\n{MessageData.ofGoal s₁.mvarId}"
+        trace[Meta.Tactic.cases] "after generalizeIndices\n{MessageData.ofGoal s₁.mvarId}"
         let s₂ ← inductionCasesOn s₁.mvarId s₁.fvarId givenNames ctx
         let s₂ ← elimAuxIndices s₁ s₂
         unifyCasesEqs s₁.numEqs s₂
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index e3acf657fc..d1b6f7ccc0 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -124,7 +124,7 @@ private def throwUnexpectedMajorType {α} (mvarId : MVarId) (majorType : Expr) :
 
 def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) :=
   withMVarContext mvarId do
-    trace[Meta.Tactic.induction]! "initial\n{MessageData.ofGoal mvarId}"
+    trace[Meta.Tactic.induction] "initial\n{MessageData.ofGoal mvarId}"
     checkNotAssigned mvarId `induction
     let majorLocalDecl ← getLocalDecl majorFVarId
     let recursorInfo ← mkRecursorInfo recursorName
@@ -168,7 +168,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
           subst := subst.insert index.fvarId! (mkFVar indices'[i])
           i     := i + 1
         pure subst
-      trace[Meta.Tactic.induction]! "after revert&intro\n{MessageData.ofGoal mvarId}"
+      trace[Meta.Tactic.induction] "after revert&intro\n{MessageData.ofGoal mvarId}"
       -- Update indices and major
       let indices := indices'.map mkFVar
       let majorFVarId := majorFVarId'
diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean
index 89f4fbdcb5..400cfde0c5 100644
--- a/src/Lean/Meta/Tactic/Injection.lean
+++ b/src/Lean/Meta/Tactic/Injection.lean
@@ -93,7 +93,6 @@ def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) (
   match (← injectionCore mvarId fvarId) with
   | InjectionResultCore.solved                => pure InjectionResult.solved
   | InjectionResultCore.subgoal mvarId numEqs =>
-    trace[Meta.debug]! "before injectionIntro\n{MessageData.ofGoal mvarId}"
     injectionIntro numEqs mvarId #[] newNames
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean b/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean
index f31adb7630..16dc5d26d7 100644
--- a/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean
+++ b/src/Lean/Meta/Tactic/Simp/CongrLemmas.lean
@@ -90,7 +90,7 @@ def mkCongrLemma (declName : Name) (prio : Nat) : MetaM CongrLemma := withReduci
             foundMVars    := foundMVars.insert x.mvarId! |>.insert rhsFn.mvarId!
             hypothesesPos := hypothesesPos.push i
         i := i + 1
-      trace[Meta.debug]! "c: {c} : {type}"
+      trace[Meta.debug] "c: {c} : {type}"
       return {
         theoremName   := declName
         funName       := lhsFn.constName!
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 629c94861f..077569dcf5 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -57,7 +57,6 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
     match (← getProjectionFnInfo? cinfo.name) with
     | none => return none
     | some projInfo =>
-      trace[Meta.debug]! "reduceProjFn? {projInfo.fromClass}, {cinfo.name}, {e}"
       if projInfo.fromClass then
         if (← read).toUnfold.contains cinfo.name then
           -- We only unfold class projections when the user explicitly requested them to be unfolded.
@@ -103,7 +102,7 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   -- TODO: eta reduction
   if cfg.proj then
     match (← reduceProjFn? e) with
-    | some e => trace[Meta.debug]! "reduceProjFn? result {e}"; return (← reduce e)
+    | some e => return (← reduce e)
     | none   => pure ()
   if cfg.iota then
     match (← reduceRecMatcher? e) with
@@ -168,7 +167,7 @@ where
       let mut r ← simp f
       let mut i := 0
       for arg in args do
-        trace[Debug.Meta.Tactic.simp]! "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
+        trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
         if i < infos.size && !infos[i].hasFwdDeps then
           r ← mkCongr r (← simp arg)
         else
@@ -192,7 +191,7 @@ where
 
   /- Try to rewrite `e` children using the given congruence lemma -/
   tryCongrLemma? (c : CongrLemma) (e : Expr) : M (Option Result) := withNewMCtxDepth do
-    trace[Debug.Meta.Tactic.simp.congr]! "{c.theoremName}, {e}"
+    trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
     let info ← getConstInfo c.theoremName
     let lemma := mkConst c.theoremName (← info.levelParams.mapM fun _ => mkFreshLevelMVar)
     let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType lemma)
@@ -208,13 +207,13 @@ where
           if (← processCongrHypothesis x) then
             modified := true
         catch _ =>
-          trace[Meta.Tactic.simp.congr]! "processCongrHypothesis {c.theoremName} failed {← inferType x}"
+          trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}"
           return none
       unless modified do
-        trace[Meta.Tactic.simp.congr]! "{c.theoremName} not modified"
+        trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
         return none
       unless (← synthesizeArgs c.theoremName xs bis (← read).discharge?) do
-        trace[Meta.Tactic.simp.congr]! "{c.theoremName} synthesizeArgs failed"
+        trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
         return none
       let eNew ← instantiateMVars rhs
       let proof ← instantiateMVars (mkAppN lemma xs)
@@ -272,13 +271,13 @@ where
         return { expr := eNew, proof? := p }
 
   simpArrow (e : Expr) : M Result := do
-    trace[Debug.Meta.Tactic.simp]! "arrow {e}"
+    trace[Debug.Meta.Tactic.simp] "arrow {e}"
     let p := e.bindingDomain!
     let q := e.bindingBody!
     let rp ← simp p
-    trace[Debug.Meta.Tactic.simp]! "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
+    trace[Debug.Meta.Tactic.simp] "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
     if (← (← getConfig).contextual <&&> isProp p <&&> isProp q) then
-      trace[Debug.Meta.Tactic.simp]! "ctx arrow {rp.expr} -> {q}"
+      trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}"
       withLocalDeclD e.bindingName! rp.expr fun h => do
         let s ← getSimpLemmas
         let s ← s.add h
@@ -293,7 +292,7 @@ where
       mkImpCongr rp (← simp q)
 
   simpForall (e : Expr) : M Result := withParent e do
-    trace[Debug.Meta.Tactic.simp]! "forall {e}"
+    trace[Debug.Meta.Tactic.simp] "forall {e}"
     if e.isArrow then
       simpArrow e
     else if (← isProp e) then
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 7b7a2a999a..5be8d052db 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -15,19 +15,19 @@ def synthesizeArgs (lemmaName : Name) (xs : Array Expr) (bis : Array BinderInfo)
       match ← trySynthInstance type with
       | LOption.some val =>
         unless (← isDefEq x val) do
-          trace[Meta.Tactic.simp.discharge]! "{lemmaName}, failed to assign instance{indentExpr type}"
+          trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to assign instance{indentExpr type}"
           return false
       | _ =>
-        trace[Meta.Tactic.simp.discharge]! "{lemmaName}, failed to synthesize instance{indentExpr type}"
+        trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to synthesize instance{indentExpr type}"
         return false
     else if (← isProp type <&&> (← instantiateMVars x).isMVar) then
       match ← discharge? type with
       | some proof =>
         unless (← isDefEq x proof) do
-          trace[Meta.Tactic.simp.discharge]! "{lemmaName}, failed to assign proof{indentExpr type}"
+          trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to assign proof{indentExpr type}"
           return false
       | none =>
-        trace[Meta.Tactic.simp.discharge]! "{lemmaName}, failed to discharge hypotheses{indentExpr type}"
+        trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to discharge hypotheses{indentExpr type}"
         return false
   return true
 
@@ -37,7 +37,7 @@ Remark: the parameter tag is used for creating trace messages. It is irrelevant
 def rewrite (e : Expr) (s : DiscrTree SimpLemma) (erased : SimpLemmaNameSet) (discharge? : Expr → SimpM (Option Expr)) (tag : String) : SimpM Result := do
   let lemmas ← s.getMatch e
   if lemmas.isEmpty then
-    trace[Debug.Meta.Tactic.simp]! "no lemmas found for {tag}-rewriting {e}"
+    trace[Debug.Meta.Tactic.simp] "no lemmas found for {tag}-rewriting {e}"
     return { expr := e }
   else
     let lemmas := lemmas.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority
@@ -69,16 +69,16 @@ where
         if e == rhs then
           return none
         if lemma.perm && !Expr.lt rhs e then
-          trace[Meta.Tactic.simp.rewrite]! "{lemma}, perm rejected {e} ==> {rhs}"
+          trace[Meta.Tactic.simp.rewrite] "{lemma}, perm rejected {e} ==> {rhs}"
           return none
-        trace[Meta.Tactic.simp.rewrite]! "{lemma}, {e} ==> {rhs}"
+        trace[Meta.Tactic.simp.rewrite] "{lemma}, {e} ==> {rhs}"
         return some { expr := rhs, proof? := proof }
       else
         unless lhs.isMVar do
           -- We do not report unification failures when `lhs` is a metavariable
           -- Example: `x = ()`
           -- TODO: reconsider if we want lemmas such as `(x : Unit) → x = ()`
-          trace[Meta.Tactic.simp.unify]! "{lemma}, failed to unify {lhs} with {e}"
+          trace[Meta.Tactic.simp.unify] "{lemma}, failed to unify {lhs} with {e}"
         return none
 
 def rewriteCtorEq? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do
diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index 4c0a907afc..c58f2673d2 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -29,16 +29,16 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
       match a with
       | Expr.fvar aFVarId _ => do
         let aFVarIdOriginal := aFVarId
-        trace[Meta.Tactic.subst]! "substituting {a} (id: {aFVarId}) with {b}"
+        trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId}) with {b}"
         let mctx ← getMCtx
         if mctx.exprDependsOn b aFVarId then
           throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}"
         let aLocalDecl ← getLocalDecl aFVarId
         let (vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true
-        trace[Meta.Tactic.subst]! "after revert {MessageData.ofGoal mvarId}"
+        trace[Meta.Tactic.subst] "after revert {MessageData.ofGoal mvarId}"
         let (twoVars, mvarId) ← introNP mvarId 2
-        trace[Meta.Tactic.subst]! "after intro2 {MessageData.ofGoal mvarId}"
-        trace[Meta.Tactic.subst]! "reverted variables {vars}"
+        trace[Meta.Tactic.subst] "after intro2 {MessageData.ofGoal mvarId}"
+        trace[Meta.Tactic.subst] "reverted variables {vars}"
         let aFVarId := twoVars[0]
         let a       := mkFVar aFVarId
         let hFVarId := twoVars[1]
@@ -83,7 +83,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
                   else
                     pure mvarId
                 let (newFVars, mvarId) ← introNP mvarId (vars.size - 2)
-                trace[Meta.Tactic.subst]! "after intro rest {vars.size - 2} {MessageData.ofGoal mvarId}"
+                trace[Meta.Tactic.subst] "after intro rest {vars.size - 2} {MessageData.ofGoal mvarId}"
                 let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i (fvarSubst : FVarSubst) =>
                     let var     := vars[i+2]
                     let newFVar := newFVars[i]
diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean
index 7e5760a7bd..72a7298f0a 100644
--- a/src/Lean/Meta/UnificationHint.lean
+++ b/src/Lean/Meta/UnificationHint.lean
@@ -79,7 +79,7 @@ def addUnificationHint (declName : Name) (kind : AttributeKind) : MetaM Unit :=
         let keys ← DiscrTree.mkPath hint.pattern.lhs
         validateHint declName hint
         unificationHintExtension.add { keys := keys, val := declName } kind
-        trace[Meta.debug]! "addUnificationHint: {unificationHintExtension.getState (← getEnv)}"
+        trace[Meta.debug] "addUnificationHint: {unificationHintExtension.getState (← getEnv)}"
 
 builtin_initialize
   registerBuiltinAttribute {
@@ -91,7 +91,7 @@ builtin_initialize
   }
 
 def tryUnificationHints (t s : Expr) : MetaM Bool := do
-  trace[Meta.isDefEq.hint]! "{t} =?= {s}"
+  trace[Meta.isDefEq.hint] "{t} =?= {s}"
   unless (← read).config.unificationHints do
     return false
   if t.isMVar then
@@ -108,7 +108,7 @@ where
 
   tryCandidate candidate : MetaM Bool :=
     traceCtx `Meta.isDefEq.hint <| commitWhen do
-      trace[Meta.isDefEq.hint]! "trying hint {candidate} at {t} =?= {s}"
+      trace[Meta.isDefEq.hint] "trying hint {candidate} at {t} =?= {s}"
       let cinfo ← getConstInfo candidate
       let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
       let val := cinfo.instantiateValueLevelParams us
@@ -124,7 +124,7 @@ where
       match hint? with
       | none      => return false
       | some hint =>
-        trace[Meta.isDefEq.hint]! "{candidate} succeeded, applying constraints"
+        trace[Meta.isDefEq.hint] "{candidate} succeeded, applying constraints"
         for c in hint.constraints do
           unless (← Meta.isExprDefEqAux c.lhs c.rhs) do
             return false
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 563349641d..5dfd702157 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -337,7 +337,7 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) :=
   expand let-expressions, expand assigned meta-variables. -/
 partial def whnfCore (e : Expr) : MetaM Expr :=
   whnfEasyCases e fun e => do
-    trace[Meta.whnf]! e
+    trace[Meta.whnf] e
     match e with
     | Expr.const ..  => pure e
     | Expr.letE _ _ v b _ => whnfCore $ b.instantiate1 v
@@ -519,7 +519,7 @@ def reduceUnaryNatOp (f : Nat → Nat) (a : Expr) : MetaM (Option Expr) :=
 def reduceBinNatOp (f : Nat → Nat → Nat) (a b : Expr) : MetaM (Option Expr) :=
   withNatValue a fun a =>
   withNatValue b fun b => do
-  trace[Meta.isDefEq.whnf.reduceBinOp]! "{a} op {b}"
+  trace[Meta.isDefEq.whnf.reduceBinOp] "{a} op {b}"
   return mkNatLit <| f a b
 
 def reduceBinNatPred (f : Nat → Nat → Bool) (a b : Expr) : MetaM (Option Expr) := do
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 213169c74a..672ec7728e 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -380,7 +380,7 @@ end Delaborator
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
 def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
-  trace[PrettyPrinter.delab.input]! "{fmt e}"
+  trace[PrettyPrinter.delab.input] "{fmt e}"
   let opts ← MonadOptions.getOptions
   catchInternalId Delaborator.delabFailureId
     (Delaborator.delab.run { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls })
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 31ae88dea0..d7e06e53d0 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -187,7 +187,7 @@ def tokenWithAntiquot.formatter (p : Formatter) : Formatter := do
 @[combinatorFormatter Lean.Parser.categoryParser]
 def categoryParser.formatter (cat : Name) : Formatter := group $ indent do
   let stx ← getCur
-  trace[PrettyPrinter.format]! "formatting {indentD (fmt stx)}"
+  trace[PrettyPrinter.format] "formatting {indentD (fmt stx)}"
   if stx.getKind == `choice then
     visitArgs do
       -- format only last choice
@@ -226,7 +226,7 @@ def andthen.formatter (p1 p2 : Formatter) : Formatter := p2 *> p1
 def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do
   let stx ← getCur
   if k != stx.getKind then
-    trace[PrettyPrinter.format.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
+    trace[PrettyPrinter.format.backtrack] "unexpected node kind '{stx.getKind}', expected '{k}'"
     throwBacktrack
 
 @[combinatorFormatter Lean.Parser.node]
@@ -314,7 +314,7 @@ def symbolNoAntiquot.formatter (sym : String) : Formatter := do
     pushToken info sym
     goLeft
   else do
-    trace[PrettyPrinter.format.backtrack]! "unexpected syntax '{fmt stx}', expected symbol '{sym}'"
+    trace[PrettyPrinter.format.backtrack] "unexpected syntax '{fmt stx}', expected symbol '{sym}'"
     throwBacktrack
 
 @[combinatorFormatter Lean.Parser.nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.formatter := symbolNoAntiquot.formatter
@@ -478,7 +478,7 @@ end Formatter
 open Formatter
 
 def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
-  trace[PrettyPrinter.format.input]! "{fmt stx}"
+  trace[PrettyPrinter.format.input] "{fmt stx}"
   let options ← getOptions
   let table ← Parser.builtinTokenTable.get
   catchInternalId backtrackExceptionId
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 2e295120f1..1087978269 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -204,11 +204,11 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
   let st ← get
   -- reset precs for the recursive call
   set { stxTrav := st.stxTrav : State }
-  trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){indentD (fmt stx)}"
+  trace[PrettyPrinter.parenthesize] "parenthesizing (cont := {(st.contPrec, st.contCat)}){indentD (fmt stx)}"
   x
   let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get
     | panic! s!"maybeParenthesize: visited a syntax tree without precedences?!{line ++ fmt stx}"
-  trace[PrettyPrinter.parenthesize]! ("...precedences are {prec} >? {minPrec}" ++ if canJuxtapose then m!", {(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
@@ -226,7 +226,7 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
         stx' := stx'.setHeadInfo (SourceInfo.original lead pos "".toSubstring)
       if let SourceInfo.original _ pos trail := stx.getTailInfo then
         stx' := stx'.setTailInfo (SourceInfo.original "".toSubstring pos trail)
-      trace! `PrettyPrinter.parenthesize m!"parenthesized: {stx'.formatStx none}"
+      trace[PrettyPrinter.parenthesize] "parenthesized: {stx'.formatStx none}"
       setCur stx'
       goLeft
       -- after parenthesization, there is no more trailing parser
@@ -377,7 +377,7 @@ def andthen.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer :=
 def node.parenthesizer (k : SyntaxNodeKind) (p : Parenthesizer) : Parenthesizer := do
   let stx ← getCur
   if k != stx.getKind then
-    trace[PrettyPrinter.parenthesize.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
+    trace[PrettyPrinter.parenthesize.backtrack] "unexpected node kind '{stx.getKind}', expected '{k}'"
     -- HACK; see `orelse.parenthesizer`
     throwBacktrack
   visitArgs p
@@ -399,7 +399,7 @@ def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesiz
 def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do
   let stx ← getCur
   if k != stx.getKind then
-    trace[PrettyPrinter.parenthesize.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
+    trace[PrettyPrinter.parenthesize.backtrack] "unexpected node kind '{stx.getKind}', expected '{k}'"
     -- HACK; see `orelse.parenthesizer`
     throwBacktrack
   visitArgs do
@@ -530,7 +530,7 @@ open Parenthesizer
 
 /-- Add necessary parentheses in `stx` parsed by `parser`. -/
 def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax := do
-  trace[PrettyPrinter.parenthesize.input]! "{fmt stx}"
+  trace[PrettyPrinter.parenthesize.input] "{fmt stx}"
   catchInternalId backtrackExceptionId
     (do
       let (_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx }
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index b30e11f4b5..053c1ec84e 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -135,13 +135,10 @@ end
 def registerTraceClass (traceClassName : Name) : IO Unit :=
   registerOption (`trace ++ traceClassName) { group := "trace", defValue := false, descr := "enable/disable tracing for the given module and submodules" }
 
-macro:max "trace!" id:term:max msg:term : term =>
-  `(trace $id fun _ => ($msg : MessageData))
-
-syntax "trace[" ident "]!" (interpolatedStr(term) <|> term) : term
+syntax "trace[" ident "]" (interpolatedStr(term) <|> term) : term
 
 macro_rules
-  | `(trace[$id]! $s) =>
+  | `(trace[$id] $s) =>
     if s.getKind == interpolatedStrKind then
       `(Lean.trace $(quote id.getId) fun _ => m! $s)
     else