Coq uses wrong notations using custom entries

[amblafont]

Description of the problem

Coq displays a goal using a notation defined in another custom entry (see the end of the code below).

Declare Custom Entry foo.
Declare Custom Entry bar.

Section example.

Context (A : Type).
Context (Q : A -> A -> A).
Context (P : A -> A).


Notation "< x >" := (P x) (x custom foo).
(* Should not be allowed in a foo expression *)
Notation "| x |" := (x) (x custom bar).

Notation "{ x }" := (x) (in custom foo, x constr).

(* If moving the above notation |-| here, the issue disappears
*)


Notation "x y" := (Q x y)  (in custom bar at level 1, right associativity).
Notation "x" := x (in custom bar at level 0, x global).

Check (fun a b => < {Q b a} >).
(*  returns fun (a : A) (b : B) => < | {b a} | > 
The | - | notation should not be used! And indeed it is not accepted as input, as seen below.
*)
Fail Check (fun a b =>  < | {b a} | >).
End example.

Coq Version

8.18.0

[herbelin]

Looks strange indeed. Maybe a bug in the computation of the transitive closure of "coercions" between entries. In any cases, thanks for reporting.

[herbelin]

The order of chaining of entry coercions (such as | x | or { x }) was indeed wrong when combining them by transitivity on one side. It was correct when applying transitivity on the other side and this is why the problem was only when | x | came before { x }.

Fixed in #18230 where it now prints fun a b => < {| b a |} > in both cases.

Thanks again!