From ad4c7c20f966215c4d4d86d1f26d5fa31528771f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 Jan 2015 11:22:14 -0800
Subject: [PATCH] fix(kernel/inductive/inductive): fix assertion violation when
 K is applied to type incorrect term

---
 src/kernel/inductive/inductive.cpp | 13 ++++++-------
 tests/lean/K_bug.lean              | 18 ++++++++++++++++++
 tests/lean/K_bug.lean.expected.out |  6 ++++++
 3 files changed, 30 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/K_bug.lean
 create mode 100644 tests/lean/K_bug.lean.expected.out

diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 3e26589a7..51b8f3dec 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -891,24 +891,23 @@ auto inductive_normalizer_extension::operator()(expr const & e, extension_contex
             // If the inductive type support K-like reduction
             // we try to replace the term with associated nullary
             // intro rule
-            auto app_type_cs = ctx.infer_type(intro_app);
-            expr app_type    = app_type_cs.first;
+            expr app_type    = ctx.whnf(ctx.infer_type(intro_app, cs), cs);
             if (has_expr_metavar(app_type))
                 return none_ecs();
+            expr const & app_type_I = get_app_fn(app_type);
+            if (!is_constant(app_type_I) || const_name(app_type_I) != it1->m_inductive_name)
+                return none_ecs(); // e is type incorrect
             auto new_intro_app = mk_nullary_intro(env, app_type, it1->m_num_params);
             if (!new_intro_app)
                 return none_ecs();
-            auto new_type_cs = ctx.infer_type(*new_intro_app);
-            expr new_type    = new_type_cs.first;
+            expr new_type    = ctx.infer_type(*new_intro_app, cs);
             if (has_expr_metavar(new_type))
                 return none_ecs();
             simple_delayed_justification jst([=]() {
                     return mk_justification("elim/intro global parameters must match", some_expr(e));
                 });
-            auto dcs = ctx.is_def_eq(app_type, new_type, jst);
-            if (!dcs.first)
+            if (!ctx.is_def_eq(app_type, new_type, jst, cs))
                 return none_ecs();
-            cs += app_type_cs.second + new_type_cs.second + dcs.second;
             intro_app = *new_intro_app;
             it2 = ext.m_comp_rules.find(const_name(get_app_fn(intro_app)));
         } else {
diff --git a/tests/lean/K_bug.lean b/tests/lean/K_bug.lean
new file mode 100644
index 000000000..e0743cd33
--- /dev/null
+++ b/tests/lean/K_bug.lean
@@ -0,0 +1,18 @@
+open eq.ops
+
+inductive Nat : Type :=
+zero : Nat,
+succ : Nat → Nat
+
+namespace Nat
+
+definition pred (n : Nat) := Nat.rec zero (fun m x, m) n
+theorem pred_succ (n : Nat) : pred (succ n) = n := rfl
+
+theorem succ_inj {n m : Nat} (H : succ n = succ m) : n = m
+:= calc
+    n = pred (succ n) : pred_succ n⁻¹
+  ... = pred (succ m) : {H}
+  ... = m             : pred_succ m
+
+end Nat
diff --git a/tests/lean/K_bug.lean.expected.out b/tests/lean/K_bug.lean.expected.out
new file mode 100644
index 000000000..fdb434fbc
--- /dev/null
+++ b/tests/lean/K_bug.lean.expected.out
@@ -0,0 +1,6 @@
+K_bug.lean:14:24: error: type mismatch at term
+  pred_succ n ⁻¹
+has type
+  pred (succ n ⁻¹) = n ⁻¹
+but is expected to have type
+  n = pred (succ n)