fix(kernel/inductive/inductive): fix assertion violation when K is applied to type incorrect term

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 {

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

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)