From a9cbd3eb28190035d6bf1acb82b27c968295b98e Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 28 Sep 2012 15:55:22 +0100
Subject: [PATCH] Tons of error message wibbles

---
 tests/arrows/should_fail/T5380.stderr         |   2 +-
 tests/arrows/should_fail/arrowfail001.stderr  |  13 +--
 tests/deriving/should_fail/T5287.hs           |   1 +
 tests/deriving/should_fail/T5287.stderr       |   2 +
 tests/deriving/should_fail/drvfail002.stderr  |   2 -
 tests/gadt/T3169.stderr                       |  18 ---
 tests/generics/GenCannotDoRep0.stderr         |   2 +-
 tests/ghci/scripts/Defer02.stderr             |  68 +++++------
 .../should_fail/GADTwrong1.stderr             |   6 +-
 tests/indexed-types/should_fail/T1900.stderr  |   2 +-
 tests/indexed-types/should_fail/T2627b.stderr |   2 +-
 tests/indexed-types/should_fail/T3330c.stderr |   7 +-
 tests/indexed-types/should_fail/T3440.stderr  |   8 +-
 tests/module/mod54.stderr                     |   5 +-
 tests/polykinds/T6054.stderr                  |   2 -
 tests/simplCore/should_run/T3591.stderr       |  16 +++
 tests/th/T5358.stderr                         |  31 ++++-
 tests/typecheck/should_compile/FD2.stderr     |  10 +-
 tests/typecheck/should_compile/FD3.stderr     |   3 +
 tests/typecheck/should_compile/tc141.stderr   |  16 +--
 .../typecheck/should_fail/FrozenErrorTests.hs | 109 +++++++++---------
 .../should_fail/FrozenErrorTests.stderr       |  53 ++++-----
 tests/typecheck/should_fail/T2688.stderr      |   6 +-
 tests/typecheck/should_fail/T3950.stderr      |  12 +-
 tests/typecheck/should_fail/T5570.stderr      |   5 +-
 tests/typecheck/should_fail/T5684.stderr      |  14 ---
 tests/typecheck/should_fail/T5689.stderr      |   2 +-
 tests/typecheck/should_fail/T5853.stderr      |   2 +-
 tests/typecheck/should_fail/tcfail032.stderr  |   2 +-
 tests/typecheck/should_fail/tcfail065.stderr  |   4 +-
 tests/typecheck/should_fail/tcfail090.stderr  |   4 +-
 tests/typecheck/should_fail/tcfail099.stderr  |  13 +--
 tests/typecheck/should_fail/tcfail122.stderr  |  14 ++-
 tests/typecheck/should_fail/tcfail123.hs      |   3 +-
 tests/typecheck/should_fail/tcfail123.stderr  |   7 +-
 tests/typecheck/should_fail/tcfail133.stderr  |   6 +-
 tests/typecheck/should_fail/tcfail159.stderr  |   5 +-
 tests/typecheck/should_fail/tcfail174.stderr  |  28 -----
 tests/typecheck/should_fail/tcfail175.stderr  |   4 +-
 tests/typecheck/should_fail/tcfail179.stderr  |   4 +-
 tests/typecheck/should_fail/tcfail192.stderr  |   8 --
 tests/typecheck/should_fail/tcfail198.stderr  |   8 +-
 tests/typecheck/should_fail/tcfail200.stderr  |   7 +-
 tests/typecheck/should_fail/tcfail206.stderr  |  22 ----
 44 files changed, 247 insertions(+), 311 deletions(-)

diff --git a/tests/arrows/should_fail/T5380.stderr b/tests/arrows/should_fail/T5380.stderr
index 36cf8a4ff..1d3fa3a1e 100644
--- a/tests/arrows/should_fail/T5380.stderr
+++ b/tests/arrows/should_fail/T5380.stderr
@@ -1,6 +1,6 @@
 
 T5380.hs:7:27:
-    Couldn't match expected type `not_bool' with actual type `Bool'
+    Couldn't match expected type `Bool' with actual type `not_bool'
       `not_bool' is a rigid type variable bound by
                  the type signature for
                    testB :: not_bool -> (() -> ()) -> () -> not_unit
diff --git a/tests/arrows/should_fail/arrowfail001.stderr b/tests/arrows/should_fail/arrowfail001.stderr
index 5ba0efdfa..261aa278a 100644
--- a/tests/arrows/should_fail/arrowfail001.stderr
+++ b/tests/arrows/should_fail/arrowfail001.stderr
@@ -1,17 +1,6 @@
 
-arrowfail001.hs:16:27:
-    Couldn't match expected type `a0' with actual type `a'
-      because type variable `a' would escape its scope
-    This (rigid, skolem) type variable is bound by
-      a pattern with constructor
-        Bar :: forall a. Foo a => a -> Bar,
-      in a case alternative
-    In the pattern: Bar a
-    In a case alternative: Bar a -> foo -< a
-    In the command: case x of { Bar a -> foo -< a }
-
 arrowfail001.hs:16:36:
-    No instance for (Foo a0) arising from a use of `foo'
+    No instance for (Foo a) arising from a use of `foo'
     In the expression: foo
     In the expression: proc x -> case x of { Bar a -> foo -< a }
     In an equation for `get':
diff --git a/tests/deriving/should_fail/T5287.hs b/tests/deriving/should_fail/T5287.hs
index 5db2d85ed..cb1259ca0 100644
--- a/tests/deriving/should_fail/T5287.hs
+++ b/tests/deriving/should_fail/T5287.hs
@@ -4,5 +4,6 @@ class A a oops
 data D d = D d
 instance A a oops => Read (D a)
 data E e = E (D e) deriving Read
+instance A Int Bool
 
 
diff --git a/tests/deriving/should_fail/T5287.stderr b/tests/deriving/should_fail/T5287.stderr
index e95212f67..d74166e7a 100644
--- a/tests/deriving/should_fail/T5287.stderr
+++ b/tests/deriving/should_fail/T5287.stderr
@@ -4,6 +4,8 @@ T5287.hs:6:29:
       arising from the 'deriving' clause of a data type declaration
     The type variable `oops' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
+    Note: there is a potential instance available:
+      instance A Int Bool -- Defined at T5287.hs:7:10
     Possible fix:
       use a standalone 'deriving instance' declaration,
         so you can specify the instance context yourself
diff --git a/tests/deriving/should_fail/drvfail002.stderr b/tests/deriving/should_fail/drvfail002.stderr
index 4594fe927..20d54c678 100644
--- a/tests/deriving/should_fail/drvfail002.stderr
+++ b/tests/deriving/should_fail/drvfail002.stderr
@@ -2,8 +2,6 @@
 drvfail002.hs:19:23:
     No instance for (X T c)
       arising from the 'deriving' clause of a data type declaration
-    The type variable `c' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     Possible fix:
       use a standalone 'deriving instance' declaration,
         so you can specify the instance context yourself
