Error message wibbles, following TcErrors refactoring

23 files changed, 402 insertions, 326 deletions

diff --git a/testsuite/tests/gadt/T3651.stderr b/testsuite/tests/gadt/T3651.stderr
index 8f53dc05ef..5d5a4923b5 100644
--- a/testsuite/tests/gadt/T3651.stderr
+++ b/testsuite/tests/gadt/T3651.stderr
@@ -1,35 +1,21 @@
-
-T3651.hs:11:11:
-    Couldn't match type ‛Bool’ with ‛()’
-    Inaccessible code in
-      a pattern with constructor U :: Z (), in an equation for ‛unsafe1’
-    In the pattern: U
-    In an equation for ‛unsafe1’: unsafe1 B U = ()
-
-T3651.hs:11:15:
-    Couldn't match type ‛Bool’ with ‛()’
-    Expected type: a
-      Actual type: ()
-    In the expression: ()
-    In an equation for ‛unsafe1’: unsafe1 B U = ()
-
-T3651.hs:14:11:
-    Couldn't match type ‛Bool’ with ‛()’
-    Inaccessible code in
-      a pattern with constructor U :: Z (), in an equation for ‛unsafe2’
-    In the pattern: U
-    In an equation for ‛unsafe2’: unsafe2 B U = ()
-
-T3651.hs:14:15:
-    Couldn't match type ‛Bool’ with ‛()’
-    Expected type: a
-      Actual type: ()
-    In the expression: ()
-    In an equation for ‛unsafe2’: unsafe2 B U = ()
-
-T3651.hs:17:11:
-    Couldn't match type ‛Bool’ with ‛()’
-    Inaccessible code in
-      a pattern with constructor U :: Z (), in an equation for ‛unsafe3’
-    In the pattern: U
-    In an equation for ‛unsafe3’: unsafe3 B U = True
+

+T3651.hs:11:11:

+    Couldn't match type ‛Bool’ with ‛()’

+    Inaccessible code in

+      a pattern with constructor U :: Z (), in an equation for ‛unsafe1’

+    In the pattern: U

+    In an equation for ‛unsafe1’: unsafe1 B U = ()

+

+T3651.hs:14:11:

+    Couldn't match type ‛Bool’ with ‛()’

+    Inaccessible code in

+      a pattern with constructor U :: Z (), in an equation for ‛unsafe2’

+    In the pattern: U

+    In an equation for ‛unsafe2’: unsafe2 B U = ()

+

+T3651.hs:17:11:

+    Couldn't match type ‛Bool’ with ‛()’

+    Inaccessible code in

+      a pattern with constructor U :: Z (), in an equation for ‛unsafe3’

+    In the pattern: U

+    In an equation for ‛unsafe3’: unsafe3 B U = True

diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
index 52d6afe3e7..7fa660cf13 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
@@ -1,11 +1,25 @@
-
-T3330c.hs:23:43:
-    Couldn't match kind ‛*’ with ‛* -> *’
-    When matching types
-      Der ((->) x) :: * -> *
-      R :: (* -> *) -> *
-    Expected type: Der ((->) x) (f1 x)
-      Actual type: R f1
-    In the first argument of ‛plug’, namely ‛rf’
-    In the first argument of ‛Inl’, namely ‛(plug rf df x)’
-    In the expression: Inl (plug rf df x)
+

+T3330c.hs:23:43:

+    Could not deduce (f1 ~ f1 x)

+    from the context (f ~ (f1 :+: g))

+      bound by a pattern with constructor

+                 RSum :: forall (f :: * -> *) (g :: * -> *).

+                         R f -> R g -> R (f :+: g),

+               in an equation for ‛plug'’

+      at T3330c.hs:23:8-17

+      ‛f1’ is a rigid type variable bound by

+           a pattern with constructor

+             RSum :: forall (f :: * -> *) (g :: * -> *).

+                     R f -> R g -> R (f :+: g),

+           in an equation for ‛plug'’

+           at T3330c.hs:23:8

+    Expected type: Der ((->) x) (f1 x)

+      Actual type: R f1

+    Relevant bindings include

+      plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:23:1)

+      rf :: R f1 (bound at T3330c.hs:23:13)

+      df :: f1 x (bound at T3330c.hs:23:25)

+      x :: x (bound at T3330c.hs:23:29)

+    In the first argument of ‛plug’, namely ‛rf’

+    In the first argument of ‛Inl’, namely ‛(plug rf df x)’

+    In the expression: Inl (plug rf df x)

