feat(frontends/lean): allow multiple coercions from class A to B, closes #187

See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean

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

src/frontends/lean/coercion_elaborator.cpp

@@ -13,41 +13,33 @@ Author: Leonardo de Moura
 #include "frontends/lean/coercion_elaborator.h"
 
 namespace lean {
+coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr const & arg,
+                                         list<constraints> const & choices, list<expr> const & coes,
+                                         bool use_id):
+    m_info(info), m_arg(arg), m_id(use_id), m_choices(choices), m_coercions(coes) {
+    lean_assert(length(m_coercions) + 1 == length(m_choices));
+}
 
-struct coercion_elaborator : public choice_iterator {
+optional<constraints> coercion_elaborator::next() {
-    coercion_info_manager & m_info;
+    if (!m_choices)
-    expr                    m_arg;
+        return optional<constraints>();
-    bool                    m_id; // true if identity was not tried yet
+    if (m_id) {
-    list<constraints>       m_choices;
+        m_id = false;
-    list<expr>              m_coercions;
+        m_info.erase_coercion_info(m_arg);
-
+    } else if (m_coercions) {
-    coercion_elaborator(coercion_info_manager & info, expr const & arg,
+        expr c      = head(m_coercions);
-                        list<constraints> const & choices, list<expr> const & coes):
+        m_coercions = tail(m_coercions);
-        m_info(info), m_arg(arg), m_id(true), m_choices(choices), m_coercions(coes) {
+        m_info.save_coercion_info(m_arg, mk_app(c, m_arg));
-        lean_assert(length(m_coercions) + 1 == length(m_choices));
     }
-
+    auto r = head(m_choices);
-    optional<constraints> next() {
+    m_choices = tail(m_choices);
-        if (!m_choices)
+    return optional<constraints>(r);
-            return optional<constraints>();
+}
-        if (m_id) {
-            m_id = false;
-            m_info.erase_coercion_info(m_arg);
-        } else if (m_coercions) {
-            expr c      = head(m_coercions);
-            m_coercions = tail(m_coercions);
-            m_info.save_coercion_info(m_arg, mk_app(c, m_arg));
-        }
-        auto r = head(m_choices);
-        m_choices = tail(m_choices);
-        return optional<constraints>(r);
-    }
-};
 
 constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
                              expr const & m, expr const & a, expr const & a_type,
                              justification const & j, unsigned delay_factor, bool relax) {
-    auto choice_fn = [=, &tc, &infom](expr const & mvar, expr const & d_type, substitution const & s,
+    auto choice_fn = [=, &tc, &infom](expr const & meta, expr const & d_type, substitution const & s,
                                       name_generator const & /* ngen */) {
         expr          new_a_type;
         justification new_a_type_jst;
@@ -65,7 +57,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
                                                                             delay_factor+1, relax)));
             } else {
                 // giveup...
-                return lazy_list<constraints>(constraints(mk_eq_cnstr(mvar, a, justification(), relax)));
+                return lazy_list<constraints>(constraints(mk_eq_cnstr(meta, a, justification(), relax)));
             }
         }
         constraint_seq cs;
@@ -77,7 +69,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
             buffer<constraints> choices;
             buffer<expr> coes;
             // first alternative: no coercion
-            constraint_seq cs1 = cs + mk_eq_cnstr(mvar, a, justification(), relax);
+            constraint_seq cs1 = cs + mk_eq_cnstr(meta, a, justification(), relax);
             choices.push_back(cs1.to_list());
             unsigned i = alts.size();
             while (i > 0) {
@@ -86,26 +78,41 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
                 expr coe   = std::get<1>(t);
                 expr new_a = copy_tag(a, mk_app(coe, a));
                 coes.push_back(coe);
-                constraint_seq csi = cs + mk_eq_cnstr(mvar, new_a, new_a_type_jst, relax);
+                constraint_seq csi = cs + mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
                 choices.push_back(csi.to_list());
             }
