fix(library/elaborator): in optimization for metavariable free terms

The optimization was incorrect if the term indirectly contained a metavariable.
It could happen if the term contained a free variable that was assigned in the context to a term containing a metavariable.

This commit also adds a new test that exposes the problem.

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

src/library/elaborator/elaborator.cpp

@@ -1391,11 +1391,38 @@ class elaborator::imp {
         push_new_eq_constraint(ctx, m, update_abstraction(pi, abst_domain(pi), m1), new_jst);
     }
 
+    /**
+       \brief Return true iff \c a has not metavar and no free
+       variable that is assigned to a term containing metavariables in
+       ctx.
+    */
+    bool has_no_metavar(context const & ctx, expr const & a) {
+        if (has_metavar(a))
+            return false;
+        bool found = false;
+        for_each(a, [&](expr const & e, unsigned offset) {
+                if (found) return false; // stop the search
+                if (is_var(e)) {
+                    unsigned vidx = var_idx(e);
+                    if (vidx >= offset) {
+                        vidx -= offset;
+                        auto entry = find(ctx, vidx);
+                        if (entry && entry->get_body() && has_metavar(*entry->get_body())) {
+                            found = true;
+                            return false;
+                        }
+                    }
+                }
+                return true;
+            });
+        return !found;
+    }
+
     bool process_eq_convertible(context const & ctx, expr const & a, expr const & b, unification_constraint const & c) {
         bool eq = is_eq(c);
         if (a == b)
             return true;
-        if (!has_metavar(a) && !has_metavar(b)) {
+        if (has_no_metavar(ctx, a) && has_no_metavar(ctx, b)) {
             if (m_type_inferer.is_convertible(a, b, ctx)) {
                 return true;
             } else {

tests/lean/elab_bug1.lean

@@ -0,0 +1,4 @@
+set_option pp::implicit true
+check let P :  Nat → Bool    := λ x, x ≠ 0,
+          Q :  ∀ x, P (x + 1) := λ x, Nat::succ_nz x
+      in  Q

tests/lean/elab_bug1.lean.expected.out

@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Set: lean::pp::implicit
+let P : ℕ → Bool := λ x : ℕ, @neq ℕ x 0, Q : ∀ x : ℕ, P (x + 1) := λ x : ℕ, Nat::succ_nz x in Q :
+    ∀ x : ℕ, (λ x : ℕ, @neq ℕ x 0) (x + 1)