diff --git a/testsuite/tests/typecheck/should_compile/FD3.stderr b/testsuite/tests/typecheck/should_compile/FD3.stderr
index 9c0a11c36c..664fd35553 100644
--- a/testsuite/tests/typecheck/should_compile/FD3.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD3.stderr
@@ -1,16 +1,5 @@
-
-FD3.hs:15:15:
-    Couldn't match type ‛a’ with ‛(String, a)’
-      ‛a’ is a rigid type variable bound by
-          the type signature for translate :: (String, a) -> A a
-          at FD3.hs:14:14
-    Relevant bindings include
-      translate :: (String, a) -> A a (bound at FD3.hs:15:1)
-      a :: (String, a) (bound at FD3.hs:15:11)
-    When using functional dependencies to combine
-      MkA a a,
-        arising from the dependency ‛a -> b’
-        in the instance declaration at FD3.hs:12:10
-      MkA (String, a) a, arising from a use of ‛mkA’ at FD3.hs:15:15-17
-    In the expression: mkA a
-    In an equation for ‛translate’: translate a = mkA a
+

+FD3.hs:15:15:

+    No instance for (MkA (String, a) a) arising from a use of ‛mkA’

+    In the expression: mkA a

+    In an equation for ‛translate’: translate a = mkA a

diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
index 7538dedda8..c140ba619b 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc211.stderr
@@ -1,35 +1,92 @@
-
-tc211.hs:15:22:
-    Couldn't match type ‛forall a6. a6 -> a6’ with ‛a -> a’
-    Expected type: [a -> a]
-      Actual type: [forall a. a -> a]
-    In the first argument of ‛head’, namely ‛foo’
-    In the first argument of ‛(:) ::
-                                (forall a. a -> a)
-                                -> [forall a. a -> a] -> [forall a. a -> a]’, namely
-      ‛(head foo)’
-    In the expression:
-      ((:) ::
-         (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
-        (head foo) foo
-
-tc211.hs:70:9:
-    Couldn't match type ‛forall a7. a7 -> a7’ with ‛a6 -> a6’
-    Expected type: List (forall a. a -> a)
-                   -> (forall a. a -> a) -> a6 -> a6
-      Actual type: List (forall a. a -> a)
-                   -> (forall a. a -> a) -> forall a. a -> a
-    In the expression:
-        foo2 ::
-          List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)
-    In the expression:
-      (foo2 ::
-         List (forall a. a -> a)
-         -> (forall a. a -> a) -> (forall a. a -> a))
-        xs1 (\ x -> x)
-    In an equation for ‛bar4’:
-        bar4
-          = (foo2 ::
-               List (forall a. a -> a)
-               -> (forall a. a -> a) -> (forall a. a -> a))
-              xs1 (\ x -> x)
+

+tc211.hs:15:22:

+    Couldn't match type ‛forall a6. a6 -> a6’ with ‛a -> a’

+    Expected type: [a -> a]

+      Actual type: [forall a. a -> a]

+    In the first argument of ‛head’, namely ‛foo’

+    In the first argument of ‛(:) ::

+                                (forall a. a -> a)

+                                -> [forall a. a -> a] -> [forall a. a -> a]’, namely

+      ‛(head foo)’

+    In the expression:

+      ((:) ::

+         (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])

+        (head foo) foo

+

+tc211.hs:48:19:

+    Could not deduce (Num a2) arising from the literal ‛3’

+    from the context (Num a)

+      bound by the inferred type of

+               h1 :: Num a => (forall a1. a1 -> a1) -> a

+      at tc211.hs:(47,1)-(49,9)

+    The type variable ‛a2’ is ambiguous

+    Relevant bindings include

+      y :: Pair a2 (Pair a3 b1) (bound at tc211.hs:48:10)

+    Note: there are several potential instances:

+      instance Num Double -- Defined in ‛GHC.Float’

+      instance Num Float -- Defined in ‛GHC.Float’

+      instance Integral a => Num (GHC.Real.Ratio a)

+        -- Defined in ‛GHC.Real’

+      ...plus three others

+    In the first argument of ‛g’, namely ‛3’

+    In the first argument of ‛P’, namely ‛(g 3)’

+    In the expression: P (g 3) (g (P 3 4))

+

+tc211.hs:48:28:

+    Could not deduce (Num a3) arising from the literal ‛3’

+    from the context (Num a)

+      bound by the inferred type of

+               h1 :: Num a => (forall a1. a1 -> a1) -> a

+      at tc211.hs:(47,1)-(49,9)

+    The type variable ‛a3’ is ambiguous

+    Relevant bindings include

+      y :: Pair a2 (Pair a3 b1) (bound at tc211.hs:48:10)

+    Note: there are several potential instances:

+      instance Num Double -- Defined in ‛GHC.Float’

+      instance Num Float -- Defined in ‛GHC.Float’

+      instance Integral a => Num (GHC.Real.Ratio a)

+        -- Defined in ‛GHC.Real’

+      ...plus three others

+    In the first argument of ‛P’, namely ‛3’

+    In the first argument of ‛g’, namely ‛(P 3 4)’

+    In the second argument of ‛P’, namely ‛(g (P 3 4))’

+

+tc211.hs:48:30:

+    Could not deduce (Num b1) arising from the literal ‛4’

+    from the context (Num a)

+      bound by the inferred type of

+               h1 :: Num a => (forall a1. a1 -> a1) -> a

+      at tc211.hs:(47,1)-(49,9)

+    The type variable ‛b1’ is ambiguous

+    Relevant bindings include

+      y :: Pair a2 (Pair a3 b1) (bound at tc211.hs:48:10)

+    Note: there are several potential instances:

+      instance Num Double -- Defined in ‛GHC.Float’

+      instance Num Float -- Defined in ‛GHC.Float’

+      instance Integral a => Num (GHC.Real.Ratio a)

+        -- Defined in ‛GHC.Real’

+      ...plus three others

+    In the second argument of ‛P’, namely ‛4’

+    In the first argument of ‛g’, namely ‛(P 3 4)’

+    In the second argument of ‛P’, namely ‛(g (P 3 4))’

+

+tc211.hs:70:9:

+    Couldn't match type ‛forall a7. a7 -> a7’ with ‛a6 -> a6’

+    Expected type: List (forall a. a -> a)

+                   -> (forall a. a -> a) -> a6 -> a6

+      Actual type: List (forall a. a -> a)

+                   -> (forall a. a -> a) -> forall a. a -> a

+    In the expression:

+        foo2 ::

+          List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)

