diff --git a/leanpkg/leanpkg/main.lean b/leanpkg/leanpkg/main.lean
index c6539ef282..84d6fa1dc2 100644
--- a/leanpkg/leanpkg/main.lean
+++ b/leanpkg/leanpkg/main.lean
@@ -124,7 +124,7 @@ def fixup_git_version (dir : string) : ∀ (src : source), io source
 | src := return src
 
 def add (dep : dependency) : io unit := do
-(_, assg) ← materialize "." dep assignment.empty,
+(_, assg) ← (materialize "." dep).run assignment.empty,
 some downloaded_path ← return (assg.find dep.name),
 manif ← manifest.from_file (downloaded_path ++ "/" ++ leanpkg_toml_fn),
 src ← fixup_git_version downloaded_path dep.src,
diff --git a/leanpkg/leanpkg/resolve.lean b/leanpkg/leanpkg/resolve.lean
index 495371a7e7..9e88343532 100644
--- a/leanpkg/leanpkg/resolve.lean
+++ b/leanpkg/leanpkg/resolve.lean
@@ -92,7 +92,7 @@ deps.mmap' $ λ dep, do
   solve_deps_core p d' max_depth
 
 def solve_deps (d : manifest) : io assignment := do
-(_, assg) ← solve_deps_core "." d 1024 $ assignment.empty.insert d.name ".",
+(_, assg) ← (solve_deps_core "." d 1024).run $ assignment.empty.insert d.name ".",
 return assg
 
 def construct_path_core (depname : string) (dirname : string) : io (list string) :=
diff --git a/library/init/category/except.lean b/library/init/category/except.lean
index d6f0a8713f..101b58a668 100644
--- a/library/init/category/except.lean
+++ b/library/init/category/except.lean
@@ -34,9 +34,6 @@ section
   | (except.error err) := except.error err
   | (except.ok v) := f v
   end
-
-  instance monad : monad (except ε) :=
-  { map := @map, pure := @return, bind := @bind }
 end
 end except
 
@@ -52,14 +49,12 @@ section
   protected def return {α : Type u} (a : α) : except_t ε m α :=
   ⟨pure $ except.ok a⟩
 
-  protected def map {α β : Type u} (f : α → β) (ma : except_t ε m α) : except_t ε m β :=
-  ⟨has_map.map f <$> ma.run⟩
+  protected def bind_cont {α β : Type u} (f : α → except_t ε m β) : except ε α → m (except ε β)
+  | (except.ok a)    := (f a).run
+  | (except.error e) := pure (except.error e)
 
   protected def bind {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) : except_t ε m β :=
-  ⟨ma.run >>= λ res, match res with
-   | except.ok a    := (f a).run
-   | except.error e := pure (except.error e)
-   end⟩
+  ⟨ma.run >>= bind_cont f⟩
 
   protected def lift {α : Type u} (t : m α) : except_t ε m α :=
   ⟨except.ok <$> t⟩
@@ -71,7 +66,7 @@ section
    end⟩
 
   instance : monad (except_t ε m) :=
-  { pure := @return, map := @map, bind := @bind }
+  { pure := @return, bind := @bind }
 end
 
 instance (ε : Type u) : monad_transformer (except_t ε) :=
