From 8c1f6b9055775cf5aa7e31ef725e2fb7def49e2c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Jan 2014 13:59:55 -0800
Subject: [PATCH] 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              | 1 +
 src/kernel/kernel.h                | 1 +
 src/kernel/type_checker.cpp        | 2 +-
 tests/lean/elab8.lean              | 3 +++
 tests/lean/elab8.lean.expected.out | 5 +++++
 5 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/elab8.lean
 create mode 100644 tests/lean/elab8.lean.expected.out

diff --git a/src/kernel/kernel.cpp b/src/kernel/kernel.cpp
index a35e6b391..d7dd91407 100644
--- a/src/kernel/kernel.cpp
+++ b/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);
 // =======================================
 
 // =======================================
diff --git a/src/kernel/kernel.h b/src/kernel/kernel.h
index a58b91b9f..9c6edbd6b 100644
--- a/src/kernel/kernel.h
+++ b/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();
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 666fb2b9f..c2709bae1 100644
--- a/src/kernel/type_checker.cpp
+++ b/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);
diff --git a/tests/lean/elab8.lean b/tests/lean/elab8.lean
new file mode 100644
index 000000000..e5df8dc17
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/tests/lean/elab8.lean.expected.out b/tests/lean/elab8.lean.expected.out
new file mode 100644
index 000000000..99c7a55fe
--- /dev/null
+++ b/tests/lean/elab8.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: D1
+  Defined: D2
+  Defined: D3