From f60de96d98711896274abfa8dc55771eaad0e7b4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Sep 2016 17:03:59 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): bug at `@@` annotation

---
 src/frontends/lean/elaborator.cpp |  8 ++++----
 src/frontends/lean/elaborator.h   |  4 ++--
 tests/lean/run/at_at_bug.lean     | 14 ++++++++++++++
 3 files changed, 20 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/at_at_bug.lean

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 1b944afd9c..1666be0e28 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1000,7 +1000,7 @@ expr elaborator::visit_default_app_core(expr const & _fn, arg_mask amask, buffer
             if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size())
                 break;
             if ((amask == arg_mask::Default && !is_explicit(bi)) ||
-                (amask == arg_mask::Simple && !bi.is_inst_implicit() && !is_first_order(d))) {
+                (amask == arg_mask::InstHoExplicit && !is_explicit(bi) && !bi.is_inst_implicit() && !is_pi(d))) {
                 // implicit argument
                 if (bi.is_inst_implicit())
                     new_arg = mk_instance(d, ref);
@@ -1191,7 +1191,7 @@ expr elaborator::visit_no_confusion(expr const & fn, buffer<expr> const & args,
     new_args.push_back(copy_tag(args[0], mk_as_is(Heq)));
     for (unsigned i = 1; i < args.size(); i++)
         new_args.push_back(args[i]);
-    return visit_default_app_core(fn, arg_mask::All, new_args, false, expected_type, ref);
+    return visit_default_app_core(fn, arg_mask::AllExplicit, new_args, false, expected_type, ref);
 }
 
 expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<expr> const & expected_type,
@@ -1199,10 +1199,10 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
     arg_mask amask = arg_mask::Default;
     if (is_explicit(fn)) {
         fn   = get_explicit_arg(fn);
-        amask = arg_mask::All;
+        amask = arg_mask::AllExplicit;
     } else if (is_partial_explicit(fn)) {
         fn   = get_partial_explicit_arg(fn);
-        amask = arg_mask::Simple;
+        amask = arg_mask::InstHoExplicit;
     }
 
     bool has_args = !args.empty();
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 0ef848bc90..a12336b7d8 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -25,8 +25,8 @@ public:
 private:
     typedef std::vector<pair<expr, expr>> to_check_sorts;
     enum class arg_mask {
-        All /* @ annotation */,
-        Simple /* @@ annotation */,
+        AllExplicit /* @ annotation */,
+        InstHoExplicit, /* @@ annotation (i.e., instance implicit and higher-order arguments are explicit  */
         Default /* default behavior */
     };
     environment       m_env;
diff --git a/tests/lean/run/at_at_bug.lean b/tests/lean/run/at_at_bug.lean
new file mode 100644
index 0000000000..9fbca2852c
--- /dev/null
+++ b/tests/lean/run/at_at_bug.lean
@@ -0,0 +1,14 @@
+set_option new_elaborator true
+
+example (a b : nat) (p : nat → nat → Prop) (h₁ : p a b) (h₂ : a = b) : p b b :=
+@@eq.subst (λ x, p x b) h₂ h₁
+
+set_option pp.all true
+
+variable my_has_add : has_add nat
+check @@add my_has_add 0 1
+
+local notation h1 `▸[` m `]` h2 := @@eq.subst m h1 h2
+
+example (a b : nat) (p : nat → nat → Prop) (h₁ : p a b) (h₂ : a = b) : p b b :=
+h₂ ▸[λ x, p x b] h₁