Universe polymorphism: the inference of universes and their constraints
It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at:


Matthieu Sozeau and Nicolas Tabareau: Universe Polymorphism in Coq, Interactive Theorem Proving - 5th International Conference, ITP 2014
Beta Ziliani &amp; Matthieu Sozeau: A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading, ACM SIGPLAN International Conference on Functional Programming 2015.