-            return choose(std::make_shared<coercion_elaborator>(infom, mvar,
+            return choose(std::make_shared<coercion_elaborator>(infom, meta,
                                                                 to_list(choices.begin(), choices.end()),
                                                                 to_list(coes.begin(), coes.end())));
         } else {
-            expr new_a         = a;
             expr new_d_type    = tc.whnf(d_type, cs);
             expr const & d_cls = get_app_fn(new_d_type);
             if (is_constant(d_cls)) {
-                if (auto c = get_coercion(tc.env(), new_a_type, const_name(d_cls))) {
+                list<expr> coes = get_coercions(tc.env(), new_a_type, const_name(d_cls));
-                    new_a = copy_tag(a, mk_app(*c, a));
+                if (is_nil(coes)) {
-                    infom.save_coercion_info(a, new_a);
+                    expr new_a = a;
-                } else {
                     infom.erase_coercion_info(a);
+                    cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
+                    return lazy_list<constraints>(cs.to_list());
+                } else if (is_nil(tail(coes))) {
+                    expr new_a = copy_tag(a, mk_app(head(coes), a));
+                    infom.save_coercion_info(a, new_a);
+                    cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
+                    return lazy_list<constraints>(cs.to_list());
+                } else {
+                    list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
+                            expr new_a   = copy_tag(a, mk_app(coe, a));
+                            constraint c = mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
+                            return (cs + c).to_list();
+                        });
+                    return choose(std::make_shared<coercion_elaborator>(infom, meta, choices, coes, false));
                 }
+            } else {
+                expr new_a = a;
+                infom.erase_coercion_info(a);
+                cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
+                return lazy_list<constraints>(cs.to_list());
             }
-            cs += mk_eq_cnstr(mvar, new_a, new_a_type_jst, relax);
-            return lazy_list<constraints>(cs.to_list());
         }
     };
     return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, relax);

src/frontends/lean/coercion_elaborator.h

@@ -17,6 +17,19 @@ public:
     virtual void save_coercion_info(expr const & e, expr const & c) = 0;
 };
 
+class coercion_elaborator : public choice_iterator {
+    coercion_info_manager & m_info;
+    expr                    m_arg;
+    bool                    m_id; // true if identity was not tried yet
+    list<constraints>       m_choices;
+    list<expr>              m_coercions;
+public:
+    coercion_elaborator(coercion_info_manager & info, expr const & arg,
+                        list<constraints> const & choices, list<expr> const & coes,
+                        bool use_id = true);
+    optional<constraints> next();
+};
+
 /** \brief Create a metavariable, and attach choice constraint for generating
     coercions of the form <tt>f a</tt>, where \c f is registered coercion,
     and \c a is the input argument that has type \c a_type, but is expected
@@ -34,4 +47,8 @@ public:
 pair<expr, constraint> mk_coercion_elaborator(
     type_checker & tc, coercion_info_manager & infom, local_context & ctx, bool relax,
     expr const & a, expr const & a_type, expr const & expected_type, justification const & j);
+
+pair<expr, constraint> coercions_to_choice(coercion_info_manager & infom, local_context & ctx,
+                                           list<expr> const & coes, expr const & a,
+                                           justification const & j, bool relax);
 }

src/frontends/lean/elaborator.cpp

@@ -357,15 +357,48 @@ public:
         }
         if (!is_pi(f_type)) {
             // try coercion to function-class
-            optional<expr> c = get_coercion_to_fun(env(), f_type);
+            list<expr> coes  = get_coercions_to_fun(env(), f_type);
-            if (c) {
+            if (is_nil(coes)) {
+                throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); });
+            } else if (is_nil(tail(coes))) {
                 expr old_f = f;
-                f = mk_app(*c, f, f.get_tag());
+                f = mk_app(head(coes), f, f.get_tag());
                 f_type = infer_type(f, cs);
                 save_coercion_info(old_f, f);
                 lean_assert(is_pi(f_type));
             } else {
-                throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); });
+                bool relax = m_relax_main_opaque;
+                justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst) {
+                        return pp_function_expected(fmt, substitution(subst).instantiate(f));
+                    });
+                auto choice_fn = [=](expr const & meta, expr const &, substitution const &, name_generator const &) {
+                    list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
+                            expr new_f      = copy_tag(f, ::lean::mk_app(coe, f));
+                            constraint_seq cs;
+                            while (true) {
+                                expr new_f_type = m_tc[relax]->infer(new_f, cs);
+                                if (!is_pi(new_f_type))
+                                    break;
+                                binder_info bi = binding_info(new_f_type);
+                                if (!bi.is_strict_implicit() && !bi.is_implicit())
+                                    break;
+                                tag g          = f.get_tag();
+                                bool is_strict = false;
+                                expr imp_arg   = mk_placeholder_meta(some_expr(binding_domain(new_f_type)), g, is_strict, cs);
+                                new_f          = mk_app(new_f, imp_arg, g);
+                            }
+                            cs += mk_eq_cnstr(meta, new_f, j, relax);
+                            return cs.to_list();
+                        });
+                    return choose(std::make_shared<coercion_elaborator>(*this, f, choices, coes, false));
+                };
+                f   = m_full_context.mk_meta(none_expr(), f.get_tag());
+                cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j, relax);
+                lean_assert(is_meta(f));
+                // let type checker add constraint
+                f_type = infer_type(f, cs);
+                lean_assert(is_pi(f_type));
+                f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
             }
         } else {
             erase_coercion_info(f);
@@ -389,15 +422,30 @@ public:
         d_type = whnf(d_type).first;
         expr const & d_cls = get_app_fn(d_type);
         if (is_constant(d_cls)) {
-            if (auto c = get_coercion(env(), a_type, const_name(d_cls))) {
+            list<expr> coes = get_coercions(env(), a_type, const_name(d_cls));
-                expr r = mk_app(*c, a, a.get_tag());
+            if (is_nil(coes)) {
+                erase_coercion_info(a);
+                return a;
+            } else if (is_nil(tail(coes))) {
+                expr r = mk_app(head(coes), a, a.get_tag());
                 save_coercion_info(a, r);
                 return r;
             } else {
+                for (expr const & coe : coes) {
+                    expr r = mk_app(coe, a, a.get_tag());
+                    expr r_type = infer_type(r).first;
+                    if (m_tc[m_relax_main_opaque]->is_def_eq(r_type, d_type).first) {
+                        save_coercion_info(a, r);
+                        return r;
+                    }
+                }
                 erase_coercion_info(a);
+                return a;
             }
+        } else {
+            erase_coercion_info(a);
+            return a;
         }
-        return a;
     }
 
     /** \brief Given a term <tt>a : a_type</tt>, and an expected type generate a metavariable with a delayed coercion. */
