Universe level normalization has associativity of `max` backwards from parsing associativity

Description

Given universe level max u v w, it gets normalized as max (max u v) w.

Steps to Reproduce

In the following, the structure command derives the type automatically and normalizes the level.

structure Foo.{u,v,w} (α : Type (max u v w)) where
  val : α

#check Foo
/-
Foo.{u, v, w} (α : Type (max u v w)) : Type (max (max u v) w)
-/

Expected behavior: The universe level should be max u (max v w) (i.e., max u v w)

Actual behavior: The universe level is max (max u v) w

Versions

4.12.0 1d8555fe0bdd02c82664446309b2e167ac89c9e9

Additional Information

One way or the other, max u v w normalized should pretty print as max u v w.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the supplied Lean reproduction and inspect the universe-level normalization and pretty-printing paths; the issue names no source file or test. Done means the normalized result preserves the expected right-associated max form and a regression test covers the example.