+    In the expression:

+      (foo2 ::

+         List (forall a. a -> a)

+         -> (forall a. a -> a) -> (forall a. a -> a))

+        xs1 (\ x -> x)

+    In an equation for ‛bar4’:

+        bar4

+          = (foo2 ::

+               List (forall a. a -> a)

+               -> (forall a. a -> a) -> (forall a. a -> a))

+              xs1 (\ x -> x)

diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
index 893ec8ae12..cb47049f06 100644
--- a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
+++ b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
@@ -1,14 +1,10 @@
-
-FDsFromGivens.hs:21:15:
-    Couldn't match type ‛Char’ with ‛[a]’
-    Relevant bindings include
-      bar :: KCC -> a -> a (bound at FDsFromGivens.hs:21:1)
-    When using functional dependencies to combine
-      C Char Char,
-        arising from a pattern with constructor
-                       KCC :: C Char Char => () -> KCC,
-                     in an equation for ‛bar’
-        at FDsFromGivens.hs:21:6-10
-      C Char [a], arising from a use of ‛f’ at FDsFromGivens.hs:21:15
-    In the expression: f
-    In an equation for ‛bar’: bar (KCC _) = f
+

+FDsFromGivens.hs:21:15:

+    Could not deduce (C Char [a]) arising from a use of ‛f’

+    from the context (C Char Char)

+      bound by a pattern with constructor

+                 KCC :: C Char Char => () -> KCC,

+               in an equation for ‛bar’

+      at FDsFromGivens.hs:21:6-10

+    In the expression: f

+    In an equation for ‛bar’: bar (KCC _) = f

diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr
index b95b4f8177..b5244154b6 100644
--- a/testsuite/tests/typecheck/should_fail/T3950.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3950.stderr
@@ -1,16 +1,15 @@
-
-T3950.hs:15:13:
-    Couldn't match kind ‛* -> *’ with ‛*’
-    When matching types
-      w :: (* -> * -> *) -> *
-      Sealed :: (* -> *) -> *
-    Expected type: w (Id p)
-      Actual type: Sealed (Id p0 x0)
-    In the first argument of ‛Just’, namely ‛rp'’
-    In the expression: Just rp'
-    In an equation for ‛rp’:
-        rp _
-          = Just rp'
-          where
-              rp' :: Sealed (Id p x)
-              rp' = undefined
+

+T3950.hs:15:13:

+    Couldn't match type ‛Id p0 x0’ with ‛Id p’

+    Expected type: w (Id p)

+      Actual type: Sealed (Id p0 x0)

+    Relevant bindings include

+      rp :: Bool -> Maybe (w (Id p)) (bound at T3950.hs:15:1)