@@ -426,8 +474,8 @@ public:
                 return to_ecs(a, dcs.second);
             } else {
                 expr new_a = apply_coercion(a, a_type, expected_type);
-                bool coercion_worked = false;
                 constraint_seq cs;
+                bool coercion_worked = false;
                 if (!is_eqp(a, new_a)) {
                     expr new_a_type = infer_type(new_a, cs);
                     coercion_worked = m_tc[relax]->is_def_eq(new_a_type, expected_type, j, cs);
@@ -575,13 +623,15 @@ public:
                 return e;
             }
         }
-        optional<expr> c = get_coercion_to_sort(env(), t);
+        list<expr> coes = get_coercions_to_sort(env(), t);
-        if (c) {
+        if (is_nil(coes)) {
-            expr r = mk_app(*c, e, e.get_tag());
+            throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); });
+        } else {
+            // Remark: we ignore other coercions to sort
+            expr r = mk_app(head(coes), e, e.get_tag());
             save_coercion_info(e, r);
             return r;
         }
-        throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); });
     }
 
     /** \brief Similar to instantiate_rev, but assumes that subst contains only local constants.

src/frontends/lean/info_manager.cpp

@@ -212,6 +212,12 @@ public:
         ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl;
         ios << "-- ACK" << endl;
     }
+
+    virtual info_data_cell * instantiate(substitution & s) const {
+        expr e = s.instantiate(m_expr);
+        expr t = s.instantiate(m_type);
+        return is_eqp(e, m_expr) && is_eqp(t, m_type) ? nullptr : new coercion_info_data(get_column(), e, t);
+    }
 };
 
 class symbol_info_data : public info_data_cell {

src/library/coercion.cpp

@@ -71,31 +71,39 @@ struct coercion_info {
 struct coercion_state {
     rb_map<name, list<coercion_info>, name_quick_cmp>                    m_coercion_info;
     // m_from and m_to contain "direct" coercions
-    rb_map<name, list<pair<coercion_class, expr>>, name_quick_cmp>       m_from; // map user-class -> list of (class, coercion-fun)
+    typedef std::tuple<coercion_class, expr, expr> from_data;
+    rb_map<name, list<from_data>, name_quick_cmp>                        m_from; // map user-class -> list of (class, coercion-fun)
     rb_map<coercion_class, list<name>, coercion_class_cmp_fn>            m_to;
     rb_map<name, pair<name, unsigned>, name_quick_cmp>                   m_coercions; // map coercion -> (from-class, num-args)
-    coercion_info get_info(name const & from, coercion_class const & to) {
+
+    template<typename F>
+    void for_each_info(name const & from, coercion_class const & to, F && f) {
         auto it = m_coercion_info.find(from);
         lean_assert(it);
         for (coercion_info info : *it) {
-            if (info.m_to == to)
+            if (info.m_to == to) {
-                return info;
+                f(info);
+            }
         }
-        lean_unreachable(); // LCOV_EXCL_LINE
     }
-    void update_from_to(name const & C, coercion_class const & D, expr const & f, io_state const & ios) {
+
+    void update_from_to(type_checker & tc, name const & C, coercion_class const & D,
+                        expr const & f, expr const & f_type, io_state const & ios) {
         auto it1 = m_from.find(C);
         if (!it1) {
-            m_from.insert(C, to_list(mk_pair(D, f)));
+            m_from.insert(C, to_list(from_data(D, f, f_type)));
         } else {
+            coercion_class D_it; expr f_it, f_type_it;
             auto it  = it1->begin();
             auto end = it1->end();
-            for (; it != end; ++it)
+            for (; it != end; ++it) {
-                if (it->first == D)
+                std::tie(D_it, f_it, f_type_it) = *it;
+                if (D_it == D && tc.is_def_eq(f_type_it, f_type).first)
                     break;
+            }
             if (it == end)
-                m_from.insert(C, cons(mk_pair(D, f), *it1));
+                m_from.insert(C, cons(from_data(D, f, f_type), *it1));
-            else if (it->second != f)
+            else if (std::get<1>(*it) != f)
                 ios.get_diagnostic_channel() << "replacing the coercion from '" << C << "' to '" << D << "'\n";
         }
         auto it2 = m_to.find(D);
@@ -158,18 +166,26 @@ optional<coercion_class> type_to_coercion_class(expr const & t) {
     }
 }
 
-typedef list<pair<name, coercion_class>> arrows;
+typedef std::tuple<name, coercion_class, expr> arrow;
-static bool contains(arrows const & a, name const & C, coercion_class const & D) {
+typedef list<arrow> arrows;
-    return std::find(a.begin(), a.end(), mk_pair(C, D)) != a.end();
+static bool contains(type_checker & tc, arrows const & as, name const & C, coercion_class const & D, expr const & f_type) {
+    name C_it; coercion_class D_it; expr f_type_it;
+    for (arrow const & a : as) {
+        std::tie(C_it, D_it, f_type_it) = a;
+        if (C == C_it && D == D_it && tc.is_def_eq(f_type_it, f_type).first)
+            return true;
+    }
+    return false;
 }
-static arrows insert(arrows const & a, name const & C, coercion_class const & D) {
+static arrows insert(arrows const & a, name const & C, coercion_class const & D, expr const & f_type) {
-    return arrows(mk_pair(C, D), a);
+    return arrows(arrow(C, D, f_type), a);
 }
 
 struct add_coercion_fn {
-    coercion_state   m_state;
+    type_checker        m_tc;
-    arrows           m_visited;
+    coercion_state      m_state;
-    io_state const & m_ios;
+    arrows              m_visited;
+    io_state const &    m_ios;
 
     void add_coercion_trans(name const & C,
                             level_param_names const & f_level_params, expr const & f, expr const & f_type, unsigned f_num_args,
@@ -220,10 +236,11 @@ struct add_coercion_fn {
         if (!it1)
             return;
         for (name const & B : *it1) {
-            coercion_info info = m_state.get_info(B, C_cls);
+            m_state.for_each_info(B, C_cls, [&](coercion_info const & info) {
-            // B >-> C >-> D
+                    // B >-> C >-> D
-            add_coercion_trans(B, info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args,
+                    add_coercion_trans(B, info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args,
-                               ls, f, f_type, num_args, cls);
+                                       ls, f, f_type, num_args, cls);
+                });
         }
     }
 
@@ -237,11 +254,12 @@ struct add_coercion_fn {
         if (!it)
             return;
         for (auto const & p : *it) {
-            coercion_class E   = p.first;
+            coercion_class E   = std::get<0>(p);
-            coercion_info info = m_state.get_info(D, E);
+            m_state.for_each_info(D, E, [&](coercion_info const & info) {
-            // C >-> D >-> E
+                    // C >-> D >-> E
-            add_coercion_trans(C, ls, f, f_type, num_args,
+                    add_coercion_trans(C, ls, f, f_type, num_args,
-                               info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, info.m_to);
+                                       info.m_level_params, info.m_fun, info.m_fun_type, info.m_num_args, info.m_to);
+                });
         }
     }
 
@@ -253,7 +271,9 @@ struct add_coercion_fn {
             m_state.m_coercion_info.insert(C, infos);
         } else {
             list<coercion_info> infos = *it;
-            infos = filter(infos, [&](coercion_info const & info) { return info.m_to != cls; });
+            infos = filter(infos, [&](coercion_info const & info) {
+                    return info.m_to != cls || !m_tc.is_def_eq(info.m_fun_type, f_type).first;
+                });
             infos = cons(coercion_info(f, f_type, ls, num_args, cls), infos);
             m_state.m_coercion_info.insert(C, infos);
         }
@@ -263,23 +283,23 @@ struct add_coercion_fn {
 
     void add_coercion(name const & C, expr const & f, expr const & f_type,
                       level_param_names const & ls, unsigned num_args, coercion_class const & cls) {
-        if (contains(m_visited, C, cls))
+        if (contains(m_tc, m_visited, C, cls, f_type))
             return;
         if (cls.kind() == coercion_class_kind::User && cls.get_name() == C)
             return;
-        m_visited = insert(m_visited, C, cls);
+        m_visited = insert(m_visited, C, cls, f_type);
         add_coercion_core(C, f, f_type, ls, num_args, cls);
         add_coercion_trans_to(C, f, f_type, ls, num_args, cls);
         add_coercion_trans_from(C, f, f_type, ls, num_args, cls);
     }
 
-    add_coercion_fn(coercion_state const & s, io_state const & ios):
+    add_coercion_fn(environment const & env, coercion_state const & s, io_state const & ios):
-        m_state(s), m_ios(ios) {}
+        m_tc(env), m_state(s), m_ios(ios) {}
 
     coercion_state operator()(name const & C, expr const & f, expr const & f_type,
                               level_param_names const & ls, unsigned num_args, coercion_class const & cls) {
         add_coercion(C, f, f_type, ls, num_args, cls);
-        m_state.update_from_to(C, cls, f, m_ios);
+        m_state.update_from_to(m_tc, C, cls, f, f_type, m_ios);
         return m_state;
     }
 };
@@ -305,7 +325,7 @@ coercion_state add_coercion(environment const & env, io_state const & ios, coerc
                 throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" << C << "'");
             else if (cls->kind() == coercion_class_kind::User && cls->get_name() == C)
                 throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself");
-            return add_coercion_fn(st, ios)(C, fn, d.get_type(), d.get_univ_params(), num, *cls);
+            return add_coercion_fn(env, st, ios)(C, fn, d.get_type(), d.get_univ_params(), num, *cls);
         }
         t = binding_body(t);
         num++;
@@ -414,34 +434,35 @@ bool has_coercions_from(environment const & env, expr const & C) {
         length(head(cs).m_level_params) == length(const_levels(C_fn));
 }
 
-optional<expr> get_coercion(environment const & env, expr const & C, coercion_class const & D) {
+list<expr> get_coercions(environment const & env, expr const & C, coercion_class const & D) {
     buffer<expr> args;
     expr const & C_fn = get_app_rev_args(C, args);
     if (!is_constant(C_fn))
-        return none_expr();
+        return list<expr>();
     coercion_state const & ext = coercion_ext::get_state(env);
     auto it = ext.m_coercion_info.find(const_name(C_fn));
     if (!it)
-        return none_expr();
+        return list<expr>();
+    buffer<expr> r;
     for (coercion_info const & info : *it) {
         if (info.m_to == D && info.m_num_args == args.size() && length(info.m_level_params) == length(const_levels(C_fn))) {
             expr f = instantiate_univ_params(info.m_fun, info.m_level_params, const_levels(C_fn));
-            return some_expr(apply_beta(f, args.size(), args.data()));
+            r.push_back(apply_beta(f, args.size(), args.data()));
         }
     }
-    return none_expr();
+    return to_list(r.begin(), r.end());
 }
 
-optional<expr> get_coercion(environment const & env, expr const & C, name const & D) {
+list<expr> get_coercions(environment const & env, expr const & C, name const & D) {
-    return get_coercion(env, C, coercion_class::mk_user(D));
+    return get_coercions(env, C, coercion_class::mk_user(D));
 }
 
-optional<expr> get_coercion_to_sort(environment const & env, expr const & C) {
+list<expr> get_coercions_to_sort(environment const & env, expr const & C) {
-    return get_coercion(env, C, coercion_class::mk_sort());
+    return get_coercions(env, C, coercion_class::mk_sort());
 }
 
-optional<expr> get_coercion_to_fun(environment const & env, expr const & C) {
+list<expr> get_coercions_to_fun(environment const & env, expr const & C) {
-    return get_coercion(env, C, coercion_class::mk_fun());
+    return get_coercions(env, C, coercion_class::mk_fun());
 }
 
 bool get_user_coercions(environment const & env, expr const & C, buffer<std::tuple<name, expr, expr>> & result) {
@@ -535,16 +556,16 @@ static int has_coercions_from(lua_State * L) {
         return push_boolean(L, has_coercions_from(to_environment(L, 1), to_name_ext(L, 2)));
 }
 
-static int get_coercion(lua_State * L) {
+static int get_coercions(lua_State * L) {
-    return push_optional_expr(L, get_coercion(to_environment(L, 1), to_expr(L, 2), to_name_ext(L, 3)));
+    return push_list_expr(L, get_coercions(to_environment(L, 1), to_expr(L, 2), to_name_ext(L, 3)));
 }
 
-static int get_coercion_to_sort(lua_State * L) {
+static int get_coercions_to_sort(lua_State * L) {
-    return push_optional_expr(L, get_coercion_to_sort(to_environment(L, 1), to_expr(L, 2)));
+    return push_list_expr(L, get_coercions_to_sort(to_environment(L, 1), to_expr(L, 2)));
 }
 
-static int get_coercion_to_fun(lua_State * L) {
+static int get_coercions_to_fun(lua_State * L) {
-    return push_optional_expr(L, get_coercion_to_fun(to_environment(L, 1), to_expr(L, 2)));
+    return push_list_expr(L, get_coercions_to_fun(to_environment(L, 1), to_expr(L, 2)));
 }
 
 static int get_user_coercions(lua_State * L) {
@@ -595,9 +616,9 @@ void open_coercion(lua_State * L) {
     SET_GLOBAL_FUN(add_coercion,           "add_coercion");
     SET_GLOBAL_FUN(is_coercion,            "is_coercion");
     SET_GLOBAL_FUN(has_coercions_from,     "has_coercions_from");
-    SET_GLOBAL_FUN(get_coercion,           "get_coercion");
+    SET_GLOBAL_FUN(get_coercions,           "get_coercions");
-    SET_GLOBAL_FUN(get_coercion_to_sort,   "get_coercion_to_sort");
+    SET_GLOBAL_FUN(get_coercions_to_sort,   "get_coercions_to_sort");
-    SET_GLOBAL_FUN(get_coercion_to_fun,    "get_coercion_to_fun");
+    SET_GLOBAL_FUN(get_coercions_to_fun,    "get_coercions_to_fun");
     SET_GLOBAL_FUN(get_user_coercions,     "get_user_coercions");
     SET_GLOBAL_FUN(for_each_coercion_user, "for_each_coercion_user");
     SET_GLOBAL_FUN(for_each_coercion_sort, "for_each_coercion_sort");

src/library/coercion.h

@@ -53,9 +53,9 @@ bool has_coercions_to(environment const & env, name const & D);
    The coercion is a unary function that takes a term of type (C_name.{l1 lk} t_1 ... t_n) and returns
    and element of type (D.{L_1  L_o} s_1 ... s_m)
 */
