feat(kernel): make sure U is the maximal universe

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/heq.lean

@@ -24,7 +24,6 @@ axiom hcongr {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} {f : ∀ x, B
       f == f' → a == a' → f a == f' a'
 
 universe M ≥ 1
-universe U ≥ M + 1
 definition TypeM := (Type M)
 
 -- In the following definitions the type of A and A' cannot be TypeU

src/kernel/environment.cpp

@@ -25,6 +25,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/normalizer.h"
 #include "kernel/universe_constraints.h"
+#include "kernel/kernel.h"
 #include "version.h"
 
 namespace lean {
@@ -320,6 +321,9 @@ void environment_cell::add_constraints(name const & n, level const & l, int k) {
 void environment_cell::check_consistency(name const & n, level const & l, int k) const {
     switch (kind(l)) {
     case level_kind::UVar:
+        if (l == ty_level(TypeU))
+            throw kernel_exception(env(), sstream() << "invalid universe constraint: " << n << " >= " << l << " + " << k
+                                   << ", several modules in Lean assume that " << l << " is the maximal universe");
         if (!get_ro_ucs().is_consistent(n, uvar_name(l), k))
             throw kernel_exception(env(), sstream() << "universe constraint inconsistency: " << n << " >= " << l << " + " << k);
         if (get_ro_ucs().overflows(n, uvar_name(l), k))
@@ -338,15 +342,25 @@ level environment_cell::add_uvar_cnstr(name const & n, level const & l) {
     level r;
     auto const & uvs = get_ro_universes().m_uvars;
     auto it = std::find_if(uvs.begin(), uvs.end(), [&](level const & l) { return uvar_name(l) == n; });
+    bool new_universe;
     check_consistency(n, l, 0);
     if (it == uvs.end()) {
         r = add_uvar_core(n);
+        new_universe = true;
     } else {
         // universe n already exists, we must check consistency of the new constraint.
         r = *it;
+        new_universe = false;
     }
     m_objects.push_back(mk_uvar_cnstr(n, l));
     add_constraints(n, l, 0);
+    name const & Uname = uvar_name(ty_level(TypeU));
+    if (new_universe && n != Uname && !is_ge(ty_level(TypeU), r, 1)) {
+        // In Lean, U is the maximal universe, several Lean modules assume that,
+        // and the kernel axioms are all with respect to U.
+        // So, we force all other universes to smaller than U
+        add_uvar_cnstr(Uname, r+1);
+    }
     return r;
 }
 

tests/lean/univ.lean

@@ -8,24 +8,13 @@ assert(env:get_universe_distance("Z", "M") == 3)
 assert(not env:get_universe_distance("Z", "U"))
 *)
 
-scope
-  universe Z ≥ U + 10
-  (*
-    local env = get_environment()
-    assert(env:get_universe_distance("Z", "U") == 10)
-    assert(env:get_universe_distance("Z", "M") ==
-              env:get_universe_distance("Z", "U") +
-              env:get_universe_distance("U", "M"))
-  *)
-pop_scope
-
 (*
 local env = get_environment()
 assert(env:get_universe_distance("Z", "M") == 3)
 assert(not env:get_universe_distance("Z", "U"))
 *)
 
-universe Z1 ≥ U + 1073741824.
+universe Z1 ≥ M + 1073741824.
 universe Z2 ≥ Z1 + 1073741824.
 
 universe U1
@@ -40,3 +29,6 @@ assert(env:get_universe_distance("U4", "U3") == 3)
 assert(env:get_universe_distance("U4", "U2") == 1)
 *)
 universe U1 ≥ U4.
+
+universe Z >= U.
+universe Z >= U + 1.

tests/lean/univ.lean.expected.out

@@ -1,5 +1,7 @@
   Set: pp::colors
   Set: pp::unicode
   Defined: TypeM
-univ.lean:29:0: error: universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824
+univ.lean:18:0: error: universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824
-univ.lean:42:0: error: universe constraint inconsistency: U1 >= U4 + 0
+univ.lean:31:0: error: universe constraint inconsistency: U1 >= U4 + 0
+univ.lean:33:0: error: invalid universe constraint: Z >= U + 0, several modules in Lean assume that U is the maximal universe
+univ.lean:34:0: error: invalid universe constraint: Z >= U + 1, several modules in Lean assume that U is the maximal universe

tests/lean/univ2.lean

@@ -1,9 +1,9 @@
-universe M >= 1
+universe M1 >= 1
-universe U >= M + 1
+universe M2 >= 1
-universe Z >= max U+1 M+1
+universe Z >= max M1+1 M2+1
-print environment 2
+print environment
 (*
 local env = get_environment()
-assert(env:get_universe_distance("Z", "U") == 1)
+assert(env:get_universe_distance("Z", "M1") == 1)
-assert(env:get_universe_distance("Z", "M") == 2)
+assert(env:get_universe_distance("Z", "M2") == 1)
 *)

tests/lean/univ2.lean.expected.out

@@ -1,4 +1,10 @@
   Set: pp::colors
   Set: pp::unicode
-universe U ≥ M+1
+import "kernel"
-universe Z ≥ U+1 ⊔ M+1
+import "Nat"
+universe M1 ≥ 1
+universe U ≥ M1+1
+universe M2 ≥ 1
+universe U ≥ M2+1
+universe Z ≥ M1+1 ⊔ M2+1
+universe U ≥ Z+1