Notation with binders *and* overall type annotation (like `fix`)

Using Coq
1

How do I define notation that behaves like Coq’s fix in that the following lines parse successfully?

Check myfix f n : nat := S n.
Check myfix f (n : nat) : nat := S n.

I cannot find a Notation invocation that allows binders and correctly parses the overall type annotation. Here is a template to play around with. (I tried closed binders to see if they would play better with the : part of the notation.)

Notation "'myfix' f x .. y : T := b" := 
  (fun f => fun x => .. (fun y => b : T) ..) 
  (at level 0, x closed binder, y closed binder).
2

Not completely satisfactory, but it seems to work by replacing : with something else to avoid the conflict, and marking f as an ident:

Notation "'myfix' f x .. y '::' T ':=' b" := 
  (fun x => .. (fun y => b : T) ..) 
  (at level 0, f ident, x binder, y binder, right associativity).
3

This must be the best option then. I couldn’t find anything else. Thank you!