Wibbles (usually improvements) to error messages

45 files changed, 401 insertions, 327 deletions

diff --git a/testsuite/tests/deriving/should_fail/T5287.stderr b/testsuite/tests/deriving/should_fail/T5287.stderr
index 764c422dd1..0c068e0574 100644
--- a/testsuite/tests/deriving/should_fail/T5287.stderr
+++ b/testsuite/tests/deriving/should_fail/T5287.stderr
@@ -1,11 +1,11 @@
 
 T5287.hs:6:10:
     Could not deduce (A a oops0)
-      arising from the ambiguity check for an instance declaration
     from the context (A a oops)
       bound by an instance declaration: A a oops => Read (D a)
       at T5287.hs:6:10-31
     The type variable ‘oops0’ is ambiguous
-    In the ambiguity check for: forall a oops. A a oops => Read (D a)
+    In the ambiguity check for an instance declaration:
+      forall a oops. A a oops => Read (D a)
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the instance declaration for ‘Read (D a)’
diff --git a/testsuite/tests/ghci/scripts/Defer02.stderr b/testsuite/tests/ghci/scripts/Defer02.stderr
index 4f58b02695..669d271c78 100644
--- a/testsuite/tests/ghci/scripts/Defer02.stderr
+++ b/testsuite/tests/ghci/scripts/Defer02.stderr
@@ -83,13 +83,15 @@
     Couldn't match type ‘Int’ with ‘Bool’
     Inaccessible code in
       the type signature for k :: (Int ~ Bool) => Int -> Bool
-    In the ambiguity check for: (Int ~ Bool) => Int -> Bool
+    In the ambiguity check for the type signature for ‘k’:
+      k :: (Int ~ Bool) => Int -> Bool
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘k’: k :: (Int ~ Bool) => Int -> Bool
 
 ../../typecheck/should_run/Defer01.hs:45:6: Warning:
     Couldn't match expected type ‘Bool’ with actual type ‘Int’
-    In the ambiguity check for: (Int ~ Bool) => Int -> Bool
+    In the ambiguity check for the type signature for ‘k’:
+      k :: (Int ~ Bool) => Int -> Bool
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘k’: k :: (Int ~ Bool) => Int -> Bool
 
diff --git a/testsuite/tests/ghci/scripts/ghci012.stdout b/testsuite/tests/ghci/scripts/ghci012.stdout
index 407ef45dc3..d19785b3ee 100644
--- a/testsuite/tests/ghci/scripts/ghci012.stdout
+++ b/testsuite/tests/ghci/scripts/ghci012.stdout
@@ -1 +1 @@
-($$$) :: [b -> c] -> [b] -> [c] 	-- Defined at <interactive>:2:8
+($$$) :: [a -> c] -> [a] -> [c] 	-- Defined at <interactive>:2:8
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.hs b/testsuite/tests/indexed-types/should_compile/Simple14.hs
index dfffbc7c9c..b8e002bdcd 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.hs
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.hs
@@ -4,6 +4,7 @@ module Simple14 where
 
 data EQ_ x y = EQ_
 
+-- Nov 2014: actually eqE has an ambiguous type
 eqE :: EQ_ x y -> (x~y => EQ_ z z) -> p
 eqE = error "eqE"
 
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.stderr b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
index 3dbf213695..1e430d513b 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.stderr
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
@@ -1,18 +1,17 @@
 
-Simple14.hs:17:19:
-    Couldn't match type ‘z0’ with ‘m’
+Simple14.hs:8:8:
+    Couldn't match type ‘z0’ with ‘z’
       ‘z0’ is untouchable
-        inside the constraints (Maybe m ~ Maybe n)
-        bound by a type expected by the context:
-                   (Maybe m ~ Maybe n) => EQ_ z0 z0
-        at Simple14.hs:17:12-33
-      ‘m’ is a rigid type variable bound by
-          the type signature for foo :: EQ_ (Maybe m) (Maybe n)
-          at Simple14.hs:16:15
+        inside the constraints (x ~ y)
+        bound by the type signature for eqE :: (x ~ y) => EQ_ z0 z0
+        at Simple14.hs:8:8-39
+      ‘z’ is a rigid type variable bound by
+          the type signature for eqE :: EQ_ x y -> ((x ~ y) => EQ_ z z) -> p
+          at Simple14.hs:8:8
     Expected type: EQ_ z0 z0
-      Actual type: EQ_ m n
-    Relevant bindings include
-      foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:17:1)
-    In the second argument of ‘eqE’, namely ‘(eqI :: EQ_ m n)’
-    In the first argument of ‘ntI’, namely ‘(`eqE` (eqI :: EQ_ m n))’
-    In the expression: ntI (`eqE` (eqI :: EQ_ m n))
+      Actual type: EQ_ z z
+    In the ambiguity check for the type signature for ‘eqE’:
+      eqE :: forall x y z p. EQ_ x y -> ((x ~ y) => EQ_ z z) -> p
+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+    In the type signature for ‘eqE’:
+      eqE :: EQ_ x y -> (x ~ y => EQ_ z z) -> p
diff --git a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
index f825fd2af6..5a0443bfa1 100644
--- a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
+++ b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
@@ -1,11 +1,11 @@
 
 NoMatchErr.hs:19:7:
-    Couldn't match type ‘Memo d’ with ‘Memo d0’
+    Couldn't match type ‘Memo d0’ with ‘Memo d’
     NB: ‘Memo’ is a type function, and may not be injective
     The type variable ‘d0’ is ambiguous
     Expected type: Memo d a -> Memo d a
       Actual type: Memo d0 a -> Memo d0 a
-    In the ambiguity check for:
-      forall d a. Fun d => Memo d a -> Memo d a
+    In the ambiguity check for the type signature for ‘f’:
+      f :: forall d a. Fun d => Memo d a -> Memo d a
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘f’: f :: (Fun d) => Memo d a -> Memo d a
diff --git a/testsuite/tests/indexed-types/should_fail/T1897b.stderr b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
index 936aa26924..c6d318f047 100644
--- a/testsuite/tests/indexed-types/should_fail/T1897b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1897b.stderr
@@ -1,6 +1,6 @@
 
 T1897b.hs:16:1:
-    Couldn't match type ‘Depend a’ with ‘Depend a0’
+    Couldn't match type ‘Depend a0’ with ‘Depend a’
     NB: ‘Depend’ is a type function, and may not be injective
     The type variable ‘a0’ is ambiguous
     Expected type: t (Depend a) -> Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T1900.stderr b/testsuite/tests/indexed-types/should_fail/T1900.stderr
