Explicit universes

Universes can now be instantiated explicitly. The syntax for a universe instantiation is

f u#universe_level_expression

A universe level expression is either :

• a natural number n,
• a universe level variable a,
• a sum u1 + u2 where at most one of the two universe expression contains a variable,
• or the maximum of a list of universe expressions max u1 u2 .. un.

A universe variable is any lowercase identifier (though it is not recommended to use max as an identifier). Universe variables are bound at the enclosing toplevel definition in the syntactical order they were found in the term. If a term contains a universe level variable, there must not be any implicitly generalized universe variable, that is let f (a : Type u#a) (b : Type) = 5 is invalid since there is an implicit unconstrained universe variable in (b:Type) whereas let g (a : Type u#a) (b : Type) = a == b is valid since the unspecified type variable is unified with a.

For such an invalid term an error Generalized universe in a term containing explicit universe annotation is reported. The compiler options --print_universes --print_bound_var_types may help debugging such an issue.

The order for universe variable binding in the following example

assume type dtuple3: a:Type u#a -> b:(a -> Type u#b) -> (x:a -> b x -> Type u#c) -> Type0

is a, b, c.

If you are ever unsure about how the variables are bound (or want to find out if there is a bug in the implementation) you can use fstar test.fst --dump_module Test --print_universes where test.fst is the file in which you put the above example. This will result in something like

module Test
assume val Test.dtuple3 <> : (a:Type u#(a) -> b:(_:a@0 -> Type u#(b)) -> _:(x:a@1 -> _:(b@1 x@0) -> Type u#(c)) -> Type u#(0))
module Test
assume val Test.dtuple3 <uu___174, uu___175, uu___176> : (a:Type u#(uu___174) -> b:(uu___:a@0 -> Type u#(uu___175)) -> uu___:(x:a@1 -> uu___:(b@1 x@0) -> Type u#(uu___176)) -> Type u#(0))

where you can see that the variables have been correctly bound (with a renamed to uu__174, b to uu__175 and c to uu__176).

Let rec definitions

All mutually recursively defined definitions must share the same list of explicit universe names. Moreover, since F* do not support polymorphic recursion, it is forbidden to apply explicit universes to a recursively bound term, e.g

let rec length (a:Type u#ua) (l : list a) = match l with
  | [] -> 0
  | x :: xs -> 1 + length (* the application u# is forbidden at this point*) a xs