diff --git a/library/Init/Lean/AbstractMetavarContext.lean b/library/Init/Lean/AbstractMetavarContext.lean
deleted file mode 100644
index 0a98aaf084..0000000000
--- a/library/Init/Lean/AbstractMetavarContext.lean
+++ /dev/null
@@ -1,559 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Control.Reader
-import Init.Control.Conditional
-import Init.Data.Option
-import Init.Data.List
-import Init.Data.Nat
-import Init.Lean.LocalContext
-import Init.Lean.MonadCache
-import Init.Lean.NameGenerator
-
-/-
-- We have two kinds of metavariables in Lean: regular and temporary.
-
-- We use temporary metavariables during type class resolution,
-  matching the left-hand side of equations, etc.
-
-- During type class resolution and simplifier,
-  we use temporary metavariables which are cheaper to create and
-  dispose. Moreover, given a particular task using temporary
-  metavariables (e.g., matching the left-hand side of an equation),
-  we assume all metavariables share the same local context.
-
-- Each regular metavariable has a unique id, a user-facing name, a
-  local context, and a type. The term assigned to a metavariable must
-  only contain free variables in the local context.
-
-- A regular metavariable may be marked a synthetic. Synthetic
-  metavariables cannot be assigned by the unifier. The tactic
-  framework and elaborator are some of the modules responsible for
-  assigning synthetic metavariables.
-
-- When creating lambda/forall expressions, we need to convert/abstract
-  free variables and convert them to bound variables. Now, suppose we
-  a trying to create a lambda/forall expression by abstracting free
-  variables `xs` and a term `t[?m]` which contains a metavariable
-  `?m`, and the local context of `?m` contains `xs`. The term
-  `fun xs => t[?m]` will be ill-formed if we later assign a term `s` to `?m`,
-  and `s` contains free variables in `xs`. We address this issue by changing the free
-  variable abstraction procedure. We consider two cases: `?m` is not
-  synthetic, `?m` is synthetic. Assume the type of `?m` is `A`. Then,
-  in both cases we create an auxiliary metavariable `?n` with type
-  `forall xs => A`, and local context := local context of `?m` - `xs`.
-  In both cases, we produce the term `fun xs => t[?n xs]`
-
-  1- If `?m` is not synthetic, then we assign `?m := ?n xs`, and we produce the term
-     `fun xs => t[?n xs]`
-
-  2- If `?m` is synthetic, then we mark `?n` as a synthetic variable. However,
-     `?n` is managed by the metavariable context itself.
-     We say we have a "delayed assignment" `?n xs := ?m`
-     That is, after a term `s` is assigned to `?m`, and `s` does not
-     contain metavariables, we assign `fun xs => s` to `?n`.
-
-Gruesome details
-
-- When we create the type `forall xs => A` for `?n`, we may encounter
-  the same issue if `A` contains metavariables. So, the process above
-  is recursive. We claim it terminates because we keep creating new
-  metavariables with smaller local contexts.
-
-- The type of variables `xs` may contain metavariables, and we must
-  recursively apply the process above. Again, we claim the process
-  terminates because the metavariables is ocurring in the types of
-  `xs`, they must have smaller local contexts.
-
-- We can only assign `fun xs => s` to `?n` in case 2, the types
-  of `xs` must also not contain metavariables. To be precise, it is
-  sufficient they do not contain metavariables with local contexts
-  containing any of the `xs`s.
--/
-
-namespace Lean
-
-structure MetavarDecl :=
-(userName  : Name)
-(lctx      : LocalContext)
-(type      : Expr)
-(synthetic : Bool)
-
-namespace MetavarDecl
-
-instance : Inhabited MetavarDecl :=
-⟨⟨arbitrary _, arbitrary _, arbitrary _, false⟩⟩
-
-end MetavarDecl
-
-/--
-  A delayed assignment for a metavariable `?m`. It represents an assignment of the form
-  `?m := (fun fvars => val)`. The local context `lctx` provides the declarations for `fvars`.
-  Note that `fvars` may not be defined in the local context for `?m`. -/
-structure DelayedMetavarAssignment :=
-(lctx     : LocalContext)
-(fvars    : Array Expr)
-(val      : Expr)
-
-/--
-  Abstract interface for metavariable context objects.  The
-  `MetavarContext` is the main implementation and is used in the
-  elaborator and tactic framework.
-  The `TemporaryMetavariableContext` is used to implement the
-  type class resolution procedures and matching for rewriting rules.  -/
-class AbstractMetavarContext (σ : Type) :=
-(empty                : σ)
-(isReadOnlyLevelMVar  (mctx : σ) (mvarId : Name) : Bool)
-(getLevelAssignment   (mctx : σ) (mvarId : Name) : Option Level)
-(assignLevel          (mctx : σ) (mvarId : Name) (val : Level) : σ)
-(isReadOnlyExprMVar   (mctx : σ) (mvarId : Name) : Bool)
-(getExprAssignment    (mctx : σ) (mvarId : Name) : Option Expr)
-(assignExpr           (mctx : σ) (mvarId : Name) (val : Expr) : σ)
-(getDecl              (mctx : σ) (mvarId : Name) : MetavarDecl)
-(assignDelayed        (mctx : σ) (mvarId : Name) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : σ)
-(getDelayedAssignment (mctx : σ) (mvarId : Name) : Option DelayedMetavarAssignment)
-(eraseDelayed         (mctx : σ) (mvarId : Name) : σ)
-/- Supports auxiliary metavariables -/
-(auxMVarSupport       : Bool)
-/- Return `none` in case of failure, or if implementation does not support the creation of auxiliary metavariables. -/
-(mkAuxMVar            (mctx : σ) (mvarId : Name) (lctx : LocalContext) (type : Expr) (synthetic : Bool) : σ)
-
-namespace AbstractMetavarContext
-
-variables {σ : Type} [AbstractMetavarContext σ]
-
-@[inline] def isLevelAssigned (mctx : σ) (mvarId : Name) : Bool :=
-(getLevelAssignment mctx mvarId).isSome
-
-@[inline] def isExprAssigned (mctx : σ) (mvarId : Name) : Bool :=
-(getExprAssignment mctx mvarId).isSome
-
-/-- Return true iff the given level contains a non-readonly metavariable. -/
-def hasAssignableLevelMVar (mctx : σ) : Level → Bool
-| Level.succ lvl       => lvl.hasMVar && hasAssignableLevelMVar lvl
-| Level.max lvl₁ lvl₂  => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂)
-| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂)
-| Level.mvar mvarId    => !isReadOnlyLevelMVar mctx mvarId
-| Level.zero           => false
-| Level.param _        => false
-
-/-- Return true iff the given level contains an assigned metavariable. -/
-def hasAssignedLevelMVar (mctx : σ) : Level → Bool
-| Level.succ lvl       => lvl.hasMVar && hasAssignedLevelMVar lvl
-| Level.max lvl₁ lvl₂  => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)
-| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)
-| Level.mvar mvarId    => isLevelAssigned mctx mvarId
-| Level.zero           => false
-| Level.param _        => false
-
-/-- Return `true` iff expression contains assigned (level/expr) metavariables -/
-def hasAssignedMVar (mctx : σ) : Expr → Bool
-| Expr.const _ lvls    => lvls.any (hasAssignedLevelMVar mctx)
-| Expr.sort lvl        => hasAssignedLevelMVar mctx lvl
-| Expr.app f a         => (f.hasMVar && hasAssignedMVar f) || (a.hasMVar && hasAssignedMVar a)
-| Expr.letE _ t v b    => (t.hasMVar && hasAssignedMVar t) || (v.hasMVar && hasAssignedMVar v) || (b.hasMVar && hasAssignedMVar b)
-| Expr.forallE _ _ d b => (d.hasMVar && hasAssignedMVar d) || (b.hasMVar && hasAssignedMVar b)
-| Expr.lam _ _ d b     => (d.hasMVar && hasAssignedMVar d) || (b.hasMVar && hasAssignedMVar b)
-| Expr.fvar _          => false
-| Expr.bvar _          => false
-| Expr.lit _           => false
-| Expr.mdata _ e       => e.hasMVar && hasAssignedMVar e
-| Expr.proj _ _ e      => e.hasMVar && hasAssignedMVar e
-| Expr.mvar mvarId     => isExprAssigned mctx mvarId
-
-partial def instantiateLevelMVars : Level → StateM σ Level
-| lvl@(Level.succ lvl₁)      => do lvl₁ ← instantiateLevelMVars lvl₁; pure (Level.updateSucc! lvl lvl₁)
-| lvl@(Level.max lvl₁ lvl₂)  => do lvl₁ ← instantiateLevelMVars lvl₁; lvl₂ ← instantiateLevelMVars lvl₂; pure (Level.updateMax! lvl lvl₁ lvl₂)
-| lvl@(Level.imax lvl₁ lvl₂) => do lvl₁ ← instantiateLevelMVars lvl₁; lvl₂ ← instantiateLevelMVars lvl₂; pure (Level.updateIMax! lvl lvl₁ lvl₂)
-| lvl@(Level.mvar mvarId)    => do
-  mctx ← get;
-  match getLevelAssignment mctx mvarId with
-  | some newLvl =>
-    if !newLvl.hasMVar then pure newLvl
-    else do
-      newLvl' ← instantiateLevelMVars newLvl;
-      modify $ fun mctx => assignLevel mctx mvarId newLvl';
-      pure newLvl'
-  | none        => pure lvl
-| lvl => pure lvl
-
-namespace InstantiateExprMVars
-abbrev M (σ : Type) := StateM (WithHashMapCache Expr Expr σ)
-
-@[inline] def instantiateLevelMVars (lvl : Level) : M σ Level :=
-WithHashMapCache.fromState $ AbstractMetavarContext.instantiateLevelMVars lvl
-
-@[inline] def visit (f : Expr → M σ Expr) (e : Expr) : M σ Expr :=
-if !e.hasMVar then pure e else checkCache e f
-
-@[inline] def getMCtx : M σ σ :=
-do s ← get; pure s.state
-
-@[inline] def modifyCtx (f : σ → σ) : M σ Unit :=
-modify $ fun s => { state := f s.state, .. s }
-
-/--
-  Auxiliary function for `instantiateDelayed`.
-  `instantiateDelayed main lctx fvars i body` is used to create `fun fvars[0, i) => body`.
-  It fails if one of variable declarations in `fvars` still contains unassigned metavariables.
-
-  Pre: all expressions in `fvars` are `Expr.fvar`, and `lctx` contains their declarations. -/
-@[specialize] def instantiateDelayedAux (main : Expr → M σ Expr) (lctx : LocalContext) (fvars : Array Expr) : Nat → Expr → M σ (Option Expr)
-| 0,   b => pure b
-| i+1, b => do
-  let fvar := fvars.get! i;
-  match lctx.findFVar fvar with
-  | none => panic! "unknown free variable"
-  | some (LocalDecl.cdecl _ _ n ty bi)  => do
-    ty ← visit main ty;
-    if ty.hasMVar then pure none
-    else instantiateDelayedAux i (Expr.lam n bi (ty.abstractRange i fvars) b)
-  | some (LocalDecl.ldecl _ _ n ty val) => do
-    ty  ← visit main ty;
-    if ty.hasMVar then pure none
-    else do
-      val ← visit main val;
-      if val.hasMVar then pure none
-      else
-        let ty  := ty.abstractRange i fvars;
-        let val := val.abstractRange i fvars;
-        instantiateDelayedAux i (Expr.letE n ty val b)
-
-/-- Try to instantiate a delayed assignment. Return `none` (i.e., fail) if assignment still contains variables. -/
-@[inline] def instantiateDelayed (main : Expr → M σ Expr) (mvarId : Name) : DelayedMetavarAssignment → M σ (Option Expr)
-| { lctx := lctx, fvars := fvars, val := val } => do
-  newVal ← visit main val;
-  let fail : M σ (Option Expr) := do {
-     /- Join point for updating delayed assignment and failing -/
-     modifyCtx $ fun mctx => assignDelayed mctx mvarId lctx fvars newVal;
-     pure none
-  };
-  if newVal.hasMVar then fail
-  else do
-    /- Create `fun fvars => newVal`.
-       It fails if there is a one of the variable declarations in `fvars` still contain metavariables. -/
-    newE ← instantiateDelayedAux main lctx fvars fvars.size (newVal.abstract fvars);
-    match newE with
-    | none      => fail
-    | some newE => do
-      /- Succeeded. Thus, replace delayed assignment with a regular assignment. -/
-      modifyCtx $ fun mctx => assignExpr (eraseDelayed mctx mvarId) mvarId newE;
-      pure (some newE)
-
-/-- instantiateExprMVars main function -/
-partial def main : Expr → M σ Expr
-| e@(Expr.proj _ _ s)      => do s ← visit main s; pure (e.updateProj! s)
-| e@(Expr.forallE _ _ d b) => do d ← visit main d; b ← visit main b; pure (e.updateForallE! d b)
-| e@(Expr.lam _ _ d b)     => do d ← visit main d; b ← visit main b; pure (e.updateLambdaE! d b)
-| e@(Expr.letE _ t v b)    => do t ← visit main t; v ← visit main v; b ← visit main b; pure (e.updateLet! t v b)
-| e@(Expr.const _ lvls)    => do lvls ← lvls.mapM instantiateLevelMVars; pure (e.updateConst! lvls)
-| e@(Expr.sort lvl)        => do lvl ← instantiateLevelMVars lvl; pure (e.updateSort! lvl)
-| e@(Expr.mdata _ b)       => do b ← visit main b; pure (e.updateMData! b)
-| e@(Expr.app _ _)         => e.withAppRev $ fun f revArgs => do
-  let wasMVar := f.isMVar;
-  f ← visit main f;
-  if wasMVar && f.isLambda then
-    -- Some of the arguments in revArgs are irrelevant after we beta reduce.
-    visit main (f.betaRev revArgs)
-  else do
-    revArgs ← revArgs.mapM (visit main);
-    pure (mkAppRev f revArgs)
-| e@(Expr.mvar mvarId)     => checkCache e $ fun e => do
-  mctx ← getMCtx;
-  match getExprAssignment mctx mvarId with
-  | some newE => do
-    newE' ← visit main newE;
-    modifyCtx $ fun mctx => assignExpr mctx mvarId newE';
-    pure newE'
-  | none =>
-    /- A delayed assignment can be transformed into a regular assignment
-       as soon as all metavariables occurring in the assigned value have
-       been assigned. -/
-    match getDelayedAssignment mctx mvarId with
-    | some d => do
-       newE ← instantiateDelayed main mvarId d;
-       pure $ newE.getD e
-    | none   => pure e
-| e => pure e
-
-end InstantiateExprMVars
-
-def instantiateMVars (e : Expr) : StateM σ Expr :=
-if !e.hasMVar then pure e
-else WithHashMapCache.toState $ InstantiateExprMVars.main e
-
-namespace DependsOn
-
-abbrev M := StateM ExprSet
-
-@[inline] def visit (main : Expr → M Bool) (e : Expr) : M Bool :=
-if !e.hasMVar && !e.hasFVar then
-  pure false
-else do
-  s ← get;
-  if s.contains e then
-    pure false
-  else do
-    modify $ fun s => s.insert e;
-    main e
-
-@[specialize] partial def dep (mctx : σ) (p : Name → Bool) : Expr → M Bool
-| e@(Expr.proj _ _ s)      => visit dep s
-| e@(Expr.forallE _ _ d b) => visit dep d <||> visit dep b
-| e@(Expr.lam _ _ d b)     => visit dep d <||> visit dep b
-| e@(Expr.letE _ t v b)    => visit dep t <||> visit dep v <||> visit dep b
-| e@(Expr.mdata _ b)       => visit dep b
-| e@(Expr.app f a)         => visit dep a <||> if f.isApp then dep f else visit dep f
-| e@(Expr.mvar mvarId)     =>
-  match getExprAssignment mctx mvarId with
-  | some a => visit dep a
-  | none   =>
-    let lctx := (getDecl mctx mvarId).lctx;
-    pure $ lctx.any $ fun decl => p decl.name
-| e@(Expr.fvar fvarId)     => pure $ p fvarId
-| e                        => pure false
-
-@[inline] partial def main (mctx : σ) (p : Name → Bool) (e : Expr) : M Bool :=
-if !e.hasFVar && !e.hasMVar then pure false else dep mctx p e
-
-end DependsOn
-
-/--
-  Return `true` iff `e` depends on a free variable `x` s.t. `p x` is `true`.
-  For each metavariable `?m` occurring in `x`
-  1- If `?m := t`, then we visit `t` looking for `x`
-  2- If `?m` is unassigned, then we consider the worst case and check whether `x` is in the local context of `?m`.
-     This case is a "may dependency". That is, we may assign a term `t` to `?m` s.t. `t` contains `x`. -/
-@[inline] def exprDependsOn (mctx : σ) (p : Name → Bool) (e : Expr) : Bool :=
-(DependsOn.main mctx p e).run' {}
-
-/--
-  Similar to `exprDependsOn`, but checks the expressions in the given local declaration
-  depends on a free variable `x` s.t. `p x` is `true`. -/
-@[inline] def localDeclDependsOn (mctx : σ) (p : Name → Bool) : LocalDecl → Bool
-| LocalDecl.cdecl _ _ _ type _     => exprDependsOn mctx p type
-| LocalDecl.ldecl _ _ _ type value => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
-
-inductive MkBindingException
-| revertFailure (lctx : LocalContext) (toRevert : Array Expr) (decl : LocalDecl)
-| readOnlyMVar (mvarId : Name)
-| mkAuxMVarNotSupported
-
-namespace MkBindingException
-def toStr : MkBindingException → String
-| revertFailure lctx toRevert decl =>
-  "failed to revert "
-  ++ toString (toRevert.map (fun x => "'" ++ toString (lctx.findFVar x).get!.userName ++ "'"))
-  ++ ", '" ++ toString decl.userName ++ "' depends on them, and it is an auxiliary declaration created by the elaborator"
-  ++ " (possible solution: use tactic 'clear' to remove '" ++ toString decl.userName ++ "' from local context)"
-| readOnlyMVar _  => "failed to create binding due to read only metavariable"
-| mkAuxMVarNotSupported => "auxiliary metavariables are not supported"
-
-instance : HasToString MkBindingException := ⟨toStr⟩
-end MkBindingException
-
-namespace MkBinding
-
-/--
- `MkBinding` and `elimMVarDepsAux` are mutually recursive, but `cache` is only used at `elimMVarDepsAux`.
-  We use a single state object for convenience.
-
-  We have a `NameGenerator` because we need to generate fresh auxiliary metavariables.
--/
-structure MkBindingState (σ : Type) :=
-(mctx  : σ)
-(ngen  : NameGenerator)
-(cache : HashMap Expr Expr := {}) --
-
-abbrev M (σ : Type) := EStateM MkBindingException (MkBindingState σ)
-
-instance (σ) : MonadHashMapCacheAdapter Expr Expr (M σ) :=
-{ getCache    := do s ← get; pure s.cache,
-  modifyCache := fun f => modify $ fun s => { cache := f s.cache, .. s } }
-
-/-- Similar to `Expr.abstractRange`, but handles metavariables correctly.
-    It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not
-    contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.
-
-    `elimMVarDeps` is defined later in this file. -/
-@[inline] def abstractRange (elimMVarDeps : Array Expr → Expr → M σ Expr) (lctx : LocalContext) (xs : Array Expr) (i : Nat) (e : Expr) : M σ Expr :=
-do e ← elimMVarDeps xs e;
-   pure (e.abstractRange i xs)
-
-/-- Similar to `LocalContext.mkBinding`, but handles metavariables correctly. -/
-@[specialize] def mkBinding (isLambda : Bool) (elimMVarDeps : Array Expr → Expr → M σ Expr)
-                            (lctx : LocalContext) (xs : Array Expr) (e : Expr) : M σ Expr :=
-do e ← abstractRange elimMVarDeps lctx xs xs.size e;
-   xs.size.foldRevM
-    (fun i e =>
-      let x := xs.get! i;
-      match lctx.findFVar x with
-      | some (LocalDecl.cdecl _ _ n type bi) => do
-        type ← abstractRange elimMVarDeps lctx xs i type;
-        if isLambda then
-          pure $ Expr.lam n bi type e
-        else
-          pure $ Expr.forallE n bi type e
-      | some (LocalDecl.ldecl _ _ n type value) => do
-        type  ← abstractRange elimMVarDeps lctx xs i type;
-        value ← abstractRange elimMVarDeps lctx xs i value;
-        pure $ Expr.letE n type value e
-      | none => panic! "unknown free variable")
-   e
-
-@[inline] def mkLambda (elimMVarDeps : Array Expr → Expr → M σ Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M σ Expr :=
-mkBinding true elimMVarDeps lctx xs b
-
-@[inline] def mkForall (elimMVarDeps : Array Expr → Expr → M σ Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M σ Expr :=
-mkBinding false elimMVarDeps lctx xs b
-
-/-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/
-def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl :=
-let d : LocalDecl := (lctx.findFVar $ xs.get! 0).get!;
-xs.foldlFrom
-  (fun d x =>
-    let decl := (lctx.findFVar x).get!;
-    if decl.index < d.index then decl else d)
-  d 1
-
-/-- Given `toRevert` an array of free variables s.t. `lctx` contains their declarations,
-    return a new array of free variables that contains `toRevert` and all free variables
-    in `lctx` that may depend on `toRevert`.
-
-    Remark: the result is sorted by `LocalDecl` indices. -/
-def collectDeps (mctx : σ) (lctx : LocalContext) (toRevert : Array Expr) : Except MkBindingException (Array Expr) :=
-if toRevert.size == 0 then pure toRevert
-else
-  let minDecl := getLocalDeclWithSmallestIdx lctx toRevert;
-  lctx.foldlFromM
-    (fun newToRevert decl =>
-      if toRevert.any (fun x => decl.name == x.fvarId!) then
-        pure (newToRevert.push decl.toExpr)
-      else if localDeclDependsOn mctx (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) decl then
-        if decl.binderInfo.isAuxDecl then
-          throw (MkBindingException.revertFailure lctx toRevert decl)
-        else
-          pure (newToRevert.push decl.toExpr)
-      else
-        pure newToRevert)
-    (Array.mkEmpty toRevert.size)
-    minDecl
-
-/-- Create a new `LocalContext` by removing the free variables in `toRevert` from `lctx`.
-    We use this function when we create auxiliary metavariables at `elimMVarDepsAux`. -/
-def reduceLocalContext (lctx : LocalContext) (toRevert : Array Expr) : LocalContext :=
-toRevert.foldr
-  (fun x lctx => lctx.erase x.fvarId!)
-  lctx
-
-@[inline] def visit (f : Expr → M σ Expr) (e : Expr) : M σ Expr :=
-if !e.hasMVar then pure e else checkCache e f
-
-@[inline] def getMCtx : M σ σ :=
-do s ← get; pure s.mctx
-
-@[inline] def mkFreshId : M σ Name :=
-modifyGet $ fun s => (s.ngen.curr, { ngen := s.ngen.next, .. s})
-
-/-- Return free variables in `xs` that are in the local context `lctx` -/
-def getInScope (lctx : LocalContext) (xs : Array Expr) : Array Expr :=
-xs.foldl
-  (fun scope x =>
-    if lctx.contains x.fvarId! then
-      scope.push x
-    else
-      scope)
-  #[]
-
-/-- Execute `x` with an empty cache, and then restore the original cache. -/
-@[inline] def withFreshCache {α} (x : M σ α) : M σ α :=
-do cache ← modifyGet $ fun s => (s.cache, { cache := {}, .. s });
-   a ← x;
-   modify $ fun s => { cache := cache, .. s };
-   pure a
-
-@[inline] def mkForallAux (elimMVarDepsAux : Array Expr → Expr → M σ Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M σ Expr :=
-mkForall
-  (fun xs e =>
-    if !e.hasMVar then
-      pure e
-    else
-      -- The cached results at `elimMVarDepsAux` depend on `xs`. So, we must reset the cache.
-      withFreshCache $ elimMVarDepsAux xs e)
-  lctx xs b
-
-/-- Create an application `mvar ys` where `ys` are the free variables `xs` which are not let-declarations.
-    All free variables in `xs` are in the context `lctx`. -/
-def mkMVarApp (lctx : LocalContext) (mvar : Expr) (xs : Array Expr) : Expr :=
-xs.foldl (fun e x => if (lctx.findFVar x).get!.isLet then e else Expr.app e x) mvar
-
-partial def elimMVarDepsAux : Array Expr → Expr → M σ Expr
-| xs, e@(Expr.proj _ _ s)      => do s ← visit (elimMVarDepsAux xs) s; pure (e.updateProj! s)
-| xs, e@(Expr.forallE _ _ d b) => do d ← visit (elimMVarDepsAux xs) d; b ← visit (elimMVarDepsAux xs) b; pure (e.updateForallE! d b)
-| xs, e@(Expr.lam _ _ d b)     => do d ← visit (elimMVarDepsAux xs) d; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLambdaE! d b)
-| xs, e@(Expr.letE _ t v b)    => do t ← visit (elimMVarDepsAux xs) t; v ← visit (elimMVarDepsAux xs) v; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLet! t v b)
-| xs, e@(Expr.mdata _ b)       => do b ← visit (elimMVarDepsAux xs) b; pure (e.updateMData! b)
-| xs, e@(Expr.app _ _)         => e.withAppRev $ fun f revArgs => do
-  f ← visit (elimMVarDepsAux xs) f;
-  revArgs ← revArgs.mapM (visit (elimMVarDepsAux xs));
-  pure (mkAppRev f revArgs)
-| xs, e@(Expr.mvar mvarId) => do
-  mctx ← getMCtx;
-  match getExprAssignment mctx mvarId with
-  | some a => visit (elimMVarDepsAux xs) a
-  | none   =>
-    let mvarDecl := getDecl mctx mvarId;
-    let mvarLCtx := mvarDecl.lctx;
-    let toRevert := getInScope mvarLCtx xs;
-    if toRevert.size == 0 then
-      pure e
-    else if isReadOnlyExprMVar mctx mvarId then
-      throw $ MkBindingException.readOnlyMVar mvarId
-    else if !auxMVarSupport σ then
-      throw MkBindingException.mkAuxMVarNotSupported
-    else
-      match collectDeps mctx mvarLCtx toRevert with
-      | Except.error ex    => throw ex
-      | Except.ok toRevert => do
-        let newMVarLCtx   := reduceLocalContext mvarLCtx toRevert;
-        newMVarType ← mkForallAux (fun xs e => elimMVarDepsAux xs e) mvarLCtx toRevert mvarDecl.type;
-        mctx        ← getMCtx;
-        newMVarId   ← mkFreshId;
-        let mctx := mkAuxMVar mctx newMVarId newMVarLCtx newMVarType mvarDecl.synthetic;
-        modify $ fun s => { mctx := mctx, .. s };
-        let newMVar := Expr.mvar newMVarId;
-        let result  := mkMVarApp mvarLCtx newMVar toRevert;
-        if mvarDecl.synthetic then
-          modify (fun s => { mctx := assignDelayed s.mctx newMVarId mvarLCtx toRevert e, .. s })
-        else
-          modify (fun s => { mctx := assignExpr s.mctx mvarId result, .. s });
-        pure result
-| xs, e => pure e
-
-partial def elimMVarDeps (xs : Array Expr) (e : Expr) : M σ Expr :=
-if !e.hasMVar then
-  pure e
-else
-  withFreshCache $ elimMVarDepsAux xs e
-
-end MkBinding
-
-def mkBinding (isLambda : Bool) (mctx : σ) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr) : Except MkBindingException (σ × NameGenerator × Expr) :=
-match (MkBinding.mkBinding isLambda MkBinding.elimMVarDeps lctx xs e).run { mctx := mctx, ngen := ngen } with
-| EStateM.Result.ok e s      => Except.ok (s.mctx, s.ngen, e)
-| EStateM.Result.error err _ => Except.error err
-
-@[inline] def mkLambda (mctx : σ) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr) : Except MkBindingException (σ × NameGenerator × Expr) :=
-mkBinding true mctx ngen lctx xs e
-
-@[inline] def mkForall (mctx : σ) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr) : Except MkBindingException (σ × NameGenerator × Expr) :=
-mkBinding false mctx ngen lctx xs e
-
-end AbstractMetavarContext
-
-export AbstractMetavarContext (MkBindingException)
-
-end Lean
diff --git a/library/Init/Lean/MetavarContext.lean b/library/Init/Lean/MetavarContext.lean
index e25684202c..90f46b151f 100644
--- a/library/Init/Lean/MetavarContext.lean
+++ b/library/Init/Lean/MetavarContext.lean
@@ -4,11 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.AbstractMetavarContext
+import Init.Control.Reader
+import Init.Control.Conditional
+import Init.Data.Option
+import Init.Data.List
+import Init.Data.Nat
+import Init.Lean.LocalContext
+import Init.Lean.MonadCache
+import Init.Lean.NameGenerator
 
 namespace Lean
 
