RFC: printing coercions with type ascriptions

Stream: general

[Anne Baanen]

I wrote a modification to the pretty-printer, which adds the expected type to the pretty-printing of coercions. For example,

import data.real.basic
variables (x : ℝ) (i : ℤ)
#check x + i -- x + (↑i : ℝ)

I think this is a good idea because coercions are a major issue in the roundtripping of pretty-printed output: if I copy a goal usually I have to go through and manually add type ascriptions to each coercion. Since this expected type is an argument to docs#coe anyway, it doesn't cost us much to add the type to the pretty-printer output.

The commit includes this change for both docs#coe (↑) and docs#coe_fn (⇑). It can also be turned off using set_option pp.ascript_coercions false.

Before I add tests and everything else to make this a real PR to Lean, I'd like some feedback: is enabling the ascriptions by default a good idea?

I also feel that there's a better way to actually construct the output string (currently I just concatenate every token together), does a Lean expert have suggestions?

[Anne Baanen]

cc the people at ITP I've discussed this with: @Yaël Dillies @Frédéric Dupuis @Rob Lewis @Jannis Limperg @Bhavik Mehta

[Yaël Dillies]

Some ascriptions in the wild are by pretty long types, so I would feel uncomfortable making that the default.

[Eric Rodriguez]

This is I think something sorely needed, but I think every file has different opinions whether this is needed or not. This would be lifesaving in flt-regular and such, but I think in places where you're just casting n : nat to some ring R it could be cluttery. We're not currently allowed set_option in files, I don't think, but I think this should be allowed

[Yaël Dillies]

Surely we are:

set_option old_structure_cmd true

[Eric Rodriguez]

ahh, we're only banned pp, profiler, and trace. I guess this would go under pp, but maybe this could be excepted

[Eric Rodriguez]

this may be a good idea anyways for cardinal related files, allowing pp.universes to be on in those files would be good

[Violeta Hernández]

I believe this should be disabled by default. The whole point of coercions is that they're supposed to be (for the most part) invisible. But having the option to enable this is great.

[Bhavik Mehta]

I agree it feels weird for this to be the default, but I definitely think this will be useful!

[Mario Carneiro]

Eric Rodriguez said:

ahh, we're only banned pp, profiler, and trace. I guess this would go under pp, but maybe this could be excepted

Why would pp options be in mathlib? It doesn't affect the compilation of anything. If it's your project you can do what you like but I don't see a reason that pp.ascript_coercions would be different here

[Johan Commelin]

But if it doesn't affect the compilation of anything, yet is a sensible setting for a certain file, why shouldn't it be in mathlib?

[Johan Commelin]

Things like set_option pp.universes true at the top of a file about cardinals or categorical limits makes a lot of sense to me.

[Johan Commelin]

The lean executable isn't the only thing out there trying to work with .lean files in mathlib.

[Mario Carneiro]

At least, any such option would need to come with a comment explaining that it is meant to be a permanent addition and why

[Eric Wieser]

In my opinion, instead of adding set_option calls to files, we should be adding more attributes like pp_nodot so that we can attach the choices to declarations

[Violeta Hernández]

It would be nice to have an option to show explicit universes in e.g. docs#cardinal.lift, for instance

[Eric Wieser]

Yes, that type of thing with universes is the main thing I had in mind

[Floris van Doorn]

Anne Baanen said:

if I copy a goal usually I have to go through and manually add type ascriptions to each coercion.

I have a very different experience: if I copy a goal, I usually have to manually delete all coercion arrows for it to elaborate correctly again (note to self: use set_option pp.coercions false more frequently).
Maybe this has to do with the fact that most coercions in the goals I'm dealing with are coe_fn/⇑, where you almost always have a unique coercion, and there is usually no ambiguity if you leave out the coercion arrow (both for Lean and for human readers). I would be unhappy if ⇑ becomes an explicit type ascription by default, but of course I would welcome the option.
I'm unsure what I think about replacing the usual coercion ↑ with a type ascription by default.

[Yaël Dillies]

That to me means that we should have a round-tripping mode that will try its best to make the expression round-trip. This has a small scalar product with the current discussion (it's almost orthogonal!).

[Floris van Doorn]

That is a discussion we should only have in the context of Lean 4.

[Eric Wieser]

It strikes me as an elaboration bug that inserting ⇑ almost always makes things fail to elaborate, despite successful elaboration inserting it for us

[Eric Wieser]

An option to print without coe_fn arrows at all feels like it would eliminate that pain