feat: type-check generated recursors in the kernel

This PR adds a defensive check to the kernel.

**TL;DR.** When the kernel generates a recursor for an inductive type, it installs the recursor and its computation rules with `add_core`, which does not re-check them. This PR adds a verification pass that (1) type-checks each generated recursor's type and (2) checks that each computation rule is type-preserving: reducing the recursor applied to a constructor yields a term whose type is the recursor's declared result type. This catches a recursor whose minor-premise type and reduction rule disagree, for example a minor premise that expects an induction hypothesis while the rule omits it. Checking only that a rule's right-hand side has some type is not enough, because an under-applied minor premise is still a well-typed (function) term. The check is defense-in-depth: it does not change what the kernel accepts for well-formed inductives, and only rejects declarations that were already malformed.

When the kernel adds an inductive type, it generates the recursor's type and its computation rules and installs them with `add_core`, which does not re-check them. The surrounding machinery is trusted to produce a consistent recursor. This PR re-verifies that output.

The check has two parts. First, the recursor's type is type-checked. Second, for each constructor, the recursor applied to that constructor is reduced by one step and the type of the reduct is compared against the type of the un-reduced application; the two must be definitionally equal. The second part is what separates a type-preserving rule from a merely well-typed right-hand side: if a minor premise's type expects an induction hypothesis that the rule does not supply, the reduct is an under-applied minor premise. That reduct still has a type, but a function type rather than the recursor's result type, so the check fails.

src/kernel/inductive.cpp

diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp
index a148923..438f92d 100644
--- a/src/kernel/inductive.cpp
+++ b/src/kernel/inductive.cpp
@@ -818,6 +818,53 @@
         }
     }
 
+    /** \brief Defensively type-check the generated recursors.
+
+        `add_core` installs a recursor and its computation rules without re-checking them. We verify
+        here that (1) each recursor's type is well typed, and (2) each computation rule is
+        type-preserving: reducing the recursor applied to a constructor yields a term whose type is
+        the recursor's declared result type. This catches a recursor whose minor-premise type and
+        reduction rule disagree; checking only that a rule's right-hand side has *some* type is
+        insufficient, because an under-applied minor premise is still a well-typed (function) term. */
+    void check_recursors() {
+        buffer<expr> Cs; collect_Cs(Cs);
+        buffer<expr> minors; collect_minor_premises(minors);
+        for (unsigned d_idx = 0; d_idx < m_ind_types.size(); d_idx++) {
+            name rec_name        = mk_rec_name(m_ind_types[d_idx].get_name());
+            constant_info rec_ci = m_env.get(rec_name);
+            /* (1) The recursor type must be well typed. */
+            tc().check(rec_ci.get_type(), get_rec_lparams());
+            expr rec_pre = mk_app(mk_app(mk_app(mk_constant(rec_name, get_rec_levels()), m_params), Cs), minors);
+            /* (2) Each computation rule must preserve types. */
+            for (constructor const & cnstr : m_ind_types[d_idx].get_cnstrs()) {
+                buffer<expr> b_u;
+                expr t     = constructor_type(cnstr);
+                unsigned i = 0;
+                while (is_pi(t)) {
+                    if (i < m_nparams) {
+                        t = instantiate(binding_body(t), m_params[i]);
+                    } else {
+                        expr l = mk_local_decl_for(t);
+                        b_u.push_back(l);
+                        t = instantiate(binding_body(t), l);
+                    }
+                    i++;
+                }
+                buffer<expr> it_indices;
+                get_I_indices(t, it_indices);
+                expr intro_app      = mk_app(mk_app(mk_constant(constructor_name(cnstr), m_levels), m_params), b_u);
+                expr lhs            = mk_app(mk_app(rec_pre, it_indices), intro_app);
+                type_checker tcheck = tc();
+                expr expected       = tcheck.infer(lhs);
+                expr reduct         = tcheck.whnf(lhs);
+                expr actual         = tcheck.infer(reduct);
+                if (!tcheck.is_def_eq(actual, expected))
+                    throw kernel_exception(m_env, sstream() << "generated recursor computation rule for '"
+                                           << constructor_name(cnstr) << "' is not type-preserving");
+            }
+        }
+    }
+
     environment operator()() {
         m_env.check_duplicated_univ_params(m_lparams);
         check_inductive_types();
@@ -828,6 +875,7 @@
         init_K_target();
         mk_rec_infos();
         declare_recursors();
+        check_recursors();
         return m_env;
     }
 };