Program Fixpoint's measure conflicts with notations in where clause.

[h0nzZik]

Description of the problem

Coq does not accept a Program Fixpoint with measure and notation in where clause.

From Coq Require Import Program.

Reserved Notation "'bar' x" (at level 60).

(* works *)
(*
Fixpoint foo (n : nat) :=
  match n with
  | 0 => 0
  | S n' => S (bar n')
  end
where "'bar' x" := (foo x).
 *)

(* works *)
(*
Program Fixpoint goo (n : nat) :=
  match n with
  | 0 => 0
  | S n' => S (bar n')
  end
where "'bar' x" := (goo x).
*)

(* Works *)
(*
Program Fixpoint goo (n : nat) {struct n} :=
  match n with
  | 0 => 0
  | S n' => S (bar n')
  end
where "'bar' x" := (goo x).
*)


(* Does not work. `Error: Unknown interpretation for notation "bar _".`
 *)
Program Fixpoint goo (n : nat) {measure n} :=
  match n with
  | 0 => 0
  | S n' => S (bar n')
  end
where "'bar' x" := (goo x).

Coq Version

tested on version 8.13.2 and current master branch (bdb72aa)

[herbelin]

Will be fixed by #18834. Thanks for the report.