[TYPES] Universe Polymorphism

[Klaus Ostermann]

Dear Types Readers,

I'd like to learn about languages that support an infinite number of type universes,
and in particular the notion of "universe polymorphism", as described in Harper and Pollack's
"Type Checking With Universes" paper. 

In particular I am interested in practical (maybe implemented?) programming languages which
support an infinite number of universes, some notion of "type:type", or other interesting
features along these lines.

All the calculi that I have seen seem to be based on dependent types (such as Generalized Calculus of Constructions). 
Wouldn't it also be possible to extend, say, F-Omega, with an infinite number of universes, without adding
dependent types? Has this already been done? I would assume that in such a language it would
be possible to add, say, a fixed point operator (on the term level) to the language without rendering type checking
undecidable, because types do not depend on terms.

What are the practical implications of having "type:type"? I read that it destroys the consistency of the
type system as a logic, but this is not relevant for my purposes. On one hand, I have read
that type-checking in systems with "type:type" is not decidable, but on the other hand, the paper 
"Why dependent types matter" mentions in Sec. 7 that the authors have adopted "type:type" in their
Epigram language. How does this fit together? Are there any useful examples in Epigram (or any other language) that
use the "type:type" possibility?

Regards,
Klaus Ostermann