index 73fe38108a..0d02a52f11 100644
--- a/testsuite/tests/indexed-types/should_fail/T1900.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1900.stderr
@@ -5,7 +5,8 @@ T1900.hs:13:10:
     The type variable ‘s0’ is ambiguous
     Expected type: Depend s -> Bool
       Actual type: Depend s0 -> Bool
-    In the ambiguity check for: forall s. Bug s => Depend s -> Bool
+    In the ambiguity check for the type signature for ‘check’:
+      check :: forall s. Bug s => Depend s -> Bool
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘check’:
       check :: (Bug s) => Depend s -> Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T2693.stderr b/testsuite/tests/indexed-types/should_fail/T2693.stderr
index 0c6ea152a7..8fdb9985b6 100644
--- a/testsuite/tests/indexed-types/should_fail/T2693.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2693.stderr
@@ -1,38 +1,38 @@
-

-T2693.hs:11:7:

-    Couldn't match expected type ‘TFn a’ with actual type ‘TFn a0’

-    NB: ‘TFn’ is a type function, and may not be injective

-    The type variable ‘a0’ is ambiguous

-    When checking that ‘x’ has the inferred type

-      x :: forall a. TFn a

-    Probable cause: the inferred type is ambiguous

-    In the expression:

-      do { let Just x = ...;

-           let n = fst x + fst x;

-           return () }

-    In an equation for ‘f’:

-        f = do { let Just x = ...;

-                 let n = ...;

-                 return () }

-

-T2693.hs:19:15:

-    Couldn't match expected type ‘(a5, b0)’ with actual type ‘TFn a2’

-    The type variables ‘b0’, ‘a2’, ‘a5’ are ambiguous

-    Relevant bindings include n :: a5 (bound at T2693.hs:19:7)

-    In the first argument of ‘fst’, namely ‘x’

-    In the first argument of ‘(+)’, namely ‘fst x’

-

-T2693.hs:19:23:

-    Couldn't match expected type ‘(a3, a5)’ with actual type ‘TFn a4’

-    The type variables ‘a3’, ‘a4’, ‘a5’ are ambiguous

-    Relevant bindings include n :: a5 (bound at T2693.hs:19:7)

-    In the first argument of ‘snd’, namely ‘x’

-    In the second argument of ‘(+)’, namely ‘snd x’

-

-T2693.hs:29:20:

-    Couldn't match type ‘TFn a0’ with ‘PVR a1’

-    The type variables ‘a0’, ‘a1’ are ambiguous

-    Expected type: () -> Maybe (PVR a1)

-      Actual type: () -> Maybe (TFn a0)

-    In the first argument of ‘mapM’, namely ‘g’

-    In a stmt of a 'do' block: pvs <- mapM g undefined

+
+T2693.hs:11:7:
+    Couldn't match expected type ‘TFn a’ with actual type ‘TFn a0’
+    NB: ‘TFn’ is a type function, and may not be injective
+    The type variable ‘a0’ is ambiguous
+    When checking that ‘x’ has the inferred type
+      x :: forall a. TFn a
+    Probable cause: the inferred type is ambiguous
+    In the expression:
+      do { let Just x = ...;
+           let n = fst x + fst x;
+           return () }
+    In an equation for ‘f’:
+        f = do { let Just x = ...;
+                 let n = ...;
+                 return () }
+
+T2693.hs:19:15:
+    Couldn't match expected type ‘(a2, b0)’ with actual type ‘TFn a3’
+    The type variables ‘a2’, ‘b0’, ‘a3’ are ambiguous
+    Relevant bindings include n :: a2 (bound at T2693.hs:19:7)
+    In the first argument of ‘fst’, namely ‘x’
+    In the first argument of ‘(+)’, namely ‘fst x’
+
+T2693.hs:19:23:
+    Couldn't match expected type ‘(a4, a2)’ with actual type ‘TFn a5’
+    The type variables ‘a2’, ‘a4’, ‘a5’ are ambiguous
+    Relevant bindings include n :: a2 (bound at T2693.hs:19:7)
+    In the first argument of ‘snd’, namely ‘x’
+    In the second argument of ‘(+)’, namely ‘snd x’
+
+T2693.hs:29:20:
+    Couldn't match type ‘TFn a0’ with ‘PVR a1’
+    The type variables ‘a0’, ‘a1’ are ambiguous
+    Expected type: () -> Maybe (PVR a1)
+      Actual type: () -> Maybe (TFn a0)
+    In the first argument of ‘mapM’, namely ‘g’
+    In a stmt of a 'do' block: pvs <- mapM g undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T4093a.stderr b/testsuite/tests/indexed-types/should_fail/T4093a.stderr
index 076041be32..99188219bd 100644
--- a/testsuite/tests/indexed-types/should_fail/T4093a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4093a.stderr
@@ -5,7 +5,8 @@ T4093a.hs:7:9:
       bound by the type signature for hang :: (Foo e ~ Maybe e) => Foo e
       at T4093a.hs:7:9-34
     The type variable ‘e0’ is ambiguous
-    In the ambiguity check for: forall e. (Foo e ~ Maybe e) => Foo e
+    In the ambiguity check for the type signature for ‘hang’:
+      hang :: forall e. (Foo e ~ Maybe e) => Foo e
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘hang’:
       hang :: (Foo e ~ Maybe e) => Foo e
diff --git a/testsuite/tests/indexed-types/should_fail/T9036.stderr b/testsuite/tests/indexed-types/should_fail/T9036.stderr
index 3a6e38ee34..499e6b4ec1 100644
--- a/testsuite/tests/indexed-types/should_fail/T9036.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9036.stderr
@@ -1,12 +1,13 @@
 
 T9036.hs:17:17:
-    Couldn't match type ‘Curried t [t]’ with ‘Curried t0 [t0]’
-    NB: ‘Curried’ is a type function, and may not be injective
+    Couldn't match type ‘GetMonad t0’ with ‘GetMonad t’
+    NB: ‘GetMonad’ is a type function, and may not be injective
     The type variable ‘t0’ is ambiguous
     Expected type: Maybe (GetMonad t after) -> Curried t [t]
       Actual type: Maybe (GetMonad t0 after) -> Curried t0 [t0]
-    In the ambiguity check for:
-      forall t after. Maybe (GetMonad t after) -> Curried t [t]
+    In the ambiguity check for the type signature for ‘simpleLogger’:
+      simpleLogger :: forall t after.
+                      Maybe (GetMonad t after) -> Curried t [t]
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘simpleLogger’:
       simpleLogger :: Maybe (GetMonad t after) -> t `Curried` [t]
