From 260795f981e124c668ea626fd6b843f7bb4eca91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Jan 2015 22:18:09 -0800
Subject: [PATCH] fix(frontends/lean/structure_cmd): collect universe levels
 that only occur in structure parameters

fixes #395
---
 src/frontends/lean/structure_cmd.cpp   |  2 ++
 tests/lean/hott/bug_struct_level.hlean | 34 ++++++++++++++++++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 tests/lean/hott/bug_struct_level.hlean

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 3080471f55..41816e8b24 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -579,6 +579,8 @@ struct structure_cmd_fn {
     void include_ctx_levels() {
         name_set all_lvl_params;
         all_lvl_params = collect_univ_params(m_type);
+        for (expr const & p : m_params)
+            all_lvl_params = collect_univ_params(mlocal_type(p), all_lvl_params);
         for (expr const & f : m_fields)
             all_lvl_params = collect_univ_params(mlocal_type(f), all_lvl_params);
         buffer<name> section_lvls;
diff --git a/tests/lean/hott/bug_struct_level.hlean b/tests/lean/hott/bug_struct_level.hlean
new file mode 100644
index 0000000000..3ddc64b040
--- /dev/null
+++ b/tests/lean/hott/bug_struct_level.hlean
@@ -0,0 +1,34 @@
+import algebra.precategory.basic
+
+open precategory
+
+context
+  parameter {D₀ : Type}
+  parameter (C  : precategory D₀)
+  parameter (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type)
+  reducible compose
+
+  definition comp₁_type [reducible]  : Type :=
+  Π ⦃a b c₁ d₁ c₂ d₂ : D₀⦄
+    ⦃f₁ : hom a b⦄ ⦃g₁ : hom c₁ d₁⦄ ⦃h₁ : hom a c₁⦄ ⦃i₁ : hom b d₁⦄
+    ⦃g₂ : hom c₂ d₂⦄ ⦃h₂ : hom c₁ c₂⦄ ⦃i₂ : hom d₁ d₂⦄,
+    (D₂ g₁ g₂ h₂ i₂) → (D₂ f₁ g₁ h₁ i₁) → (@D₂ a b c₂ d₂ f₁ g₂ (h₂ ∘ h₁) (i₂ ∘ i₁))
+
+  definition ID₁_type [reducible] : Type :=
+  Π ⦃a b : D₀⦄ (f : hom a b), D₂ f f (ID a) (ID b)
+
+  structure worm_precat [class] : Type :=
+  (comp₁     : comp₁_type)
+  (ID₁       : ID₁_type)
+end
+
+context
+  parameter {D₀ : Type}
+  parameter [C : precategory D₀]
+  parameter {D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type}
+  parameter [D : worm_precat C D₂]
+  include D
+
+  structure two_cell_ob : Type :=
+  (vo1 : D₀) (vo2 : D₀) (vo3 : hom vo1 vo2)
+end