diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 04857ff234..964d2b6ee2 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -31,6 +31,8 @@ import Lean.Syntax
 import Lean.Elab.Term
 
 namespace Lean
+namespace Meta end Meta -- HACK for old frontend
+open Meta (MetaM) -- HACK for old frontend
 
 -- TODO: move, maybe
 namespace Level
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 919d7371eb..3aa3ec8f8f 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -26,14 +27,9 @@ This module provides four (mutually dependent) goodies that are needed for build
 They are packed into the MetaM monad.
 -/
 
-namespace Lean
-namespace Meta
+namespace Lean.Meta
 
-def registerIsDefEqStuckId : IO InternalExceptionId :=
-registerInternalExceptionId `isDefEqStuck
-
-@[builtinInit registerIsDefEqStuckId]
-constant isDefEqStuckExceptionId : InternalExceptionId := arbitrary _
+builtin_initialize isDefEqStuckExceptionId : InternalExceptionId ← registerInternalExceptionId `isDefEqStuck
 
 structure Config :=
 (foApprox           : Bool := false)
@@ -120,32 +116,28 @@ structure PostponedEntry :=
 abbrev DefEqM := StateRefT (PersistentArray PostponedEntry) MetaM
 
 instance : MonadIO MetaM :=
-{ liftIO := fun α x => liftM (liftIO x : CoreM α) }
+{ liftIO := fun x => liftM (liftIO x : CoreM _) }
 
 instance MetaM.inhabited {α} : Inhabited (MetaM α) :=
 ⟨fun _ _ => arbitrary _⟩
 
 instance : MonadLCtx MetaM :=
-{ getLCtx := do ctx ← read; pure ctx.lctx }
+{ getLCtx := do pure (← read).lctx }
 
 instance : MonadMCtx MetaM :=
-{ getMCtx := do s ← get; pure s.mctx }
+{ getMCtx := do pure (← get).mctx }
 
 instance : AddMessageContext MetaM :=
 { addMessageContext := addMessageContextFull }
 
