only parsing notations should not disable the printing of other notations defined after them

[JasonGross]

Version

8.8.0 (present as far back as 8.5, though)

Description of the problem

Consider this code:

Inductive type := nat | bool.
Definition denote (t : type)
  := match t with
     | nat => Datatypes.nat
     | bool => Datatypes.bool
     end.
Ltac reify t :=
  lazymatch eval cbv beta in t with
  | Datatypes.nat => nat
  | Datatypes.bool => bool
  end.
Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing).
Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing).
Axiom Literal : forall {t}, denote t -> Type.
Delimit Scope foo_scope with foo.
Open Scope foo_scope.
Section A.
  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
  Check [1]. (* Literal 1 : Type *) (* as expected *)
  Notation "[ x ]" := (Literal x) : foo_scope.
  Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1] *)
  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
  Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1] *)
End A.
Section B.
  Notation "[ x ]" := (Literal x) : foo_scope.
  Check @Literal nat 1. (* [1] : Type *)
  Fail Check [1]. (* As expected: The command has indeed failed with message:
The term "1" has type "Datatypes.nat" while it is expected to have type
 "denote ?t". *)
  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
  Check [1]. (* Should succeed, but instead fails with: Error:
The term "1" has type "Datatypes.nat" while it is expected to have type
 "denote ?t". *)
End B.

There are two issues here:

1. Adding the only parsing notation makes the later printing-and-parsing notation not be used for printing, which is incorrect
2. Adding the only parsing notation after the printing-and-parsing notation does not update the parser, which is incorrect

My guess is that the notation system is incorrectly considering _ and ltac:(...) to be equal when deciding whether or not, and how, to overwrite a notation with another?

cc @herbelin

[herbelin]

My guess is that the notation system is incorrectly considering _ and ltac:(...) to be equal when deciding whether or not, and how, to overwrite a notation with another?

Your guess is right.

What to do is a bit unclear (comparing tactic code would be a bit difficult with locations, arbitrary generic arguments, ...). Maybe assuming that two tactics always differ by default, even if exactly the same)?

[herbelin]

Fixed by #12950 but the current semantics adopted in #12950 makes that redefining a notation in only-parsing mode cancels the whole of a previous combined parsing-printing notation, including its printing part.

In particular, this means displaying Literal 1 in the third and fifth example.