From f21f1219d90cf2ddf368f8ba4758bcd6c41ad693 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 2 Oct 2016 08:07:19 -0700
Subject: [PATCH] fix(frontends/lean/structure_cmd): handle is_one_placeholder

---
 src/frontends/lean/structure_cmd.cpp          |  3 +++
 tests/lean/bad_structures.lean                |  6 +++---
 tests/lean/bad_structures.lean.expected.out   |  4 ++--
 tests/lean/run/structure_result_universe.lean | 18 ++++++++++++++++++
 4 files changed, 26 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/structure_result_universe.lean

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index f808fba39c..6f854a0d57 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -254,6 +254,9 @@ struct structure_cmd_fn {
             m_inductive_predicate = is_zero(sort_level(m_type));
             if (m_inductive_predicate) {
                 m_infer_result_universe = false;
+            } else if (is_one_placeholder(sort_level(m_type))) {
+                m_infer_result_universe = false;
+                m_type = m_p.save_pos(mk_sort(mk_level_one()), pos);
             } else {
                 m_infer_result_universe = is_placeholder(sort_level(m_type));
                 if (!m_infer_result_universe) {
diff --git a/tests/lean/bad_structures.lean b/tests/lean/bad_structures.lean
index 91170032f7..022a291cab 100644
--- a/tests/lean/bad_structures.lean
+++ b/tests/lean/bad_structures.lean
@@ -1,12 +1,12 @@
 prelude namespace foo structure {l} prod (A : Type l) (B : Type l) :=
 (pr1 : A) (pr2 : B)
 
-structure {l} prod (A : Type l) (B : Type l) : Type :=
+structure {l} prod1 (A : Type l) (B : Type l) : Type :=
 (pr1 : A) (pr2 : B)
 
-structure {l} prod (A : Type l) (B : Type l) : Type l :=
+structure {l} prod2 (A : Type l) (B : Type l) : Type l :=
 (pr1 : A) (pr2 : B)
 
-structure {l} prod2 (A : Type l) (B : Type l) : Type (max 1 l) :=
+structure {l} prod3 (A : Type l) (B : Type l) : Type (max 1 l) :=
 (pr1 : A) (pr2 : B)
 end foo
diff --git a/tests/lean/bad_structures.lean.expected.out b/tests/lean/bad_structures.lean.expected.out
index 91fda4ca71..24dfaffb2c 100644
--- a/tests/lean/bad_structures.lean.expected.out
+++ b/tests/lean/bad_structures.lean.expected.out
@@ -1,2 +1,2 @@
-bad_structures.lean:4:52: error: invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')
-bad_structures.lean:7:54: error: invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')
+bad_structures.lean:4:0: error: universe level of type_of(arg #3) of 'foo.prod1.mk' is too big for the corresponding inductive datatype
+bad_structures.lean:7:55: error: invalid universe polymorphic structure declaration, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')
diff --git a/tests/lean/run/structure_result_universe.lean b/tests/lean/run/structure_result_universe.lean
new file mode 100644
index 0000000000..534288ebfb
--- /dev/null
+++ b/tests/lean/run/structure_result_universe.lean
@@ -0,0 +1,18 @@
+structure foo1 (A : Type) : Type :=
+(elt : A)
+
+structure {u} foo2 (A : Type u) : Type (u+1) :=
+(val : A)
+
+structure {u} foo3 (A : Type u) : Type (max u 1) :=
+(val : A)
+
+universe variable u
+
+structure foo4 (A : Type u) : Type (max u 1) :=
+(val : A)
+
+check foo1
+check foo2
+check foo3
+check foo4