diff --git a/testsuite/tests/indexed-types/should_fail/T9171.stderr b/testsuite/tests/indexed-types/should_fail/T9171.stderr
index fe49925118..28c1a2373f 100644
--- a/testsuite/tests/indexed-types/should_fail/T9171.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9171.stderr
@@ -1,22 +1,22 @@
-

-T9171.hs:10:1:

-    Couldn't match expected type ‘GetParam Base (GetParam Base Int)’

-                with actual type ‘GetParam Base (GetParam Base Int)’

-    NB: ‘GetParam’ is a type function, and may not be injective

-    The kind variable ‘k0’ is ambiguous

-    Use -fprint-explicit-kinds to see the kind arguments

-    When checking that ‘foo’ has the inferred type

-      foo :: forall (k :: BOX). GetParam Base (GetParam Base Int)

-    Probable cause: the inferred type is ambiguous

-

-T9171.hs:10:20:

-    Couldn't match expected type ‘GetParam Base (GetParam Base Int)’

-                with actual type ‘GetParam Base (GetParam Base Int)’

-    NB: ‘GetParam’ is a type function, and may not be injective

-    The kind variable ‘k0’ is ambiguous

-    Use -fprint-explicit-kinds to see the kind arguments

-    In the ambiguity check for:

-      forall (k :: BOX). GetParam Base (GetParam Base Int)

-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

-    In an expression type signature: GetParam Base (GetParam Base Int)

-    In the expression: undefined :: GetParam Base (GetParam Base Int)

+
+T9171.hs:10:1:
+    Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
+                with actual type ‘GetParam Base (GetParam Base Int)’
+    NB: ‘GetParam’ is a type function, and may not be injective
+    The kind variable ‘k0’ is ambiguous
+    Use -fprint-explicit-kinds to see the kind arguments
+    When checking that ‘foo’ has the inferred type
+      foo :: forall (k :: BOX). GetParam Base (GetParam Base Int)
+    Probable cause: the inferred type is ambiguous
+
+T9171.hs:10:20:
+    Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
+                with actual type ‘GetParam Base (GetParam Base Int)’
+    NB: ‘GetParam’ is a type function, and may not be injective
+    The kind variable ‘k0’ is ambiguous
+    Use -fprint-explicit-kinds to see the kind arguments
+    In the ambiguity check for an expression type signature:
+      forall (k :: BOX). GetParam Base (GetParam Base Int)
+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+    In an expression type signature: GetParam Base (GetParam Base Int)
+    In the expression: undefined :: GetParam Base (GetParam Base Int)
diff --git a/testsuite/tests/parser/should_fail/T7848.stderr b/testsuite/tests/parser/should_fail/T7848.stderr
index 1cbf5f4a85..202c66c07e 100644
--- a/testsuite/tests/parser/should_fail/T7848.stderr
+++ b/testsuite/tests/parser/should_fail/T7848.stderr
@@ -1,12 +1,39 @@
 
+T7848.hs:6:57:
+    Occurs check: cannot construct the infinite type:
+      t2 ~ t0 -> t -> t1 -> A -> A -> A -> A -> t2
+    Relevant bindings include
+      y :: forall t3. t3 -> t -> t1 -> A -> A -> A -> A -> t2
+        (bound at T7848.hs:8:9)
+      (&) :: t -> t1 -> A -> A -> A -> A -> t2 (bound at T7848.hs:11:9)
+      z :: t1 (bound at T7848.hs:6:12)
+      (&) :: t1 (bound at T7848.hs:6:8)
+      (+) :: t (bound at T7848.hs:6:3)
+      x :: t -> t1 -> A -> A -> A -> A -> t2 (bound at T7848.hs:6:1)
+    In the expression: y
+    In an equation for ‘x’:
+        x (+) ((&)@z) ((:&&) a b) (c :&& d) (e `A` f) (A g h)
+          = y
+          where
+              infixl 3 `y`
+              y _ = (&)
+              {-# INLINE (&) #-}
+              {-# SPECIALIZE (&) :: a #-}
+              (&) = x
+
 T7848.hs:10:9:
-    Couldn't match expected type ‘forall a. a’
-                with actual type ‘t -> t1 -> A -> A -> A -> A -> t2’
+    Couldn't match type ‘a’ with ‘t -> t1 -> A -> A -> A -> A -> t2’
+      ‘a’ is a rigid type variable bound by
+          the type signature for (&) :: a at T7848.hs:10:9
+    Expected type: forall a. a
+      Actual type: t -> t1 -> A -> A -> A -> A -> t2
     Relevant bindings include
       z :: t1 (bound at T7848.hs:6:12)
       (&) :: t1 (bound at T7848.hs:6:8)
       (+) :: t (bound at T7848.hs:6:3)
       x :: t -> t1 -> A -> A -> A -> A -> t2 (bound at T7848.hs:6:1)
+    When checking that: t -> t1 -> A -> A -> A -> A -> t2
+      is more polymorphic than: forall a. a
     In the SPECIALISE pragma {-# SPECIALIZE (&) :: a #-}
     In an equation for ‘x’:
         x (+) ((&)@z) ((:&&) a b) (c :&& d) (e `A` f) (A g h)
diff --git a/testsuite/tests/perf/compiler/T5837.stderr b/testsuite/tests/perf/compiler/T5837.stderr
index 193bff1728..f3ee82ca66 100644
--- a/testsuite/tests/perf/compiler/T5837.stderr
+++ b/testsuite/tests/perf/compiler/T5837.stderr
@@ -157,5 +157,6 @@ T5837.hs:8:6:
                                                                                                                                                            (TF
                                                                                                                                                               (TF
                                                                                                                                                                  Int)))))))))))))))))))))))))))))))))))))))))))))))))))
-    In the ambiguity check for: forall a. (a ~ TF (a, Int)) => Int
+    In the ambiguity check for the type signature for ‘t’:
+      t :: forall a. (a ~ TF (a, Int)) => Int
     In the type signature for ‘t’: t :: (a ~ TF (a, Int)) => Int
diff --git a/testsuite/tests/typecheck/should_compile/T2494.stderr b/testsuite/tests/typecheck/should_compile/T2494.stderr
index dee00ab6b4..0346e62a3f 100644
--- a/testsuite/tests/typecheck/should_compile/T2494.stderr
+++ b/testsuite/tests/typecheck/should_compile/T2494.stderr
@@ -1,34 +1,34 @@
-

-T2494.hs:15:14:

-    Couldn't match type ‘b’ with ‘a’

-      ‘b’ is a rigid type variable bound by

-          the RULE "foo/foo" at T2494.hs:14:16

-      ‘a’ is a rigid type variable bound by

-          the RULE "foo/foo" at T2494.hs:13:16