diff --git a/tests/gadt/T3169.stderr b/tests/gadt/T3169.stderr
index f256f8cbf..62f49d467 100644
--- a/tests/gadt/T3169.stderr
+++ b/tests/gadt/T3169.stderr
@@ -1,22 +1,4 @@
 
-T3169.hs:13:22:
-    Could not deduce (Map a ~ MP a b)
-    from the context (Key a, Key b)
-      bound by the instance declaration at T3169.hs:10:10-36
-    Expected type: Map a (Map b elt)
-      Actual type: Map (a, b) elt
-    Relevant bindings include
-      lookup :: (a, b) -> Map (a, b) elt -> Maybe elt
-        (bound at T3169.hs:12:3)
-      a :: a (bound at T3169.hs:12:11)
-      b :: b (bound at T3169.hs:12:13)
-      m :: Map (a, b) elt (bound at T3169.hs:12:17)
-    In the second argument of `lookup', namely `m'
-    In the expression: lookup a m :: Maybe (Map b elt)
-    In the expression:
-      case lookup a m :: Maybe (Map b elt) of {
-        Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
-
 T3169.hs:13:22:
     Could not deduce (elt ~ Map b elt)
     from the context (Key a, Key b)
diff --git a/tests/generics/GenCannotDoRep0.stderr b/tests/generics/GenCannotDoRep0.stderr
index 291ab14b5..e222819e9 100644
--- a/tests/generics/GenCannotDoRep0.stderr
+++ b/tests/generics/GenCannotDoRep0.stderr
@@ -9,7 +9,7 @@ GenCannotDoRep0.hs:13:45:
 
 GenCannotDoRep0.hs:17:1:
     Can't make a derived instance of `Generic (P Int)':
-      P must not be instantiated; try deriving `P a' instead
+      P must not be instantiated; try deriving `P Int' instead
     In the stand-alone deriving instance for `Generic (P Int)'
 
 GenCannotDoRep0.hs:26:1:
diff --git a/tests/ghci/scripts/Defer02.stderr b/tests/ghci/scripts/Defer02.stderr
index 189b4b7f9..28f859669 100644
--- a/tests/ghci/scripts/Defer02.stderr
+++ b/tests/ghci/scripts/Defer02.stderr
@@ -12,58 +12,37 @@
     In the expression: 'p'
     In an equation for `a': a = 'p'
 
-../../typecheck/should_run/Defer01.hs:18:9: Warning:
-    No instance for (Eq B) arising from a use of `=='
-    Possible fix: add an instance declaration for (Eq B)
-    In the expression: x == x
-    In an equation for `b': b x = x == x
-
-../../typecheck/should_run/Defer01.hs:28:5: Warning:
-    No instance for (Num (a -> a)) arising from the literal `1'
-    Possible fix: add an instance declaration for (Num (a -> a))
-    In the expression: 1
-    In an equation for `d': d = 1
+../../typecheck/should_run/Defer01.hs:25:4: Warning:
+    Couldn't match type `Int' with `Bool'
+    Inaccessible code in
+      a pattern with constructor
+        C2 :: Bool -> C Bool,
+      in an equation for `c'
+    In the pattern: C2 x
+    In an equation for `c': c (C2 x) = True
 
 ../../typecheck/should_run/Defer01.hs:31:5: Warning:
     Couldn't match expected type `Char -> t' with actual type `Char'
+    Relevant bindings include
+      f :: t (bound at ../../typecheck/should_run/Defer01.hs:31:1)
     The function `e' is applied to one argument,
     but its type `Char' has none
     In the expression: e 'q'
     In an equation for `f': f = e 'q'
 
-../../typecheck/should_run/Defer01.hs:34:8: Warning:
-    Couldn't match expected type `a' with actual type `Char'
-      `a' is a rigid type variable bound by
-          the type signature for h :: a -> (Char, Char)
-          at ../../typecheck/should_run/Defer01.hs:33:6
-    In the expression: x
-    In the expression: (x, 'c')
-    In an equation for `h': h x = (x, 'c')
-
 ../../typecheck/should_run/Defer01.hs:39:17: Warning:
     Couldn't match expected type `Bool' with actual type `T a'
+    Relevant bindings include
+      i :: a -> () (bound at ../../typecheck/should_run/Defer01.hs:39:1)
+      a :: a (bound at ../../typecheck/should_run/Defer01.hs:39:3)
     In the return type of a call of `K'
     In the first argument of `not', namely `(K a)'
     In the expression: (not (K a))
 
-../../typecheck/should_run/Defer01.hs:43:5: Warning:
-    No instance for (MyClass a1) arising from a use of `myOp'
-    In the expression: myOp 23
-    In an equation for `j': j = myOp 23
-
-../../typecheck/should_run/Defer01.hs:43:10: Warning:
-    No instance for (Num a1) arising from the literal `23'
-    The type variable `a1' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
-    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 `myOp', namely `23'
-    In the expression: myOp 23
-    In an equation for `j': j = myOp 23
+../../typecheck/should_run/Defer01.hs:45:6: Warning:
+    Couldn't match type `Int' with `Bool'
+    Inaccessible code in
+      the type signature for k :: Int ~ Bool => Int -> Bool
 
 ../../typecheck/should_run/Defer01.hs:46:7: Warning:
     Couldn't match expected type `Bool' with actual type `Int'
@@ -91,7 +70,6 @@
 (deferred type error)
 *** Exception: ../../typecheck/should_run/Defer01.hs:18:9:
     No instance for (Eq B) arising from a use of `=='
-    Possible fix: add an instance declaration for (Eq B)
     In the expression: x == x
     In an equation for `b': b x = x == x
 (deferred type error)
@@ -105,28 +83,36 @@
     In the first argument of `print', namely `(c (C2 True))'
 *** Exception: ../../typecheck/should_run/Defer01.hs:28:5:
     No instance for (Num (a -> a)) arising from the literal `1'
-    Possible fix: add an instance declaration for (Num (a -> a))
     In the expression: 1
     In an equation for `d': d = 1
 (deferred type error)
 *** Exception: ../../typecheck/should_run/Defer01.hs:31:5:
     Couldn't match expected type `Char -> t' with actual type `Char'
+    Relevant bindings include
+      f :: t (bound at ../../typecheck/should_run/Defer01.hs:31:1)
     The function `e' is applied to one argument,
     but its type `Char' has none
     In the expression: e 'q'
     In an equation for `f': f = e 'q'
 (deferred type error)
 *** Exception: ../../typecheck/should_run/Defer01.hs:34:8:
-    Couldn't match expected type `a' with actual type `Char'
+    Couldn't match expected type `Char' with actual type `a'
       `a' is a rigid type variable bound by
           the type signature for h :: a -> (Char, Char)
           at ../../typecheck/should_run/Defer01.hs:33:6
+    Relevant bindings include
+      h :: a -> (Char, Char)
+        (bound at ../../typecheck/should_run/Defer01.hs:34:1)
+      x :: a (bound at ../../typecheck/should_run/Defer01.hs:34:3)
     In the expression: x
     In the expression: (x, 'c')
     In an equation for `h': h x = (x, 'c')
 (deferred type error)
 *** Exception: ../../typecheck/should_run/Defer01.hs:39:17:
     Couldn't match expected type `Bool' with actual type `T a'
+    Relevant bindings include
+      i :: a -> () (bound at ../../typecheck/should_run/Defer01.hs:39:1)
+      a :: a (bound at ../../typecheck/should_run/Defer01.hs:39:3)
     In the return type of a call of `K'
     In the first argument of `not', namely `(K a)'
     In the expression: (not (K a))
diff --git a/tests/indexed-types/should_fail/GADTwrong1.stderr b/tests/indexed-types/should_fail/GADTwrong1.stderr
index a90b09d6e..9c5465f27 100644
--- a/tests/indexed-types/should_fail/GADTwrong1.stderr
+++ b/tests/indexed-types/should_fail/GADTwrong1.stderr
@@ -1,18 +1,18 @@
 
 GADTwrong1.hs:12:19:
-    Could not deduce (b ~ a1)
+    Could not deduce (a1 ~ b)
     from the context (() ~ Const a1)
       bound by a pattern with constructor
                  T :: forall a. a -> T (Const a),
                in a case alternative
       at GADTwrong1.hs:12:12-14
-      `b' is a rigid type variable bound by
-          the type signature for coerce :: a -> b at GADTwrong1.hs:10:20
       `a1' is a rigid type variable bound by
            a pattern with constructor
              T :: forall a. a -> T (Const a),
            in a case alternative
            at GADTwrong1.hs:12:12
+      `b' is a rigid type variable bound by
+          the type signature for coerce :: a -> b at GADTwrong1.hs:10:20
     Relevant bindings include
       coerce :: a -> b (bound at GADTwrong1.hs:11:1)
       y :: a1 (bound at GADTwrong1.hs:12:14)
diff --git a/tests/indexed-types/should_fail/T1900.stderr b/tests/indexed-types/should_fail/T1900.stderr
index c170c984d..93b566d97 100644
--- a/tests/indexed-types/should_fail/T1900.stderr
+++ b/tests/indexed-types/should_fail/T1900.stderr
@@ -6,7 +6,7 @@ T1900.hs:11:12:
     In the instance declaration for `Bug Int'
 
 T1900.hs:14:16:
-    Could not deduce (Depend s ~ Depend s0)
+    Could not deduce (Depend s0 ~ Depend s)
     from the context (Bug s)
       bound by the type signature for check :: Bug s => Depend s -> Bool
       at T1900.hs:13:10-36
diff --git a/tests/indexed-types/should_fail/T2627b.stderr b/tests/indexed-types/should_fail/T2627b.stderr
index 0338bf620..e18a8d230 100644
--- a/tests/indexed-types/should_fail/T2627b.stderr
+++ b/tests/indexed-types/should_fail/T2627b.stderr
@@ -1,6 +1,6 @@
 
 T2627b.hs:20:24:
-    Couldn't match expected type `a0' with actual type `Dual (Dual a0)'
+    Couldn't match expected type `Dual (Dual a0)' with actual type `a0'
       `a0' is untouchable
         inside the constraints (b ~ W a2 b2)
         bound by a pattern with constructor
diff --git a/tests/indexed-types/should_fail/T3330c.stderr b/tests/indexed-types/should_fail/T3330c.stderr
index c9b6348e7..8c657c811 100644
--- a/tests/indexed-types/should_fail/T3330c.stderr
+++ b/tests/indexed-types/should_fail/T3330c.stderr
@@ -1,10 +1,11 @@
 
 T3330c.hs:23:43:
     Couldn't match kind `*' with `* -> *'
-    Expected type: Der ((->) x) (f1 x)
-      Actual type: R f1
-    Kind incompatibility when matching types:
+    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)
diff --git a/tests/indexed-types/should_fail/T3440.stderr b/tests/indexed-types/should_fail/T3440.stderr
index 55b021b64..b9f49fa0b 100644
--- a/tests/indexed-types/should_fail/T3440.stderr
+++ b/tests/indexed-types/should_fail/T3440.stderr
@@ -1,19 +1,19 @@
 
 T3440.hs:11:22:
