diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index bbb0bc9a70..2a036206b4 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -199,6 +199,9 @@ end
 instance (ε m out) [MonadRun out m] : MonadRun (fun α => out (Except ε α)) (ExceptT ε m) :=
 ⟨fun α => run⟩
 
+@[inline] def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α) :=
+catch (do a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
+
 /-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
 @[inline] def finally {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) (finalizer : m PUnit) : m α := do
 r ← catch (Except.ok <$> x) (fun ex => @pure m _ _ $ Except.error ex);
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 961ddbda2e..2a2224c8cd 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -191,8 +191,8 @@ namespace Environment
 @[export lean_add_attribute]
 def addAttribute (env : Environment) (decl : Name) (attrName : Name) (args : Syntax := Syntax.missing) (persistent := true) : IO Environment := do
 attr ← IO.ofExcept $ getAttributeImpl env attrName;
-(env, _) ← (attr.add decl args persistent).run' env;
-pure env
+(_, s) ← (attr.add decl args persistent).toIO {} { env := env };
+pure s.env
 
 /-
 /- Add a scoped attribute `attr` to declaration `decl` with arguments `args` and scope `decl.getPrefix`.
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index b01afc6afd..05f7b5d32f 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -23,7 +23,7 @@ instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
 structure Context :=
 (options        : Options := {})
 (currRecDepth   : Nat := 0)
-(maxRecDepth    : Nat)
+(maxRecDepth    : Nat := 1000)
 (ref            : Syntax := Syntax.missing)
 
 inductive Exception
@@ -75,13 +75,13 @@ checkRecDepth; adaptReader Context.incCurrRecDepth x
 def getRef {ε} : ECoreM ε Syntax := do
 ctx ← read; pure ctx.ref
 
-def getEnv : CoreM Environment := do
+def getEnv {ε} : ECoreM ε Environment := do
 s ← get; pure s.env
 
-def setEnv (env : Environment) : CoreM Unit :=
+def setEnv {ε} (env : Environment) : ECoreM ε Unit :=
 modify $ fun s => { s with env := env }
 
-@[inline] def modifyEnv (f : Environment → Environment) : CoreM Unit :=
+@[inline] def modifyEnv {ε} (f : Environment → Environment) : ECoreM ε Unit :=
 modify $ fun s => { s with env := f s.env }
 
 def getOptions {ε} : ECoreM ε Options :=  do
@@ -90,16 +90,16 @@ ctx ← read; pure ctx.options
 def getTraceState {ε} : ECoreM ε TraceState := do
 s ← get; pure s.traceState
 
-def setTraceState {ε} [MonadIO (EIO ε)] (traceState : TraceState) : ECoreM ε Unit := do
+def setTraceState {ε} (traceState : TraceState) : ECoreM ε Unit := do
 modify fun s => { s with traceState := traceState }
 
-def getNGen : CoreM NameGenerator := do
+def getNGen {ε} : ECoreM ε NameGenerator := do
 s ← get; pure s.ngen
 
-def setNGen (ngen : NameGenerator) : CoreM Unit :=
+def setNGen {ε} (ngen : NameGenerator) : ECoreM ε Unit :=
 modify fun s => { s with ngen := ngen }
 
-def mkFreshId : CoreM Name := do
+def mkFreshId {ε} : ECoreM ε Name := do
 s ← get;
 let id := s.ngen.curr;
 modify $ fun s => { s with ngen := s.ngen.next };
@@ -113,10 +113,10 @@ match ref.getPos with
 def Context.replaceRef (ref : Syntax) (ctx : Context) : Context :=
 { ctx with ref := replaceRef ref ctx.ref }
 
-@[inline] def withRef {α} (ref : Syntax) (x : CoreM α) : CoreM α := do
+@[inline] def withRef {ε} {α} (ref : Syntax) (x : ECoreM ε α) : ECoreM ε α := do
 adaptReader (Context.replaceRef ref) x
 
-@[inline] private def getTraceState : CoreM TraceState := do
+@[inline] private def getTraceState {ε} : ECoreM ε TraceState := do
 s ← get; pure s.traceState
 
 def addContext {ε} (msg : MessageData) : ECoreM ε MessageData := do
@@ -147,7 +147,7 @@ def addAndCompile (decl : Declaration) : CoreM Unit := do
 addDecl decl;
 compileDecl decl
 
-def dbgTrace {α} [HasToString α] (a : α) : CoreM Unit :=
+def dbgTrace {ε} {α} [HasToString α] (a : α) : ECoreM ε Unit :=
 _root_.dbgTrace (toString a) $ fun _ => pure ()
 
 def getConstInfo (constName : Name) : CoreM ConstantInfo := do
@@ -156,29 +156,28 @@ match env.find? constName with
 | some info => pure info
 | none      => throwError ("unknown constant '" ++ constName ++ "'")
 
-@[inline] def CoreM.run' {α} (x : CoreM α) (env : Environment) (options : Options := {}) : IO (Environment × α) := do
-let x : CoreM (Environment × α) := finally (do a ← x; env ← getEnv; pure (env, a)) do {
-  traceState ← getTraceState;
-  traceState.traces.forM $ fun m => liftIO $ IO.println $ format m
-};
-let x : EIO Exception (Environment × α) := (x { maxRecDepth := getMaxRecDepth options, options := options }).run' { env := env };
-x.toIO fun ex => match ex with
+def printTraces : CoreM Unit := do
+traceState ← getTraceState;
+traceState.traces.forM $ fun m => liftIO $ IO.println $ format m
+
+def resetTraceState {ε} : ECoreM ε Unit :=
+modify fun s => { s with traceState := {} }
+
+@[inline] def ECoreM.run {ε α} (x : ECoreM ε α) (ctx : Context) (s : State) : EIO ε (α × State) :=
+(x.run ctx).run s
+
+@[inline] def CoreM.toIO {α} (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) :=
+adaptExcept
+  (fun ex => match ex with
     | Exception.io ex         => ex
     | Exception.kernel ex opt => IO.userError $ toString $ format $ ex.toMessageData opt
-    | Exception.error _ msg   => IO.userError $ toString $ format $ msg
-
-@[inline] def CoreM.run {α} (x : CoreM α) (env : Environment) (options : Options := {}) : IO α := do
-(_, a) ← x.run' env options;
-pure a
+    | Exception.error _ msg   => IO.userError $ toString $ format $ msg)
+  (x.run ctx s)
 
 instance hasEval {α} [MetaHasEval α] : MetaHasEval (CoreM α) :=
 ⟨fun env opts x _ => do
-  (env, a) ← x.run' env opts;
-  MetaHasEval.eval env opts a⟩
-
-@[inline] def ECoreM.run {ε α} (x : ECoreM ε α) (env : Environment) (options : Options) (maxRecDepth? : Option Nat := none) : EIO ε α :=
-let maxRecDepth := maxRecDepth?.getD (getMaxRecDepth options);
-(x.run { options := options, maxRecDepth := maxRecDepth }).run' { env := env }
+   (a, s) ← (finally x printTraces).toIO { maxRecDepth := getMaxRecDepth opts, options := opts} { env := env};
+   MetaHasEval.eval s.env opts a⟩
 
 end Core
 
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index f4081c0e7c..2d9305217f 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -206,9 +206,15 @@ def annotateCurPos (stx : Syntax) : Delab := do
 ctx ← read;
 pure $ annotatePos ctx.pos stx
 
+@[inline] def liftMetaM {α} (x : MetaM α) : DelabM α :=
+liftM x
+
+def getEnv : DelabM Environment :=
+liftMetaM $ Meta.getEnv
+
 partial def delabFor : Name → Delab
 | k => do
-  env ← liftM getEnv;
+  env ← getEnv;
   (match (delabAttribute.ext.getState env).table.find? k with
    | some delabs => delabs.firstM id >>= annotateCurPos
    | none        => failure) <|>
@@ -330,7 +336,7 @@ private partial def delabBinders (delabGroup : Array Syntax → Syntax → Delab
 -- binder group `(d e ...)` as determined by `shouldGroupWithNext`. We cannot do grouping
 -- inside-out, on the Syntax level, because it depends on comparing the Expr binder types.
 | curNames => do
-  lctx ← liftM $ getLCtx;
+  lctx ← liftMetaM $ getLCtx;
   e ← getExpr;
   let n := lctx.getUnusedName e.bindingName!;
   stxN ← annotateCurPos (mkIdent n);
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 1dd743c546..e99c8d0df3 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -136,7 +136,7 @@ private partial def elabBinderViews (binderViews : Array BinderView)
       let fvars := fvars.push fvar;
       -- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
       let lctx  := lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
-      className? ← isClass type;
+      className? ← isClass? type;
       match className? with
       | none           => elabBinderViews (i+1) fvars lctx localInsts
       | some className => do
@@ -327,7 +327,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat 
       let lctx  := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
       s ← withRef binderView.id $ propagateExpectedType fvar type s;
       let s := { s with lctx := lctx };
-      className? ← isClass type;
+      className? ← isClass? type;
       match className? with
       | none           => elabFunBinderViews (i+1) s
       | some className => do
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 44a9b20d62..85ea6f4bc2 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -409,20 +409,18 @@ structure OldContext :=
 (open_nss : List Name)
 
 private unsafe def oldRunTermElabMUnsafe {α} (oldCtx : OldContext) (x : TermElabM α) : Except String α := do
-let updateCtx (ctx : Context) : Context :=
-  { ctx with
-    fileName      := "foo",
-    currNamespace := oldCtx.env.getNamespace,
-    openDecls     := oldCtx.open_nss.map $ fun n => OpenDecl.simple n []
-  };
-let x : TermElabM α := adaptReader updateCtx x;
-let updateMetaCtx (ctx : Meta.Context) : Meta.Context :=
-  { ctx with lctx := oldCtx.locals.foldl (fun lctx l => LocalContext.mkLocalDecl lctx l l exprPlaceholder) $ LocalContext.mkEmpty () };
-let x : TermElabM α := adaptTheReader Meta.Context updateMetaCtx x;
-let x : IO α := ((x.run).run).run oldCtx.env;
-match unsafeIO x with
-| Except.ok a      => Except.ok a
-| Except.error e   => Except.error (toString e)
+let ctxMeta : Meta.Context := {
+  lctx := oldCtx.locals.foldl (fun lctx l => LocalContext.mkLocalDecl lctx l l exprPlaceholder) $ LocalContext.mkEmpty ()
+};
+let ctxTerm : Term.Context := {
+  fileName := "foo",
+  fileMap := FileMap.ofString "",
+  currNamespace := oldCtx.env.getNamespace,
+  openDecls := oldCtx.open_nss.map $ fun n => OpenDecl.simple n []
+};
+match unsafeIO $ x.toIO {} { env := oldCtx.env } ctxMeta {} ctxTerm {} with
+| Except.ok (a, _, _, _) => Except.ok a
+| Except.error e         => Except.error (toString e)
 
 @[implementedBy oldRunTermElabMUnsafe]
 constant oldRunTermElabM {α} (oldCtx : OldContext) (x : TermElabM α) : Except String α := arbitrary _
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 014e4faf2f..adc24ac6ec 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -324,7 +324,7 @@ def whnfCore (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnfCore e
 def unfoldDefinition? (e : Expr) : TermElabM (Option Expr) := liftMetaM $ Meta.unfoldDefinition? e
 def instantiateMVars (e : Expr) : TermElabM Expr := liftMetaM $ Meta.instantiateMVars e
 def instantiateLevelMVars (u : Level) : TermElabM Level := liftMetaM $ Meta.instantiateLevelMVars u
-def isClass (t : Expr) : TermElabM (Option Name) := liftMetaM $ Meta.isClass t
+def isClass? (t : Expr) : TermElabM (Option Name) := liftMetaM $ Meta.isClass? t
 def mkFreshId : TermElabM Name := liftMetaM Meta.mkFreshId
 def mkFreshLevelMVar : TermElabM Level := liftMetaM $ Meta.mkFreshLevelMVar
 def mkFreshExprMVar (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
@@ -504,7 +504,7 @@ lctx       ← getLCtx;
 localInsts ← getLocalInsts;
 let lctx   := lctx.mkLocalDecl fvarId n type binderInfo;
 let fvar   := mkFVar fvarId;
-c?         ← isClass type;
+c?         ← isClass? type;
 match c? with
 | some c => adaptTheReader Meta.Context
     (fun ctx => { ctx with lctx := lctx, localInstances := localInsts.push { className := c, fvar := fvar } }) $
@@ -517,7 +517,7 @@ lctx       ← getLCtx;
 localInsts ← getLocalInsts;
 let lctx   := lctx.mkLetDecl fvarId n type val;
 let fvar   := mkFVar fvarId;
-c?         ← isClass type;
+c?         ← isClass? type;
 match c? with
 | some c => adaptTheReader Meta.Context
               (fun ctx => { ctx with lctx := lctx, localInstances := localInsts.push { className := c, fvar := fvar } }) $
@@ -1324,18 +1324,15 @@ fun stx _ =>
   | some val => pure $ toExpr val
   | none     => throwError "ill-formed syntax"
 
-private def printMessages : TermElabM Unit := do
-s ← get;
-s.messages.forM $ fun m => IO.println $ format m
-
-def TermElabM.run {α} (x : TermElabM α) : MetaM α := do
-let x : TermElabM α := do { a ← x; printMessages; pure a };
-let ctx : Context := {
-  fileName      := "<TermElabM>",
+private def mkSomeContext : Context :=
+{ fileName      := "<TermElabM>",
   fileMap       := arbitrary _,
-  currNamespace := Name.anonymous,
-};
-let x : EMetaM Exception α := (x ctx).run' {};
+  currNamespace := Name.anonymous }
+
+@[inline] def ETermElabM.run {ε α} (x : ETermElabM ε α) (ctx : Context := mkSomeContext) (s : State := {}) : EMetaM ε (α × State) :=
+(x.run ctx).run s
+
+@[inline] private def toMetaMAux {α} (x : EMetaM Exception α) : MetaM α := do
 ref ← Meta.getRef;
 let mkMetaException (msg : MessageData) : Meta.Exception := Meta.Exception.core (Core.Exception.error ref msg);
 adaptExcept
@@ -1346,8 +1343,18 @@ adaptExcept
     | Exception.ex (Elab.Exception.error msg)        => mkMetaException msg.data)
   x
 
+@[inline] def TermElabM.toMetaM {α} (x : TermElabM α) (ctx : Context := mkSomeContext) (s : State := {}) : MetaM (α × State) :=
+toMetaMAux $ x.run ctx s
+
+@[inline] def TermElabM.toIO {α} (x : TermElabM α)
+    (ctxCore : Core.Context) (sCore : Core.State)
+    (ctxMeta : Meta.Context) (sMeta : Meta.State)
+    (ctx : Context) (s : State) : IO (α × Core.State × Meta.State × State) := do
+((a, s), sCore, sMeta) ← (toMetaMAux (x.run ctx s)).toIO ctxCore sCore ctxMeta sMeta;
+pure (a, sCore, sMeta, s)
+
 instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
-⟨fun env opts x _ => MetaHasEval.eval env opts x.run⟩
+⟨fun env opts x _ => MetaHasEval.eval env opts (do (a, _) ← x.toMetaM; pure a)⟩
 
 end Term
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 4956a8057c..669c23c32a 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -139,14 +139,20 @@ abbrev MetaM := EMetaM Exception
 @[inline] def liftCoreM {α} (x : CoreM α) : MetaM α :=
 liftM $ (adaptExcept Exception.core x : ECoreM Exception α)
 
+@[inline] def liftECoreM {ε α} (x : ECoreM ε α) : EMetaM ε α :=
+liftM x
+
+@[inline] def mapECoreM {ε} (f : forall {α}, ECoreM ε α → ECoreM ε α) {α} : EMetaM ε α → EMetaM ε α :=
+monadMap @f
+
 instance MetaM.inhabited {α} : Inhabited (MetaM α) :=
 ⟨fun _ _ => arbitrary _⟩
 
 def throwError {α} (msg : MessageData) : MetaM α :=
 liftCoreM $ Core.throwError msg
 
-def addContext (msg : MessageData) : MetaM MessageData :=
-liftCoreM $ Core.addContext msg
+def addContext {ε} (msg : MessageData) : EMetaM ε MessageData :=
+liftECoreM $ Core.addContext msg
 
 def checkRecDepth : MetaM Unit :=
 liftCoreM $ Core.checkRecDepth
@@ -155,47 +161,47 @@ liftCoreM $ Core.checkRecDepth
 checkRecDepth;
 adaptTheReader Core.Context Core.Context.incCurrRecDepth x
 
-def getRef : MetaM Syntax :=
-liftCoreM Core.getRef
+def getRef {ε} : EMetaM ε Syntax :=
+liftECoreM Core.getRef
 
-@[inline] def withRef {α} (ref : Syntax) (x : MetaM α) : MetaM α := do
-adaptTheReader Core.Context (Core.Context.replaceRef ref) x
+@[inline] def withRef {ε α} (ref : Syntax) (x : EMetaM ε α) : EMetaM ε α := do
+mapECoreM (fun α => Core.withRef ref) x
 
-@[inline] def getLCtx : MetaM LocalContext := do
+@[inline] def getLCtx {ε} : EMetaM ε LocalContext := do
 ctx ← read; pure ctx.lctx
 
-@[inline] def getLocalInstances : MetaM LocalInstances := do
+@[inline] def getLocalInstances {ε} : EMetaM ε LocalInstances := do
 ctx ← read; pure ctx.localInstances
 
-@[inline] def getConfig : MetaM Config := do
+@[inline] def getConfig {ε} : EMetaM ε Config := do
 ctx ← read; pure ctx.config
 
-@[inline] def getMCtx : MetaM MetavarContext := do
+@[inline] def getMCtx {ε} : EMetaM ε MetavarContext := do
 s ← get; pure s.mctx
 
-def setMCtx (mctx : MetavarContext) : MetaM Unit :=
+def setMCtx {ε} (mctx : MetavarContext) : EMetaM ε Unit :=
 modify $ fun s => { s with mctx := mctx }
 
-@[inline] def getOptions : MetaM Options :=
-liftCoreM Core.getOptions
+@[inline] def getOptions {ε} : EMetaM ε Options :=
+liftECoreM Core.getOptions
 
-@[inline] def getEnv : MetaM Environment :=
-liftCoreM Core.getEnv
+@[inline] def getEnv {ε} : EMetaM ε Environment :=
+liftECoreM Core.getEnv
 
-def setEnv (env : Environment) : MetaM Unit :=
-liftCoreM $ Core.setEnv env
+def setEnv {ε} (env : Environment) : EMetaM ε Unit :=
+liftECoreM $ Core.setEnv env
 
-def getNGen : MetaM NameGenerator :=
-liftCoreM Core.getNGen
+def getNGen {ε} : EMetaM ε NameGenerator :=
+liftECoreM Core.getNGen
 
-def setNGen (ngen : NameGenerator) : MetaM Unit :=
-liftCoreM $ Core.setNGen ngen
+def setNGen {ε} (ngen : NameGenerator) : EMetaM ε Unit :=
+liftECoreM $ Core.setNGen ngen
 
-def getTraceState : MetaM TraceState :=
-liftCoreM $ Core.getTraceState
+def getTraceState {ε}  : EMetaM ε TraceState :=
+liftECoreM $ Core.getTraceState
 
-def setTraceState (traceState : TraceState) : MetaM Unit :=
-liftCoreM $ Core.setTraceState traceState
+def setTraceState {ε} (traceState : TraceState) : EMetaM ε Unit :=
+liftECoreM $ Core.setTraceState traceState
 
 def mkWHNFRef : IO (IO.Ref (Expr → MetaM Expr)) :=
 IO.mkRef $ fun _ => throwError "whnf implementation was not set"
@@ -241,33 +247,33 @@ withIncRecDepth do
   fn ← liftIO synthPendingRef.get;
   fn mvarId
 
-def mkFreshId : MetaM Name := do
-liftCoreM Core.mkFreshId
+def mkFreshId {ε} : EMetaM ε Name := do
+liftECoreM Core.mkFreshId
 
-private def mkFreshExprMVarAtCore
-    (mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name) (kind : MetavarKind) : MetaM Expr := do
+private def mkFreshExprMVarAtCore {ε}
+    (mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name) (kind : MetavarKind) : EMetaM ε Expr := do
 modify $ fun s => { s with mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type kind };
 pure $ mkMVar mvarId
 
-def mkFreshExprMVarAt
+def mkFreshExprMVarAt {ε}
     (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural)
-    : MetaM Expr := do
+    : EMetaM ε Expr := do
 mvarId ← mkFreshId;
 mkFreshExprMVarAtCore mvarId lctx localInsts type userName kind
 
-def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
+def mkFreshExprMVar {ε} (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : EMetaM ε Expr := do
 lctx ← getLCtx;
 localInsts ← getLocalInstances;
 mkFreshExprMVarAt lctx localInsts type userName kind
 
 /- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create
    the metavar using this method. -/
-def mkFreshExprMVarWithId (mvarId : MVarId) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
+def mkFreshExprMVarWithId {ε} (mvarId : MVarId) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : EMetaM ε Expr := do
 lctx ← getLCtx;
 localInsts ← getLocalInstances;
 mkFreshExprMVarAtCore mvarId lctx localInsts type userName kind
 
-def mkFreshLevelMVar : MetaM Level := do
+def mkFreshLevelMVar {ε} : EMetaM ε Level := do
 mvarId ← mkFreshId;
 modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
 pure $ mkLevelMVar mvarId
@@ -284,31 +290,31 @@ match x with
 | Except.ok a    => pure a
 | Except.error e => throwError (toString e)
 
-@[inline] def shouldReduceAll : MetaM Bool := do
+@[inline] def shouldReduceAll {ε} : EMetaM ε Bool := do
 ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all
 
-@[inline] def shouldReduceReducibleOnly : MetaM Bool := do
+@[inline] def shouldReduceReducibleOnly {ε} : EMetaM ε Bool := do
 ctx ← read; pure $ ctx.config.transparency == TransparencyMode.reducible
 
-@[inline] def getTransparency : MetaM TransparencyMode := do
+@[inline] def getTransparency {ε} : EMetaM ε TransparencyMode := do
 ctx ← read; pure $ ctx.config.transparency
 
 -- Remark: wanted to use `private`, but in C++ parser, `private` declarations do not shadow outer public ones.
 -- TODO: fix this bug
-@[inline] def isReducible (constName : Name) : MetaM Bool := do
+@[inline] def isReducible {ε} (constName : Name) : EMetaM ε Bool := do
 env ← getEnv; pure $ isReducible env constName
 
-@[inline] def withConfig {α} (f : Config → Config) (x : MetaM α) : MetaM α :=
+@[inline] def withConfig {ε α} (f : Config → Config) (x : EMetaM ε α) : EMetaM ε α :=
 adaptReader (fun (ctx : Context) => { ctx with config := f ctx.config }) x
 
 /-- While executing `x`, ensure the given transparency mode is used. -/
-@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
+@[inline] def withTransparency {ε α} (mode : TransparencyMode) (x : EMetaM ε α) : EMetaM ε α :=
 withConfig (fun config => { config with transparency := mode }) x
 
-@[inline] def withReducible {α} (x : MetaM α) : MetaM α :=
+@[inline] def withReducible {ε α} (x : EMetaM ε α) : EMetaM ε α :=
 withTransparency TransparencyMode.reducible x
 
-@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
+@[inline] def withAtLeastTransparency {ε α} (mode : TransparencyMode) (x : EMetaM ε α) : EMetaM ε α :=
 withConfig
   (fun config =>
     let oldMode := config.transparency;
@@ -344,34 +350,31 @@ match mctx.findLevelDepth? mvarId with
 | some depth => pure $ depth != mctx.depth
 | _          => throwError ("unknown universe metavariable '" ++ mkLevelMVar mvarId ++ "'")
 
-def renameMVar (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
+def renameMVar {ε} (mvarId : MVarId) (newUserName : Name) : EMetaM ε Unit :=
 modify $ fun s => { s with mctx := s.mctx.renameMVar mvarId newUserName }
 
-@[inline] def isExprMVarAssigned (mvarId : MVarId) : MetaM Bool := do
+@[inline] def isExprMVarAssigned {ε} (mvarId : MVarId) : EMetaM ε Bool := do
 mctx ← getMCtx;
 pure $ mctx.isExprAssigned mvarId
 
-@[inline] def getExprMVarAssignment? (mvarId : MVarId) : MetaM (Option Expr) := do
+@[inline] def getExprMVarAssignment? {ε} (mvarId : MVarId) : EMetaM ε (Option Expr) := do
 mctx ← getMCtx; pure (mctx.getExprAssignment? mvarId)
 
-def assignExprMVar (mvarId : MVarId) (val : Expr) : MetaM Unit := do
+def assignExprMVar {ε} (mvarId : MVarId) (val : Expr) : EMetaM ε Unit := do
 modify $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
 
-def isDelayedAssigned (mvarId : MVarId) : MetaM Bool := do
+def isDelayedAssigned {ε} (mvarId : MVarId) : EMetaM ε Bool := do
 mctx ← getMCtx;
 pure $ mctx.isDelayedAssigned mvarId
 
-def hasAssignableMVar (e : Expr) : MetaM Bool := do
+def hasAssignableMVar {ε} (e : Expr) : EMetaM ε Bool := do
 mctx ← getMCtx;
 pure $ mctx.hasAssignableMVar e
 
-def dbgTrace {α} [HasToString α] (a : α) : MetaM Unit :=
-_root_.dbgTrace (toString a) $ fun _ => pure ()
-
 def throwUnknownConstant {α} (constName : Name) : MetaM α :=
 throwError ("unknown constant '" ++ constName ++ "'")
 
-def getConstAux (constName : Name) (exception? : Bool) : MetaM (Option ConstantInfo) := do
+def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
 env ← getEnv;
 match env.find? constName with
 | some (info@(ConstantInfo.thmInfo _)) =>
@@ -381,15 +384,7 @@ match env.find? constName with
     (condM (isReducible constName) (pure (some info)) (pure none))
     (pure (some info))
 | some info => pure (some info)
-| none                                 =>
-  if exception? then throwUnknownConstant constName
-  else pure none
-
-@[inline] def getConst (constName : Name) : MetaM (Option ConstantInfo) :=
-getConstAux constName true
-
-@[inline] def getConstNoEx (constName : Name) : MetaM (Option ConstantInfo) :=
-getConstAux constName false
+| none      => throwUnknownConstant constName
 
 def getConstInfo (constName : Name) : MetaM ConstantInfo := do
 env ← getEnv;
@@ -397,6 +392,18 @@ match env.find? constName with
 | some info => pure info
 | none      => throwUnknownConstant constName
 
+def getConstNoEx? {ε} (constName : Name) : EMetaM ε (Option ConstantInfo) := do
+env ← getEnv;
+match env.find? constName with
+| some (info@(ConstantInfo.thmInfo _)) =>
+  condM shouldReduceAll (pure (some info)) (pure none)
+| some (info@(ConstantInfo.defnInfo _)) =>
+  condM shouldReduceReducibleOnly
+    (condM (isReducible constName) (pure (some info)) (pure none))
+    (pure (some info))
+| some info => pure (some info)
+| none      => pure none
+
 def throwUnknownFVar {α} (fvarId : FVarId) : MetaM α :=
 throwError ("unknown free variable '" ++ mkFVar fvarId ++ "'")
 
@@ -409,7 +416,7 @@ match lctx.find? fvarId with
 def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl :=
 getLocalDecl fvar.fvarId!
 
-def instantiateMVars (e : Expr) : MetaM Expr :=
+def instantiateMVars {ε} (e : Expr) : EMetaM ε Expr :=
 if e.hasMVar then
   modifyGet $ fun s =>
     let (e, mctx) := s.mctx.instantiateMVars e;
@@ -417,7 +424,7 @@ if e.hasMVar then
 else
   pure e
 
-def instantiateLocalDeclMVars (localDecl : LocalDecl) : MetaM LocalDecl :=
+def instantiateLocalDeclMVars {ε} (localDecl : LocalDecl) : EMetaM ε LocalDecl :=
 match localDecl with
   | LocalDecl.cdecl idx id n type bi  => do
     type ← instantiateMVars type;
@@ -454,22 +461,22 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.elimMVarDeps xs e preserveOrder
 
 /-- Save cache, execute `x`, restore cache -/
-@[inline] def savingCache {α} (x : MetaM α) : MetaM α := do
+@[inline] def savingCache {ε α} (x : EMetaM ε α) : EMetaM ε α := do
 s ← get;
 let savedCache := s.cache;
 finally x (modify $ fun s => { s with cache := savedCache })
 
-def isClassQuickConst (constName : Name) : MetaM (LOption Name) := do
+def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do
 env ← getEnv;
 if isClass env constName then
   pure (LOption.some constName)
 else do
-  cinfo? ← getConst constName;
+  cinfo? ← getConst? constName;
   match cinfo? with
   | some _ => pure LOption.undef
   | none   => pure LOption.none
 
-partial def isClassQuick : Expr → MetaM (LOption Name)
+partial def isClassQuick? : Expr → MetaM (LOption Name)
 | Expr.bvar _ _        => pure LOption.none
 | Expr.lit _ _         => pure LOption.none
 | Expr.fvar _ _        => pure LOption.none
@@ -477,39 +484,39 @@ partial def isClassQuick : Expr → MetaM (LOption Name)
 | Expr.lam _ _ _ _     => pure LOption.none
 | Expr.letE _ _ _ _ _  => pure LOption.undef
 | Expr.proj _ _ _  _   => pure LOption.undef
-| Expr.forallE _ _ b _ => isClassQuick b
-| Expr.mdata _ e _     => isClassQuick e
-| Expr.const n _ _     => isClassQuickConst n
+| Expr.forallE _ _ b _ => isClassQuick? b
+| Expr.mdata _ e _     => isClassQuick? e
+| Expr.const n _ _     => isClassQuickConst? n
 | Expr.mvar mvarId _   => do
   val? ← getExprMVarAssignment? mvarId;
   match val? with
-  | some val => isClassQuick val
+  | some val => isClassQuick? val
   | none     => pure LOption.none
 | Expr.app f _ _       =>
   match f.getAppFn with
-  | Expr.const n _ _  => isClassQuickConst n
+  | Expr.const n _ _  => isClassQuickConst? n
   | Expr.lam _ _ _ _  => pure LOption.undef
   | _                 => pure LOption.none
 | Expr.localE _ _ _ _ => unreachable!
 
-def saveAndResetSynthInstanceCache : MetaM SynthInstanceCache := do
+def saveAndResetSynthInstanceCache {ε} : EMetaM ε SynthInstanceCache := do
 s ← get;
 let savedSythInstance := s.cache.synthInstance;
 modify $ fun s => { s with cache := { s.cache with synthInstance := {} } };
 pure savedSythInstance
 
-def restoreSynthInstanceCache (cache : SynthInstanceCache) : MetaM Unit :=
+def restoreSynthInstanceCache {ε} (cache : SynthInstanceCache) : EMetaM ε Unit :=
 modify $ fun s => { s with cache := { s.cache with synthInstance := cache } }
 
 /-- Reset `synthInstance` cache, execute `x`, and restore cache -/
-@[inline] def resettingSynthInstanceCache {α} (x : MetaM α) : MetaM α := do
+@[inline] def resettingSynthInstanceCache {ε α} (x : EMetaM ε α) : EMetaM ε α := do
 savedSythInstance ← saveAndResetSynthInstanceCache;
 finally x (restoreSynthInstanceCache savedSythInstance)
 
 /-- Add entry `{ className := className, fvar := fvar }` to localInstances,
     and then execute continuation `k`.
     It resets the type class cache using `resettingSynthInstanceCache`. -/
-@[inline] def withNewLocalInstance {α} (className : Name) (fvar : Expr) (k : MetaM α) : MetaM α :=
+@[inline] def withNewLocalInstance {ε α} (className : Name) (fvar : Expr) (k : EMetaM ε α) : EMetaM ε α :=
 resettingSynthInstanceCache $
   adaptReader
     (fun (ctx : Context) => { ctx with localInstances := ctx.localInstances.push { className := className, fvar := fvar } })
@@ -524,17 +531,17 @@ resettingSynthInstanceCache $
   - `isClassExpensive` uses `whnf` which depends (indirectly) on the set of local instances.
     Thus, each new local instance requires a new `resettingSynthInstanceCache`. -/
 @[specialize] partial def withNewLocalInstances {α}
-    (isClassExpensive : Expr → MetaM (Option Name))
+    (isClassExpensive? : Expr → MetaM (Option Name))
     (fvars : Array Expr) : Nat → MetaM α → MetaM α
 | i, k =>
   if h : i < fvars.size then do
     let fvar := fvars.get ⟨i, h⟩;
     decl ← getFVarLocalDecl fvar;
-    c?   ← isClassQuick decl.type;
+    c?   ← isClassQuick? decl.type;
     match c? with
     | LOption.none   => withNewLocalInstances (i+1) k
     | LOption.undef  => do
-      c? ← isClassExpensive decl.type;
+      c? ← isClassExpensive? decl.type;
       match c? with
       | none   => withNewLocalInstances (i+1) k
       | some c => withNewLocalInstance c fvar $ withNewLocalInstances (i+1) k
@@ -568,9 +575,9 @@ resettingSynthInstanceCache $
   when `fvars.size == max`
 -/
 @[specialize] private partial def forallTelescopeReducingAuxAux {α}
-    (isClassExpensive : Expr → MetaM (Option Name))
-    (reducing?        : Bool) (maxFVars? : Option Nat)
-    (k                : Array Expr → Expr → MetaM α)
+    (isClassExpensive? : Expr → MetaM (Option Name))
+    (reducing?         : Bool) (maxFVars? : Option Nat)
+    (k                 : Array Expr → Expr → MetaM α)
     : LocalContext → Array Expr → Nat → Expr → MetaM α
 | lctx, fvars, j, type@(Expr.forallE n d b c) => do
   let process : Unit → MetaM α := fun _ => do {
@@ -589,12 +596,12 @@ resettingSynthInstanceCache $
     else
       let type := type.instantiateRevRange j fvars.size fvars;
       adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
-        withNewLocalInstances isClassExpensive fvars j $
+        withNewLocalInstances isClassExpensive? fvars j $
           k fvars type
 | lctx, fvars, j, type =>
   let type := type.instantiateRevRange j fvars.size fvars;
   adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
-    withNewLocalInstances isClassExpensive fvars j $
+    withNewLocalInstances isClassExpensive? fvars j $
       if reducing? then do
         newType ← whnf type;
         if newType.isForall then
@@ -607,18 +614,18 @@ resettingSynthInstanceCache $
 /- We need this auxiliary definition because it depends on `isClassExpensive`,
    and `isClassExpensive` depends on it. -/
 @[specialize] private def forallTelescopeReducingAux {α}
-    (isClassExpensive : Expr → MetaM (Option Name))
+    (isClassExpensive? : Expr → MetaM (Option Name))
     (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α := do
 newType ← whnf type;
 if newType.isForall then do
   lctx ← getLCtx;
-  forallTelescopeReducingAuxAux isClassExpensive true maxFVars? k lctx #[] 0 newType
+  forallTelescopeReducingAuxAux isClassExpensive? true maxFVars? k lctx #[] 0 newType
 else
   k #[] type
 
-partial def isClassExpensive : Expr → MetaM (Option Name)
+partial def isClassExpensive? : Expr → MetaM (Option Name)
 | type => withReducible $ -- when testing whether a type is a type class, we only unfold reducible constants.
-  forallTelescopeReducingAux isClassExpensive type none $ fun xs type => do
+  forallTelescopeReducingAux isClassExpensive? type none $ fun xs type => do
     match type.getAppFn with
     | Expr.const c _ _ => do
       env ← getEnv;
@@ -631,19 +638,19 @@ partial def isClassExpensive : Expr → MetaM (Option Name)
   execute `k` with updated local context, and make sure the cache is restored after executing `k`. -/
 def forallTelescope {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α := do
 lctx ← getLCtx;
-forallTelescopeReducingAuxAux isClassExpensive false none k lctx #[] 0 type
+forallTelescopeReducingAuxAux isClassExpensive? false none k lctx #[] 0 type
 
 /--
   Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
   it reduces `A` and continues bulding the telescope if it is a `forall`. -/
 def forallTelescopeReducing {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
-forallTelescopeReducingAux isClassExpensive type none k
+forallTelescopeReducingAux isClassExpensive? type none k
 
 /--
   Similar to `forallTelescopeReducing`, stops constructing the telescope when
   it reaches size `maxFVars`. -/
 def forallBoundedTelescope {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
-forallTelescopeReducingAux isClassExpensive type maxFVars? k
+forallTelescopeReducingAux isClassExpensive? type maxFVars? k
 
 /-- Return the parameter names for the givel global declaration. -/
 def getParamNames (declName : Name) : MetaM (Array Name) := do
@@ -653,12 +660,12 @@ forallTelescopeReducing cinfo.type $ fun xs _ => do
     localDecl ← getLocalDecl x.fvarId!;
     pure localDecl.userName
 
-def isClass (type : Expr) : MetaM (Option Name) := do
-c? ← isClassQuick type;
+def isClass? (type : Expr) : MetaM (Option Name) := do
+c? ← isClassQuick? type;
 match c? with
 | LOption.none   => pure none
 | LOption.some c => pure (some c)
-| LOption.undef  => isClassExpensive type
+| LOption.undef  => isClassExpensive? type
 
 /-- Similar to `forallTelescopeAuxAux` but for lambda and let expressions. -/
 private partial def lambdaTelescopeAux {α}
@@ -680,7 +687,7 @@ private partial def lambdaTelescopeAux {α}
 | lctx, fvars, j, e =>
   let e := e.instantiateRevRange j fvars.size fvars;
   adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
-    withNewLocalInstances isClassExpensive fvars j $ do
+    withNewLocalInstances isClassExpensive? fvars j $ do
       k fvars e
 
 /-- Similar to `forallTelescope` but for lambda and let expressions. -/
@@ -795,7 +802,7 @@ adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApp
   x
 
 @[inline] private def withNewFVar {α} (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
-c? ← isClass fvarType;
+c? ← isClass? fvarType;
 match c? with
 | none   => k fvar
 | some c => withNewLocalInstance c fvar $ k fvar
@@ -826,7 +833,7 @@ let lctx := decls.foldl (fun (lctx : LocalContext) decl => lctx.addDecl decl) ct
 adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) do
   newLocalInsts ← decls.foldlM
     (fun (newlocalInsts : Array LocalInstance) (decl : LocalDecl) => do
-      c? ← isClass decl.type;
+      c? ← isClass? decl.type;
       match c? with
       | none   => pure newlocalInsts
       | some c => pure $ newlocalInsts.push { className := c, fvar := decl.toExpr })
@@ -912,7 +919,10 @@ instantiateForallAux ps 0 e
 registerTraceClass `Meta;
 registerTraceClass `Meta.debug
 
-@[inline] private abbrev runAux {α} (x : ECoreM Exception α) : CoreM α := do
+@[inline] def EMetaM.run {ε α} (x : EMetaM ε α) (ctx : Context := {}) (s : State := {}) : ECoreM ε (α × State) :=
+(x.run ctx).run s
+
+@[inline] private def toCoreMAux {α} (x : ECoreM Exception α) : CoreM α := do
 ref ← Core.getRef;
 adaptExcept
   (fun ex => match ex with
@@ -920,21 +930,15 @@ adaptExcept
   | ex => Core.Exception.error ref ex.toMessageData)
   x
 
-@[inline] def MetaM.toECoreM {α} (x : MetaM α) : ECoreM Exception α :=
-(x.run {}).run' {}
+@[inline] def MetaM.toCoreM {α} (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM (α × State) :=
+toCoreMAux $ x.run ctx s
 
-@[inline] def MetaM.run {α} (x : MetaM α) : CoreM α := do
-runAux $ x.toECoreM
-
-@[inline] def MetaM.toIO {α} (x : MetaM α) (env : Environment) (options : Options := {}) : IO α :=
-(x.run).run env options
-
-def printTraces : MetaM Unit := do
-s ← getTraceState;
-s.traces.forM fun msg _ => IO.println (toString msg)
+@[inline] def MetaM.toIO {α} (x : MetaM α) (ctxCore : Core.Context) (sCore : Core.State) (ctx : Context := {}) (s : State := {}) : IO (α × Core.State × State) := do
+((a, s), sCore) ← (toCoreMAux (x.run ctx s)).toIO ctxCore sCore;
+pure (a, sCore, s)
 
 instance hasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
-⟨fun env opts x _ => MetaHasEval.eval env opts x.run⟩
+⟨fun env opts x _ => MetaHasEval.eval env opts (do (a, _) ← x.toCoreM {} {}; pure a)⟩
 
 end Meta
 
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 512c19ff71..e7902f64d2 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -191,7 +191,7 @@ else
     let fvarType := fvarDecl.type;
     let d₂       := ds₂.get! i;
     condM (isExprDefEqAux fvarType d₂)
-      (do c? ← isClass fvarType;
+      (do c? ← isClass? fvarType;
           match c? with
           | some className => withNewLocalInstance className fvar $ isDefEqBindingDomain (i+1) k
           | none           => isDefEqBindingDomain (i+1) k)
@@ -709,9 +709,9 @@ traceCtx `Meta.isDefEq.assign $ do
   mvarDecl ← getMVarDecl mvar.mvarId!;
   processAssignmentAux mvar mvarDecl 0 mvarApp.getAppArgs v
 
-private def isDeltaCandidate (t : Expr) : MetaM (Option ConstantInfo) :=
+private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) :=
 match t.getAppFn with
-| Expr.const c _ _ => getConst c
+| Expr.const c _ _ => getConst? c
 | _                => pure none
 
 /-- Auxiliary method for isDefEqDelta -/
@@ -872,8 +872,8 @@ else
   11- Otherwise, unfold `t` and `s` and continue.
   Remark: 9&10&11 are implemented by `unfoldComparingHeadsDefEq` -/
 private def isDefEqDelta (t s : Expr) : MetaM LBool := do
-tInfo? ← isDeltaCandidate t.getAppFn;
-sInfo? ← isDeltaCandidate s.getAppFn;
+tInfo? ← isDeltaCandidate? t.getAppFn;
+sInfo? ← isDeltaCandidate? s.getAppFn;
 match tInfo?, sInfo? with
 | none,       none       => pure LBool.undef
 | some tInfo, none       => unfold t (pure LBool.undef) $ fun t => isDefEqLeft tInfo.name t s
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index 8815092e40..6bd1edd493 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -39,8 +39,8 @@ match env.find? constName with
 | none => throw $ IO.userError "unknown constant"
 | some cinfo => do
   let c := mkConst constName (cinfo.lparams.map mkLevelParam);
-  (env, keys) ← ((mkInstanceKey c).run).run' env;
-  pure $ instanceExtension.addEntry env { keys := keys, val := c }
+  (keys, s, _) ← (mkInstanceKey c).toIO {} { env := env } {} {};
+  pure $ instanceExtension.addEntry s.env { keys := keys, val := c }
 
 @[init] def registerInstanceAttr : IO Unit :=
 registerBuiltinAttribute {
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index bcec901657..227fc7dc05 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -291,7 +291,9 @@ match cinfo with
 def mkRecursorAttr : IO (ParametricAttribute Nat) :=
 registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
   (fun _ stx => Core.ofExcept $ syntaxToMajorPos stx)
-  (fun declName majorPos => do _ ← (mkRecursorInfoCore declName (some majorPos)).run; pure ())
+  (fun declName majorPos => do
+    _ ← (mkRecursorInfoCore declName (some majorPos)).toCoreM {} {};
+    pure ())
 
 @[init mkRecursorAttr] constant recursorAttribute : ParametricAttribute Nat := arbitrary _
 
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 8f35b2e6d7..250acb4f8f 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -157,20 +157,19 @@ abbrev SynthM := StateRefT State MetaM
 @[inline] def liftMetaM {α} (x : MetaM α) : SynthM α :=
 liftM x
 
-instance meta2Synth {α} : HasCoe (MetaM α) (SynthM α) := ⟨liftMetaM⟩
+@[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
+monadMap @f
 
 instance SynthM.inhabited {α} : Inhabited (SynthM α) :=
 ⟨fun _ => arbitrary _⟩
 
-@[inline] def withMCtx {α} (mctx : MetavarContext) (x : SynthM α) : SynthM α := do
-mctx' ← getMCtx;
-setMCtx mctx;
-finally x (setMCtx mctx')
+@[inline] def withMCtx {α} (mctx : MetavarContext) (x : SynthM α) : SynthM α :=
+mapMetaM (fun α => Meta.withMCtx mctx) x
 
 /-- Return globals and locals instances that may unify with `type` -/
 def getInstances (type : Expr) : MetaM (Array Expr) :=
 forallTelescopeReducing type $ fun _ type => do
-  className? ← isClass type;
+  className? ← isClass? type;
   match className? with
   | none   => throwError $ "type class instance expected" ++ indentExpr type
   | some className => do
@@ -186,24 +185,30 @@ forallTelescopeReducing type $ fun _ type => do
       result;
     pure result
 
+def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do
+mvarType  ← inferType mvar;
+mvarType  ← instantiateMVars mvarType;
+instances ← getInstances mvarType;
+if instances.isEmpty then pure none
+else do
+  mctx ← getMCtx;
+  pure $ some {
+    mvar            := mvar,
+    key             := key,
+    mctx            := mctx,
+    instances       := instances,
+    currInstanceIdx := instances.size
+  }
+
 /-- Create a new generator node for `mvar` and add `waiter` as its waiter.
     `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;
-  mvarType  ← inferType mvar;
-  mvarType  ← instantiateMVars mvarType;
-  instances ← getInstances mvarType;
-  mctx      ← getMCtx;
-  if instances.isEmpty then pure ()
-  else do
-    let node : GeneratorNode := {
-      mvar            := mvar,
-      key             := key,
-      mctx            := mctx,
-      instances       := instances,
-      currInstanceIdx := instances.size
-    };
+  node? ← liftMetaM $ mkGeneratorNode? key mvar;
+  match node? with
+  | none      => pure ()
+  | some node =>
     let entry : TableEntry := { waiters := #[waiter] };
     modify $ fun s =>
      { s with
@@ -227,8 +232,8 @@ match entry? with
   We must instantiate assigned metavariables before we invoke `mkTableKey`. -/
 def mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) : SynthM Expr :=
 withMCtx mctx $ do
-  mvarType ← inferType mvar;
-  mvarType ← instantiateMVars mvarType;
+  mvarType ← liftMetaM $ inferType mvar;
+  mvarType ← liftMetaM $ instantiateMVars mvarType;
   pure $ mkTableKey mctx mvarType
 
 /- See `getSubgoals` and `getSubgoalsAux`
@@ -312,13 +317,13 @@ forallTelescopeReducing mvarType $ fun xs mvarTypeBody => do
   If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
   A subgoal is created for each instance implicit parameter of `inst`. -/
 def tryResolve (mctx : MetavarContext) (mvar : Expr) (inst : Expr) : SynthM (Option (MetavarContext × List Expr)) :=
-traceCtx `Meta.synthInstance.tryResolve $ withMCtx mctx $ tryResolveCore mvar inst
+liftMetaM $ traceCtx `Meta.synthInstance.tryResolve $ Meta.withMCtx mctx $ tryResolveCore mvar inst
 
 /--
   Assign a precomputed answer to `mvar`.
   If it succeeds, the result is a new updated metavariable context and a new list of subgoals. -/
 def tryAnswer (mctx : MetavarContext) (mvar : Expr) (answer : Answer) : SynthM (Option MetavarContext) :=
-withMCtx mctx $ do
+liftMetaM $ Meta.withMCtx mctx $ do
   (_, _, val) ← openAbstractMVarsResult answer.result;
   condM (isDefEq mvar val)
     (do mctx ← getMCtx; pure $ some mctx)
@@ -330,7 +335,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
   if answer.result.paramNames.isEmpty && answer.result.numMVars == 0 then do
     modify $ fun s => { s with result := answer.result.expr }
   else do
-    (_, _, answerExpr) ← openAbstractMVarsResult answer.result;
+    (_, _, answerExpr) ← liftMetaM $ openAbstractMVarsResult answer.result;
     trace! `Meta.synthInstance ("skip answer containing metavariables " ++ answerExpr);
     pure ()
 | Waiter.consumerNode cNode => modify $ fun s => { s with resumeStack := s.resumeStack.push (cNode, answer) }
@@ -341,18 +346,20 @@ oldAnswers.all $ fun oldAnswer => do
   -- iseq ← isDefEq oldAnswer.resultType answer.resultType; pure (!iseq)
   oldAnswer.resultType != answer.resultType
 
+private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
+Meta.withMCtx cNode.mctx do
+  traceM `Meta.synthInstance.newAnswer $ do { mvarType ← inferType cNode.mvar; pure mvarType };
+  val ← instantiateMVars cNode.mvar;
+  result ← abstractMVars val; -- assignable metavariables become parameters
+  resultType ← inferType result.expr;
+  pure { result := result, resultType := resultType }
+
 /--
   Create a new answer after `cNode` resolved all subgoals.
   That is, `cNode.subgoals == []`.
   And then, store it in the tabled entries map, and wakeup waiters. -/
 def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
-answer ← withMCtx cNode.mctx $ do {
-  traceM `Meta.synthInstance.newAnswer $ do { mvarType ← inferType cNode.mvar; pure mvarType };
-  val ← instantiateMVars cNode.mvar;
-  result ← abstractMVars val; -- assignable metavariables become parameters
-  resultType ← inferType result.expr;
-  pure { result := result, resultType := resultType : Answer }
-};
+answer ← liftMetaM $ mkAnswer cNode;
 -- Remark: `answer` does not contain assignable or assigned metavariables.
 let key := cNode.key;
 entry ← getEntry key;
@@ -418,7 +425,7 @@ match cNode.subgoals with
   match result? with
   | none      => pure ()
   | some mctx => do
-    withMCtx mctx $ traceM `Meta.synthInstance.resume $ do {
+    liftMetaM $ Meta.withMCtx mctx $ traceM `Meta.synthInstance.resume $ do {
       goal    ← inferType cNode.mvar;
       subgoal ← inferType mvar;
       pure (goal ++ " <== " ++ subgoal)
@@ -590,7 +597,7 @@ def synthPendingImp (mvarId : MVarId) : MetaM Bool := do
 mvarDecl ← getMVarDecl mvarId;
 match mvarDecl.kind with
 | MetavarKind.synthetic => do
-  c? ← isClass mvarDecl.type;
+  c? ← isClass? mvarDecl.type;
   match c? with
   | none   => pure false
   | some _ => do
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index 992b486a9b..3f003be6d1 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/src/Lean/Meta/Tactic/Intro.lean
@@ -14,7 +14,7 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
 | 0, lctx, fvars, j, _, type =>
   let type := type.instantiateRevRange j fvars.size fvars;
   adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
-    withNewLocalInstances isClassExpensive fvars j $ do
+    withNewLocalInstances isClassExpensive? fvars j $ do
       tag     ← getMVarTag mvarId;
       let type := type.headBeta;
       newMVar ← mkFreshExprSyntheticOpaqueMVar type tag;
@@ -44,7 +44,7 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
 | (i+1), lctx, fvars, j, s, type =>
   let type := type.instantiateRevRange j fvars.size fvars;
   adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
-    withNewLocalInstances isClassExpensive fvars j $ do
+    withNewLocalInstances isClassExpensive? fvars j $ do
       newType ← whnf type;
       if newType.isForall then
         introNCoreAux i lctx fvars fvars.size s newType
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 9a0f1774a5..90184079e9 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -15,10 +15,10 @@ def isAuxDef? (constName : Name) : MetaM Bool := do
 env ← getEnv; pure (isAuxRecursor env constName || isNoConfusion env constName)
 
 def unfoldDefinition? (e : Expr) : MetaM (Option Expr)  :=
-Lean.WHNF.unfoldDefinitionAux getConstNoEx isAuxDef? whnf inferType isExprDefEq synthPending getLocalDecl getExprMVarAssignment? e
+Lean.WHNF.unfoldDefinitionAux getConstNoEx? isAuxDef? whnf inferType isExprDefEq synthPending getLocalDecl getExprMVarAssignment? e
 
 def whnfCore (e : Expr) : MetaM Expr :=
-Lean.WHNF.whnfCore getConstNoEx isAuxDef? whnf inferType isExprDefEqAux getLocalDecl getExprMVarAssignment? e
+Lean.WHNF.whnfCore getConstNoEx? isAuxDef? whnf inferType isExprDefEqAux getLocalDecl getExprMVarAssignment? e
 
 unsafe def reduceNativeConst (α : Type) (typeName : Name) (constName : Name) : MetaM α := do
 env ← getEnv;
@@ -173,7 +173,7 @@ if e.isAppOf declName then pure e
 else pure none
 
 def getStuckMVar? (e : Expr) : MetaM (Option MVarId) :=
-WHNF.getStuckMVar? getConst whnf e
+WHNF.getStuckMVar? getConst? whnf e
 
 end Meta
 end Lean
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 9a8b8c4108..e621476736 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -261,7 +261,7 @@ es.foldlM
          p ← IO.ofExcept $ mkParserOfConstant env s.categories declName;
          categories ← IO.ofExcept $ addParser s.categories catName declName p.1 p.2;
          -- discard result env; all environment side effects should already have happened when the parser was declared initially
-         (runParserAttributeHooks catName declName /- builtin -/ false).run env;
+         _ ← (runParserAttributeHooks catName declName /- builtin -/ false).toIO {} { env := env };
          pure { s with categories := categories })
       s)
   s
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index f5bf8a8362..30b3b50861 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -101,7 +101,7 @@ def compileParser {α} (ctx : Context α) (declName : Name) (builtin : Bool) : C
 -- Note that simply having `[(builtin)Parenthesizer]` imply `[combinatorParenthesizer]` is not ideal since builtin
 -- attributes are active only in the next stage, while `[combinatorParenthesizer]` is active immediately (since we never
 -- call them at compile time but only reference them).
-(Expr.const c' _ _) ← (compileParserBody ctx (mkConst declName)).run
+(Expr.const c' _ _, _) ← (compileParserBody ctx (mkConst declName)).toCoreM
   | unreachable!;
 -- We assume that for tagged parsers, the kind is equal to the declaration name. This is automatically true for parsers
 -- using `parser!` or `syntax`.
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index af04035737..5d9aaf759d 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -39,12 +39,9 @@ abbrev PPExprFn := Environment → MetavarContext → LocalContext → Options 
 ```
 -/
 unsafe def ppExprFnUnsafe (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : Format :=
-let x : MetaM Format := do { Meta.setMCtx mctx; ppExpr e };
-let x : MetaM Format := adaptReader (fun (ctx : Meta.Context) => { ctx with lctx := lctx }) x;
-let x : IO Format    := (x.run).run env opts;
-match unsafeIO x with
-| Except.ok  fmt => fmt
-| Except.error e => "<pretty printer error: " ++ toString e ++ ">"
+match unsafeIO $ (ppExpr e).toIO { options := opts } { env := env } { lctx := lctx } { mctx := mctx }  with
+| Except.ok  (fmt, _, _) => fmt
+| Except.error e         => "<pretty printer error: " ++ toString e ++ ">"
 
 @[implementedBy ppExprFnUnsafe]
 constant ppExprFn (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : Format := arbitrary _
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 51973ed1a6..c61eed8024 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -121,6 +121,15 @@ fold (Array.foldl (fun acc f => f ++ acc) Format.nil) x
 def concatArgs (x : FormatterM Unit) : FormatterM Unit :=
 concat (visitArgs x)
 
+@[inline] def liftCoreM {α} (x : CoreM α) : FormatterM α :=
+liftM x
+
+def getEnv : FormatterM Environment :=
+liftCoreM Core.getEnv
+
+def throwError {α} (msg : MessageData) : FormatterM α :=
+liftCoreM $ Core.throwError msg
+
 /-
 /--
   Call an appropriate `[formatter]` depending on the `Parser` `Expr` `p`. After the call, the traverser position
@@ -181,9 +190,9 @@ constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (a
 arbitrary _
 
 def formatterForKind (k : SyntaxNodeKind) : Formatter := do
-env ← liftM getEnv;
+env ← getEnv;
 p::_ ← pure $ formatterAttribute.getValues env k
-  | liftM $ throwError $ "no known formatter for kind '" ++ k ++ "'";
+  | throwError $ "no known formatter for kind '" ++ k ++ "'";
 p
 
 @[combinatorFormatter Lean.Parser.withAntiquot]
@@ -250,7 +259,7 @@ concatArgs do
 
 def parseToken (s : String) : FormatterM ParserState := do
 ctx ← read;
-env ← liftM getEnv;
+env ← getEnv;
 pure $ Parser.tokenFn { input := s, fileName := "", fileMap := FileMap.ofString "", prec := 0, env := env, tokens := ctx.table } (Parser.mkParserState s)
 
 def pushToken (tk : String) : FormatterM Unit := do
@@ -285,7 +294,7 @@ goLeft
 def unicodeSymbol.formatter (sym asciiSym : String) : Formatter := do
 stx ← getCur;
 Syntax.atom _ val ← pure stx
-  | liftM $ throwError $ "not an atom: " ++ toString stx;
+  | throwError $ "not an atom: " ++ toString stx;
 if val == sym.trim then
   pushToken sym
 else
@@ -318,7 +327,7 @@ stx ← getCur;
 when (k != Name.anonymous) $
   checkKind k;
 Syntax.atom _ val ← pure $ stx.ifNode (fun n => n.getArg 0) (fun _ => stx)
-  | liftM $ throwError $ "not an atom: " ++ toString stx;
+  | throwError $ "not an atom: " ++ toString stx;
 pushToken val;
 goLeft
 
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index f619e1afe3..0bc7ab17b2 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -244,10 +244,19 @@ p1 <|> p2
 constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer :=
 arbitrary _
 
+@[inline] def liftCoreM {α} (x : CoreM α) : ParenthesizerM α :=
+liftM x
+
+def getEnv : ParenthesizerM Environment :=
+liftCoreM Core.getEnv
+
+def throwError {α} (msg : MessageData) : ParenthesizerM α :=
+liftCoreM $ Core.throwError msg
+
 def parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer := do
-env ← liftM getEnv;
+env ← getEnv;
 p::_ ← pure $ parenthesizerAttribute.getValues env k
-  | liftM (throwError $ "no known parenthesizer for kind '" ++ toString k ++ "'");
+  | throwError $ "no known parenthesizer for kind '" ++ toString k ++ "'";
 p
 
 @[combinatorParenthesizer Lean.Parser.withAntiquot]
@@ -269,7 +278,7 @@ adaptReader (fun (ctx : Context) => { ctx with cat := cat }) do
 
 @[combinatorParenthesizer Lean.Parser.categoryParser]
 def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do
-env ← liftM getEnv;
+env ← getEnv;
 match categoryParenthesizerAttribute.getValues env cat with
 | p::_ => p prec
 -- Fall back to the generic parenthesizer.
diff --git a/tests/lean/run/Reformat.lean b/tests/lean/run/Reformat.lean
index 9913cd250b..5de3494ab3 100644
--- a/tests/lean/run/Reformat.lean
+++ b/tests/lean/run/Reformat.lean
@@ -13,7 +13,7 @@ let (debug, f) : Bool × String := match args with
   | _         => panic! "usage: file [-d]";
 env ← mkEmptyEnvironment;
 stx ← Lean.Parser.parseFile env args.head!;
-f ← (PrettyPrinter.ppModule stx).run env (KVMap.insert {} `trace.PrettyPrinter.format debug);
+(f, _) ← (PrettyPrinter.ppModule stx).toIO { options := Options.empty.setBool `trace.PrettyPrinter.format debug } { env := env };
 IO.print f;
 let inputCtx := Parser.mkInputContext (toString f) "<foo>";
 let (stx', state, messages) := Parser.parseHeader env inputCtx;
diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean
index 1fe2b5b62d..4a9189f097 100644
--- a/tests/lean/run/Reparen.lean
+++ b/tests/lean/run/Reparen.lean
@@ -30,8 +30,7 @@ IO.print s;
 let cmds := stx.getArgs.extract 1 stx.getArgs.size;
 cmds.forM $ fun cmd => do
   let cmd := unparen cmd;
-  cmd ← (PrettyPrinter.parenthesizeCommand cmd).run
-    env (KVMap.insert {} `trace.PrettyPrinter.parenthesize debug);
+  (cmd, _) ← (PrettyPrinter.parenthesizeCommand cmd).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
   some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
   IO.print s
 
diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean
index 64bc1fa720..bd617e3fcd 100644
--- a/tests/lean/run/meta1.lean
+++ b/tests/lean/run/meta1.lean
@@ -4,17 +4,17 @@ open Lean.Meta
 
 unsafe def tstInferType (mods : List Name) (e : Expr) : IO Unit :=
 withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
-   type ← (inferType e).toIO env;
+   (type, _, _) ← (inferType e).toIO {} { env := env } {} {};
    IO.println (toString e ++ " : " ++ toString type)
 
 unsafe def tstWHNF (mods : List Name) (e : Expr) (t := TransparencyMode.default) : IO Unit :=
 withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
-   s ← (whnf e).toIO env;
+   (s, _, _) ← (whnf e).toIO {} { env := env };
    IO.println (toString e ++ " ==> " ++ toString s)
 
 unsafe def tstIsProp (mods : List Name) (e : Expr) : IO Unit :=
 withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
-  b ← (isProp e).toIO env;
+  (b, _, _) ← (isProp e).toIO {} { env := env };
   IO.println (toString e ++ ", isProp: " ++ toString b)
 
 def t1 : Expr :=
diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
index 3840c92735..cec0539357 100644
--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@@ -22,8 +22,9 @@ do v? ← getExprMVarAssignment? m.mvarId!;
 
 unsafe def run (mods : List Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit :=
 withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
-   let x := do { x; Meta.printTraces };
-   x.toIO env opts
+   let x := do { x; liftCoreM $ Core.printTraces };
+   _ ← x.toIO { options := opts } { env := env };
+   pure ()
 
 def nat  := mkConst `Nat
 def succ := mkConst `Nat.succ