Question: importing twice breaks notation

[alxest]

Importing ITree twice breaks the monadic notation (_ <- _ ;; _). Surprisingly, re-importing ITreeNotations does not fix the problem. Below is the minimal code. (Checked with Coq 8.12.2 / itree 3.2.0)

From ITree Require Import ITree.
(* Check (x <- Ret 0;; Ret x). *)     (** no parsing, no printing **)
Import ITreeNotations.
Check (x <- Ret 0;; Ret x).           (** parsing ok, printing ok **)
From ITree Require Import ITree.
Check (x <- Ret 0;; Ret x).           (** parsing ok, no printing **)
Import ITreeNotations.
Check (x <- Ret 0;; Ret x).           (** parsing ok, no printing **)

It is not an issue in my development, but I just wanted to report it and possibly understand why it happens.

[Lysxia]

That's odd. This seems to have been fixed in Coq 8.13.

Coq 8.13 output:

x <- Ret 0;; Ret x
     : itree ?E nat
where
?E : [ |- Type -> Type]
x <- Ret 0;; Ret x
     : itree ?E nat
where
?E : [ |- Type -> Type]
x <- Ret 0;; Ret x
     : itree ?E nat
where
?E : [ |- Type -> Type]

Coq 8.12 output:

x <- Ret 0;; Ret x
     : itree ?E nat
where
?E : [ |- Type -> Type]
ITree.bind (Ret 0) (fun x : nat => Ret x)
     : itree ?E nat
where
?E : [ |- Type -> Type]
ITree.bind (Ret 0) (fun x : nat => Ret x)
     : itree ?E nat
where
?E : [ |- Type -> Type]

[Lysxia]

The changelog of Coq 8.13 mentions some relevant updates in notations, in particular this one (though I don't really get the details):

Changed: Redeclaring a notation also reactivates its printing rule; in particular a second Import of the same module reactivates the printing rules declared in this module.

So this seems likely to have been fixed.

[alxest]

Thanks for your answer, @Lysxia ! I should update to 8.13. I will close the issue because it is already fixed and future users will not be relevant to this problem.