feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit

doc/lean/declarations.org

@@ -5,7 +5,7 @@
 The command =definition= declares a new constant/function. The identity function is defined as
 
 #+BEGIN_SRC lean
-  definition id (A : Type) (a : A) : A := a
+  definition id {A : Type} (a : A) : A := a
 #+END_SRC
 
 We say definitions are "transparent", because the type checker can
@@ -22,12 +22,12 @@ _definitionally equal_.
 #+END_SRC
 
 Similarly, the following definition only type checks because =id= is transparent, and the type checker can establish that
-=nat= and =id Type nat= are definitionally equal, that is, they are the "same".
+=nat= and =id nat= are definitionally equal, that is, they are the "same".
 
 #+BEGIN_SRC lean
   import data.nat
-  definition id (A : Type) (a : A) : A := a
+  definition id {A : Type} (a : A) : A := a
-  check λ (x : nat) (y : id Type nat), x = y
+  check λ (x : nat) (y : id nat), x = y
 #+END_SRC
 
 ** Theorems
@@ -38,8 +38,8 @@ really care about the actual proof, only about its existence.  As
 described in previous sections, =Prop= (the type of all propositions)
 is _proof irrelevant_.  If we had defined =id= using a theorem the
 previous example would produce a typing error because the type checker
-would be unable to unfold =id= and establish that =nat= and =id Type
+would be unable to unfold =id= and establish that =nat= and =id nat=
-nat= are definitionally equal.
+are definitionally equal.
 
 ** Opaque definitions
 
@@ -58,26 +58,26 @@ Here is an example
 
 #+BEGIN_SRC lean
     import data.nat
-    opaque definition id (A : Type) (a : A) : A := a
+    opaque definition id {A : Type} (a : A) : A := a
     -- The following command is type correct since it is being executed in the
     -- same file where id was defined
-    check λ (x : nat) (y : id Type nat), x = y
+    check λ (x : nat) (y : id nat), x = y
 
     -- The following theorem is also type correct since id is being treated as
     -- transparent only in the proof by reflexivity.
-    theorem id_eq (A : Type) (a : A) : id A a = a :=
+    theorem id_eq {A : Type} (a : A) : id a = a :=
     eq.refl a
 
     -- The following transparent definition is also type correct. It uses
     -- id but it can be type checked without unfolding id.
-    definition id2 (A : Type) (a : A) : A :=
+    definition id2 {A : Type} (a : A) : A :=
-    id A a
+    id a
 
     -- The following definition is type incorrect. It only type checks if
     -- we unfold id, but it is not allowed because the definition is opaque.
     /-
-    definition buggy_def (A : Type) (a : A) : Prop :=
+    definition buggy_def {A : Type} (a : A) : Prop :=
-    ∀ (b : id Type A), a = b
+    ∀ (b : id A), a = b
     -/
 #+END_SRC
 
@@ -87,9 +87,9 @@ unfold the opaque definition =id= to type check it.
 
 #+BEGIN_SRC lean
     import data.unit
-    opaque definition id (A : Type) (a : A) : A := a
+    opaque definition id {A : Type} (a : A) : A := a
     /-
-    theorem buggy_thm (a : unit) (b : id Type unit) : a = b :=
+    theorem buggy_thm (a : unit) (b : id unit) : a = b :=
     unit.equal a b
     -/
 #+END_SRC
@@ -99,8 +99,8 @@ transparent in this example.
 
 #+BEGIN_SRC lean
   import data.unit
-  definition id (A : Type) (a : A) : A := a
+  definition id {A : Type} (a : A) : A := a
-  theorem simple (a : unit) (b : id Type unit) : a = b :=
+  theorem simple (a : unit) (b : id unit) : a = b :=
   unit.equal a b
 #+END_SRC
 

library/hott/trunc.lean

@@ -26,7 +26,7 @@ trunc_S : trunc_index → trunc_index
 -- TODO: add coercions to / from nat
 
 -- TODO: note in the Coq version, there is an internal version
-definition IsTrunc (n : trunc_index) : Type → Type :=
+definition IsTrunc (n : trunc_index) : Type.{1} → Type.{1} :=
 trunc_index.rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n
 
 -- TODO: in the Coq version, this is notation

src/frontends/lean/elaborator.cpp

@@ -1051,6 +1051,15 @@ public:
                             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')");
+                            return r;
+                        });
+                }
             }
         }
     }

src/kernel/level.cpp

@@ -205,6 +205,11 @@ pair<level, unsigned> to_offset(level l) {
     return mk_pair(l, k);
 }
 
+unsigned to_explicit(level const & l) {
+    lean_assert(is_explicit(l));
+    return to_offset(l).second;
+}
+
 level mk_max(level const & l1, level const & l2)  {
     if (is_explicit(l1) && is_explicit(l2)) {
         return get_depth(l1) >= get_depth(l2) ? l1 : l2;

src/kernel/level.h

@@ -114,7 +114,10 @@ name const & level_id(level const & l);
    2) l = succ(l') and l' is explicit
 */
 bool is_explicit(level const & l);
-
+/** \brief Convert an explicit universe into a unsigned integer.
+    \pre is_explicit(l)
+*/
+unsigned to_explicit(level const & l);
 /** \brief Return true iff \c l contains placeholder (aka meta parameters). */
 bool has_meta(level const & l);
 /** \brief Return true iff \c l contains globals */

tests/lean/run/imp2.lean

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