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.

1 files changed, 30 insertions, 26 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index 8a267d7bd0..0df2b3cf83 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -1,28 +1,32 @@
 
-T8518.hs:14:18:
-    Couldn't match expected type ‘Maybe (F c)’ with actual type ‘F c’
-    In the expression: rpt (4 :: Int) c z b
-    In an equation for ‘callCont’:
-        callCont c z b
-          = rpt (4 :: Int) c z b
-          where
-              rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
-              rpt i c' z' b' = let ... in rpt (i - 1) c''
-    Relevant bindings include
-      b :: B c (bound at T8518.hs:14:14)
-      z :: Z c (bound at T8518.hs:14:12)
-      c :: c (bound at T8518.hs:14:10)
-      callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
+T8518.hs:14:18: error:
+    • Couldn't match expected type ‘Maybe (F c)’ with actual type ‘F c’
+    • In the expression: rpt (4 :: Int) c z b
+      In an equation for ‘callCont’:
+          callCont c z b
+            = rpt (4 :: Int) c z b
+            where
+                rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
+                rpt i c' z' b' = let ... in rpt (i - 1) c''
+    • Relevant bindings include
+        b :: B c (bound at T8518.hs:14:14)
+        z :: Z c (bound at T8518.hs:14:12)
+        c :: c (bound at T8518.hs:14:10)
+        callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
 
-T8518.hs:17:78:
-    Couldn't match expected type ‘F a1’
-                with actual type ‘Z a1 -> B a1 -> F a1’
-    In the expression: rpt (i - 1) c''
-    In the expression:
-      let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i - 1) c''
-    Relevant bindings include
-      c'' :: a1 (bound at T8518.hs:17:30)
-      b' :: B a1 (bound at T8518.hs:17:21)
-      z' :: Z a1 (bound at T8518.hs:17:18)
-      c' :: a1 (bound at T8518.hs:17:15)
-      rpt :: a -> a1 -> Z a1 -> B a1 -> F a1 (bound at T8518.hs:16:9)
+T8518.hs:17:78: error:
+    • Couldn't match expected type ‘F a’
+                  with actual type ‘Z a -> B a -> F a’
+    • In the expression: rpt (i - 1) c''
+      In the expression:
+        let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i - 1) c''
+      In an equation for ‘rpt’:
+          rpt i c' z' b'
+            = let c'' = fromJust (snd <$> (continue c' z' b'))
+              in rpt (i - 1) c''
+    • Relevant bindings include
+        c'' :: a (bound at T8518.hs:17:30)
+        b' :: B a (bound at T8518.hs:17:21)
+        z' :: Z a (bound at T8518.hs:17:18)
+        c' :: a (bound at T8518.hs:17:15)
+        rpt :: a1 -> a -> Z a -> B a -> F a (bound at T8518.hs:16:9)