[Merged by Bors] - fix(lean/elaborator.cpp): reject Sort and suggest Prop

src/frontends/lean/elaborator.cpp

@@ -3513,7 +3513,11 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
         } else if (is_emptyc_or_emptys(e)) {
             return visit_emptyc_or_emptys(e, expected_type);
         } else if (is_sort_wo_universe(e)) {
-            return visit(get_annotation_arg(e), expected_type);
+            auto& arg = get_annotation_arg(e);
+            if (sort_level(arg) == mk_level_zero())
+                report_or_throw(elaborator_exception(arg,
+                    "invalid universe `Sort`, use `Sort 0` or `Prop` instead"));
+            return visit(arg, expected_type);
         } else {
             switch (e.kind()) {
                 case expr_kind::Var: lean_unreachable();  // LCOV_EXCL_LINE

tests/lean/sort.lean

@@ -0,0 +1,3 @@
+#check Sort
+#check Sort 0
+#check Prop

tests/lean/sort.lean.expected.out

@@ -0,0 +1,4 @@
+sort.lean:1:7: error: invalid universe `Sort`, use `Sort 0` or `Prop` instead
+Prop : Type
+Prop : Type
+Prop : Type