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

19 files changed, 93 insertions, 52 deletions

diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr
index 11a81baf62..156f8490e8 100644
--- a/testsuite/tests/polykinds/T11520.stderr
+++ b/testsuite/tests/polykinds/T11520.stderr
@@ -1,6 +1,9 @@
 
 T11520.hs:15:77: error:
     • Expected kind ‘k20 -> k10’, but ‘g’ has kind ‘k’
+      ‘k’ is a rigid type variable bound by
+        the instance declaration
+        at T11520.hs:(15,1)-(16,23)
     • In the second argument of ‘Compose’, namely ‘g’
       In the first argument of ‘Typeable’, namely ‘(Compose f g)’
       In the instance declaration for ‘Typeable (Compose f g)’
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index 5ce7b07187..fcf194ba50 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -1,16 +1,9 @@
 
-T12593.hs:11:16: error:
-    • Expected kind ‘k0 -> k1 -> *’, but ‘Free k k1 k2 p’ has kind ‘*’
-    • In the type signature:
-        run :: k2 q =>
-               Free k k1 k2 p a b
-               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
-
 T12593.hs:12:31: error:
     • Expecting one more argument to ‘k’
       Expected a type, but
       ‘k’ has kind
-      ‘((k2 -> Constraint) -> k3 -> *) -> Constraint’
+      ‘((k0 -> Constraint) -> k1 -> *) -> Constraint’
     • In the kind ‘k’
       In the type signature:
         run :: k2 q =>
diff --git a/testsuite/tests/polykinds/T14172.hs b/testsuite/tests/polykinds/T14172.hs
index 10fff5af69..06956be91a 100644
--- a/testsuite/tests/polykinds/T14172.hs
+++ b/testsuite/tests/polykinds/T14172.hs
@@ -5,3 +5,8 @@ import T14172a
 
 traverseCompose :: (a -> f b) -> g a -> f (h _)
 traverseCompose = _Wrapping Compose . traverse
