feat(frontends/lean/coercion_elaborator): implement "coercion lifting"

closes #644

src/frontends/lean/coercion_elaborator.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/metavar.h"
 #include "kernel/constraint.h"
+#include "kernel/abstract.h"
 #include "library/coercion.h"
 #include "library/unifier.h"
 #include "library/choice_iterator.h"
@@ -21,23 +22,45 @@ coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr cons
     lean_assert(use_id  || length(m_coercions)     == length(m_choices));
 }
 
-list<expr> get_coercions_from_to(type_checker & /* from_tc */, type_checker & to_tc,
+list<expr> get_coercions_from_to(type_checker & from_tc, type_checker & to_tc,
                                  expr const & from_type, expr const & to_type, constraint_seq & cs) {
     constraint_seq new_cs;
     environment const & env = to_tc.env();
-    expr whnf_to_type = to_tc.whnf(to_type, new_cs);
-    expr const & fn   = get_app_fn(whnf_to_type);
-    list<expr> r;
-    if (is_constant(fn)) {
-        r = get_coercions(env, from_type, const_name(fn));
-    } else if (is_pi(whnf_to_type)) {
-        r = get_coercions_to_fun(env, from_type);
-    } else if (is_sort(whnf_to_type)) {
-        r = get_coercions_to_sort(env, from_type);
+    expr whnf_from_type = from_tc.whnf(from_type, new_cs);
+    expr whnf_to_type   = to_tc.whnf(to_type, new_cs);
+    if (is_arrow(whnf_from_type)) {
+        // Try to lift coercions.
+        // The idea is to convert a coercion from A to B, into a coercion from D->A to D->B
+        if (!is_arrow(whnf_to_type))
+            return list<expr>(); // failed
+        if (!from_tc.is_def_eq(binding_domain(whnf_from_type), binding_domain(whnf_to_type), justification(), new_cs))
+            return list<expr>(); // failed, the domains must be definitionally equal
+        list<expr> coe = get_coercions_from_to(from_tc, to_tc, binding_body(whnf_from_type), binding_body(whnf_to_type), new_cs);
+        if (coe) {
+            cs += new_cs;
+            // Remark: each coercion c in coe is a function from A to B
+            // We create a new list: (fun (f : D -> A) (x : D), c (f x))
+            expr f = mk_local(from_tc.mk_fresh_name(), "f", whnf_from_type, binder_info());
+            expr x = mk_local(from_tc.mk_fresh_name(), "x", binding_domain(whnf_from_type), binder_info());
+            expr fx = mk_app(f, x);
+            return map(coe, [&](expr const & c) { return Fun(f, Fun(x, mk_app(c, fx))); });
+        } else {
+            return list<expr>();
+        }
+    } else {
+        expr const & fn   = get_app_fn(whnf_to_type);
+        list<expr> r;
+        if (is_constant(fn)) {
+            r = get_coercions(env, whnf_from_type, const_name(fn));
+        } else if (is_pi(whnf_to_type)) {
+            r = get_coercions_to_fun(env, whnf_from_type);
+        } else if (is_sort(whnf_to_type)) {
+            r = get_coercions_to_sort(env, whnf_from_type);
+        }
+        if (r)
+            cs += new_cs;
+        return r;
     }
-    if (r)
-        cs += new_cs;
-    return r;
 }
 
 optional<constraints> coercion_elaborator::next() {

src/frontends/lean/elaborator.cpp

@@ -481,6 +481,10 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
 bool elaborator::has_coercions_from(expr const & a_type) {
     try {
         expr a_cls = get_app_fn(m_coercion_from_tc->whnf(a_type).first);
+        while (is_pi(a_cls)) {
+            expr local = mk_local(binding_name(a_cls), binding_domain(a_cls), binding_info(a_cls));
+            a_cls      = get_app_fn(m_coercion_from_tc->whnf(instantiate(binding_body(a_cls), local)).first);
+        }
         return is_constant(a_cls) && ::lean::has_coercions_from(env(), const_name(a_cls));
     } catch (exception&) {
         return false;

tests/lean/644.lean

@@ -0,0 +1,38 @@
+import data.list
+
+constant A : Type₁
+constant B : Type₁
+constant coe : A → B
+attribute coe [coercion]
+variable f : B → B
+variable a : A
+set_option pp.coercions true
+check f a
+
+constant C : Type₁
+variable g : (C → B) → B
+variable h : C → A
+check g h
+
+definition tst (g : C → B) : Prop := g = h
+
+open bool list
+
+definition bool_to_Prop [coercion] [reducible] (b : bool) : Prop := b = tt
+
+definition bpred_dec [instance] {A : Type} (p : A → bool) : ∀ a, decidable (p a = tt) :=
+begin
+  intro a,
+  eapply (bool.rec_on (p a)),
+    right, contradiction,
+    left, reflexivity
+end
+
+definition negb : bool → bool := bool.rec tt ff
+
+check filter negb [tt, ff, tt, ff]
+
+eval filter negb [tt, ff, tt, ff]
+
+example : filter negb [tt, ff, tt, ff] = [ff, ff] :=
+rfl

tests/lean/644.lean.expected.out

@@ -0,0 +1,4 @@
+f (coe a) : B
+g (λ (x : C), coe (h x)) : B
+filter (λ (x : bool), bool_to_Prop (negb x)) [tt, ff, tt, ff] : list bool
+[ff, ff]