Discussed some of this on Slack with Phil and Nathan. This is a way to make proxies easier to use without going full polykinds.

New type syntax for proxies. Proxy will no longed be a user-defined type, but rather a language construct.

<type> ::= 'Proxy' <type>
         | …

New expression syntax for proxy literals. This syntax comes from the recent GHC syntax for type arguments, however we prefer proxies so that the order of nested universal quantifiers stays insignificant.

<expr> ::= '@' <type>
         | …

Code generation of such expressions may just be {} or null or something. The values can't be inspected so it doesn't matter what their JS representation is.