Mixing notations and tactics makes Coq report errors in the wrong file

[Mbodin]

Description of the problem

It took me a while to understand what was happening.
Here is a self-contained example:

Notation "'test' x" :=
  (ltac:(exact x))
  (at level 50, no associativity, only parsing).

Definition t :=
  test something_undefined.

This code is rejected by Coq (and meant to be: something_undefined is not defined).
My issue is about the error message, and in particular the place where the error is displayed: Coq complains with Error: The reference x was not found in the current environment., pointing to the definition of the notation ((ltac:(exact x))), instead of its usage (test something_undefined).

Coq even does this if the notation is defined in a separate file, which makes the error very difficult to understand and/or work with.
In my usage case, the notation was defined in a first file that compiled fine, but was erroneously used in a second file… but the error reported on the first file (that actually compiled fine). This made me check the first file instead of the erroneously usage (of which I couldn’t easily know the line).

Coq Version

$ coqtop -v
The Coq Proof Assistant, version 8.13.0 (September 2021)
compiled on Sep 8 2021 9:03:15 with OCaml 4.13.0~beta1