fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/type_checker.cpp

@@ -406,6 +406,20 @@ bool type_checker::is_def_eq(expr const & t, expr const & s, justification const
     return is_def_eq(t, s, djst);
 }
 
+bool type_checker::is_def_eq_types(expr const & t, expr const & s, justification const & j, buffer<constraint> & new_cnstrs) {
+    scope mk_scope(*this);
+    unsigned cs_qhead = m_cs_qhead;
+    expr r1 = infer_type_core(t, true);
+    expr r2 = infer_type_core(s, true);
+    if (is_def_eq(r1, r2, j)) {
+        for (unsigned i = cs_qhead; i < m_cs_qhead; i++)
+            new_cnstrs.push_back(m_cs[i]);
+        return true;
+    } else {
+        return false;
+    }
+}
+
 /** \brief Return true iff \c e is a proposition */
 bool type_checker::is_prop(expr const & e) {
     scope mk_scope(*this);

src/kernel/type_checker.h

@@ -147,6 +147,10 @@ public:
     bool is_def_eq(expr const & t, expr const & s);
     bool is_def_eq(expr const & t, expr const & s, justification const & j);
     bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst);
+    /** \brief Return true iff \c t and \c s (may b) definitionally equal (modulo constraints)
+        New constraints associated with test are store in \c new_cnstrs.
+    */
+    bool is_def_eq_types(expr const & t, expr const & s, justification const & j, buffer<constraint> & new_cnstrs);
     /** \brief Return true iff t is a proposition. */
     bool is_prop(expr const & t);
     /** \brief Return the weak head normal form of \c t. */

src/library/inductive_unifier_plugin.cpp

@@ -44,7 +44,8 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
        to the different constructors of decl.
     */
     lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl,
-                                                expr const & elim, buffer<expr> & args, expr const & t, justification const & j) const {
+                                                expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
+                                                buffer<constraint> & tc_cnstr_buffer) const {
         lean_assert(is_constant(elim));
         environment const & env = tc.env();
         levels elim_lvls       = const_levels(elim);
@@ -54,7 +55,6 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
         lean_assert(has_expr_metavar(meta));
         buffer<expr> margs;
         expr const & m     = get_app_args(meta, margs);
-        buffer<constraint> tc_cnstr_buffer;
         expr mtype = tc.infer(m, tc_cnstr_buffer);
         list<constraint> tc_cnstrs = to_list(tc_cnstr_buffer.begin(), tc_cnstr_buffer.end());
         buffer<constraints> alts;
@@ -87,14 +87,17 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     lazy_list<constraints> process_elim_meta_core(type_checker & tc, name_generator const & ngen,
                                                   expr const & lhs, expr const & rhs, justification const & j) const {
         lean_assert(inductive::is_elim_meta_app(tc, lhs));
+        buffer<constraint> tc_cnstr_buffer;
+        if (!tc.is_def_eq_types(lhs, rhs, j, tc_cnstr_buffer))
+            return lazy_list<constraints>();
         buffer<expr> args;
         expr const & elim = get_app_args(lhs, args);
         environment const & env = tc.env();
         auto it_name = *inductive::is_elim_rule(env, const_name(elim));
-        auto decls = *inductive::is_inductive_decl(env, it_name);
+        auto decls   = *inductive::is_inductive_decl(env, it_name);
         for (auto const & d : std::get<2>(decls)) {
             if (inductive::inductive_decl_name(d) == it_name)
-                return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j);
+                return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, tc_cnstr_buffer);
         }
         lean_unreachable(); // LCOV_EXCL_LINE
     }

tests/lean/run/nat_bug4.lean

@@ -0,0 +1,17 @@
+import logic num
+using num eq_proofs
+
+inductive nat : Type :=
+| zero : nat
+| succ : nat → nat
+
+definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
+infixl `+`:65 := add
+definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
+infixl `*`:75 := mul
+
+axiom mul_succ_right (n m : nat) : n * succ m = n * m + n
+
+theorem small2 (n m l : nat) : n * succ l + m = n * l + n + m
+:= subst (mul_succ_right _ _) (refl (n * succ l + m))
+