Add doc on the new API for universe polymorphism and primitive projections
- Add back some compatibility functions to avoid rewriting plugins.
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
Avoid u+k <= v constraints, don't take the sup of an algebraic universe during
minimization.