Only printing abbreviations · Coq devs & plugin devs

Today abbreviations cannot be only printing. I'm wondering if this limitation can be lifted, since it would provide a quick alternative to https://github.com/coq/coq/pull/17484
CC @Hugo Herbelin

Enrico Tassi (May 17 2023 at 08:53):

In particular reverse coercions lets on type, say, nat in place of nat_eqType. If we could print nat in place of nat_eqType we would both obtain a nicer output and keep "round tripping", e.g. copy pasting the goal would just typecheck.

Enrico Tassi (May 17 2023 at 08:53):

Gaëtan Gilbert (May 17 2023 at 08:57):

so you would do Notation nat := nat_eqType (only printing).?
but then depending on imports it might print mathcomp.whatever.nat which sounds confusing (and not round trip since only printing)

On the technical side abbreviations are in the nametab and the nametab doesn't understand "only printing" so you would need to add that somehow. I don't know if it would be easy or a deeper redesign.

Enrico Tassi (May 17 2023 at 09:01):

Enrico Tassi (May 17 2023 at 09:02):

Abuot import, yes, but that is fine since if you don't import a file you also don't get the canonical instances which make the elaboration of nat to nat_eqType possible

Gaëtan Gilbert (May 17 2023 at 09:04):

printing an abbrev involves doing shortest_qualid_of in the nametab doesn't it?

Guillaume Melquiond (May 17 2023 at 09:06):

Was there a reason to not just reverse the canonical projections? That is, when printing a value that is registered in the table of canonical projections, just print the target. It seems straightforward but perhaps I am missing something.

Gaëtan Gilbert (May 17 2023 at 09:07):

Module M.
  Notation x := nat.
End M.

Check nat. (* nat *)

Import M.
Check nat. (* x *)

Definition x := bool.
Check nat. (* M.x *)

Enrico Tassi (May 17 2023 at 09:09):

@Gaëtan Gilbert I think I see, the nametab does not have a print-only thing. Could be added, but it is not there.
@Guillaume Melquiond I think you are right, it is more ad-hoc, but also simpler.

Enrico Tassi (May 17 2023 at 09:14):

@Guillaume Melquiond there is a caveat.
Take a record with 2 projections hence 2 values, eg Canonical foo_canonical := {| p1 := x; p2 := y |}.
Sometimes p2 is not flagged as a canonical projection, so there is a 1:1 correspondence between foo_canonical and x.
But we have to be careful not to print x if the user wrote y ;-)

Enrico Tassi (May 17 2023 at 09:16):

Guillaume Melquiond (May 17 2023 at 09:18):

Oh! I guess you meant the opposite, that is, both p1 and p2 were registered as canonical projections, so we don't know whether x or y should be displayed.

Gaëtan Gilbert (May 17 2023 at 09:20):

Enrico Tassi (May 17 2023 at 09:27):

@Gaëtan Gilbert yes.
Indeed, so this printing behavior should only be enabled if the record has exactly 1 canonical projection

Guillaume Melquiond (May 17 2023 at 09:29):

Shouldn't it then be "exactly 1 coercion that happens to be a canonical projection"?

Guillaume Melquiond (May 17 2023 at 09:29):

Pierre Roux (May 17 2023 at 10:00):

Indeed, whereas it is common to have multiple fields being canonical projections, it seems much less common for more than one to be a coercion?