[TYPES] Universe Polymorphism

[Stefan Holdermans]

Thorsten,

> It seems to me that Type:Type is an honest form of impredicativity,
> because at least you know that the system is inconsistent as a logic
> (as opposed to System F where so far nobody has been able to show
> this :-). Type:Type includes System F and the calculus of
> constructions and I think all *reasonable* programs can be reformed
> into Type(i):Type(i+1) possibly parametric in i. However, sometimes
> you don't want to think about the levels initially and sort this out
> later - i.e. use Type:Type. A similar attitude makes sense in
> Mathematics, in particular Category Theory, where it is convenient to
> worry about size conditions later...

 From a programmer's perspective: what can be said about the  
inferrability of universe polymorphism? I mean: it would be great if  
the programmer could just proceed as if Type:Type and have the  
compiler infer the correct indices, universe abstractions, and  
universe applications.

Cheers,

  Stefan