+structure MetavarDecl :=
+(userName  : Name := Name.anonymous)
+(lctx      : LocalContext)
+(type      : Expr)
+(depth     : Nat)
+(synthetic : Bool)
+
+namespace MetavarDecl
+instance : Inhabited MetavarDecl := ⟨{ lctx := arbitrary _, type := arbitrary _, depth := 0, synthetic := false }⟩
+end MetavarDecl
+
+structure DelayedMetavarAssignment :=
+(lctx     : LocalContext)
+(fvars    : Array Expr)
+(val      : Expr)
+
 structure MetavarContext :=
+(depth       : Nat := 0)
+(lDepth      : PersistentHashMap Name Nat := {})
 (decls       : PersistentHashMap Name MetavarDecl := {})
 (lAssignment : PersistentHashMap Name Level := {})
 (eAssignment : PersistentHashMap Name Expr := {})
@@ -26,8 +51,14 @@ fun _ => {}
    It is used to implement actions in the monads `Elab` and `Tactic`.
    It should not be used directly since the argument `(mvarId : Name)` is assumed to be "unique". -/
 @[export lean_metavar_ctx_mk_decl]
-def mkDecl (m : MetavarContext) (mvarId : Name) (userName : Name) (lctx : LocalContext) (type : Expr) (synthetic : Bool := false) : MetavarContext :=
-{ decls := m.decls.insert mvarId { userName := userName, lctx := lctx, type := type, synthetic := synthetic }, .. m }
+def mkDecl (mctx : MetavarContext) (mvarId : Name) (userName : Name) (lctx : LocalContext) (type : Expr) (synthetic : Bool := false) : MetavarContext :=
+{ decls := mctx.decls.insert mvarId {
+    userName  := userName,
+    lctx      := lctx,
+    type      := type,
+    depth     := mctx.depth,
+    synthetic := synthetic },
+  .. mctx }
 
 @[export lean_metavar_ctx_find_decl]
 def findDecl (m : MetavarContext) (mvarId : Name) : Option MetavarDecl :=