-optional<expr> get_coercion(environment const & env, expr const & C, name const & D);
+list<expr> get_coercions(environment const & env, expr const & C, name const & D);
-optional<expr> get_coercion_to_sort(environment const & env, expr const & C);
+list<expr> get_coercions_to_sort(environment const & env, expr const & C);
-optional<expr> get_coercion_to_fun(environment const & env, expr const & C);
+list<expr> get_coercions_to_fun(environment const & env, expr const & C);
 /**
    \brief Return all user coercions C >-> D for the type C of the form (C_name.{l1 ... lk} t_1 ... t_n)
    The result is a pair (user-class D, coercion, coercion type), and is stored in the result buffer \c result.

tests/lean/run/coe10.lean

@@ -0,0 +1,17 @@
+import data.nat
+open nat
+
+inductive fn2 (A B C : Type) :=
+mk : (A → C) → (B → C) → fn2 A B C
+
+definition to_ac [coercion] {A B C : Type} (f : fn2 A B C) : A → C :=
+fn2.rec (λ f g, f) f
+
+definition to_bc [coercion] {A B C : Type} (f : fn2 A B C) : B → C :=
+fn2.rec (λ f g, g) f
+
+variable f : fn2 Prop nat nat
+variable a : Prop
+variable n : nat
+check f a
+check f n

tests/lean/run/coe11.lean

@@ -0,0 +1,25 @@
+import data.category
+open category
+
+inductive my_functor {obC obD : Type} (C : category obC) (D : category obD) : Type :=
+mk : Π (obF : obC → obD) (morF : Π{A B : obC}, mor A B → mor (obF A) (obF B)),
+    (Π {A : obC}, morF (ID A) = ID (obF A)) →
+    (Π {A B C : obC} {f : mor A B} {g : mor B C}, morF (g ∘ f) = morF g ∘ morF f) →
+     my_functor C D
+
+definition my_object [coercion] {obC obD : Type} {C : category obC} {D : category obD} (F : my_functor C D) : obC → obD :=
+my_functor.rec (λ obF morF Hid Hcomp, obF) F
+
+definition my_morphism [coercion] {obC obD : Type} {C : category obC} {D : category obD} (F : my_functor C D) :
+      Π{A B : obC}, mor A B → mor (my_object F A) (my_object F B) :=
+my_functor.rec (λ obF morF Hid Hcomp, morF) F
+
+variables obC obD : Type
+variables a b : obC
+variable C : category obC
+instance C
+variable D : category obD
+variable F : my_functor C D
+variable m : mor a b
+check F a
+check F m

tests/lean/run/coe9.lean

@@ -0,0 +1,27 @@
+import data.nat
+open nat
+
+variable list.{l} : Type.{l} → Type.{l}
+variable vector.{l} : Type.{l} → nat → Type.{l}
+variable matrix.{l} : Type.{l} → nat → nat → Type.{l}
+variable length : Pi {A : Type}, list A → nat
+
+variable list_to_vec {A : Type} (l : list A) : vector A (length l)
+variable to_row {A : Type} {n : nat} : vector A n → matrix A 1 n
+variable to_col {A : Type} {n : nat} : vector A n → matrix A n 1
+variable to_list {A : Type} {n : nat} : vector A n → list A
+
+coercion to_row
+coercion to_col
+coercion list_to_vec
+coercion to_list
+
+variable f {A : Type} {n : nat} (M : matrix A n 1) : nat
+variable g {A : Type} {n : nat} (M : matrix A 1 n) : nat
+variable v : vector nat 10
+variable l : list nat
+
+check f v
+check g v
+check f l
+check g l

tests/lua/coe1.lua

@@ -32,33 +32,41 @@ env = add_coercion(env, "lst2vec")
 assert(is_coercion(env, Const("lst2vec", {l})))
 assert(has_coercions_from(env, "lst"))
 local lst_nat = lst_1(nat)
-print(get_coercion(env, lst_nat, "vec"))
+
+function display_coercions(coes)
+   if not coes:is_nil() then
+      print(coes:head())
+      display_coercions(coes:tail())
+   end
+end
+
+display_coercions(get_coercions(env, lst_nat, "vec"))
 env = add_coercion(env, "vec2mat")
-print(get_coercion(env, lst_nat, "mat"))
+display_coercions(get_coercions(env, lst_nat, "mat"))
-assert(env:type_check(get_coercion(env, lst_nat, "mat")))
+assert(env:type_check(get_coercions(env, lst_nat, "mat"):head()))
 for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
 env = add_coercion(env, "nat2lst")
 print("---------")
 for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
-print(get_coercion(env, nat, "mat"))
+print(get_coercions(env, nat, "mat"):head())
-assert(env:type_check(get_coercion(env, nat, "mat")))
+assert(env:type_check(get_coercions(env, nat, "mat"):head()))
 env = add_coercion(env, "mat2dlst")
 print("---------")
 for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
-print(get_coercion(env, lst_nat, "dlst"))
+print(get_coercions(env, lst_nat, "dlst"):head())
-assert(env:type_check(get_coercion(env, lst_nat, "dlst")))
+assert(env:type_check(get_coercions(env, lst_nat, "dlst"):head()))
 
 env:export("coe1_mod.olean")
 local env2 = import_modules("coe1_mod")
-print(get_coercion(env2, lst_nat, "dlst"))
+print(get_coercions(env2, lst_nat, "dlst"):head())
-assert(env2:type_check(get_coercion(env2, lst_nat, "dlst")))
+assert(env2:type_check(get_coercions(env2, lst_nat, "dlst"):head()))
 assert(is_coercion(env2, "vec2mat"))
 assert(is_coercion(env2, "lst2vec"))
 env2 = add_decl(env2, mk_var_decl("lst2vec2", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
 print("======")
 env2 = add_coercion(env2, "lst2vec2")
 print("======")
-print(get_coercion(env2, lst_nat, "dlst"))
+print(get_coercions(env2, lst_nat, "dlst"):head())
 print("---------")
 for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
 env2 = add_coercion(env2, "vec2lst")

tests/lua/coe2.lua

@@ -13,9 +13,9 @@ env = add_decl(env, mk_var_decl("real", Type))
 local nat    = Const("nat")
 local real   = Const("real")
 env = add_decl(env, mk_var_decl("f1", Const("functor", {1, 1})(nat, real)))
-print(get_coercion_to_fun(env, Const("functor", {1, 1})(nat, real)))
+print(get_coercions_to_fun(env, Const("functor", {1, 1})(nat, real)):head())
 env = add_decl(env, mk_var_decl("sfunctor", {l1}, mk_arrow(mk_sort(l1), mk_sort(l1))))
 env = add_decl(env, mk_var_decl("sf2f", {l1}, Pi(A, mk_arrow(Const("sfunctor", {l1})(A), Const("functor", {l1, l1})(A, A)))))
 env = add_coercion(env, "sf2f")
-print(get_coercion_to_fun(env, Const("sfunctor", {1})(nat)))
+print(get_coercions_to_fun(env, Const("sfunctor", {1})(nat)):head())
-assert(env:type_check(get_coercion_to_fun(env, Const("sfunctor", {1})(nat))))
+assert(env:type_check(get_coercions_to_fun(env, Const("sfunctor", {1})(nat)):head()))

tests/lua/coe3.lua

@@ -9,5 +9,5 @@ env = add_coercion(env, "carrier")
 env = add_decl(env, mk_var_decl("abg2g", {l}, mk_arrow(ab_group, group)))
 env = add_coercion(env, "abg2g")
 for_each_coercion_sort(env, function(C, f) print(tostring(C) .. " >-> sort : " .. tostring(f)) end)
-print(get_coercion_to_sort(env, Const("abelian_group", {1})))
+print(get_coercions_to_sort(env, Const("abelian_group", {1})):head())
-assert(env:type_check(get_coercion_to_sort(env, Const("abelian_group", {1}))))
+assert(env:type_check(get_coercions_to_sort(env, Const("abelian_group", {1})):head()))

tests/lua/coe5.lua

@@ -22,8 +22,8 @@ env = add_coercion(env, "ar2ag")
 for_each_coercion_sort(env, function(C, f) print(tostring(C) .. " >-> sort : " .. tostring(f)) end)
 for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
 
-print(get_coercion_to_sort(env, Const("abelian_ring", {1})))
+print(get_coercions_to_sort(env, Const("abelian_ring", {1})):head())
-assert(env:type_check(get_coercion_to_sort(env, Const("abelian_ring", {1}))))
+assert(env:type_check(get_coercions_to_sort(env, Const("abelian_ring", {1})):head()))
 print("Coercions (abelian ring): ")
 cs = get_user_coercions(env, ab_ring)
 for i = 1, #cs do

tests/lua/scope.lua

@@ -31,10 +31,10 @@ env = add_decl(env, mk_var_decl("nat2lst", mk_arrow(nat, lst_1(nat))))
 env = add_coercion(env, "lst2vec")
 env = push_scope(env, "tst")
 local lst_nat = lst_1(nat)
-print(get_coercion(env, lst_nat, "vec"))
+print(get_coercions(env, lst_nat, "vec"):head())
 env = add_coercion(env, "vec2mat")
-print(get_coercion(env, lst_nat, "mat"))
+print(get_coercions(env, lst_nat, "mat"):head())
-assert(env:type_check(get_coercion(env, lst_nat, "mat")))
+assert(env:type_check(get_coercions(env, lst_nat, "mat"):head()))
 function get_num_coercions(env)
    local r = 0
    for_each_coercion_user(env, function(C, D, f) r = r + 1 end)