Unless I'm missing something, all the examples in that PEP are first-order. There's no discussion of what the semantics is in the higher-order case. Pyret's annotations are perfectly well-defined and draw on a long history of research of getting these very subtle cases right (starting with Findler and Felleisen's ICFP 2002 paper). There's much more to this than just syntax.
PEP 3107 introduced function annotations to Python 3. The following syntax is valid:
Nothing is done with annotations by default. Here's an article discussing this "unused feature": http://ceronman.com/2013/03/12/a-powerful-unused-feature-of-...