diff --git a/library/init/category/transformers.lean b/library/init/category/transformers.lean
index 01b8ddff97..f4c273cb5d 100644
--- a/library/init/category/transformers.lean
+++ b/library/init/category/transformers.lean
@@ -26,7 +26,7 @@ class has_monad_lift_t (m n : Type → Type) :=
 def monad_lift {m n} [has_monad_lift_t m n] {α} : m α → n α :=
 has_monad_lift_t.monad_lift n α
 
-instance {m n} [has_monad_lift_t m n] {α} : has_coe (m α) (n α) :=
+@[reducible] def has_monad_lift_to_has_coe {m n} [has_monad_lift_t m n] {α} : has_coe (m α) (n α) :=
 ⟨monad_lift⟩
 
 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 :=
diff --git a/library/init/meta/smt_tactic.lean b/library/init/meta/smt_tactic.lean
index 9a2b134adb..53491b47c5 100644
--- a/library/init/meta/smt_tactic.lean
+++ b/library/init/meta/smt_tactic.lean
@@ -33,6 +33,9 @@ meta constant tactic_to_smt_tactic (α : Type) : tactic α → smt_tactic α
 meta instance : monad.has_monad_lift tactic smt_tactic :=
 ⟨tactic_to_smt_tactic⟩
 
+meta instance (α : Type) : has_coe (tactic α) (smt_tactic α) :=
+⟨monad.monad_lift⟩
+
 namespace smt_tactic
 open tactic
 
diff --git a/library/tools/super/cdcl_solver.lean b/library/tools/super/cdcl_solver.lean
index eb62bcd0c4..8081250367 100644
--- a/library/tools/super/cdcl_solver.lean
+++ b/library/tools/super/cdcl_solver.lean
@@ -108,6 +108,8 @@ end state
 meta def solver := state_t state tactic
 meta instance : monad solver := state_t.monad _ _
 meta instance : has_monad_lift tactic solver := monad.monad_transformer_lift (state_t state) tactic
+meta instance (α : Type) : has_coe (tactic α) (solver α) :=
+⟨monad.monad_lift⟩
 
 meta def fail {A B} [has_to_format B] (b : B) : solver A :=
 @tactic.fail A B _ b
diff --git a/library/tools/super/clause_ops.lean b/library/tools/super/clause_ops.lean
index 52da00ed35..ff0379459c 100644
--- a/library/tools/super/clause_ops.lean
+++ b/library/tools/super/clause_ops.lean
@@ -8,6 +8,8 @@ open monad tactic expr
 
 namespace super
 
+local attribute [instance] has_monad_lift_to_has_coe
+
 meta def on_left_at {m} [monad m] (c : clause) (i : ℕ)
                     [has_monad_lift_t tactic m]
                     -- f gets a type and returns a list of proofs of that type
diff --git a/library/tools/super/prover_state.lean b/library/tools/super/prover_state.lean
index 97738a4ebb..4994de3ff9 100644
--- a/library/tools/super/prover_state.lean
+++ b/library/tools/super/prover_state.lean
@@ -131,6 +131,8 @@ meta instance : has_to_tactic_format prover_state :=
 meta def prover := state_t prover_state tactic
 meta instance : monad prover := state_t.monad _ _
 meta instance : has_monad_lift tactic prover := monad.monad_transformer_lift (state_t prover_state) tactic
+meta instance (α : Type) : has_coe (tactic α) (prover α) :=
+⟨monad.monad_lift⟩
 
 meta def prover.fail {A B : Type} [has_to_format B] (msg : B) : prover A := @tactic.fail A _ _ msg