+
+-- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
+-- (.) :: (y->z) -> (x->y) -> (x -> z)
+-- x := a -> f b
+-- z := g a -> f (h a1)
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index d27f45bb9c..0f5d0271b4 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -15,6 +15,10 @@ T14172.hs:7:19: error:
       Expected: (f'0 a -> f (f'0 b)) -> Compose f'0 g'0 a -> f (h a')
         Actual: (Unwrapped (Compose f'0 g'0 a) -> f (Unwrapped (h a')))
                 -> Compose f'0 g'0 a -> f (h a')
+      ‘a’ is a rigid type variable bound by
+        the inferred type of
+          traverseCompose :: (a -> f b) -> g a -> f (h a')
+        at T14172.hs:6:1-47
     • In the first argument of ‘(.)’, namely ‘_Wrapping Compose’
       In the expression: _Wrapping Compose . traverse
       In an equation for ‘traverseCompose’:
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 2d49b819a0..8ff308ba1d 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -5,14 +5,14 @@ T14846.hs:38:8: error:
         Actual: Hom riki a a
       ‘ríki’ is a rigid type variable bound by
         the type signature for:
-          i :: forall {k5} {k6} {cls3 :: k6 -> Constraint} (xx :: k5)
-                      (a :: Struct cls3) (ríki :: Struct cls3 -> Struct cls3 -> *).
+          i :: forall {k4} {k5} {cls2 :: k5 -> Constraint} (xx :: k4)
+                      (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 -> *).
                StructI xx a =>
                ríki a a
         at T14846.hs:38:8-48
     • When checking that instance signature for ‘i’
         is more general than its signature in the class
-        Instance sig: forall {k1} {k2} {cls :: k2 -> Constraint} (xx :: k1)
+        Instance sig: forall {k1} {k3} {cls :: k3 -> Constraint} (xx :: k1)
                              (a :: Struct cls).
                       StructI xx a =>
                       Hom riki a a
@@ -23,10 +23,10 @@ T14846.hs:38:8: error:
       In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:44: error:
-    • Couldn't match kind ‘k4’ with ‘Struct cls3’
-      Expected kind ‘Struct cls3 -> Constraint’,
-        but ‘cls’ has kind ‘k4 -> Constraint’
-      ‘k4’ is a rigid type variable bound by
+    • Couldn't match kind ‘k3’ with ‘Struct cls2’
+      Expected kind ‘Struct cls2 -> Constraint’,
+        but ‘cls’ has kind ‘k3 -> Constraint’
+      ‘k3’ is a rigid type variable bound by
         the instance declaration
         at T14846.hs:37:10-65
     • In the second argument of ‘Structured’, namely ‘cls’
diff --git a/testsuite/tests/polykinds/T15787.stderr b/testsuite/tests/polykinds/T15787.stderr
index 88eca5c1ac..7241e2f7fb 100644
--- a/testsuite/tests/polykinds/T15787.stderr
+++ b/testsuite/tests/polykinds/T15787.stderr
@@ -1,6 +1,9 @@
 
 T15787.hs:15:14: error:
     • Expected a type, but ‘k’ has kind ‘ob’
+      ‘ob’ is a rigid type variable bound by
+        the data constructor ‘Kl’
+        at T15787.hs:15:3-43
     • In the type ‘k’
       In the definition of data constructor ‘Kl’
       In the data declaration for ‘Kl_kind’
diff --git a/testsuite/tests/polykinds/T16221a.stderr b/testsuite/tests/polykinds/T16221a.stderr
index 27edc2c8ec..7b550b6c8f 100644
--- a/testsuite/tests/polykinds/T16221a.stderr
+++ b/testsuite/tests/polykinds/T16221a.stderr
@@ -1,6 +1,12 @@
 
 T16221a.hs:6:49: error:
-    • Expected kind ‘k1’, but ‘b’ has kind ‘k’
+    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
+      ‘k1’ is a rigid type variable bound by
+        the data constructor ‘MkT2’
+        at T16221a.hs:6:20
+      ‘k’ is a rigid type variable bound by
+        the data constructor ‘MkT2’
+        at T16221a.hs:6:20
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type ‘(SameKind a b)’
       In the definition of data constructor ‘MkT2’
diff --git a/testsuite/tests/polykinds/T16245a.hs b/testsuite/tests/polykinds/T16245a.hs
new file mode 100644
index 0000000000..d649701261
--- /dev/null
+++ b/testsuite/tests/polykinds/T16245a.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+
+type Const a b = a
+data SameKind :: k -> k -> Type
+
+newtype T (k :: Const Type a) = MkT (forall (b :: k). SameKind a b)
diff --git a/testsuite/tests/polykinds/T16245a.stderr b/testsuite/tests/polykinds/T16245a.stderr
new file mode 100644
index 0000000000..6279ba18bb
--- /dev/null
+++ b/testsuite/tests/polykinds/T16245a.stderr
@@ -0,0 +1,12 @@
+
+T16245a.hs:10:66: error:
+    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
+      ‘k1’ is a rigid type variable bound by
+        the data constructor ‘MkT’
+        at T16245a.hs:10:12
+      ‘k’ is a rigid type variable bound by
+        the data constructor ‘MkT’
+        at T16245a.hs:10:1-67
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the type ‘(forall (b :: k). SameKind a b)’
+      In the definition of data constructor ‘MkT’
diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr
index 2da3e41c36..61d1b0a2ae 100644
--- a/testsuite/tests/polykinds/T16902.stderr
+++ b/testsuite/tests/polykinds/T16902.stderr
@@ -1,6 +1,9 @@
 
 T16902.hs:11:10: error:
     • Expected a type, but found something with kind ‘a’
+      ‘a’ is a rigid type variable bound by
+        the data constructor ‘MkF’
+        at T16902.hs:11:3-12
     • In the type ‘F a’
       In the definition of data constructor ‘MkF’
       In the data declaration for ‘F’
diff --git a/testsuite/tests/polykinds/T17841.stderr b/testsuite/tests/polykinds/T17841.stderr
index de33036dcf..739e4f2680 100644
--- a/testsuite/tests/polykinds/T17841.stderr
+++ b/testsuite/tests/polykinds/T17841.stderr
@@ -1,7 +1,7 @@
 
 T17841.hs:7:45: error:
-    • Expected a type, but ‘t’ has kind ‘k2’
-      ‘k2’ is a rigid type variable bound by
+    • Expected a type, but ‘t’ has kind ‘k’
+      ‘k’ is a rigid type variable bound by
         the class declaration for ‘Foo’
         at T17841.hs:7:12-17
     • In the kind ‘t’
diff --git a/testsuite/tests/polykinds/T17963.stderr b/testsuite/tests/polykinds/T17963.stderr
index 5cade1ded2..e38d216faf 100644
--- a/testsuite/tests/polykinds/T17963.stderr
+++ b/testsuite/tests/polykinds/T17963.stderr
@@ -1,10 +1,10 @@
 
 T17963.hs:15:23: error:
-    • Couldn't match kind ‘rep1’ with ‘'LiftedRep’
+    • Couldn't match kind ‘rep’ with ‘'LiftedRep’
       When matching kinds
         k0 :: *
-        ob :: TYPE rep1
-      ‘rep1’ is a rigid type variable bound by
+        ob :: TYPE rep
+      ‘rep’ is a rigid type variable bound by
         the class declaration for ‘Category'’
         at T17963.hs:13:27-29
     • In the first argument of ‘cat’, namely ‘a’
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index 34440d774e..dd953fa69a 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -1,16 +1,17 @@
 
 T7438.hs:6:14: error:
-    • Couldn't match expected type ‘p1’ with actual type ‘p’
-        ‘p’ is untouchable
-          inside the constraints: b ~ a
-          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
+    • Could not deduce: p ~ p1
+      from the context: b ~ a
+        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
       ‘p’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16
+        the inferred type of go :: Thrist a b -> p -> p1
+        at T7438.hs:6:1-16
       ‘p1’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16
+        the inferred type of go :: Thrist a b -> p -> p1
+        at T7438.hs:6:1-16
       Possible fix: add a type signature for ‘go’
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
diff --git a/testsuite/tests/polykinds/T7594.stderr b/testsuite/tests/polykinds/T7594.stderr
index ea5484d464..fc0aa1fcc3 100644
--- a/testsuite/tests/polykinds/T7594.stderr
+++ b/testsuite/tests/polykinds/T7594.stderr
@@ -1,13 +1,12 @@
 
 T7594.hs:37:12: error:
-    • Couldn't match type ‘b’ with ‘IO ()’
+    • Could not deduce: b ~ IO ()
+      from the context: (:&:) c0 Real a
+        bound by a type expected by the context:
+                   forall a. (:&:) c0 Real a => a -> b
+        at T7594.hs:37:12-16
       Expected: a -> b
         Actual: a -> IO ()
-        ‘b’ is untouchable
-          inside the constraints: (:&:) c0 Real a
-          bound by a type expected by the context:
-                     forall a. (:&:) c0 Real a => a -> b
-          at T7594.hs:37:12-16
       ‘b’ is a rigid type variable bound by
         the inferred type of bar2 :: b
         at T7594.hs:37:1-19
diff --git a/testsuite/tests/polykinds/T7805.stderr b/testsuite/tests/polykinds/T7805.stderr
index 869ecc9200..e4fdff52e0 100644
--- a/testsuite/tests/polykinds/T7805.stderr
+++ b/testsuite/tests/polykinds/T7805.stderr
@@ -1,8 +1,6 @@
 
 T7805.hs:7:21: error:
-    • Expected kind ‘forall a. a -> a’, but ‘x’ has kind ‘k0’
-      Cannot instantiate unification variable ‘k0’
-      with a kind involving polytypes: forall a. a -> a
+    • Expected kind ‘forall a. a -> a’, but ‘x’ has kind ‘*’
     • In the first argument of ‘HR’, namely ‘x’
       In the first argument of ‘F’, namely ‘(HR x)’
       In the type instance declaration for ‘F’
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index 653f3beb1a..71c2f00584 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -1,14 +1,12 @@
 
-T8616.hs:8:16: error:
-    • Couldn't match kind ‘k1’ with ‘*’
-      When matching types
-        Any :: k1
-        Proxy kproxy :: *
-      ‘k1’ is a rigid type variable bound by
+T8616.hs:8:30: error:
+    • Expected a type, but ‘Any :: k’ has kind ‘k’
+      ‘k’ is a rigid type variable bound by
         the type signature for:
-          withSomeSing :: forall k1 (kproxy :: k1). Proxy kproxy
+          withSomeSing :: forall k (kproxy :: k). Proxy kproxy
         at T8616.hs:7:1-52
-    • In the expression: undefined :: (Any :: k)
+    • In an expression type signature: (Any :: k)
+      In the expression: undefined :: (Any :: k)
       In an equation for ‘withSomeSing’:
           withSomeSing = undefined :: (Any :: k)
     • Relevant bindings include
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index 2fc5bb1792..b18efe0111 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -1,15 +1,14 @@
 
 T9017.hs:8:7: error:
-    • Couldn't match kind ‘k2’ with ‘*’
+    • Couldn't match kind ‘k’ with ‘*’
       When matching types
         a0 :: * -> * -> *
-        a :: k2 -> k3 -> *
+        a :: k -> k1 -> *
       Expected: a b (m b)
         Actual: a0 b0 (m0 b0)
-      ‘k2’ is a rigid type variable bound by
+      ‘k’ is a rigid type variable bound by
         the type signature for:
-          foo :: forall {k2} {k3} (a :: k2 -> k3 -> *) (b :: k2)
-                        (m :: k2 -> k3).
+          foo :: forall {k} {k1} (a :: k -> k1 -> *) (b :: k) (m :: k -> k1).
                  a b (m b)
         at T9017.hs:7:1-16
     • In the expression: arr return
diff --git a/testsuite/tests/polykinds/TyVarTvKinds3.stderr b/testsuite/tests/polykinds/TyVarTvKinds3.stderr
index 67da965d09..b0b7924444 100644
--- a/testsuite/tests/polykinds/TyVarTvKinds3.stderr
+++ b/testsuite/tests/polykinds/TyVarTvKinds3.stderr
@@ -1,6 +1,12 @@
 
 TyVarTvKinds3.hs:9:62: error:
     • Expected kind ‘k1’, but ‘b’ has kind ‘k2’
+      ‘k2’ is a rigid type variable bound by
+        the data constructor ‘MkBad’
+        at TyVarTvKinds3.hs:9:22-23
+      ‘k1’ is a rigid type variable bound by
+        the data constructor ‘MkBad’
+        at TyVarTvKinds3.hs:9:19-20
     • In the second argument of ‘SameKind’, namely ‘b’
       In the first argument of ‘Bad’, namely ‘(SameKind a b)’
       In the type ‘Bad (SameKind a b)’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 1ff66e63ab..b167b930dc 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -213,6 +213,7 @@ test('T16221', normal, compile, [''])
 test('T16221a', normal, compile_fail, [''])
 test('T16244', normal, compile_fail, [''])
 test('T16245', normal, compile_fail, [''])
+test('T16245a', normal, compile_fail, [''])
 test('T16342', normal, compile, [''])
 test('T16263', normal, compile_fail, [''])
 test('T16902', normal, compile_fail, [''])