diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index c234139f91..cd8ab43a2e 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -672,5 +672,15 @@ do fvarId ← mkFreshId;
    adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
      withNewFVar fvar type k
 
+/--
+  Save cache and `MetavarContext`, bump the `MetavarContext` depth, execute `x`,
+  and restore saved data. -/
+@[inline] def withNewMCtxDepth {α} (x : MetaM α) : MetaM α :=
+do s ← get;
+   let savedCache := s.cache;
+   let savedMCtx  := s.mctx;
+   modify $ fun s => { mctx := s.mctx.incDepth, .. s };
+   finally x (modify $ fun s => { cache := savedCache, mctx := savedMCtx, .. s })
+
 end Meta
 end Lean
diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean
index 909abd4145..5a4764f361 100644
--- a/src/Init/Lean/MetavarContext.lean
+++ b/src/Init/Lean/MetavarContext.lean
@@ -310,6 +310,9 @@ def isExprAssignable (mctx : MetavarContext) (mvarId : Name) : Bool :=
 let decl := mctx.getDecl mvarId;
 decl.depth == mctx.depth
 
+def incDepth (mctx : MetavarContext) : MetavarContext :=
+{ depth := mctx.depth + 1, .. mctx }
+
 /-- Return true iff the given level contains an assigned metavariable. -/
 def hasAssignedLevelMVar (mctx : MetavarContext) : Level → Bool
 | Level.succ lvl _       => lvl.hasMVar && hasAssignedLevelMVar lvl