diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean
index 38fd9d2115..65bdfbc82a 100644
--- a/src/Init/Control/StateRef.lean
+++ b/src/Init/Control/StateRef.lean
@@ -31,7 +31,6 @@ variables {ω σ : Type} {m : Type → Type} {α : Type}
 
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
 instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
-instance [Monad m] [MonadIO m] : MonadIO (StateRefT' ω σ m) := inferInstanceAs (MonadIO (ReaderT _ _))
 instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
 
 @[inline] protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 226eb83227..4e031b3231 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -73,17 +73,6 @@ set_option compiler.extract_closed false in
    The action `initializing` returns `true` iff it is invoked during initialization. -/
 @[extern "lean_io_initializing"] constant IO.initializing : IO Bool
 
-class MonadIO (m : Type → Type) :=
-  { liftIO {α} : IO α → m α }
-
-export MonadIO (liftIO)
-
-instance (m n) [MonadIO m] [MonadLift m n] : MonadIO n :=
-  { liftIO := fun x => liftM (liftIO x : m _) }
-
-instance : MonadIO IO :=
-{ liftIO := id }
-
 namespace IO
 
 def ofExcept {ε α : Type} [ToString ε] (e : Except ε α) : IO α :=
@@ -190,10 +179,10 @@ def fopenFlags (m : FS.Mode) (b : Bool) : String :=
 end Prim
 
 namespace FS
-variables {m : Type → Type} [Monad m] [MonadIO m]
+variables {m : Type → Type} [Monad m] [MonadLiftT IO m]
 
 def Handle.mk (s : String) (Mode : Mode) (bin : Bool := true) : m Handle :=
-  liftIO (Prim.Handle.mk s (Prim.fopenFlags Mode bin))
+  liftM (Prim.Handle.mk s (Prim.fopenFlags Mode bin))
 
 @[inline]
 def withFile {α} (fn : String) (mode : Mode) (f : Handle → m α) : m α :=
@@ -203,15 +192,15 @@ def withFile {α} (fn : String) (mode : Mode) (f : Handle → m α) : m α :=
 `h.isEof` returns true /after/ the first attempt at reading past the end of `h`.
 Once `h.isEof` is true, the reading `h` raises `IO.Error.eof`.
 -/
-def Handle.isEof : Handle → m Bool := liftIO ∘ Prim.Handle.isEof
-def Handle.flush : Handle → m Unit := liftIO ∘ Prim.Handle.flush
-def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := liftIO (Prim.Handle.read h (USize.ofNat bytes))
-def Handle.write (h : Handle) (s : ByteArray) : m Unit := liftIO (Prim.Handle.write h s)
+def Handle.isEof : Handle → m Bool := liftM ∘ Prim.Handle.isEof
+def Handle.flush : Handle → m Unit := liftM ∘ Prim.Handle.flush
+def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := liftM (Prim.Handle.read h (USize.ofNat bytes))
+def Handle.write (h : Handle) (s : ByteArray) : m Unit := liftM (Prim.Handle.write h s)
 
-def Handle.getLine : Handle → m String := liftIO ∘ Prim.Handle.getLine
+def Handle.getLine : Handle → m String := liftM ∘ Prim.Handle.getLine
 
 def Handle.putStr (h : Handle) (s : String) : m Unit :=
-  liftIO $ Prim.Handle.putStr h s
+  liftM $ Prim.Handle.putStr h s
 
 def Handle.putStrLn (h : Handle) (s : String) : m Unit :=
   h.putStr (s.push '\n')
@@ -246,27 +235,27 @@ partial def lines (fname : String) : m (Array String) := do
 namespace Stream
 
 def putStrLn (strm : FS.Stream) (s : String) : m Unit :=
-  liftIO (strm.putStr (s.push '\n'))
+  liftM (strm.putStr (s.push '\n'))
 
 end Stream
 
 end FS
 
 section
-variables {m : Type → Type} [Monad m] [MonadIO m]
+variables {m : Type → Type} [Monad m] [MonadLiftT IO m]
 
-def getStdin : m FS.Stream := liftIO Prim.getStdin
-def getStdout : m FS.Stream := liftIO Prim.getStdout
-def getStderr : m FS.Stream := liftIO Prim.getStderr
+def getStdin : m FS.Stream := liftM Prim.getStdin
+def getStdout : m FS.Stream := liftM Prim.getStdout
+def getStderr : m FS.Stream := liftM Prim.getStderr
 
 /-- Replaces the stdin stream of the current thread and returns its previous value. -/
-def setStdin : FS.Stream → m FS.Stream := liftIO ∘ Prim.setStdin
+def setStdin : FS.Stream → m FS.Stream := liftM ∘ Prim.setStdin
 
 /-- Replaces the stdout stream of the current thread and returns its previous value. -/
-def setStdout : FS.Stream → m FS.Stream := liftIO ∘ Prim.setStdout
+def setStdout : FS.Stream → m FS.Stream := liftM ∘ Prim.setStdout
 
 /-- Replaces the stderr stream of the current thread and returns its previous value. -/
-def setStderr : FS.Stream → m FS.Stream := liftIO ∘ Prim.setStderr
+def setStderr : FS.Stream → m FS.Stream := liftM ∘ Prim.setStderr
 
 def withStdin [MonadFinally m] {α} (h : FS.Stream) (x : m α) : m α := do
   let prev ← setStdin h
@@ -280,32 +269,35 @@ def withStderr [MonadFinally m] {α} (h : FS.Stream) (x : m α) : m α := do
   let prev ← setStderr h
   try x finally discard $ setStderr prev
 
-def print {α} [ToString α] (s : α) : m Unit := do
+def print {α} [ToString α] (s : α) : IO Unit := do
   let out ← getStdout
-  liftIO $ out.putStr $ toString s
+  out.putStr $ toString s
 
-def println {α} [ToString α] (s : α) : m Unit := print ((toString s).push '\n')
+def println {α} [ToString α] (s : α) : IO Unit :=
+  print ((toString s).push '\n')
 
-def eprint {α} [ToString α] (s : α) : m Unit := do
+def eprint {α} [ToString α] (s : α) : IO Unit := do
   let out ← getStderr
-  liftIO $ out.putStr $ toString s
+  liftM $ out.putStr $ toString s
 
-def eprintln {α} [ToString α] (s : α) : m Unit := eprint ((toString s).push '\n')
+def eprintln {α} [ToString α] (s : α) : IO Unit :=
+  eprint ((toString s).push '\n')
 
 @[export lean_io_eprintln]
-private def eprintlnAux (s : String) : IO Unit := eprintln s
+private def eprintlnAux (s : String) : IO Unit :=
+  eprintln s
 
-def getEnv : String → m (Option String) := liftIO ∘ Prim.getEnv
-def realPath : String → m String := liftIO ∘ Prim.realPath
-def isDir : String → m Bool := liftIO ∘ Prim.isDir
-def fileExists : String → m Bool := liftIO ∘ Prim.fileExists
-def appPath : m String := liftIO Prim.appPath
+def getEnv : String → m (Option String) := liftM ∘ Prim.getEnv
+def realPath : String → m String := liftM ∘ Prim.realPath
+def isDir : String → m Bool := liftM ∘ Prim.isDir
+def fileExists : String → m Bool := liftM ∘ Prim.fileExists
+def appPath : m String := liftM Prim.appPath
 
 def appDir : m String := do
   let p ← appPath
   realPath (System.FilePath.dirName p)
 
-def currentDir : m String := liftIO Prim.currentDir
+def currentDir : m String := liftM Prim.currentDir
 
 end
 
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index dc319c9d04..65034a591a 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -27,7 +27,7 @@ structure Attr.Context :=
 abbrev AttrM := ReaderT Attr.Context CoreM
 
 instance : MonadLift ImportM AttrM := {
-  monadLift := fun x => do liftIO (x { env := (← getEnv), opts := (← getOptions) })
+  monadLift := fun x => do liftM (m := IO) (x { env := (← getEnv), opts := (← getOptions) })
 }
 
 instance : MonadResolveName AttrM := {
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 09e2686a69..d30b40a304 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -64,8 +64,8 @@ instance : MonadRecDepth CoreM := {
   let ref ← getRef
   IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x
 
-instance : MonadIO CoreM := {
-  liftIO := @liftIOCore
+instance : MonadLift IO CoreM := {
+  monadLift := liftIOCore
 }
 
 instance : MonadTrace CoreM := {
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 88658c853b..64079a535c 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -125,7 +125,7 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
   let ctx ← read
   IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
 
-instance : MonadIO CommandElabM := { liftIO := liftIO }
+instance : MonadLiftT IO CommandElabM := { monadLift := liftIO }
 
 def getScope : CommandElabM Scope := do pure (← get).scopes.head!
 
@@ -573,7 +573,7 @@ unsafe def elabEvalUnsafe : CommandElab := fun stx => do
     let env ← getEnv
     let opts ← getOptions
     let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) n finally setEnv env
-    let (out, res) ← MonadIO.liftIO $ act env opts -- we execute `act` using the environment
+    let (out, res) ← act env opts -- we execute `act` using the environment
     logInfo out
     match res with
     | Except.error e => throwError e.toString
@@ -587,7 +587,7 @@ unsafe def elabEvalUnsafe : CommandElab := fun stx => do
     let e ← mkAppM `Lean.runEval #[e]
     let env ← getEnv
     let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) n finally setEnv env
-    let (out, res) ← MonadIO.liftIO act
+    let (out, res) ← liftM (m := IO) act
     logInfo out
     match res with
     | Except.error e => throwError e.toString
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index ea611b48ac..3f7e3a607b 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -62,12 +62,12 @@ def logWarning (msgData : MessageData) : m Unit :=
 def logInfo (msgData : MessageData) : m Unit :=
   log msgData MessageSeverity.information
 
-def logException [MonadIO m] (ex : Exception) : m Unit := do
+def logException [MonadLiftT IO m] (ex : Exception) : m Unit := do
   match ex with
   | Exception.error ref msg => logErrorAt ref msg
   | Exception.internal id   =>
     unless id == abortExceptionId do
-      let name ← liftIO $ id.getName
+      let name ← id.getName
       logError ("internal exception: " ++ name)
 
 def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index cc4a6d5c92..6a294dfd35 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -82,20 +82,20 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := withRef s
     toParserDescrAux stx[1]
   else if kind == `Lean.Parser.Syntax.unary then
     let aliasName := (stx[0].getId).eraseMacroScopes
-    liftIO $ Parser.ensureUnaryParserAlias aliasName
+    Parser.ensureUnaryParserAlias aliasName
     let d ← withNestedParser $ toParserDescrAux stx[2]
     `(ParserDescr.unary $(quote aliasName) $d)
   else if kind == `Lean.Parser.Syntax.binary then
     let aliasName := (stx[0].getId).eraseMacroScopes
-    liftIO $ Parser.ensureBinaryParserAlias aliasName
+    Parser.ensureBinaryParserAlias aliasName
     let d₁ ← withNestedParser $ toParserDescrAux stx[2]
     let d₂ ← withNestedParser $ toParserDescrAux stx[4]
     `(ParserDescr.binary $(quote aliasName) $d₁ $d₂)
   else if kind == `Lean.Parser.Syntax.cat then
     let cat   := stx[0].getId.eraseMacroScopes
     let prec? : Option Nat  := expandOptPrecedence stx[1]
-    if (← liftIO $ Parser.isParserAlias cat) then
-      liftIO $ Parser.ensureConstantParserAlias cat
+    if (← Parser.isParserAlias cat) then
+      Parser.ensureConstantParserAlias cat
       if prec?.isSome then
         throwErrorAt! stx[1] "unexpected precedence in atomic parser"
       `(ParserDescr.const $(quote cat))
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 6c7f7b10c2..497a18bda6 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -201,9 +201,6 @@ def applyResult (result : TermElabResult) : TermElabM Expr :=
   | EStateM.Result.ok e r     => do r.restore; pure e
   | EStateM.Result.error ex r => do r.restore; throw ex
 
-instance : MonadIO TermElabM :=
-{ liftIO := fun x => liftMetaM $ liftIO x }
-
 @[inline] protected def liftMetaM {α} (x : MetaM α) : TermElabM α :=
   liftM x
 
@@ -1264,7 +1261,7 @@ instance {α} [MetaEval α] : MetaEval (TermElabM α) :=
     let x : TermElabM α := do
       try x finally
         let s ← get
-        liftIO $ s.messages.forM fun msg => msg.toString >>= IO.println
+        s.messages.forM fun msg => do IO.println (← msg.toString)
     MetaEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩
 
 end Term
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index 50e390a9c3..7f91e8de10 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -142,7 +142,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
         if c != df.valueTypeName then throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected"
         else
           let env ← getEnv
-          let env ← liftIO $ declareBuiltin df attrDeclName env key declName
+          let env ← declareBuiltin df attrDeclName env key declName
           setEnv env
       | _ => throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected",
     applicationTime := AttributeApplicationTime.afterCompilation
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 01135df4ea..22ef4c9fa2 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -113,10 +113,6 @@ structure Context :=
 
 abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 
-instance : MonadIO MetaM := {
-  liftIO := fun x => liftM (liftIO x : CoreM _)
-}
-
 instance {α} : Inhabited (MetaM α) := {
   default := fun _ _ => arbitrary _
 }
@@ -191,20 +187,20 @@ builtin_initialize isExprDefEqAuxRef : IO.Ref (Expr → Expr → MetaM Bool) ←
 builtin_initialize synthPendingRef : IO.Ref (MVarId → MetaM Bool) ← IO.mkRef fun _ => pure false
 
 def whnf (e : Expr) : m Expr :=
-  liftMetaM $ withIncRecDepth do (← liftIO whnfRef.get) e
+  liftMetaM $ withIncRecDepth do (← whnfRef.get) e
 
 def whnfForall [Monad m] (e : Expr) : m Expr := do
   let e' ← whnf e
   if e'.isForall then pure e' else pure e
 
 def inferType (e : Expr) : m Expr :=
-  liftMetaM $ withIncRecDepth do (← liftIO inferTypeRef.get) e
+  liftMetaM $ withIncRecDepth do (← inferTypeRef.get) e
 
 protected def isExprDefEqAux (t s : Expr) : MetaM Bool :=
-  withIncRecDepth do (← liftIO isExprDefEqAuxRef.get) t s
+  withIncRecDepth do (← isExprDefEqAuxRef.get) t s
 
 protected def synthPending (mvarId : MVarId) : MetaM Bool :=
-  withIncRecDepth do (← liftIO synthPendingRef.get) mvarId
+  withIncRecDepth do (← synthPendingRef.get) mvarId
 
 -- withIncRecDepth for a monad `n` such that `[MonadControlT MetaM n]`
 protected def withIncRecDepth {α} (x : n α) : n α :=
@@ -982,7 +978,7 @@ def ppExprImp (e : Expr) : MetaM Format := do
   let mctx ← getMCtx
   let lctx ← getLCtx
   let opts ← getOptions
-  liftIO $ Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts } e
+  Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts } e
 
 def ppExpr (e : Expr) : m Format :=
   liftMetaM $ ppExprImp e
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index bc9329de72..8c84db4b47 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -38,9 +38,9 @@ def addGlobalInstanceImp (env : Environment) (constName : Name) : IO Environment
     let (keys, s, _) ← (mkInstanceKey c).toIO {} { env := env } {} {}
     pure $ instanceExtension.addEntry s.env { keys := keys, val := c }
 
-def addGlobalInstance {m} [Monad m] [MonadEnv m] [MonadIO m] (declName : Name) : m Unit := do
+def addGlobalInstance {m} [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m Unit := do
   let env ← getEnv
-  let env ← liftIO $ Meta.addGlobalInstanceImp env declName
+  let env ← Meta.addGlobalInstanceImp env declName
   setEnv env
 
 builtin_initialize
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index e00498dd93..100dcdfa9e 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -40,7 +40,7 @@ def getMVarType (mvarId : MVarId) : MetaM Expr := do
   pure (← getMVarDecl mvarId).type
 
 def ppGoal (mvarId : MVarId) : MetaM Format := do
-  liftIO $ Lean.ppGoal { env := (← getEnv), mctx := (← getMCtx), opts := (← getOptions) } mvarId
+  Lean.ppGoal { env := (← getEnv), mctx := (← getMCtx), opts := (← getOptions) } mvarId
 
 builtin_initialize registerTraceClass `Meta.Tactic
 
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 8e332c2deb..5745efe975 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -476,10 +476,10 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
   let env ← getEnv
   match decl.type with
   | Expr.const `Lean.Parser.TrailingParser _ _ => do
-    let env ← liftIO $ declareTrailingBuiltinParser env catName declName prio
+    let env ← declareTrailingBuiltinParser env catName declName prio
     setEnv env
   | Expr.const `Lean.Parser.Parser _ _ => do
-    let env ← liftIO $ declareLeadingBuiltinParser env catName declName prio
+    let env ← declareLeadingBuiltinParser env catName declName prio
     setEnv env
   | _ => throwError! "unexpected parser type at '{declName}' (`Parser` or `TrailingParser` expected)"
   runParserAttributeHooks catName declName (builtin := true)
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index c02254ab82..7364637ff5 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -87,7 +87,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
         let env ← getEnv
         let env ← match env.addAndCompile {} decl with
           | Except.ok    env => pure env
-          | Except.error kex => do throwError (← liftIO $ (kex.toMessageData {}).toString)
+          | Except.error kex => do throwError (← (kex.toMessageData {}).toString)
         setEnv $ ctx.combinatorAttr.setDeclFor env c c'
         mkCall c'
       else
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index aea98a6c08..0097b62e02 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -438,9 +438,9 @@ builtin_initialize
 
 @[export lean_pretty_printer_formatter_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
-  | ParserDescr.const n                             => liftIO $ getConstAlias formatterAliasesRef n
-  | ParserDescr.unary n d                           => return (← liftIO $ getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d)
-  | ParserDescr.binary n d₁ d₂                      => return (← liftIO $ getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
+  | ParserDescr.const n                             => getConstAlias formatterAliasesRef n
+  | ParserDescr.unary n d                           => return (← getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d)
+  | ParserDescr.binary n d₁ d₂                      => return (← getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
   | ParserDescr.node k prec d                       => return node.formatter k (← interpretParserDescr d)
   | ParserDescr.nodeWithAntiquot _ k d              => return node.formatter k (← interpretParserDescr d)
   | ParserDescr.trailingNode k prec d               => return trailingNode.formatter k prec (← interpretParserDescr d)
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index f406a8acd3..328c3a67a6 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -517,9 +517,9 @@ builtin_initialize
 
 @[export lean_pretty_printer_parenthesizer_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer
-  | ParserDescr.const n                             => liftIO $ getConstAlias parenthesizerAliasesRef n
-  | ParserDescr.unary n d                           => return (← liftIO $ getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d)
-  | ParserDescr.binary n d₁ d₂                      => return (← liftIO $ getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
+  | ParserDescr.const n                             => getConstAlias parenthesizerAliasesRef n
+  | ParserDescr.unary n d                           => return (← getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d)
+  | ParserDescr.binary n d₁ d₂                      => return (← getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
   | ParserDescr.node k prec d                       => return leadingNode.parenthesizer k prec (← interpretParserDescr d)
   | ParserDescr.nodeWithAntiquot _ k d              => return node.parenthesizer k (← interpretParserDescr d)
   | ParserDescr.trailingNode k prec d               => return trailingNode.parenthesizer k prec (← interpretParserDescr d)
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index 07e717cf4c..7a71e13bf1 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -71,7 +71,6 @@ instance  : MonadHashMapCacheAdapter α β (MonadCacheT α β m) := {
 
 instance : Monad (MonadCacheT α β m) := inferInstanceAs (Monad (StateRefT' _ _ _))
 instance : MonadLift m (MonadCacheT α β m) := inferInstanceAs (MonadLift m (StateRefT' _ _ _))
-instance [MonadIO m] : MonadIO (MonadCacheT α β m) := inferInstanceAs (MonadIO (StateRefT' _ _ _))
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (MonadCacheT α β m) := inferInstanceAs (MonadExceptOf ε (StateRefT' _ _ _))
 instance : MonadControl m (MonadCacheT α β m) := inferInstanceAs (MonadControl m (StateRefT' _ _ _))
 instance [MonadFinally m] : MonadFinally (MonadCacheT α β m) := inferInstanceAs (MonadFinally (StateRefT' _ _ _))
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index f678dc7fe0..a92e1e062c 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -47,11 +47,11 @@ instance (m n) [MonadTrace m] [MonadLift m n] : MonadTrace n :=
 
 variables {α : Type} {m : Type → Type} [Monad m] [MonadTrace m]
 
-def printTraces {m} [Monad m] [MonadTrace m] [MonadIO m] : m Unit := do
+def printTraces {m} [Monad m] [MonadTrace m] [MonadLiftT IO m] : m Unit := do
   let traceState ← getTraceState
   traceState.traces.forM fun m => do
-    let d ← liftIO m.msg.format
-    liftIO $ IO.println d
+    let d ← m.msg.format
+    IO.println d
 
 def resetTraceState {m} [MonadTrace m] : m Unit :=
   modifyTraceState (fun _ => {})
diff --git a/tests/lean/ppExpr.lean b/tests/lean/ppExpr.lean
index edf393c0dd..642569acef 100644
--- a/tests/lean/ppExpr.lean
+++ b/tests/lean/ppExpr.lean
@@ -5,8 +5,8 @@ import Lean
 
 open Lean
 
-def test (e : Expr) : MetaM Unit :=
-PrettyPrinter.ppExpr Name.anonymous [] e >>= IO.println
+def test (e : Expr) : MetaM Unit := do
+  IO.println (← PrettyPrinter.ppExpr Name.anonymous [] e)
 
 -- loose bound variable
 #eval test (mkBVar 0)
diff --git a/tests/lean/ppSyntax.lean b/tests/lean/ppSyntax.lean
index 76c4d66c46..cc02000351 100644
--- a/tests/lean/ppSyntax.lean
+++ b/tests/lean/ppSyntax.lean
@@ -2,8 +2,8 @@ import Lean
 
 open Lean
 
-def test (stx : Unhygienic Syntax) : MetaM Unit :=
-  PrettyPrinter.ppTerm stx.run >>= IO.println
+def test (stx : Unhygienic Syntax) : MetaM Unit := do
+  IO.println (← PrettyPrinter.ppTerm stx.run)
 
 -- test imported `ParserDescr`
 #eval test `(s!"hi!")
diff --git a/tests/lean/run/evalconst.lean b/tests/lean/run/evalconst.lean
index 43f1a962ae..697caa6f26 100644
--- a/tests/lean/run/evalconst.lean
+++ b/tests/lean/run/evalconst.lean
@@ -14,7 +14,7 @@ def f (x : Nat) := x + 1
 
 unsafe def tst2 : CoreM Unit := do
 let env ← getEnv
-let f ← liftIO $ IO.ofExcept $ env.evalConst (Nat → Nat) {} `f
+let f ←  IO.ofExcept $ env.evalConst (Nat → Nat) {} `f
 IO.println $ (f 10)
 
 #eval tst2
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index d7aa814e93..261aeabc56 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -6,8 +6,8 @@ open Lean.Elab
 def runM (input : String) (failIff : Bool := true) : CoreM Unit := do
 let env  ← getEnv;
 let opts ← getOptions;
-let (env, messages) ← liftIO $ process input env opts;
-messages.forM $ fun msg => (liftIO msg.toString) >>= IO.println;
+let (env, messages) ← process input env opts;
+messages.forM fun msg => do IO.println (← msg.toString)
 when (failIff && messages.hasErrors) $ throwError "errors have been found";
 when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
 pure ()
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index ebee6a09e9..48c64ea052 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -6,8 +6,8 @@ open Lean.Elab
 def runCore (input : String) (failIff : Bool := true) : CoreM Unit := do
 let env  ← getEnv;
 let opts ← getOptions;
-let (env, messages) ← liftIO $ process input env opts;
-messages.toList.forM $ fun msg => liftIO (msg.toString >>= IO.println);
+let (env, messages) ← process input env opts;
+messages.toList.forM fun msg => do IO.println (← msg.toString)
 when (failIff && messages.hasErrors) $ throwError "errors have been found";
 when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
 pure ()
diff --git a/tests/lean/typeMismatch.lean.expected.out b/tests/lean/typeMismatch.lean.expected.out
index fa2d061a67..a0a68e83f4 100644
--- a/tests/lean/typeMismatch.lean.expected.out
+++ b/tests/lean/typeMismatch.lean.expected.out
@@ -1,7 +1,7 @@
 typeMismatch.lean:7:0: error: type mismatch
   IO.println ""
 has type
-  EIO IO.Error Unit
+  IO Unit
 but is expected to have type
   IO Nat
 typeMismatch.lean:12:0: error: type mismatch