diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 3a070a20be..806aad8370 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -215,9 +215,7 @@ private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : Std.Persisten
   let tree := InfoTree.context {
     env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts
   } tree
-  if checkTraceOption (← getOptions) `Elab.info then
-    let fmt ← tree.format
-    trace[Elab.info] fmt
+  trace[Elab.info] ← tree.format
   return tree
 
 private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Unit
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index b0a5aa23a0..9768897ecb 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -542,7 +542,7 @@ private def expandNatValuePattern (p : Problem) : Problem := do
     | _                                                     => alt
   { p with alts := alts }
 
-private def traceStep (msg : String) : StateRefT State MetaM Unit :=
+private def traceStep (msg : String) : StateRefT State MetaM Unit := do
   trace[Meta.Match.match] "{msg} step"
 
 private def traceState (p : Problem) : MetaM Unit :=
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index d70fabcdf6..96e97f9d62 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -135,15 +135,12 @@ end
 def registerTraceClass (traceClassName : Name) : IO Unit :=
   registerOption (`trace ++ traceClassName) { group := "trace", defValue := false, descr := "enable/disable tracing for the given module and submodules" }
 
-syntax "trace[" ident "]" (interpolatedStr(term) <|> term) : term
-
-macro_rules
-  | `(trace[$id] $s) =>
-    if s.getKind == interpolatedStrKind then
-      `(Lean.trace $(quote id.getId) fun _ => m! $s)
-    else
-      `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
-
+macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $s) else `(($s : MessageData))
+  `(doElem| do
+    let cls := $(quote id.getId)
+    if (← Lean.isTracingEnabledFor cls) then
+      Lean.addTrace cls $msg)
 
 private def withNestedTracesFinalizer [Monad m] [MonadTrace m] (ref : Syntax) (currTraces : PersistentArray TraceElem) : m Unit := do
   modifyTraces fun traces =>
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index a26336f192..36b85cd110 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -7,7 +7,7 @@ open Lean.Meta
 -- set_option trace.Meta.isDefEq.delta false
 set_option trace.Meta.debug true
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def checkM (x : MetaM Bool) : MetaM Unit :=
diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
index 1e5c7eaa97..ed8b1379a1 100644
--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@@ -9,7 +9,7 @@ let opt := opt.setBool `trace.Meta true;
 -- let opt := opt.setBool `trace.Meta.check false;
 opt
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def check (x : MetaM Bool) : MetaM Unit :=
diff --git a/tests/lean/run/meta4.lean b/tests/lean/run/meta4.lean
index 1d8e41e84e..ea2eb872b6 100644
--- a/tests/lean/run/meta4.lean
+++ b/tests/lean/run/meta4.lean
@@ -3,7 +3,7 @@ import Lean.Meta
 open Lean
 open Lean.Meta
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def checkM (x : MetaM Bool) : MetaM Unit :=
diff --git a/tests/lean/run/meta6.lean b/tests/lean/run/meta6.lean
index e23aa0f729..162708022c 100644
--- a/tests/lean/run/meta6.lean
+++ b/tests/lean/run/meta6.lean
@@ -3,7 +3,7 @@ import Lean.Meta
 open Lean
 open Lean.Meta
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def checkM (x : MetaM Bool) : MetaM Unit :=
diff --git a/tests/lean/run/meta7.lean b/tests/lean/run/meta7.lean
index 9b86b1d6ae..b4b976f659 100644
--- a/tests/lean/run/meta7.lean
+++ b/tests/lean/run/meta7.lean
@@ -10,7 +10,7 @@ partial def fact : Nat → Nat
 set_option trace.Meta.debug true
 set_option trace.Meta.check false
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def checkM (x : MetaM Bool) : MetaM Unit :=
diff --git a/tests/lean/run/recInfo1.lean b/tests/lean/run/recInfo1.lean
index fc00da5188..fa38cb19fc 100644
--- a/tests/lean/run/recInfo1.lean
+++ b/tests/lean/run/recInfo1.lean
@@ -3,7 +3,7 @@ import Lean.Meta
 open Lean
 open Lean.Meta
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def showRecInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM Unit := do
diff --git a/tests/lean/run/synth1.lean b/tests/lean/run/synth1.lean
index 767a7b7912..74477ca9bf 100644
--- a/tests/lean/run/synth1.lean
+++ b/tests/lean/run/synth1.lean
@@ -24,7 +24,7 @@ instance coerceNatToBool : HasCoerce Nat Bool :=
 instance coerceNatToInt : HasCoerce Nat Int :=
 ⟨fun x => Int.ofNat x⟩
 
-def print {α} [ToString α] (a : α) : MetaM Unit :=
+def print {α} [ToString α] (a : α) : MetaM Unit := do
 trace[Meta.synthInstance] (toString a)
 
 
diff --git a/tests/lean/run/tactic.lean b/tests/lean/run/tactic.lean
index ec0e3df36f..b2c74c1474 100644
--- a/tests/lean/run/tactic.lean
+++ b/tests/lean/run/tactic.lean
@@ -6,7 +6,7 @@ open Lean.Meta
 
 axiom simple : forall {p q : Prop}, p → q → p
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.Tactic] msg
 
 def tst1 : MetaM Unit := do
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index 87b89119b2..d03c295fd3 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -38,6 +38,8 @@ do traceCtx `module $ do {
    -- Messages are computed lazily. The following message will only be computed
    -- if `trace.slow is active.
    trace[slow] (m!"slow message: " ++ toString (slow b))
+   -- This is true even if it is a monad computation:
+   trace[slow] (m!"slow message: " ++ (← toString (slow b)))
 
 def run (x : M Unit) : M Unit :=
 withReader