`Set Printing Projections` should not print implicit arguments

[samuelgruetter]

Module wordmodule.
  Class word := {
    rep: Type;
    add: rep -> rep -> rep;
  }.
End wordmodule.
Notation word := wordmodule.word.
Coercion wordmodule.rep : word >-> Sortclass.

Section Test.
  Context {int: wordmodule.word}.

  Record Machine := {
    getPc: int;
  }.

  Definition P: Prop :=
    forall (m: Machine) (w1 w2 w3: int),
    wordmodule.add w1 w2 = w3 ->
    m.(getPc) = w3.

  About wordmodule.add.

wordmodule.add : forall word : word, word -> word -> word

Argument word is implicit and maximally inserted
wordmodule.add is transparent
Expands to: Constant Top.wordmodule.add

  Print P. 

prints, as desired:

P = forall (m : Machine) (w1 w2 w3 : int), wordmodule.add w1 w2 = w3 -> getPc m = w3
     : Prop

But:

  Set Printing Projections.
  Print P.

Bug: this prints the implicit argument int:

P = forall (m : Machine) (w1 w2 w3 : int), int.(@wordmodule.add) w1 w2 = w3 -> m.(getPc) = w3
     : Prop

Desired output:

P = forall (m : Machine) (w1 w2 w3 : int), wordmodule.add w1 w2 = w3 -> m.(getPc) = w3
     : Prop

Coq Version: 8.9.0

[samuelgruetter]

If Set Printing Projections. is on, this bug makes goals in bedrock2 so unreadable that it's not worth using Set Printing Projections., so even though https://github.com/coq/coq/issues/6257 has been fixed, we still can't use Set Printing Projections.. Not the biggest problem but a bit unfortunate :wink:

[SkySkimmer]

This would mean we have to use the projection compatibility constants when the projection's principal argument is implicit. Considering we want to move away from the compatibility constants, I'd like to avoid adding a behaviour that relies on them. OTOH I don't know how else we could get you nice goal printing. What would this even look like in a Coq without the compatibility layer? I guess you could define Notation add x y := _.(add) x y. immediately after defining the record (assuming projections live in a separate namespace from everything else, otherwise you'd get a collision). That seems heavy compared to implicits though.

WDYT @ppedrot @mattam82 ?

[samuelgruetter]

There might be some complexities I'm not aware of, but why is it not as simple as this pseudo code?

prettyPrint (App t1 t2) = 
   if t1 is a projection and its first argument is not implicit then
      use projection notation
   else
      don't use projection notation

[tchajed]

More specifically Set Printing Projections is happy to print class instances, which doesn't make much sense to me. Would it be easier to avoid the projection printing when the principal argument's type is a class, and not generally when it's implicit? (My actual use case is identical to Sam's above, with the same word library, but in Perennial rather than bedrock2.)

Here's a simple example:

Class ToNat T :=
  { to_nat (x:T) : nat; }.

Instance unit_to_nat_instance : ToNat unit :=
  { to_nat _ := 0; }.

Check (to_nat tt).
Set Printing Projections.
Check (to_nat tt).
(*
unit_to_nat_instance.(to_nat) tt
     : nat
*)