Fail fast in solveLocalEqualities

This patch makes us fail fast in TcSimplify.solveLocalEqualities,
and in TcHsType.tc_hs_sig_type, if there are insoluble constraints.

Previously we ploughed on even if there were insoluble constraints,
leading to a cascade of hard-to-understand type errors. Failing
eagerly is much better; hence a lot of testsuite error message
changes.  Eg if we have
          f :: [Maybe] -> blah
          f xs = e
then trying typecheck 'f x = e' with an utterly bogus type
is just asking for trouble.

I can't quite remember what provoked me to make this change,
but I think the error messages are notably improved, by
removing confusing clutter and focusing on the real error.

22 files changed, 28 insertions, 441 deletions

diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr
index a8e64d4e0c..0201005943 100644
--- a/testsuite/tests/dependent/should_fail/DepFail1.stderr
+++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr
@@ -4,23 +4,7 @@ DepFail1.hs:7:6: error:
       Expected a type, but ‘Proxy Bool’ has kind ‘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
-
-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/ghci/scripts/T15898.stderr b/testsuite/tests/ghci/scripts/T15898.stderr
index 11ca6cc142..aeda5ba5fe 100644
--- a/testsuite/tests/ghci/scripts/T15898.stderr
+++ b/testsuite/tests/ghci/scripts/T15898.stderr
@@ -1,12 +1,4 @@
 
-<interactive>:3:1: error:
-    • Couldn't match kind ‘()’ with ‘*’
-      When matching types
-        a0 :: *
-        '() :: ()
-    • In the expression: undefined :: '()
-      In an equation for ‘it’: it = undefined :: '()
-
 <interactive>:3:14: error:
     • Expected a type, but ‘'()’ has kind ‘()’
     • In an expression type signature: '()
@@ -19,34 +11,14 @@
       In the expression: undefined :: Proxy '() Int
       In an equation for ‘it’: it = undefined :: Proxy '() Int
 
-<interactive>:5:1: error:
-    • Couldn't match kind ‘[*]’ with ‘*’
-      When matching types
-        a0 :: *
-        '[(), ()] :: [*]
-    • In the expression: undefined :: [(), ()]
-      In an equation for ‘it’: it = undefined :: [(), ()]
-
 <interactive>:5:14: error:
     • Expected a type, but ‘[(), ()]’ has kind ‘[*]’
     • In an expression type signature: [(), ()]
       In the expression: undefined :: [(), ()]
       In an equation for ‘it’: it = undefined :: [(), ()]
 
-<interactive>:6:1: error:
-    • Couldn't match kind ‘([k0], [k1])’ with ‘*’
-      When matching types
-        a0 :: *
-        '( '[], '[]) :: ([k0], [k1])
-    • In the expression: undefined :: '( '[], '[])
-      In an equation for ‘it’: it = undefined :: '( '[], '[])
-    • Relevant bindings include
-        it :: '( '[], '[]) (bound at <interactive>:6:1)
-
 <interactive>:6:14: error:
     • Expected a type, but ‘'( '[], '[])’ has kind ‘([k0], [k1])’
     • In an expression type signature: '( '[], '[])
       In the expression: undefined :: '( '[], '[])
       In an equation for ‘it’: it = undefined :: '( '[], '[])
-    • Relevant bindings include
-        it :: '( '[], '[]) (bound at <interactive>:6:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T13877.stderr b/testsuite/tests/indexed-types/should_fail/T13877.stderr
index 9dc8534ca1..674b258c24 100644
--- a/testsuite/tests/indexed-types/should_fail/T13877.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13877.stderr
@@ -1,25 +1,7 @@
 
