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.

8 files changed, 37 insertions, 14 deletions

diff --git a/testsuite/tests/polykinds/T10503.stderr b/testsuite/tests/polykinds/T10503.stderr
index 7c39c41738..141f16fc6e 100644
--- a/testsuite/tests/polykinds/T10503.stderr
+++ b/testsuite/tests/polykinds/T10503.stderr
@@ -9,8 +9,6 @@ T10503.hs:8:6: error:
         the type signature for:
           h :: forall k r. ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
         at T10503.hs:8:6
-      Expected type: ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
-        Actual type: ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
     • In the ambiguity check for ‘h’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
diff --git a/testsuite/tests/polykinds/T6068.stdout b/testsuite/tests/polykinds/T6068.stdout
index e096418727..f0fe7de899 100644
--- a/testsuite/tests/polykinds/T6068.stdout
+++ b/testsuite/tests/polykinds/T6068.stdout
@@ -1 +1 @@
-exists Nothing :: Floop a mp => Existential mp

+exists Nothing :: Floop a mp => Existential mp
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index 539d15d406..46b7181840 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -2,18 +2,18 @@
 T7438.hs:6:14: error:
     • Couldn't match expected type ‘r1’ with actual type ‘r’
         ‘r1’ is untouchable
-          inside the constraints: r3 ~ r2
+          inside the constraints: t1 ~ t
           bound by a pattern with constructor:
                      Nil :: forall k (a :: k). Thrist a a,
                    in an equation for ‘go’
           at T7438.hs:6:4-6
       ‘r1’ is a rigid type variable bound by
-        the inferred type of go :: Thrist r2 r3 -> r -> r1 at T7438.hs:6:1
+        the inferred type of go :: Thrist t t1 -> r -> r1 at T7438.hs:6:1
       ‘r’ is a rigid type variable bound by
-        the inferred type of go :: Thrist r2 r3 -> r -> r1 at T7438.hs:6:1
+        the inferred type of go :: Thrist t t1 -> r -> r1 at T7438.hs:6:1
       Possible fix: add a type signature for ‘go’
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
     • Relevant bindings include
         acc :: r (bound at T7438.hs:6:8)
-        go :: Thrist r2 r3 -> r -> r1 (bound at T7438.hs:6:1)
+        go :: Thrist t t1 -> r -> r1 (bound at T7438.hs:6:1)
diff --git a/testsuite/tests/polykinds/T7594.stderr b/testsuite/tests/polykinds/T7594.stderr
index 2f1844ecdb..be2acfebe0 100644
--- a/testsuite/tests/polykinds/T7594.stderr
+++ b/testsuite/tests/polykinds/T7594.stderr
@@ -13,4 +13,5 @@ T7594.hs:35:12: error:
         Actual type: a -> IO ()
     • In the first argument of ‘app’, namely ‘print’
       In the expression: app print q2
+      In an equation for ‘bar2’: bar2 = app print q2
     • Relevant bindings include bar2 :: b (bound at T7594.hs:35:1)
diff --git a/testsuite/tests/polykinds/T9144.stderr b/testsuite/tests/polykinds/T9144.stderr
index f2c65530ee..b62d1f175d 100644
--- a/testsuite/tests/polykinds/T9144.stderr
+++ b/testsuite/tests/polykinds/T9144.stderr
@@ -1,7 +1,9 @@
-

-T9144.hs:34:26:

-    Couldn't match type ‘Integer’ with ‘FooTerm’

-    Expected type: DemoteRep 'KProxy

-      Actual type: DemoteRep 'KProxy

-    In the first argument of ‘toSing’, namely ‘n’

-    In the expression: toSing n

+
+T9144.hs:34:26: error:
+    • Couldn't match type ‘Integer’ with ‘FooTerm’
+      Expected type: DemoteRep 'KProxy
+        Actual type: DemoteRep 'KProxy
+    • In the first argument of ‘toSing’, namely ‘n’
+      In the expression: toSing n
+      In the expression:
+        case toSing n of { SomeSing n' -> SomeSing (SBar n') }
diff --git a/testsuite/tests/polykinds/TidyClassKinds.hs b/testsuite/tests/polykinds/TidyClassKinds.hs
new file mode 100644
index 0000000000..83f6eaaea2
--- /dev/null
+++ b/testsuite/tests/polykinds/TidyClassKinds.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MultiParamTypeClasses, PolyKinds #-}
+{-# OPTIONS_GHC -fprint-explicit-kinds #-}
+
+module TidyClassKinds where
+
+import Data.Proxy
+
+class Poly a b
+
+type ProxySyn = Proxy
+
+instance Poly ProxySyn ProxySyn
+  -- output should really talk about k1 and k2, not about k and k!
diff --git a/testsuite/tests/polykinds/TidyClassKinds.stderr b/testsuite/tests/polykinds/TidyClassKinds.stderr
new file mode 100644
index 0000000000..69ca49c188
--- /dev/null
+++ b/testsuite/tests/polykinds/TidyClassKinds.stderr
@@ -0,0 +1,8 @@
+
+TidyClassKinds.hs:12:10: error:
+    • Illegal instance declaration for
+        ‘Poly (k1 -> *) (k1 -> *) (ProxySyn k1) (ProxySyn k1)’
+        (All instance types must be of the form (T t1 ... tn)
+         where T is not a synonym.
+         Use TypeSynonymInstances if you want to disable this.)
+    • In the instance declaration for ‘Poly ProxySyn ProxySyn’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 6387d1790d..5a8a9043ab 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -127,6 +127,7 @@ test('T11142', normal, compile_fail, [''])
 test('SigTvKinds', normal, compile, [''])
 test('SigTvKinds2', expect_broken(11203), compile_fail, [''])
 test('T9017', normal, compile_fail, [''])
+test('TidyClassKinds', normal, compile_fail, ['-fprint-explicit-kinds'])
 test('T11249', normal, compile, [''])
 test('T11248', normal, compile, [''])
 test('T11278', normal, compile, [''])