In Juvix Core we have a nameless representation by default, with names being introduced as an extension in HR (and HRAnn). By default, this unfortunately means that λx. t is represented as Lam t x. So it would be nice if the fields could be reordered.
A related idea is to have annotations which are products be split up in the patterns, e.g. being able to write (in Ann) (π f: s) (ρ e: t) as App π f s ρ e t instead of App f e (π, s, ρ, t)