-    Expected type: Maybe (m a) -> Maybe (m a)

-      Actual type: Maybe (m b) -> Maybe (m b)

-    Relevant bindings include

-      f :: forall (m :: * -> *). Monad m => Maybe (m a) -> Maybe (m a)

-        (bound at T2494.hs:13:11)

-      g :: forall (m :: * -> *). Monad m => Maybe (m b) -> Maybe (m b)

-        (bound at T2494.hs:14:11)

-      x :: Maybe a (bound at T2494.hs:14:65)

-    In the first argument of ‘foo’, namely ‘g’

-    In the second argument of ‘foo’, namely ‘(foo g x)’

-

-T2494.hs:15:30:

-    Couldn't match type ‘b’ with ‘a’

-      ‘b’ is a rigid type variable bound by

-          the RULE "foo/foo" at T2494.hs:14:16

-      ‘a’ is a rigid type variable bound by

-          the RULE "foo/foo" at T2494.hs:13:16

-    Expected type: Maybe (m a) -> Maybe (m a)

-      Actual type: Maybe (m b) -> Maybe (m b)

-    Relevant bindings include

-      f :: forall (m :: * -> *). Monad m => Maybe (m a) -> Maybe (m a)

-        (bound at T2494.hs:13:11)

-      g :: forall (m :: * -> *). Monad m => Maybe (m b) -> Maybe (m b)

-        (bound at T2494.hs:14:11)

-      x :: Maybe a (bound at T2494.hs:14:65)

-    In the second argument of ‘(.)’, namely ‘g’

-    In the first argument of ‘foo’, namely ‘(f . g)’

+
+T2494.hs:15:14:
+    Couldn't match type ‘b’ with ‘a’
+      ‘b’ is a rigid type variable bound by
+          the RULE "foo/foo" at T2494.hs:14:16
+      ‘a’ is a rigid type variable bound by
+          the RULE "foo/foo" at T2494.hs:13:16
+    Expected type: Maybe (m a) -> Maybe (m a)
+      Actual type: Maybe (m b) -> Maybe (m b)
+    Relevant bindings include
+      f :: forall (m :: * -> *). Monad m => Maybe (m a) -> Maybe (m a)
+        (bound at T2494.hs:13:11)
+      g :: forall (m :: * -> *). Monad m => Maybe (m b) -> Maybe (m b)
+        (bound at T2494.hs:14:11)
+      x :: Maybe a (bound at T2494.hs:14:65)
+    In the first argument of ‘foo’, namely ‘g’
+    In the second argument of ‘foo’, namely ‘(foo g x)’
+
+T2494.hs:15:30:
+    Couldn't match type ‘b’ with ‘a’
+      ‘b’ is a rigid type variable bound by
+          the RULE "foo/foo" at T2494.hs:14:16
+      ‘a’ is a rigid type variable bound by
+          the RULE "foo/foo" at T2494.hs:13:16
+    Expected type: Maybe (m a) -> Maybe (m a)
+      Actual type: Maybe (m b) -> Maybe (m b)
+    Relevant bindings include
+      f :: forall (m :: * -> *). Monad m => Maybe (m a) -> Maybe (m a)
+        (bound at T2494.hs:13:11)
+      g :: forall (m :: * -> *). Monad m => Maybe (m b) -> Maybe (m b)
+        (bound at T2494.hs:14:11)
+      x :: Maybe a (bound at T2494.hs:14:65)
+    In the second argument of ‘(.)’, namely ‘g’
+    In the first argument of ‘foo’, namely ‘(f . g)’
diff --git a/testsuite/tests/typecheck/should_compile/T3692.hs b/testsuite/tests/typecheck/should_compile/T3692.hs
index b10e184d94..9fccb0a52f 100644
--- a/testsuite/tests/typecheck/should_compile/T3692.hs
+++ b/testsuite/tests/typecheck/should_compile/T3692.hs
@@ -7,4 +7,4 @@ type Foo a b = () -> (Bar a => a)
 class Bar a where {}

 

 foo :: Foo a b

-foo = id (undefined :: Foo a b)

+foo = id (undefined :: Foo p q)

diff --git a/testsuite/tests/typecheck/should_compile/T9708.stderr b/testsuite/tests/typecheck/should_compile/T9708.stderr
index fca5df7bc8..fb8a6a7ef9 100644
--- a/testsuite/tests/typecheck/should_compile/T9708.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9708.stderr
@@ -1,17 +1,17 @@
-

-T9708.hs:9:8:

-    Could not deduce (SomeFun x ~ SomeFun y)

-    from the context (x <= y, y <= x)

-      bound by the type signature for

-                 ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> ()

-      at T9708.hs:9:8-61

-    NB: ‘SomeFun’ is a type function, and may not be injective

-    Expected type: Proxy (SomeFun x) -> Proxy y -> ()

-      Actual type: Proxy (SomeFun y) -> Proxy y -> ()

-    In the ambiguity check for:

-      forall (x :: Nat) (y :: Nat).

-      (x <= y, y <= x) =>

-      Proxy (SomeFun x) -> Proxy y -> ()

-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

-    In the type signature for ‘ti7’:

-      ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> ()

+
+T9708.hs:9:8:
+    Could not deduce (SomeFun y ~ SomeFun x)
+    from the context (x <= y, y <= x)
+      bound by the type signature for
+                 ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> ()
+      at T9708.hs:9:8-61
+    NB: ‘SomeFun’ is a type function, and may not be injective
+    Expected type: Proxy (SomeFun x) -> Proxy y -> ()
+      Actual type: Proxy (SomeFun y) -> Proxy y -> ()
+    In the ambiguity check for the type signature for ‘ti7’:
+      ti7 :: forall (x :: Nat) (y :: Nat).
+             (x <= y, y <= x) =>
+             Proxy (SomeFun x) -> Proxy y -> ()
+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+    In the type signature for ‘ti7’:
+      ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> ()
diff --git a/testsuite/tests/typecheck/should_compile/tc168.stderr b/testsuite/tests/typecheck/should_compile/tc168.stderr
index b46cdd04b3..16df4a466b 100644
--- a/testsuite/tests/typecheck/should_compile/tc168.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc168.stderr
@@ -1,11 +1,10 @@
-

-tc168.hs:17:1:

-    Could not deduce (C a1 (a, b0))

-      arising from the ambiguity check for ‘g’

-    from the context (C a1 (a, b))

-      bound by the inferred type for ‘g’: C a1 (a, b) => a1 -> a

-      at tc168.hs:17:1-16

-    The type variable ‘b0’ is ambiguous

-    When checking that ‘g’ has the inferred type

