Remove decideKindGeneralisationPlan

TypeInType came with a new function: decideKindGeneralisationPlan.
This type-level counterpart to the term-level decideGeneralisationPlan
chose whether or not a kind should be generalized. The thinking was
that if `let` should not be generalized, then kinds shouldn't either
(under the same circumstances around -XMonoLocalBinds).

However, this is too conservative -- the situation described in the
motivation for "let should be be generalized" does not occur in types.

This commit thus removes decideKindGeneralisationPlan, always
generalizing.

One consequence is that tc_hs_sig_type_and_gen no longer calls
solveEqualities, which reports all unsolved constraints, instead
relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect
of this is that reporing kind errors gets delayed more frequently.
This seems to be a net benefit in error reporting; often, alongside
a kind error, the type error is now reported (and users might find
type errors easier to understand).

Some of these errors ended up at the top level, where it was
discovered that the GlobalRdrEnv containing the definitions in the
local module was not in the TcGblEnv, and thus errors were reported
with qualified names unnecessarily. This commit rejiggers some of
the logic around captureTopConstraints accordingly.

One error message (typecheck/should_fail/T1633)
is a regression, mentioning the name of a default method. However,
that problem is already reported as #10087, its solution is far from
clear, and so I'm not addressing it here.

This commit fixes #15141. As it's an internal refactor, there is
no concrete test case for it.

Along the way, we no longer need the hsib_closed field of
HsImplicitBndrs (it was used only in decideKindGeneralisationPlan)
and so it's been removed, simplifying the datatype structure.

Along the way, I removed code in the validity checker that looks
at coercions. This isn't related to this patch, really (though
it was, at one point), but it's an improvement, so I kept it.

This updates the haddock submodule.

44 files changed, 386 insertions, 146 deletions

diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_compile/T14066h.hs
index a20ae30958..df3db1c15d 100644
--- a/testsuite/tests/dependent/should_fail/T14066h.hs
+++ b/testsuite/tests/dependent/should_compile/T14066h.hs
@@ -7,5 +7,5 @@ import Data.Proxy
 f :: forall b. b -> (Proxy Int, Proxy Maybe)
 f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
   where
-    y :: (Proxy a, b)  -- MonoLocalBinds means this won't generalize over the kind of a
+    y :: (Proxy a, b)  -- this generalizes over the kind of a
     y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 4e096c1f71..418fba2d85 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -53,3 +53,4 @@ test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
 test('T15346', normal, compile, [''])
 test('T15419', normal, compile, [''])
