From 7b6d06df0dd027c14bc669df67cee7b214ffdfd0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Sep 2020 17:31:09 -0700
Subject: [PATCH] fix: remove bad instances

They are unnecessary, and were producing a very big search space in a
few examples.
---
 src/Init/Control/Monad.lean | 6 ------
 src/Lean/Elab/Term.lean     | 8 +++-----
 2 files changed, 3 insertions(+), 11 deletions(-)

diff --git a/src/Init/Control/Monad.lean b/src/Init/Control/Monad.lean
index dcb0eb6bbc..0252acd662 100644
--- a/src/Init/Control/Monad.lean
+++ b/src/Init/Control/Monad.lean
@@ -52,9 +52,3 @@ condM c (pure ()) t
 @[inline] def coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
 a ← x;
 pure $ coe a
-
-instance coeMethod {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] : Coe (m α) (m β) :=
-{ coe := coeM }
-
-instance pureCoeDepProp {m : Type → Type v} [HasPure m] {p : Prop} [Decidable p] : CoeDep (m Prop) (pure p) (m Bool) :=
-{ coe := pure $ decide $ p }
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 77393e375a..565f0819d9 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -650,11 +650,9 @@ Given an expected type of the form `n β`, if `eType` is of the form `α`
 
 If `eType` is of the form `m α`. We use the following approaches.
 
-1- Try to unify `n` and `m`. If it succeeds, then we rely on `tryCoe`, and
-   the instances
+1- Try to unify `n` and `m`. If it succeeds, then we use
    ```
-   instance coeMethod {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] : Coe (m α) (m β)
-   instance pureCoeDepProp {m : Type → Type v} [HasPure m] {p : Prop} [Decidable p] : CoeDep (m Prop) (pure p) (m Bool)
+   coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β
    ```
 
 2- If there is monad lift from `m` to `n` and we can unify `α` and `β`, we use
@@ -702,7 +700,7 @@ match eNew? with
 | some eNew => pure eNew
 | none      => do
 some (m, α) ← isTypeApp? eType | tryCoe expectedType eType e f?;
-condM (isDefEq m n) (tryCoe expectedType eType e f?) $
+condM (isDefEq m n) (mkAppOptM `coeM #[m, α, β, none, monadInst, e]) $
   catch
     (do
       -- Construct lift from `m` to `n`