Fix bug in ho_unifier

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

src/library/ho_unifier.cpp

@@ -236,6 +236,19 @@ class ho_unifier::imp {
         bool failed() const { return m_failed; }
     };
 
+    /**
+       \brief Create the term (fun (x_0 : types[0]) ... (x_{n-1} : types[n-1]) body)
+     */
+    expr mk_lambda(buffer<expr> const & types, expr const & body) {
+        expr r = body;
+        unsigned i = types.size();
+        while (i > 0) {
+            --i;
+            r = ::lean::mk_lambda(name(g_x_name, i), types[i], r);
+        }
+        return r;
+    }
+
     /**
        \brief Process a constraint <tt>ctx |- a = b</tt> where \c a is of the form <tt>(?m ...)</tt>.
        We perform a "case split" using "projection" or "imitation". See Huet&Lang's paper on higher order matching
@@ -264,12 +277,10 @@ class ho_unifier::imp {
         m_state_stack.pop_back();
         // add projections
         for (unsigned i = 1; i < num_a; i++) {
-            expr proj = mk_var(i - 1);
-            for (unsigned j = 1; j < num_a; j++)
-                proj = mk_lambda(name(g_x_name, j), arg_types[j - 1], proj);
             cqueue new_q = q;
             new_q.push_front(constraint(ctx, arg(a, i), b));
             metavar_env new_s = s;
+            expr proj         = mk_lambda(arg_types, mk_var(num_a - i - 1));
             new_s.assign(midx, proj);
             m_state_stack.push_back(mk_state(new_s, new_q));
         }
@@ -294,17 +305,13 @@ class ho_unifier::imp {
                 imitation_args.push_back(mk_app(h_app_var_args.size(), h_app_var_args.data()));
                 new_q.push_front(constraint(ctx, mk_app(h_app_subst_args.size(), h_app_subst_args.data()), arg(b, i)));
             }
-            expr imitation = mk_app(imitation_args.size(), imitation_args.data());
+            expr imitation = mk_lambda(arg_types, mk_app(imitation_args.size(), imitation_args.data()));
-            for (unsigned j = 1; j < num_a; j++)
-                imitation = mk_lambda(name(g_x_name, j), arg_types[j - 1], imitation);
             new_s.assign(midx, imitation);
             m_state_stack.push_back(mk_state(new_s, new_q));
         } else {
             // TODO(Leo) handle eq like we handle applications
             // make f_a the constant function
-            expr imitation = lift_free_vars(b, 0, num_a - 1);
+            expr imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1));
-            for (unsigned j = 1; j < num_a; j++)
-                imitation = mk_lambda(name(g_x_name, j), arg_types[j - 1], imitation);
             new_s.assign(midx, imitation);
             m_state_stack.push_back(mk_state(new_s, new_q));
         }

src/tests/library/ho_unifier.cpp

@@ -16,20 +16,24 @@ void tst1() {
     metavar_env menv;
     ho_unifier  unify(env);
     expr N  = Const("N");
+    expr M  = Const("M");
     env.add_var("N", Type());
-    env.add_var("f", N >> (N >> N));
+    env.add_var("M", Type());
+    env.add_var("f", N >> (M >> M));
     env.add_var("a", N);
-    env.add_var("b", N);
+    env.add_var("b", M);
     expr f  = Const("f");
     expr x  = Const("x");
     expr a  = Const("a");
     expr b  = Const("b");
     expr m1 = menv.mk_metavar();
     expr m2 = menv.mk_metavar();
-    expr l = m1(b);
+    expr l = m1(b, a);
     expr r = f(b, f(a, b));
     for (auto sol : unify(context(), l, r, menv)) {
         std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n";
+        std::cout << beta_reduce(instantiate_metavars(l, sol.first)) << "\n";
+        lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == r);
         std::cout << "--------------\n";
     }
 }