From 33e562a7ce44247bb9197ec618eae11801e8951b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Feb 2015 22:43:28 -0800
Subject: [PATCH] fix(frontends/lean/structure_cmd): effect of "include"
 command in the structure command

closes #438
---
 src/frontends/lean/structure_cmd.cpp | 21 ++++++++++++++-------
 tests/lean/438.lean                  | 12 ++++++++++++
 tests/lean/438.lean.expected.out     | 15 +++++++++++++++
 tests/lean/run/structure_test.lean   |  1 +
 4 files changed, 42 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/438.lean
 create mode 100644 tests/lean/438.lean.expected.out

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 6494c78bd..39348d034 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -298,19 +298,27 @@ struct structure_cmd_fn {
         tmp_locals.append(m_params);
         for (expr const & parent : m_parents)
             tmp_locals.push_back(mk_local(m_ngen.next(), parent));
-        expr tmp       = Pi_as_is(include_vars, Pi(tmp_locals, m_type, m_p), m_p);
-        list<expr> ctx = m_p.locals_to_context();
+
+        expr_struct_set dep_set;
+        for (expr const & v : include_vars) {
+            ::lean::collect_locals(mlocal_type(v), dep_set);
+            dep_set.insert(v);
+        }
+        buffer<expr> all_include_vars;
+        sort_locals(dep_set, m_p, all_include_vars);
+
+        expr tmp       = Pi_as_is(all_include_vars, Pi(tmp_locals, m_type, m_p), m_p);
         level_param_names new_ls;
         expr new_tmp;
-        std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, ctx);
+        std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, list<expr>());
         levels new_meta_ls = map2<level>(new_ls, [](name const & n) { return mk_meta_univ(n); });
         new_tmp = instantiate_univ_params(new_tmp, new_ls, new_meta_ls);
-        new_tmp = update_locals(new_tmp, include_vars);
+        new_tmp = update_locals(new_tmp, all_include_vars);
         new_tmp = update_locals(new_tmp, m_params);
         buffer<expr> explicit_params;
         explicit_params.append(m_params);
         m_params.clear();
-        m_params.append(include_vars);
+        m_params.append(all_include_vars);
         m_params.append(explicit_params);
         new_tmp = update_parents(new_tmp);
         m_type = new_tmp;
@@ -518,7 +526,6 @@ struct structure_cmd_fn {
 
     /** \brief Elaborate new fields, and copy them to m_fields */
     void elaborate_new_fields(buffer<expr> & new_fields) {
-        list<expr> ctx = m_p.locals_to_context();
         expr dummy = mk_Prop();
         unsigned j = m_parents.size();
         while (j > 0) {
@@ -528,7 +535,7 @@ struct structure_cmd_fn {
         expr tmp = Pi_as_is(m_params, Pi_as_is(m_fields, Pi(new_fields, dummy, m_p), m_p), m_p);
         level_param_names new_ls;
         expr new_tmp;
-        std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, ctx);
+        std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, list<expr>());
         for (auto new_l : new_ls)
             m_level_names.push_back(new_l);
         new_tmp = update_locals(new_tmp, m_params);
diff --git a/tests/lean/438.lean b/tests/lean/438.lean
new file mode 100644
index 000000000..186547d34
--- /dev/null
+++ b/tests/lean/438.lean
@@ -0,0 +1,12 @@
+import algebra.group
+open algebra
+
+attribute Group.struct [coercion]
+
+section
+  parameters {P₀ : Type} [P : group P₀]
+  include P
+
+  structure lambda_morphism := (comm : _ = _)
+
+end
diff --git a/tests/lean/438.lean.expected.out b/tests/lean/438.lean.expected.out
new file mode 100644
index 000000000..9028f72f5
--- /dev/null
+++ b/tests/lean/438.lean.expected.out
@@ -0,0 +1,15 @@
+438.lean:10:41: error: don't know how to synthesize placeholder
+P₀ : Type,
+P : group P₀
+⊢ Type
+438.lean:10:39: error: don't know how to synthesize placeholder
+P₀ : Type,
+P : group P₀
+⊢ ?M_1
+438.lean:10:43: error: don't know how to synthesize placeholder
+P₀ : Type,
+P : group P₀
+⊢ ?M_1
+438.lean:10:2: error: failed to add declaration 'lambda_morphism.mk' to environment, type has metavariables
+  Π {P₀ : Type} {P : group P₀},
+    ?M_2 = ?M_3 → lambda_morphism P₀ P
diff --git a/tests/lean/run/structure_test.lean b/tests/lean/run/structure_test.lean
index 684b6c34d..94b391378 100644
--- a/tests/lean/run/structure_test.lean
+++ b/tests/lean/run/structure_test.lean
@@ -14,6 +14,7 @@ section
   universe variable l
   variable A : Type.{l}
   variable Ha : decidable_eq A
+  include Ha
   variable E : Type₂
   include E
    -- include Ha