From c7e68e57cf64a75dffa2bfa1ba8361cbf064cfb4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Jun 2017 16:22:38 -0700
Subject: [PATCH] fix(frontends/lean/structure_cmd): fixes #1681

@kha I'm not sure if this is the right fix. I just avoided the loop that adds
`mk_expr_placeholder` if the function is not a projection.
I didn't spend time investigating why we need `mk_proj_app`.
I know the library doesn't compile if we don't use it, and just use
```
    return mk_app(copy_tag(ref, mk_constant(S_name + fname)), e);
```
:)
---
 src/frontends/lean/structure_cmd.cpp | 16 +++++++++-------
 tests/lean/run/1681.lean             | 19 +++++++++++++++++++
 2 files changed, 28 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/1681.lean

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 7e5d911235..1cdf80ec35 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -179,14 +179,16 @@ void get_structure_fields_flattened(environment const & env, name const & struct
 
 expr mk_proj_app(environment const & env, name const & S_name, name const & fname, expr const & e, expr const & ref) {
     if (is_structure_like(env, S_name)) {
-        auto nparams = std::get<1>(get_structure_info(env, S_name));
-        auto proj = mk_explicit(copy_tag(ref, mk_constant(S_name + fname)));
-        for (unsigned i = 0; i < nparams; i++)
-            proj = mk_app(proj, mk_expr_placeholder());
-        return mk_app(proj, e);
-    } else {
-        return mk_app(copy_tag(ref, mk_constant(S_name + fname)), e);
+        name proj_name = S_name + fname;
+        if (get_projection_info(env, proj_name)) {
+            auto proj    = mk_explicit(copy_tag(ref, mk_constant(proj_name)));
+            auto nparams = std::get<1>(get_structure_info(env, S_name));
+            for (unsigned i = 0; i < nparams; i++)
+                proj = mk_app(proj, mk_expr_placeholder());
+            return mk_app(proj, e);
+        }
     }
+    return mk_app(copy_tag(ref, mk_constant(S_name + fname)), e);
 }
 
 optional<expr> mk_base_projections(environment const & env, name const & S_name, name const & base_S_name, expr const & e) {
diff --git a/tests/lean/run/1681.lean b/tests/lean/run/1681.lean
new file mode 100644
index 0000000000..70db944cf0
--- /dev/null
+++ b/tests/lean/run/1681.lean
@@ -0,0 +1,19 @@
+def prod.foo (s : bool × bool) (fst : bool) : bool × bool :=
+match s with
+(a, b) := (fst, b)
+end
+
+variable s : bool × bool
+
+#check prod.foo s
+#check prod.foo s tt
+#check s.foo
+#check s.foo tt
+
+def prod.foo2 {α β} (s : α × β) (fst : α) : α × β :=
+match s with
+(a, b) := (fst, b)
+end
+
+#check s.foo2
+#check s.foo2 tt