fix(frontends/lean/elaborator): don't block on metavariables that dep…

…end on an `out_param` (#657)

We noticed in [mathlib#11128](leanprover-community/mathlib#11128) some cases where parameters weren't being inferred, even though they were `out_param`s to an instance: it turned out the instances themselves also weren't being inferred by the elaborator. This PR tweaks the logic in `elaborator::ready_to_synthesize` to match the `out_param` handling in `type_context_old::preprocess_class`.

I created a new function that determines the list of parameters that are either an `out_param` themselves, or depend on an `out_param`. The code is a bit different since `preprocess_class` updates the expression during the check. I left the previous check of `preprocess_class` in an `assert` so we can be sure the results are the same.

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Instance.20parameters.20depending.20on.20.60out_params.60

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/frontends/lean/elaborator.cpp

@@ -326,13 +326,17 @@ bool elaborator::ready_to_synthesize(expr inst_type) {
     if (!is_constant(C))
         return false;
     expr it = m_ctx.infer(C);
+    buffer<bool> is_out_param;
+    class_out_param_deps(it, is_out_param);
+    int i = 0;
     for (expr const & C_arg : C_args) {
         if (!is_pi(it))
             return false; /* failed */
-        expr const & d = binding_domain(it);
-        if (has_expr_metavar(C_arg) && !is_class_out_param(d))
+        if (has_expr_metavar(C_arg) && !is_out_param[i])
             return false;
+
         it = binding_body(it);
+        i++;
     }
     return true;
 }

src/library/class.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/fresh_name.h"
 #include "util/name_set.h"
 #include "kernel/type_checker.h"
+#include "kernel/free_vars.h"
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
 #include "library/scoped_ext.h"
@@ -307,6 +308,29 @@ bool has_class_out_params(environment const & env, name const & c) {
     return s.m_has_out_params.contains(c);
 }
 
+void class_out_param_deps(expr const & cls_type, buffer<bool> & is_out_param) {
+    expr cur_cls_type = cls_type;
+    for (unsigned int i = 0; is_pi(cur_cls_type); i++) {
+        expr const & d = binding_domain(cur_cls_type);
+
+        bool is_out = false;
+        // Is this parameter itself an out_param?
+        if (is_class_out_param(d)) {
+            is_out = true;
+        } else if (has_free_vars(d)) {
+            // Are there any bound variables in this parameter corresponding to an out_param?
+            for (unsigned int j = 0; j < i; j++) {
+                if (is_out_param[j] && has_free_var(d, i - j - 1)) {
+                    is_out = true;
+                    break;
+                }
+            }
+        }
+        is_out_param.push_back(is_out);
+        cur_cls_type = binding_body(cur_cls_type);
+    }
+}
+
 environment add_instance_core(environment const & env, name const & n, unsigned priority, bool persistent, bool disable) {
     declaration d = env.get(n);
     expr type = d.get_type();

src/library/class.h

@@ -36,6 +36,10 @@ bool is_anonymous_inst_name(name const & n);
 /** \brief Return true iff e is of the form `out_param a` */
 bool is_class_out_param(expr const & e);
 
+/** \brief Determine which arguments to `cls` have the form `out_param a`, or depend on another parameter that is an `out_param`.
+ * `cls` should be the type of an instance parameter. */
+void class_out_param_deps(expr const & cls, buffer<bool> & is_out_param);
+
 /** \brief Return true iff c is a type class that contains an `out_param` */
 bool has_class_out_params(environment const & env, name const & c);
 

src/library/type_context.cpp

@@ -4011,6 +4011,7 @@ OR
    If we reject this kind of declaration, then we don't need
    this extra case which may artificially treat regular parameters
    as `out` (**).
+These two cases are detected by `type_context_old::class_out_param_deps`.
 
 Then, we execute type class resolution as usual.
 If it succeeds, and metavariables ?x_i have been assigned, we solve the unification
@@ -4097,22 +4098,24 @@ expr type_context_old::preprocess_class(expr const & type,
     if (!u_replacements.empty())
         C = update_constant(C, to_list(C_levels));
     expr it2 = infer(C);
+    buffer<bool> is_out_param;
+    class_out_param_deps(it2, is_out_param);
+    int i = 0;
     for (expr & C_arg : C_args) {
         it2  = whnf(it2);
         if (!is_pi(it2))
             return type; /* failed */
         expr const & d = binding_domain(it2);
-        if (/* Case 1 */
-            is_class_out_param(d) ||
-            /* Case 2 */
-            depends_on_mvar(d, new_mvars)) {
+
+        if (i < is_out_param.size() && is_out_param[i]) {
             expr new_mvar = mk_tmp_mvar(locals.mk_pi(d));
             new_mvars.push_back(new_mvar);
             expr new_arg  = mk_app(new_mvar, locals.as_buffer());
             e_replacements.emplace_back(C_arg, new_arg);
             C_arg = new_arg;
         }
         it2 = instantiate(binding_body(it2), C_arg);
+        i++;
     }
     expr new_class = mk_app(C, C_args);
     return locals.mk_pi(new_class);

tests/lean/run/tc_out_param_deps.lean

@@ -0,0 +1,23 @@
+prelude
+import init.core
+
+class semiring (G : Type*) := (one : G)
+
+instance : semiring nat := ⟨1⟩
+
+class add_monoid_hom_class (F : Type*) (H : out_param Type*) [semiring H] :=
+(coe : F → nat → H)
+(ext_nat : ∀ (f g : F), coe f 1 = coe g 1 → f = g)
+
+open add_monoid_hom_class
+
+class semiring_hom_class (F : Type*) (H : out_param Type*) [semiring H]
+  extends add_monoid_hom_class F H :=
+(map_one : ∀ (f : F), coe f 1 = semiring.one)
+
+-- Ensure `H` can be inferred through the `out_param` of `semiring_hom_class`,
+-- even though `semiring H` is a non-out_param depending on it.
+lemma semiring_hom_class.ext_nat {F : Type*} {H : Type*} [semiring H]
+  [semiring_hom_class F H] (f g : F) : f = g :=
+add_monoid_hom_class.ext_nat f g $
+  (semiring_hom_class.map_one f).trans (semiring_hom_class.map_one g).symm