diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index e3dbed7c3b..948ff3026d 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -147,15 +147,10 @@ let r := ngen.curr;
 setNGen ngen.next;
 pure r
 
--- TODO: mark as instance as soon as we move to new frontend
-def monadNameGeneratorLift (m : Type → Type) {n : Type → Type} [MonadNameGenerator m] [HasMonadLiftT m n] : MonadNameGenerator n :=
+instance monadNameGeneratorLift (m n : Type → Type) [MonadNameGenerator m] [HasMonadLift m n] : MonadNameGenerator n :=
 { getNGen := liftM (getNGen : m _),
   setNGen := fun ngen => liftM (setNGen ngen : m _) }
 
-instance ReaderT.monadNGen {m ρ} [Monad m] [MonadNameGenerator m] : MonadNameGenerator (ReaderT ρ m) := monadNameGeneratorLift m
-instance StateRefT.monadNGen {ω m σ} [MonadNameGenerator m] : MonadNameGenerator (StateRefT' ω σ m)  := monadNameGeneratorLift m
-instance OptionT.monadNGen {m} [Monad m] [MonadNameGenerator m] : MonadNameGenerator (OptionT m)     := monadNameGeneratorLift m
-
 /-
   Small DSL for describing parsers. We implement an interpreter for it
   at `Parser.lean` -/
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index 6feb9f4ab7..1e1fe34d50 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -95,13 +95,9 @@ class MonadOptions (m : Type → Type) :=
 
 export MonadOptions (getOptions)
 
-/- We currently cannot mark the following definition as an instance since it increases the search space too much -/
-def monadOptsFromLift (m) {n} [MonadOptions m] [HasMonadLiftT m n] : MonadOptions n :=
+instance monadOptsFromLift (m n) [MonadOptions m] [HasMonadLift m n] : MonadOptions n :=
 { getOptions := liftM (getOptions : m _) }
 
-instance ReaderT.monadOpts {ρ m} [MonadOptions m] : MonadOptions (ReaderT ρ m) := monadOptsFromLift m
-instance StateRefT.monadOpts {ω σ m} [MonadOptions m] : MonadOptions (StateRefT' ω σ m) := monadOptsFromLift m
-
 section Methods
 
 variables {m : Type → Type} [Monad m] [MonadOptions m]
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 0d408d3ad0..7679e58b12 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -15,15 +15,10 @@ class MonadEnv (m : Type → Type) :=
 
 export MonadEnv (getEnv modifyEnv)
 
-/- We currently cannot mark the following definition as an instance since it increases the search space too much -/
-def monadEnvFromLift (m) {n} [MonadEnv m] [HasMonadLiftT m n] : MonadEnv n :=
+instance monadEnvFromLift (m n) [MonadEnv m] [HasMonadLift m n] : MonadEnv n :=
 { getEnv    := liftM (getEnv : m Environment),
   modifyEnv := fun f => liftM (modifyEnv f : m Unit) }
 
-instance ReaderT.monadEnv {m ρ} [Monad m] [MonadEnv m] : MonadEnv (ReaderT ρ m) := monadEnvFromLift m
-instance StateRefT.monadEnv {ω m σ} [MonadEnv m] : MonadEnv (StateRefT' ω σ m)   := monadEnvFromLift m
-instance OptionT.monadEnv {m} [Monad m] [MonadEnv m] : MonadEnv (OptionT m) := monadEnvFromLift m
-
 section Methods
 
 variables {m : Type → Type} [MonadEnv m]