Improve kind generalisation, error messages

This patch does two things:

* It refactors GHC.Tc.Errors a bit.  In debugging Quick Look I was
  forced to look in detail at error messages, and ended up doing a bit
  of refactoring, esp in mkTyVarEqErr'.  It's still quite a mess, but
  a bit better, I think.

* It makes a significant improvement to the kind checking of type and
  class declarations. Specifically, we now ensure that if kind
  checking fails with an unsolved constraint, all the skolems are in
  scope.  That wasn't the case before, which led to some obscure error
  messages; and occasional failures with "no skolem info" (eg #16245).

Both of these, and the main Quick Look patch itself, affect a /lot/ of
error messages, as you can see from the number of files changed.  I've
checked them all; I think they are as good or better than before.

Smaller things

* I documented the various instances of VarBndr better.
  See Note [The VarBndr tyep and its uses] in GHC.Types.Var

* Renamed GHC.Tc.Solver.simpl_top to simplifyTopWanteds

* A bit of refactoring in bindExplicitTKTele, to avoid the
  footwork with Either.  Simpler now.

* Move promoteTyVar from GHC.Tc.Solver to GHC.Tc.Utils.TcMType

Fixes #16245 (comment 211369), memorialised as
  typecheck/polykinds/T16245a
Also fixes the three bugs in #18640

3 files changed, 14 insertions, 13 deletions

diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index e59a28a99d..a3cdc763fc 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -36,8 +36,8 @@ T10403.hs:22:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
         ...plus two instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the second argument of ‘(.)’, namely ‘fmap (const ())’
-      In the expression: H . fmap (const ())
       In the expression: (H . fmap (const ())) (fmap f b)
+      In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b)
 
 T10403.hs:28:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type ‘f0’ with ‘B t’
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index ced11e50a2..0e7967a276 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -1,7 +1,7 @@
 
 T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Could not deduce (SingI a) arising from a use of ‘sing’
-      from the context: (Action act, Monoid a, Good m1)
+      from the context: (Action act, Monoid a, Good m)
         bound by the instance declaration at T14584.hs:54:10-89
     • In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
@@ -11,10 +11,10 @@ T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
         act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
 
 T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce: m1 ~ *
-      from the context: (Action act, Monoid a, Good m1)
+    • Could not deduce: m ~ *
+      from the context: (Action act, Monoid a, Good m)
         bound by the instance declaration at T14584.hs:54:10-89
-      ‘m1’ is a rigid type variable bound by
+      ‘m’ is a rigid type variable bound by
         the instance declaration
         at T14584.hs:54:10-89
     • In the type ‘a’
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
index 9d7ab35dd5..c3e957b9dd 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr
@@ -1,14 +1,15 @@
 
 T14584a.hs:12:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘()’ with actual type ‘m -> m’
-    • In the expression: id @m :: _
+    • Probable cause: ‘id @m :: _’ is applied to too few arguments
+      In the expression: id @m :: _
       In an equation for ‘f’: f = id @m :: _
 
 T14584a.hs:12:9: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Expected a type, but ‘m’ has kind ‘k2’
-      ‘k2’ is a rigid type variable bound by
+    • Expected a type, but ‘m’ has kind ‘k’
+      ‘k’ is a rigid type variable bound by
         the type signature for:
-          f :: forall {k2} (m :: k2). ()
+          f :: forall {k} (m :: k). ()
         at T14584a.hs:11:1-17
     • In the type ‘m’
       In the expression: id @m :: _
@@ -18,7 +19,7 @@ T14584a.hs:12:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘m -> m’
       Where: ‘m’, ‘k’ are rigid type variables bound by
                the type signature for:
-                 f :: forall {k2} (m :: k2). ()
+                 f :: forall {k} (m :: k). ()
                at T14584a.hs:11:1-17
     • In an expression type signature: _
       In the expression: id @m :: _
@@ -26,10 +27,10 @@ T14584a.hs:12:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Relevant bindings include f :: () (bound at T14584a.hs:12:1)
 
 T14584a.hs:15:17: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Expected a type, but ‘m’ has kind ‘k2’
-      ‘k2’ is a rigid type variable bound by
+    • Expected a type, but ‘m’ has kind ‘k’
+      ‘k’ is a rigid type variable bound by
         the type signature for:
-          g :: forall {k2} (m :: k2). ()
+          g :: forall {k} (m :: k). ()
         at T14584a.hs:14:1-17
     • In the type ‘m’
       In the expression: id @m