+    In the first argument of ‛Just’, namely ‛rp'’

+    In the expression: Just rp'

+    In an equation for ‛rp’:

+        rp _

+          = Just rp'

+          where

+              rp' :: Sealed (Id p x)

+              rp' = undefined

diff --git a/testsuite/tests/typecheck/should_fail/T5236.stderr b/testsuite/tests/typecheck/should_fail/T5236.stderr
index b2de3de8d6..f448534b67 100644
--- a/testsuite/tests/typecheck/should_fail/T5236.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5236.stderr
@@ -1,12 +1,5 @@
-
-T5236.hs:13:9:
-    Couldn't match type ‛A’ with ‛B’
-    When using functional dependencies to combine
-      Id A A,
-        arising from the dependency ‛a -> b’
-        in the instance declaration at T5236.hs:10:10
-      Id A B,
-        arising from the type signature for loop :: Id A B => Bool
-        at T5236.hs:13:9-22
-    In the ambiguity check for: Id A B => Bool
-    In the type signature for ‛loop’: loop :: Id A B => Bool
+

+T5236.hs:17:5:

+    No instance for (Id A B) arising from a use of ‛loop’

+    In the expression: loop

+    In an equation for ‛f’: f = loop

diff --git a/testsuite/tests/typecheck/should_fail/T5246.stderr b/testsuite/tests/typecheck/should_fail/T5246.stderr
index f494a4c5b7..fc8e35ef51 100644
--- a/testsuite/tests/typecheck/should_fail/T5246.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5246.stderr
@@ -1,10 +1,9 @@
-
-T5246.hs:11:10:
-    Couldn't match type ‛[Char]’ with ‛Int’
-    When using functional dependencies to combine
-      ?x::[Char],
-        arising from the implicit-parameter bindings for ?x
-        at T5246.hs:(10,7)-(11,12)
-      ?x::Int, arising from a use of ‛foo’ at T5246.hs:11:10-12
-    In the expression: foo
-    In the expression: let ?x = "hello" in foo
+

+T5246.hs:11:10:

+    Could not deduce (?x::Int) arising from a use of ‛foo’

+    from the context (?x::[Char])

+      bound by the implicit-parameter bindings for ?x

+      at T5246.hs:(10,7)-(11,12)

+    In the expression: foo

+    In the expression: let ?x = "hello" in foo

+    In an equation for ‛bar’: bar = let ?x = "hello" in foo

diff --git a/testsuite/tests/typecheck/should_fail/T5570.stderr b/testsuite/tests/typecheck/should_fail/T5570.stderr
index 90f9155afa..7bf7535815 100644
--- a/testsuite/tests/typecheck/should_fail/T5570.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5570.stderr
@@ -1,9 +1,8 @@
-
-T5570.hs:7:16:
-    Couldn't match kind ‛*’ with ‛#’
-    When matching types
-      s0 :: *
-      Double# :: #
-    In the second argument of ‛($)’, namely ‛D# $ 3.0##’
-    In the expression: print $ D# $ 3.0##
-    In an equation for ‛main’: main = print $ D# $ 3.0##
+

+T5570.hs:7:16:

+    Kind incompatibility when matching types:

+      s0 :: *

+      Double# :: #

+    In the second argument of ‛($)’, namely ‛D# $ 3.0##’

+    In the expression: print $ D# $ 3.0##

+    In an equation for ‛main’: main = print $ D# $ 3.0##

diff --git a/testsuite/tests/typecheck/should_fail/T5978.stderr b/testsuite/tests/typecheck/should_fail/T5978.stderr
index e07acd49b1..0deac96834 100644
--- a/testsuite/tests/typecheck/should_fail/T5978.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5978.stderr
@@ -1,10 +1,5 @@
-
-T5978.hs:22:11:
-    Couldn't match type ‛Bool’ with ‛Char’
-    When using functional dependencies to combine
-      C Double Bool,
-        arising from the dependency ‛from -> to’
-        in the instance declaration at T5978.hs:8:10
-      C Double Char, arising from a use of ‛polyBar’ at T5978.hs:22:11-17
-    In the expression: polyBar id monoFoo
-    In an equation for ‛monoBar’: monoBar = polyBar id monoFoo
+

+T5978.hs:22:11:

+    No instance for (C Double Char) arising from a use of ‛polyBar’

+    In the expression: polyBar id monoFoo

+    In an equation for ‛monoBar’: monoBar = polyBar id monoFoo

diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr
index cdb043c10d..091cafb378 100644
--- a/testsuite/tests/typecheck/should_fail/T7368.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368.stderr
@@ -1,18 +1,11 @@
 

 T7368.hs:3:10:

