While visiting the IAS for the special year on homotopy type theory, I've been working on an implementation of universe polymorphism and inference in Coq that should sove many of the current problems with the lack of polymorphism in the current system. The github is here and I've given a talk [1] about it.