From 68629b2e5fc70ec567acc84825d32955e5c5b8ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Jan 2017 09:15:25 -0800
Subject: [PATCH] feat(library/init/category/transformers): disable instance
 has_monad_lift_t ==> has_coe
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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 | 2 +-
 library/init/meta/smt_tactic.lean       | 3 +++
 library/tools/super/cdcl_solver.lean    | 2 ++
 library/tools/super/clause_ops.lean     | 2 ++
 library/tools/super/prover_state.lean   | 2 ++
 5 files changed, 10 insertions(+), 1 deletion(-)

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