-instance : Ref MetaM :=
-{ getRef     := getRef,
-  withRef    := fun α => withRef }
-
 @[inline] def MetaM.run {α} (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM (α × State) :=
-(x.run ctx).run s
+x ctx $.run s
 
 @[inline] def MetaM.run' {α} (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM α :=
 Prod.fst <$> x.run ctx s
 
 @[inline] def MetaM.toIO {α} (x : MetaM α) (ctxCore : Core.Context) (sCore : Core.State) (ctx : Context := {}) (s : State := {}) : IO (α × Core.State × State) := do
-((a, s), sCore) ← (x.run ctx s).toIO ctxCore sCore;
+let ((a, s), sCore) ← (x.run ctx s).toIO ctxCore sCore
 pure (a, sCore, s)
 
 instance hasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
@@ -154,9 +146,9 @@ instance hasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
 protected def throwIsDefEqStuck {α} : DefEqM α :=
 throw $ Exception.internal isDefEqStuckExceptionId
 
-@[builtinInit] private def regTraceClasses : IO Unit := do
-registerTraceClass `Meta;
-registerTraceClass `Meta.debug
+builtin_initialize
+  registerTraceClass `Meta
+  registerTraceClass `Meta.debug
 
 @[inline] def liftMetaM {α m} [MonadLiftT MetaM m] (x : MetaM α) : m α :=
 liftM x
@@ -174,57 +166,34 @@ section Methods
 variables {m : Type → Type} [MonadLiftT MetaM m]
 variables {n : Type → Type} [MonadControlT MetaM n] [Monad n]
 
-def getLocalInstances : m LocalInstances := liftMetaM do ctx ← read; pure ctx.localInstances
-def getConfig : m Config := liftMetaM do ctx ← read; pure ctx.config
+def getLocalInstances : m LocalInstances := liftMetaM do pure (← read).localInstances
+def getConfig : m Config := liftMetaM do pure (← read).config
 def setMCtx (mctx : MetavarContext) : m Unit := liftMetaM $ modify fun s => { s with mctx := mctx }
 @[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : m Unit :=
 liftMetaM $ modify fun s => { s with mctx := f s.mctx }
 def resetZetaFVarIds : m Unit := liftMetaM $ modify fun s => { s with zetaFVarIds := {} }
-def getZetaFVarIds : m NameSet := liftMetaM do s ← get; pure s.zetaFVarIds
+def getZetaFVarIds : m NameSet := liftMetaM do pure (← get).zetaFVarIds
 
-def mkWHNFRef : IO (IO.Ref (Expr → MetaM Expr)) :=
-IO.mkRef $ fun _ => throwError "whnf implementation was not set"
-
-@[builtinInit mkWHNFRef] def whnfRef : IO.Ref (Expr → MetaM Expr) := arbitrary _
-
-def mkInferTypeRef : IO (IO.Ref (Expr → MetaM Expr)) :=
-IO.mkRef $ fun _ => throwError "inferType implementation was not set"
-
-@[builtinInit mkInferTypeRef] def inferTypeRef : IO.Ref (Expr → MetaM Expr) := arbitrary _
-
-def mkIsExprDefEqAuxRef : IO (IO.Ref (Expr → Expr → DefEqM Bool)) :=
-IO.mkRef $ fun _ _ => throwError "isDefEq implementation was not set"
-
-@[builtinInit mkIsExprDefEqAuxRef] def isExprDefEqAuxRef : IO.Ref (Expr → Expr → DefEqM Bool) := arbitrary _
-
-def mkSynthPendingRef : IO (IO.Ref (MVarId → MetaM Bool)) :=
-IO.mkRef $ fun _ => pure false
-
-@[builtinInit mkSynthPendingRef] def synthPendingRef : IO.Ref (MVarId → MetaM Bool) := arbitrary _
+builtin_initialize whnfRef : IO.Ref (Expr → MetaM Expr) ← IO.mkRef fun _ => throwError "whnf implementation was not set"
+builtin_initialize inferTypeRef : IO.Ref (Expr → MetaM Expr) ← IO.mkRef fun _ => throwError "inferType implementation was not set"
+builtin_initialize isExprDefEqAuxRef : IO.Ref (Expr → Expr → DefEqM Bool) ← IO.mkRef fun _ _ => throwError "isDefEq implementation was not set"
+builtin_initialize synthPendingRef : IO.Ref (MVarId → MetaM Bool) ← IO.mkRef fun _ => pure false
 
 def whnf (e : Expr) : m Expr :=
-liftMetaM $ withIncRecDepth do
-  fn ← liftIO whnfRef.get;
-  fn e
+liftMetaM $ withIncRecDepth do (← liftIO whnfRef.get) e
 
 def whnfForall [Monad m] (e : Expr) : m Expr := do
-e' ← whnf e;
+let e' ← whnf e
 if e'.isForall then pure e' else pure e
 
 def inferType (e : Expr) : m Expr :=
-liftMetaM $ withIncRecDepth do
-  fn ← liftIO inferTypeRef.get;
-  fn e
+liftMetaM $ withIncRecDepth do (← liftIO inferTypeRef.get) e
 
 protected def isExprDefEqAux (t s : Expr) : DefEqM Bool :=
-withIncRecDepth do
-  fn ← liftIO isExprDefEqAuxRef.get;
-  fn t s
+withIncRecDepth do (← liftIO isExprDefEqAuxRef.get) t s
 
 protected def synthPending (mvarId : MVarId) : MetaM Bool :=
-withIncRecDepth do
-  fn ← liftIO synthPendingRef.get;
-  fn mvarId
+withIncRecDepth do (← liftIO synthPendingRef.get) mvarId
 
 private def mkFreshExprMVarAtCore
     (mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (kind : MetavarKind) (userName : Name) (numScopeArgs : Nat) : MetaM Expr := do
@@ -235,128 +204,126 @@ def mkFreshExprMVarAt
     (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr)
     (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) (numScopeArgs : Nat := 0)
     : m Expr := liftMetaM do
-mvarId ← mkFreshId;
+let mvarId ← mkFreshId
 mkFreshExprMVarAtCore mvarId lctx localInsts type kind userName numScopeArgs
 
 def mkFreshLevelMVar : m Level := liftMetaM do
-mvarId ← mkFreshId;
+let mvarId ← mkFreshId
 modifyMCtx fun mctx => mctx.addLevelMVarDecl mvarId;
 pure $ mkLevelMVar mvarId
 
 private def mkFreshExprMVarCore (type : Expr) (kind : MetavarKind) (userName : Name) : MetaM Expr := do
-lctx ← getLCtx;
-localInsts ← getLocalInstances;
+let lctx ← getLCtx
+let localInsts ← getLocalInstances
 mkFreshExprMVarAt lctx localInsts type kind userName
 
 private def mkFreshExprMVarImpl (type? : Option Expr) (kind : MetavarKind) (userName : Name) : MetaM Expr :=
 match type? with
 | some type => mkFreshExprMVarCore type kind userName
 | none      => do
-  u ← mkFreshLevelMVar;
-  type ← mkFreshExprMVarCore (mkSort u) MetavarKind.natural Name.anonymous;
+  let u ← mkFreshLevelMVar
+  let type ← mkFreshExprMVarCore (mkSort u) MetavarKind.natural Name.anonymous
   mkFreshExprMVarCore type kind userName
 
 def mkFreshExprMVar (type? : Option Expr) (kind := MetavarKind.natural) (userName := Name.anonymous) : m Expr :=
 liftMetaM $ mkFreshExprMVarImpl type? kind userName
 
 def mkFreshTypeMVar (kind := MetavarKind.natural) (userName := Name.anonymous) : m Expr := liftMetaM do
-u ← mkFreshLevelMVar; mkFreshExprMVar (mkSort u) kind userName
+let u ← mkFreshLevelMVar; mkFreshExprMVar (mkSort u) kind userName
 
 /- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create
    the metavar using this method. -/
 private def mkFreshExprMVarWithIdCore (mvarId : MVarId) (type : Expr)
     (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) (numScopeArgs : Nat := 0)
     : m Expr := liftMetaM do
-lctx ← getLCtx;
-localInsts ← getLocalInstances;
+let lctx ← getLCtx
+let localInsts ← getLocalInstances
 mkFreshExprMVarAtCore mvarId lctx localInsts type kind userName numScopeArgs
 
 def mkFreshExprMVarWithIdImpl (mvarId : MVarId) (type? : Option Expr) (kind : MetavarKind) (userName : Name) : MetaM Expr :=
 match type? with
 | some type => mkFreshExprMVarWithIdCore mvarId type kind userName
 | none      => do
-  u ← mkFreshLevelMVar;
-  type ← mkFreshExprMVar (mkSort u);
+  let u ← mkFreshLevelMVar
+  let type ← mkFreshExprMVar (mkSort u)
   mkFreshExprMVarWithIdCore mvarId type kind userName
 
 def mkFreshExprMVarWithId (mvarId : MVarId) (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName := Name.anonymous) : m Expr :=
 liftMetaM $ mkFreshExprMVarWithIdImpl mvarId type? kind userName
 
 def shouldReduceAll : MetaM Bool := liftMetaM do
-ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all
+return (← read).config.transparency == TransparencyMode.all
+
 def shouldReduceReducibleOnly : m Bool := liftMetaM do
-ctx ← read; pure $ ctx.config.transparency == TransparencyMode.reducible
+return (← read).config.transparency == TransparencyMode.reducible
+
 def getTransparency : m TransparencyMode := liftMetaM do
-ctx ← read; pure $ ctx.config.transparency
+return (← read).config.transparency
 
 -- Remark: wanted to use `private`, but in the C++ parser, `private` declarations do not shadow outer public ones.
 -- TODO: fix this bug
 def isReducible (constName : Name) : MetaM Bool := do
-env ← getEnv; pure $ isReducible env constName
+return Lean.isReducible (← getEnv) constName
 
 def getMVarDecl (mvarId : MVarId) : m MetavarDecl := liftMetaM do
-mctx ← getMCtx;
+let mctx ← getMCtx
 match mctx.findDecl? mvarId with
 | some d => pure d
-| none   => throwError ("unknown metavariable '" ++ mkMVar mvarId ++ "'")
+| none   => throwError! "unknown metavariable '{mkMVar mvarId}'"
 
 def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : m Unit :=
 modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
 
 def isReadOnlyExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
-mvarDecl ← getMVarDecl mvarId;
-mctx     ← getMCtx;
+let mvarDecl ← getMVarDecl mvarId
+let mctx     ← getMCtx
 pure $ mvarDecl.depth != mctx.depth
 
 def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
-mvarDecl ← getMVarDecl mvarId;
+let mvarDecl ← getMVarDecl mvarId
 match mvarDecl.kind with
 | MetavarKind.syntheticOpaque => pure true
 | _ => do
-  mctx ← getMCtx;
+  let mctx ← getMCtx
   pure $ mvarDecl.depth != mctx.depth
 
 def isReadOnlyLevelMVar (mvarId : MVarId) : m Bool := liftMetaM do
-mctx ← getMCtx;
+let mctx ← getMCtx
 match mctx.findLevelDepth? mvarId with
 | some depth => pure $ depth != mctx.depth
-| _          => throwError ("unknown universe metavariable '" ++ mkLevelMVar mvarId ++ "'")
+| _          => throwError! "unknown universe metavariable '{mkLevelMVar mvarId}'"
 
 def renameMVar (mvarId : MVarId) (newUserName : Name) : m Unit :=
 modifyMCtx fun mctx => mctx.renameMVar mvarId newUserName
 
 def isExprMVarAssigned (mvarId : MVarId) : m Bool := liftMetaM do
-mctx ← getMCtx;
+let mctx ← getMCtx
 pure $ mctx.isExprAssigned mvarId
 
 def getExprMVarAssignment? (mvarId : MVarId) : m (Option Expr) := liftMetaM do
-mctx ← getMCtx; pure (mctx.getExprAssignment? mvarId)
+let mctx ← getMCtx
+pure (mctx.getExprAssignment? mvarId)
 
 def assignExprMVar (mvarId : MVarId) (val : Expr) : m Unit := liftMetaM do
 modifyMCtx fun mctx => mctx.assignExpr mvarId val
 
 def isDelayedAssigned (mvarId : MVarId) : m Bool := liftMetaM do
-mctx ← getMCtx;
-pure $ mctx.isDelayedAssigned mvarId
+return (← getMCtx).isDelayedAssigned mvarId
 
 def getDelayedAssignment? (mvarId : MVarId) : m (Option DelayedMetavarAssignment) := liftMetaM do
-mctx ← getMCtx;
-pure $ mctx.getDelayedAssignment? mvarId
+return (← getMCtx).getDelayedAssignment? mvarId
 
 def hasAssignableMVar (e : Expr) : m Bool := liftMetaM do
-mctx ← getMCtx;
-pure $ mctx.hasAssignableMVar e
+return (← getMCtx).hasAssignableMVar e
 
 def throwUnknownFVar {α} (fvarId : FVarId) : MetaM α :=
-throwError ("unknown free variable '" ++ mkFVar fvarId ++ "'")
+throwError! "unknown free variable '{mkFVar fvarId}'"
 
 def findLocalDecl? (fvarId : FVarId) : m (Option LocalDecl) := liftMetaM do
-lctx ← getLCtx;
-pure $ lctx.find? fvarId
+return (← getLCtx).find? fvarId
 
 def getLocalDecl (fvarId : FVarId) : m LocalDecl := liftMetaM do
-lctx ← getLCtx;
-match lctx.find? fvarId with
+match (← getLCtx).find? fvarId with
 | some d => pure d
 | none   => throwUnknownFVar fvarId
 
@@ -364,14 +331,13 @@ def getFVarLocalDecl (fvar : Expr) : m LocalDecl := liftMetaM do
 getLocalDecl fvar.fvarId!
 
 def getLocalDeclFromUserName (userName : Name) : m LocalDecl := liftMetaM do
-lctx ← getLCtx;
-match lctx.findFromUserName? userName with
+match (← getLCtx).findFromUserName? userName with
 | some d => pure d
-| none   => throwError ("unknown local declaration '" ++ userName ++ "'")
+| none   => throwError! "unknown local declaration '{userName}'"
 
 def instantiateMVars (e : Expr) : m Expr := liftMetaM do
 if e.hasMVar then
-  modifyGet $ fun s =>
+  modifyGet fun s =>
     let (e, mctx) := s.mctx.instantiateMVars e;
     (e, { s with mctx := mctx })
 else
@@ -379,19 +345,16 @@ else
 
 def instantiateLocalDeclMVars (localDecl : LocalDecl) : m LocalDecl := liftMetaM do
 match localDecl with
-  | LocalDecl.cdecl idx id n type bi  => do
-    type ← instantiateMVars type;
+  | LocalDecl.cdecl idx id n type bi  =>
+    let type ← instantiateMVars type
     pure $ LocalDecl.cdecl idx id n type bi
-  | LocalDecl.ldecl idx id n type val nonDep => do
-    type ← instantiateMVars type;
-    val ← instantiateMVars val;
+  | LocalDecl.ldecl idx id n type val nonDep =>
+    let type ← instantiateMVars type
+    let val ← instantiateMVars val
     pure $ LocalDecl.ldecl idx id n type val nonDep
 
 @[inline] private def liftMkBindingM {α} (x : MetavarContext.MkBindingM α) : MetaM α := do
-mctx ← getMCtx;
-ngen ← getNGen;
-lctx ← getLCtx;
-match x lctx { mctx := mctx, ngen := ngen } with
+match x (← getLCtx) { mctx := (← getMCtx), ngen := (← getNGen) } with
 | EStateM.Result.ok e newS => do
   setNGen newS.ngen;
   setMCtx newS.mctx;
@@ -411,7 +374,7 @@ def mkLetFVars (xs : Array Expr) (e : Expr) : m Expr :=
 mkLambdaFVars xs e
 
 def mkArrow (d b : Expr) : m Expr := liftMetaM do
-n ← mkFreshUserName `x;
+let n ← mkFreshUserName `x
 pure $ Lean.mkForall n BinderInfo.default d b
 
 def mkForallUsedOnly (xs : Array Expr) (e : Expr) : m (Expr × Nat) := liftMetaM do
@@ -421,13 +384,13 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.elimMVarDeps xs e preserveOrder
 
 @[inline] def withConfig {α} (f : Config → Config) : n α → n α :=
-mapMetaM fun _ => withReader (fun ctx => { ctx with config := f ctx.config })
+mapMetaM $ withReader (fun ctx => { ctx with config := f ctx.config })
 
 @[inline] def withTrackingZeta {α} (x : n α) : n α :=
 withConfig (fun cfg => { cfg with trackZeta := true }) x
 
 @[inline] def withTransparency {α} (mode : TransparencyMode) : n α → n α :=
-mapMetaM fun _ => withConfig (fun config => { config with transparency := mode })
+mapMetaM $ withConfig (fun config => { config with transparency := mode })
 
 @[inline] def withReducible {α} (x : n α) : n α :=
 withTransparency TransparencyMode.reducible x
@@ -435,13 +398,13 @@ withTransparency TransparencyMode.reducible x
 @[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : n α) : n α :=
 withConfig
   (fun config =>
-    let oldMode := config.transparency;
-    let mode    := if oldMode.lt mode then mode else oldMode;
+    let oldMode := config.transparency
+    let mode    := if oldMode.lt mode then mode else oldMode
     { config with transparency := mode })
   x
 
 def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
-env ← getEnv;
+let env ← getEnv
 match env.find? constName with
 | some (info@(ConstantInfo.thmInfo _)) =>
   condM shouldReduceAll (pure (some info)) (pure none)
@@ -453,7 +416,7 @@ match env.find? constName with
 | none      => throwUnknownConstant constName
 
 def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
-env ← getEnv;
+let env ← getEnv
 match env.find? constName with
 | some (info@(ConstantInfo.thmInfo _)) =>
   condM shouldReduceAll (pure (some info)) (pure none)
@@ -466,20 +429,19 @@ match env.find? constName with
 
 /-- Save cache, execute `x`, restore cache -/
 @[inline] private def savingCacheImpl {α} (x : MetaM α) : MetaM α := do
-s ← get;
-let savedCache := s.cache;
-finally x (modify fun s => { s with cache := savedCache })
+let s ← get
+let savedCache := s.cache
+try x finally modify fun s => { s with cache := savedCache }
 
 @[inline] def savingCache {α} : n α → n α :=
-mapMetaM fun _ => savingCacheImpl
+mapMetaM savingCacheImpl
 
 private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do
-env ← getEnv;
+let env ← getEnv
 if isClass env constName then
   pure (LOption.some constName)
-else do
-  cinfo? ← getConst? constName;
-  match cinfo? with
+else
+  match (← getConst? constName) with
   | some _ => pure LOption.undef
   | none   => pure LOption.none
 
@@ -495,8 +457,7 @@ private partial def isClassQuick? : Expr → MetaM (LOption Name)
 | Expr.mdata _ e _     => isClassQuick? e
 | Expr.const n _ _     => isClassQuickConst? n
 | Expr.mvar mvarId _   => do
-  val? ← getExprMVarAssignment? mvarId;
-  match val? with
+  match (← getExprMVarAssignment? mvarId) with
   | some val => isClassQuick? val
   | none     => pure LOption.none
 | Expr.app f _ _       =>
@@ -507,27 +468,27 @@ private partial def isClassQuick? : Expr → MetaM (LOption Name)
 | Expr.localE _ _ _ _ => unreachable!
 
 def saveAndResetSynthInstanceCache : MetaM SynthInstanceCache := do
-s ← get;
-let savedSythInstance := s.cache.synthInstance;
-modify $ fun s => { s with cache := { s.cache with synthInstance := {} } };
+let 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 :=
-modify $ fun s => { s with cache := { s.cache with synthInstance := cache } }
+modify fun s => { s with cache := { s.cache with synthInstance := cache } }
 
 @[inline] private def resettingSynthInstanceCacheImpl {α} (x : MetaM α) : MetaM α := do
-savedSythInstance ← saveAndResetSynthInstanceCache;
-finally x (restoreSynthInstanceCache savedSythInstance)
+let savedSythInstance ← saveAndResetSynthInstanceCache
+try x finally restoreSynthInstanceCache savedSythInstance
 
 /-- Reset `synthInstance` cache, execute `x`, and restore cache -/
 @[inline] def resettingSynthInstanceCache {α} : n α → n α :=
-mapMetaM fun _ => resettingSynthInstanceCacheImpl
+mapMetaM resettingSynthInstanceCacheImpl
 
 @[inline] def resettingSynthInstanceCacheWhen {α} (b : Bool) (x : n α) : n α :=
 if b then resettingSynthInstanceCache x else x
 
 private def withNewLocalInstanceImp {α} (className : Name) (fvar : Expr) (k : MetaM α) : MetaM α := do
-localDecl ← getFVarLocalDecl fvar;
+let localDecl ← getFVarLocalDecl fvar
 /- Recall that we use `auxDecl` binderInfo when compiling recursive declarations. -/
 match localDecl.binderInfo with
 | BinderInfo.auxDecl => k
@@ -541,7 +502,7 @@ match localDecl.binderInfo with
     and then execute continuation `k`.
     It resets the type class cache using `resettingSynthInstanceCache`. -/
 def withNewLocalInstance {α} (className : Name) (fvar : Expr) : n α → n α :=
-mapMetaM fun _ => withNewLocalInstanceImp className fvar
+mapMetaM $ withNewLocalInstanceImp className fvar
 
 /--
   `withNewLocalInstances isClassExpensive fvars j k` updates the vector or local instances
@@ -552,23 +513,19 @@ mapMetaM fun _ => withNewLocalInstanceImp className fvar
   - `isClassExpensive` uses `whnf` which depends (indirectly) on the set of local instances.
     Thus, each new local instance requires a new `resettingSynthInstanceCache`. -/
 @[specialize] private partial def withNewLocalInstancesImp {α}
-    (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;
-    match c? with
-    | LOption.none   => withNewLocalInstancesImp (i+1) k
-    | LOption.undef  => do
-      c? ← isClassExpensive? decl.type;
-      match c? with
-      | none   => withNewLocalInstancesImp (i+1) k
-      | some c => withNewLocalInstance c fvar $ withNewLocalInstancesImp (i+1) k
-    | LOption.some c => withNewLocalInstance c fvar $ withNewLocalInstancesImp (i+1) k
-  else
-    k
+    (isClassExpensive? : Expr → MetaM (Option Name)) (fvars : Array Expr) (i : Nat) (k : MetaM α) : MetaM α := do
+if h : i < fvars.size then
+  let fvar := fvars.get ⟨i, h⟩
+  let decl ← getFVarLocalDecl fvar
+  match (← isClassQuick? decl.type) with
+  | LOption.none   => withNewLocalInstancesImp isClassExpensive? fvars (i+1) k
+  | LOption.undef  =>
+    match (← isClassExpensive? decl.type) with
+    | none   => withNewLocalInstancesImp isClassExpensive? fvars (i+1) k
+    | some c => withNewLocalInstance c fvar $ withNewLocalInstancesImp isClassExpensive? fvars (i+1) k
+  | LOption.some c => withNewLocalInstance c fvar $ withNewLocalInstancesImp isClassExpensive? fvars (i+1) k
+else
+  k
 
 private def fvarsSizeLtMaxFVars (fvars : Array Expr) (maxFVars? : Option Nat) : Bool :=
 match maxFVars? with
@@ -603,36 +560,36 @@ match maxFVars? with
 @[specialize] private partial def forallTelescopeReducingAuxAux {α}
     (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 {
-    let d     := d.instantiateRevRange j fvars.size fvars;
-    fvarId ← mkFreshId;
-    let lctx  := lctx.mkLocalDecl fvarId n d c.binderInfo;
-    let fvar  := mkFVar fvarId;
-    let fvars := fvars.push fvar;
-    forallTelescopeReducingAuxAux lctx fvars j b
-  };
-  if fvarsSizeLtMaxFVars fvars maxFVars? then
-    process ()
-  else
+    (type              : Expr)
+    (k                 : Array Expr → Expr → MetaM α) : MetaM α := do
+let rec process (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (type : Expr) : MetaM α := do
+  match type with
+  | Expr.forallE n d b c =>
+    if fvarsSizeLtMaxFVars fvars maxFVars? then
+      let d     := d.instantiateRevRange j fvars.size fvars
+      let fvarId ← mkFreshId
+      let lctx  := lctx.mkLocalDecl fvarId n d c.binderInfo
+      let fvar  := mkFVar fvarId
+      let fvars := fvars.push fvar
+      process lctx fvars j b
+    else
+      let type := type.instantiateRevRange j fvars.size fvars;
+      withReader (fun ctx => { ctx with lctx := lctx }) do
+        withNewLocalInstancesImp isClassExpensive? fvars j do
+          k fvars type
+  | _ =>
     let type := type.instantiateRevRange j fvars.size fvars;
-    withReader (fun ctx => { ctx with lctx := lctx }) $
-      withNewLocalInstancesImp isClassExpensive? fvars j $
-        k fvars type
-| lctx, fvars, j, type =>
-  let type := type.instantiateRevRange j fvars.size fvars;
-  withReader (fun ctx => { ctx with lctx := lctx }) $
-    withNewLocalInstancesImp isClassExpensive? fvars j $
-      if reducing? && fvarsSizeLtMaxFVars fvars maxFVars? then do
-        newType ← whnf type;
-        if newType.isForall then
-          forallTelescopeReducingAuxAux lctx fvars fvars.size newType
+    withReader (fun ctx => { ctx with lctx := lctx }) do
+      withNewLocalInstancesImp isClassExpensive? fvars j do
+        if reducing? && fvarsSizeLtMaxFVars fvars maxFVars? then
+          let newType ← whnf type
+          if newType.isForall then
+            process lctx fvars fvars.size newType
+          else
+            k fvars type
         else
           k fvars type
-      else
-        k fvars type
+process (← getLCtx) #[] 0 type
 
 /- We need this auxiliary definition because it depends on `isClassExpensive`,
    and `isClassExpensive` depends on it. -/
@@ -642,48 +599,45 @@ match maxFVars? with
 match maxFVars? with
 | some 0 => k #[] type
 | _ => do
-  newType ← whnf type;
-  if newType.isForall then do
-    lctx ← getLCtx;
-    forallTelescopeReducingAuxAux isClassExpensive? true maxFVars? k lctx #[] 0 newType
+  let newType ← whnf type
+  if newType.isForall then
+    forallTelescopeReducingAuxAux isClassExpensive? true maxFVars? newType k
   else
     k #[] type
 
 private 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;
+      let env ← getEnv
       pure $ if isClass env c then some c else none
     | _ => pure none
 
 private def isClassImp? (type : Expr) : MetaM (Option Name) := do
-c? ← isClassQuick? type;
-match c? with
+match (← isClassQuick? type) with
 | LOption.none   => pure none
 | LOption.some c => pure (some c)
 | LOption.undef  => isClassExpensive? type
 
 def isClass? (type : Expr) : m (Option Name) :=
-liftMetaM $ catch (isClassImp? type) (fun _ => pure none)
+liftMetaM do try isClassImp? type catch _ => pure none
 
 private def withNewLocalInstancesImpAux {α} (fvars : Array Expr) (j : Nat) : n α → n α :=
-mapMetaM fun _ => withNewLocalInstancesImp isClassExpensive? fvars j
+mapMetaM $ withNewLocalInstancesImp isClassExpensive? fvars j
 
 def withNewLocalInstances {α} (fvars : Array Expr) (j : Nat) : n α → n α :=
-mapMetaM fun _ => withNewLocalInstancesImpAux fvars j
+mapMetaM $ withNewLocalInstancesImpAux fvars j
 
 private def forallTelescopeImp {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α := do
-lctx ← getLCtx;
-forallTelescopeReducingAuxAux isClassExpensive? false none k lctx #[] 0 type
+forallTelescopeReducingAuxAux isClassExpensive? false none type k
 
 /--
   Given `type` of the form `forall xs, A`, execute `k xs A`.
   This combinator will declare local declarations, create free variables for them,
   execute `k` with updated local context, and make sure the cache is restored after executing `k`. -/
 def forallTelescope {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
-map2MetaM (fun _ k => forallTelescopeImp type k) k
+map2MetaM (fun k => forallTelescopeImp type k) k
 
 @[noinline] private def forallTelescopeReducingImp {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
 forallTelescopeReducingAux isClassExpensive? type none k
@@ -692,7 +646,7 @@ forallTelescopeReducingAux isClassExpensive? type none k
   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 → n α) : n α :=
-map2MetaM (fun _ k => forallTelescopeReducingImp type k) k
+map2MetaM (fun k => forallTelescopeReducingImp type k) k
 
 @[noinline] private def forallBoundedTelescopeImp {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
 forallTelescopeReducingAux isClassExpensive? type maxFVars? k
@@ -701,48 +655,67 @@ forallTelescopeReducingAux isClassExpensive? type maxFVars? k
   Similar to `forallTelescopeReducing`, stops constructing the telescope when
   it reaches size `maxFVars`. -/
 def forallBoundedTelescope {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) : n α :=
-map2MetaM (fun _ k => forallBoundedTelescopeImp type maxFVars? k) k
+map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k) k
 
 /-- Similar to `forallTelescopeAuxAux` but for lambda and let expressions. -/
 private partial def lambdaTelescopeAux {α}
     (k : Array Expr → Expr → MetaM α)
     : Bool → LocalContext → Array Expr → Nat → Expr → MetaM α
 | consumeLet, lctx, fvars, j, Expr.lam n d b c => do
-  let d := d.instantiateRevRange j fvars.size fvars;
-  fvarId ← mkFreshId;
-  let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo;
-  let fvar := mkFVar fvarId;
-  lambdaTelescopeAux consumeLet lctx (fvars.push fvar) j b
+  let d := d.instantiateRevRange j fvars.size fvars
+  let fvarId ← mkFreshId
+  let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo
+  let fvar := mkFVar fvarId
+  lambdaTelescopeAux k consumeLet lctx (fvars.push fvar) j b
 | true, lctx, fvars, j, Expr.letE n t v b _ => do
-  let t := t.instantiateRevRange j fvars.size fvars;
-  let v := v.instantiateRevRange j fvars.size fvars;
-  fvarId ← mkFreshId;
-  let lctx := lctx.mkLetDecl fvarId n t v;
-  let fvar := mkFVar fvarId;
-  lambdaTelescopeAux true lctx (fvars.push fvar) j b
+  let t := t.instantiateRevRange j fvars.size fvars
+  let v := v.instantiateRevRange j fvars.size fvars
+  let fvarId ← mkFreshId
+  let lctx := lctx.mkLetDecl fvarId n t v
+  let fvar := mkFVar fvarId
+  lambdaTelescopeAux k true lctx (fvars.push fvar) j b
 | _, lctx, fvars, j, e =>
   let e := e.instantiateRevRange j fvars.size fvars;
-  withReader (fun ctx => { ctx with lctx := lctx }) $
-    withNewLocalInstancesImp isClassExpensive? fvars j $ do
+  withReader (fun ctx => { ctx with lctx := lctx }) do
+    withNewLocalInstancesImp isClassExpensive? fvars j do
       k fvars e
 
-private def lambdaTelescopeImp {α} (e : Expr) (consumeLet : Bool) (k : Array Expr → Expr → MetaM α) : MetaM α := do
-lctx ← getLCtx;
-lambdaTelescopeAux k consumeLet lctx #[] 0 e
+private partial def lambdaTelescopeImp {α} (e : Expr) (consumeLet : Bool) (k : Array Expr → Expr → MetaM α) : MetaM α := do
+let rec process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (e : Expr) : MetaM α := do
+  match consumeLet, e with
+  | _, Expr.lam n d b c =>
+    let d := d.instantiateRevRange j fvars.size fvars
+    let fvarId ← mkFreshId
+    let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo
+    let fvar := mkFVar fvarId
+    process consumeLet lctx (fvars.push fvar) j b
+  | true, Expr.letE n t v b _ => do
+    let t := t.instantiateRevRange j fvars.size fvars
+    let v := v.instantiateRevRange j fvars.size fvars
+    let fvarId ← mkFreshId
+    let lctx := lctx.mkLetDecl fvarId n t v
+    let fvar := mkFVar fvarId
+    process true lctx (fvars.push fvar) j b
+  | _, e =>
+    let e := e.instantiateRevRange j fvars.size fvars
+    withReader (fun ctx => { ctx with lctx := lctx }) do
+      withNewLocalInstancesImp isClassExpensive? fvars j do
+        k fvars e
+process consumeLet (← getLCtx) #[] 0 e
 
 /-- Similar to `forallTelescope` but for lambda and let expressions. -/
 def lambdaLetTelescope {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
-map2MetaM (fun _ k => lambdaTelescopeImp type true k) k
+map2MetaM (fun k => lambdaTelescopeImp type true k) k
 
 /-- Similar to `forallTelescope` but for lambda expressions. -/
 def lambdaTelescope {α} (type : Expr) (k : Array Expr → Expr → n α) : n α :=
-map2MetaM (fun _ k => lambdaTelescopeImp type false k) k
+map2MetaM (fun k => lambdaTelescopeImp type false k) k
 
 def getParamNamesImp (declName : Name) : MetaM (Array Name) := do
-cinfo ← getConstInfo declName;
-forallTelescopeReducing cinfo.type $ fun xs _ => do
-  xs.mapM $ fun x => do
-    localDecl ← getLocalDecl x.fvarId!;
+let cinfo ← getConstInfo declName
+forallTelescopeReducing cinfo.type fun xs _ => do
+  xs.mapM fun x => do
+    let localDecl ← getLocalDecl x.fvarId!
     pure localDecl.userName
 
 /-- Return the parameter names for the givel global declaration. -/
@@ -751,114 +724,111 @@ liftMetaM $ getParamNamesImp declName
 
 -- `kind` specifies the metavariable kind for metavariables not corresponding to instance implicit `[ ... ]` arguments.
 private partial def forallMetaTelescopeReducingAux
-    (reducing? : Bool) (maxMVars? : Option Nat) (kind : MetavarKind)
-    : Array Expr → Array BinderInfo → Nat → Expr → MetaM (Array Expr × Array BinderInfo × Expr)
-| mvars, bis, j, type@(Expr.forallE n d b c) => do
-  let process : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do {
-    let d  := d.instantiateRevRange j mvars.size mvars;
-    let k  := if c.binderInfo.isInstImplicit then  MetavarKind.synthetic else kind;
-    mvar ← mkFreshExprMVar d k n;
-    let mvars := mvars.push mvar;
-    let bis   := bis.push c.binderInfo;
-    forallMetaTelescopeReducingAux mvars bis j b
-  };
-  match maxMVars? with
-  | none          => process ()
-  | some maxMVars =>
-    if mvars.size < maxMVars then
-      process ()
-    else
-      let type := type.instantiateRevRange j mvars.size mvars;
-      pure (mvars, bis, type)
-| mvars, bis, j, type =>
-  let type := type.instantiateRevRange j mvars.size mvars;
-  if reducing? then do
-    newType ← whnf type;
-    if newType.isForall then
-      forallMetaTelescopeReducingAux mvars bis mvars.size newType
+    (e : Expr) (reducing : Bool) (maxMVars? : Option Nat) (kind : MetavarKind) : MetaM (Array Expr × Array BinderInfo × Expr) :=
+let rec process (mvars : Array Expr) (bis : Array BinderInfo) (j : Nat) (type : Expr) : MetaM (Array Expr × Array BinderInfo × Expr) := do
+  match type with
+  | Expr.forallE n d b c =>
+    let cont : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do
+      let d  := d.instantiateRevRange j mvars.size mvars
+      let k  := if c.binderInfo.isInstImplicit then  MetavarKind.synthetic else kind
+      let mvar ← mkFreshExprMVar d k n
+      let mvars := mvars.push mvar
+      let bis   := bis.push c.binderInfo
+      process mvars bis j b
+    match maxMVars? with
+    | none          => cont ()
+    | some maxMVars =>
+      if mvars.size < maxMVars then
+        cont ()
+      else
+        let type := type.instantiateRevRange j mvars.size mvars;
+        pure (mvars, bis, type)
+  | _ =>
+    let type := type.instantiateRevRange j mvars.size mvars;
+    if reducing then do
+      let newType ← whnf type;
+      if newType.isForall then
+        process mvars bis mvars.size newType
+      else
+        pure (mvars, bis, type)
     else
       pure (mvars, bis, type)
-  else
-    pure (mvars, bis, type)
+process #[] #[] 0 e
 
 /-- Similar to `forallTelescope`, but creates metavariables instead of free variables. -/
 def forallMetaTelescope (e : Expr) (kind := MetavarKind.natural) : m (Array Expr × Array BinderInfo × Expr) :=
-liftMetaM $ forallMetaTelescopeReducingAux false none kind #[] #[] 0 e
+liftMetaM $ forallMetaTelescopeReducingAux e (reducing := false) (maxMVars? := none) kind
 
 /-- Similar to `forallTelescopeReducing`, but creates metavariables instead of free variables. -/
 def forallMetaTelescopeReducing (e : Expr) (maxMVars? : Option Nat := none) (kind := MetavarKind.natural) : m (Array Expr × Array BinderInfo × Expr) :=
-liftMetaM $ forallMetaTelescopeReducingAux true maxMVars? kind #[] #[] 0 e
+liftMetaM $ forallMetaTelescopeReducingAux e (reducing := true) maxMVars? kind
 
 /-- Similar to `forallMetaTelescopeReducingAux` but for lambda expressions. -/
-private partial def lambdaMetaTelescopeAux (maxMVars? : Option Nat)
-    : Array Expr → Array BinderInfo → Nat → Expr → MetaM (Array Expr × Array BinderInfo × Expr)
-| mvars, bis, j, type => do
-  let finalize : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do {
-    let type := type.instantiateRevRange j mvars.size mvars;
+private partial def lambdaMetaTelescopeImp (e : Expr) (maxMVars? : Option Nat) : MetaM (Array Expr × Array BinderInfo × Expr) :=
+let rec process (mvars : Array Expr) (bis : Array BinderInfo) (j : Nat) (type : Expr) : MetaM (Array Expr × Array BinderInfo × Expr) := do
+  let finalize : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do
+    let type := type.instantiateRevRange j mvars.size mvars
     pure (mvars, bis, type)
-  };
-  let process : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do {
+  let cont : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do
     match type with
-    | Expr.lam n d b c => do
-      let d     := d.instantiateRevRange j mvars.size mvars;
-      mvar ← mkFreshExprMVar d;
-      let mvars := mvars.push mvar;
-      let bis   := bis.push c.binderInfo;
-      lambdaMetaTelescopeAux mvars bis j b
+    | Expr.lam n d b c =>
+      let d     := d.instantiateRevRange j mvars.size mvars
+      let mvar ← mkFreshExprMVar d
+      let mvars := mvars.push mvar
+      let bis   := bis.push c.binderInfo
+      process mvars bis j b
     | _ => finalize ()
-  };
   match maxMVars? with
-  | none          => process ()
+  | none          => cont ()
   | some maxMVars =>
     if mvars.size < maxMVars then
-      process ()
+      cont ()
     else
       finalize ()
+process #[] #[] 0 e
 
 /-- Similar to `forallMetaTelescope` but for lambda expressions. -/
-def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : m (Array Expr × Array BinderInfo × Expr) :=
-liftMetaM $ lambdaMetaTelescopeAux maxMVars? #[] #[] 0 e
+partial def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : m (Array Expr × Array BinderInfo × Expr) :=
+liftMetaM $ lambdaMetaTelescopeImp e maxMVars?
 
 private def withNewFVar {α} (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
-c? ← isClass? fvarType;
-match c? with
+match (← isClass? fvarType) with
 | none   => k fvar
 | some c => withNewLocalInstance c fvar $ k fvar
 
 private def withLocalDeclImp {α} (n : Name) (bi : BinderInfo) (type : Expr) (k : Expr → MetaM α) : MetaM α := do
-fvarId ← mkFreshId;
-ctx ← read;
-let lctx := ctx.lctx.mkLocalDecl fvarId n type bi;
-let fvar := mkFVar fvarId;
-withReader (fun ctx => { ctx with lctx := lctx }) $
+let fvarId ← mkFreshId
+let ctx ← read
+let lctx := ctx.lctx.mkLocalDecl fvarId n type bi
+let fvar := mkFVar fvarId
+withReader (fun ctx => { ctx with lctx := lctx }) do
   withNewFVar fvar type k
 
 def withLocalDecl {α} (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n α) : n α :=
-map1MetaM (fun _ k => withLocalDeclImp name bi type k) k
+map1MetaM (fun k => withLocalDeclImp name bi type k) k
 
 def withLocalDeclD {α} (name : Name) (type : Expr) (k : Expr → n α) : n α :=
 withLocalDecl name BinderInfo.default type k
 
 private def withLetDeclImp {α} (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) : MetaM α := do
-fvarId ← mkFreshId;
-ctx ← read;
-let lctx := ctx.lctx.mkLetDecl fvarId n type val;
-let fvar := mkFVar fvarId;
-withReader (fun ctx => { ctx with lctx := lctx }) $
+let fvarId ← mkFreshId
+let ctx ← read
+let lctx := ctx.lctx.mkLetDecl fvarId n type val
+let fvar := mkFVar fvarId
+withReader (fun ctx => { ctx with lctx := lctx }) do
   withNewFVar fvar type k
 
 def withLetDecl {α} (name : Name) (type : Expr) (val : Expr) (k : Expr → n α) : n α :=
-map1MetaM (fun _ k => withLetDeclImp name type val k) k
+map1MetaM (fun k => withLetDeclImp name type val k) k
 
 private def withExistingLocalDeclsImp {α} (decls : List LocalDecl) (k : MetaM α) : MetaM α := do
-ctx ← read;
-let numLocalInstances := ctx.localInstances.size;
-let lctx := decls.foldl (fun (lctx : LocalContext) decl => lctx.addDecl decl) ctx.lctx;
+let ctx ← read
+let numLocalInstances := ctx.localInstances.size
+let lctx := decls.foldl (fun (lctx : LocalContext) decl => lctx.addDecl decl) ctx.lctx
 withReader (fun ctx => { ctx with lctx := lctx }) do
-  newLocalInsts ← decls.foldlM
+  let newLocalInsts ← decls.foldlM
     (fun (newlocalInsts : Array LocalInstance) (decl : LocalDecl) => (do {
-      c? ← isClass? decl.type;
-      match c? with
+      match (← isClass? decl.type) with
       | none   => pure newlocalInsts
       | some c => pure $ newlocalInsts.push { className := c, fvar := decl.toExpr } } : MetaM _))
     ctx.localInstances;
@@ -868,33 +838,33 @@ withReader (fun ctx => { ctx with lctx := lctx }) do
     resettingSynthInstanceCache $ withReader (fun ctx => { ctx with localInstances := newLocalInsts }) k
 
 def withExistingLocalDecls {α} (decls : List LocalDecl) : n α → n α :=
-mapMetaM fun _ => withExistingLocalDeclsImp decls
+mapMetaM $ withExistingLocalDeclsImp decls
 
 private def withNewMCtxDepthImp {α} (x : MetaM α) : MetaM α := do
-s ← get;
-let savedMCtx  := s.mctx;
-modifyMCtx fun mctx => mctx.incDepth;
-finally x (setMCtx savedMCtx)
+let s ← get
+let savedMCtx  := s.mctx
+modifyMCtx fun mctx => mctx.incDepth
+try x finally setMCtx savedMCtx
 
 /--
   Save cache and `MetavarContext`, bump the `MetavarContext` depth, execute `x`,
   and restore saved data. -/
 def withNewMCtxDepth {α} : n α → n α :=
-mapMetaM fun _ => withNewMCtxDepthImp
+mapMetaM withNewMCtxDepthImp
 
 private def withLocalContextImp {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : MetaM α) : MetaM α := do
-localInstsCurr ← getLocalInstances;
-withReader (fun ctx => { ctx with lctx := lctx, localInstances := localInsts }) $
+let localInstsCurr ← getLocalInstances
+withReader (fun ctx => { ctx with lctx := lctx, localInstances := localInsts }) do
   if localInsts == localInstsCurr then
     x
   else
     resettingSynthInstanceCache x
 
 def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) : n α → n α :=
-mapMetaM fun _ => withLocalContextImp lctx localInsts
+mapMetaM $ withLocalContextImp lctx localInsts
 
 private def withMVarContextImp {α} (mvarId : MVarId) (x : MetaM α) : MetaM α := do
-mvarDecl ← getMVarDecl mvarId;
+let mvarDecl ← getMVarDecl mvarId
 withLocalContextImp mvarDecl.lctx mvarDecl.localInstances x
 
 /--
@@ -902,22 +872,22 @@ withLocalContextImp mvarDecl.lctx mvarDecl.localInstances x
   The type class resolution cache is flushed when executing `x` if its `LocalInstances` are
   different from the current ones. -/
 def withMVarContext {α} (mvarId : MVarId) : n α → n α :=
-mapMetaM fun _ => withMVarContextImp mvarId
+mapMetaM $ withMVarContextImp mvarId
 
 private def withMCtxImp {α} (mctx : MetavarContext) (x : MetaM α) : MetaM α := do
-mctx' ← getMCtx;
-setMCtx mctx;
-finally x (setMCtx mctx')
+let mctx' ← getMCtx
+setMCtx mctx
+try x finally setMCtx mctx'
 
 def withMCtx {α} (mctx : MetavarContext) : n α → n α :=
-mapMetaM fun _ => withMCtxImp mctx
+mapMetaM $ withMCtxImp mctx
 
 @[inline] private def approxDefEqImp {α} (x : MetaM α) : MetaM α :=
 withConfig (fun config => { config with foApprox := true, ctxApprox := true, quasiPatternApprox := true}) x
 
 /-- Execute `x` using approximate unification: `foApprox`, `ctxApprox` and `quasiPatternApprox`.  -/
 @[inline] def approxDefEq {α} : n α → n α :=
-mapMetaM fun _ => approxDefEqImp
+mapMetaM approxDefEqImp
 
 @[inline] private def fullApproxDefEqImp {α} (x : MetaM α) : MetaM α :=
 withConfig (fun config => { config with foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true }) x
@@ -930,19 +900,19 @@ withConfig (fun config => { config with foApprox := true, ctxApprox := true, qua
   as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
   solve `[HasPure (fun _ => IO Bool)]` -/
 @[inline] def fullApproxDefEq {α} : n α → n α :=
-mapMetaM fun _ => fullApproxDefEqImp
+mapMetaM fullApproxDefEqImp
 
 @[inline] private def liftStateMCtx {α} (x : StateM MetavarContext α) : MetaM α := do
-mctx ← getMCtx;
-let (a, mctx) := x.run mctx;
-setMCtx mctx;
+let mctx ← getMCtx
+let (a, mctx) := x.run mctx
+setMCtx mctx
 pure a
 
 def instantiateLevelMVars (u : Level) : m Level :=
 liftMetaM $ liftStateMCtx $ MetavarContext.instantiateLevelMVars u
 
 def normalizeLevel (u : Level) : m Level :=
-liftMetaM do u ← instantiateLevelMVars u; pure u.normalize
+liftMetaM do let u ← instantiateLevelMVars u; pure u.normalize
 
 def assignLevelMVar (mvarId : MVarId) (u : Level) : m Unit :=
 modifyMCtx fun mctx => mctx.assignLevel mvarId u
@@ -951,7 +921,7 @@ def whnfD [MonadLiftT MetaM n] (e : Expr) : n Expr :=
 withTransparency TransparencyMode.default $ whnf e
 
 def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): m Unit := liftMetaM do
-env ← getEnv;
+let env ← getEnv
 match Compiler.setInlineAttribute env declName kind with
 | Except.ok env    => setEnv env
 | Except.error msg => throwError msg
@@ -959,10 +929,10 @@ match Compiler.setInlineAttribute env declName kind with
 private partial def instantiateForallAux (ps : Array Expr) : Nat → Expr → MetaM Expr
 | i, e =>
   if h : i < ps.size then do
-    let p := ps.get ⟨i, h⟩;
-    e ← whnf e;
+    let p := ps.get ⟨i, h⟩
+    let e ← whnf e
     match e with
-    | Expr.forallE _ _ b _ => instantiateForallAux (i+1) (b.instantiate1 p)
+    | Expr.forallE _ _ b _ => instantiateForallAux ps (i+1) (b.instantiate1 p)
     | _                    => throwError "invalid instantiateForall, too many parameters"
   else
     pure e
@@ -974,10 +944,10 @@ liftMetaM $ instantiateForallAux ps 0 e
 private partial def instantiateLambdaAux (ps : Array Expr) : Nat → Expr → MetaM Expr
 | i, e =>
   if h : i < ps.size then do
-    let p := ps.get ⟨i, h⟩;
-    e ← whnf e;
+    let p := ps.get ⟨i, h⟩
+    let e ← whnf e
     match e with
-    | Expr.lam _ _ b _ => instantiateLambdaAux (i+1) (b.instantiate1 p)
+    | Expr.lam _ _ b _ => instantiateLambdaAux ps (i+1) (b.instantiate1 p)
     | _                => throwError "invalid instantiateLambda, too many parameters"
   else
     pure e
@@ -989,40 +959,45 @@ liftMetaM $ instantiateLambdaAux ps 0 e
 
 /-- Return true iff `e` depends on the free variable `fvarId` -/
 def dependsOn (e : Expr) (fvarId : FVarId) : m Bool := liftMetaM do
-mctx ← getMCtx;
+let mctx ← getMCtx
 pure $ mctx.exprDependsOn e fvarId
 
 def ppExprImp (e : Expr) : MetaM Format := do
-env  ← getEnv;
-mctx ← getMCtx;
-lctx ← getLCtx;
-opts ← getOptions;
+let env  ← getEnv
+let mctx ← getMCtx
+let lctx ← getLCtx
+let opts ← getOptions
 liftIO $ Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts } e
 
 def ppExpr (e : Expr) : m Format :=
 liftMetaM $ ppExprImp e
 
 @[inline] protected def orelse {α} (x y : MetaM α) : MetaM α := do
-env  ← getEnv;
-mctx ← getMCtx;
-catch x (fun _ => do setEnv env; setMCtx mctx; y)
+let env  ← getEnv
+let mctx ← getMCtx
+try x catch _ => setEnv env; setMCtx mctx; y
 
-instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩
+instance {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩
 
 @[inline] private def orelseMergeErrorsImp {α} (x y : MetaM α)
   (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁)
   (mergeMsg : MessageData → MessageData → MessageData := fun m₁ m₂ => m₁ ++ Format.line ++ m₂)
   : MetaM α := do
-env  ← getEnv;
-mctx ← getMCtx;
-catch x fun ex => do
-  setEnv env; setMCtx mctx;
+let env  ← getEnv
+let mctx ← getMCtx
+try
+  x
+catch ex =>
+  setEnv env
+  setMCtx mctx
   match ex with
   | Exception.error ref₁ m₁ =>
-    catch y fun ex => match ex with
-    | Exception.error ref₂ m₂ => throw $ Exception.error (mergeRef ref₁ ref₂) (mergeMsg m₁ m₂)
-    | _ => throw ex
-  | _ => throw ex
+    try
+      y
+    catch
+      | Exception.error ref₂ m₂ => throw $ Exception.error (mergeRef ref₁ ref₂) (mergeMsg m₁ m₂)
+      | ex => throw ex
+  | ex => throw ex
 
 /--
   Similar to `orelse`, but merge errors. Note that internal errors are not caught.
@@ -1035,25 +1010,31 @@ catch x fun ex => do
 controlAt MetaM fun runInBase => orelseMergeErrorsImp (runInBase x) (runInBase y) mergeRef mergeMsg
 
 /-- Execute `x`, and apply `f` to the produced error message -/
-def mapErrorImp {α} (x : MetaM α) (f : MessageData → MessageData) : MetaM α :=
-catch x fun ex => match ex with
+def mapErrorImp {α} (x : MetaM α) (f : MessageData → MessageData) : MetaM α := do
+try
+  x
+catch
   | Exception.error ref msg => throw $ Exception.error ref $ f msg
-  | _ => throw ex
+  | ex => throw ex
 
 @[inline] def mapError {α m} [MonadControlT MetaM m] [Monad m] (x : m α) (f : MessageData → MessageData) : m α :=
 controlAt MetaM fun runInBase => mapErrorImp (runInBase x) f
 
 /-- `commitWhenSome? x` executes `x` and keep modifications when it returns `some a`. -/
 @[specialize] def commitWhenSome? {α} (x? : MetaM (Option α)) : MetaM (Option α) := do
-env  ← getEnv;
-mctx ← getMCtx;
-catch
-  (do
-    a? ← x?;
-    match a? with
-    | some a => pure a?
-    | none   => do setEnv env; setMCtx mctx; pure none)
-  (fun ex => do setEnv env; setMCtx mctx; throw ex)
+let env  ← getEnv
+let mctx ← getMCtx
+try
+  match (← x?) with
+  | some a => pure (some a)
+  | none   =>
+    setEnv env
+    setMCtx mctx
+    pure none
+catch ex =>
+  setEnv env
+  setMCtx mctx
+  throw ex
 
 end Methods
 end Meta
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 270cd7cc19..71f16441f6 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -15,6 +15,9 @@ import Lean.ParserCompiler.Attribute
 import Lean.Parser.Extension
 
 namespace Lean
+namespace Meta end Meta -- HACK for old frontend
+open Meta (MetaM) -- HACK for old frontend
+
 namespace ParserCompiler
 
 structure Context (α : Type) :=
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index cf51293976..88d3ef81a6 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -9,6 +9,8 @@ import Lean.PrettyPrinter.Formatter
 import Lean.Parser.Module
 
 namespace Lean
+namespace Meta end Meta -- HACK for old frontend
+open Meta (MetaM) -- HACK for old frontend
 
 def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
 Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env }