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.

5 files changed, 18 insertions, 10 deletions

diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr
index 0ec531c526..4c9097eacd 100644
--- a/testsuite/tests/gadt/T3169.stderr
+++ b/testsuite/tests/gadt/T3169.stderr
@@ -9,6 +9,9 @@ T3169.hs:13:22: error:
         Actual type: Map (a, b) elt
     • In the second argument of ‘lookup’, namely ‘m’
       In the expression: lookup a m :: Maybe (Map b elt)
+      In the expression:
+        case lookup a m :: Maybe (Map b elt) of {
+          Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
     • Relevant bindings include
         m :: Map (a, b) elt (bound at T3169.hs:12:17)
         b :: b (bound at T3169.hs:12:13)
diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index 829dfa0e2b..215426ed15 100644
--- a/testsuite/tests/gadt/gadt-escape1.stderr
+++ b/testsuite/tests/gadt/gadt-escape1.stderr
@@ -10,8 +10,10 @@ gadt-escape1.hs:19:58: error:
         the inferred type of weird1 :: r at gadt-escape1.hs:19:1
       Possible fix: add a type signature for ‘weird1’
       Expected type: r
-      Actual type: ExpGADT t
+        Actual type: ExpGADT t
     • In the expression: a
       In a case alternative: Hidden (ExpInt _) a -> a
+      In the expression:
+        case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }
     • Relevant bindings include
         weird1 :: r (bound at gadt-escape1.hs:19:1)
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index 44b100b059..57ee3fdc92 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -3,14 +3,15 @@ gadt13.hs:15:13: error:
     • Couldn't match expected type ‘r’
                   with actual type ‘String -> [Char]’
         ‘r’ is untouchable
-          inside the constraints: r1 ~ Int
+          inside the constraints: t ~ Int
           bound by a pattern with constructor: I :: Int -> Term Int,
                    in an equation for ‘shw’
           at gadt13.hs:15:6-8
       ‘r’ is a rigid type variable bound by
-        the inferred type of shw :: Term r1 -> r at gadt13.hs:15:1
+        the inferred type of shw :: Term t -> r at gadt13.hs:15:1
       Possible fix: add a type signature for ‘shw’
-    • In the expression: ("I " ++) . shows t
+    • Possible cause: ‘(.)’ is applied to too many arguments
+      In the expression: ("I " ++) . shows t
       In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
     • Relevant bindings include
-        shw :: Term r1 -> r (bound at gadt13.hs:15:1)
+        shw :: Term t -> r (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index 8720d7fe10..93b8c70c1f 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -13,6 +13,7 @@ gadt7.hs:16:38: error:
       Possible fix: add a type signature for ‘i1b’
     • In the expression: y1
       In a case alternative: K -> y1
+      In the expression: case t1 of { K -> y1 }
     • Relevant bindings include
         y1 :: r1 (bound at gadt7.hs:16:16)
         y :: r1 (bound at gadt7.hs:16:7)
diff --git a/testsuite/tests/gadt/rw.stderr b/testsuite/tests/gadt/rw.stderr
index 39529a7003..c79bb72b4c 100644
--- a/testsuite/tests/gadt/rw.stderr
+++ b/testsuite/tests/gadt/rw.stderr
@@ -13,16 +13,17 @@ rw.hs:14:47: error:
         v :: T a (bound at rw.hs:13:10)
         writeInt :: T a -> IORef a -> IO () (bound at rw.hs:13:1)
 
-rw.hs:19:51: error:
+rw.hs:19:43: error:
     • Couldn't match type ‘a’ with ‘Bool’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           readBool :: forall a. T a -> IORef a -> IO ()
         at rw.hs:16:12
-      Expected type: a -> Bool
-        Actual type: Bool -> Bool
-    • In the second argument of ‘(.)’, namely ‘not’
-      In the second argument of ‘(>>=)’, namely ‘(print . not)’
+      Expected type: a -> IO ()
+        Actual type: Bool -> IO ()
+    • In the second argument of ‘(>>=)’, namely ‘(print . not)’
+      In the expression: readIORef ref >>= (print . not)
+      In a case alternative: ~(Lb x) -> readIORef ref >>= (print . not)
     • Relevant bindings include
         ref :: IORef a (bound at rw.hs:17:12)
         v :: T a (bound at rw.hs:17:10)