fix(library/init/meta/constructor_tactic): fixes #1598

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',

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

tests/lean/1598.lean

@@ -0,0 +1,4 @@
+lemma notc :  exists b, b = false :=
+begin
+   existsi 0, -- ERROR here
+end

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