fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler

src/frontends/lean/elaborator.cpp

@@ -955,16 +955,20 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) {
     return update_equations(eqns, new_eqs);
 }
 
-static constraint mk_equations_cnstr(environment const & env, io_state const & ios, expr const & m, expr const & eqns,
+constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
-                                     bool relax) {
+    bool relax               = m_relax_main_opaque;
-    justification j         = mk_failed_to_synthesize_jst(env, m);
+    environment const & _env = env();
+    io_state const & _ios    = ios();
+    justification j          = mk_failed_to_synthesize_jst(_env, m);
     auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
                          name_generator const & ngen) {
         substitution new_s  = s;
-        expr new_eqns       = substitution(s).instantiate_all(eqns);
+        expr new_eqns       = new_s.instantiate_all(eqns);
-        type_checker_ptr tc = mk_type_checker(env, ngen, relax);
+        new_eqns            = solve_unassigned_mvars(new_s, new_eqns);
+        display_unassigned_mvars(new_eqns, new_s);
+        type_checker_ptr tc = mk_type_checker(_env, ngen, relax);
         new_eqns            = assign_equation_lhs_metas(*tc, new_eqns);
-        expr val            = compile_equations(*tc, ios, new_eqns, meta, meta_type, relax);
+        expr val            = compile_equations(*tc, _ios, new_eqns, meta, meta_type, relax);
         justification j     = mk_justification("equation compilation", some_expr(eqns));
         constraint c        = mk_eq_cnstr(meta, val, j, relax);
         return lazy_list<constraints>(c);
@@ -1025,7 +1029,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) {
     expr type = binding_domain(*first_eq);
     expr m = m_full_context.mk_meta(m_ngen, some_expr(type), eqns.get_tag());
     register_meta(m);
-    constraint c = mk_equations_cnstr(env(), ios(), m, new_eqns, m_relax_main_opaque);
+    constraint c = mk_equations_cnstr(m, new_eqns);
     cs += c;
     return m;
 }

src/frontends/lean/elaborator.h

@@ -165,6 +165,7 @@ class elaborator : public coercion_info_manager {
     expr visit_equation(expr const & e, constraint_seq & cs);
     expr visit_inaccessible(expr const & e, constraint_seq & cs);
     expr visit_decreasing(expr const & e, constraint_seq & cs);
+    constraint mk_equations_cnstr(expr const & m, expr const & eqns);
 
 public:
     elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false);

tests/lean/place_eqn.lean

@@ -0,0 +1,5 @@
+open nat
+
+definition foo : nat → nat,
+foo zero     := _,
+foo (succ a) := _

tests/lean/place_eqn.lean.expected.out

@@ -0,0 +1,12 @@
+place_eqn.lean:4:16: error: don't know how to synthesize placeholder
+foo : ℕ → ℕ
+⊢ ℕ
+place_eqn.lean:5:16: error: don't know how to synthesize placeholder
+foo : ℕ → ℕ,
+a : ℕ
+⊢ ℕ
+place_eqn.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
+  λ (a : ℕ),
+    nat.brec_on a
+      (λ (a_1 : ℕ) (b : nat.below a_1),
+         nat.cases_on a_1 (λ (b_1 : nat.below 0), ?M_1) (λ (a_2 : ℕ) (b_1 : nat.below (succ a_2)), ?M_2) b)

tests/lean/run/eqn_tac.lean

@@ -0,0 +1,18 @@
+open nat
+
+definition foo : nat → nat,
+foo zero     := begin exact zero end,
+foo (succ a) := begin exact a end
+
+example : foo zero = zero := rfl
+example (a : nat) : foo (succ a) = a := rfl
+
+definition bla : nat → nat,
+bla zero := zero,
+bla (succ a) :=
+  begin
+    apply foo,
+    exact a
+  end
+
+example (a : nat) : foo (succ a) = bla (succ (succ a)) := rfl