-    Couldn't match kind ‛* -> *’ with ‛*’

-    When matching types

-      b1 :: * -> *

-      b0 :: *

+    Kind incompatibility when matching types:

+      c0 :: (* -> *) -> *

+      (->) a0 :: * -> *

     Expected type: a0 -> b0

-      Actual type: c0 b1

+      Actual type: c0 Maybe

     In the return type of a call of ‛l’

     Probable cause: ‛l’ is applied to too many arguments

-    In the first argument of ‛b’, namely ‛(l ())’

-    In the expression: b (l ())

-

-T7368.hs:3:13:

-    Couldn't match expected type ‛b1 a1’ with actual type ‛()’

-    In the first argument of ‛l’, namely ‛()’

-    In the first argument of ‛b’, namely ‛(l ())’

-    In the expression: b (l ())

+    In the first argument of ‛b’, namely ‛(l Nothing)’

+    In the expression: b (l Nothing)

diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr
index bc193cab05..94d3688d32 100644
--- a/testsuite/tests/typecheck/should_fail/T7368a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr
@@ -1,10 +1,11 @@
-
-T7368a.hs:8:6:
-    Couldn't match kind ‛*’ with ‛* -> *’
-    When matching types
-      f :: * -> *
-      Bad :: (* -> *) -> *
-    Expected type: f (Bad f)
-      Actual type: Bad t0
-    In the pattern: Bad x
-    In an equation for ‛fun’: fun (Bad x) = True
+

+T7368a.hs:8:6:

+    Couldn't match type ‛f’ with ‛Bad’

+      ‛f’ is a rigid type variable bound by

+          the type signature for fun :: f (Bad f) -> Bool at T7368a.hs:7:15

+    Expected type: f (Bad f)

+      Actual type: Bad t0

+    Relevant bindings include

+      fun :: f (Bad f) -> Bool (bound at T7368a.hs:8:1)

+    In the pattern: Bad x

+    In an equation for ‛fun’: fun (Bad x) = True

diff --git a/testsuite/tests/typecheck/should_fail/T7696.stderr b/testsuite/tests/typecheck/should_fail/T7696.stderr
index da30556cd6..b166faa21b 100644
--- a/testsuite/tests/typecheck/should_fail/T7696.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7696.stderr
@@ -1,17 +1,7 @@
-
-T7696.hs:7:6:
-    Couldn't match kind ‛* -> *’ with ‛*’
-    When matching types
-      m0 :: * -> *
-      () :: *
-    Expected type: ((), w ())
-      Actual type: (m0 a0, t0 m0)
-    In the expression: f1
-    In an equation for ‛f2’: f2 = f1
-
-T7696.hs:7:6:
-    Couldn't match type ‛m0 a0’ with ‛()’
-    Expected type: ((), w ())
-      Actual type: (m0 a0, t0 m0)
-    In the expression: f1
-    In an equation for ‛f2’: f2 = f1
+

+T7696.hs:7:6:

+    Couldn't match type ‛m0 a0’ with ‛()’

+    Expected type: ((), w ())

+      Actual type: (m0 a0, t0 m0)

+    In the expression: f1

+    In an equation for ‛f2’: f2 = f1

diff --git a/testsuite/tests/typecheck/should_fail/mc22.stderr b/testsuite/tests/typecheck/should_fail/mc22.stderr
index 7a4cc4e44b..3a149fdcba 100644
--- a/testsuite/tests/typecheck/should_fail/mc22.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc22.stderr
@@ -1,11 +1,22 @@
-
-mc22.hs:10:26:
-    Couldn't match type ‛a’ with ‛t a’
-      ‛a’ is a rigid type variable bound by
-          a type expected by the context: [a] -> [t a] at mc22.hs:10:9
-    Expected type: [a] -> [t a]
-      Actual type: [a] -> [a]
-    Relevant bindings include foo :: [t [Char]] (bound at mc22.hs:8:1)
-    In the return type of a call of ‛take’
-    In the expression: take 5
-    In a stmt of a monad comprehension: then group using take 5
+

+mc22.hs:10:9:

+    No instance for (Functor t) arising from a use of ‛fmap’

+    Possible fix:

+      add (Functor t) to the context of

+        a type expected by the context: (a -> b) -> t a -> t b

+        or the inferred type of foo :: [t [Char]]

+    In the expression: fmap

+    In a stmt of a monad comprehension: then group using take 5

+    In the expression:

+      [x + 1 | x <- ["Hello", "World"], then group using take 5]