-    Could not deduce (a ~ a1)
+    Could not deduce (a1 ~ a)
     from the context (Fam a ~ Fam a1)
       bound by a pattern with constructor
                  GADT :: forall a. a -> Fam a -> GADT (Fam a),
                in an equation for `unwrap'
       at T3440.hs:11:9-16
-      `a' is a rigid type variable bound by
-          the type signature for unwrap :: GADT (Fam a) -> (a, Fam a)
-          at T3440.hs:10:11
       `a1' is a rigid type variable bound by
            a pattern with constructor
              GADT :: forall a. a -> Fam a -> GADT (Fam a),
            in an equation for `unwrap'
            at T3440.hs:11:9
+      `a' is a rigid type variable bound by
+          the type signature for unwrap :: GADT (Fam a) -> (a, Fam a)
+          at T3440.hs:10:11
     Relevant bindings include
       unwrap :: GADT (Fam a) -> (a, Fam a) (bound at T3440.hs:11:1)
       x :: a1 (bound at T3440.hs:11:14)
diff --git a/tests/module/mod54.stderr b/tests/module/mod54.stderr
index 8b41e7f8b..2670b53e2 100644
--- a/tests/module/mod54.stderr
+++ b/tests/module/mod54.stderr
@@ -3,7 +3,6 @@ mod54.hs:3:22:
     No instance for (Eq T)
       arising from the 'deriving' clause of a data type declaration
     Possible fix:
-      add an instance declaration for (Eq T)
-      or use a standalone 'deriving instance' declaration,
-           so you can specify the instance context yourself
+      use a standalone 'deriving instance' declaration,
+        so you can specify the instance context yourself
     When deriving the instance for (Ord T)
diff --git a/tests/polykinds/T6054.stderr b/tests/polykinds/T6054.stderr
index 8270f4dd4..bc034d313 100644
--- a/tests/polykinds/T6054.stderr
+++ b/tests/polykinds/T6054.stderr
@@ -2,8 +2,6 @@
 T6054.hs:7:14:
     No instance for (Bar () '() a0)
       arising from an expression type signature
-    The type variable `a0' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     In the first argument of `print', namely
       `(Proxy :: Bar () a => Proxy a)'
     In the expression: print (Proxy :: Bar () a => Proxy a)
diff --git a/tests/simplCore/should_run/T3591.stderr b/tests/simplCore/should_run/T3591.stderr
index 3fcef522a..de1d02019 100644
--- a/tests/simplCore/should_run/T3591.stderr
+++ b/tests/simplCore/should_run/T3591.stderr
@@ -51,9 +51,17 @@ fmap await
 fmap await
 fmap await
 liftOut
+liftOut
+inject suspend
+liftFunctor id
+calling fmap
+fmap Either
+poking a
+fmap RightF
 fmap Either
 fmap RightF
 fmap await
+fmap await
 bounce start
 bounce end
 liftOut
@@ -177,9 +185,17 @@ fmap await
 fmap await
 fmap await
 liftOut
+liftOut
+inject suspend
+liftFunctor id
+calling fmap
+fmap Either
+poking a
+fmap RightF
 fmap Either
 fmap RightF
 fmap await
+fmap await
 bounce start
 bounce end
 bounce start
diff --git a/tests/th/T5358.stderr b/tests/th/T5358.stderr
index 01f1ffa60..5c9e68ca0 100644
--- a/tests/th/T5358.stderr
+++ b/tests/th/T5358.stderr
@@ -1,3 +1,11 @@
+Loading package ghc-prim ... linking ... done.
+Loading package integer-gmp ... linking ... done.
+Loading package base ... linking ... done.
+Loading package array-0.4.0.1 ... linking ... done.
+Loading package deepseq-1.3.0.1 ... linking ... done.
+Loading package containers-0.5.0.0 ... linking ... done.
+Loading package pretty-1.1.1.0 ... linking ... done.
+Loading package template-haskell ... linking ... done.
 
 T5358.hs:7:1:
     Couldn't match expected type `t1 -> t1' with actual type `Int'
