diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 639b6674b..c264df933 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -201,6 +201,10 @@ struct structure_cmd_fn {
         }
     }
 
+    void throw_explicit_universe(pos_info const & pos) {
+        throw parser_error("invalid 'structure', the resultant universe must be provided when explicit universe levels are being used", pos);
+    }
+
     /** \brief Parse resultant universe */
     void parse_result_type() {
         auto pos = m_p.pos();
@@ -209,7 +213,14 @@ struct structure_cmd_fn {
             m_type = m_p.parse_expr();
             if (!is_sort(m_type))
                 throw parser_error("invalid 'structure', 'Type' expected", pos);
+            if (has_placeholder(m_type))
+                throw_explicit_universe(pos);
+            level l = sort_level(m_type);
+            if (m_env.impredicative() && !is_not_zero(l))
+                throw parser_error("invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment", pos);
         } else {
+            if (!m_infer_result_universe)
+                throw_explicit_universe(pos);
             m_type = m_p.save_pos(mk_sort(mk_level_placeholder()), pos);
         }
     }
diff --git a/tests/lean/bad_structures.lean b/tests/lean/bad_structures.lean
new file mode 100644
index 000000000..27f0755a5
--- /dev/null
+++ b/tests/lean/bad_structures.lean
@@ -0,0 +1,11 @@
+structure prod.{l} (A : Type.{l}) (B : Type.{l}) :=
+(pr1 : A) (pr2 : B)
+
+structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type :=
+(pr1 : A) (pr2 : B)
+
+structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{l} :=
+(pr1 : A) (pr2 : B)
+
+structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{max 1 l} :=
+(pr1 : A) (pr2 : B)
diff --git a/tests/lean/bad_structures.lean.expected.out b/tests/lean/bad_structures.lean.expected.out
new file mode 100644
index 000000000..9eabca9f0
--- /dev/null
+++ b/tests/lean/bad_structures.lean.expected.out
@@ -0,0 +1,10 @@
+bad_structures.lean:1:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
+bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
+bad_structures.lean:7:49: error: invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment
+generated type
+proj_type: Pi {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), A
+proj_val: fun {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), (prod.rec.{l l} A B (fun (c : prod.{l} A B), A) (fun (pr1 : A) (pr2 : B), pr1) c)
+proj_type: Pi {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), B
+proj_val: fun {A : Type.{l}} {B : Type.{l}} (c : prod.{l} A B), (prod.rec.{l l} A B (fun (c : prod.{l} A B), B) (fun (pr1 : A) (pr2 : B), pr2) c)
+generated projs
+generated auxiliary