+

+mc22.hs:10:26:

+    Couldn't match type ‛a’ with ‛t a’

+      ‛a’ is a rigid type variable bound by

+          a type expected by the context: [a] -> [t a] at mc22.hs:10:9

+    Expected type: [a] -> [t a]

+      Actual type: [a] -> [a]

+    Relevant bindings include foo :: [t [Char]] (bound at mc22.hs:8:1)

+    In the return type of a call of ‛take’

+    In the expression: take 5

+    In a stmt of a monad comprehension: then group using take 5

diff --git a/testsuite/tests/typecheck/should_fail/mc25.stderr b/testsuite/tests/typecheck/should_fail/mc25.stderr
index 855ec1eb18..52b40c75dd 100644
--- a/testsuite/tests/typecheck/should_fail/mc25.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc25.stderr
@@ -1,9 +1,19 @@
-
-mc25.hs:9:46:
-    Couldn't match type ‛Int’ with ‛a -> t’
-    Expected type: (a -> t) -> [a] -> [t1 a]
-      Actual type: Int -> [a] -> [a]
-    Relevant bindings include z :: [t1 t] (bound at mc25.hs:9:1)
-    In the expression: take
-    In a stmt of a monad comprehension: then group by x using take
-    In the expression: [x | x <- [1 .. 10], then group by x using take]
+

+mc25.hs:9:24:

+    No instance for (Functor t1) arising from a use of ‛fmap’

+    Possible fix:

+      add (Functor t1) to the context of

+        a type expected by the context: (a -> b) -> t1 a -> t1 b

+        or the inferred type of z :: [t1 t]

+    In the expression: fmap

+    In a stmt of a monad comprehension: then group by x using take

+    In the expression: [x | x <- [1 .. 10], then group by x using take]

+

+mc25.hs:9:46:

+    Couldn't match type ‛Int’ with ‛a -> t’

+    Expected type: (a -> t) -> [a] -> [t1 a]

+      Actual type: Int -> [a] -> [a]

+    Relevant bindings include z :: [t1 t] (bound at mc25.hs:9:1)

+    In the expression: take

+    In a stmt of a monad comprehension: then group by x using take

+    In the expression: [x | x <- [1 .. 10], then group by x using take]

diff --git a/testsuite/tests/typecheck/should_fail/tcfail090.stderr b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
index 622e181401..1c43e12436 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail090.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
@@ -1,8 +1,7 @@
-
-tcfail090.hs:8:9:
-    Couldn't match kind ‛*’ with ‛#’
-    When matching types
-      a0 :: *
-      ByteArray# :: #
-    In the expression: undefined
-    In an equation for ‛die’: die _ = undefined
+

+tcfail090.hs:8:9:

+    Kind incompatibility when matching types:

+      a0 :: *

+      ByteArray# :: #

+    In the expression: undefined

+    In an equation for ‛die’: die _ = undefined

diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
index ec0f6a33bd..9e07184677 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
@@ -1,17 +1,18 @@
-
-tcfail122.hs:8:9:
-    Couldn't match kind ‛* -> *’ with ‛*’
-    When matching types
-      d0 :: * -> *
-      b :: *
-    Expected type: a b
-      Actual type: c0 d0
-    In the expression:
-        undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d
-    In the expression:
-      [undefined :: forall a b. a b,
-       undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d]
-    In an equation for ‛foo’:
-        foo
-          = [undefined :: forall a b. a b,
-             undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d]
+

+tcfail122.hs:8:9:

+    Kind incompatibility when matching types:

+      c0 :: (* -> *) -> *

+      a0 :: * -> *

+    Expected type: a0 b0

+      Actual type: c0 d0

+    Relevant bindings include

+      foo :: [a0 b0] (bound at tcfail122.hs:7:1)

+    In the expression:

+        undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d

+    In the expression:

+      [undefined :: forall a b. a b,

+       undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d]

+    In an equation for ‛foo’:

+        foo

+          = [undefined :: forall a b. a b,

+             undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d]

diff --git a/testsuite/tests/typecheck/should_fail/tcfail123.stderr b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
index 2a70414aaf..510d1db490 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail123.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
@@ -1,9 +1,8 @@
-
-tcfail123.hs:11:9:
-    Couldn't match kind ‛*’ with ‛#’
-    When matching types
-      t0 :: *
-      GHC.Prim.Int# :: #
-    In the first argument of ‛f’, namely ‛3#’
-    In the expression: f 3#
-    In an equation for ‛h’: h v = f 3#
+

+tcfail123.hs:11:9:

