From 9675b7c9520eaee5ce4f0f626ba40514978ec44a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Feb 2019 17:29:38 -0800
Subject: [PATCH] fix(frontends/lean/elaborator): ignore mdata when processing
 field notation

---
 src/frontends/lean/elaborator.cpp | 2 +-
 src/library/util.cpp              | 8 ++++++++
 src/library/util.h                | 2 ++
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 51b871605e..689f5c295e 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1903,7 +1903,7 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
         unsigned i       = 0;
         while (is_pi(proj_type)) {
             if (is_explicit(binding_info(proj_type))) {
-                if (is_app_of(binding_domain(proj_type), field_res.m_base_S_name)) {
+                if (is_app_of(extract_mdata(binding_domain(proj_type)), field_res.m_base_S_name)) {
                     /* found s location */
                     expr coerced_s = *mk_base_projections(m_env, field_res.m_S_name, field_res.m_base_S_name, mk_as_is(s));
                     new_args.push_back(copy_pos(fn, std::move(coerced_s)));
diff --git a/src/library/util.cpp b/src/library/util.cpp
index b7a9285d78..c69808ec0a 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -1030,6 +1030,14 @@ expr mk_tactic_unit() {
 static std::string * g_version_string = nullptr;
 std::string const & get_version_string() { return *g_version_string; }
 
+expr const & extract_mdata(expr const & e) {
+    if (is_mdata(e)) {
+        return extract_mdata(mdata_expr(e));
+    } else {
+        return e;
+    }
+}
+
 void initialize_library_util() {
     g_unit           = new expr(mk_constant(get_unit_name()));
     g_unit_mk        = new expr(mk_constant(get_unit_star_name()));
diff --git a/src/library/util.h b/src/library/util.h
index f2d77151b4..3058d44363 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -315,6 +315,8 @@ expr mk_tactic_unit();
 
 std::string const & get_version_string();
 
+expr const & extract_mdata(expr const &);
+
 void initialize_library_util();
 void finalize_library_util();
 }