From ef75cac1c0e46c43400df5f37e6b79a93f178db2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 25 Nov 2014 12:54:07 -0800
Subject: [PATCH] feat(kernel/expr): change the rules for inferring implicit
 arguments, closes #344

---
 src/kernel/expr.cpp                     | 11 +++++++----
 src/library/definitional/projection.cpp |  4 +++-
 tests/lean/run/imp3.lean                | 12 ++++++++++++
 3 files changed, 22 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/imp3.lean

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index e89144841..2688df684 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -596,9 +596,13 @@ optional<expr> has_expr_metavar_strict(expr const & e) {
     return r;
 }
 
-static bool has_free_var_in_domain(expr const & b, unsigned vidx) {
+static bool has_free_var_in_domain(expr const & b, unsigned vidx, bool strict) {
     if (is_pi(b)) {
-        return has_free_var(binding_domain(b), vidx) || has_free_var_in_domain(binding_body(b), vidx+1);
+        return
+            (has_free_var(binding_domain(b), vidx) && is_explicit(binding_info(b))) ||
+            has_free_var_in_domain(binding_body(b), vidx+1, strict);
+    } else if (!strict) {
+        return has_free_var(b, vidx);
     } else {
         return false;
     }
@@ -612,8 +616,7 @@ expr infer_implicit(expr const & t, unsigned num_params, bool strict) {
         if (binding_info(t).is_implicit() || binding_info(t).is_strict_implicit()) {
             // argument is already marked as implicit
             return update_binding(t, binding_domain(t), new_body);
-        } else if ((strict  && has_free_var_in_domain(new_body, 0)) ||
-                   (!strict && has_free_var(new_body, 0))) {
+        } else if (has_free_var_in_domain(new_body, 0, strict)) {
             return update_binding(t, binding_domain(t), new_body, mk_implicit_binder_info());
         } else {
             return update_binding(t, binding_domain(t), new_body);
diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp
index 937bd1f50..424ae854b 100644
--- a/src/library/definitional/projection.cpp
+++ b/src/library/definitional/projection.cpp
@@ -68,7 +68,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
     for (unsigned i = 0; i < nparams; i++) {
         if (!is_pi(intro_type))
             throw_ill_formed(n);
-        expr param = mk_local(ngen.next(), binding_name(intro_type), binding_domain(intro_type), mk_implicit_binder_info());
+        expr param = mk_local(ngen.next(), binding_name(intro_type), binding_domain(intro_type), binder_info());
         intro_type = instantiate(binding_body(intro_type), param);
         params.push_back(param);
     }
@@ -107,6 +107,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         rec_args.push_back(major_premise);
         expr rec_app      = mk_app(rec, rec_args);
         expr proj_type    = Pi(proj_args, result_type);
+        bool strict       = false;
+        proj_type         = infer_implicit(proj_type, nparams, strict);
         expr proj_val     = Fun(proj_args, rec_app);
         bool opaque       = false;
         bool use_conv_opt = false;
diff --git a/tests/lean/run/imp3.lean b/tests/lean/run/imp3.lean
new file mode 100644
index 000000000..9fc586ce9
--- /dev/null
+++ b/tests/lean/run/imp3.lean
@@ -0,0 +1,12 @@
+structure is_equiv [class] {A B : Type} (f : A → B) :=
+  (inv : B → A)
+
+check @is_equiv.inv
+namespace is_equiv
+context
+   parameters A B : Type
+   parameter  f : A → B
+   parameter  c : is_equiv f
+   check inv f
+end
+end is_equiv