+    Kind incompatibility when matching types:

+      t0 :: *

+      GHC.Prim.Int# :: #

+    In the first argument of ‛f’, namely ‛3#’

+    In the expression: f 3#

+    In an equation for ‛h’: h v = f 3#

diff --git a/testsuite/tests/typecheck/should_fail/tcfail143.stderr b/testsuite/tests/typecheck/should_fail/tcfail143.stderr
index dadccbe781..7c1cc92d60 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail143.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail143.stderr
@@ -1,11 +1,5 @@
-
-tcfail143.hs:29:9:
-    Couldn't match type ‛S Z’ with ‛Z’
-    When using functional dependencies to combine
-      MinMax a Z Z a,
-        arising from the dependency ‛a b -> c d’
-        in the instance declaration at tcfail143.hs:11:10
-      MinMax (S Z) Z Z Z,
-        arising from a use of ‛extend’ at tcfail143.hs:29:9-16
-    In the expression: n1 `extend` n0
-    In an equation for ‛t2’: t2 = n1 `extend` n0
+

+tcfail143.hs:29:9:

+    No instance for (MinMax (S Z) Z Z Z) arising from a use of ‛extend’

+    In the expression: n1 `extend` n0

+    In an equation for ‛t2’: t2 = n1 `extend` n0

