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, 5 insertions, 7 deletions

diff --git a/testsuite/tests/polykinds/T10570.stderr b/testsuite/tests/polykinds/T10570.stderr
index 3c91db5cfb..568d6b298c 100644
--- a/testsuite/tests/polykinds/T10570.stderr
+++ b/testsuite/tests/polykinds/T10570.stderr
@@ -3,7 +3,6 @@ T10570.hs:10:10: error:
     • Illegal instance declaration for ‘ConsByIdx2 Int a Proxy cls’
         The coverage condition fails in class ‘ConsByIdx2’
           for functional dependency: ‘x -> m’
-        Reason: lhs type ‘Int’ does not determine rhs type ‘Proxy’
+        Reason: lhs type ‘Int’ does not determine rhs type ‘Proxy @{k}’
         Un-determined variable: k
-        Use -fprint-explicit-kinds to see the kind arguments
     • In the instance declaration for ‘ConsByIdx2 Int a Proxy cls’
diff --git a/testsuite/tests/polykinds/T14520.stderr b/testsuite/tests/polykinds/T14520.stderr
index 9c290ff4a5..cc7619d39b 100644
--- a/testsuite/tests/polykinds/T14520.stderr
+++ b/testsuite/tests/polykinds/T14520.stderr
@@ -1,6 +1,6 @@
 
 T14520.hs:15:24: error:
     • Expected kind ‘bat w w’,
-        but ‘Id’ has kind ‘XXX a0 * (XXX a0 (a0 ~>> *) kat0 b0) b0’
+        but ‘Id’ has kind ‘XXX @a0 @* (XXX @a0 @(a0 ~>> *) kat0 b0) b0’
     • In the first argument of ‘Sing’, namely ‘(Id :: bat w w)’
       In the type signature: sId :: Sing w -> Sing (Id :: bat w w)
diff --git a/testsuite/tests/polykinds/T9144.stderr b/testsuite/tests/polykinds/T9144.stderr
index 5db0260fc9..f58a57254b 100644
--- a/testsuite/tests/polykinds/T9144.stderr
+++ b/testsuite/tests/polykinds/T9144.stderr
@@ -1,9 +1,8 @@
 
 T9144.hs:34:26: error:
     • Couldn't match type ‘Integer’ with ‘FooTerm’
-      Expected type: DemoteRep 'KProxy
-        Actual type: DemoteRep 'KProxy
-      Use -fprint-explicit-kinds to see the kind arguments
+      Expected type: DemoteRep @Nat ('KProxy @Nat)
+        Actual type: DemoteRep @Foo ('KProxy @Foo)
     • In the first argument of ‘toSing’, namely ‘n’
       In the expression: toSing n
       In the expression:
diff --git a/testsuite/tests/polykinds/TidyClassKinds.stderr b/testsuite/tests/polykinds/TidyClassKinds.stderr
index 5cbea8b417..eb51ca5692 100644
--- a/testsuite/tests/polykinds/TidyClassKinds.stderr
+++ b/testsuite/tests/polykinds/TidyClassKinds.stderr
@@ -1,7 +1,7 @@
 
 TidyClassKinds.hs:12:10: error:
     • Illegal instance declaration for
-        ‘Poly (k -> *) (k -> *) (ProxySyn k) (ProxySyn k)’
+        ‘Poly @{k -> *} @{k -> *} (ProxySyn @{k}) (ProxySyn @{k})’
         (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.)