From 029acbd1dfd87742ad92fcf6f0f7b1853fc98dad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 12 Sep 2014 13:17:20 -0700
Subject: [PATCH] feat(library/coercion): better support for coercions to
 function-class. closes #185

---
 src/library/coercion.cpp   | 22 ++++++++++++++++++----
 tests/lean/run/coefun.lean | 13 +++++++++++++
 2 files changed, 31 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/coefun.lean

diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp
index 93f9d89e9..4ba9006b0 100644
--- a/src/library/coercion.cpp
+++ b/src/library/coercion.cpp
@@ -344,16 +344,30 @@ environment add_coercion(environment const & env, name const & f, io_state const
     declaration d = env.get(f);
     expr t = d.get_type();
     check_pi(f, t);
-    optional<name> C;
+    buffer<name> Cs; // possible Cs
     while (is_pi(t)) {
         expr d = get_app_fn(binding_domain(t));
         if (is_constant(d))
-            C = const_name(d);
+            Cs.push_back(const_name(d));
         t = binding_body(t);
     }
-    if (!C)
+    if (Cs.empty())
         throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion");
-    return add_coercion(env, f, *C, ios);
+    unsigned i = Cs.size();
+    while (i > 0) {
+        --i;
+        if (i == 0) {
+            // last alternative
+            return add_coercion(env, f, Cs[i], ios);
+        } else {
+            try {
+                return add_coercion(env, f, Cs[i], ios);
+            } catch (exception &) {
+                // failed, keep trying...
+            }
+        }
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 optional<pair<name, unsigned>> is_coercion(environment const & env, name const & f) {
diff --git a/tests/lean/run/coefun.lean b/tests/lean/run/coefun.lean
new file mode 100644
index 000000000..eca7730b7
--- /dev/null
+++ b/tests/lean/run/coefun.lean
@@ -0,0 +1,13 @@
+inductive obj (A : Type) :=
+mk : A → obj A
+
+inductive fn (A B : Type) :=
+mk : (obj A → obj B) → fn A B
+
+definition to_fun [coercion] {A B : Type} (f : fn A B) : obj A → obj B :=
+fn.rec (λf, f) f
+
+variable n : Type.{1}
+variable f : fn n n
+variable a : obj n
+check (f a)