Add extension for type application

In http://www.haskell.org/pipermail/libraries/2010-October/014761.html we discussed adding an extension for explicit type application.

The main stumbling block is syntax.

For example, we would like to be able to write something to the effect of

(Just @ Char) 'a'

and also to be able to pattern match types, e.g.

f ((Just @ t) x) = (Right @ String @ t) x

For a more useful example:

data T where
    MkT :: forall a. a -> (a -> Int) -> T

f (MkT @ a x g) = g (x::a)

Possible suggested syntaxes to make something of type

Maybe (forall a. a->a)

were:

Just @ (forall a. a->a) id    (@ has another meaning in patterns)
Just[forall a. a->a] id       (pvs, opal, HasCASL with paramterized modules; conflicts with Haskell list syntax)
Just {forall a. a->a} id      (Agda)
#Just (forall a. a->a) id
@Just (forall a. a->a) id     (coq)

In the last 2 cases we would presumably have something like

Just :: forall a . a -> Maybe a
Just :: Char -> Maybe Char
#Just :: /\ a . a -> Maybe a
#Just Char :: Char -> Maybe Char

and similarly

#map :: /\ a b . (a -> b) -> [a] -> [b]

Trac metadata

Trac field	Value
Version	6.12.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture