refactor(builtin/kernel): start with small universes

The universe constraint manager is more flexible now.
We don't need to start with a huge universe  U >= 512.
We can start small, and increase it on demand.

If module mod1 needs it, it can always add

   universe U >= 3

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

src/builtin/kernel.lean

@@ -1,7 +1,6 @@
 import macros
 
-universe M ≥ 512
-universe U ≥ M+512
+universe U ≥ 1
 
 variable Bool : Type
 -- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions
@@ -10,7 +9,6 @@ builtin false : Bool
 builtin if {A : (Type U)} : Bool → A → A → A
 
 definition TypeU := (Type U)
-definition TypeM := (Type M)
 
 definition not (a : Bool) : Bool
 := a → false

src/kernel/builtin.cpp

@@ -13,9 +13,7 @@ Author: Leonardo de Moura
 namespace lean {
 // =======================================
 // Bultin universe variables m and u
-static level m_lvl(name("M"));
 static level u_lvl(name("U"));
-expr const TypeM = Type(m_lvl);
 expr const TypeU = Type(u_lvl);
 // =======================================
 

src/kernel/builtin.h

@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 // See src/builtin/kernel.lean for signatures.
-extern expr const TypeM;
 extern expr const TypeU;
 
 /** \brief Return the Lean Boolean type. */

src/library/elaborator/elaborator.cpp

@@ -148,7 +148,6 @@ class elaborator::imp {
     justification                            m_conflict;
     bool                                     m_first;
     level                                    m_U; // universe U used for builtin kernel axioms
-    level                                    m_M; // universe M
 
     // options
     bool                                     m_use_justifications;
@@ -1179,19 +1178,15 @@ class elaborator::imp {
             // We approximate and only consider the most useful ones.
             justification new_jst(new destruct_justification(c));
             if (is_bool(a)) {
-                expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU };
+                expr choices[5] = { Bool, Type(), Type(level() + 1), TypeU };
                 push_active(mk_choice_constraint(get_context(c), b, 5, choices, new_jst));
                 return true;
             } else if (m_env->is_ge(ty_level(a), m_U)) {
                 expr choices[2] = { a, Type(ty_level(a) + 1) };
                 push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst));
                 return true;
-            } else if (m_env->is_ge(ty_level(a), m_M)) {
-                expr choices[3] = { a, Type(ty_level(a) + 1), TypeU };
-                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
-                return true;
             } else {
-                expr choices[4] = { a, Type(ty_level(a) + 1), TypeM, TypeU };
+                expr choices[4] = { a, Type(ty_level(a) + 1), TypeU };
                 push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst));
                 return true;
             }
@@ -1254,13 +1249,9 @@ class elaborator::imp {
                 push_active(mk_choice_constraint(get_context(c), a, 2, choices, new_jst));
                 return true;
             } else if (b == TypeU) {
-                expr choices[5] = { TypeU, TypeM, Type(level() + 1), Type(), Bool };
+                expr choices[5] = { TypeU, Type(level() + 1), Type(), Bool };
                 push_active(mk_choice_constraint(get_context(c), a, 5, choices, new_jst));
                 return true;
-            } else if (b == TypeM) {
-                expr choices[4] = { TypeM, Type(level() + 1), Type(), Bool };
-                push_active(mk_choice_constraint(get_context(c), a, 4, choices, new_jst));
-                return true;
             } else {
                 level const & lvl = ty_level(b);
                 lean_assert(!lvl.is_bottom());
@@ -1772,7 +1763,6 @@ public:
         m_next_id     = 0;
         m_first       = true;
         m_U           = m_env->get_uvar("U");
-        m_M           = m_env->get_uvar("M");
         // display(std::cout);
     }
 

src/tests/library/elaborator/elaborator.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "library/io_state_stream.h"
 #include "library/placeholder.h"
+#include "library/printer.h"
 #include "library/arith/arith.h"
 #include "library/elaborator/elaborator.h"
 #include "frontends/lean/frontend.h"
@@ -821,6 +822,7 @@ void tst26() {
     */
     environment env;
     init_test_frontend(env);
+    env->add_uvar_cnstr("U", level() + 2);
     metavar_env menv;
     buffer<unification_constraint> ucs;
     type_checker checker(env);
@@ -861,7 +863,7 @@ void tst27() {
     expr eq = Const("my_eq");
     env->add_var("my_eq", Pi({A, TypeU}, A >> (A >> Bool)));
     env->add_var("g", Pi({A, TypeU}, A >> A));
-    env->add_var("a", TypeM);
+    env->add_var("a", Type());
     expr m1 = menv->mk_metavar();
     expr m2 = menv->mk_metavar();
     expr m3 = menv->mk_metavar();
@@ -872,7 +874,7 @@ void tst27() {
     metavar_env s = elb.next();
     std::cout << s->instantiate_metavars(F) << "\n";
     lean_assert_eq(s->instantiate_metavars(F),
-                   Fun({f, TypeM >> TypeM}, eq(TypeM, g(TypeM >> TypeM, f)(a), a)));
+                   Fun({f, Type() >> Type()}, eq(Type(), g(Type() >> Type(), f)(a), a)));
 }
 
 int main() {

tests/lean/cast4.lean

@@ -1,5 +1,8 @@
 import cast
 set::option pp::colors false
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (B   : A -> TypeM)

tests/lean/cast4.lean.expected.out

@@ -2,6 +2,7 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
+  Defined: TypeM
 λ (A A' : TypeM)
   (B : A → TypeM)
   (B' : A' → TypeM)

tests/lean/norm_bug1.lean

@@ -1,5 +1,8 @@
 import cast
 set::option pp::colors false
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (a   : A)

tests/lean/norm_bug1.lean.expected.out

@@ -2,6 +2,7 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
+  Defined: TypeM
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
     ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)

tests/lean/tst15.lean

@@ -1,3 +1,5 @@
+universe M >= 1
+universe U >= M + 1
 variable x : (Type max U+1+2 M+1 M+2 3)
 check x
 variable f : (Type U+10) -> Type

tests/lean/tst5.lean

@@ -1,3 +1,4 @@
+universe U >= 3
 variable N : Type
 variable a : N
 variable b : N

tests/lean/type_inf_bug1.lean

@@ -1,5 +1,8 @@
 import cast
 set::option pp::colors false
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (a   : A)

tests/lean/type_inf_bug1.lean.expected.out

@@ -2,6 +2,7 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
+  Defined: TypeM
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
     ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)

tests/lean/univ.lean

@@ -1,4 +1,7 @@
 
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
 universe Z ≥ M+3
 (*
 local env = get_environment()

tests/lean/univ.lean.expected.out

@@ -1,4 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
-Error (line: 27, pos: 0) universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824
-Error (line: 40, pos: 0) universe constraint inconsistency: U1 >= U4 + 0
+  Defined: TypeM
+Error (line: 30, pos: 0) universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824
+Error (line: 43, pos: 0) universe constraint inconsistency: U1 >= U4 + 0

tests/lean/univ2.lean

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

tests/lean/univ2.lean.expected.out

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