Explicit universes

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

f u#universe_level_expression or f 'u_universe_level_variable

A universe level expression is either :

• a natural number n,
• a universe level variable 'ua,
• 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 must be prefixed by 'u. Universe variables are bound at the enclosing toplevel definition in the syntactical order they wermodule Test assume val Test.dtuple3 <> : (a:Type('ua) -> b:(:a@0 -> Type('ub)) -> :(x:a@1 -> :(b@1 x@0) -> Type('uc)) -> Type(0)) module Test assume val Test.dtuple3 <'uu___174, 'uu___175, 'uu___176> : (a:Type('uu___174) -> b:(uu:a@0 -> Type('uu___175)) -> uu___:(x:a@1 -> uu___:(b@1 x@0) -> Type('uu___176)) -> Type(0)) e 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 'ua) (b : Type) = 5 is invalid since there is an implicit unconstrained universe variable in (b:Type) whereas let g (a : Type 'ua) (b : Type) = a == b is valid.

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.

Note that 'u... is solely for universe variables, and you can't have type variables named 'u....

The order for universe variable binding in the following example

assume type dtuple3: a:Type 'ua -> b:(a -> Type 'ub) -> (x:a -> b x -> Type 'uc) -> Type0

is 'ua, 'ub, 'uc.

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('ua) -> b:(_:a@0 -> Type('ub)) -> _:(x:a@1 -> _:(b@1 x@0) -> Type('uc)) -> Type(0))
module Test
assume val Test.dtuple3 <'uu___174, 'uu___175, 'uu___176> : (a:Type('uu___174) -> b:(uu___:a@0 -> Type('uu___175)) -> uu___:(x:a@1 -> uu___:(b@1 x@0) -> Type('uu___176)) -> Type(0))

where you can see that the variables have been correctly bound (with 'ua renamed to 'uu__174, 'ub to 'uu__175 and 'uc to 'uu__176).