I'm looking on bemused as the Visible `forall` aka RequiredTypeArguments proposal goes through GHC Committee discussion. I sympathise with Simon M's alarm at the namespacing effects needed. SPJ's attempt at softening the blow:

>                 f (List Int)
> or
>                 f (type [Int])
> but I think the alternative (of requiring the reader to know

> the type of the function in order to resolve the binding of names

> in its argument) is much, much worse.

If a `type` herald is supposed to emolliate me, I have Hugs accepting this:

Hugs> sizeOf (:: Int)

4

Hugs> typeOf (:: [Int])

TypeRep 3 ...

* `(:: t)` -- the parens are required -- is a lot less cluttered than Proxy;

* It's a little less cluttered than the proposed `type`;

* More importantly, it heralds much better to my eye 'here comes a type'.

I'm curious why so much of the proposal uses the `sizeOf` example. Its type currently is `Sized a => a -> Int`. It seems to me quite useful I can supply a term as argument -- I might well have in scope a (term) var of the required type.

I haven't needed to change the type of `sizeOf` for the Hugs heralded syntax. The syntax is sugar for `(termType :: Int)`, in which `termType` is in effect the same as `undefined`, but with a name more revealing for diagnostics.

Whereas the proposal won't actually help with `sizeOf`, until/unless the library changes its signature -- thereby breaking a load of code and dependencies. Or introduce a different-named function?

The other Motivation from the proposal is to fix an inconsistency with DataKinds. It seems to me there's another way to fix such an inconsistency: change the design for DataKinds -- which to me has always been a bit of a kludge.

There's also some interaction in the ugliness with `ScopedTypeVariables` -- which, with the benefit of hindsight, is increasingly getting regarded as a mis-feature. Hugs has always had the `PatternSignatures` feature, and indeed `FunctionSignatures`.

It seems to me that erasure/pi-types is an implementation detail that should be kept out of the surface syntax. If the programmer wants to signal that it's the type of a term that's of concern (such that the term can be erased as well as -- ultimately -- its type), annotate the terms' position in the signature (something like with strictness), rather than banjaxing familiar syntax. Behind the scenes translate to a pi-types implementation.

AntC