Overhaul -fprint-explicit-kinds to use VKA

This patch changes the behavior of `-fprint-explicit-kinds`
so that it displays kind argument using visible kind application.
In other words, the flag now:

1. Prints instantiations of specified variables with `@(...)`.
2. Prints instantiations of inferred variables with `@{...}`.

In addition, this patch removes the `Use -fprint-explicit-kinds to
see the kind arguments` error message that often arises when a type
mismatch occurs due to different kinds. Instead, whenever there is a
kind mismatch, we now enable the `-fprint-explicit-kinds` flag
locally to help cue to the programmer where the error lies.
(See `Note [Kind arguments in error messages]` in `TcErrors`.)
As a result, these funny `@{...}` things can now appear to the user
even without turning on the `-fprint-explicit-kinds` flag explicitly,
so I took the liberty of documenting them in the users' guide.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15871

Differential Revision: https://phabricator.haskell.org/D5314

4 files changed, 13 insertions, 15 deletions

diff --git a/testsuite/tests/ghci/scripts/GhciKinds.stdout b/testsuite/tests/ghci/scripts/GhciKinds.stdout
index 5431bbc17d..b00c8650e6 100644
--- a/testsuite/tests/ghci/scripts/GhciKinds.stdout
+++ b/testsuite/tests/ghci/scripts/GhciKinds.stdout
@@ -14,4 +14,4 @@ $(unboxedTupleT 2) :: forall (k0 :: RuntimeRep) (k1 :: RuntimeRep).
                       -> TYPE k1
                       -> TYPE
                            ('TupleRep
-                              ((':) RuntimeRep k0 ((':) RuntimeRep k1 ('[] RuntimeRep))))
+                              ((':) @RuntimeRep k0 ((':) @RuntimeRep k1 ('[] @RuntimeRep))))
diff --git a/testsuite/tests/ghci/scripts/T11376.stdout b/testsuite/tests/ghci/scripts/T11376.stdout
index c94516772c..01e749a22c 100644
--- a/testsuite/tests/ghci/scripts/T11376.stdout
+++ b/testsuite/tests/ghci/scripts/T11376.stdout
@@ -1,6 +1,6 @@
 bar @Int :: Int -> b -> Int
 bar @Int :: forall {b}. Int -> b -> Int
-prox :: forall {k} {a :: k}. Prox k a
-prox @Int :: Prox * Int
-Prox :: forall {k} {a :: k}. Prox k a
-Prox @Int :: Prox * Int
+prox :: forall {k} {a :: k}. Prox @{k} a
+prox @Int :: Prox @{*} Int
+Prox :: forall {k} {a :: k}. Prox @{k} a
+Prox @Int :: Prox @{*} Int
diff --git a/testsuite/tests/ghci/scripts/T15341.stdout b/testsuite/tests/ghci/scripts/T15341.stdout
index 1d29dc7f8f..0633ae5b39 100644
--- a/testsuite/tests/ghci/scripts/T15341.stdout
+++ b/testsuite/tests/ghci/scripts/T15341.stdout
@@ -1,6 +1,6 @@
 type family Foo (a :: k) :: k
   where Foo a = a
   	-- Defined at T15341.hs:5:1
-type family Foo k (a :: k) :: k
-  where Foo k a = a
+type family Foo @k (a :: k) :: k
+  where Foo @k a = a
   	-- Defined at T15341.hs:5:1
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index 6970eb3d7c..15e19cf105 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -40,33 +40,31 @@
 <interactive>:55:41: error:
     Type family equation violates injectivity annotation.
     Kind variable ‘k2’ cannot be inferred from the right-hand side.
-    Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
-      PolyKindVarsF '[] = '[] -- Defined at <interactive>:55:41
+      PolyKindVarsF @{[k2]} @[k1] ('[] @k2) = '[] @k1
+        -- Defined at <interactive>:55:41
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
     Kind variable ‘k1’ cannot be inferred from the right-hand side.
-    Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
-      PolyKindVars '[] = '[] -- Defined at <interactive>:60:15
+      PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
+        -- Defined at <interactive>:60:15
 
 <interactive>:64:15: error:
     Type family equation violates injectivity annotation.
     Kind variable ‘k’ cannot be inferred from the right-hand side.
-    Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       forall k (a :: k) (b :: k).
-        Fc a b = Int -- Defined at <interactive>:64:15
+        Fc @k a b = Int -- Defined at <interactive>:64:15
 
 <interactive>:68:15: error:
     Type family equation violates injectivity annotation.
     Type and kind variables ‘k’, ‘a’, ‘b’
     cannot be inferred from the right-hand side.
-    Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       forall k (a :: k) (b :: k).
-        Gc a b = Int -- Defined at <interactive>:68:15
+        Gc @k a b = Int -- Defined at <interactive>:68:15
 
 <interactive>:81:15: error:
     Type family equations violate injectivity annotation: