diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index a24efb7e3b..b033db6851 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -104,10 +104,10 @@ ExceptT.mk $ x >>= fun a => match a with
 @[inline] protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
 ExceptT.mk $ Except.ok <$> t
 
-instance exceptTOfExcept : HasMonadLift (Except ε) (ExceptT ε m) :=
+instance exceptTOfExcept : MonadLift (Except ε) (ExceptT ε m) :=
 ⟨fun α e => ExceptT.mk $ pure e⟩
 
-instance : HasMonadLift m (ExceptT ε m) :=
+instance : MonadLift m (ExceptT ε m) :=
 ⟨@ExceptT.lift _ _ _⟩
 
 @[inline] protected def catch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α :=
diff --git a/src/Init/Control/Lift.lean b/src/Init/Control/Lift.lean
index 58cbb63fa0..bb8cd0aaeb 100644
--- a/src/Init/Control/Lift.lean
+++ b/src/Init/Control/Lift.lean
@@ -18,32 +18,29 @@ universes u v w
     Like [MonadTrans](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html),
     but `n` does not have to be a monad transformer.
     Alternatively, an implementation of [MonadLayer](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer) without `layerInvmap` (so far). -/
-class HasMonadLift (m : Type u → Type v) (n : Type u → Type w) :=
+class MonadLift (m : Type u → Type v) (n : Type u → Type w) :=
 (monadLift : ∀ {α}, m α → n α)
 
-/-- The reflexive-transitive closure of `HasMonadLift`.
+/-- The reflexive-transitive closure of `MonadLift`.
     `monadLift` is used to transitively lift monadic computations such as `StateT.get` or `StateT.put s`.
     Corresponds to [MonadLift](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift). -/
-class HasMonadLiftT (m : Type u → Type v) (n : Type u → Type w) :=
+class MonadLiftT (m : Type u → Type v) (n : Type u → Type w) :=
 (monadLift : ∀ {α}, m α → n α)
 
-export HasMonadLiftT (monadLift)
+export MonadLiftT (monadLift)
 
 abbrev liftM := @monadLift
 
