http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism
In Agda, Level is an explicit value that one can specify, so you need to make sure to quantify over all n if you want a type that works at all levels.
Coq's paper for universe polymorphism seems to indicate that n can be inferred, such that one can write a Set : Set and still have a consistent language (where it is automatically turned into something of the form {n m} Set n : Set m, and constraint of n < m is added to the context).
Is there some assumption that Agda makes that makes it impossible for the levels to infer? (Or makes it infeasible to compute for some reason?)