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, 94 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
new file mode 100644
index 0000000000..313d174b74
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -0,0 +1,94 @@
+
+VtaFail.hs:7:16: error:
+    • Cannot not apply expression of type ‘t1 -> t0 -> (t1, t0)’
+      to a visible type argument ‘Int’
+    • In the expression: pairup_nosig @Int @Bool 5 True
+      In an equation for ‘answer_nosig’:
+          answer_nosig = pairup_nosig @Int @Bool 5 True
+
+VtaFail.hs:12:26: error:
+    • No instance for (Num Bool) arising from a use of ‘addOne’
+    • In the expression: addOne @Bool 5
+      In an equation for ‘answer_constraint_fail’:
+          answer_constraint_fail = addOne @Bool 5
+
+VtaFail.hs:14:17: error:
+    • Cannot not apply expression of type ‘r0 -> r0’
+      to a visible type argument ‘Int’
+    • In the expression: (\ x -> x) @Int 12
+      In an equation for ‘answer_lambda’:
+          answer_lambda = (\ x -> x) @Int 12
+
+VtaFail.hs:19:5: error:
+    • Cannot not apply expression of type ‘Int -> (a0, Int)’
+      to a visible type argument ‘Bool’
+    • In the expression: pair 3 @Int @Bool True
+      In an equation for ‘a’: a = pair 3 @Int @Bool True
+
+VtaFail.hs:26:15: error:
+    • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
+    • In the type ‘Int’
+      In the expression: first @Int F
+      In an equation for ‘fInt’: fInt = first @Int F
+
+VtaFail.hs:33:18: error:
+    • Couldn't match type ‘Int’ with ‘Bool’
+      Expected type: Proxy Bool
+        Actual type: Proxy Int
+    • In the second argument of ‘foo’, namely ‘(P :: Proxy Int)’
+      In the expression: foo @Bool (P :: Proxy Int)
+      In an equation for ‘baz’: baz = foo @Bool (P :: Proxy Int)
+
+VtaFail.hs:40:17: error:
+    • Expected kind ‘* -> k0 -> *’, but ‘Maybe’ has kind ‘* -> *’
+    • In the type ‘Maybe’
+      In the expression: too @Maybe T
+      In an equation for ‘threeBad’: threeBad = too @Maybe T
+
+VtaFail.hs:41:27: error:
+    • Couldn't match type ‘Either’ with ‘(->)’
+      Expected type: Three (->)
+        Actual type: Three Either
+    • In the second argument of ‘too’, namely ‘(T :: Three Either)’
+      In the expression: too @(->) (T :: Three Either)
+      In an equation for ‘threeWorse’:
+          threeWorse = too @(->) (T :: Three Either)
+
+VtaFail.hs:46:5: error:
+    • Cannot not apply expression of type ‘Int -> Int -> Int’
+      to a visible type argument ‘Int’
+    • In the expression: plus @Int 5 7
+      In an equation for ‘b’: b = plus @Int 5 7
+
+VtaFail.hs:47:5: error:
+    • Cannot not apply expression of type ‘Int -> Int -> Int’
+      to a visible type argument ‘Rational’
+    • In the expression: plus @Rational 5 10
+      In an equation for ‘c’: c = plus @Rational 5 10
+
+VtaFail.hs:48:5: error:
+    • Cannot not apply expression of type ‘Int -> Int -> Int’
+      to a visible type argument ‘Int’
+    • In the expression: (+) @Int @Int @Int 12 14
+      In an equation for ‘d’: d = (+) @Int @Int @Int 12 14
+
+VtaFail.hs:51:5: error:
+    • Cannot not apply expression of type ‘Int -> String’
+      to a visible type argument ‘Float’
+    • In the expression: show @Int @Float (read "5")
+      In an equation for ‘e’: e = show @Int @Float (read "5")
+
+VtaFail.hs:52:11: error:
+    • Cannot not apply expression of type ‘String -> Int’
+      to a visible type argument ‘Bool’
+    • In the first argument of ‘show’, namely
+        ‘(read @Int @Bool @Float "3")’
+      In the expression: show (read @Int @Bool @Float "3")
+      In an equation for ‘f’: f = show (read @Int @Bool @Float "3")
+
+VtaFail.hs:57:12: error:
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the type ‘Maybe’
+      In the expression: silly @Maybe
+      In an equation for ‘g’: g = silly @Maybe