From 0bf51e63e8a163ac776a8ee11ace86f75cd404dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 May 2017 09:56:38 -0700
Subject: [PATCH] fix(library/init/meta/constructor_tactic): fixes #1598

---
 library/init/data/list/instances.lean     | 2 +-
 library/init/meta/constructor_tactic.lean | 6 +++++-
 tests/lean/1598.lean                      | 4 ++++
 tests/lean/1598.lean.expected.out         | 3 +++
 4 files changed, 13 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/1598.lean
 create mode 100644 tests/lean/1598.lean.expected.out

diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index f97f445596..cd875055ba 100644
--- a/library/init/data/list/instances.lean
+++ b/library/init/data/list/instances.lean
@@ -69,7 +69,7 @@ instance decidable_bex : ∀ (l : list α), decidable (∃ x ∈ l, p x)
     match decidable_bex xs with
     | is_true  hxs := is_true $ begin
         cases hxs with x' hx', cases hx' with hx' hpx',
-        existsi x', existsi (or.inr hx'), assumption, exact x' = x
+        existsi x', existsi (or.inr hx'), assumption
       end
     | is_false hxs := is_false $ begin
         intro hxxs, cases hxxs with x' hx', cases hx' with hx' hpx',
diff --git a/library/init/meta/constructor_tactic.lean b/library/init/meta/constructor_tactic.lean
index d1601fefd7..6cf94c42e6 100644
--- a/library/init/meta/constructor_tactic.lean
+++ b/library/init/meta/constructor_tactic.lean
@@ -58,6 +58,10 @@ do [c]     ← target >>= get_constructors_for | fail "existsi tactic failed, ta
    n       ← get_arity fn,
    when (n < 2) (fail "existsi tactic failed, constructor must have at least two arguments"),
    t       ← apply_num_metavars fn fn_type (n - 2),
-   apply (app t e)
+   apply (app t e),
+   t_type  ← infer_type t >>= whnf,
+   e_type  ← infer_type e,
+   (guard t_type.is_pi <|> fail "existsi tactic failed, failed to infer type"),
+   (unify t_type.binding_domain e_type <|> fail "existsi tactic failed, type mismatch between given term witness and expected type")
 
 end tactic
diff --git a/tests/lean/1598.lean b/tests/lean/1598.lean
new file mode 100644
index 0000000000..72e928e4a2
--- /dev/null
+++ b/tests/lean/1598.lean
@@ -0,0 +1,4 @@
+lemma notc :  exists b, b = false :=
+begin
+   existsi 0, -- ERROR here
+end
diff --git a/tests/lean/1598.lean.expected.out b/tests/lean/1598.lean.expected.out
new file mode 100644
index 0000000000..0de20f19a1
--- /dev/null
+++ b/tests/lean/1598.lean.expected.out
@@ -0,0 +1,3 @@
+1598.lean:3:3: error: existsi tactic failed, type mismatch between given term witness and expected type
+state:
+⊢ 0 = false