Implicit arguments are not printed in match ... in

[ali-ghanbari]

Description of the problem

When I run the following commands.

Set Printing All.
Print eq_sym.

I get the following type-correct and valid definition.

eq_sym =
fun (A : Type) (x y : A) (H : @eq A x y) =>
match H in (eq _ a) return (@eq A a x) with
| eq_refl => @eq_refl A x
end
     : forall (A : Type) (x y : A) (_ : @eq A x y), @eq A y x

Unfortunately, despite the fact that I had instructed Coq to print implicit arguments, it used implicit arguments in the subexpression (eq _ a). I would expect to see the following definition, which is also valid and equivalent to the definition above.

eq_sym =
fun (A : Type) (x y : A) (H : @eq A x y) =>
match H in (@eq _ _ a) return (@eq A a x) with
| @eq_refl _ _ => @eq_refl A x
end
:  forall (A : Type) (x y : A) (_ : @eq A x y), @eq A y x

I did this test with both Coqtop and CoqIDE (by turning on the Display Implicit Arguments option), they both give the same results.
I might be missing something or this might be just a bug in the printing facility of Coq.

Coq Version

8.17.1 on MacOSX 14.0

[SkySkimmer]

This needs to check the printing options

coq/interp/constrextern.ml

Line 520 in 49fce3a

match drop_implicits_in_patt (GlobRef.IndRef ind) 0 args with

[herbelin]

@SkySkimmer: are you on? (Otherwise I'll propose something.)

[JasonGross]

Does the expanded version work regardless of the Set Asymmetric Patterns setting? If not, that setting should also be checked so that printing is reversible

[herbelin]

Does the expanded version work regardless of the Set Asymmetric Patterns setting?

Yes, when using a @...

If not, that setting should also be checked so that printing is reversible

... but indeed, it should be checked that @ is used when Print All and Asymmetric Patterns are both on.

Made #18176.