From e3efe39eeb42676fd456f06ace60122bab1282ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Oct 2013 17:53:37 -0700
Subject: [PATCH] fix(elaborator): fix bug in higher-order matching/unification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/frontend_elaborator.cpp | 4 ++++
 src/library/elaborator/elaborator.cpp      | 5 +++--
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index 87d7a9323..ac32b8114 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -332,6 +332,10 @@ public:
         // std::cout << "After preprocessing\n" << new_e << "\n";
         if (has_metavar(new_e)) {
             m_type_checker.infer_type(new_e, context(), &m_menv, m_ucs);
+            // for (auto c : m_ucs) {
+            //     formatter fmt = mk_simple_formatter();
+            //     std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
+            // }
             substitution s = elaborate_core();
             return instantiate_metavars(new_e, s);
         } else {
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 65eb57f20..6cda633fb 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -732,6 +732,7 @@ class elaborator::imp {
         state new_state(m_state);
         justification new_assumption = mk_assumption();
         expr imitation;
+        lean_assert(arg_types.size() == num_a - 1);
         if (is_app(b)) {
             // Imitation for applications
             expr f_b          = arg(b, 0);
@@ -739,7 +740,7 @@ class elaborator::imp {
             // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), f_b (h_1 x_1 ... x_{num_a-1}) ... (h_{num_b-1} x_1 ... x_{num_a-1})
             // New constraints (h_i a_1 ... a_{num_a-1}) == arg(b, i)
             buffer<expr> imitation_args; // arguments for the imitation
-            imitation_args.push_back(f_b);
+            imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1));
             for (unsigned i = 1; i < num_b; i++) {
                 expr h_i = new_state.m_menv.mk_metavar(ctx);
                 imitation_args.push_back(mk_app_vars(h_i, num_a - 1));
@@ -767,7 +768,7 @@ class elaborator::imp {
             expr h_2 = new_state.m_menv.mk_metavar(new_ctx);
             push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption);
             push_new_eq_constraint(new_state.m_queue, new_ctx,
-                                   mk_app(update_app(a, 0, h_2), Var(0)), abst_body(b), new_assumption);
+                                   mk_app(update_app(a, 0, h_2), mk_var(0)), abst_body(b), new_assumption);
             imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a)));
         } else {
             // "Dumb imitation" aka the constant function