There should be a way to specify both sorts of scope stacks for both notations and Arguments

[JasonGross]

Description of the problem

Consider:

Declare Scope foo_scope.
Delimit Scope foo_scope with foo.
Notation "'FOO'" := tt : foo_scope.
Arguments id {_} _%foo.
Notation "'id2' x" := x%foo (at level 10, only parsing).
Check id FOO. (* id FOO : unit *)
Fail Check id (fun x : unit => FOO). (* Error: Unknown interpretation for notation "FOO". *)
Check id2 FOO. (* FOO%foo : unit *)
Check id2 (fun x : unit => FOO). (* fun _ : unit => FOO%foo : unit -> unit *)

As far as I know, there's no way to get the Arguments-sort of behavior for Notation, and no way to get the Notation-sort of behavior for Arguments.

cc @herbelin , who I believe had a plan for implementing this?

See also #3990 (where I reported my initial confusion about this)

Coq Version

8.11.1

[herbelin]

See #9123. This was stalled by lack of a good transition strategy. Maybe worth to reconsider it again though. It also comes to the surface back again in #11762.