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

4 files changed, 20 insertions, 23 deletions

diff --git a/testsuite/tests/gadt/T12468.stderr b/testsuite/tests/gadt/T12468.stderr
index 402a93d82d..5abe870814 100644
--- a/testsuite/tests/gadt/T12468.stderr
+++ b/testsuite/tests/gadt/T12468.stderr
@@ -1,8 +1,7 @@
 
 T12468.hs:9:7: error:
     • Found hole: _ :: Int
-    • In the expression: _
-      In an equation for ‘f’: f I = _
+    • In an equation for ‘f’: f I = _
     • Relevant bindings include f :: T a -> a (bound at T12468.hs:9:1)
       Constraints include a ~ Int (from T12468.hs:9:3)
       Valid hole fits include
diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index 19aa501a4c..d771c63828 100644
--- a/testsuite/tests/gadt/gadt-escape1.stderr
+++ b/testsuite/tests/gadt/gadt-escape1.stderr
@@ -1,13 +1,12 @@
 
 gadt-escape1.hs:19:58: error:
-    • Couldn't match type ‘p’ with ‘ExpGADT Int’
+    • Could not deduce: p ~ ExpGADT Int
+      from the context: t ~ Int
+        bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int,
+                 in a case alternative
+        at gadt-escape1.hs:19:43-50
       Expected: p
         Actual: ExpGADT t
-        ‘p’ is untouchable
-          inside the constraints: t ~ Int
-          bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int,
-                   in a case alternative
-          at gadt-escape1.hs:19:43-50
       ‘p’ is a rigid type variable bound by
         the inferred type of weird1 :: p
         at gadt-escape1.hs:19:1-58
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index cea221944b..49eb2bc96f 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -1,12 +1,10 @@
 
 gadt13.hs:15:13: error:
-    • Couldn't match expected type ‘p’
-                  with actual type ‘String -> [Char]’
-        ‘p’ is untouchable
-          inside the constraints: a ~ Int
-          bound by a pattern with constructor: I :: Int -> Term Int,
-                   in an equation for ‘shw’
-          at gadt13.hs:15:6-8
+    • Could not deduce: p ~ (String -> [Char])
+      from the context: a ~ Int
+        bound by a pattern with constructor: I :: Int -> Term Int,
+                 in an equation for ‘shw’
+        at gadt13.hs:15:6-8
       ‘p’ is a rigid type variable bound by
         the inferred type of shw :: Term a -> p
         at gadt13.hs:15:1-30
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index bb179975fb..679ec3b00e 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,15 +1,16 @@
 
 gadt7.hs:16:38: error:
-    • Couldn't match expected type ‘p1’ with actual type ‘p’
-        ‘p’ is untouchable
-          inside the constraints: a ~ Int
-          bound by a pattern with constructor: K :: T Int,
-                   in a case alternative
-          at gadt7.hs:16:33
+    • Could not deduce: p ~ p1
+      from the context: a ~ Int
+        bound by a pattern with constructor: K :: T Int,
+                 in a case alternative
+        at gadt7.hs:16:33
       ‘p’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
+        the inferred type of i1b :: T a -> p -> p1
+        at gadt7.hs:16:1-44
       ‘p1’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
+        the inferred type of i1b :: T a -> p -> p1
+        at gadt7.hs:16:1-44
       Possible fix: add a type signature for ‘i1b’
     • In the expression: y1
       In a case alternative: K -> y1