feat(frontends/lean/elaborator): more strict test for bad universe solution

src/frontends/lean/elaborator.cpp

@@ -49,6 +49,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/placeholder_elaborator.h"
 #include "frontends/lean/coercion_elaborator.h"
 #include "frontends/lean/proof_qed_elaborator.h"
+#include "frontends/lean/pp_options.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
 #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
@@ -604,9 +605,20 @@ public:
             });
     }
 
+    static bool contains_placeholder(level const & l) {
+        bool contains = false;
+        for_each(l, [&](level const & l) {
+                if (contains) return false;
+                if (is_placeholder(l))
+                    contains = true;
+                return true;
+            });
+        return contains;
+    }
+
     expr visit_sort(expr const & e) {
         expr r = update_sort(e, replace_univ_placeholder(sort_level(e)));
-        if (is_placeholder(sort_level(e)))
+        if (contains_placeholder(sort_level(e)))
             m_to_check_sorts.emplace_back(e, r);
         return r;
     }
@@ -1042,25 +1054,23 @@ public:
             expr pre  = p.first;
             expr post = p.second;
             lean_assert(is_sort(post));
-            level u   = sort_level(post);
-            lean_assert(is_meta(u));
-            if (s.is_assigned(u)) {
+            for_each(sort_level(post), [&](level const & u) {
+                    if (is_meta(u) && s.is_assigned(u)) {
                         level r = *s.get_level(u);
-                if (is_zero(r)) {
-                    throw_kernel_exception(env(), pre, [=](formatter const &) {
-                            return format("solution computed by the elaborator forces Type to be Prop");
-                        });
-                }
                         if (is_explicit(r)) {
-                    throw_kernel_exception(env(), pre, [=](formatter const &) {
-                            unsigned u = to_explicit(r);
-                            format   r = format("solution computed by the elaborator forces Type to be Type.{");
-                            r += format(u);
-                            r += format("}, (possible solution: use Type')");
+                            substitution saved_s(s);
+                            throw_kernel_exception(env(), pre, [=](formatter const & fmt) {
+                                    options o = fmt.get_options();
+                                    o  = o.update(get_pp_universes_option_name(), true);
+                                    format r("solution computed by the elaborator forces a universe placeholder"
+                                             " to be a fixed value, computed sort is");
+                                    r += pp_indent_expr(fmt.update_options(o), substitution(saved_s).instantiate(post));
                                     return r;
                                 });
                         }
                     }
+                    return true;
+                });
         }
     }
 

src/frontends/lean/pp_options.cpp

@@ -119,6 +119,7 @@ void finalize_pp_options() {
 
 name const & get_pp_coercions_option_name() { return *g_pp_coercions; }
 name const & get_pp_full_names_option_name() { return *g_pp_full_names; }
+name const & get_pp_universes_option_name() { return *g_pp_universes; }
 
 unsigned get_pp_max_depth(options const & opts)     { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
 unsigned get_pp_max_steps(options const & opts)     { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }

src/frontends/lean/pp_options.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 namespace lean {
 name const & get_pp_coercions_option_name();
 name const & get_pp_full_names_option_name();
+name const & get_pp_universes_option_name();
 
 unsigned get_pp_max_depth(options const & opts);
 unsigned get_pp_max_steps(options const & opts);

tests/lean/run/imp2.lean

@@ -1,4 +1,4 @@
 import data.num
-check (λ {A : Type'} (a : A), a) 10
+check (λ {A : Type.{1}} (a : A), a) 10
 check (λ {A} a, a) 10
 check (λ a, a) 10

tests/lean/univ.lean

@@ -0,0 +1,19 @@
+import data.num
+
+definition id (A : Type) (a : A) := a
+
+check id Type num
+
+check id Type' num
+
+check id Type.{1} num
+
+check id _ num
+
+check id Type.{_+1} num
+
+check id Type.{0+1} num
+
+check id Type Type.{1}
+
+check id Type' Type.{1}

tests/lean/univ.lean.expected.out

@@ -0,0 +1,13 @@
+univ.lean:5:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+  Type.{1}
+univ.lean:7:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+  Type.{1}
+id Type num : Type
+id Type num : Type
+univ.lean:13:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+  Type.{1}
+id Type num : Type
+univ.lean:17:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+  Type.{2}
+univ.lean:19:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+  Type.{2}