But I wanted to point out that there are really two, interlocked, yet distinct, parts in this proposal.
1. Having a `forall a ->` construct for types of terms
2. How is `f blah` parsed if `f` has type `forall a -> …`?
I am definitely sympathetic to (1). As much as I like my `f @…`s I am bound to admit that it produces error messages from the 7th Circle of Hell. And, since it's a very useful pattern, making it "official" is rather neat a plan on paper.
But (2) is very very difficult, because we have really two grammars at play here: the grammar for term, and the grammar for types (I'll conflate grammar and name resolution in the following). In the `f @…` style, we switch to the type grammar to parse whatever's in the `@`. But if we want to to write type applications in the `forall a->` case as `f a`, then we sort of have to parse `a` as a term (though there is some leeway in name resolution). And that introduces all sorts of potentially weird behaviour (see the link above for a good documentation of what). Part of the difficulty, I should stress, is that, in types the apostrophe `'` means: I'm speaking of a data constructor, not a type constructor. Whereas in terms, it means: I'm opening a Template Haskell slice.
Part of the impetus for the proposal actually going in the direction of parsing the type argument as a term, is the desire to eventually merge the terms and types grammars. I don't know how widespread this desire actually is (maybe this is something we should speak about). In my personal opinion, it's not a very plausibly achievable goal, nor is it particularly necessary for dependent types. (It does, of course, have a number of advantages, which is why Coq, Agda, and Idris do have a single grammar indeed).
I think that I'd be happier if we had a sigil to switch between the type grammar and the term grammar. But, here, the issue is that nice sigils are harder and harder to come by.
My point, though, is that while this proposal may look like it has a small scope, it actually is a fairly large and intricate proposal, and requires quite a bit of attention.
/Arnaud