-      g :: forall a b a1. C a1 (a, b) => a1 -> a

-    Probable cause: the inferred type is ambiguous

+
+tc168.hs:17:1:
+    Could not deduce (C a1 (a, b0))
+    from the context (C a1 (a, b))
+      bound by the inferred type for ‘g’: C a1 (a, b) => a1 -> a
+      at tc168.hs:17:1-16
+    The type variable ‘b0’ is ambiguous
+    When checking that ‘g’ has the inferred type
+      g :: forall a b a1. C a1 (a, b) => a1 -> a
+    Probable cause: the inferred type is ambiguous
diff --git a/testsuite/tests/typecheck/should_compile/tc211.hs b/testsuite/tests/typecheck/should_compile/tc211.hs
index 5bd5c34821..8f273ba923 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.hs
+++ b/testsuite/tests/typecheck/should_compile/tc211.hs
@@ -1,5 +1,8 @@
 {-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XScopedTypeVariables -XGADTs #-}
 
+-- Nov 2014: impredicative types are very dodgy so I am
+--           FAR from confident that these tests give the right errors
+
 -- Here are a bunch of tests for impredicative polymorphism
 -- mainly written by Dimitrios
 
diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
index 533155a657..34a35f1781 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc211.stderr
@@ -1,25 +1,61 @@
-

-tc211.hs:15:22:

-    Couldn't match type ‘forall a1. a1 -> a1’ 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)’

-

-tc211.hs:70:9:

-    Couldn't match type ‘forall a2. a2 -> a2’ with ‘a1 -> a1’

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

-                   -> (forall a. a -> a) -> a1 -> a1

-      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)

+
+tc211.hs:17:8:
+    Couldn't match expected type ‘forall a. a -> a’
+                with actual type ‘a2 -> a2’
+    In the expression:
+        (:) ::
+          (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]
+    In the expression:
+      ((:) ::
+         (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
+        (head foo) foo
+
+tc211.hs:18:22:
+    Couldn't match type ‘forall a3. a3 -> a3’ 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)’
+
+tc211.hs:59:18:
+    Couldn't match expected type ‘forall a. a -> a’
+                with actual type ‘a1 -> a1’
+    In the expression:
+        Cons ::
+          (forall a. a -> a)
+          -> List (forall a. a -> a) -> List (forall a. a -> a)
+    In an equation for ‘cons’:
+        cons
+          = Cons ::
+              (forall a. a -> a)
+              -> List (forall a. a -> a) -> List (forall a. a -> a)
+
+tc211.hs:65:8:
+    Couldn't match expected type ‘forall a. a -> a’
+                with actual type ‘a0 -> a0’
+    In the expression:
+        Cons ::
+          (forall a. a -> a)
+          -> List (forall a. a -> a) -> List (forall a. a -> a)
+    In the expression:
+      (Cons ::
+         (forall a. a -> a)
+         -> List (forall a. a -> a) -> List (forall a. a -> a))
+        (\ x -> x) Nil
+
+tc211.hs:73:9:
+    Couldn't match type ‘forall a4. a4 -> a4’ with ‘a3 -> a3’
+    Expected type: List (forall a. a -> a)
+                   -> (forall a. a -> a) -> a3 -> a3
+      Actual type: List (a3 -> a3) -> (a3 -> a3) -> a3 -> a3
+    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)
diff --git a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr b/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
index fbbd5980bc..90e728551b 100644
--- a/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
+++ b/testsuite/tests/typecheck/should_fail/ContextStack2.stderr
@@ -5,5 +5,6 @@ ContextStack2.hs:8:6:
       TF (TF (TF (TF (TF (TF (TF (TF (TF (TF a)))))))))
       ~ (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF a)))))))))),
          TF (TF (TF (TF (TF (TF (TF (TF (TF (TF (TF Int)))))))))))
-    In the ambiguity check for: forall a. (a ~ TF (a, Int)) => Int
+    In the ambiguity check for the type signature for ‘t’:
+      t :: forall a. (a ~ TF (a, Int)) => Int
     In the type signature for ‘t’: t :: (a ~ TF (a, Int)) => Int
diff --git a/testsuite/tests/typecheck/should_fail/T1897a.stderr b/testsuite/tests/typecheck/should_fail/T1897a.stderr
index 58f1a2d6ff..e0f76ee17c 100644
--- a/testsuite/tests/typecheck/should_fail/T1897a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1897a.stderr
@@ -1,11 +1,10 @@
-

-T1897a.hs:9:1:

-    Could not deduce (Wob a0 b)

-      arising from the ambiguity check for ‘foo’

-    from the context (Wob a b)

-      bound by the inferred type for ‘foo’: Wob a b => b -> [b]

-      at T1897a.hs:9:1-24

-    The type variable ‘a0’ is ambiguous

-    When checking that ‘foo’ has the inferred type

-      foo :: forall a b. Wob a b => b -> [b]

-    Probable cause: the inferred type is ambiguous

+
+T1897a.hs:9:1:
+    Could not deduce (Wob a0 b)
+    from the context (Wob a b)
+      bound by the inferred type for ‘foo’: Wob a b => b -> [b]
+      at T1897a.hs:9:1-24
+    The type variable ‘a0’ is ambiguous
+    When checking that ‘foo’ has the inferred type
+      foo :: forall a b. Wob a b => b -> [b]
+    Probable cause: the inferred type is ambiguous
diff --git a/testsuite/tests/typecheck/should_fail/T2414.stderr b/testsuite/tests/typecheck/should_fail/T2414.stderr
index 7c4310398d..0f797da713 100644
--- a/testsuite/tests/typecheck/should_fail/T2414.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2414.stderr
@@ -2,6 +2,6 @@
 T2414.hs:9:13:
     Occurs check: cannot construct the infinite type: b0 ~ (Bool, b0)
     Expected type: b0 -> Maybe (Bool, b0)
-      Actual type: b0 -> Maybe b0
+      Actual type: (Bool, b0) -> Maybe (Bool, b0)
     In the first argument of ‘unfoldr’, namely ‘Just’
     In the expression: unfoldr Just
diff --git a/testsuite/tests/typecheck/should_fail/T2534.stderr b/testsuite/tests/typecheck/should_fail/T2534.stderr
index 7a0aa3a991..157521f953 100644
--- a/testsuite/tests/typecheck/should_fail/T2534.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2534.stderr
@@ -1,8 +1,8 @@
 
-T2534.hs:3:19:
-    Couldn't match expected type ‘a -> a -> b’ with actual type ‘[t0]’
-    Relevant bindings include
-      foo :: a -> a -> b (bound at T2534.hs:3:1)
-    In the second argument of ‘foldr’, namely ‘[]’
+T2534.hs:3:13:
+    Couldn't match type ‘[b]’ with ‘a0 -> [b]’
+    Expected type: [a0] -> [b] -> [b]
+      Actual type: [a0] -> (a0 -> [b]) -> [b]
+    Relevant bindings include foo :: [b] (bound at T2534.hs:3:1)
+    In the first argument of ‘foldr’, namely ‘(>>=)’
     In the expression: foldr (>>=) [] []
-    In an equation for ‘foo’: foo = foldr (>>=) [] []
diff --git a/testsuite/tests/typecheck/should_fail/T3592.stderr b/testsuite/tests/typecheck/should_fail/T3592.stderr
index a7f0f28b16..05ea89a064 100644
--- a/testsuite/tests/typecheck/should_fail/T3592.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3592.stderr
@@ -1,6 +1,9 @@
 
 T3592.hs:8:5:
-    No instance for (Show (T a)) arising from a use of ‘show’
+    No instance for (Show a) arising from a use of ‘show’
+    Possible fix:
+      add (Show a) to the context of
+        the type signature for f :: T a -> String
     In the expression: show
     In an equation for ‘f’: f = show
 
diff --git a/testsuite/tests/typecheck/should_fail/T3613.stderr b/testsuite/tests/typecheck/should_fail/T3613.stderr
index f230fc469d..f7fa6d4871 100644
--- a/testsuite/tests/typecheck/should_fail/T3613.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3613.stderr
@@ -7,9 +7,7 @@ T3613.hs:14:20:
     In the first argument of ‘fooThen’, namely ‘(bar >> undefined)’
 
 T3613.hs:17:24:
