fix(kernel/typechecker): allow elaborator to infer (Type U+1)

In the new test elab8.lean, the parameter B is in (Type U+1).
Before, this commit, the type checker was forcing all metavariables that must be types to be <= (Type U). This restriction was preventing the elaborator from succeeding in reasonable cases.

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

src/kernel/kernel.cpp

@@ -16,6 +16,7 @@ namespace lean {
 // Bultin universe variables m and u
 static level u_lvl(name("U"));
 expr const TypeU = Type(u_lvl);
+expr const TypeU1 = Type(u_lvl+1);
 // =======================================
 
 // =======================================

src/kernel/kernel.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 namespace lean {
 // See src/builtin/kernel.lean for signatures.
 extern expr const TypeU;
+extern expr const TypeU1; // Type (U+1)
 
 /** \brief Return the Lean Boolean type. */
 expr mk_bool_type();

src/kernel/type_checker.cpp

@@ -58,7 +58,7 @@ class type_checker::imp {
             return u;
         if (has_metavar(u) && m_menv && m_uc) {
             justification jst = mk_type_expected_justification(ctx, s);
-            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst));
+            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU1, jst));
             return u;
         }
         u = normalize(e, ctx, true);

tests/lean/elab8.lean

@@ -0,0 +1,3 @@
+definition D1 (A : (Type U)) (B : Nat → (Type U)) := true
+definition D2 (A : (Type U)) (B : A → (Type U)) := true
+definition D3 (A : (Type U)) (B : A → (Type U)) := false

tests/lean/elab8.lean.expected.out

@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: D1
+  Defined: D2
+  Defined: D3