Visible type application

This re-working of the typechecker algorithm is based on
the paper "Visible type application", by Richard Eisenberg,
Stephanie Weirich, and Hamidhasan Ahmed, to be published at
ESOP'16.

This patch introduces -XTypeApplications, which allows users
to say, for example `id @Int`, which has type `Int -> Int`. See
the changes to the user manual for details.

This patch addresses tickets #10619, #5296, #10589.

2 files changed, 55 insertions, 2 deletions

diff --git a/compiler/parser/Lexer.x b/compiler/parser/Lexer.x
index cee8540c09..1bbbfbf20f 100644
--- a/compiler/parser/Lexer.x
+++ b/compiler/parser/Lexer.x
@@ -394,6 +394,14 @@ $tab          { warnTab }
                      { lex_qquasiquote_tok }
 }
 
+  -- See Note [Lexing type applications]
+<0> {
+    [^ $idchar \) ] ^
+  "@"
+    / { ifExtension typeApplicationEnabled `alexAndPred` notFollowedBySymbol }
+    { token ITtypeApp }
+}
+
 <0> {
   "(|" / { ifExtension arrowsEnabled `alexAndPred` notFollowedBySymbol }
                                         { special IToparenbar }
@@ -507,6 +515,32 @@ $tab          { warnTab }
   \"                            { lex_string_tok }
 }
 
+-- Note [Lexing type applications]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- The desired syntax for type applications is to prefix the type application
+-- with '@', like this:
+--
+--   foo @Int @Bool baz bum
+--
+-- This, of course, conflicts with as-patterns. The conflict arises because
+-- expressions and patterns use the same parser, and also because we want
+-- to allow type patterns within expression patterns.
+--
+-- Disambiguation is accomplished by requiring *something* to appear betwen
+-- type application and the preceding token. This something must end with
+-- a character that cannot be the end of the variable bound in an as-pattern.
+-- Currently (June 2015), this means that the something cannot end with a
+-- $idchar or a close-paren. (The close-paren is necessary if the as-bound
+-- identifier is symbolic.)
+--
+-- Note that looking for whitespace before the '@' is insufficient, because
+-- of this pathological case:
+--
+--   foo {- hi -}@Int
+--
+-- This design is predicated on the fact that as-patterns are generally
+-- whitespace-free, and also that this whole thing is opt-in, with the
+-- TypeApplications extension.
 
 -- -----------------------------------------------------------------------------
 -- Alex "Haskell code fragment bottom"
@@ -686,8 +720,13 @@ data Token
   | ITLarrowtail IsUnicodeSyntax --  -<<
   | ITRarrowtail IsUnicodeSyntax --  >>-
 
-  | ITunknown String             -- Used when the lexer can't make sense of it
-  | ITeof                        -- end of file token
+  -- type application '@' (lexed differently than as-pattern '@',
+  -- due to checking for preceding whitespace)
+  | ITtypeApp
+
+
+  | ITunknown String            -- Used when the lexer can't make sense of it
+  | ITeof                       -- end of file token
 
   -- Documentation annotations
   | ITdocCommentNext  String     -- something beginning '-- |'
@@ -2023,6 +2062,7 @@ data ExtBits
   | LambdaCaseBit
   | BinaryLiteralsBit
   | NegativeLiteralsBit
+  | TypeApplicationsBit
   deriving Enum
 
 
@@ -2083,6 +2123,8 @@ negativeLiteralsEnabled :: ExtsBitmap -> Bool
 negativeLiteralsEnabled = xtest NegativeLiteralsBit
 patternSynonymsEnabled :: ExtsBitmap -> Bool
 patternSynonymsEnabled = xtest PatternSynonymsBit
+typeApplicationEnabled :: ExtsBitmap -> Bool
+typeApplicationEnabled = xtest TypeApplicationsBit
 
 -- PState for parsing options pragmas
 --
@@ -2153,6 +2195,8 @@ mkPState flags buf loc =
                .|. BinaryLiteralsBit           `setBitIf` xopt LangExt.BinaryLiterals           flags
                .|. NegativeLiteralsBit         `setBitIf` xopt LangExt.NegativeLiterals         flags
                .|. PatternSynonymsBit          `setBitIf` xopt LangExt.PatternSynonyms          flags
+               .|. TypeApplicationsBit         `setBitIf` xopt LangExt.TypeApplications         flags
+
       --
       setBitIf :: ExtBits -> Bool -> ExtsBitmap
       b `setBitIf` cond | cond      = xbit b
diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y
index ead81ac337..11dc84f0a6 100644
--- a/compiler/parser/Parser.y
+++ b/compiler/parser/Parser.y
@@ -414,6 +414,7 @@ output it generates.
  '-<<'          { L _ (ITLarrowtail _) }            -- for arrow notation
  '>>-'          { L _ (ITRarrowtail _) }            -- for arrow notation
  '.'            { L _ ITdot }
+ TYPEAPP        { L _ ITtypeApp }
 
  '{'            { L _ ITocurly }                        -- special symbols
  '}'            { L _ ITccurly }
@@ -2237,7 +2238,11 @@ fexp    :: { LHsExpr RdrName }
 
 aexp    :: { LHsExpr RdrName }
         : qvar '@' aexp         {% ams (sLL $1 $> $ EAsPat $1 $3) [mj AnnAt $2] }
+            -- If you change the parsing, make sure to understand
+            -- Note [Lexing type applications] in Lexer.x
+
         | '~' aexp              {% ams (sLL $1 $> $ ELazyPat $2) [mj AnnTilde $1] }
+        | TYPEAPP atype         {% ams (sLL $1 $> $ HsType (mkHsWildCardBndrs $2)) [mj AnnAt $1] }
         | aexp1                 { $1 }
 
 aexp1   :: { LHsExpr RdrName }
@@ -2954,6 +2959,10 @@ var     :: { Located RdrName }
         | '(' varsym ')'        {% ams (sLL $1 $> (unLoc $2))
                                        [mop $1,mj AnnVal $2,mcp $3] }
 
+ -- Lexing type applications depends subtly on what characters can possibly
+ -- end a qvar. Currently (June 2015), only $idchars and ")" can end a qvar.
+ -- If you're changing this, please see Note [Lexing type applications] in
+ -- Lexer.x.
 qvar    :: { Located RdrName }
         : qvarid                { $1 }
         | '(' varsym ')'        {% ams (sLL $1 $> (unLoc $2))