[GHC] #4466: Add extension for type application

[GHC]

#4466: Add extension for type application
---------------------------------+------------------------------------------
    Reporter:  igloo             |        Owner:              
        Type:  feature request   |       Status:  new         
    Priority:  normal            |    Milestone:              
   Component:  Compiler          |      Version:  6.12.3      
    Keywords:                    |     Testcase:              
   Blockedby:                    |   Difficulty:              
          Os:  Unknown/Multiple  |     Blocking:              
Architecture:  Unknown/Multiple  |      Failure:  None/Unknown
---------------------------------+------------------------------------------
 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]
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4466>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler