pp_with_univ for only some universe arguments

Stream: general

[Eric Wieser]

For things like docs#ULift and docs#Category, ideally we would only show the first universe argument when pretty-printing, as the second one is obvious by unification; so ULift.{v} C and Category.{v} C where C : Type u

A quick investigation suggests that modifying pp_with_univ to achieve this (perhaps with syntax pp_with_univ 1) is challenging because the current approach is to locally turn on pp.universes, print the entire constant name, then turn it off again.

Is it straightforward to write a custom constant pretty-printer?

[Eric Wieser]

(context: #6684 makes ULift X now print as ULift.{v,u} X, which overshoots the printing behavior we actually want)

[Gabriel Ebner]

To quote my original PR (#5564):

It might be cute to pretty-print Category.{v} as well, but that is much more involved since the pretty-printer for constants is hardcoded.

[Eric Wieser]

I don't know why I didn't think of reading the commit history here, thanks for reminding me. I came to the same hunch reading the source.

[Eric Wieser]

Would a core change to have explicit vs implicit universe arguments be anywhere near plausible?

[Scott Morrison]

I think this is a rather too small issue to warrant core changes at this point.

[Eric Wieser]

Yes, I meant this in more of a "if I opened an RFC would anyone think this was a good idea", rather than the higher bar of "worth spending time on".

[Scott Morrison]

I think at the moment "is opening this RFC a good idea" is a higher bar than "is this worth spending time on"!

[Scott Morrison]

(I appreciate that this is not exactly what you said. :-)