diff --git a/testsuite/tests/typecheck/should_fail/tcfail159.stderr b/testsuite/tests/typecheck/should_fail/tcfail159.stderr
index 3ff73d8c72..9154e4383e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail159.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail159.stderr
@@ -1,9 +1,8 @@
-
-tcfail159.hs:9:11:
-    Couldn't match kind ‛*’ with ‛#’
-    When matching types
-      t0 :: *
-      (# Int, Int #) :: #
-    In the pattern: ~(# p, q #)
-    In a case alternative: ~(# p, q #) -> p
-    In the expression: case h x of { ~(# p, q #) -> p }
+

+tcfail159.hs:9:11:

+    Kind incompatibility when matching types:

+      t0 :: *

+      (# Int, Int #) :: #

+    In the pattern: ~(# p, q #)

+    In a case alternative: ~(# p, q #) -> p

+    In the expression: case h x of { ~(# p, q #) -> p }

diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
index 56442b867f..cdf21761f7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
@@ -1,7 +1,35 @@
-
-tcfail174.hs:9:10:
-    Couldn't match expected type ‛forall a. a -> a’
-                with actual type ‛a0 -> a0’
-    In the first argument of ‛Base’, namely ‛id’
-    In the expression: Base id
-    In an equation for ‛g’: g = Base id
+

+tcfail174.hs:9:10:

+    Couldn't match expected type ‛forall a. a -> a’

+                with actual type ‛a0 -> a0’

+    In the first argument of ‛Base’, namely ‛id’

+    In the expression: Base id

+    In an equation for ‛g’: g = Base id

+

+tcfail174.hs:13:14:

+    Couldn't match type ‛a’ with ‛a1’

+      because type variable ‛a1’ would escape its scope

+    This (rigid, skolem) type variable is bound by

+      the type forall a2. a2 -> a2

+      at tcfail174.hs:13:14

+    Expected type: Capture (forall x. x -> a)

+      Actual type: Capture (forall a. a -> a)

+    Relevant bindings include

+      h1 :: Capture a (bound at tcfail174.hs:13:1)

+    In the first argument of ‛Capture’, namely ‛g’

+    In the expression: Capture g

+    In an equation for ‛h1’: h1 = Capture g

+

+tcfail174.hs:16:14:

+    Couldn't match type ‛a’ with ‛b’

+      ‛a’ is a rigid type variable bound by

+          the type forall a1. a1 -> a1 at tcfail174.hs:16:14

+      ‛b’ is a rigid type variable bound by

+          the type signature for h2 :: Capture b at tcfail174.hs:15:7

+    Expected type: Capture (forall x. x -> b)

+      Actual type: Capture (forall a. a -> a)

+    Relevant bindings include

+      h2 :: Capture b (bound at tcfail174.hs:16:1)

+    In the first argument of ‛Capture’, namely ‛g’

+    In the expression: Capture g

+    In an equation for ‛h2’: h2 = Capture g

diff --git a/testsuite/tests/typecheck/should_fail/tcfail200.stderr b/testsuite/tests/typecheck/should_fail/tcfail200.stderr
index 57c174d109..f6d80a249a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail200.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail200.stderr
@@ -1,9 +1,11 @@
-
-tcfail200.hs:5:15:
-    Couldn't match kind ‛*’ with ‛#’
-    When matching types
-      t1 :: *
-      GHC.Prim.Int# :: #
-    In the expression: 1#
-    In the expression: (1#, 'c')
-    In an equation for ‛x’: x = (1#, 'c')
+

+tcfail200.hs:5:15:

+    Kind incompatibility when matching types:

+      t0 :: *

+      GHC.Prim.Int# :: #

+    Relevant bindings include

+      f :: (t0, Char) (bound at tcfail200.hs:5:1)

+      x :: (t0, Char) (bound at tcfail200.hs:5:9)

+    In the expression: 1#

+    In the expression: (1#, 'c')

+    In an equation for ‛x’: x = (1#, 'c')

diff --git a/testsuite/tests/typecheck/should_fail/tcfail206.stderr b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
index d503b16207..5a30f93e81 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail206.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
@@ -1,28 +1,50 @@
-
-tcfail206.hs:5:5:
-    Couldn't match type ‛Bool’ with ‛Int’
-    Expected type: Bool -> (Int, Bool)
-      Actual type: Bool -> (Bool, Bool)
-    In the expression: (, True)
-    In an equation for ‛a’: a = (, True)
-
-tcfail206.hs:8:5:
-    Couldn't match type ‛(t0, Int)’ with ‛Bool -> (Int, Bool)’
-    Expected type: Int -> Bool -> (Int, Bool)
-      Actual type: Int -> (t0, Int)
-    In the expression: (1,)
-    In an equation for ‛b’: b = (1,)
-
-tcfail206.hs:14:5:
-    Couldn't match type ‛Bool’ with ‛Int’
-    Expected type: Bool -> (# Int, Bool #)
-      Actual type: Bool -> (# Bool, Bool #)
-    In the expression: (# , True #)
-    In an equation for ‛d’: d = (# , True #)
-
-tcfail206.hs:17:5:
-    Couldn't match type ‛(# a0, Int #)’ with ‛Bool -> (# Int, Bool #)’
-    Expected type: Int -> Bool -> (# Int, Bool #)
-      Actual type: Int -> (# a0, Int #)
-    In the expression: (# 1, #)
-    In an equation for ‛e’: e = (# 1, #)
+

+tcfail206.hs:5:5:

+    Couldn't match type ‛Bool’ with ‛Int’

+    Expected type: Bool -> (Int, Bool)

+      Actual type: Bool -> (Bool, Bool)

+    In the expression: (, True)

+    In an equation for ‛a’: a = (, True)

+

+tcfail206.hs:8:5:

+    Couldn't match type ‛(t0, Int)’ with ‛Bool -> (Int, Bool)’

+    Expected type: Int -> Bool -> (Int, Bool)

+      Actual type: Int -> (t0, Int)

+    In the expression: (1,)

+    In an equation for ‛b’: b = (1,)

+

+tcfail206.hs:11:5:

+    Couldn't match type ‛a’ with ‛Bool’

+      ‛a’ is a rigid type variable bound by

+          the type signature for c :: a -> (a, Bool) at tcfail206.hs:10:6

+    Expected type: a -> (a, Bool)

+      Actual type: a -> (a, a)

+    Relevant bindings include

+      c :: a -> (a, Bool) (bound at tcfail206.hs:11:1)

+    In the expression: (True || False,)

+    In an equation for ‛c’: c = (True || False,)

+

+tcfail206.hs:14:5:

+    Couldn't match type ‛Bool’ with ‛Int’

+    Expected type: Bool -> (# Int, Bool #)

+      Actual type: Bool -> (# Bool, Bool #)

+    In the expression: (# , True #)

+    In an equation for ‛d’: d = (# , True #)

+

+tcfail206.hs:17:5:

+    Couldn't match type ‛(# a0, Int #)’ with ‛Bool -> (# Int, Bool #)’

+    Expected type: Int -> Bool -> (# Int, Bool #)

+      Actual type: Int -> (# a0, Int #)

+    In the expression: (# 1, #)

+    In an equation for ‛e’: e = (# 1, #)

+

+tcfail206.hs:20:5:

+    Couldn't match type ‛a’ with ‛Bool’

+      ‛a’ is a rigid type variable bound by

+          the type signature for f :: a -> (# a, Bool #) at tcfail206.hs:19:6

+    Expected type: a -> (# a, Bool #)

+      Actual type: a -> (# a, a #)

+    Relevant bindings include

+      f :: a -> (# a, Bool #) (bound at tcfail206.hs:20:1)

+    In the expression: (# True || False, #)

+    In an equation for ‛f’: f = (# True || False, #)