diff --git a/library/init/category/lawful.lean b/library/init/category/lawful.lean
index 66c80a0e20..c0d0ebc488 100644
--- a/library/init/category/lawful.lean
+++ b/library/init/category/lawful.lean
@@ -76,59 +76,91 @@ lemma map_ext_congr {α β} {m : Type u → Type v} [has_map m] {x : m α} {f :
 
 -- instances of previously defined monads
 
+namespace state_t
+section
+  variable  {σ : Type u}
+  variable  {m : Type u → Type v}
+  variable  [monad m]
+  variables {α β : Type u}
+  variables (x : state_t σ m α) (st : σ)
+
+  lemma ext {x x' : state_t σ m α} (h : ∀ st, x.run st = x'.run st) : x = x' :=
+  by cases_type* state_t; simp [show x = x', from funext h]
+
+  @[simp] lemma run_pure (a) : (pure a : state_t σ m α).run st = pure (a, st) := rfl
+  @[simp] lemma run_bind (f : α → state_t σ m β) : (x >>= f).run st = x.run st >>= λ p, (f p.1).run p.2 :=
+  by simp [bind, state_t.bind, state_t.run]; rw bind_ext_congr; intro a; cases a; simp [state_t.bind, state_t.run]
+  @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run st = (λ p : α × σ, (f (prod.fst p), prod.snd p)) <$> x.run st :=
+  begin
+    rw ←bind_pure_comp_eq_map m,
+    change (x >>= pure ∘ f).run st = _,
+    simp
+  end
+end
+end state_t
+
 instance (m : Type u → Type v) [monad m] [is_lawful_monad m] (σ : Type u) : is_lawful_monad (state_t σ m) :=
-{ id_map := begin
-    intros, funext,
-    simp [(<$>), state_t.bind, state_t.return, function.comp, return],
-    rw [bind_ext_congr pure], swap,
-    { intros, cases a, refl },
-    { simp [bind_pure] }
-  end,
-  pure_bind := begin
-    intros, funext,
-    simp [bind, pure, has_pure.pure, state_t.bind, state_t.return, pure_bind],
-  end,
-  bind_assoc := begin
-    intros, funext,
-    simp [bind, state_t.bind, state_t.return, bind_assoc],
-    apply congr_arg, funext r,
-    cases r, refl
-  end }
+{ id_map := by intros; apply state_t.ext; intro; simp; erw id_map,
+  pure_bind := by intros; apply state_t.ext; intro; simp,
+  bind_assoc := by intros; apply state_t.ext; intro; simp [bind_assoc] }
 
 
-instance (ε : Type u) : is_lawful_monad (except ε) :=
-{ id_map := begin intros, cases x; refl, end,
-  pure_bind := begin intros; refl end,
-  bind_pure_comp_eq_map := begin intros, cases x; refl end,
-  bind_assoc := begin intros, cases x; reflexivity end }
+namespace except_t
+  variables {α β ε : Type u} {m : Type u → Type v} [monad m] (x : except_t ε m α)
 
-local attribute [simp] except_t.map except_t.bind except_t.return except_t.monad
+  lemma ext {x x' : except_t ε m α} (h : x.run = x'.run) : x = x' :=
+  by cases_type* except_t; simp * at *
+
+  @[simp] lemma run_pure (a) : (pure a : except_t ε m α).run = pure (@except.ok ε α a) := rfl
+  @[simp] lemma run_bind (f : α → except_t ε m β) : (x >>= f).run = x.run >>= except_t.bind_cont f := rfl
+  @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run = except.map f <$> x.run :=
+  begin
+    rw ←bind_pure_comp_eq_map m,
+    change (x >>= pure ∘ f).run = _,
+    simp,
+    rw [bind_ext_congr],
+    intro a; cases a; simp [except_t.bind_cont, except.map]
+  end
+end except_t
 
 instance (m : Type u → Type v) [monad m] [is_lawful_monad m] (ε : Type u) : is_lawful_monad (except_t ε m) :=
 { id_map := begin
-    intros, cases x, dsimp,
-    rw map_ext_congr id; simp
+    intros, apply except_t.ext, simp,
+    rw [map_ext_congr, id_map],
+    intro a, cases a; refl
   end,
   bind_pure_comp_eq_map := begin
-    intros, cases x, dsimp,
+    intros, apply except_t.ext, simp,
     rw [bind_ext_congr, bind_pure_comp_eq_map],
-    intro a, cases a; dsimp [except.monad, except.map]; refl
+    intro a, cases a; refl
   end,
   bind_assoc := begin
-    intros, cases x, dsimp, simp [bind_assoc],
+    intros, apply except_t.ext, simp [bind_assoc],
     rw [bind_ext_congr],
-    { intro a, cases a; simp }
+    { intro a, cases a; simp [except_t.bind_cont] }
   end,
-  pure_bind := begin
-    intros, dsimp, simp,
-    cases f x, refl
-  end,
-  ..except_t.monad }
+  pure_bind := by intros; apply except_t.ext; simp [except_t.bind_cont] }
 
 
-local attribute [simp] reader_t.bind reader_t.pure
+namespace reader_t
+section
+  variable  {r : Type u}
+  variable  {m : Type u → Type v}
+  variable  [monad m]
+  variables {α β : Type u}
+  variables (x : reader_t r m α) (cfg : r)
+
+  lemma ext {x x' : reader_t r m α} (h : ∀ cfg, x.run cfg = x'.run cfg) : x = x' :=
+  by cases_type* reader_t; simp [show x = x', from funext h]
+
+  @[simp] lemma run_pure (a) : (pure a : reader_t r m α).run cfg = pure a := rfl
+  @[simp] lemma run_bind (f : α → reader_t r m β) : (x >>= f).run cfg = x.run cfg >>= λ a, (f a).run cfg := rfl
+  @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run cfg = f <$> x.run cfg :=
+  by rw ←bind_pure_comp_eq_map m; refl
+end
+end reader_t
 
 instance (r : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (reader_t r m) :=
-{ id_map := by intros; dsimp [reader_t.monad]; simp,
-  pure_bind := by intros; dsimp [reader_t.monad]; simp,
-  bind_assoc := by intros; dsimp [reader_t.monad]; simp [bind_assoc] }
+{ id_map := by intros; apply reader_t.ext; intro; simp,
+  pure_bind := by intros; apply reader_t.ext; intro; simp,
+  bind_assoc := by intros; apply reader_t.ext; intro; simp [bind_assoc] }
diff --git a/library/init/category/reader.lean b/library/init/category/reader.lean
index 6cb7a1442a..19b8be0835 100644
--- a/library/init/category/reader.lean
+++ b/library/init/category/reader.lean
@@ -8,16 +8,8 @@ prelude
 import init.category.transformers init.category.id
 universes u v w
 
-class monad_reader (r : out_param (Type u)) (m : Type u → Type v) [monad m] :=
-(reader {} {α : Type u} : (r → α) → m α)
-(read {} : m r := reader id)
-(reader := λ α f, f <$> read)
-
-
-export monad_reader (read)
-
-def reader_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-r → m α
+structure reader_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+(run : r → m α)
 
 @[reducible] def reader (r : Type u) := reader_t r id
 
@@ -29,31 +21,41 @@ section
   variables {α β : Type u}
 
   protected def read : reader_t r m r :=
-  λ r, pure r
-
-  protected def run : r → reader_t r m α → m α :=
-  λ r x, x r
+  ⟨pure⟩
 
   protected def pure (a : α) : reader_t r m α :=
-  λ r, pure a
+  ⟨λ r, pure a⟩
 
   protected def bind (x : reader_t r m α) (f : α → reader_t r m β) : reader_t r m β :=
-  λ r, do a ← x r,
-          f a r
+  ⟨λ r, do a ← x.run r,
+           (f a).run r⟩
 
   instance : monad (reader_t r m) :=
   { pure := @reader_t.pure _ _ _, bind := @reader_t.bind _ _ _ }
 
   protected def lift (a : m α) : reader_t r m α :=
-  λ r, a
+  ⟨λ r, a⟩
 
   instance (m) [monad m] : has_monad_lift m (reader_t r m) :=
   ⟨@reader_t.lift r m _⟩
+
+  protected def map {r m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : reader_t r m α → reader_t r m' α :=
+  λ x, ⟨λ r, f (x.run r)⟩
+
+  instance (r m m') [monad m] [monad m'] : monad_functor m m' (reader_t r m) (reader_t r m') :=
+  ⟨@reader_t.map r m m' _ _⟩
 end
 end reader_t
 
-def with_reader_t {r r' m} [monad m] {α} (f : r' → r) : reader_t r m α → reader_t r' m α :=
-λ x r, x (f r)
+class monad_reader_lift (r : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
+[has_lift : has_monad_lift_t (reader_t r m) n]
+
+attribute [instance] monad_reader_lift.mk
+local attribute [instance] monad_reader_lift.has_lift
+
+def monad_reader_lift.read {r : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m] [monad_reader_lift r m n] : n r :=
+@monad_lift _ _ _ _ (reader_t.read : reader_t r m _)
+export monad_reader_lift (read)
 
 class monad_reader_functor (r r' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
 [functor {} : monad_functor_t (reader_t r m) (reader_t r' m) n n']
@@ -61,17 +63,8 @@ class monad_reader_functor (r r' : out_param (Type u)) (m : out_param (Type u 
 attribute [instance] monad_reader_functor.mk
 local attribute [instance] monad_reader_functor.functor
 
+def with_reader_t {r r' m} [monad m] {α} (f : r' → r) : reader_t r m α → reader_t r' m α :=
+λ x, ⟨λ r, x.run (f r)⟩
+
 def with_reader {r r'} {m n n'} [monad m] [monad_reader_functor r r' m n n'] {α : Type u} (f : r' → r) : n α → n' α :=
 monad_map $ λ α, (with_reader_t f : reader_t r m α → reader_t r' m α)
-
-def map_reader_t {r m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : reader_t r m α → reader_t r m' α :=
-λ x r, f (x r)
-
-instance (r m m') [monad m] [monad m'] : monad_functor m m' (reader_t r m) (reader_t r m') :=
-⟨@map_reader_t r m m' _ _⟩
-
-instance (r m) [monad m] : monad_reader r (reader_t r m) :=
-{ reader := λ α f, pure ∘ f }
-
-instance monad_reader_lift (r m m') [has_monad_lift m m'] [monad m] [monad_reader r m] [monad m'] : monad_reader r m' :=
-{ reader := λ α, monad_lift ∘ (monad_reader.reader : _ → m α) }
diff --git a/library/init/category/state.lean b/library/init/category/state.lean
index 9b7240dcfc..edd225c05e 100644
--- a/library/init/category/state.lean
+++ b/library/init/category/state.lean
@@ -9,8 +9,8 @@ import init.category.id
 import init.category.transformers
 universes u v w
 
-def state_t (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-σ → m (α × σ)
+structure state_t (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+(run' : σ → m (α × σ))
 
 @[reducible] def state (σ α : Type u) : Type u := state_t σ id α
 
@@ -22,25 +22,23 @@ section
   variables {α β : Type u}
 
   protected def run (st : σ) (x : state_t σ m α) : m (α × σ) :=
-  x st
+  state_t.run' x st
 
-  protected def return (a : α) : state_t σ m α :=
-  λ s, show m (α × σ), from
-    return (a, s)
+  protected def pure (a : α) : state_t σ m α :=
+  ⟨λ s, pure (a, s)⟩
 
   protected def bind (act₁ : state_t σ m α) (act₂ : α → state_t σ m β) : state_t σ m β :=
-  λ s, show m (β × σ), from
-     do (a, new_s) ← act₁ s,
-        act₂ a new_s
+  ⟨λ s, do (a, new_s) ← act₁.run s,
+           (act₂ a).run new_s⟩
 
   instance : monad (state_t σ m) :=
-  { pure := @state_t.return σ m _, bind := @state_t.bind σ m _ }
+  { pure := @state_t.pure σ m _, bind := @state_t.bind σ m _ }
 
   protected def orelse [alternative m] (α : Type u) (act₁ act₂ : state_t σ m α) : state_t σ m α :=
-  λ s, act₁ s <|> act₂ s
+  ⟨λ s, act₁.run s <|> act₂.run s⟩
 
   protected def failure [alternative m] (α : Type u) : state_t σ m α :=
-  λ s, failure
+  ⟨λ s, failure⟩
 
   instance [alternative m] : alternative (state_t σ m) :=
   { failure := @state_t.failure σ m _ _,
@@ -48,46 +46,52 @@ section
     ..state_t.monad }
 
   protected def get : state_t σ m σ :=
-  λ s, return (s, s)
+  ⟨λ s, return (s, s)⟩
 
   protected def put : σ → state_t σ m punit :=
-  λ s' s, return (punit.star, s')
+  λ s', ⟨λ s, return (punit.star, s')⟩
 
   protected def modify (f : σ → σ) : state_t σ m punit :=
-  λ s, return (punit.star, f s)
-
-  protected def embed {α : Type u} (x : state σ α) : state_t σ m α :=
-  pure ∘ x
+  ⟨λ s, return (punit.star, f s)⟩
 
   protected def lift {α : Type u} (t : m α) : state_t σ m α :=
-  λ s, do a ← t, return (a, s)
+  ⟨λ s, do a ← t, return (a, s)⟩
 
-  instance (m) [monad m] : has_monad_lift m (state_t σ m) :=
+  instance has_monad_lift_lift (m) [monad m] : has_monad_lift m (state_t σ m) :=
   ⟨@state_t.lift σ m _⟩
 
+  protected def map {σ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : state_t σ m α → state_t σ m' α :=
+  λ x, ⟨λ st, f (x.run st)⟩
+
+  instance (σ m m') [monad m] [monad m'] : monad_functor m m' (state_t σ m) (state_t σ m') :=
+  ⟨@state_t.map σ m m' _ _⟩
+
   -- TODO(Sebastian): uses lenses as in https://hackage.haskell.org/package/lens-4.15.4/docs/Control-Lens-Zoom.html#t:Zoom ?
   protected def zoom {σ σ' α : Type u} {m : Type u → Type v} [monad m] (f : σ → σ') (f' : σ' → σ) (x : state_t σ' m α) : state_t σ m α :=
-  λ st, (λ p : α × σ', (p.fst, f' p.snd)) <$> x.run (f st)
+  ⟨λ st, (λ p : α × σ', (p.fst, f' p.snd)) <$> x.run (f st)⟩
 end
 end state_t
 
 @[reducible] protected def state.run {σ α : Type u} (st : σ) (x : state σ α) : α × σ :=
 state_t.run st x
 
-@[reducible] def monad_state (σ : out_param (Type u)) (m : Type u → Type u) [monad m] :=
-has_monad_lift_t (state σ) m
+class monad_state_lift (σ : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
+[has_lift : has_monad_lift_t (state_t σ m) n]
+
+attribute [instance] monad_state_lift.mk
+local attribute [instance] monad_state_lift.has_lift
 
 section
-variables {σ : Type u} {m : Type u → Type u} [monad m] [monad_state σ m]
+variables {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m] [monad_state_lift σ m n]
 
-@[inline] def get : m σ :=
-@monad_lift _ _ _ _ (state_t.get : state σ _)
+@[inline] def get : n σ :=
+@monad_lift _ _ _ _ (state_t.get : state_t σ m _)
 
-@[inline] def put (st : σ) : m punit :=
-monad_lift (state_t.put st : state σ _)
+@[inline] def put (st : σ) : n punit :=
+monad_lift (state_t.put st : state_t σ m _)
 
-@[inline] def modify (f : σ → σ) : m punit :=
-monad_lift (state_t.modify f : state σ _)
+@[inline] def modify (f : σ → σ) : n punit :=
+monad_lift (state_t.modify f : state_t σ m _)
 end
 
 class monad_state_functor (σ σ' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
@@ -98,9 +102,3 @@ local attribute [instance] monad_state_functor.functor
 
 def zoom {σ σ'} {m n n'} [monad m] {α : Type u} (f : σ → σ') (f' : σ' → σ) [monad_state_functor σ' σ m n n'] : n α → n' α :=
 monad_map $ λ α, (state_t.zoom f f' : state_t σ' m α → state_t σ m α)
-
-def map_state_t {σ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : state_t σ m α → state_t σ m' α :=
-λ x st, f (x st)
-
-instance (σ m m') [monad m] [monad m'] : monad_functor m m' (state_t σ m) (state_t σ m') :=
-⟨@map_state_t σ m m' _ _⟩
diff --git a/library/init/category/transformers.lean b/library/init/category/transformers.lean
index 8461910569..24fe041426 100644
--- a/library/init/category/transformers.lean
+++ b/library/init/category/transformers.lean
@@ -34,7 +34,7 @@ has_monad_lift_t.monad_lift n α
 instance has_monad_lift_t_trans (m n o) [has_monad_lift n o] [has_monad_lift_t m n] : has_monad_lift_t m o :=
 ⟨λ α (ma : m α), has_monad_lift.monad_lift o α $ has_monad_lift_t.monad_lift n α ma⟩
 
-instance has_monad_lift_t_refl (m) [monad m] : has_monad_lift_t m m :=
+instance has_monad_lift_t_refl (m) : has_monad_lift_t m m :=
 ⟨λ α, id⟩
 
 /-- A functor in the category of monads. Can be used to lift monad-transforming functions.
@@ -49,6 +49,9 @@ class monad_functor_t (m m' : Type u → Type v) (n n' : Type u → Type w) :=
 
 export monad_functor_t (monad_map)
 
+def monad_map' {α : Type u} (m m' : Type u → Type v) (n n' : Type u → Type w) [monad_functor_t (λ (α : Type u), m α) (λ (α : Type u), m' punit) n (λ {α : Type u}, n' punit)] : (∀ {α}, m α → m' punit) → n α → n' punit :=
+monad_map
+
 instance monad_functor_t_trans (m m' n n' o o') [monad_functor n n' o o'] [monad_functor_t m m' n n'] : monad_functor_t m m' o o' :=
 ⟨λ α f, monad_functor.monad_map (λ α, (monad_map @f : n α → n' α))⟩
 
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index 47b6e92151..a3ec935129 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -22,7 +22,7 @@ meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit :=
 tac >> solve_goals
 
 meta def istep {α : Type} (line0 col0 line col : nat) (tac : smt_tactic α) : smt_tactic unit :=
-λ ss ts, (@scope_trace _ line col (λ _, (tac >> solve_goals) ss ts)).clamp_pos line0 line col
+⟨λ ss ts, (@scope_trace _ line col (λ _, (tac >> solve_goals).run ss ts)).clamp_pos line0 line col⟩
 
 meta def execute (tac : smt_tactic unit) : tactic unit :=
 using_smt tac
diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean
index bf2f6cf237..07f731e3ad 100644
--- a/library/init/meta/smt/smt_tactic.lean
+++ b/library/init/meta/smt/smt_tactic.lean
@@ -59,11 +59,12 @@ state_t smt_state tactic
 meta instance : has_append smt_state :=
 list.has_append
 
-meta instance : monad smt_tactic :=
-state_t.monad
-
-meta instance : monad_state smt_state smt_tactic :=
-state_t.monad_state
+section
+local attribute [reducible] smt_tactic
+meta instance : monad smt_tactic := by apply_instance
+meta instance : alternative smt_tactic := by apply_instance
+meta instance : monad_state_lift smt_state tactic smt_tactic := by apply_instance
+end
 
 /- We don't use the default state_t lift operation because only
    tactics that do not change hypotheses can be automatically lifted to smt_tactic. -/
@@ -75,21 +76,9 @@ meta instance : has_monad_lift tactic smt_tactic :=
 meta instance (α : Type) : has_coe (tactic α) (smt_tactic α) :=
 ⟨monad_lift⟩
 
-meta def smt_tactic_orelse {α : Type} (t₁ t₂ : smt_tactic α) : smt_tactic α :=
-λ ss ts, result.cases_on (t₁ ss ts)
-  result.success
-  (λ e₁ ref₁ s', result.cases_on (t₂ ss ts)
-     result.success
-     result.exception)
-
 meta instance : monad_fail smt_tactic :=
 { fail := λ α s, (tactic.fail (to_fmt s) : smt_tactic α), ..smt_tactic.monad }
 
-meta instance : alternative smt_tactic :=
-{ failure := λ α, @tactic.failed α,
-  orelse  := @smt_tactic_orelse,
-  ..smt_tactic.monad }
-
 namespace smt_tactic
 open tactic (transparency)
 meta constant intros                     : smt_tactic unit
@@ -154,9 +143,9 @@ meta def fail {α : Type} {β : Type u} [has_to_format β] (msg : β) : smt_tact
 tactic.fail msg
 
 meta def try {α : Type} (t : smt_tactic α) : smt_tactic unit :=
-λ ss ts, result.cases_on (t ss ts)
+⟨λ ss ts, result.cases_on (t.run ss ts)
  (λ ⟨a, new_ss⟩, result.success ((), new_ss))
- (λ e ref s', result.success ((), ss) ts)
+ (λ e ref s', result.success ((), ss) ts)⟩
 
 /-- `iterate_at_most n t`: repeat the given tactic at most n times or until t fails -/
 meta def iterate_at_most : nat → smt_tactic unit → smt_tactic unit
@@ -182,7 +171,7 @@ do s₁ ← get,
    return (s₁, s₂)
 
 protected meta def write : smt_state × tactic_state → smt_tactic unit :=
-λ ⟨ss, ts⟩ _ _, result.success ((), ss) ts
+λ ⟨ss, ts⟩, ⟨λ _ _, result.success ((), ss) ts⟩
 
 private meta def mk_smt_goals_for (cfg : smt_config) : list expr → list smt_goal → list expr
                                   → tactic (list smt_goal × list expr)
@@ -195,14 +184,14 @@ private meta def mk_smt_goals_for (cfg : smt_config) : list expr → list smt_go
 
 /- See slift -/
 meta def slift_aux {α : Type} (t : tactic α) (cfg : smt_config) : smt_tactic α :=
-λ ss, do
+⟨λ ss, do
    _::sgs  ← return ss | tactic.fail "slift tactic failed, there no smt goals to be solved",
    tg::tgs ← tactic.get_goals | tactic.failed,
    tactic.set_goals [tg], a ← t,
    new_tgs ← tactic.get_goals,
    (new_sgs, new_tgs) ← mk_smt_goals_for cfg new_tgs [] [],
    tactic.set_goals (new_tgs ++ tgs),
-   return (a, new_sgs ++ sgs)
+   return (a, new_sgs ++ sgs)⟩
 
 /--
   This lift operation will restart the SMT state.
@@ -225,7 +214,7 @@ do s ← get,
    return s.classical
 
 meta def num_goals : smt_tactic nat :=
-λ ss, return (ss.length, ss)
+list.length <$> get
 
 /- Low level primitives for managing set of goals -/
 meta def get_goals : smt_tactic (list smt_goal × list expr) :=
@@ -234,7 +223,7 @@ do (g₁, _) ← smt_tactic.read,
    return (g₁, g₂)
 
 meta def set_goals : list smt_goal → list expr → smt_tactic unit :=
-λ g₁ g₂ ss, tactic.set_goals g₂ >> return ((), g₁)
+λ g₁ g₂, ⟨λ ss, tactic.set_goals g₂ >> return ((), g₁)⟩
 
 private meta def all_goals_core (tac : smt_tactic unit) : list smt_goal → list expr → list smt_goal → list expr → smt_tactic unit
 | []        ts        acs act := set_goals acs (ts ++ act)
@@ -407,7 +396,7 @@ open smt_tactic
 
 meta def using_smt {α} (t : smt_tactic α) (cfg : smt_config := {}) : tactic α :=
 do ss ← smt_state.mk cfg,
-   (a, _) ← (do a ← t, iterate close, return a) ss,
+   (a, _) ← (do a ← t, iterate close, return a).run ss,
    return a
 
 meta def using_smt_with {α} (cfg : smt_config) (t : smt_tactic α) : tactic α :=
diff --git a/tests/lean/interactive/my_tac_class.lean b/tests/lean/interactive/my_tac_class.lean
index 2a06d766a2..28cd1be81f 100644
--- a/tests/lean/interactive/my_tac_class.lean
+++ b/tests/lean/interactive/my_tac_class.lean
@@ -1,14 +1,12 @@
 meta def mytac :=
 state_t nat tactic
 
-meta instance : monad mytac :=
-state_t.monad
-
-meta instance : monad_state nat mytac :=
-state_t.monad_state
-
-meta instance : has_monad_lift tactic mytac :=
-state_t.has_monad_lift _
+section
+local attribute [reducible] mytac
+meta instance : monad mytac := by apply_instance
+meta instance : monad_state_lift nat tactic mytac := by apply_instance
+meta instance : has_monad_lift tactic mytac := by apply_instance
+end
 
 meta instance (α : Type) : has_coe (tactic α) (mytac α) :=
 ⟨monad_lift⟩
@@ -19,17 +17,17 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
 t >> return ()
 
 meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac unit :=
-λ v s, result.cases_on (@scope_trace _ line col (λ_, t v s))
+⟨λ v s, result.cases_on (@scope_trace _ line col (λ_, t.run v s))
   (λ ⟨a, v⟩ new_s, result.success ((), v) new_s)
   (λ opt_msg_thunk e new_s, match opt_msg_thunk with
     | some msg_thunk :=
       let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
           interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s
     | none := interaction_monad.silent_fail new_s
-    end)
+    end)⟩
 
 meta def execute (tac : mytac unit) : tactic unit :=
-tac 0 >> return ()
+tac.run 0 >> return ()
 
 meta def save_info (p : pos) : mytac unit :=
 do v ← get,
diff --git a/tests/lean/interactive/my_tac_class.lean.expected.out b/tests/lean/interactive/my_tac_class.lean.expected.out
index 70b2b4d5d4..beb6b3c9a3 100644
--- a/tests/lean/interactive/my_tac_class.lean.expected.out
+++ b/tests/lean/interactive/my_tac_class.lean.expected.out
@@ -1,3 +1,3 @@
-{"msgs":[{"caption":"trace output","file_name":"my_tac_class.lean","pos_col":2,"pos_line":64,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"my_tac_class.lean","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"source":,"state":"Custom state: 2\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":68}
+{"record":{"source":,"state":"Custom state: 2\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":66}
diff --git a/tests/lean/interactive/rb_map_ts.lean b/tests/lean/interactive/rb_map_ts.lean
index 69fa0a2495..cbfcde1561 100644
--- a/tests/lean/interactive/rb_map_ts.lean
+++ b/tests/lean/interactive/rb_map_ts.lean
@@ -1,14 +1,12 @@
 meta def mytac :=
 state_t (name_map nat) tactic
 
-meta instance : monad mytac :=
-state_t.monad
-
-meta instance : monad_state (name_map nat) mytac :=
-state_t.monad_state
-
-meta instance : has_monad_lift tactic mytac :=
-state_t.has_monad_lift _
+section
+local attribute [reducible] mytac
+meta instance : monad mytac := by apply_instance
+meta instance : monad_state_lift (name_map nat) tactic mytac := by apply_instance
+meta instance : has_monad_lift tactic mytac := by apply_instance
+end
 
 meta instance (α : Type) : has_coe (tactic α) (mytac α) :=
 ⟨monad_lift⟩
@@ -19,7 +17,7 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
 t >> return ()
 
 meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac unit :=
-λ v s, result.cases_on (@scope_trace _ line col (λ_, t v s))
+⟨λ v s, result.cases_on (@scope_trace _ line col (λ_, t.run v s))
   (λ ⟨a, v⟩ new_s, result.success ((), v) new_s)
   (λ opt_msg_thunk e new_s,
     match opt_msg_thunk with
@@ -27,10 +25,10 @@ meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac un
       let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
           interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s
     | none := interaction_monad.silent_fail new_s
-    end)
+    end)⟩
 
 meta def execute (tac : mytac unit) : tactic unit :=
-tac (name_map.mk nat) >> return ()
+tac.run (name_map.mk nat) >> return ()
 
 meta def save_info (p : pos) : mytac unit :=
 do v ← get,
diff --git a/tests/lean/interactive/rb_map_ts.lean.expected.out b/tests/lean/interactive/rb_map_ts.lean.expected.out
index 214887f481..3ff682a1fc 100644
--- a/tests/lean/interactive/rb_map_ts.lean.expected.out
+++ b/tests/lean/interactive/rb_map_ts.lean.expected.out
@@ -1,8 +1,8 @@
-{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":69,"severity":"information","text":"test\n"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":69,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":80,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":78,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":69,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":80,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":78,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":84,"severity":"information","text":"test\n"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":69,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":80,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":78,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":84,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":92,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":92,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":82,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":82,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":90,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":90,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":70}
-{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":74}
-{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":88}
+{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":68}
+{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":72}
+{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":86}
diff --git a/tests/lean/run/1562.lean b/tests/lean/run/1562.lean
index a4bd2fde3e..3a0f450bc0 100644
--- a/tests/lean/run/1562.lean
+++ b/tests/lean/run/1562.lean
@@ -7,7 +7,7 @@ meta constant smt2_state : Type
 state_t smt2_state tactic α
 
 meta instance tactic_to_smt2_m (α : Type) : has_coe (tactic α) (smt2_m α) :=
-⟨ fun tc, fun s, do res ← tc, return (res, s) ⟩
+⟨ fun tc, ⟨fun s, do res ← tc, return (res, s)⟩ ⟩
 
 meta def reflect_arith_formula : expr → smt2_m term
 | `(has_zero.zero) := smt2.builder.int_const <$> tactic.eval_expr int `(has_zero.zero int)
diff --git a/tests/lean/run/io_state.lean b/tests/lean/run/io_state.lean
index a243dba5a1..2566b8ca21 100644
--- a/tests/lean/run/io_state.lean
+++ b/tests/lean/run/io_state.lean
@@ -14,4 +14,4 @@ do x ← get,
    print_ln y,
    put_str "end of program"
 
-#eval tst 5
+#eval tst.run 5
diff --git a/tests/lean/run/my_tac_class.lean b/tests/lean/run/my_tac_class.lean
index e37c35eda9..df2565d802 100644
--- a/tests/lean/run/my_tac_class.lean
+++ b/tests/lean/run/my_tac_class.lean
@@ -1,14 +1,12 @@
 meta def mytac :=
 state_t nat tactic
 
-meta instance : monad mytac :=
-state_t.monad
-
-meta instance : monad_state nat mytac :=
-state_t.monad_state
-
-meta instance : has_monad_lift tactic mytac :=
-state_t.has_monad_lift _
+section
+local attribute [reducible] mytac
+meta instance : monad mytac := by apply_instance
+meta instance : monad_state_lift nat tactic mytac := by apply_instance
+meta instance : has_monad_lift tactic mytac := by apply_instance
+end
 
 meta instance (α : Type) : has_coe (tactic α) (mytac α) :=
 ⟨monad_lift⟩
@@ -19,7 +17,7 @@ meta def step {α : Type} (t : mytac α) : mytac unit :=
 t >> return ()
 
 meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac unit :=
-λ v s, result.cases_on (@scope_trace _ line col (λ_, t v s))
+⟨λ v s, result.cases_on (@scope_trace _ line col (λ_, t.run v s))
   (λ ⟨a, v⟩ new_s, result.success ((), v) new_s)
   (λ opt_msg_thunk e new_s,
     match opt_msg_thunk with
@@ -27,10 +25,10 @@ meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac un
       let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
           interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s
     | none := interaction_monad.silent_fail new_s
-    end)
+    end)⟩
 
 meta def execute (tac : mytac unit) : tactic unit :=
-tac 0 >> return ()
+tac.run 0 >> return ()
 
 meta def save_info (p : pos) : mytac unit :=
 do v ← get,
diff --git a/tests/lean/run/using_smt3.lean b/tests/lean/run/using_smt3.lean
index 0ae11c07d1..da8cd68c8b 100644
--- a/tests/lean/run/using_smt3.lean
+++ b/tests/lean/run/using_smt3.lean
@@ -6,10 +6,10 @@ by using_smt $ smt_tactic.intros >> get_local `x >>= (fun a, trace a)
 open tactic_result
 
 meta def fail_if_success {α : Type} (t : smt_tactic α) : smt_tactic unit :=
-λ ss ts, match t ss ts with
+⟨λ ss ts, match t.run ss ts with
 | success _ _     := failed ts
 | exception _ _ _ := success ((), ss) ts
-end
+end⟩
 
 def my_smt_config : smt_config :=
 { pre_cfg := { zeta := tt } }