From 4e6ad1d34dac7329646f2c8fb13162d1b80e0077 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Jan 2017 18:42:27 -0800
Subject: [PATCH] fix(library/init/meta/contradiction_tactic): make sure
 contradiction uses whnf for constructor-eq-constructor case

---
 library/init/meta/contradiction_tactic.lean | 5 ++---
 tests/lean/run/tuple_head_issue.lean        | 8 ++++++++
 2 files changed, 10 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/tuple_head_issue.lean

diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean
index 626a93fce8..4b42d7bd12 100644
--- a/library/init/meta/contradiction_tactic.lean
+++ b/library/init/meta/contradiction_tactic.lean
@@ -13,8 +13,7 @@ open expr tactic decidable environment
 private meta def contra_p_not_p : list expr → list expr → tactic unit
 | []         Hs := failed
 | (H1 :: Rs) Hs :=
-  do t_0 ← infer_type H1,
-     t   ← whnf t_0,
+  do t ← infer_type H1 >>= whnf,
      (do a ← match_not t,
          H2 ← find_same_type a Hs,
          tgt ← target,
@@ -54,7 +53,7 @@ private meta def contra_not_a_refl_rel_a : list expr → tactic unit
 private meta def contra_constructor_eq : list expr → tactic unit
 | []        := failed
 | (H :: Hs) :=
-  do t ← infer_type H,
+  do t ← infer_type H >>= whnf,
      match (is_eq t) with
      | (some (lhs_0, rhs_0)) :=
        do env ← get_env,
diff --git a/tests/lean/run/tuple_head_issue.lean b/tests/lean/run/tuple_head_issue.lean
new file mode 100644
index 0000000000..e3e8fbd638
--- /dev/null
+++ b/tests/lean/run/tuple_head_issue.lean
@@ -0,0 +1,8 @@
+import data.tuple
+open nat
+universe variables u
+variable {α : Type u}
+
+def head (n) : tuple α (succ n) → α
+| ⟨[], H⟩   := by contradiction
+| ⟨a::b, H⟩ := a