-    Couldn't match type ‘IO’ with ‘Maybe’
-    Expected type: Maybe ()
-      Actual type: IO ()
+    Couldn't match expected type ‘Maybe a0’ with actual type ‘IO ()’
     In a stmt of a 'do' block: bar
     In the first argument of ‘fooThen’, namely
       ‘(do { bar;
diff --git a/testsuite/tests/typecheck/should_fail/T5236.stderr b/testsuite/tests/typecheck/should_fail/T5236.stderr
index e1e136a249..7b5830c0ea 100644
--- a/testsuite/tests/typecheck/should_fail/T5236.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5236.stderr
@@ -1,10 +1,11 @@
-

-T5236.hs:13:9:

-    Couldn't match type ‘B’ with ‘A’

-    arising from a functional dependency between:

-      constraint ‘Id A B’

-        arising from the type signature for loop :: Id A B => Bool

-      instance ‘Id B B’ at T5236.hs:11:10-15

-    In the ambiguity check for: Id A B => Bool

-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

-    In the type signature for ‘loop’: loop :: Id A B => Bool

+
+T5236.hs:13:9:
+    Couldn't match type ‘B’ with ‘A’
+    arising from a functional dependency between:
+      constraint ‘Id A B’
+        arising from the type signature for loop :: Id A B => Bool
+      instance ‘Id B B’ at T5236.hs:11:10-15
+    In the ambiguity check for the type signature for ‘loop’:
+      loop :: Id A B => Bool
+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+    In the type signature for ‘loop’: loop :: Id A B => Bool
diff --git a/testsuite/tests/typecheck/should_fail/T5300.stderr b/testsuite/tests/typecheck/should_fail/T5300.stderr
index 912cd19842..14e069af9b 100644
--- a/testsuite/tests/typecheck/should_fail/T5300.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5300.stderr
@@ -1,33 +1,31 @@
 
 T5300.hs:11:7:
     Could not deduce (C1 a b c0)
-      arising from the ambiguity check for ‘f1’
     from the context (Monad m, C1 a b c)
       bound by the type signature for
                  f1 :: (Monad m, C1 a b c) => a -> StateT (T b) m a
       at T5300.hs:11:7-50
     The type variable ‘c0’ is ambiguous
-    In the ambiguity check for:
-      forall a b (m :: * -> *) c.
-      (Monad m, C1 a b c) =>
-      a -> StateT (T b) m a
+    In the ambiguity check for the type signature for ‘f1’:
+      f1 :: forall a b (m :: * -> *) c.
+            (Monad m, C1 a b c) =>
+            a -> StateT (T b) m a
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘f1’:
       f1 :: (Monad m, C1 a b c) => a -> StateT (T b) m a
 
 T5300.hs:14:7:
     Could not deduce (C2 a2 b2 c20)
-      arising from the ambiguity check for ‘f2’
     from the context (Monad m, C1 a1 b1 c1, C2 a2 b2 c2)
       bound by the type signature for
                  f2 :: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
                        a1 -> StateT (T b2) m a2
       at T5300.hs:14:7-69
     The type variable ‘c20’ is ambiguous
-    In the ambiguity check for:
-      forall a1 b2 (m :: * -> *) a2 b1 c1 c2.
-      (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
-      a1 -> StateT (T b2) m a2
+    In the ambiguity check for the type signature for ‘f2’:
+      f2 :: forall a1 b2 (m :: * -> *) a2 b1 c1 c2.
+            (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
+            a1 -> StateT (T b2) m a2
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘f2’:
       f2 :: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
diff --git a/testsuite/tests/typecheck/should_fail/T5691.stderr b/testsuite/tests/typecheck/should_fail/T5691.stderr
index 674ffc76d7..e4151c1769 100644
--- a/testsuite/tests/typecheck/should_fail/T5691.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5691.stderr
@@ -1,11 +1,12 @@
 
 T5691.hs:14:9:
     Couldn't match type ‘p’ with ‘PrintRuleInterp’
-    Expected type: PrintRuleInterp a
-      Actual type: p a
+    Expected type: p a
+      Actual type: PrintRuleInterp a
+    When checking that the pattern signature: p a
+      fits the type of its context: PrintRuleInterp a
     In the pattern: f :: p a
     In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f
-    In the instance declaration for ‘Test PrintRuleInterp’
 
 T5691.hs:15:24:
     Couldn't match type ‘p’ with ‘PrintRuleInterp’
diff --git a/testsuite/tests/typecheck/should_fail/T6069.stderr b/testsuite/tests/typecheck/should_fail/T6069.stderr
index 81b1552cba..eff2e8b5cf 100644
--- a/testsuite/tests/typecheck/should_fail/T6069.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6069.stderr
@@ -1,21 +1,21 @@
 
 T6069.hs:13:15:
-    Couldn't match type ‘ST s0 Int’ with ‘forall s. ST s b0’
-    Expected type: ST s0 Int -> b0
-      Actual type: (forall s. ST s b0) -> b0
+    Couldn't match type ‘ST s0 Int’ with ‘forall s. ST s a0’
+    Expected type: ST s0 Int -> a0
+      Actual type: (forall s. ST s a0) -> a0
     In the second argument of ‘(.)’, namely ‘runST’
     In the expression: print . runST
 
 T6069.hs:14:15:
-    Couldn't match type ‘ST s1 Int’ with ‘forall s. ST s b1’
-    Expected type: ST s1 Int -> b1
-      Actual type: (forall s. ST s b1) -> b1
+    Couldn't match type ‘ST s1 Int’ with ‘forall s. ST s a1’
+    Expected type: ST s1 Int -> a1
+      Actual type: (forall s. ST s a1) -> a1
     In the second argument of ‘(.)’, namely ‘runST’
     In the expression: (print . runST)
 
 T6069.hs:15:16:
-    Couldn't match type ‘ST s2 Int’ with ‘forall s. ST s b2’
-    Expected type: ST s2 Int -> b2
-      Actual type: (forall s. ST s b2) -> b2
+    Couldn't match type ‘ST s2 Int’ with ‘forall s. ST s a2’
+    Expected type: ST s2 Int -> a2
+      Actual type: (forall s. ST s a2) -> a2
     In the second argument of ‘(.)’, namely ‘runST’
     In the first argument of ‘($)’, namely ‘(print . runST)’
diff --git a/testsuite/tests/typecheck/should_fail/T7279.stderr b/testsuite/tests/typecheck/should_fail/T7279.stderr
index df0328ccdd..10acbbec8b 100644
--- a/testsuite/tests/typecheck/should_fail/T7279.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7279.stderr
@@ -1,11 +1,11 @@
 
 T7279.hs:6:10:
     Could not deduce (Show b0)
-      arising from the ambiguity check for an instance declaration
     from the context (Eq a, Show b)
       bound by an instance declaration: (Eq a, Show b) => Eq (T a)
       at T7279.hs:6:10-35
     The type variable ‘b0’ is ambiguous
-    In the ambiguity check for: forall a b. (Eq a, Show b) => Eq (T a)
+    In the ambiguity check for an instance declaration:
+      forall a b. (Eq a, Show b) => Eq (T a)
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the instance declaration for ‘Eq (T a)’
diff --git a/testsuite/tests/typecheck/should_fail/T8392a.stderr b/testsuite/tests/typecheck/should_fail/T8392a.stderr
index 9be12a5b0b..a51cc83932 100644
--- a/testsuite/tests/typecheck/should_fail/T8392a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8392a.stderr
@@ -3,5 +3,6 @@ T8392a.hs:6:8:
     Couldn't match type ‘Int’ with ‘Bool’
     Inaccessible code in
       the type signature for foo :: (Int ~ Bool) => a -> a
-    In the ambiguity check for: forall a. (Int ~ Bool) => a -> a
+    In the ambiguity check for the type signature for ‘foo’:
+      foo :: forall a. (Int ~ Bool) => a -> a
     In the type signature for ‘foo’: foo :: (Int ~ Bool) => a -> a
diff --git a/testsuite/tests/typecheck/should_fail/T8883.stderr b/testsuite/tests/typecheck/should_fail/T8883.stderr
index 28730ae9c7..27b4d943f1 100644
--- a/testsuite/tests/typecheck/should_fail/T8883.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8883.stderr
@@ -3,6 +3,6 @@ T8883.hs:20:1:
     Non type-variable argument in the constraint: Functor (PF a)
     (Use FlexibleContexts to permit this)
     When checking that ‘fold’ has the inferred type
-      fold :: forall a b.
+      fold :: forall b a.
               (Functor (PF a), Regular a) =>
               (PF a b -> b) -> a -> b
diff --git a/testsuite/tests/typecheck/should_fail/mc21.stderr b/testsuite/tests/typecheck/should_fail/mc21.stderr
index e3a8b882c8..0e727291d6 100644
--- a/testsuite/tests/typecheck/should_fail/mc21.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc21.stderr
@@ -1,9 +1,9 @@
-

-mc21.hs:12:26:

-    Couldn't match type ‘a’ with ‘[a]’

-      ‘a’ is a rigid type variable bound by

-          a type expected by the context: [a] -> [[a]] at mc21.hs:12:9

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

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

-    In the expression: take 5

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

+
+mc21.hs:12:26:
+    Couldn't match type ‘a’ with ‘[a]’
+      ‘a’ is a rigid type variable bound by
+          a type expected by the context: [a] -> [[a]] at mc21.hs:12:9
+    Expected type: [a] -> [[a]]
+      Actual type: [[a]] -> [[a]]
+    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/mc22.stderr b/testsuite/tests/typecheck/should_fail/mc22.stderr
index 104bcffe4c..ebae89eb9b 100644
--- a/testsuite/tests/typecheck/should_fail/mc22.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc22.stderr
@@ -1,21 +1,21 @@
-

-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 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: [t a] -> [t a]
+    Relevant bindings include foo :: [t [Char]] (bound at mc22.hs:8:1)
+    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/mc23.stderr b/testsuite/tests/typecheck/should_fail/mc23.stderr
index cdb10800e4..9f4a467a9d 100644
--- a/testsuite/tests/typecheck/should_fail/mc23.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc23.stderr
@@ -1,9 +1,9 @@
 
 mc23.hs:9:29:
-    Couldn't match type ‘[a0]’ with ‘a -> b’
-    Expected type: (a -> b) -> [a] -> t a
+    Couldn't match type ‘[a0]’ with ‘[a] -> m a’
+    Expected type: (a -> b) -> [a] -> m a
       Actual type: [a0] -> [a0]
-    Relevant bindings include z :: t b (bound at mc23.hs:9:1)
+    Relevant bindings include z :: m b (bound at mc23.hs:9:1)
     Possible cause: ‘take’ is applied to too many arguments
     In the expression: take 5
     In a stmt of a monad comprehension: then take 5 by x
diff --git a/testsuite/tests/typecheck/should_fail/mc24.stderr b/testsuite/tests/typecheck/should_fail/mc24.stderr
index 495693c9f8..3260edbcb7 100644
--- a/testsuite/tests/typecheck/should_fail/mc24.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc24.stderr
@@ -1,8 +1,9 @@
-

-mc24.hs:10:31:

-    Couldn't match type ‘[a0]’ with ‘a -> Integer’

-    Expected type: (a -> Integer) -> [a] -> t [a]

-      Actual type: [a0] -> [a0]

-    Possible cause: ‘take’ is applied to too many arguments

-    In the expression: take 2

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

+
+mc24.hs:10:31:
+    Couldn't match type ‘[a0]’ with ‘[a] -> m [a]’
+    Expected type: (a -> Integer) -> [a] -> m [a]
+      Actual type: [a0] -> [a0]
+    Relevant bindings include foo :: m Int (bound at mc24.hs:8:1)
+    Possible cause: ‘take’ is applied to too many arguments
+    In the expression: take 2
+    In a stmt of a monad comprehension: then group by x using take 2
diff --git a/testsuite/tests/typecheck/should_fail/mc25.stderr b/testsuite/tests/typecheck/should_fail/mc25.stderr
index e145af4339..fb136bcdcb 100644
--- a/testsuite/tests/typecheck/should_fail/mc25.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc25.stderr
@@ -1,18 +1,18 @@
-

-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

+
+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 ‘a -> t’ with ‘Int’
+    Expected type: (a -> t) -> [a] -> [t1 a]
+      Actual type: Int -> [t1 a] -> [t1 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
diff --git a/testsuite/tests/typecheck/should_fail/tcfail080.stderr b/testsuite/tests/typecheck/should_fail/tcfail080.stderr
index 4e02b3e012..fcd974da90 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail080.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail080.stderr
@@ -1,11 +1,10 @@
-

-tcfail080.hs:27:1:

-    Could not deduce (Collection c0 a)

-      arising from the ambiguity check for ‘q’

-    from the context (Collection c a)

-      bound by the inferred type for ‘q’: Collection c a => a -> Bool

-      at tcfail080.hs:27:1-27

-    The type variable ‘c0’ is ambiguous

-    When checking that ‘q’ has the inferred type

-      q :: forall (c :: * -> *) a. Collection c a => a -> Bool

-    Probable cause: the inferred type is ambiguous

+
+tcfail080.hs:27:1:
+    Could not deduce (Collection c0 a)
+    from the context (Collection c a)
+      bound by the inferred type for ‘q’: Collection c a => a -> Bool
+      at tcfail080.hs:27:1-27
+    The type variable ‘c0’ is ambiguous
+    When checking that ‘q’ has the inferred type
+      q :: forall (c :: * -> *) a. Collection c a => a -> Bool
+    Probable cause: the inferred type is ambiguous
diff --git a/testsuite/tests/typecheck/should_fail/tcfail097.stderr b/testsuite/tests/typecheck/should_fail/tcfail097.stderr
index cbd5612b96..821972402b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail097.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail097.stderr
@@ -1,10 +1,11 @@
 
 tcfail097.hs:5:6:
-    Could not deduce (Eq a0) arising from the ambiguity check for ‘f’
+    Could not deduce (Eq a0)
     from the context (Eq a)
       bound by the type signature for f :: Eq a => Int -> Int
       at tcfail097.hs:5:6-23
     The type variable ‘a0’ is ambiguous
-    In the ambiguity check for: forall a. Eq a => Int -> Int
+    In the ambiguity check for the type signature for ‘f’:
+      f :: forall a. Eq a => Int -> Int
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘f’: f :: Eq a => Int -> Int
diff --git a/testsuite/tests/typecheck/should_fail/tcfail098.stderr b/testsuite/tests/typecheck/should_fail/tcfail098.stderr
index 94ade75946..8ac2960d3c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail098.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail098.stderr
@@ -1,11 +1,11 @@
 
 tcfail098.hs:12:10:
     Could not deduce (Bar a0)
-      arising from the ambiguity check for an instance declaration
     from the context (Bar a)
       bound by an instance declaration: Bar a => Bar Bool
       at tcfail098.hs:12:10-26
     The type variable ‘a0’ is ambiguous
-    In the ambiguity check for: forall a. Bar a => Bar Bool
+    In the ambiguity check for an instance declaration:
+      forall a. Bar a => Bar Bool
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the instance declaration for ‘Bar Bool’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail142.stderr b/testsuite/tests/typecheck/should_fail/tcfail142.stderr
index e2338eb917..fecb2f370f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail142.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail142.stderr
@@ -1,11 +1,11 @@
 
 tcfail142.hs:18:8:
     Could not deduce (Bar a0 r)
-      arising from the ambiguity check for ‘bar’
     from the context (Bar a r)
       bound by the type signature for bar :: Bar a r => r -> ()
       at tcfail142.hs:18:8-25
     The type variable ‘a0’ is ambiguous
-    In the ambiguity check for: forall r a. Bar a r => r -> ()
+    In the ambiguity check for the type signature for ‘bar’:
+      bar :: forall r a. Bar a r => r -> ()
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘bar’: bar :: Bar a r => r -> ()
diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
index f48d15369e..577c36e94b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
@@ -10,7 +10,7 @@ tcfail174.hs:13:14:
       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
+      at tcfail174.hs:13:1-14
     Expected type: Capture (forall x. x -> a)
       Actual type: Capture (forall a. a -> a)
     Relevant bindings include
@@ -21,7 +21,7 @@ tcfail174.hs:13:14:
 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
+          the type forall a1. a1 -> a1 at tcfail174.hs:1:1
       ‘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)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail189.stderr b/testsuite/tests/typecheck/should_fail/tcfail189.stderr
index 6bd08a266c..380b014947 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail189.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail189.stderr
@@ -1,8 +1,8 @@
-

-tcfail189.hs:10:31:

-    Couldn't match type ‘[a0]’ with ‘a -> Integer’

-    Expected type: (a -> Integer) -> [a] -> [[a]]

-      Actual type: [a0] -> [a0]

-    Possible cause: ‘take’ is applied to too many arguments

-    In the expression: take 2

-    In a stmt of a list comprehension: then group by x using take 2

+
+tcfail189.hs:10:31:
+    Couldn't match type ‘[a0]’ with ‘[a] -> [[a]]’
+    Expected type: (a -> Integer) -> [a] -> [[a]]
+      Actual type: [a0] -> [a0]
+    Possible cause: ‘take’ is applied to too many arguments
+    In the expression: take 2
+    In a stmt of a list comprehension: then group by x using take 2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail191.stderr b/testsuite/tests/typecheck/should_fail/tcfail191.stderr
index c766699880..2158927e55 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail191.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail191.stderr
@@ -4,6 +4,6 @@ tcfail191.hs:11:26:
       ‘a’ is a rigid type variable bound by
           a type expected by the context: [a] -> [[a]] at tcfail191.hs:11:9
     Expected type: [a] -> [[a]]
-      Actual type: [a] -> [a]
+      Actual type: [[a]] -> [[a]]
     In the expression: take 5
     In a stmt of a list comprehension: then group using take 5