From 82e51ddad56bb76c82d9ef1f4ce403b2b867bf25 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 May 2017 16:39:38 -0700
Subject: [PATCH] fix(library/constructions/injective): fixes #1609
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

@dselsam You have assumed that the left-hand-side (t) and
right-hand-side (s) of (t = s) and (t == s) are the last two arguments.
This is a reasonable assumption, and it is correct for eq, but it is
incorrect for heq.
The type of heq is
```
Π {α : Sort u_1}, α → Π {β : Sort u_1}, β → Prop
```
Do you recall other places where we may have made this assumption?
---
 src/library/constructions/injective.cpp | 8 ++++++--
 tests/lean/run/1609.lean                | 4 ++++
 2 files changed, 10 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1609.lean

diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp
index d2cfaf2454..11d48a84d3 100644
--- a/src/library/constructions/injective.cpp
+++ b/src/library/constructions/injective.cpp
@@ -157,8 +157,12 @@ expr prove_injective(environment const & env, expr const & inj_type, name const
     while (is_pi(ty)) {
         expr eq = tctx.push_local_from_binding(ty);
         eqs.push_back(eq);
-        if (app_arg(tctx.infer(eq)) != app_arg(app_fn(tctx.infer(eq))))
+        expr eq_type = tctx.infer(eq);
+        expr lhs, rhs;
+        if ((is_eq(eq_type, lhs, rhs) && lhs != rhs) ||
+            (is_heq(eq_type, lhs, rhs) && lhs != rhs)) {
             eqs_to_keep.push_back(eq);
+        }
         ty = tctx.relaxed_whnf(instantiate(binding_body(ty), eq));
     }
 
@@ -253,7 +257,7 @@ environment mk_injective_lemmas(environment const & _env, name const & ind_name)
         expr ir_type = inductive::intro_rule_type(ir);
         expr inj_type = mk_injective_type(env, ir_name, ir_type, num_params, lp_names);
         expr inj_val = prove_injective(env, inj_type, ind_name);
-        lean_trace(name({"constructions", "injective"}), tout() << ir_name << " : " << inj_type << " :=\n  " << inj_val;);
+        lean_trace(name({"constructions", "injective"}), tout() << ir_name << " : " << inj_type << " :=\n  " << inj_val << "\n";);
         env = module::add(env, check(env, mk_definition_inferring_trusted(env, mk_injective_name(ir_name), lp_names, inj_type, inj_val, true)));
         env = mk_injective_arrow(env, ir_name);
     }
diff --git a/tests/lean/run/1609.lean b/tests/lean/run/1609.lean
new file mode 100644
index 0000000000..c80d9ef656
--- /dev/null
+++ b/tests/lean/run/1609.lean
@@ -0,0 +1,4 @@
+universe variable u
+
+inductive pred : ∀ (X : Type u), list X → Type (u+1)
+| foo X (l1 : list X) (l2 : list (option X)) : pred (option X) l2 → pred X l1