diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index a9d2d5934e..ce8766d7c9 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Message
 import Lean.InternalExceptionId
 import Lean.Data.Options
+import Lean.Util.MonadCache
 
 namespace Lean
 
@@ -76,6 +77,9 @@ instance {ρ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m) := {
 instance {ω σ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m) :=
   inferInstanceAs (MonadRecDepth (ReaderT _ _))
 
+instance {ω α β m} [BEq α] [Hashable α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m) :=
+  inferInstanceAs (MonadRecDepth (StateRefT' _ _ _))
+
 @[inline] def withIncRecDepth {α m} [Monad m] [MonadRecDepth m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
     (x : m α) : m α := do
   let curr ← MonadRecDepth.getRecDepth
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 143d3ed6d7..01135df4ea 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -206,6 +206,10 @@ protected def isExprDefEqAux (t s : Expr) : MetaM Bool :=
 protected def synthPending (mvarId : MVarId) : MetaM Bool :=
   withIncRecDepth do (← liftIO synthPendingRef.get) mvarId
 
+-- withIncRecDepth for a monad `n` such that `[MonadControlT MetaM n]`
+protected def withIncRecDepth {α} (x : n α) : n α :=
+  mapMetaM (withIncRecDepth (m := MetaM)) x
+
 private def mkFreshExprMVarAtCore
     (mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (kind : MetavarKind) (userName : Name) (numScopeArgs : Nat) : MetaM Expr := do
   modifyMCtx fun mctx => mctx.addExprMVarDecl mvarId userName lctx localInsts type kind numScopeArgs;
diff --git a/src/Lean/Meta/Tactic/Assert.lean b/src/Lean/Meta/Tactic/Assert.lean
index d57ec1133b..a8be65a5bd 100644
--- a/src/Lean/Meta/Tactic/Assert.lean
+++ b/src/Lean/Meta/Tactic/Assert.lean
@@ -37,7 +37,7 @@ def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MV
     pure newMVar.mvarId!
 
 /--
-  Convert the given goal `Ctx |- target` into `Ctx |- forall (name : type) -> name = val -> target`.
+  Convert the given goal `Ctx |- target` into `Ctx |- (hName : type) -> hName = val -> target`.
   It assumes `val` has type `type` -/
 def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do
   withMVarContext mvarId $ do
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index adde4a47f9..07e717cf4c 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Std.Data.HashMap
+
 namespace Lean
 /-- Interface for caching results.  -/
 class MonadCache (α β : Type) (m : Type → Type) :=
@@ -74,6 +75,7 @@ instance [MonadIO m] : MonadIO (MonadCacheT α β m) := inferInstanceAs (MonadIO
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (MonadCacheT α β m) := inferInstanceAs (MonadExceptOf ε (StateRefT' _ _ _))
 instance : MonadControl m (MonadCacheT α β m) := inferInstanceAs (MonadControl m (StateRefT' _ _ _))
 instance [MonadFinally m] : MonadFinally (MonadCacheT α β m) := inferInstanceAs (MonadFinally (StateRefT' _ _ _))
+instance [MonadRef m] : MonadRef (MonadCacheT α β m) := inferInstanceAs (MonadRef (StateRefT' _ _ _))
 
 end MonadCacheT
 end Lean