From bed0d6df6b9486069f99cd798735aee0b531fde9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Mar 2015 23:04:45 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): inaccessible over coercion

---
 library/data/vector.lean          |  2 +-
 src/frontends/lean/elaborator.cpp | 17 ++++++++++++-----
 tests/lean/run/deceq_vec.lean     |  8 ++++++++
 3 files changed, 21 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/deceq_vec.lean

diff --git a/library/data/vector.lean b/library/data/vector.lean
index c3b6d2dc4..a0e9ab7d1 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -259,7 +259,7 @@ namespace vector
    /- decidable equality -/
   open decidable
   definition decidable_eq [H : decidable_eq A] : ∀ {n : nat} (v₁ v₂ : vector A n), decidable (v₁ = v₂)
-  | ⌞zero⌟ []      []      := inl rfl
+  | ⌞0⌟    []      []      := inl rfl
   | ⌞n+1⌟  (a::v₁) (b::v₂) :=
     match H a b with
     | inl Hab  :=
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 766d6002e..447b6ae31 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -365,6 +365,13 @@ expr elaborator::add_implict_args(expr e, constraint_seq & cs, bool relax) {
     }
 }
 
+static expr mk_coercion_app(expr const & coe, expr const & a) {
+    if (is_inaccessible(a))
+        return copy_tag(a, mk_inaccessible(mk_app(coe, get_annotation_arg(a), a.get_tag())));
+    else
+        return mk_app(coe, a, a.get_tag());
+}
+
 /** \brief Make sure \c f is really a function, if it is not, try to apply coercions.
     The result is a pair <tt>new_f, f_type</tt>, where new_f is the new value for \c f,
     and \c f_type is its type (and a Pi-expression)
@@ -392,7 +399,7 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
         } else if (is_nil(tail(coes))) {
             expr old_f = f;
             bool relax = m_relax_main_opaque;
-            f = mk_app(head(coes), f, f.get_tag());
+            f = mk_coercion_app(head(coes), f);
             f = add_implict_args(f, cs, relax);
             f_type = infer_type(f, cs);
             save_coercion_info(old_f, f);
@@ -408,7 +415,7 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
                 flet<local_context> save1(m_context,      ctx);
                 flet<local_context> save2(m_full_context, full_ctx);
                 list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
-                        expr new_f      = copy_tag(f, ::lean::mk_app(coe, f));
+                        expr new_f      = mk_coercion_app(coe, f);
                         constraint_seq cs;
                         new_f = add_implict_args(new_f, cs, relax);
                         cs += mk_eq_cnstr(meta, new_f, j, relax);
@@ -467,12 +474,12 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) {
         erase_coercion_info(a);
         return a;
     } else if (is_nil(tail(coes))) {
-        expr r = mk_app(head(coes), a, a.get_tag());
+        expr r = mk_coercion_app(head(coes), a);
         save_coercion_info(a, r);
         return r;
     } else {
         for (expr const & coe : coes) {
-            expr r = mk_app(coe, a, a.get_tag());
+            expr r = mk_coercion_app(coe, a);
             expr r_type = infer_type(r).first;
             try {
                 if (m_tc[m_relax_main_opaque]->is_def_eq(r_type, d_type).first) {
@@ -708,7 +715,7 @@ expr elaborator::ensure_type(expr const & e, constraint_seq & cs) {
         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());
+        expr r = mk_coercion_app(head(coes), e);
         save_coercion_info(e, r);
         return r;
     }
diff --git a/tests/lean/run/deceq_vec.lean b/tests/lean/run/deceq_vec.lean
new file mode 100644
index 000000000..4f7f9555a
--- /dev/null
+++ b/tests/lean/run/deceq_vec.lean
@@ -0,0 +1,8 @@
+import data.vector
+open vector nat decidable
+
+variable A : Type
+
+definition foo [H : decidable_eq A] : ∀ {n : nat} (v₁ v₂ : vector A n), decidable (v₁ = v₂)
+| ⌞0⌟    []      []      := sorry
+| ⌞n+1⌟  (a::v₁) (b::v₂) := sorry