-T13877.hs:65:17: error:
-    • Couldn't match type ‘Apply p (x : xs)’ with ‘p (x : xs)’
-      Expected type: Sing x
-                     -> Sing xs
-                     -> App [a1] (':->) * p xs
-                     -> App [a1] (':->) * p (x : xs)
-        Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
-    • In the expression: listElimPoly @(:->) @a @p @l
-      In an equation for ‘listElimTyFun’:
-          listElimTyFun = listElimPoly @(:->) @a @p @l
-    • Relevant bindings include
-        listElimTyFun :: Sing l
-                         -> (p @@ '[])
-                         -> (forall (x :: a1) (xs :: [a1]).
-                             Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-                         -> p @@ l
-          (bound at T13877.hs:65:1)
-
 T13877.hs:65:41: error:
     • Expecting one more argument to ‘p’
-      Expected kind ‘(-?>) [a1] * (':->)’, but ‘p’ has kind ‘[a1] ~> *’
+      Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
     • In the type ‘p’
       In the expression: listElimPoly @(:->) @a @p @l
       In an equation for ‘listElimTyFun’:
@@ -27,7 +9,7 @@ T13877.hs:65:41: error:
     • Relevant bindings include
         listElimTyFun :: Sing l
                          -> (p @@ '[])
-                         -> (forall (x :: a1) (xs :: [a1]).
+                         -> (forall (x :: a) (xs :: [a]).
                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
                          -> p @@ l
           (bound at T13877.hs:65:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T11976.stderr b/testsuite/tests/partial-sigs/should_fail/T11976.stderr
index c4c3d50e59..bcc69bf2d8 100644
--- a/testsuite/tests/partial-sigs/should_fail/T11976.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T11976.stderr
@@ -1,17 +1,6 @@
 
-T11976.hs:7:7: error:
-    • Cannot instantiate unification variable ‘a0’
-      with a type involving foralls: Lens _3 _4 _5
-        GHC doesn't yet support impredicative polymorphism
-    • In the expression: undefined :: Lens _ _ _
-      In an equation for ‘foo’: foo = undefined :: Lens _ _ _
-    • Relevant bindings include
-        foo :: Lens _ _1 _2 (bound at T11976.hs:7:1)
-
 T11976.hs:7:20: error:
     • Expected kind ‘k0 -> *’, but ‘Lens _ _’ has kind ‘*’
     • In the type ‘Lens _ _ _’
       In an expression type signature: Lens _ _ _
       In the expression: undefined :: Lens _ _ _
-    • Relevant bindings include
-        foo :: Lens _ _1 _2 (bound at T11976.hs:7:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T12634.stderr b/testsuite/tests/partial-sigs/should_fail/T12634.stderr
index 7aab25f5f8..4287110149 100644
--- a/testsuite/tests/partial-sigs/should_fail/T12634.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T12634.stderr
@@ -1,31 +1,10 @@
 
-T12634.hs:14:19: error:
-    • Found type wildcard ‘_’ standing for ‘()’
-      To use the inferred type, enable PartialTypeSignatures
-    • In the type signature:
-        bench_twacePow :: forall t m m' r.
-                          _ => t m' r -> Bench '(t, m, m', r)
-
 T12634.hs:14:58: error:
     • Expected a type, but
       ‘'(t, m, m', r)’ has kind
-      ‘(* -> * -> *, *, *, *)’
+      ‘(k1 -> k2 -> *, k0, k1, k2)’
     • In the first argument of ‘Bench’, namely ‘'(t, m, m', r)’
       In the type ‘t m' r -> Bench '(t, m, m', r)’
       In the type signature:
         bench_twacePow :: forall t m m' r.
                           _ => t m' r -> Bench '(t, m, m', r)
-
-T12634.hs:15:18: error:
-    • Couldn't match kind ‘(* -> * -> *, *, *, *)’ with ‘*’
-      When matching types
-        params0 :: *
-        '(t, m, m', r) :: (* -> * -> *, *, *, *)
-      Expected type: t m' r -> Bench '(t, m, m', r)
-        Actual type: t m' r -> Bench params0
-    • In the expression: bench (twacePowDec :: t m' r -> t m r)
-      In an equation for ‘bench_twacePow’:
-          bench_twacePow = bench (twacePowDec :: t m' r -> t m r)
-    • Relevant bindings include
-        bench_twacePow :: t m' r -> Bench '(t, m, m', r)
-          (bound at T12634.hs:15:1)
diff --git a/testsuite/tests/patsyn/should_fail/T15289.stderr b/testsuite/tests/patsyn/should_fail/T15289.stderr
index 952d358692..64cc153ff8 100644
--- a/testsuite/tests/patsyn/should_fail/T15289.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15289.stderr
@@ -1,10 +1,4 @@
 
-T15289.hs:5:16: error:
-    • Couldn't match expected type ‘Maybe’ with actual type ‘Bool’
-    • In the pattern: True
-      In the pattern: True :: Maybe
-      In the declaration for pattern synonym ‘What’
-
 T15289.hs:5:24: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index e150299ea1..fcf194ba50 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -1,116 +1,11 @@
 
-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
-      ‘(((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-       -> Constraint’
+      ‘((k0 -> Constraint) -> k1 -> *) -> Constraint’
     • In the kind ‘k’
       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:40: error:
-    • Expecting two more arguments to ‘k1’
-      Expected a type, but
-      ‘k1’ has kind
-      ‘((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *’
-    • In the kind ‘k1’
-      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:47: error:
-    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-                            -> (k3 -> k4 -> *) -> *)
-                           -> Constraint’
-                     with ‘*’
-      When matching kinds
-        k3 :: *
-        k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-              -> Constraint
-    • In the first argument of ‘p’, namely ‘c’
-      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:49: error:
-    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-                           -> (k3 -> k4 -> *) -> *’
-                     with ‘*’
-      When matching kinds
-        k4 :: *
-        k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
-    • In the second argument of ‘p’, 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:12:56: error:
-    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-                            -> (k3 -> k4 -> *) -> *)
-                           -> Constraint’
-                     with ‘*’
-      When matching kinds
-        k0 :: *
-        k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-              -> Constraint
-    • In the first argument of ‘q’, namely ‘c’
-      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:58: error:
-    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-                           -> (k3 -> k4 -> *) -> *’
-                     with ‘*’
-      When matching kinds
-        k1 :: *
-        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 k k4 k8 p a b
-               -> (forall (c :: k) (d :: k4). 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 k k4 k8 p a b
-               -> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b
-          (bound at T12593.hs:14:1)
diff --git a/testsuite/tests/polykinds/T15577.stderr b/testsuite/tests/polykinds/T15577.stderr
index fef17090f8..5478da8b4a 100644
--- a/testsuite/tests/polykinds/T15577.stderr
+++ b/testsuite/tests/polykinds/T15577.stderr
@@ -7,65 +7,3 @@ T15577.hs:20:18: error:
                      an equation for ‘g’:
         Refl <- f @f @a @r r
       In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
-
-T15577.hs:20:21: error:
-    • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
-    • In the type ‘a’
-      In a stmt of a pattern guard for
-                     an equation for ‘g’:
-        Refl <- f @f @a @r r
-      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
-    • Relevant bindings include
-        r :: Proxy r1 (bound at T15577.hs:18:3)
-        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
-
-T15577.hs:20:24: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching kinds
-        f1 :: * -> *
-        f1 a1 :: *
-      Expected kind ‘f1’, but ‘r’ has kind ‘f1 a1’
-    • In the type ‘r’
-      In a stmt of a pattern guard for
-                     an equation for ‘g’:
-        Refl <- f @f @a @r r
-      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
-    • Relevant bindings include
-        r :: Proxy r1 (bound at T15577.hs:18:3)
-        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
-
-T15577.hs:20:26: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching kinds
-        f1 :: * -> *
-        a1 :: *
-    • In the fourth argument of ‘f’, namely ‘r’
-      In a stmt of a pattern guard for
-                     an equation for ‘g’:
-        Refl <- f @f @a @r r
-      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
-    • Relevant bindings include
-        r :: Proxy r1 (bound at T15577.hs:18:3)
-        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
-
-T15577.hs:21:7: error:
-    • Could not deduce: F r1 ~ r1
-      from the context: r0 ~ F r0
-        bound by a pattern with constructor:
-                   Refl :: forall k (a :: k). a :~: a,
-                 in a pattern binding in
-                      a pattern guard for
-                        an equation for ‘g’
-        at T15577.hs:18:7-10
-      ‘r1’ is a rigid type variable bound by
-        the type signature for:
-          g :: forall (f1 :: * -> *) a1 (r1 :: f1 a1).
-               Proxy r1 -> F r1 :~: r1
-        at T15577.hs:17:1-76
-      Expected type: F r1 :~: r1
-        Actual type: r1 :~: r1
-    • In the expression: Refl
-      In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
-    • Relevant bindings include
-        r :: Proxy r1 (bound at T15577.hs:18:3)
-        g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
diff --git a/testsuite/tests/typecheck/should_fail/T11112.stderr b/testsuite/tests/typecheck/should_fail/T11112.stderr
index 304078158e..db6e1822cb 100644
--- a/testsuite/tests/typecheck/should_fail/T11112.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11112.stderr
@@ -2,12 +2,3 @@
 T11112.hs:3:9: error:
     • Expected a type, but ‘Ord s’ has kind ‘Constraint’
     • 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/T13819.stderr b/testsuite/tests/typecheck/should_fail/T13819.stderr
index 89959cba39..917345f710 100644
--- a/testsuite/tests/typecheck/should_fail/T13819.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13819.stderr
@@ -1,15 +1,4 @@
 
-T13819.hs:12:10: error:
-    • Couldn't match type ‘_0 -> A _0’ with ‘A a’
-      Expected type: a -> A a
-        Actual type: (_1 -> WrappedMonad A _2) (_0 -> A _0)
-    • In the expression: pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
-      In an equation for ‘pure’:
-          pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
-      In the instance declaration for ‘Applicative A’
-    • Relevant bindings include
-        pure :: a -> A a (bound at T13819.hs:12:3)
-
 T13819.hs:12:17: error:
     • Expected kind ‘* -> *’, but ‘_ -> WrappedMonad A _’ has kind ‘*’
     • In the type ‘(_ -> WrappedMonad A _)’
diff --git a/testsuite/tests/typecheck/should_fail/T14232.stderr b/testsuite/tests/typecheck/should_fail/T14232.stderr
index 1ca41f0bd5..a497be7b19 100644
--- a/testsuite/tests/typecheck/should_fail/T14232.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14232.stderr
@@ -2,16 +2,3 @@
 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/T3540.stderr b/testsuite/tests/typecheck/should_fail/T3540.stderr
index eeb2c051f2..0fdb88b313 100644
--- a/testsuite/tests/typecheck/should_fail/T3540.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3540.stderr
@@ -3,16 +3,6 @@ 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 1993b772e0..a0f10fcd92 100644
--- a/testsuite/tests/typecheck/should_fail/T7778.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7778.stderr
@@ -1,10 +1,4 @@
 
-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/T8806.stderr b/testsuite/tests/typecheck/should_fail/T8806.stderr
index f0043a3edb..a0cc76ec46 100644
--- a/testsuite/tests/typecheck/should_fail/T8806.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8806.stderr
@@ -1,10 +1,8 @@
 
 T8806.hs:5:6: error:
     • Expected a constraint, but ‘Int’ has kind ‘*’
-    • In the type signature:
-        f :: Int => Int
+    • In the type signature: f :: Int => Int
 
 T8806.hs:8:7: error:
     • Expected a constraint, but ‘Int’ has kind ‘*’
-    • In the type signature:
-        g :: (Int => Show a) => Int
+    • In the type signature: g :: (Int => Show a) => Int
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
index 6cb1f442a7..a9958016ce 100644
--- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -25,17 +25,6 @@ VtaFail.hs:26:15: error:
       In the expression: first @Int F
       In an equation for ‘fInt’: fInt = first @Int F
 
-VtaFail.hs:26:19: error:
-    • Couldn't match kind ‘*’ with ‘* -> *’
-      When matching types
-        a1 :: * -> *
-        Int :: *
-      Expected type: First Int
-        Actual type: First a1
-    • In the second argument of ‘first’, namely ‘F’
-      In the expression: first @Int F
-      In an equation for ‘fInt’: fInt = first @Int F
-
 VtaFail.hs:33:18: error:
     • Couldn't match type ‘Int’ with ‘Bool’
       Expected type: Proxy Bool
@@ -50,17 +39,6 @@ VtaFail.hs:40:17: error:
       In the expression: too @Maybe T
       In an equation for ‘threeBad’: threeBad = too @Maybe T
 
-VtaFail.hs:40:23: error:
-    • Couldn't match kind ‘*’ with ‘k0 -> *’
-      When matching types
-        a0 :: * -> k0 -> *
-        Maybe :: * -> *
-      Expected type: Three Maybe
-        Actual type: Three a0
-    • In the second argument of ‘too’, namely ‘T’
-      In the expression: too @Maybe T
-      In an equation for ‘threeBad’: threeBad = too @Maybe T
-
 VtaFail.hs:41:27: error:
     • Couldn't match type ‘Either’ with ‘(->)’
       Expected type: Three (->)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail057.stderr b/testsuite/tests/typecheck/should_fail/tcfail057.stderr
index 9ddffeb28b..4229e2fc38 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail057.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail057.stderr
@@ -2,12 +2,3 @@
 tcfail057.hs:5:7: error:
     • Expected a type, but ‘RealFrac a’ has kind ‘Constraint’
     • 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 5150637cb9..a0ad07ea1f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail058.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail058.stderr
@@ -3,23 +3,3 @@ 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
-
-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 7dd1e9ce02..a3347122e7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail063.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail063.stderr
@@ -3,20 +3,3 @@ 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
-
-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/tcfail113.stderr b/testsuite/tests/typecheck/should_fail/tcfail113.stderr
index 80c97d2737..fbdffa5ab9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail113.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail113.stderr
@@ -4,32 +4,11 @@ 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/tcfail160.stderr b/testsuite/tests/typecheck/should_fail/tcfail160.stderr
index 400b2bf5a4..96f2b4701c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail160.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail160.stderr
@@ -3,9 +3,3 @@ 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
-
-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 89042d1d20..b07d6031a6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail161.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail161.stderr
@@ -3,11 +3,3 @@ tcfail161.hs:5:7: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
     • 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 8ceab3e931..ad5985e63a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail212.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
@@ -9,20 +9,6 @@ tcfail212.hs:10:14: error:
       Expected a type, but ‘Either Int’ has kind ‘* -> *’
     • 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#)
@@ -30,3 +16,25 @@ tcfail212.hs:13:7: error:
 tcfail212.hs:13:13: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
     • In the type signature: g :: (Int#, Int#)
+
+tcfail212.hs:14:6: error:
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        a :: *
+        Int# :: TYPE 'IntRep
+    • In the expression: 1#
+      In the expression: (1#, 2#)
+      In an equation for ‘g’: g = (1#, 2#)
+    • Relevant bindings include
+        g :: (a, b) (bound at tcfail212.hs:14:1)
+
+tcfail212.hs:14:10: error:
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        b :: *
+        Int# :: TYPE 'IntRep
+    • In the expression: 2#
+      In the expression: (1#, 2#)
+      In an equation for ‘g’: g = (1#, 2#)
+    • Relevant bindings include
+        g :: (a, b) (bound at tcfail212.hs:14:1)