-@[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [HasMonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
+@[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
 a ← liftM $ x;
 pure $ coe a
 
-instance hasMonadLiftTTrans (m n o) [HasMonadLiftT m n] [HasMonadLift n o] : HasMonadLiftT m o :=
-⟨fun α ma => HasMonadLift.monadLift (monadLift ma : n α)⟩
+instance monadLiftTrans (m n o) [MonadLiftT m n] [MonadLift n o] : MonadLiftT m o :=
+⟨fun α ma => MonadLift.monadLift (monadLift ma : n α)⟩
 
-instance hasMonadLiftTRefl (m) : HasMonadLiftT m m :=
+instance monadLiftRefl (m) : MonadLiftT m m :=
 ⟨fun α => id⟩
 
-theorem monadLiftRefl {m : Type u → Type v} {α} : (monadLift : m α → m α) = id := rfl
-
-
 /-- A functor in the category of monads. Can be used to lift monad-transforming functions.
     Based on pipes' [MFunctor](https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html),
     but not restricted to monad transformers.
@@ -63,15 +60,13 @@ class MonadFunctorT (m m' : Type u → Type v) (n n' : Type u → Type w) :=
 
 export MonadFunctorT (monadMap)
 
-instance monadFunctorTTrans (m m' n n' o o') [MonadFunctorT m m' n n'] [MonadFunctor n n' o o'] :
+instance monadFunctorTrans (m m' n n' o o') [MonadFunctorT m m' n n'] [MonadFunctor n n' o o'] :
   MonadFunctorT m m' o o' :=
 ⟨fun α f => MonadFunctor.monadMap (fun β => (monadMap @f : n β → n' β))⟩
 
-instance monadFunctorTRefl (m m') : MonadFunctorT m m' m m' :=
+instance monadFunctorRefl (m m') : MonadFunctorT m m' m m' :=
 ⟨fun α f => f⟩
 
-theorem monadMapRefl {m m' : Type u → Type v} (f : ∀ {β}, m β → m' β) {α} : (monadMap @f : m α → m' α) = f := rfl
-
 /-- Run a Monad stack to completion.
     `run` should be the composition of the transformers' individual `run` functions.
     This class mostly saves some typing when using highly nested Monad stacks:
diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 3f9cd15715..8b0b741080 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -50,7 +50,7 @@ namespace OptionT
   @[inline] protected def lift (ma : m α) : OptionT m α :=
   (some <$> ma : m (Option α))
 
-  instance : HasMonadLift m (OptionT m) :=
+  instance : MonadLift m (OptionT m) :=
   ⟨@OptionT.lift _ _⟩
 
   @[inline] protected def monadMap {m'} [Monad m'] {α} (f : ∀ {α}, m α → m' α) : OptionT m α → OptionT m' α :=
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index ec948f88d0..9a67fbf085 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -33,7 +33,7 @@ variables {ρ : Type u} {m : Type u → Type v} {α : Type u}
 @[inline] protected def lift  (a : m α) : ReaderT ρ m α :=
 fun r => a
 
-instance  : HasMonadLift m (ReaderT ρ m) :=
+instance  : MonadLift m (ReaderT ρ m) :=
 ⟨@ReaderT.lift ρ m⟩
 
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) :=
@@ -106,7 +106,7 @@ instance MonadReaderOf.isMonadReader (ρ : Type u) (m : Type u → Type v) [Mona
 ⟨readThe ρ⟩
 
 instance monadReaderTrans {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w}
-  [MonadReaderOf ρ m] [HasMonadLift m n] : MonadReaderOf ρ n :=
+  [MonadReaderOf ρ m] [MonadLift m n] : MonadReaderOf ρ n :=
 ⟨monadLift (MonadReader.read : m ρ)⟩
 
 instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) :=
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index e4896c70b1..4a31cb9c84 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -67,7 +67,7 @@ fun s => pure (f s)
 @[inline] protected def lift {α : Type u} (t : m α) : StateT σ m α :=
 fun s => do a ← t; pure (a, s)
 
-instance : HasMonadLift m (StateT σ m) :=
+instance : MonadLift m (StateT σ m) :=
 ⟨@StateT.lift σ m _⟩
 
 instance (σ m m') [Monad m] [Monad m'] : MonadFunctor m m' (StateT σ m) (StateT σ m') :=
@@ -136,7 +136,7 @@ modifyGet fun s => (s, f s)
 
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
 -- will be picked first
-instance monadStateTrans {n : Type u → Type w} [MonadStateOf σ m] [HasMonadLift m n] : MonadStateOf σ n :=
+instance monadStateTrans {n : Type u → Type w} [MonadStateOf σ m] [MonadLift m n] : MonadStateOf σ n :=
 { get       := monadLift (MonadStateOf.get : m _),
   set       := fun st => monadLift (MonadStateOf.set st : m _),
   modifyGet := fun α f => monadLift (MonadState.modifyGet f : m _) }
diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean
index 926e06aec2..b9f389232c 100644
--- a/src/Init/Control/StateRef.lean
+++ b/src/Init/Control/StateRef.lean
@@ -13,13 +13,13 @@ def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type :=
 -- TODO: remove `[STWorld ω m]`. We should use a tactic for synthesizing ω, and the tactic infers the instance `[STWorld ω m]`
 abbrev StateRefT {ω : Type} (σ : Type) (m : Type → Type) [STWorld ω m] (α : Type) := StateRefT' ω σ m α
 
-@[inline] def StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [HasMonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m (α × σ) := do
+@[inline] def StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m (α × σ) := do
 ref ← ST.mkRef s;
 a ← x ref;
 s ← ref.get;
 pure (a, s)
 
-@[inline] def StateRefT'.run' {ω σ : Type} {m : Type → Type} [Monad m] [HasMonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m α := do
+@[inline] def StateRefT'.run' {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m α := do
 (a, _) ← x.run s;
 pure a
 
@@ -30,21 +30,21 @@ variables {ω σ : Type} {m : Type → Type} {α : Type}
 fun _ => x
 
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
-instance : HasMonadLift m (StateRefT' ω σ m) := ⟨fun _ => StateRefT'.lift⟩
+instance : MonadLift m (StateRefT' ω σ m) := ⟨fun _ => StateRefT'.lift⟩
 instance [Monad m] [MonadIO m] : MonadIO (StateRefT' ω σ m) := inferInstanceAs (MonadIO (ReaderT _ _))
 instance (σ m m') [Monad m] [Monad m'] : MonadFunctor m m' (StateRefT' ω σ m) (StateRefT' ω σ m') :=
 inferInstanceAs (MonadFunctor m m' (ReaderT _ _) (ReaderT _ _))
 
-@[inline] protected def get [Monad m] [HasMonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
+@[inline] protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
 fun ref => ref.get
 
-@[inline] protected def set [Monad m] [HasMonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
+@[inline] protected def set [Monad m] [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
 fun ref => ref.set s
 
-@[inline] protected def modifyGet [Monad m] [HasMonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
+@[inline] protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
 fun ref => ref.modifyGet f
 
-instance [HasMonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) :=
+instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) :=
 { get       := StateRefT'.get,
   set       := StateRefT'.set,
   modifyGet := fun α f => StateRefT'.modifyGet f }
diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 948ff3026d..e412cb7fd2 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -147,7 +147,7 @@ let r := ngen.curr;
 setNGen ngen.next;
 pure r
 
-instance monadNameGeneratorLift (m n : Type → Type) [MonadNameGenerator m] [HasMonadLift m n] : MonadNameGenerator n :=
+instance monadNameGeneratorLift (m n : Type → Type) [MonadNameGenerator m] [MonadLift m n] : MonadNameGenerator n :=
 { getNGen := liftM (getNGen : m _),
   setNGen := fun ngen => liftM (setNGen ngen : m _) }
 
@@ -441,7 +441,7 @@ instance MacroM.monadQuotation : MonadQuotation MacroM :=
   getMainModule       := fun ctx => pure ctx.mainModule,
   withFreshMacroScope := @Macro.withFreshMacroScope }
 
-instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=
+instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [MonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=
 { getCurrMacroScope   := liftM (getCurrMacroScope : m MacroScope),
   getMainModule       := liftM (getMainModule : m Name),
   withFreshMacroScope := fun α => monadMap (fun α => (withFreshMacroScope : m α → m α)) }
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index a0a4a63273..234a86abf9 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -323,12 +323,12 @@ Prim.setAccessRights filename mode.flags
 /- References -/
 abbrev Ref (α : Type) := ST.Ref IO.RealWorld α
 
-instance st2eio {ε} : HasMonadLift (ST IO.RealWorld) (EIO ε) :=
+instance st2eio {ε} : MonadLift (ST IO.RealWorld) (EIO ε) :=
 ⟨fun α x s => match x s with
  | EStateM.Result.ok a s     => EStateM.Result.ok a s
  | EStateM.Result.error ex _ => Empty.rec _ ex⟩
 
-def mkRef {α : Type} {m : Type → Type} [Monad m] [HasMonadLiftT (ST IO.RealWorld) m] (a : α) : m (IO.Ref α) :=
+def mkRef {α : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (a : α) : m (IO.Ref α) :=
 ST.mkRef a
 
 end IO
diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean
index 106ac18aa0..0930afb427 100644
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@@ -18,7 +18,7 @@ instance (σ : Type) : Monad (ST σ) := inferInstanceAs (Monad (EST _ _))
 -- Auxiliary class for inferring the "state" of `EST` and `ST` monads
 class STWorld (σ : outParam Type) (m : Type → Type)
 
-instance STWorld.trans {σ m n} [STWorld σ m] [HasMonadLift m n] : STWorld σ n := ⟨⟩
+instance STWorld.trans {σ m n} [STWorld σ m] [MonadLift m n] : STWorld σ n := ⟨⟩
 instance STWorld.base {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
 
 def runEST {ε α : Type} (x : forall (σ : Type), EST ε σ α) : Except ε α :=
@@ -31,7 +31,7 @@ match x Unit () with
 | EStateM.Result.ok a _     => a
 | EStateM.Result.error ex _ => Empty.rec _ ex
 
-instance st2est {ε σ} : HasMonadLift (ST σ) (EST ε σ) :=
+instance st2est {ε σ} : MonadLift (ST σ) (EST ε σ) :=
 ⟨fun α x s => match x s with
   | EStateM.Result.ok a s     => EStateM.Result.ok a s
   | EStateM.Result.error ex _ => Empty.rec _ ex⟩
@@ -91,7 +91,7 @@ pure b
 end Prim
 
 section
-variables {σ : Type} {m : Type → Type} [Monad m] [HasMonadLiftT (ST σ) m]
+variables {σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST σ) m]
 
 @[inline] def mkRef {α : Type} (a : α) : m (Ref σ α) :=  liftM $ Prim.mkRef a
 @[inline] def Ref.get {α : Type} (r : Ref σ α) : m α := liftM $ Prim.Ref.get r
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index 1e1fe34d50..f4b85e09de 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -95,7 +95,7 @@ class MonadOptions (m : Type → Type) :=
 
 export MonadOptions (getOptions)
 
-instance monadOptsFromLift (m n) [MonadOptions m] [HasMonadLift m n] : MonadOptions n :=
+instance monadOptsFromLift (m n) [MonadOptions m] [MonadLift m n] : MonadOptions n :=
 { getOptions := liftM (getOptions : m _) }
 
 section Methods
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 7679e58b12..5f426b9b3e 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -15,7 +15,7 @@ class MonadEnv (m : Type → Type) :=
 
 export MonadEnv (getEnv modifyEnv)
 
-instance monadEnvFromLift (m n) [MonadEnv m] [HasMonadLift m n] : MonadEnv n :=
+instance monadEnvFromLift (m n) [MonadEnv m] [MonadLift m n] : MonadEnv n :=
 { getEnv    := liftM (getEnv : m Environment),
   modifyEnv := fun f => liftM (modifyEnv f : m Unit) }
 
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index cc7ea58b8a..19c6f8cab1 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -109,7 +109,7 @@ instance monadTracerAdapterExcept {ε : Type} {m : Type → Type} [Monad m] [Mon
   trace    := @MonadTracerAdapter.trace _ _ _,
   traceM   := @MonadTracerAdapter.traceM _ _ _ }
 
-instance liftMonadTracerAdapter {m n : Type → Type} [MonadTracerAdapter n] [HasMonadLift n m] : MonadTracerAdapter m :=
+instance liftMonadTracerAdapter {m n : Type → Type} [MonadTracerAdapter n] [MonadLift n m] : MonadTracerAdapter m :=
 { isTracingEnabledFor := fun cls => liftM (MonadTracerAdapter.isTracingEnabledFor cls : n _),
   addTraceContext     := fun msg => liftM (MonadTracerAdapter.addTraceContext msg : n _),
   enableTracing       := fun b => liftM (MonadTracerAdapter.enableTracing b : n _),
@@ -223,7 +223,7 @@ def resetTraceState {m} [SimpleMonadTracerAdapter m] : m Unit :=
 modifyTraceState (fun _ => {})
 
 /- We currently cannot mark the following definition as an instance since it increases the search space too much -/
-def simpleMonadTracerAdapterLift (m : Type → Type) {n : Type → Type} [SimpleMonadTracerAdapter m] [HasMonadLiftT m n] : SimpleMonadTracerAdapter n :=
+def simpleMonadTracerAdapterLift (m : Type → Type) {n : Type → Type} [SimpleMonadTracerAdapter m] [MonadLiftT m n] : SimpleMonadTracerAdapter n :=
 { getOptions       := liftM (SimpleMonadTracerAdapter.getOptions : m _),
   modifyTraceState := fun f => liftM (SimpleMonadTracerAdapter.modifyTraceState f : m _),
   getTraceState    := liftM (SimpleMonadTracerAdapter.getTraceState : m _),