@@ -78,44 +109,436 @@ m.dAssignment.contains mvarId
 def eraseDelayed (m : MetavarContext) (mvarId : Name) : MetavarContext :=
 { dAssignment := m.dAssignment.erase mvarId, .. m }
 
-/- Remark: the following instance assumes all metavariables can be updated. -/
-instance metavarContextIsAbstractMetavarContext : AbstractMetavarContext MetavarContext :=
-{ empty                := {},
-  isReadOnlyLevelMVar  := fun _ _ => false,
-  getLevelAssignment   := MetavarContext.getLevelAssignment,
-  assignLevel          := MetavarContext.assignLevel,
-  isReadOnlyExprMVar   := fun _ _ => false,
-  getExprAssignment    := MetavarContext.getExprAssignment,
-  assignExpr           := MetavarContext.assignExpr,
-  getDecl              := MetavarContext.getDecl,
-  assignDelayed        := MetavarContext.assignDelayed,
-  getDelayedAssignment := MetavarContext.getDelayedAssignment,
-  eraseDelayed         := MetavarContext.eraseDelayed,
-  auxMVarSupport       := true,
-  mkAuxMVar            := fun mctx mvarId lctx type synthetic => MetavarContext.mkDecl mctx mvarId Name.anonymous lctx type synthetic
-}
+def isLevelAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
+match mctx.lDepth.find mvarId with
+| some d => d == mctx.depth
+| _      => panic! "unknown universe metavariable"
 
