It seems to me that there are no real reasons to not like cumulativity (the example given here seems to not be too relevant, according to the comments), and yet most proof assistants (apart from Coq?) don't have cumulativity. Why is this so? This seems a very nice property mathematically, and is akin to how most people would think of universes intuitively.
The short answer is that cummulativity is just one possible design choice which does not fit all purposes.
The slightly longer answer is that baking commulativity into type theory is a very dramatic design choice that complicates the typing rules, equality and conversion, universe management, and the semantics.
The real question is not whether we should have cummulativity but rather how to organize universes so that the user can control them when they wish or must do so, and at the same time the proof assistant can handle them by itself in a reasonable way. It is not clear (to me) that cummulativity is the best way to approach the problem. There are other options, such as implicit coercions, explicit coercions (also known as "lifting"), univere polymorphism, etc.
There is also a wider issue, namely that from a foundational point of view there seems little reason to fix a specific hierachy of universes (such as a linearly ordered sequence of universes indexed by natural numbers). You may call me a logician but I really dislike arbitrary choices in foundations of mathematics.
The biggest problem in my head is that cumulativity opens the door of subtyping in type theory, which, IMO, a potential calamity to type theory. If you elaborate cumulativity to non-cumulativity + lifting, then it's probably fine, but let me say something about the subtyping-based approach.
Once you have subtyping, you'll start thinking about covariance and contravariance, which brings a lot more things to the type theory. Also, subtyping itself distinguishes two notions: consider $(a:A)\in\Gamma$, then "the type of $a$" and "$A$" are no longer the same under the context $\Gamma$. Instead, "the type of $a$" is a subtype of $A$, and when you want to, for example, apply $a$ to the identity function with the type argument an implicit argument, then probably you can't solve the metavariable because $A$ won't be the most accurate solution (I thank Pavel for sharing some ideas with me about this).
Apart from that, cumulativity generates more complex universe level equations, which are harder to solve.