perf(frontends/lean/elaborator): do not invoke recursive equation compiler when equations still contain metavariables

src/frontends/lean/elaborator.cpp

@@ -1053,7 +1053,8 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
         substitution new_s  = s;
         expr new_eqns       = new_s.instantiate_all(eqns);
         new_eqns            = solve_unassigned_mvars(new_s, new_eqns);
-        display_unassigned_mvars(new_eqns, new_s);
+        if (display_unassigned_mvars(new_eqns, new_s))
+            return lazy_list<constraints>();
         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);
@@ -1746,7 +1747,8 @@ expr elaborator::solve_unassigned_mvars(substitution & subst, expr const & e) {
     return solve_unassigned_mvars(subst, e, visited);
 }
 
-void elaborator::display_unassigned_mvars(expr const & e, substitution const & s) {
+bool elaborator::display_unassigned_mvars(expr const & e, substitution const & s) {
+    bool r = false;
     if (check_unassigned() && has_metavar(e)) {
         substitution tmp_s(s);
         visit_unassigned_mvars(e, [&](expr const & mvar) {
@@ -1757,9 +1759,11 @@ void elaborator::display_unassigned_mvars(expr const & e, substitution const & s
                     bool relax     = true;
                     proof_state ps(goals(g), s, m_ngen, constraints(), relax);
                     display_unsolved_proof_state(mvar, ps, "don't know how to synthesize placeholder");
+                    r = true;
                 }
             });
     }
+    return r;
 }
 
 /** \brief Check whether the solution found by the elaborator is producing too specific

src/frontends/lean/elaborator.h

@@ -155,7 +155,7 @@ class elaborator : public coercion_info_manager {
     void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr const & e);
-    void display_unassigned_mvars(expr const & e, substitution const & s);
+    bool display_unassigned_mvars(expr const & e, substitution const & s);
     void check_sort_assignments(substitution const & s);
     expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params);
     std::tuple<expr, level_param_names> apply(substitution & s, expr const & e);

tests/lean/place_eqn.lean.expected.out

@@ -5,8 +5,6 @@ place_eqn.lean:5:18: 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
+place_eqn.lean:3:11: error: failed to synthesize placeholder
-remark: set 'formatter.hide_full_terms' to false to see the complete term
+
-  λ (a : ℕ),
+⊢ ℕ → ℕ
-    nat.brec_on a
-      (λ (a_1 : ℕ) (b : …), nat.cases_on a_1 (λ (b_1 : …), ?M_1) (λ (a_2 : ℕ) (b_1 : …), ?M_2) b)

tests/lean/run/eq13.lean

@@ -7,7 +7,7 @@ definition f : nat → nat → nat
 
 theorem f_zero_right : ∀ a, f a 0 = 0
 | f_zero_right 0        := rfl
-| f_zero_right (succ _) := rfl
+| f_zero_right (succ a) := rfl
 
 theorem f_zero_succ (a : nat) : f 0 (a+1) = 1 :=
 rfl

tests/lean/run/eq2.lean

@@ -1,5 +1,5 @@
 definition symm {A : Type} : Π {a b : A}, a = b → b = a
-| symm rfl := rfl
+| a a rfl := rfl
 
 definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
-| trans rfl rfl := rfl
+| a a a rfl rfl := rfl