fix(library/type_context): unifier failed to solve `?m =?= fun x_1 ..…

…. x_n, ?m x_1 ... x_n`

Before this commit, the unifier would try to solve the unification consraint

     ?m =?= fun x_1 ... x_n, ?m x_1 ... x_n

by assigning

     ?m := fun x_1 ... x_n, ?m x_1 ... x_n

which fails the occurs check.

This commit skips the assignment by using eta-reduction.

src/library/type_context.cpp

@@ -2433,16 +2433,9 @@ expr type_context_old::complete_instance(expr const & e) {
     return e;
 }
 
-/*
-If `e` is an unassigned metavariable, then return `some(e)`.
-If `e` is of the form `fun (x_1 ... x_n), ?m x_1 ... x_n)`, and `?m` is unassigned, then return `some(?m)`.
-Otherwise, return `none`.
-
-We use this method to implement `is_def_eq_args`.
-*/
-optional<expr> type_context_old::is_unassigned_mvar_arg(expr const & e) {
-    if (is_mode_mvar(e) && !is_assigned(e))
-        return some_expr(e);
+/* If `e` is of the form `(fun x_1 ... x_n, f x_1 ... x_n)` and `f` does not contain `x_1`, ..., `x_n`,
+   then return `some(f)`. Otherwise, return `none` */
+static optional<expr> is_eta_expanded(expr const & e) {
     if (!is_lambda(e))
         return none_expr();
     expr it    = e;
@@ -2459,12 +2452,28 @@ optional<expr> type_context_old::is_unassigned_mvar_arg(expr const & e) {
             return none_expr();
         it = app_fn(it);
     }
-    if (is_mode_mvar(it) && !is_assigned(it))
+    if (closed(it))
         return some_expr(it);
     else
         return none_expr();
 }
 
+/*
+If `e` is an unassigned metavariable, then return `some(e)`.
+If `e` is of the form `fun (x_1 ... x_n), ?m x_1 ... x_n)`, and `?m` is unassigned, then return `some(?m)`.
+Otherwise, return `none`.
+
+We use this method to implement `is_def_eq_args`.
+*/
+optional<expr> type_context_old::is_eta_unassigned_mvar(expr const & e) {
+    if (is_mode_mvar(e) && !is_assigned(e))
+        return some_expr(e);
+    if (auto r = is_eta_expanded(e))
+        if (is_mode_mvar(*r) && !is_assigned(*r))
+            return r;
+    return none_expr();
+}
+
 bool type_context_old::is_def_eq_args(expr const & e1, expr const & e2) {
     lean_assert(is_app(e1) && is_app(e2));
     buffer<expr> args1, args2;
@@ -2504,7 +2513,7 @@ bool type_context_old::is_def_eq_args(expr const & e1, expr const & e2) {
     */
     for (param_info const & pinfo : finfo.get_params_info()) {
         if (pinfo.is_inst_implicit() || pinfo.is_implicit()) {
-            if (is_unassigned_mvar_arg(args1[i]) || is_unassigned_mvar_arg(args2[i])) {
+            if (is_eta_unassigned_mvar(args1[i]) || is_eta_unassigned_mvar(args2[i])) {
                 if (!is_def_eq_core(args1[i], args2[i]))
                     return false;
             } else {
@@ -2676,6 +2685,8 @@ static bool mvar_has_user_facing_name(expr const & m) {
     return mlocal_name(m) != mlocal_pp_name(m);
 }
 
+
+
 lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
     if (e1 == e2)
         return l_true;
@@ -2685,7 +2696,6 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
         return to_lbool(is_def_eq_core(get_annotation_arg(e1), e2));
     if (is_annotation(e2))
         return to_lbool(is_def_eq_core(e1, get_annotation_arg(e2)));
-
     expr const & f1 = get_app_fn(e1);
     expr const & f2 = get_app_fn(e2);
 
@@ -2707,6 +2717,10 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
 
     if (is_mode_mvar(f1)) {
         lean_assert(!is_assigned(f1));
+        if (optional<expr> ee2 = is_eta_expanded(e2)) {
+            if (e1 == *ee2)
+                return l_true; /* ?m =?= (fun x_1 ... x_n, ?m x_1 ... x_n) */
+        }
         if (m_update_left && !is_mode_mvar(f2)) {
             return to_lbool(process_assignment(e1, e2));
         } else if (m_update_left && in_tmp_mode()) {
@@ -2768,6 +2782,10 @@ lbool type_context_old::quick_is_def_eq(expr const & e1, expr const & e2) {
 
     if (is_mode_mvar(f2)) {
         lean_assert(!is_assigned(f2));
+        if (optional<expr> ee1 = is_eta_expanded(e1)) {
+            if (e2 == *ee1)
+                return l_true; /* (fun x_1 ... x_n, ?m x_1 ... x_n) =?= ?m */
+        }
         if (m_update_right) {
             swap_update_flags_scope scope(*this);
             /* We need to swap `m_update_left` and `m_update_right` because `process_assignment` uses `is_def_eq` */

src/library/type_context.h

@@ -962,7 +962,7 @@ class type_context_old : public abstract_type_context {
     bool is_def_eq_core(expr const & t, expr const & s);
     bool is_def_eq_binding(expr e1, expr e2);
     expr try_to_unstuck_using_complete_instance(expr const & e);
-    optional<expr> is_unassigned_mvar_arg(expr const & e);
+    optional<expr> is_eta_unassigned_mvar(expr const & e);
     bool is_def_eq_args(expr const & e1, expr const & e2);
     bool is_def_eq_eta(expr const & e1, expr const & e2);
     bool is_def_eq_proof_irrel(expr const & e1, expr const & e2);

tests/lean/run/mvar_eta_issue.lean

@@ -0,0 +1,26 @@
+open tactic
+example : true :=
+by do
+  let n : expr  := `(nat),
+  let t : expr  := `(nat → nat),
+  m ← mk_meta_var t,
+  let em : expr := (expr.lam `x binder_info.default n (expr.app m (expr.var 0))),
+  /- The unification constraint
+        ?m =?= (fun x, ?m x)
+     should work.
+  -/
+  unify m em,
+  constructor
+
+example : true :=
+by do
+  let n : expr  := `(nat),
+  let t : expr  := `(nat → nat),
+  m ← mk_meta_var t,
+  let em : expr := (expr.lam `x binder_info.default n (expr.app m (expr.var 0))),
+  /- The unification constraint
+        ?m =?= (fun x, ?m x)
+     should work.
+  -/
+  unify em m,
+  constructor