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.

2 files changed, 1 insertions, 168 deletions

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)