@@ -10,15 +18,34 @@ T5358.hs:8:1:
     but its type `Int' has none
 
 T5358.hs:10:13:
-    Couldn't match expected type `t0 -> a0' with actual type `Int'
+    Couldn't match expected type `t -> a0' with actual type `Int'
+    Relevant bindings include
+      prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
+      x :: t (bound at T5358.hs:10:9)
     The function `t1' is applied to one argument,
     but its type `Int' has none
     In the first argument of `(==)', namely `t1 x'
     In the expression: t1 x == t2 x
 
 T5358.hs:10:21:
-    Couldn't match expected type `t0 -> a0' with actual type `Int'
+    Couldn't match expected type `t -> a0' with actual type `Int'
+    Relevant bindings include
+      prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
+      x :: t (bound at T5358.hs:10:9)
     The function `t2' is applied to one argument,
     but its type `Int' has none
     In the second argument of `(==)', namely `t2 x'
     In the expression: t1 x == t2 x
+
+T5358.hs:12:15:
+    Exception when trying to run compile-time code:
+      runTest called error: forall t_0 . t_0 -> GHC.Types.Bool
+      Code: do { VarI _ t _ _ <- reify (mkName "prop_x1");
+                 ($) error ((++) "runTest called error: " pprint t) }
+    In the expression:
+      $(do { VarI _ t _ _ <- reify (mkName "prop_x1");
+             error $ ("runTest called error: " ++ pprint t) })
+    In an equation for `runTests':
+        runTests
+          = $(do { VarI _ t _ _ <- reify (mkName "prop_x1");
+                   error $ ("runTest called error: " ++ pprint t) })
diff --git a/tests/typecheck/should_compile/FD2.stderr b/tests/typecheck/should_compile/FD2.stderr
index d23dd33e6..8822c1ccb 100644
--- a/tests/typecheck/should_compile/FD2.stderr
+++ b/tests/typecheck/should_compile/FD2.stderr
@@ -1,6 +1,6 @@
 
 FD2.hs:26:34:
-    Could not deduce (e1 ~ e)
+    Could not deduce (e ~ e1)
     from the context (Foldable a)
       bound by the class declaration for `Foldable'
       at FD2.hs:(17,1)-(26,39)
@@ -12,14 +12,14 @@ FD2.hs:26:34:
       bound by the type signature for
                  mf :: Elem a e1 => e1 -> Maybe e1 -> Maybe e1
       at FD2.hs:24:18-54
-      `e1' is a rigid type variable bound by
-           the type signature for
-             mf :: Elem a e1 => e1 -> Maybe e1 -> Maybe e1
-           at FD2.hs:24:18
       `e' is a rigid type variable bound by
           the type signature for
             foldr1 :: Elem a e => (e -> e -> e) -> a -> e
           at FD2.hs:21:13
+      `e1' is a rigid type variable bound by
+           the type signature for
+             mf :: Elem a e1 => e1 -> Maybe e1 -> Maybe e1
+           at FD2.hs:24:18
     Relevant bindings include
       foldr1 :: (e -> e -> e) -> a -> e (bound at FD2.hs:22:3)
       f :: e -> e -> e (bound at FD2.hs:22:10)
diff --git a/tests/typecheck/should_compile/FD3.stderr b/tests/typecheck/should_compile/FD3.stderr
index 00b0a816a..ad849e6b0 100644
--- a/tests/typecheck/should_compile/FD3.stderr
+++ b/tests/typecheck/should_compile/FD3.stderr
@@ -4,6 +4,9 @@ FD3.hs:15:15:
       `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'
diff --git a/tests/typecheck/should_compile/tc141.stderr b/tests/typecheck/should_compile/tc141.stderr
index 1942963d3..e7d7f7cb1 100644
--- a/tests/typecheck/should_compile/tc141.stderr
+++ b/tests/typecheck/should_compile/tc141.stderr
@@ -8,10 +8,10 @@ tc141.hs:11:12:
 
 tc141.hs:11:31:
     Couldn't match expected type `a1' with actual type `a'
-      `a1' is a rigid type variable bound by
-           an expression type signature: a1 at tc141.hs:11:31
-      `a' is a rigid type variable bound by
-          the inferred type of f :: (a, a) -> (t, a) at tc141.hs:11:1
+      because type variable `a1' would escape its scope
+    This (rigid, skolem) type variable is bound by
+      an expression type signature: a1
+      at tc141.hs:11:31-34
     Relevant bindings include
       f :: (a, a) -> (t, a) (bound at tc141.hs:11:1)
       x :: (a, a) (bound at tc141.hs:11:3)
