refactor: remove MonadIO

There is no reason for having `MonadIO` anymore. The `MonadLift` type
class is well behaved in the new frontend, the `MonadFinally` solves
the problem at monad stacks such as `ExcepT e IO`.

This commit also changes the type of the IO printing functions.
For example, the type of `IO.println` was
```
def IO.println {m} [MonadIO m] {α} [ToString α] (s : α) : m Unit
```
and now it is just
```
def IO.println {α} [ToString α] (s : α) : IO Unit
```
We rely on the new frontend auto-lifting feature.
That is, if there is an instance `[MonadLiftT IO m]`, then
a term of type `IO a` is automatically coerced to `m a`

We also want a simpler `IO.println` for writing tests.
For example,
```
```
doesn't work because there isn't sufficient information for inferring
the parameter `m` in the previous `IO.println`.
The shortest workaround looked very weird
```
```

I considered adding `IO` as a default value for `m` when we have
`MonadIO m`, as we use `Nat` as the default for `ofNat a`, but it felt
like uncessary complexity.

@Kha The commit seems to work well. The auto-lifting featuring has
been working great for me. There is still room for improvement.
For example, given `MonadLiftT m n`, it doesn't automatically lift
`a -> m b` into `a -> n b`. So, code such as
`foo >>= IO.println`
had to be rewritten as
`foo >>= fun x => IO.println x`
I will add this feature later.
If you have time, please try to play with this feature and figure out
if it is stable enough for making it the default.
That is, if it roboust enough, we can stop using the following idiom
for writing functions that can be lifted automatically.
```
def instantiateLevelMVarsImp (u : Level) : MetaM Level :=
  ...

def instantiateLevelMVars {m} [MonadLiftT MetaM m] (u : Level) : m Level :=
  liftMetaM $ instantiateLevelMVarsImp u
```
I think we only need this idiom when using `MonadControlT` which is
not as common as `MonadLiftT`.

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 σ :=

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
 

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 := {

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 := {

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

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

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))

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

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

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

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

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
 

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)

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

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)

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)

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' _ _ _))

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 _ => {})

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)

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!")

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

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 ()

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 ()

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