feat(library/init/category/transformers): disable instance has_monad_lift_t ==> has_coe

It produces non-termination because it triggers sub-problems of the
form (has_monad_lift_t t ?M), and this kind of sub-problem is bad
for the transitive closure rule:

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

The trick above only behaves well for synthesis subproblems that do not
contain sub-variables.

Note that the sub-problem (has_monad_lift_t t ?M) is created by a
similar rule used at has_coe_t.

instance {a : Type u₁} {b : Type u₂} {c : Type u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c
AND
instance {m n} [has_monad_lift_t m n] {α} : has_coe (m α) (n α) :=

We workaround the issue by disabling

  instance {m n} [has_monad_lift_t m n] {α} : has_coe (m α) (n α)

and adding instances of it. Example:

  meta instance (α : Type) : has_coe (tactic α) (solver α) := ...
  meta instance (α : Type) : has_coe (tactic α) (prover α) := ...
  meta instance (α : Type) : has_coe (tactic α) (smt_tactic α) := ...

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 :=

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
 

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

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

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