@@ -35,10 +35,10 @@ tc141.hs:13:13:
 
 tc141.hs:15:18:
     Couldn't match expected type `a2' with actual type `t'
-      `a2' is a rigid type variable bound by
-           the type signature for v :: a2 at tc141.hs:14:19
-      `t' is a rigid type variable bound by
-          the inferred type of g :: a -> t -> a1 at tc141.hs:13:1
+      because type variable `a2' would escape its scope
+    This (rigid, skolem) type variable is bound by
+      the type signature for v :: a2
+      at tc141.hs:14:19
     Relevant bindings include
       g :: a -> t -> a1 (bound at tc141.hs:13:1)
       b :: t (bound at tc141.hs:13:5)
diff --git a/tests/typecheck/should_fail/FrozenErrorTests.hs b/tests/typecheck/should_fail/FrozenErrorTests.hs
index bea549551..479087b0d 100644
--- a/tests/typecheck/should_fail/FrozenErrorTests.hs
+++ b/tests/typecheck/should_fail/FrozenErrorTests.hs
@@ -1,56 +1,53 @@
-{-# LANGUAGE RankNTypes, GADTs, TypeFamilies #-}
-module Test where 
-
-
-data T a where 
-  MkT :: a -> T a 
-  MkT2 :: forall a b. (b ~ T b) => b -> T a
-  MkT3 :: forall a. (a ~ Bool) => T a 
--- Occurs checks in givens
-foo :: forall a. (a ~ T a) => a -> a 
-foo x = x 
-
-blah x = case x of 
-           MkT2 y -> ()
-
--- Mismatches in givens 
-bloh :: T Int -> () 
-bloh x = case x of 
-           MkT3 -> () 
-
-type family F a b 
-type family G a b
-type instance F a Bool = a 
-type instance G a Char = a
-
-goo1 :: forall a b. (F a b ~ [a]) => b -> a  -> a
-goo1 = undefined 
-
-goo2 :: forall a. G a Char ~ [Int] => a -> a
-goo2 = undefined
-
--- Just an occurs check
-test1 = goo1 False undefined
-
--- A frozen occurs check, now transformed to decomposition error
-test2 = goo2 (goo1 False undefined)
-test3 = goo1 False (goo2 undefined)
-
-
--- A frozen occurs check, now transformed to both a decomposition and occurs check
-data M a where 
-  M :: M a 
-data T2 a b where
-  T2 :: T2 a b 
-
-goo3 :: forall a b. F a b ~ T2 (M a) a => b -> a -> a 
-goo3 = undefined
-
-goo4 :: forall a c. G a Char ~ T2 (T2 c c) c => a -> a
-goo4 = undefined 
-
-test4 = goo4 (goo3 False undefined)
-test5 = goo3 False (goo4 undefined)
-
-
-
+{-# LANGUAGE RankNTypes, GADTs, TypeFamilies #-}
+module Test where 
+
+
+data T a where 
+  MkT :: a -> T a 
+  MkT3 :: forall a. (a ~ Bool) => T a 
+
+-- Occurs checks in givens
+foo :: forall a. (a ~ T a) => a -> a 
+foo x = x 
+
+-- Mismatches in givens 
+bloh :: T Int -> () 
+bloh x = case x of 
+           MkT3 -> () 
+
+type family F a b 
+type family G a b
+type instance F a Bool = a 
+type instance G a Char = a
+
+goo1 :: forall a b. (F a b ~ [a]) => b -> a  -> a
+goo1 = undefined 
+
+goo2 :: forall a. G a Char ~ [Int] => a -> a
+goo2 = undefined
+
+-- Just an occurs check
+test1 = goo1 False undefined
+
+-- A frozen occurs check, now transformed to decomposition error
+test2 = goo2 (goo1 False undefined)
+test3 = goo1 False (goo2 undefined)
+
+
+-- A frozen occurs check, now transformed to both a decomposition and occurs check
+data M a where 
+  M :: M a 
+data T2 a b where
+  T2 :: T2 a b 
+
+goo3 :: forall a b. F a b ~ T2 (M a) a => b -> a -> a 
+goo3 = undefined
+
+goo4 :: forall a c. G a Char ~ T2 (T2 c c) c => a -> a
+goo4 = undefined 
+
+test4 = goo4 (goo3 False undefined)
+test5 = goo3 False (goo4 undefined)
+
+
+
diff --git a/tests/typecheck/should_fail/FrozenErrorTests.stderr b/tests/typecheck/should_fail/FrozenErrorTests.stderr
index d4ce2ce00..0e2ec6c2f 100644
--- a/tests/typecheck/should_fail/FrozenErrorTests.stderr
+++ b/tests/typecheck/should_fail/FrozenErrorTests.stderr
@@ -7,22 +7,7 @@ FrozenErrorTests.hs:10:8:
     Inaccessible code in
       the type signature for foo :: a ~ T a => a -> a
 
-FrozenErrorTests.hs:14:12:
-    Couldn't match type `b' with `T b'
-      `b' is a rigid type variable bound by
-          a pattern with constructor
-            MkT2 :: forall a b. b ~ T b => b -> T a,
-          in a case alternative
-          at FrozenErrorTests.hs:14:12
-    Inaccessible code in
-      a pattern with constructor
-        MkT2 :: forall a b. b ~ T b => b -> T a,
-      in a case alternative
-    In the pattern: MkT2 y
-    In a case alternative: MkT2 y -> ()
-    In the expression: case x of { MkT2 y -> () }
-
-FrozenErrorTests.hs:19:12:
+FrozenErrorTests.hs:16:12:
     Couldn't match type `Int' with `Bool'
     Inaccessible code in
       a pattern with constructor
@@ -32,14 +17,16 @@ FrozenErrorTests.hs:19:12:
     In a case alternative: MkT3 -> ()
     In the expression: case x of { MkT3 -> () }
 
-FrozenErrorTests.hs:33:9:
-    Occurs check: cannot construct the infinite type: a0 = [a0]
-    Expected type: [a0]
-      Actual type: F a0 Bool
+FrozenErrorTests.hs:30:9:
+    Occurs check: cannot construct the infinite type: a ~ [a]
+    Expected type: [a]
+      Actual type: F a Bool
+    Relevant bindings include
+      test1 :: a (bound at FrozenErrorTests.hs:30:1)
     In the expression: goo1 False undefined
     In an equation for `test1': test1 = goo1 False undefined
 
-FrozenErrorTests.hs:36:15:
+FrozenErrorTests.hs:33:15:
     Couldn't match type `Int' with `[Int]'
     Expected type: [[Int]]
       Actual type: F [Int] Bool
@@ -47,24 +34,28 @@ FrozenErrorTests.hs:36:15:
     In the expression: goo2 (goo1 False undefined)
     In an equation for `test2': test2 = goo2 (goo1 False undefined)
 
-FrozenErrorTests.hs:37:9:
-    Couldn't match type `[Int]' with `Int'
+FrozenErrorTests.hs:34:9:
+    Couldn't match type `Int' with `[Int]'
     Expected type: [[Int]]
       Actual type: F [Int] Bool
     In the expression: goo1 False (goo2 undefined)
     In an equation for `test3': test3 = goo1 False (goo2 undefined)
 
-FrozenErrorTests.hs:52:15:
-    Couldn't match type `T2 c0 c0' with `M (T2 (T2 c0 c0) c0)'
-    Expected type: T2 (M (T2 (T2 c0 c0) c0)) (T2 (T2 c0 c0) c0)
-      Actual type: F (T2 (T2 c0 c0) c0) Bool
+FrozenErrorTests.hs:49:15:
+    Couldn't match type `T2 c c' with `M (T2 (T2 c c) c)'
+    Expected type: T2 (M (T2 (T2 c c) c)) (T2 (T2 c c) c)
+      Actual type: F (T2 (T2 c c) c) Bool
+    Relevant bindings include
+      test4 :: T2 (T2 c c) c (bound at FrozenErrorTests.hs:49:1)
     In the first argument of `goo4', namely `(goo3 False undefined)'
     In the expression: goo4 (goo3 False undefined)
     In an equation for `test4': test4 = goo4 (goo3 False undefined)
 
-FrozenErrorTests.hs:53:9:
-    Couldn't match type `T2 c0 c0' with `M (T2 (T2 c0 c0) c0)'
-    Expected type: T2 (M (T2 (T2 c0 c0) c0)) (T2 (T2 c0 c0) c0)
-      Actual type: F (T2 (T2 c0 c0) c0) Bool
+FrozenErrorTests.hs:50:9:
+    Couldn't match type `T2 c c' with `M (T2 (T2 c c) c)'
+    Expected type: T2 (M (T2 (T2 c c) c)) (T2 (T2 c c) c)
+      Actual type: F (T2 (T2 c c) c) Bool
+    Relevant bindings include
+      test5 :: T2 (T2 c c) c (bound at FrozenErrorTests.hs:50:1)
     In the expression: goo3 False (goo4 undefined)
     In an equation for `test5': test5 = goo3 False (goo4 undefined)
diff --git a/tests/typecheck/should_fail/T2688.stderr b/tests/typecheck/should_fail/T2688.stderr
index b937de07b..3bb0f4934 100644
--- a/tests/typecheck/should_fail/T2688.stderr
+++ b/tests/typecheck/should_fail/T2688.stderr
@@ -1,13 +1,13 @@
 
 T2688.hs:8:22:
-    Could not deduce (v ~ s)
+    Could not deduce (s ~ v)
     from the context (VectorSpace v s)
       bound by the class declaration for `VectorSpace'
       at T2688.hs:(5,1)-(8,23)
-      `v' is a rigid type variable bound by
-          the class declaration for `VectorSpace' at T2688.hs:5:19
       `s' is a rigid type variable bound by
           the class declaration for `VectorSpace' at T2688.hs:5:21
+      `v' is a rigid type variable bound by
+          the class declaration for `VectorSpace' at T2688.hs:5:19
     Relevant bindings include
       ^/ :: v -> s -> v (bound at T2688.hs:8:5)
       v :: v (bound at T2688.hs:8:5)
diff --git a/tests/typecheck/should_fail/T3950.stderr b/tests/typecheck/should_fail/T3950.stderr
index 876a4997c..07b1d32f9 100644
--- a/tests/typecheck/should_fail/T3950.stderr
+++ b/tests/typecheck/should_fail/T3950.stderr
@@ -1,10 +1,16 @@
 
 T3950.hs:15:13:
     Couldn't match kind `* -> *' with `*'
-    Expected type: w (Id p)
-      Actual type: Sealed (Id p0 x0)
-    Kind incompatibility when matching types:
+    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
diff --git a/tests/typecheck/should_fail/T5570.stderr b/tests/typecheck/should_fail/T5570.stderr
index e69cbd588..63229e6aa 100644
--- a/tests/typecheck/should_fail/T5570.stderr
+++ b/tests/typecheck/should_fail/T5570.stderr
@@ -1,6 +1,9 @@
 
 T5570.hs:7:16:
-    Couldn't match expected kind `*' with actual kind `#'
+    Couldn't match kind `*' with `#'
+    When matching types
+      t0 :: *
+      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/tests/typecheck/should_fail/T5684.stderr b/tests/typecheck/should_fail/T5684.stderr
index c0575fd5a..a94aa8834 100644
--- a/tests/typecheck/should_fail/T5684.stderr
+++ b/tests/typecheck/should_fail/T5684.stderr
@@ -1,8 +1,6 @@
 
 T5684.hs:25:12:
     No instance for (A b6) arising from a use of `op'
-    The type variable `b6' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     In the expression: op True undefined
     In the expression:
       [op False False, op 'c' undefined, op True undefined]
@@ -11,8 +9,6 @@ T5684.hs:25:12:
 
 T5684.hs:30:12:
     No instance for (A b5) arising from a use of `op'
-    The type variable `b5' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     In the expression: op True undefined
     In the expression:
       [op False False, op True undefined, op 'c' undefined]
@@ -21,8 +17,6 @@ T5684.hs:30:12:
 
 T5684.hs:36:12:
     No instance for (A b4) arising from a use of `op'
-    The type variable `b4' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     In the expression: op True undefined
     In the expression:
       [op 'c' undefined, op True undefined, op False False]
@@ -31,8 +25,6 @@ T5684.hs:36:12:
 
 T5684.hs:42:12:
     No instance for (A b3) arising from a use of `op'
-    The type variable `b3' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     In the expression: op True undefined
     In the expression:
       [op 'c' undefined, op False False, op True undefined]
@@ -41,8 +33,6 @@ T5684.hs:42:12:
 
 T5684.hs:46:12:
     No instance for (A b2) arising from a use of `op'
-    The type variable `b2' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     In the expression: op True undefined
     In the expression:
       [op True undefined, op 'c' undefined, op False False]
@@ -51,8 +41,6 @@ T5684.hs:46:12:
 
 T5684.hs:52:12:
     No instance for (A b0) arising from a use of `op'
-    The type variable `b0' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     In the expression: op True undefined
     In the expression:
       [op True undefined, op False False, op 'c' undefined]
@@ -69,8 +57,6 @@ T5684.hs:53:12:
 
 T5684.hs:54:12:
     No instance for (B Char b1) arising from a use of `op'
-    The type variable `b1' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
     In the expression: op 'c' undefined
     In the expression:
       [op True undefined, op False False, op 'c' undefined]
diff --git a/tests/typecheck/should_fail/T5689.stderr b/tests/typecheck/should_fail/T5689.stderr
index 48e923bd6..ca4562eca 100644
--- a/tests/typecheck/should_fail/T5689.stderr
+++ b/tests/typecheck/should_fail/T5689.stderr
@@ -1,6 +1,6 @@
 
 T5689.hs:10:36:
-    Couldn't match expected type `t' with actual type `Bool'
+    Couldn't match expected type `Bool' with actual type `t'
     Relevant bindings include
       r :: IORef (t -> t) (bound at T5689.hs:7:14)
       v :: t (bound at T5689.hs:10:28)
diff --git a/tests/typecheck/should_fail/T5853.stderr b/tests/typecheck/should_fail/T5853.stderr
index 6ee736c0b..c36d64e84 100644
--- a/tests/typecheck/should_fail/T5853.stderr
+++ b/tests/typecheck/should_fail/T5853.stderr
@@ -1,6 +1,6 @@
 
 T5853.hs:15:52:
-    Could not deduce (Subst fa b ~ Subst (Subst fa a) b)
+    Could not deduce (Subst (Subst fa a) b ~ Subst fa b)
     from the context (F fa,
                       Elem (Subst fa b) ~ b,
                       Subst (Subst fa b) (Elem fa) ~ fa,
diff --git a/tests/typecheck/should_fail/tcfail032.stderr b/tests/typecheck/should_fail/tcfail032.stderr
index 09d69ca13..5a93f8c66 100644
--- a/tests/typecheck/should_fail/tcfail032.stderr
+++ b/tests/typecheck/should_fail/tcfail032.stderr
@@ -1,6 +1,6 @@
 
 tcfail032.hs:14:8:
-    Couldn't match expected type `t' with actual type `a1 -> Int'
+    Couldn't match expected type `a1 -> Int' with actual type `t'
       because type variable `a1' would escape its scope
     This (rigid, skolem) type variable is bound by
       an expression type signature: Eq a1 => a1 -> Int
diff --git a/tests/typecheck/should_fail/tcfail065.stderr b/tests/typecheck/should_fail/tcfail065.stderr
index ae1981653..c680e8264 100644
--- a/tests/typecheck/should_fail/tcfail065.stderr
+++ b/tests/typecheck/should_fail/tcfail065.stderr
@@ -1,11 +1,11 @@
 
 tcfail065.hs:29:20:
     Couldn't match expected type `x' with actual type `x1'
-      `x' is a rigid type variable bound by
-          the instance declaration at tcfail065.hs:28:10
       `x1' is a rigid type variable bound by
            the type signature for setX :: x1 -> X x -> X x
            at tcfail065.hs:29:3
+      `x' is a rigid type variable bound by
+          the instance declaration at tcfail065.hs:28:10
     Relevant bindings include
       setX :: x1 -> X x -> X x (bound at tcfail065.hs:29:3)
       x :: x1 (bound at tcfail065.hs:29:8)
diff --git a/tests/typecheck/should_fail/tcfail090.stderr b/tests/typecheck/should_fail/tcfail090.stderr
index f63d96ee9..3096b226c 100644
--- a/tests/typecheck/should_fail/tcfail090.stderr
+++ b/tests/typecheck/should_fail/tcfail090.stderr
@@ -1,7 +1,7 @@
 
 tcfail090.hs:8:9:
-    Couldn't match kind `*' against `#'
-    Kind incompatibility when matching types:
+    Couldn't match kind `*' with `#'
+    When matching types
       a0 :: *
       ByteArray# :: #
     In the expression: undefined
diff --git a/tests/typecheck/should_fail/tcfail099.stderr b/tests/typecheck/should_fail/tcfail099.stderr
index 49132b002..45531250b 100644
--- a/tests/typecheck/should_fail/tcfail099.stderr
+++ b/tests/typecheck/should_fail/tcfail099.stderr
@@ -1,13 +1,12 @@
 
 tcfail099.hs:9:20:
     Couldn't match expected type `a' with actual type `t'
-      `a' is a rigid type variable bound by
-          a pattern with constructor
-            C :: forall a. (a -> Int) -> DS,
-          in an equation for `call'
-          at tcfail099.hs:9:7
-      `t' is a rigid type variable bound by
-          the inferred type of call :: DS -> t -> Int at tcfail099.hs:9:1
+      because type variable `a' would escape its scope
+    This (rigid, skolem) type variable is bound by
+      a pattern with constructor
+        C :: forall a. (a -> Int) -> DS,
+      in an equation for `call'
+      at tcfail099.hs:9:7-9
     Relevant bindings include
       call :: DS -> t -> Int (bound at tcfail099.hs:9:1)
       f :: a -> Int (bound at tcfail099.hs:9:9)
diff --git a/tests/typecheck/should_fail/tcfail122.stderr b/tests/typecheck/should_fail/tcfail122.stderr
index 7002ee096..d08332116 100644
--- a/tests/typecheck/should_fail/tcfail122.stderr
+++ b/tests/typecheck/should_fail/tcfail122.stderr
@@ -1,11 +1,17 @@
 
 tcfail122.hs:8:9:
-    Couldn't match kind `* -> *' against `*'
-    Kind incompatibility when matching types:
-      c0 :: (* -> *) -> *
-      a0 :: * -> *
+    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]
diff --git a/tests/typecheck/should_fail/tcfail123.hs b/tests/typecheck/should_fail/tcfail123.hs
index 8e91bbe88..6a33eb7e6 100644
--- a/tests/typecheck/should_fail/tcfail123.hs
+++ b/tests/typecheck/should_fail/tcfail123.hs
@@ -8,4 +8,5 @@ module ShouldFail where
 
 f x = True
 
-h v = (f 3#, f 4.3#, f True)
+h v = f 3#
+-- h v = (f 3#, f 4.3#, f True)
diff --git a/tests/typecheck/should_fail/tcfail123.stderr b/tests/typecheck/should_fail/tcfail123.stderr
index b7ec97fd3..1ca291fd9 100644
--- a/tests/typecheck/should_fail/tcfail123.stderr
+++ b/tests/typecheck/should_fail/tcfail123.stderr
@@ -1,8 +1,9 @@
 
-tcfail123.hs:11:10:
-    Couldn't match kind `*' against `#'
-    Kind incompatibility when matching types:
+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#
diff --git a/tests/typecheck/should_fail/tcfail133.stderr b/tests/typecheck/should_fail/tcfail133.stderr
index 48ea0ebae..ed65b28a8 100644
--- a/tests/typecheck/should_fail/tcfail133.stderr
+++ b/tests/typecheck/should_fail/tcfail133.stderr
@@ -3,8 +3,8 @@ tcfail133.hs:2:61: Warning:
     -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
 
 tcfail133.hs:68:7:
-    No instance for (Show a0) arising from a use of `show'
-    The type variable `a0' is ambiguous
+    No instance for (Show t0) arising from a use of `show'
+    The type variable `t0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
     Note: there are several potential instances:
       instance Show Zero -- Defined at tcfail133.hs:8:29
@@ -18,7 +18,7 @@ tcfail133.hs:68:7:
         foo = show $ add (One :@ Zero) (One :@ One)
 
 tcfail133.hs:68:14:
-    No instance for (AddDigit (Zero :@ (One :@ One)) One a0)
+    No instance for (AddDigit (Zero :@ (One :@ One)) One t0)
       arising from a use of `add'
     In the second argument of `($)', namely
       `add (One :@ Zero) (One :@ One)'
diff --git a/tests/typecheck/should_fail/tcfail159.stderr b/tests/typecheck/should_fail/tcfail159.stderr
index c809e39d8..3576c7e24 100644
--- a/tests/typecheck/should_fail/tcfail159.stderr
+++ b/tests/typecheck/should_fail/tcfail159.stderr
@@ -1,8 +1,9 @@
 
 tcfail159.hs:9:11:
-    Couldn't match kind `*' against `#'
-    Kind incompatibility when matching types:
+    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 }
diff --git a/tests/typecheck/should_fail/tcfail174.stderr b/tests/typecheck/should_fail/tcfail174.stderr
index 762a87efe..d093e3238 100644
--- a/tests/typecheck/should_fail/tcfail174.stderr
+++ b/tests/typecheck/should_fail/tcfail174.stderr
@@ -5,31 +5,3 @@ tcfail174.hs:9:10:
     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 a. a -> a
-      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 a. a -> a 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/tests/typecheck/should_fail/tcfail175.stderr b/tests/typecheck/should_fail/tcfail175.stderr
index d467a1570..65f4cb9e4 100644
--- a/tests/typecheck/should_fail/tcfail175.stderr
+++ b/tests/typecheck/should_fail/tcfail175.stderr
@@ -1,7 +1,7 @@
 
 tcfail175.hs:11:1:
-    Couldn't match expected type `a'
-                with actual type `String -> String -> String'
+    Couldn't match expected type `String -> String -> String'
+                with actual type `a'
       `a' is a rigid type variable bound by
           the type signature for evalRHS :: Int -> a at tcfail175.hs:10:12
     Relevant bindings include
diff --git a/tests/typecheck/should_fail/tcfail179.stderr b/tests/typecheck/should_fail/tcfail179.stderr
index c60c7ac2e..ed0325acd 100644
--- a/tests/typecheck/should_fail/tcfail179.stderr
+++ b/tests/typecheck/should_fail/tcfail179.stderr
@@ -1,13 +1,13 @@
 
 tcfail179.hs:14:39:
     Couldn't match expected type `s' with actual type `x'
-      `s' is a rigid type variable bound by
-          the type signature for run :: T s -> Int at tcfail179.hs:12:8
       `x' is a rigid type variable bound by
           a pattern with constructor
             T :: forall s x. (s -> (x -> s) -> (x, s, Int)) -> T s,
           in a case alternative
           at tcfail179.hs:14:14
+      `s' is a rigid type variable bound by
+          the type signature for run :: T s -> Int at tcfail179.hs:12:8
     Relevant bindings include
       run :: T s -> Int (bound at tcfail179.hs:13:1)
       ts :: T s (bound at tcfail179.hs:13:5)
diff --git a/tests/typecheck/should_fail/tcfail192.stderr b/tests/typecheck/should_fail/tcfail192.stderr
index d4cc8bbbf..caf7ef140 100644
--- a/tests/typecheck/should_fail/tcfail192.stderr
+++ b/tests/typecheck/should_fail/tcfail192.stderr
@@ -1,12 +1,4 @@
 
-tcfail192.hs:8:11:
-    No instance for (Num [[Char]]) arising from a use of `+'
-    In the expression: x + 1
-    In the expression:
-      [x + 1 | x <- ["Hello", "World"], then group using take 5]
-    In an equation for `foo':
-        foo = [x + 1 | x <- ["Hello", "World"], then group using take 5]
-
 tcfail192.hs:10:26:
     Couldn't match type `a' with `[a]'
       `a' is a rigid type variable bound by
diff --git a/tests/typecheck/should_fail/tcfail198.stderr b/tests/typecheck/should_fail/tcfail198.stderr
index ab040a1e2..22a09f59f 100644
--- a/tests/typecheck/should_fail/tcfail198.stderr
+++ b/tests/typecheck/should_fail/tcfail198.stderr
@@ -1,10 +1,10 @@
 
 tcfail198.hs:6:36:
     Couldn't match expected type `a1' with actual type `a'
-      `a1' is a rigid type variable bound by
-           an expression type signature: a1 at tcfail198.hs:6:36
-      `a' is a rigid type variable bound by
-          the inferred type of f3 :: [a] -> [a] at tcfail198.hs:6:1
+      because type variable `a1' would escape its scope
+    This (rigid, skolem) type variable is bound by
+      an expression type signature: a1
+      at tcfail198.hs:6:36-41
     Relevant bindings include
       f3 :: [a] -> [a] (bound at tcfail198.hs:6:6)
       x :: a (bound at tcfail198.hs:6:19)
diff --git a/tests/typecheck/should_fail/tcfail200.stderr b/tests/typecheck/should_fail/tcfail200.stderr
index c75dc8f88..731f906fd 100644
--- a/tests/typecheck/should_fail/tcfail200.stderr
+++ b/tests/typecheck/should_fail/tcfail200.stderr
@@ -1,8 +1,9 @@
 
 tcfail200.hs:5:15:
-    Couldn't match kind `*' against `#'
-    Kind incompatibility when matching types:
-      t0 :: *
+    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')
diff --git a/tests/typecheck/should_fail/tcfail206.stderr b/tests/typecheck/should_fail/tcfail206.stderr
index 2d0f87132..706933dc9 100644
--- a/tests/typecheck/should_fail/tcfail206.stderr
+++ b/tests/typecheck/should_fail/tcfail206.stderr
@@ -13,17 +13,6 @@ tcfail206.hs:8:5:
     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 #)
@@ -38,14 +27,3 @@ tcfail206.hs:17:5:
       Actual type: Int -> (# Integer, 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, #)
-- 
GitLab