fix(library/inductive_unifier_plugin): unification problem failure on problems with inductive datatypes

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

src/kernel/inductive/inductive.cpp

@@ -823,7 +823,7 @@ bool is_elim_meta_app_core(Ctx & ctx, expr const & e) {
     if (elim_args.size() < major_idx + 1)
         return false;
     expr intro_app = ctx.whnf(elim_args[major_idx]);
-    return is_meta(intro_app);
+    return has_expr_metavar(intro_app);
 }
 
 bool is_elim_meta_app(type_checker & tc, expr const & e) {

src/kernel/type_checker.cpp

@@ -355,6 +355,15 @@ expr type_checker::infer_type(expr const & e) {
     return r;
 }
 
+expr type_checker::infer(expr const & e, buffer<constraint> & new_cnstrs) {
+    scope mk_scope(*this);
+    unsigned cs_qhead = m_cs_qhead;
+    expr r = infer_type_core(e, true);
+    for (unsigned i = cs_qhead; i < m_cs_qhead; i++)
+        new_cnstrs.push_back(m_cs[i]);
+    return r;
+}
+
 expr type_checker::check(expr const & e, level_param_names const & ps) {
     scope mk_scope(*this);
     flet<level_param_names> updt(m_params, ps);

src/kernel/type_checker.h

@@ -132,6 +132,8 @@ public:
        constraint handler can be solved.
    */
     expr infer(expr const & t) { return infer_type(t); }
+    /** \brief Infer \c t type and copy constraints associated with type inference to \c new_cnstrs */
+    expr infer(expr const & t, buffer<constraint> & new_cnstrs);
 
     /**
        \brief Type check the given expression, and return the type of \c t.

src/library/inductive_unifier_plugin.cpp

@@ -51,10 +51,12 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
         unsigned elim_num_lvls = length(elim_lvls);
         unsigned major_idx     = *inductive::get_elim_major_idx(env, const_name(elim));
         expr meta              = args[major_idx]; // save this argument, we will update it
-        lean_assert(is_meta(meta));
+        lean_assert(has_expr_metavar(meta));
         buffer<expr> margs;
         expr const & m     = get_app_args(meta, margs);
-        expr const & mtype = mlocal_type(m);
+        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;
         for (auto const & intro : inductive::inductive_decl_intros(decl)) {
             name const & intro_name = inductive::intro_rule_name(intro);
@@ -77,7 +79,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
             args[major_idx]    = hint;
             expr reduce_elim   = tc.whnf(mk_app(elim, args));
             constraint c2      = mk_eq_cnstr(reduce_elim, t, j);
-            alts.push_back(constraints({c1, c2}));
+            alts.push_back(cons(c1, cons(c2, tc_cnstrs)));
         }
         return to_lazy(to_list(alts.begin(), alts.end()));
     }

tests/lean/run/nat_bug2.lean

@@ -0,0 +1,22 @@
+import logic num
+using num eq_proofs
+
+inductive nat : Type :=
+| zero : nat
+| succ : nat → nat
+
+abbreviation plus (x y : nat) : nat
+:= nat_rec x (λn r, succ r) y
+definition to_nat [coercion] [inline] (n : num) : nat
+:= num_rec zero (λn, pos_num_rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
+definition add (x y : nat) : nat
+:= plus x y
+variable le : nat → nat → Prop
+
+infixl `+`:65 := add
+infix `≤`:50  := le
+axiom add_one (n:nat) : n + (succ zero) = succ n
+axiom add_le_right {n m : nat} (H : n ≤ m) (k : nat) : n + k ≤ m + k
+
+theorem succ_le {n m : nat} (H : n ≤ m) : succ n ≤ succ m
+:= add_one m ▸ add_one n ▸ add_le_right H 1