+test('T14066h', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr
index 630f010fa3..a8e64d4e0c 100644
--- a/testsuite/tests/dependent/should_fail/DepFail1.stderr
+++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr
@@ -2,11 +2,25 @@
 DepFail1.hs:7:6: error:
     • Expecting one more argument to ‘Proxy Bool’
       Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’
-    • In the type signature:
-        z :: Proxy Bool
+    • In the type signature: z :: Proxy Bool
+
+DepFail1.hs:8:5: error:
+    • Couldn't match expected type ‘Proxy Bool’
+                  with actual type ‘Proxy k0 a1’
+    • In the expression: P
+      In an equation for ‘z’: z = P
 
 DepFail1.hs:10:16: error:
     • Expected kind ‘Int’, but ‘Bool’ has kind ‘*’
     • In the second argument of ‘Proxy’, namely ‘Bool’
-      In the type signature:
-        a :: Proxy Int Bool
+      In the type signature: a :: Proxy Int Bool
+
+DepFail1.hs:11:5: error:
+    • Couldn't match kind ‘*’ with ‘Int’
+      When matching types
+        a0 :: Int
+        Bool :: *
+      Expected type: Proxy Int Bool
+        Actual type: Proxy Int a0
+    • In the expression: P
+      In an equation for ‘a’: a = P
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
index 0ae1710bf0..3e8bef6858 100644
--- a/testsuite/tests/dependent/should_fail/T13895.stderr
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -1,4 +1,28 @@
 
+T13895.hs:8:14: error:
+    • Could not deduce (Typeable (t dict0))
+      from the context: (Data a, Typeable (t dict))
+        bound by the type signature for:
+                   dataCast1 :: forall k (dict :: Typeable k) (dict1 :: Typeable
+                                                                          *) a (c :: *
+                                                                                     -> *) (t :: forall k1.
+                                                                                                 Typeable
+                                                                                                   k1 =>
+                                                                                                 k1
+                                                                                                 -> *).
+                                (Data a, Typeable (t dict)) =>
+                                (forall d. Data d => c (t dict1 d)) -> Maybe (c a)
+        at T13895.hs:(8,14)-(14,24)
+      The type variable ‘dict0’ is ambiguous
+    • In the ambiguity check for ‘dataCast1’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
 T13895.hs:12:23: error:
     • Illegal constraint in a kind: Typeable k0
     • In the first argument of ‘Typeable’, namely ‘t’
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
index cd0142f5c1..e5179e510b 100644
--- a/testsuite/tests/dependent/should_fail/T14066.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -1,6 +1,6 @@
 
 T14066.hs:15:59: error:
-    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature: g :: forall k (b :: k). SameKind a b
       In the expression:
@@ -8,4 +8,6 @@ T14066.hs:15:59: error:
           g :: forall k (b :: k). SameKind a b
           g = undefined
         in ()
-    • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4)
+    • Relevant bindings include
+        x :: Proxy a (bound at T14066.hs:15:4)
+        f :: Proxy a -> () (bound at T14066.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
index 504ca5a80e..193c74d193 100644
--- a/testsuite/tests/dependent/should_fail/T14066e.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -1,6 +1,15 @@
 
 T14066e.hs:13:59: error:
-    • Expected kind ‘c’, but ‘b'’ has kind ‘k0’
+    • Couldn't match kind ‘k1’ with ‘*’
+      ‘k1’ is a rigid type variable bound by
+        the type signature for:
+          j :: forall k k1 (c :: k1) (b :: k).
+               Proxy a -> Proxy b -> Proxy c -> Proxy b
+        at T14066e.hs:12:5-61
+      When matching kinds
+        k :: *
+        c :: k1
+      Expected kind ‘c’, but ‘b'’ has kind ‘k’
     • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
       In an expression type signature: Proxy (b' :: c')
       In the expression: (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr
deleted file mode 100644
index bfd33693b6..0000000000
--- a/testsuite/tests/dependent/should_fail/T14066h.stderr
+++ /dev/null
@@ -1,16 +0,0 @@
-
-T14066h.hs:8:28: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching types
-        a0 :: *
-        Maybe :: * -> *
-      Expected type: Proxy Maybe
-        Actual type: Proxy a0
-    • In the expression: fst y :: Proxy Maybe
-      In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe)
-      In an equation for ‘f’:
-          f x
-            = (fst y :: Proxy Int, fst y :: Proxy Maybe)
-            where
-                y :: (Proxy a, b)
-                y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 593b7787a1..0f7129020e 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -26,7 +26,6 @@ test('T14066d', normal, compile_fail, [''])
 test('T14066e', normal, compile_fail, [''])
 test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
-test('T14066h', normal, compile_fail, [''])
 test('T14845_fail1', normal, compile_fail, [''])
 test('T14845_fail2', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index a1c412bd7d..2c1a0ec7df 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -125,10 +125,8 @@
           (Just
            [({ DumpRenamedAst.hs:9:3-36 }
              (HsIB
-              (HsIBRn
-               [{Name: a}
-               ,{Name: as}]
-               (True))
+              [{Name: a}
+              ,{Name: as}]
               (FamEqn
                (NoExt)
                ({ DumpRenamedAst.hs:9:3-8 }
@@ -183,9 +181,7 @@
                         {Name: as}))))))))))))
            ,({ DumpRenamedAst.hs:10:3-24 }
              (HsIB
-              (HsIBRn
-               []
-               (True))
+              []
               (FamEqn
                (NoExt)
                ({ DumpRenamedAst.hs:10:3-8 }
@@ -285,10 +281,8 @@
         (NoExt)
         (DataFamInstDecl
          (HsIB
-          (HsIBRn
-           [{Name: k}
-           ,{Name: a}]
-           (True))
+          [{Name: k}
+          ,{Name: a}]
           (FamEqn
            (NoExt)
            ({ DumpRenamedAst.hs:15:18-20 }
diff --git a/testsuite/tests/polykinds/T11142.stderr b/testsuite/tests/polykinds/T11142.stderr
index ea687c3247..a3b40c1222 100644
--- a/testsuite/tests/polykinds/T11142.stderr
+++ b/testsuite/tests/polykinds/T11142.stderr
@@ -1,6 +1,17 @@
 
 T11142.hs:9:49: error:
-    • Expected kind ‘k’, but ‘b’ has kind ‘k0’
+    • Expected kind ‘k1’, but ‘b’ has kind ‘k0’
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature:
         foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
+
+T11142.hs:10:7: error:
+    • Cannot instantiate unification variable ‘a0’
+      with a type involving foralls:
+        (forall k1 (a :: k1). SameKind a b) -> ()
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: undefined
+      In an equation for ‘foo’: foo = undefined
+    • Relevant bindings include
+        foo :: (forall k1 (a :: k1). SameKind a b) -> ()
+          (bound at T11142.hs:10:1)
diff --git a/testsuite/tests/polykinds/T11516.hs b/testsuite/tests/polykinds/T11516.hs
index 3b19a997f9..66feeec387 100644
--- a/testsuite/tests/polykinds/T11516.hs
+++ b/testsuite/tests/polykinds/T11516.hs
@@ -3,6 +3,7 @@
 {-# language ConstraintKinds #-}
 {-# language FlexibleInstances #-}
 {-# language FunctionalDependencies #-}
+{-# language UndecidableInstances #-}
 
 import GHC.Exts (Constraint)
 
diff --git a/testsuite/tests/polykinds/T11516.stderr b/testsuite/tests/polykinds/T11516.stderr
index 5db11c8f83..5f8083309c 100644
--- a/testsuite/tests/polykinds/T11516.stderr
+++ b/testsuite/tests/polykinds/T11516.stderr
@@ -1,5 +1,5 @@
 
-T11516.hs:11:16: error:
+T11516.hs:12:16: error:
     • Expected kind ‘i0 -> i0 -> *’, but ‘()’ has kind ‘*’
     • In the first argument of ‘Varpi’, namely ‘()’
       In the instance declaration for ‘Varpi (->) (->) (Either f)’
diff --git a/testsuite/tests/polykinds/T11520.hs b/testsuite/tests/polykinds/T11520.hs
index eef999d4ba..9c1d4fe1be 100644
--- a/testsuite/tests/polykinds/T11520.hs
+++ b/testsuite/tests/polykinds/T11520.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, PolyKinds, GADTs, UndecidableSuperClasses #-}
+{-# LANGUAGE RankNTypes, PolyKinds, GADTs, UndecidableSuperClasses, UndecidableInstances #-}
 
 module T11520 where
 
diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr
index 11a81baf62..75147e6a00 100644
--- a/testsuite/tests/polykinds/T11520.stderr
+++ b/testsuite/tests/polykinds/T11520.stderr
@@ -1,4 +1,8 @@
 
+T11520.hs:15:57: error:
+    • Illegal type synonym family application in instance: Compose f g
+    • In the instance declaration for ‘Typeable (Compose f g)’
+
 T11520.hs:15:77: error:
     • Expected kind ‘k20 -> k10’, but ‘g’ has kind ‘k’
     • In the second argument of ‘Compose’, namely ‘g’
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index 43f762221e..27123a8bc8 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -10,7 +10,7 @@ T12593.hs:12:31: error:
     • Expecting one more argument to ‘k’
       Expected a type, but
       ‘k’ has kind
-      ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+      ‘(((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
        -> Constraint’
     • In the kind ‘k’
       In the type signature:
@@ -22,7 +22,7 @@ T12593.hs:12:40: error:
     • Expecting two more arguments to ‘k1’
       Expected a type, but
       ‘k1’ has kind
-      ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’
+      ‘((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *’
     • In the kind ‘k1’
       In the type signature:
         run :: k2 q =>
@@ -31,13 +31,13 @@ T12593.hs:12:40: error:
 
 T12593.hs:12:47: error:
     • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-                            -> (k2 -> k3 -> *) -> *)
+                            -> (k3 -> k4 -> *) -> *)
                            -> Constraint’
                      with ‘*’
       When matching kinds
-        k2 :: *
-        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
-             -> Constraint
+        k3 :: *
+        k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
+              -> Constraint
     • In the first argument of ‘p’, namely ‘c’
       In the type signature:
         run :: k2 q =>
@@ -46,11 +46,11 @@ T12593.hs:12:47: error:
 
 T12593.hs:12:49: error:
     • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-                           -> (k2 -> k3 -> *) -> *’
+                           -> (k3 -> k4 -> *) -> *’
                      with ‘*’
       When matching kinds
-        k3 :: *
-        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k4 :: *
+        k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
     • In the second argument of ‘p’, namely ‘d’
       In the type signature:
         run :: k2 q =>
@@ -59,13 +59,13 @@ T12593.hs:12:49: error:
 
 T12593.hs:12:56: error:
     • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-                            -> (k2 -> k3 -> *) -> *)
+                            -> (k3 -> k4 -> *) -> *)
                            -> Constraint’
                      with ‘*’
       When matching kinds
         k0 :: *
-        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
-             -> Constraint
+        k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
+              -> Constraint
     • In the first argument of ‘q’, namely ‘c’
       In the type signature:
         run :: k2 q =>
@@ -74,13 +74,43 @@ T12593.hs:12:56: error:
 
 T12593.hs:12:58: error:
     • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-                           -> (k2 -> k3 -> *) -> *’
+                           -> (k3 -> k4 -> *) -> *’
                      with ‘*’
       When matching kinds
         k1 :: *
-        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
     • In the second argument of ‘q’, namely ‘d’
       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:14:6: error:
+    • Couldn't match type ‘Free k2 p0’ with ‘Free k6 k7 k8 p’
+      Expected type: Free k6 k7 k8 p a b
+        Actual type: Free k2 p0 a b
+    • In the pattern: Free cat
+      In an equation for ‘run’: run (Free cat) = cat
+    • Relevant bindings include
+        run :: Free k6 k7 k8 p a b
+               -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b
+          (bound at T12593.hs:14:1)
+
+T12593.hs:14:18: error:
+    • Couldn't match kind ‘*’
+                     with ‘(((k3 -> k4 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
+                           -> Constraint’
+      When matching kinds
+        k0 :: *
+        k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
+              -> Constraint
+    • In the expression: cat
+      In an equation for ‘run’: run (Free cat) = cat
+    • Relevant bindings include
+        cat :: forall (q :: k0 -> k1 -> *).
+               k2 q =>
+               (forall (c :: k0) (d :: k1). p0 c d -> q c d) -> q a b
+          (bound at T12593.hs:14:11)
+        run :: Free k6 k7 k8 p a b
+               -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b
+          (bound at T12593.hs:14:1)
diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr
deleted file mode 100644
index 3d2492e23d..0000000000
--- a/testsuite/tests/polykinds/T13555.stderr
+++ /dev/null
@@ -1,20 +0,0 @@
-
-T13555.hs:25:14: error:
-    • Couldn't match type ‘k2’ with ‘k0’
-      ‘k2’ is a rigid type variable bound by
-        the type signature for:
-          crtInfo :: forall k2 (m :: k2).
-                     Reflects m Int =>
-                     TaggedT m Maybe (CRTInfo (GF fp d))
-        at T13555.hs:25:14-79
-      Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
-        Actual type: TaggedT m0 Maybe (CRTInfo (GF fp d))
-    • When checking that instance signature for ‘crtInfo’
-        is more general than its signature in the class
-        Instance sig: forall (m :: k0).
-                      Reflects m Int =>
-                      TaggedT m Maybe (CRTInfo (GF fp d))
-           Class sig: forall k2 (m :: k2).
-                      Reflects m Int =>
-                      TaggedT m Maybe (CRTInfo (GF fp d))
-      In the instance declaration for ‘CRTrans Maybe (GF fp d)’
diff --git a/testsuite/tests/polykinds/T14520.hs b/testsuite/tests/polykinds/T14520.hs
index 23e903773b..44dc2ee18d 100644
--- a/testsuite/tests/polykinds/T14520.hs
+++ b/testsuite/tests/polykinds/T14520.hs
@@ -1,4 +1,4 @@
-{-# Language DataKinds, PolyKinds, TypeFamilies, TypeOperators #-}
+{-# Language DataKinds, PolyKinds, TypeFamilies, TypeOperators, AllowAmbiguousTypes #-}
 
 module T14520 where
 
diff --git a/testsuite/tests/polykinds/T14520.stderr b/testsuite/tests/polykinds/T14520.stderr
index e19d834b95..07042fde92 100644
--- a/testsuite/tests/polykinds/T14520.stderr
+++ b/testsuite/tests/polykinds/T14520.stderr
@@ -1,5 +1,6 @@
 
 T14520.hs:15:24: error:
-    • Expected kind ‘bat w w’, but ‘Id’ has kind ‘XXX (XXX kat0 b0) b0’
+    • Expected kind ‘bat w w’,
+        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/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 3abdb88d2f..1d852031d9 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -13,10 +13,11 @@ T14846.hs:38:8: error:
                ríki a a
         at T14846.hs:38:8-48
       Expected type: ríki a a
-        Actual type: Hom riki a0 a0
+        Actual type: Hom riki a a
     • When checking that instance signature for ‘i’
         is more general than its signature in the class
-        Instance sig: forall (xx :: k0) (a :: Struct cls0).
+        Instance sig: forall k1 (cls :: k1
+                                        -> Constraint) k2 (xx :: k2) (a :: Struct cls).
                       StructI xx a =>
                       Hom riki a a
            Class sig: forall k1 (cls :: k1
@@ -31,15 +32,15 @@ T14846.hs:38:8: error:
       In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:31: error:
-    • Couldn't match kind ‘k4’ with ‘Struct cls0’
+    • Couldn't match kind ‘k4’ with ‘Struct cls2’
       ‘k4’ is a rigid type variable bound by
         the instance declaration
         at T14846.hs:37:10-65
       When matching kinds
-        cls :: k4 -> Constraint
-        cls1 :: Struct cls0 -> Constraint
-      Expected kind ‘Struct cls1’,
-        but ‘Structured a cls’ has kind ‘Struct cls’
+        cls1 :: k4 -> Constraint
+        cls0 :: Struct cls -> Constraint
+      Expected kind ‘Struct cls0’,
+        but ‘Structured a cls’ has kind ‘Struct cls1’
     • In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
       In an expression type signature: AStruct (Structured a cls)
       In the expression: struct :: AStruct (Structured a cls)
diff --git a/testsuite/tests/polykinds/T7224.stderr b/testsuite/tests/polykinds/T7224.stderr
index daab1c40a9..774a4bce69 100644
--- a/testsuite/tests/polykinds/T7224.stderr
+++ b/testsuite/tests/polykinds/T7224.stderr
@@ -2,6 +2,12 @@
 T7224.hs:6:19: error:
     • Expected kind ‘i’, but ‘i’ has kind ‘*’
     • In the first argument of ‘m’, namely ‘i’
+      In the type signature: ret' :: a -> m i i a
+      In the class declaration for ‘PMonad'’
+
+T7224.hs:7:14: error:
+    • Expected kind ‘i’, but ‘i’ has kind ‘*’
+    • In the first argument of ‘m’, namely ‘i’
       In the type signature:
-        ret' :: a -> m i i a
+        bind' :: m i j a -> (a -> m j k b) -> m i k b
       In the class declaration for ‘PMonad'’
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index 6249bf7b62..9aa4ab50d9 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -1,8 +1,14 @@
 
-T8616.hs:8:29: error:
-    • Expected a type, but ‘(Any :: k)’ has kind ‘k’
-    • In an expression type signature: (Any :: k)
-      In the expression: undefined :: (Any :: k)
+T8616.hs:8:16: error:
+    • Couldn't match kind ‘k’ with ‘*’
+      ‘k’ is a rigid type variable bound by
+        the type signature for:
+          withSomeSing :: forall k (kproxy :: k). Proxy kproxy
+        at T8616.hs:7:1-50
+      When matching types
+        a0 :: *
+        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/all.T b/testsuite/tests/polykinds/all.T
index 425e57a946..de46acfc3a 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -161,7 +161,7 @@ test('T13394a', normal, compile, [''])
 test('T13394', normal, compile, [''])
 test('T13371', normal, compile, [''])
 test('T13393', normal, compile_fail, [''])
-test('T13555', normal, compile_fail, [''])
+test('T13555', normal, compile, [''])
 test('T13659', normal, compile_fail, [''])
 test('T13625', normal, compile_fail, [''])
 test('T13985', normal, compile_fail, [''])
@@ -176,7 +176,7 @@ test('T14450', normal, compile_fail, [''])
 test('T14172', normal, multimod_compile_fail, ['T14172.hs','-v0'])
 test('T14174', normal, compile_fail, [''])
 test('T14174a', normal, compile, [''])
-test('T14520', normal, compile_fail, [''])
+test('T14520', normal, compile_fail, ['-fprint-explicit-kinds'])
 test('T11203', normal, compile_fail, [''])
 test('T14555', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('T14563', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
diff --git a/testsuite/tests/rename/should_fail/T5951.stderr b/testsuite/tests/rename/should_fail/T5951.stderr
index 8fda353b33..a6969971ab 100644
--- a/testsuite/tests/rename/should_fail/T5951.stderr
+++ b/testsuite/tests/rename/should_fail/T5951.stderr
@@ -4,6 +4,10 @@ T5951.hs:8:8: error:
       Expected a constraint, but ‘A’ has kind ‘* -> Constraint’
     • In the instance declaration for ‘B => C’
 
+T5951.hs:8:8: error:
+    • Instance head is not headed by a class: C
+    • In the instance declaration for ‘B => C’
+
 T5951.hs:9:8: error:
     • Expecting one more argument to ‘B’
       Expected a constraint, but ‘B’ has kind ‘* -> Constraint’
diff --git a/testsuite/tests/rename/should_fail/rnfail026.hs b/testsuite/tests/rename/should_fail/rnfail026.hs
index d09d9fc22f..2d22df20d4 100644
--- a/testsuite/tests/rename/should_fail/rnfail026.hs
+++ b/testsuite/tests/rename/should_fail/rnfail026.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE RankNTypes, FlexibleInstances #-}
 
--- This one made ghc-4.08 crash 
+-- This one made ghc-4.08 crash
 -- rename/RnEnv.lhs:239: Non-exhaustive patterns in function get_tycon_key
 -- The type in the Monad instance is utterly bogus, of course
 
@@ -9,11 +9,12 @@ module ShouldCompile ( Set ) where
 
 data Set a = Set [a]
        deriving (Eq, Ord, Read, Show)
-
+{-
 instance Functor Set where
         f `fmap` (Set xs) = Set $ f `fmap` xs
-
+-}
 instance Monad (forall a. Eq a => Set a) where
         return x = Set [x]
-
-instance Eq (forall a. [a]) where 
+{-
+instance Eq (forall a. [a]) where
+-}
diff --git a/testsuite/tests/rename/should_fail/rnfail026.stderr b/testsuite/tests/rename/should_fail/rnfail026.stderr
index 8bd80b1b58..79b07c4d24 100644
--- a/testsuite/tests/rename/should_fail/rnfail026.stderr
+++ b/testsuite/tests/rename/should_fail/rnfail026.stderr
@@ -1,10 +1,10 @@
 
+rnfail026.hs:16:10: error:
+    • Illegal polymorphic type: forall a. Eq a => Set a
+    • In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
+
 rnfail026.hs:16:27: error:
     • Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’
     • In the first argument of ‘Monad’, namely
         ‘(forall a. Eq a => Set a)’
       In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
-
-rnfail026.hs:19:10: error:
-    • Illegal polymorphic type: forall a. [a]
-    • In the instance declaration for ‘Eq (forall a. [a])’
diff --git a/testsuite/tests/th/T5358.stderr b/testsuite/tests/th/T5358.stderr
index b698bc1004..4bfc53a78e 100644
--- a/testsuite/tests/th/T5358.stderr
+++ b/testsuite/tests/th/T5358.stderr
@@ -1,24 +1,4 @@
 
-T5358.hs:10:13: error:
-    • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
-    • The function ‘T5358.t1’ is applied to one argument,
-      but its type ‘Int’ has none
-      In the first argument of ‘(==)’, namely ‘T5358.t1 x’
-      In the expression: T5358.t1 x == T5358.t2 x
-    • Relevant bindings include
-        x :: t (bound at T5358.hs:10:9)
-        T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
-
-T5358.hs:10:21: error:
-    • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
-    • The function ‘T5358.t2’ is applied to one argument,
-      but its type ‘Int’ has none
-      In the second argument of ‘(==)’, namely ‘T5358.t2 x’
-      In the expression: T5358.t1 x == T5358.t2 x
-    • Relevant bindings include
-        x :: t (bound at T5358.hs:10:9)
-        T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
-
 T5358.hs:14:12: error:
     • Exception when trying to run compile-time code:
         runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool
diff --git a/testsuite/tests/typecheck/should_compile/T15141.hs b/testsuite/tests/typecheck/should_compile/T15141.hs
new file mode 100644
index 0000000000..c0cb5d8488
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15141.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE PolyKinds, TypeFamilies, TypeFamilyDependencies,
+             ScopedTypeVariables, TypeOperators, GADTs,
+             DataKinds #-}
+
+module T15141 where
+
+import Data.Type.Equality
+import Data.Proxy
+
+type family F a = r | r -> a where
+  F () = Bool
+
+data Wumpus where
+  Unify :: k1 ~ F k2 => k1 -> k2 -> Wumpus
+
+f :: forall k (a :: k). k :~: Bool -> ()
+f Refl = let x :: Proxy ('Unify a b)
+             x = undefined
+         in ()
+
+{-
+We want this situation:
+
+forall[1] k[1].
+  [G] k ~ Bool
+  forall [2] ... . [W] k ~ F kappa[2]
+
+where the inner wanted can be solved only by taking the outer
+given into account. This means that the wanted needs to be floated out.
+More germane to this bug, we need *not* to generalize over kappa.
+
+The code above builds this scenario fairly exactly, and indeed fails
+without the logic in kindGeneralize that excludes constrained variables
+from generalization.
+-}
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 2fb5429715..1857ba814e 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -646,3 +646,4 @@ test('T15431', normal, compile, [''])
 test('T15431a', normal, compile, [''])
 test('T15428', normal, compile, [''])
 test('T15412', normal, compile, [''])
+test('T15141', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T11112.stderr b/testsuite/tests/typecheck/should_fail/T11112.stderr
index ec2154c8ce..304078158e 100644
--- a/testsuite/tests/typecheck/should_fail/T11112.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11112.stderr
@@ -1,5 +1,13 @@
 
 T11112.hs:3:9: error:
     • Expected a type, but ‘Ord s’ has kind ‘Constraint’
-    • In the type signature:
-        sort :: Ord s -> [s] -> [s]
+    • In the type signature: sort :: Ord s -> [s] -> [s]
+
+T11112.hs:4:11: error:
+    • Couldn't match expected type ‘[s] -> [s]’
+                  with actual type ‘Ord s’
+    • In the expression: xs
+      In an equation for ‘sort’: sort xs = xs
+    • Relevant bindings include
+        xs :: Ord s (bound at T11112.hs:4:6)
+        sort :: Ord s => [s] -> [s] (bound at T11112.hs:4:1)
diff --git a/testsuite/tests/typecheck/should_fail/T11563.stderr b/testsuite/tests/typecheck/should_fail/T11563.stderr
index 27eca84816..1283c33983 100644
--- a/testsuite/tests/typecheck/should_fail/T11563.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11563.stderr
@@ -1,4 +1,10 @@
 
+T11563.hs:5:10: error:
+    • Variable ‘s’ occurs more often
+        in the constraint ‘C s’ than in the instance head ‘C T’
+      (Use UndecidableInstances to permit this)
+    • In the instance declaration for ‘C T’
+
 T11563.hs:5:19: error:
     • Expecting one more argument to ‘T’
       Expected a type, but ‘T’ has kind ‘* -> *’
diff --git a/testsuite/tests/typecheck/should_fail/T14232.stderr b/testsuite/tests/typecheck/should_fail/T14232.stderr
index a497be7b19..1ca41f0bd5 100644
--- a/testsuite/tests/typecheck/should_fail/T14232.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14232.stderr
@@ -2,3 +2,16 @@
 T14232.hs:3:6: error:
     • Expected kind ‘* -> *’, but ‘String -> a’ has kind ‘*’
     • In the type signature: f :: (String -> a) String -> a
+
+T14232.hs:4:9: error:
+    • Couldn't match type ‘String -> a’ with ‘(->) t0’
+      Expected type: t0 -> [Char]
+        Actual type: (String -> a) String
+    • The function ‘g’ is applied to one argument,
+      but its type ‘(String -> a) String’ has none
+      In the expression: g s
+      In an equation for ‘f’: f g s = g s
+    • Relevant bindings include
+        s :: t0 (bound at T14232.hs:4:5)
+        g :: (String -> a) String (bound at T14232.hs:4:3)
+        f :: (String -> a) String -> a (bound at T14232.hs:4:1)
diff --git a/testsuite/tests/typecheck/should_fail/T1633.stderr b/testsuite/tests/typecheck/should_fail/T1633.stderr
index 300e6c3def..5d9dcc44f5 100644
--- a/testsuite/tests/typecheck/should_fail/T1633.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1633.stderr
@@ -1,5 +1,5 @@
 
 T1633.hs:8:18: error:
-    Expected kind ‘* -> *’, but ‘Bool’ has kind ‘*’
-    In the first argument of ‘Functor’, namely ‘Bool’
-    In the instance declaration for ‘Functor Bool’
+    • Expected kind ‘* -> *’, but ‘Bool’ has kind ‘*’
+    • In the first argument of ‘Functor’, namely ‘Bool’
+      In the instance declaration for ‘Functor Bool’
diff --git a/testsuite/tests/typecheck/should_fail/T2994.stderr b/testsuite/tests/typecheck/should_fail/T2994.stderr
index 7f20acf5aa..09b36165a6 100644
--- a/testsuite/tests/typecheck/should_fail/T2994.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2994.stderr
@@ -5,12 +5,20 @@ T2994.hs:11:10: error:
         but ‘MonadReader Int’ has kind ‘* -> Constraint’
     • In the instance declaration for ‘MonadReader Int’
 
+T2994.hs:11:10: error:
+    • Instance head is not headed by a class: MonadReader Int
+    • In the instance declaration for ‘MonadReader Int’
+
 T2994.hs:13:10: error:
     • Expecting one more argument to ‘MonadReader (Reader' r)’
       Expected a constraint,
         but ‘MonadReader (Reader' r)’ has kind ‘* -> Constraint’
     • In the instance declaration for ‘MonadReader (Reader' r)’
 
+T2994.hs:13:10: error:
+    • Instance head is not headed by a class: MonadReader (Reader' r)
+    • In the instance declaration for ‘MonadReader (Reader' r)’
+
 T2994.hs:13:23: error:
     • Expecting one more argument to ‘Reader' r’
       Expected a type, but ‘Reader' r’ has kind ‘* -> *’
@@ -21,3 +29,8 @@ T2994.hs:15:10: error:
     • Expected kind ‘(* -> *) -> Constraint’,
         but ‘MonadReader r r’ has kind ‘Constraint’
     • In the instance declaration for ‘MonadReader r r (Reader' r)’
+
+T2994.hs:15:10: error:
+    • Instance head is not headed by a class:
+        MonadReader r r (Reader' r)
+    • In the instance declaration for ‘MonadReader r r (Reader' r)’
diff --git a/testsuite/tests/typecheck/should_fail/T3540.stderr b/testsuite/tests/typecheck/should_fail/T3540.stderr
index 0fdb88b313..eeb2c051f2 100644
--- a/testsuite/tests/typecheck/should_fail/T3540.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3540.stderr
@@ -3,6 +3,16 @@ T3540.hs:4:12: error:
     • Expected a type, but ‘a ~ Int’ has kind ‘Constraint’
     • In the type signature: thing :: (a ~ Int)
 
+T3540.hs:5:9: error:
+    • Couldn't match kind ‘Constraint’ with ‘*’
+      When matching types
+        a0 :: *
+        a ~ Int :: Constraint
+    • In the expression: undefined
+      In an equation for ‘thing’: thing = undefined
+    • Relevant bindings include
+        thing :: a ~ Int (bound at T3540.hs:5:1)
+
 T3540.hs:7:20: error:
     • Expected a type, but ‘a ~ Int’ has kind ‘Constraint’
     • In the type signature: thing1 :: Int -> (a ~ Int)
diff --git a/testsuite/tests/typecheck/should_fail/T7778.stderr b/testsuite/tests/typecheck/should_fail/T7778.stderr
index a0f10fcd92..1993b772e0 100644
--- a/testsuite/tests/typecheck/should_fail/T7778.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7778.stderr
@@ -1,4 +1,10 @@
 
+T7778.hs:3:6: error:
+    • Illegal qualified type: Num Int => Num
+      A constraint must be a monotype
+      Perhaps you intended to use QuantifiedConstraints
+    • In the type signature: v :: ((Num Int => Num) ()) => ()
+
 T7778.hs:3:7: error:
     • Expected kind ‘* -> Constraint’,
         but ‘Num Int => Num’ has kind ‘*’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail057.stderr b/testsuite/tests/typecheck/should_fail/tcfail057.stderr
index 945c81c1cd..9ddffeb28b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail057.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail057.stderr
@@ -1,5 +1,13 @@
 
 tcfail057.hs:5:7: error:
     • Expected a type, but ‘RealFrac a’ has kind ‘Constraint’
-    • In the type signature:
-        f :: (RealFrac a) -> a -> a
+    • In the type signature: f :: (RealFrac a) -> a -> a
+
+tcfail057.hs:6:7: error:
+    • Couldn't match expected type ‘a -> a’
+                  with actual type ‘RealFrac a’
+    • In the expression: x
+      In an equation for ‘f’: f x = x
+    • Relevant bindings include
+        x :: RealFrac a (bound at tcfail057.hs:6:3)
+        f :: RealFrac a => a -> a (bound at tcfail057.hs:6:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail058.stderr b/testsuite/tests/typecheck/should_fail/tcfail058.stderr
index 478aa7f467..5150637cb9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail058.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail058.stderr
@@ -2,5 +2,24 @@
 tcfail058.hs:6:7: error:
     • Expecting one more argument to ‘Array a’
       Expected a constraint, but ‘Array a’ has kind ‘* -> *’
-    • In the type signature:
-        f :: (Array a) => a -> b
+    • In the type signature: f :: (Array a) => a -> b
+
+tcfail058.hs:7:7: error:
+    • Could not deduce: a ~ b
+      from the context: Array a
+        bound by the type signature for:
+                   f :: forall a b. Array a => a -> b
+        at tcfail058.hs:6:1-24
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. Array a => a -> b
+        at tcfail058.hs:6:1-24
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. Array a => a -> b
+        at tcfail058.hs:6:1-24
+    • In the expression: x
+      In an equation for ‘f’: f x = x
+    • Relevant bindings include
+        x :: a (bound at tcfail058.hs:7:3)
+        f :: a -> b (bound at tcfail058.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail063.stderr b/testsuite/tests/typecheck/should_fail/tcfail063.stderr
index 935390e436..7dd1e9ce02 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail063.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail063.stderr
@@ -2,5 +2,21 @@
 tcfail063.hs:6:9: error:
     • Expecting one more argument to ‘Num’
       Expected a constraint, but ‘Num’ has kind ‘* -> Constraint’
-    • In the type signature:
-        moby :: Num => Int -> a -> Int
+    • In the type signature: moby :: Num => Int -> a -> Int
+
+tcfail063.hs:7:14: error:
+    • Could not deduce: a ~ Int
+      from the context: Num
+        bound by the type signature for:
+                   moby :: forall a. Num => Int -> a -> Int
+        at tcfail063.hs:6:1-30
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          moby :: forall a. Num => Int -> a -> Int
+        at tcfail063.hs:6:1-30
+    • In the second argument of ‘(+)’, namely ‘y’
+      In the expression: x + y
+      In an equation for ‘moby’: moby x y = x + y
+    • Relevant bindings include
+        y :: a (bound at tcfail063.hs:7:8)
+        moby :: Int -> a -> Int (bound at tcfail063.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail078.stderr b/testsuite/tests/typecheck/should_fail/tcfail078.stderr
index 014d589bf6..a0816a746c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail078.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail078.stderr
@@ -2,3 +2,16 @@
 tcfail078.hs:5:6: error:
     • Expected kind ‘* -> Constraint’, but ‘Integer’ has kind ‘*’
     • In the type signature: f :: Integer i => i
+
+tcfail078.hs:6:19: error:
+    • Could not deduce (Num i) arising from the literal ‘0’
+      from the context: Integer i
+        bound by the type signature for:
+                   f :: forall i. Integer i => i
+        at tcfail078.hs:5:1-19
+      Possible fix:
+        add (Num i) to the context of
+          the type signature for:
+            f :: forall i. Integer i => i
+    • In the expression: 0
+      In an equation for ‘f’: f = 0
diff --git a/testsuite/tests/typecheck/should_fail/tcfail113.stderr b/testsuite/tests/typecheck/should_fail/tcfail113.stderr
index fbdffa5ab9..80c97d2737 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail113.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail113.stderr
@@ -4,11 +4,32 @@ tcfail113.hs:12:7: error:
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
     • In the type signature: f :: [Maybe]
 
+tcfail113.hs:13:1: error:
+    • Couldn't match expected type ‘[Maybe]’
+                  with actual type ‘p1 -> p1’
+    • The equation(s) for ‘f’ have one argument,
+      but its type ‘[Maybe]’ has none
+    • Relevant bindings include
+        f :: [Maybe] (bound at tcfail113.hs:13:1)
+
 tcfail113.hs:15:8: error:
     • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the first argument of ‘T’, namely ‘Int’
       In the type signature: g :: T Int
 
+tcfail113.hs:16:1: error:
+    • Couldn't match expected type ‘T Int’ with actual type ‘p0 -> p0’
+    • The equation(s) for ‘g’ have one argument,
+      but its type ‘T Int’ has none
+    • Relevant bindings include g :: T Int (bound at tcfail113.hs:16:1)
+
 tcfail113.hs:18:6: error:
     • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the type signature: h :: Int Int
+
+tcfail113.hs:19:1: error:
+    • Couldn't match type ‘Int’ with ‘(->) Int’
+      Expected type: Int Int
+        Actual type: Int -> Int
+    • The equation(s) for ‘h’ have one argument,
+      but its type ‘Int Int’ has none
diff --git a/testsuite/tests/typecheck/should_fail/tcfail158.stderr b/testsuite/tests/typecheck/should_fail/tcfail158.stderr
index 12f8a4e8df..995be74380 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail158.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail158.stderr
@@ -1,6 +1,3 @@
 
-tcfail158.hs:14:19: error:
-    • Expecting one more argument to ‘Val v’
-      Expected a type, but ‘Val v’ has kind ‘* -> *’
-    • In the type signature:
-        bar :: forall v. Val v
+tcfail158.hs:1:1: error:
+    The IO action ‘main’ is not defined in module ‘Main’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail160.stderr b/testsuite/tests/typecheck/should_fail/tcfail160.stderr
index 46a7640cf9..400b2bf5a4 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail160.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail160.stderr
@@ -2,5 +2,10 @@
 tcfail160.hs:7:8: error:
     • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the first argument of ‘T’, namely ‘Int’
-      In the type signature:
-        g :: T Int
+      In the type signature: g :: T Int
+
+tcfail160.hs:8:1: error:
+    • Couldn't match expected type ‘T Int’ with actual type ‘p0 -> p0’
+    • The equation(s) for ‘g’ have one argument,
+      but its type ‘T Int’ has none
+    • Relevant bindings include g :: T Int (bound at tcfail160.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail161.stderr b/testsuite/tests/typecheck/should_fail/tcfail161.stderr
index ce783bb5ab..89042d1d20 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail161.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail161.stderr
@@ -2,5 +2,12 @@
 tcfail161.hs:5:7: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    • In the type signature:
-        f :: [Maybe]
+    • In the type signature: f :: [Maybe]
+
+tcfail161.hs:6:1: error:
+    • Couldn't match expected type ‘[Maybe]’
+                  with actual type ‘p0 -> p0’
+    • The equation(s) for ‘f’ have one argument,
+      but its type ‘[Maybe]’ has none
+    • Relevant bindings include
+        f :: [Maybe] (bound at tcfail161.hs:6:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail212.stderr b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
index 8eb7e6e57f..8ceab3e931 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail212.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
@@ -2,21 +2,31 @@
 tcfail212.hs:10:7: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    • In the type signature:
-        f :: (Maybe, Either Int)
+    • In the type signature: f :: (Maybe, Either Int)
 
 tcfail212.hs:10:14: error:
     • Expecting one more argument to ‘Either Int’
       Expected a type, but ‘Either Int’ has kind ‘* -> *’
-    • In the type signature:
-        f :: (Maybe, Either Int)
+    • In the type signature: f :: (Maybe, Either Int)
+
+tcfail212.hs:11:6: error:
+    • Couldn't match expected type ‘Maybe’
+                  with actual type ‘Maybe Integer’
+    • In the expression: Just 1
+      In the expression: (Just 1, Left 1)
+      In an equation for ‘f’: f = (Just 1, Left 1)
+
+tcfail212.hs:11:14: error:
+    • Couldn't match expected type ‘Either Int’
+                  with actual type ‘Either Integer b0’
+    • In the expression: Left 1
+      In the expression: (Just 1, Left 1)
+      In an equation for ‘f’: f = (Just 1, Left 1)
 
 tcfail212.hs:13:7: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
-    • In the type signature:
-        g :: (Int#, Int#)
+    • In the type signature: g :: (Int#, Int#)
 
 tcfail212.hs:13:13: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
-    • In the type signature:
-        g :: (Int#, Int#)
+    • In the type signature: g :: (Int#, Int#)