-/-- Return `true` iff `lvl` contains assigned level metavariables -/
-@[inline] def hasAssignedLevelMVar (m : MetavarContext) (lvl : Level) : Bool :=
-AbstractMetavarContext.hasAssignedLevelMVar m lvl
+def isExprAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
+let decl := mctx.getDecl mvarId;
+decl.depth == mctx.depth
 
-/-- Return `true` iff `e` contains assigned (level/expr) metavariables -/
-@[inline] def hasAssignedMVar (m : MetavarContext) (e : Expr) : Bool :=
-AbstractMetavarContext.hasAssignedMVar m e
+/-- Return true iff the given level contains an assigned metavariable. -/
+def hasAssignedLevelMVar (mctx : MetavarContext) : Level → Bool
+| Level.succ lvl       => lvl.hasMVar && hasAssignedLevelMVar lvl
+| Level.max lvl₁ lvl₂  => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)
+| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignedLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignedLevelMVar lvl₂)
+| Level.mvar mvarId    => mctx.isLevelAssigned mvarId
+| Level.zero           => false
+| Level.param _        => false
 
-@[inline] def instantiateLevelMVars (m : MetavarContext) (lvl : Level) : Level × MetavarContext :=
-AbstractMetavarContext.instantiateLevelMVars lvl m
+/-- Return `true` iff expression contains assigned (level/expr) metavariables -/
+def hasAssignedMVar (mctx : MetavarContext) : Expr → Bool
+| Expr.const _ lvls    => lvls.any (hasAssignedLevelMVar mctx)
+| Expr.sort lvl        => hasAssignedLevelMVar mctx lvl
+| Expr.app f a         => (f.hasMVar && hasAssignedMVar f) || (a.hasMVar && hasAssignedMVar a)
+| Expr.letE _ t v b    => (t.hasMVar && hasAssignedMVar t) || (v.hasMVar && hasAssignedMVar v) || (b.hasMVar && hasAssignedMVar b)
+| Expr.forallE _ _ d b => (d.hasMVar && hasAssignedMVar d) || (b.hasMVar && hasAssignedMVar b)
+| Expr.lam _ _ d b     => (d.hasMVar && hasAssignedMVar d) || (b.hasMVar && hasAssignedMVar b)
+| Expr.fvar _          => false
+| Expr.bvar _          => false
+| Expr.lit _           => false
+| Expr.mdata _ e       => e.hasMVar && hasAssignedMVar e
+| Expr.proj _ _ e      => e.hasMVar && hasAssignedMVar e
+| Expr.mvar mvarId     => mctx.isExprAssigned mvarId
 
-@[inline] def instantiateMVars (m : MetavarContext) (e : Expr) : Expr × MetavarContext :=
-AbstractMetavarContext.instantiateMVars e m
+/-- Return true iff the given level contains a metavariable that can be assigned. -/
+def hasAssignableLevelMVar (mctx : MetavarContext) : Level → Bool
+| Level.succ lvl       => lvl.hasMVar && hasAssignableLevelMVar lvl
+| Level.max lvl₁ lvl₂  => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂)
+| Level.imax lvl₁ lvl₂ => (lvl₁.hasMVar && hasAssignableLevelMVar lvl₁) || (lvl₂.hasMVar && hasAssignableLevelMVar lvl₂)
+| Level.mvar mvarId    => mctx.isLevelAssignable mvarId
+| Level.zero           => false
+| Level.param _        => false
 
-@[inline] def mkLambda (m : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
-                       : Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
-AbstractMetavarContext.mkLambda m ngen lctx xs e
+private partial def instantiateLevelMVarsAux : Level → StateM MetavarContext Level
+| lvl@(Level.succ lvl₁)      => do lvl₁ ← instantiateLevelMVarsAux lvl₁; pure (Level.updateSucc! lvl lvl₁)
+| lvl@(Level.max lvl₁ lvl₂)  => do lvl₁ ← instantiateLevelMVarsAux lvl₁; lvl₂ ← instantiateLevelMVarsAux lvl₂; pure (Level.updateMax! lvl lvl₁ lvl₂)
+| lvl@(Level.imax lvl₁ lvl₂) => do lvl₁ ← instantiateLevelMVarsAux lvl₁; lvl₂ ← instantiateLevelMVarsAux lvl₂; pure (Level.updateIMax! lvl lvl₁ lvl₂)
+| lvl@(Level.mvar mvarId)    => do
+  mctx ← get;
+  match getLevelAssignment mctx mvarId with
+  | some newLvl =>
+    if !newLvl.hasMVar then pure newLvl
+    else do
+      newLvl' ← instantiateLevelMVarsAux newLvl;
+      modify $ fun mctx => mctx.assignLevel mvarId newLvl';
+      pure newLvl'
+  | none        => pure lvl
+| lvl => pure lvl
 
-@[inline] def mkForall (m : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
-                       : Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
-AbstractMetavarContext.mkForall m ngen lctx xs e
+namespace InstantiateExprMVars
+private abbrev M := StateM (WithHashMapCache Expr Expr MetavarContext)
+
+@[inline] private def instantiateLevelMVars (lvl : Level) : M Level :=
+WithHashMapCache.fromState $ instantiateLevelMVarsAux lvl
+
+@[inline] private def visit (f : Expr → M Expr) (e : Expr) : M Expr :=
+if !e.hasMVar then pure e else checkCache e f
+
+@[inline] private def getMCtx : M MetavarContext :=
+do s ← get; pure s.state
+
+@[inline] private def modifyCtx (f : MetavarContext → MetavarContext) : M Unit :=
+modify $ fun s => { state := f s.state, .. s }
+
+/--
+  Auxiliary function for `instantiateDelayed`.
+  `instantiateDelayed main lctx fvars i body` is used to create `fun fvars[0, i) => body`.
+  It fails if one of variable declarations in `fvars` still contains unassigned metavariables.
+
+  Pre: all expressions in `fvars` are `Expr.fvar`, and `lctx` contains their declarations. -/
+@[specialize] private def instantiateDelayedAux (main : Expr → M Expr) (lctx : LocalContext) (fvars : Array Expr) : Nat → Expr → M (Option Expr)
+| 0,   b => pure b
+| i+1, b => do
+  let fvar := fvars.get! i;
+  match lctx.findFVar fvar with
+  | none => panic! "unknown free variable"
+  | some (LocalDecl.cdecl _ _ n ty bi)  => do
+    ty ← visit main ty;
+    if ty.hasMVar then pure none
+    else instantiateDelayedAux i (Expr.lam n bi (ty.abstractRange i fvars) b)
+  | some (LocalDecl.ldecl _ _ n ty val) => do
+    ty  ← visit main ty;
+    if ty.hasMVar then pure none
+    else do
+      val ← visit main val;
+      if val.hasMVar then pure none
+      else
+        let ty  := ty.abstractRange i fvars;
+        let val := val.abstractRange i fvars;
+        instantiateDelayedAux i (Expr.letE n ty val b)
+
+/-- Try to instantiate a delayed assignment. Return `none` (i.e., fail) if assignment still contains variables. -/
+@[inline] private def instantiateDelayed (main : Expr → M Expr) (mvarId : Name) : DelayedMetavarAssignment → M (Option Expr)
+| { lctx := lctx, fvars := fvars, val := val } => do
+  newVal ← visit main val;
+  let fail : M (Option Expr) := do {
+     /- Join point for updating delayed assignment and failing -/
+     modifyCtx $ fun mctx => assignDelayed mctx mvarId lctx fvars newVal;
+     pure none
+  };
+  if newVal.hasMVar then fail
+  else do
+    /- Create `fun fvars => newVal`.
+       It fails if there is a one of the variable declarations in `fvars` still contain metavariables. -/
+    newE ← instantiateDelayedAux main lctx fvars fvars.size (newVal.abstract fvars);
+    match newE with
+    | none      => fail
+    | some newE => do
+      /- Succeeded. Thus, replace delayed assignment with a regular assignment. -/
+      modifyCtx $ fun mctx => assignExpr (eraseDelayed mctx mvarId) mvarId newE;
+      pure (some newE)
+
+/-- instantiateExprMVars main function -/
+partial def main : Expr → M Expr
+| e@(Expr.proj _ _ s)      => do s ← visit main s; pure (e.updateProj! s)
+| e@(Expr.forallE _ _ d b) => do d ← visit main d; b ← visit main b; pure (e.updateForallE! d b)
+| e@(Expr.lam _ _ d b)     => do d ← visit main d; b ← visit main b; pure (e.updateLambdaE! d b)
+| e@(Expr.letE _ t v b)    => do t ← visit main t; v ← visit main v; b ← visit main b; pure (e.updateLet! t v b)
+| e@(Expr.const _ lvls)    => do lvls ← lvls.mapM instantiateLevelMVars; pure (e.updateConst! lvls)
+| e@(Expr.sort lvl)        => do lvl ← instantiateLevelMVars lvl; pure (e.updateSort! lvl)
+| e@(Expr.mdata _ b)       => do b ← visit main b; pure (e.updateMData! b)
+| e@(Expr.app _ _)         => e.withAppRev $ fun f revArgs => do
+  let wasMVar := f.isMVar;
+  f ← visit main f;
+  if wasMVar && f.isLambda then
+    -- Some of the arguments in revArgs are irrelevant after we beta reduce.
+    visit main (f.betaRev revArgs)
+  else do
+    revArgs ← revArgs.mapM (visit main);
+    pure (mkAppRev f revArgs)
+| e@(Expr.mvar mvarId)     => checkCache e $ fun e => do
+  mctx ← getMCtx;
+  match mctx.getExprAssignment mvarId with
+  | some newE => do
+    newE' ← visit main newE;
+    modifyCtx $ fun mctx => mctx.assignExpr mvarId newE';
+    pure newE'
+  | none =>
+    /- A delayed assignment can be transformed into a regular assignment
+       as soon as all metavariables occurring in the assigned value have
+       been assigned. -/
+    match mctx.getDelayedAssignment mvarId with
+    | some d => do
+       newE ← instantiateDelayed main mvarId d;
+       pure $ newE.getD e
+    | none   => pure e
+| e => pure e
+
+end InstantiateExprMVars
+
+def instantiateMVars (mctx : MetavarContext) (e : Expr) : Expr × MetavarContext :=
+if !e.hasMVar then (e, mctx)
+else (WithHashMapCache.toState $ InstantiateExprMVars.main e).run mctx
+
+namespace DependsOn
+
+private abbrev M := StateM ExprSet
+
+@[inline] private def visit (main : Expr → M Bool) (e : Expr) : M Bool :=
+if !e.hasMVar && !e.hasFVar then
+  pure false
+else do
+  s ← get;
+  if s.contains e then
+    pure false
+  else do
+    modify $ fun s => s.insert e;
+    main e
+
+@[specialize] private partial def dep (mctx : MetavarContext) (p : Name → Bool) : Expr → M Bool
+| e@(Expr.proj _ _ s)      => visit dep s
+| e@(Expr.forallE _ _ d b) => visit dep d <||> visit dep b
+| e@(Expr.lam _ _ d b)     => visit dep d <||> visit dep b
+| e@(Expr.letE _ t v b)    => visit dep t <||> visit dep v <||> visit dep b
+| e@(Expr.mdata _ b)       => visit dep b
+| e@(Expr.app f a)         => visit dep a <||> if f.isApp then dep f else visit dep f
+| e@(Expr.mvar mvarId)     =>
+  match mctx.getExprAssignment mvarId with
+  | some a => visit dep a
+  | none   =>
+    let lctx := (mctx.getDecl mvarId).lctx;
+    pure $ lctx.any $ fun decl => p decl.name
+| e@(Expr.fvar fvarId)     => pure $ p fvarId
+| e                        => pure false
+
+@[inline] partial def main (mctx : MetavarContext) (p : Name → Bool) (e : Expr) : M Bool :=
+if !e.hasFVar && !e.hasMVar then pure false else dep mctx p e
+
+end DependsOn
+
+/--
+  Return `true` iff `e` depends on a free variable `x` s.t. `p x` is `true`.
+  For each metavariable `?m` occurring in `x`
+  1- If `?m := t`, then we visit `t` looking for `x`
+  2- If `?m` is unassigned, then we consider the worst case and check whether `x` is in the local context of `?m`.
+     This case is a "may dependency". That is, we may assign a term `t` to `?m` s.t. `t` contains `x`. -/
+@[inline] def exprDependsOn (mctx : MetavarContext) (p : Name → Bool) (e : Expr) : Bool :=
+(DependsOn.main mctx p e).run' {}
+
+/--
+  Similar to `exprDependsOn`, but checks the expressions in the given local declaration
+  depends on a free variable `x` s.t. `p x` is `true`. -/
+@[inline] def localDeclDependsOn (mctx : MetavarContext) (p : Name → Bool) : LocalDecl → Bool
+| LocalDecl.cdecl _ _ _ type _     => exprDependsOn mctx p type
+| LocalDecl.ldecl _ _ _ type value => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
+
+inductive MkBindingException
+| revertFailure (lctx : LocalContext) (toRevert : Array Expr) (decl : LocalDecl)
+| readOnlyMVar (mvarId : Name)
+| mkAuxMVarNotSupported
+
+namespace MkBindingException
+def toStr : MkBindingException → String
+| revertFailure lctx toRevert decl =>
+  "failed to revert "
+  ++ toString (toRevert.map (fun x => "'" ++ toString (lctx.findFVar x).get!.userName ++ "'"))
+  ++ ", '" ++ toString decl.userName ++ "' depends on them, and it is an auxiliary declaration created by the elaborator"
+  ++ " (possible solution: use tactic 'clear' to remove '" ++ toString decl.userName ++ "' from local context)"
+| readOnlyMVar mvarId   => "failed to create binding due to read only metavariable " ++ toString mvarId
+| mkAuxMVarNotSupported => "auxiliary metavariables are not supported"
+
+instance : HasToString MkBindingException := ⟨toStr⟩
+end MkBindingException
+
+namespace MkBinding
+
+/--
+ `MkBinding` and `elimMVarDepsAux` are mutually recursive, but `cache` is only used at `elimMVarDepsAux`.
+  We use a single state object for convenience.
+
+  We have a `NameGenerator` because we need to generate fresh auxiliary metavariables.
+-/
+structure MkBindingState :=
+(mctx  : MetavarContext)
+(ngen  : NameGenerator)
+(cache : HashMap Expr Expr := {}) --
+
+private abbrev M := EStateM MkBindingException MkBindingState
+
+instance : MonadHashMapCacheAdapter Expr Expr M :=
+{ getCache    := do s ← get; pure s.cache,
+  modifyCache := fun f => modify $ fun s => { cache := f s.cache, .. s } }
+
+/-- Similar to `Expr.abstractRange`, but handles metavariables correctly.
+    It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not
+    contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.
+
+    `elimMVarDeps` is defined later in this file. -/
+@[inline] private def abstractRange (elimMVarDeps : Array Expr → Expr → M Expr) (lctx : LocalContext) (xs : Array Expr) (i : Nat) (e : Expr) : M Expr :=
+do e ← elimMVarDeps xs e;
+   pure (e.abstractRange i xs)
+
+/-- Similar to `LocalContext.mkBinding`, but handles metavariables correctly. -/
+@[specialize] def mkBinding (isLambda : Bool) (elimMVarDeps : Array Expr → Expr → M Expr)
+                            (lctx : LocalContext) (xs : Array Expr) (e : Expr) : M Expr :=
+do e ← abstractRange elimMVarDeps lctx xs xs.size e;
+   xs.size.foldRevM
+    (fun i e =>
+      let x := xs.get! i;
+      match lctx.findFVar x with
+      | some (LocalDecl.cdecl _ _ n type bi) => do
+        type ← abstractRange elimMVarDeps lctx xs i type;
+        if isLambda then
+          pure $ Expr.lam n bi type e
+        else
+          pure $ Expr.forallE n bi type e
+      | some (LocalDecl.ldecl _ _ n type value) => do
+        type  ← abstractRange elimMVarDeps lctx xs i type;
+        value ← abstractRange elimMVarDeps lctx xs i value;
+        pure $ Expr.letE n type value e
+      | none => panic! "unknown free variable")
+   e
+
+@[inline] private def mkLambda (elimMVarDeps : Array Expr → Expr → M Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M Expr :=
+mkBinding true elimMVarDeps lctx xs b
+
+@[inline] private def mkForall (elimMVarDeps : Array Expr → Expr → M Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M Expr :=
+mkBinding false elimMVarDeps lctx xs b
+
+/-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/
+private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl :=
+let d : LocalDecl := (lctx.findFVar $ xs.get! 0).get!;
+xs.foldlFrom
+  (fun d x =>
+    let decl := (lctx.findFVar x).get!;
+    if decl.index < d.index then decl else d)
+  d 1
+
+/-- Given `toRevert` an array of free variables s.t. `lctx` contains their declarations,
+    return a new array of free variables that contains `toRevert` and all free variables
+    in `lctx` that may depend on `toRevert`.
+
+    Remark: the result is sorted by `LocalDecl` indices. -/
+private def collectDeps (mctx : MetavarContext) (lctx : LocalContext) (toRevert : Array Expr) : Except MkBindingException (Array Expr) :=
+if toRevert.size == 0 then pure toRevert
+else
+  let minDecl := getLocalDeclWithSmallestIdx lctx toRevert;
+  lctx.foldlFromM
+    (fun newToRevert decl =>
+      if toRevert.any (fun x => decl.name == x.fvarId!) then
+        pure (newToRevert.push decl.toExpr)
+      else if localDeclDependsOn mctx (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) decl then
+        if decl.binderInfo.isAuxDecl then
+          throw (MkBindingException.revertFailure lctx toRevert decl)
+        else
+          pure (newToRevert.push decl.toExpr)
+      else
+        pure newToRevert)
+    (Array.mkEmpty toRevert.size)
+    minDecl
+
+/-- Create a new `LocalContext` by removing the free variables in `toRevert` from `lctx`.
+    We use this function when we create auxiliary metavariables at `elimMVarDepsAux`. -/
+private def reduceLocalContext (lctx : LocalContext) (toRevert : Array Expr) : LocalContext :=
+toRevert.foldr
+  (fun x lctx => lctx.erase x.fvarId!)
+  lctx
+
+@[inline] private def visit (f : Expr → M Expr) (e : Expr) : M Expr :=
+if !e.hasMVar then pure e else checkCache e f
+
+@[inline] private def getMCtx : M MetavarContext :=
+do s ← get; pure s.mctx
+
+/-- Return free variables in `xs` that are in the local context `lctx` -/
+private def getInScope (lctx : LocalContext) (xs : Array Expr) : Array Expr :=
+xs.foldl
+  (fun scope x =>
+    if lctx.contains x.fvarId! then
+      scope.push x
+    else
+      scope)
+  #[]
+
+/-- Execute `x` with an empty cache, and then restore the original cache. -/
+@[inline] private def withFreshCache {α} (x : M α) : M α :=
+do cache ← modifyGet $ fun s => (s.cache, { cache := {}, .. s });
+   a ← x;
+   modify $ fun s => { cache := cache, .. s };
+   pure a
+
+@[inline] private def mkForallAux (elimMVarDepsAux : Array Expr → Expr → M Expr) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : M Expr :=
+mkForall
+  (fun xs e =>
+    if !e.hasMVar then
+      pure e
+    else
+      -- The cached results at `elimMVarDepsAux` depend on `xs`. So, we must reset the cache.
+      withFreshCache $ elimMVarDepsAux xs e)
+  lctx xs b
+
+/-- Create an application `mvar ys` where `ys` are the free variables `xs` which are not let-declarations.
+    All free variables in `xs` are in the context `lctx`. -/
+private def mkMVarApp (lctx : LocalContext) (mvar : Expr) (xs : Array Expr) : Expr :=
+xs.foldl (fun e x => if (lctx.findFVar x).get!.isLet then e else Expr.app e x) mvar
+
+private def mkAuxMVar (lctx : LocalContext) (type : Expr) (synthetic : Bool) : M Name :=
+do s ← get;
+   let mvarId := s.ngen.curr;
+   modify $ fun s => { mctx := s.mctx.mkDecl mvarId Name.anonymous lctx type synthetic, ngen := s.ngen.next, .. s };
+   pure mvarId
+
+private partial def elimMVarDepsAux : Array Expr → Expr → M Expr
+| xs, e@(Expr.proj _ _ s)      => do s ← visit (elimMVarDepsAux xs) s; pure (e.updateProj! s)
+| xs, e@(Expr.forallE _ _ d b) => do d ← visit (elimMVarDepsAux xs) d; b ← visit (elimMVarDepsAux xs) b; pure (e.updateForallE! d b)
+| xs, e@(Expr.lam _ _ d b)     => do d ← visit (elimMVarDepsAux xs) d; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLambdaE! d b)
+| xs, e@(Expr.letE _ t v b)    => do t ← visit (elimMVarDepsAux xs) t; v ← visit (elimMVarDepsAux xs) v; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLet! t v b)
+| xs, e@(Expr.mdata _ b)       => do b ← visit (elimMVarDepsAux xs) b; pure (e.updateMData! b)
+| xs, e@(Expr.app _ _)         => e.withAppRev $ fun f revArgs => do
+  f ← visit (elimMVarDepsAux xs) f;
+  revArgs ← revArgs.mapM (visit (elimMVarDepsAux xs));
+  pure (mkAppRev f revArgs)
+| xs, e@(Expr.mvar mvarId) => do
+  mctx ← getMCtx;
+  match mctx.getExprAssignment mvarId with
+  | some a => visit (elimMVarDepsAux xs) a
+  | none   =>
+    let mvarDecl := mctx.getDecl mvarId;
+    let mvarLCtx := mvarDecl.lctx;
+    let toRevert := getInScope mvarLCtx xs;
+    if toRevert.size == 0 then
+      pure e
+    else if !mctx.isExprAssignable mvarId then
+      throw $ MkBindingException.readOnlyMVar mvarId
+    else
+      match collectDeps mctx mvarLCtx toRevert with
+      | Except.error ex    => throw ex
+      | Except.ok toRevert => do
+        let newMVarLCtx   := reduceLocalContext mvarLCtx toRevert;
+        newMVarType ← mkForallAux (fun xs e => elimMVarDepsAux xs e) mvarLCtx toRevert mvarDecl.type;
+        newMVarId   ← mkAuxMVar newMVarLCtx newMVarType mvarDecl.synthetic;
+        let newMVar := Expr.mvar newMVarId;
+        let result  := mkMVarApp mvarLCtx newMVar toRevert;
+        if mvarDecl.synthetic then
+          modify (fun s => { mctx := assignDelayed s.mctx newMVarId mvarLCtx toRevert e, .. s })
+        else
+          modify (fun s => { mctx := assignExpr s.mctx mvarId result, .. s });
+        pure result
+| xs, e => pure e
+
+partial def elimMVarDeps (xs : Array Expr) (e : Expr) : M Expr :=
+if !e.hasMVar then
+  pure e
+else
+  withFreshCache $ elimMVarDepsAux xs e
+
+end MkBinding
+
+def mkBinding (isLambda : Bool) (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
+    : Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
+match (MkBinding.mkBinding isLambda MkBinding.elimMVarDeps lctx xs e).run { mctx := mctx, ngen := ngen } with
+| EStateM.Result.ok e s      => Except.ok (s.mctx, s.ngen, e)
+| EStateM.Result.error err _ => Except.error err
+
+@[inline] def mkLambda (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
+    : Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
+mkBinding true mctx ngen lctx xs e
+
+@[inline] def mkForall (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
+    : Except MkBindingException (MetavarContext × NameGenerator × Expr) :=
+mkBinding false mctx ngen lctx xs e
 
 end MetavarContext
 end Lean
diff --git a/library/Init/Lean/TmpMetavarContext.lean b/library/Init/Lean/TmpMetavarContext.lean
deleted file mode 100644
index dcecd9b7ec..0000000000
--- a/library/Init/Lean/TmpMetavarContext.lean
+++ /dev/null
@@ -1,132 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Lean.MetavarContext
-
-namespace Lean
-/--
-  Several procedures (e.g., type class resolution, simplifier) need
-  to create metavariables that are needed for a short period of time.
-  For example, when applying a simplification lemma such as
-  ```
-  forall x, f x x = x
-  ```
-  to a subterm `t`, we need need to check whether the term
-  `t` is an instance of the pattern `f ?x ?x`, where `?x` is a fresh metavariable.
-  That is, we need to find an assignment for `?x` such that `t`
-  and `f ?x ?x` become definitionally equal. If the assignment is found,
-  we replace the term `t` with the term assigned to `?x`. After that,
-  we don't need the metavariable `?x` anymore. We don't want to
-  use regular metavariables for this operation since we don't want
-  to waste time declaring them at `MetavarContext`,
-  then creating the term `f ?x ?x` with the newly created metavariable,
-  and then performing the matching operation, and finally deleting `?x`.
-  We avoid this overhead by using temporary metavariables.
-
-  `TmpMetavarContext` implements `AbstractMetavarContext` for temporary metavariables.
-  All temporary metavariables used to solve a particular problem (e.g., matching)
-  share the same local context (field `mvarLCtx`), the type of a metavariable is stored in the
-  field `mvarTypes`. The assignments are implemented using small arrays.
-  We assume the number of temporary metavariables is usually small (< 1000),
-  and their names store a small integer that is used to read the arrays.
-
-  `TmpMetavarContext` also keeps a reference to the main `MetavarContext` used in the elaborator and
-  tactic framework. -/
-structure TmpMetavarContext :=
-(mctx        : MetavarContext       := {})
-(mvarLCtx    : LocalContext         := {})
-(mvarTypes   : Array Expr           := #[])
-(lAssignment : Array (Option Level) := #[])
-(eAssignment : Array (Option Expr)  := #[])
-
-def mkTmpMVarId (idx : Nat) :=
-Name.mkNumeral `_tmp idx
-
-def Name.isTmpMVarId : Name → Bool
-| Name.mkNumeral `_tmp _ => true
-| _                      => false
-
-def Name.getTmpMVarIdx : Name → Nat
-| Name.mkNumeral _ i => i
-| _                  => panic! "expected a temporary metavariable name"
-
-def Level.isTmpMVar : Level → Bool
-| Level.mvar mvarId => mvarId.isTmpMVarId
-| _                 => false
-
-def Expr.isTmpMVar : Expr → Bool
-| Expr.mvar mvarId => mvarId.isTmpMVarId
-| _                => false
-
-/--
-  Create a temporary metavariable context with the following characteristics:
-  - It contains `numLevelMVars` temporary `Level` metavariables
-  - It contains `mvarTypes.size` temporary `Expr` metavariables
-  - The temporary metavariable `i` has type `mvarTypes[i]`
-  - All temporary metavariables have local context `mvarLCtx`
-
-  `mctx` is the main metavariable context, and it is used to
-  retrieve regular metavariable information.  -/
-def mkTmpMetavarContext (mctx : MetavarContext) (mvarLCtx : LocalContext) (mvarTypes : Array Expr) (numLevelMVars : Nat) : TmpMetavarContext :=
-{ mctx        := mctx,
-  mvarLCtx    := mvarLCtx,
-  mvarTypes   := mvarTypes,
-  eAssignment := mkArray mvarTypes.size none,
-  lAssignment := mkArray numLevelMVars none }
-
-namespace TmpMetavarContext
-
-instance : Inhabited TmpMetavarContext := ⟨{}⟩
-
-def getLevelAssignment (m : TmpMetavarContext) (mvarId : Name) : Option Level :=
-if mvarId.isTmpMVarId then
-  m.lAssignment.get! mvarId.getTmpMVarIdx
-else
-  m.mctx.getLevelAssignment mvarId
-
-def assignLevel (m : TmpMetavarContext) (mvarId : Name) (val : Level) : TmpMetavarContext :=
-if mvarId.isTmpMVarId then
-  { lAssignment := m.lAssignment.set! mvarId.getTmpMVarIdx val, .. m }
-else
-  { mctx := m.mctx.assignLevel mvarId val, .. }
-
-def getExprAssignment (m : TmpMetavarContext) (mvarId : Name) : Option Expr :=
-if mvarId.isTmpMVarId then
-  m.eAssignment.get! mvarId.getTmpMVarIdx
-else
-  m.mctx.getExprAssignment mvarId
-
-def assignExpr (m : TmpMetavarContext) (mvarId : Name) (val : Expr) : TmpMetavarContext :=
-if mvarId.isTmpMVarId then
-  { eAssignment := m.eAssignment.set! mvarId.getTmpMVarIdx val, .. m }
-else
-  { mctx := m.mctx.assignExpr mvarId val, .. }
-
-def getDecl (m : TmpMetavarContext) (mvarId : Name) : MetavarDecl :=
-if mvarId.isTmpMVarId then
-  { userName := Name.anonymous, lctx := m.mvarLCtx, type := m.mvarTypes.get! mvarId.getTmpMVarIdx, synthetic := false }
-else
-  m.mctx.getDecl mvarId
-
-instance isAbstractMetavarContext : AbstractMetavarContext TmpMetavarContext :=
-{ empty                := {},
-  isReadOnlyLevelMVar  := fun _ mvarId => !mvarId.isTmpMVarId,
-  getLevelAssignment   := TmpMetavarContext.getLevelAssignment,
-  assignLevel          := TmpMetavarContext.assignLevel,
-  isReadOnlyExprMVar   := fun _ mvarId => !mvarId.isTmpMVarId,
-  getExprAssignment    := TmpMetavarContext.getExprAssignment,
-  assignExpr           := TmpMetavarContext.assignExpr,
-  getDecl              := TmpMetavarContext.getDecl,
-  -- TmpMetavarContext does not support delayed assignments or the creation of auxiliary metavariables.
-  auxMVarSupport       := false,
-  mkAuxMVar            := fun _ _ _ _ _ => panic! "TmpMetavarContex does not support the creation of auxiliary metavariables",
-  assignDelayed        := fun _ _ _ _ _ => panic! "TmpMetavarContex does not support delayed assignments",
-  eraseDelayed         := fun _ _ => panic! "TmpMetavarContex does not support delayed assignments",
-  getDelayedAssignment := fun _ _ => none }
-
-end TmpMetavarContext
-
-end Lean
diff --git a/library/Init/Lean/TypeUtil.lean b/library/Init/Lean/TypeUtil.lean
index 7901ef914e..a4221b659d 100644
--- a/library/Init/Lean/TypeUtil.lean
+++ b/library/Init/Lean/TypeUtil.lean
@@ -7,13 +7,14 @@ prelude
 import Init.Control.Reader
 import Init.Lean.NameGenerator
 import Init.Lean.Environment
-import Init.Lean.AbstractMetavarContext
 import Init.Lean.Trace
 import Init.Lean.InductiveUtil
 import Init.Lean.QuotUtil
 import Init.Lean.AuxRecursor
 import Init.Lean.ProjFns
 
+#exit
+
 /-
 This module provides three (mutually dependent) goodies:
 1- Weak head normal form computation with support for metavariables and transparency modes.