Visible type application

This re-working of the typechecker algorithm is based on the paper "Visible type application", by Richard Eisenberg, Stephanie Weirich, and Hamidhasan Ahmed, to be published at ESOP'16. This patch introduces -XTypeApplications, which allows users to say, for example `id @Int`, which has type `Int -> Int`. See the changes to the user manual for details. This patch addresses tickets #10619, #5296, #10589.
author: Richard Eisenberg <eir@cis.upenn.edu> 2015-12-24 14:33:19 -0500
committer: Richard Eisenberg <eir@cis.upenn.edu> 2015-12-24 14:37:39 -0500
commit: 2db18b8135335da2da9918b722699df684097be9 (patch)
tree: 660dd90916aa6568694bbe39cdab83c7af98c5d7 /testsuite
parent: 48db13d279d592ed3044cbaf3513854bcb0d3dce (diff)
download: haskell-2db18b8135335da2da9918b722699df684097be9.tar.gz
202 files changed, 1991 insertions, 1375 deletions
diff --git a/testsuite/tests/ado/ado002.stderr b/testsuite/tests/ado/ado002.stderr
index cdfdbc4b19..9e7eba0a67 100644
--- a/testsuite/tests/ado/ado002.stderr
+++ b/testsuite/tests/ado/ado002.stderr
@@ -1,55 +1,81 @@
 
 ado002.hs:8:8: error:
-    Couldn't match expected type ‘Char -> IO t1’
-                with actual type ‘IO Char’
-    The function ‘getChar’ is applied to one argument,
-    but its type ‘IO Char’ has none
-    In a stmt of a 'do' block: y <- getChar 'a'
-    In the expression:
-      do { x <- getChar;
-           y <- getChar 'a';
-           print (x, y) }
+    • Couldn't match expected type ‘Char -> IO t1’
+                  with actual type ‘IO Char’
+    • The function ‘getChar’ is applied to one argument,
+      but its type ‘IO Char’ has none
+      In a stmt of a 'do' block: y <- getChar 'a'
+      In the expression:
+        do { x <- getChar;
+             y <- getChar 'a';
+             print (x, y) }
 
 ado002.hs:9:3: error:
-    Couldn't match type ‘()’ with ‘Int’
-    Expected type: IO Int
-      Actual type: IO ()
-    In a stmt of a 'do' block: print (x, y)
-    In the expression:
-      do { x <- getChar;
-           y <- getChar 'a';
-           print (x, y) }
+    • Couldn't match type ‘()’ with ‘Int’
+      Expected type: IO Int
+        Actual type: IO ()
+    • In a stmt of a 'do' block: print (x, y)
+      In the expression:
+        do { x <- getChar;
+             y <- getChar 'a';
+             print (x, y) }
+      In an equation for ‘f’:
+          f = do { x <- getChar;
+                   y <- getChar 'a';
+                   print (x, y) }
 
 ado002.hs:15:11: error:
-    Couldn't match expected type ‘Int’ with actual type ‘Char’
-    In the expression: y
-    In a stmt of a 'do' block: return (y, x)
+    • Couldn't match expected type ‘Int’ with actual type ‘Char’
+    • In the expression: y
+      In a stmt of a 'do' block: return (y, x)
+      In the expression:
+        do { x <- getChar;
+             y <- getChar;
+             return (y, x) }
 
 ado002.hs:15:13: error:
-    Couldn't match expected type ‘Int’ with actual type ‘Char’
-    In the expression: x
-    In a stmt of a 'do' block: return (y, x)
+    • Couldn't match expected type ‘Int’ with actual type ‘Char’
+    • In the expression: x
+      In a stmt of a 'do' block: return (y, x)
+      In the expression:
+        do { x <- getChar;
+             y <- getChar;
+             return (y, x) }
 
 ado002.hs:23:9: error:
-    Couldn't match expected type ‘Char -> IO t0’
-                with actual type ‘IO Char’
-    The function ‘getChar’ is applied to one argument,
-    but its type ‘IO Char’ has none
-    In a stmt of a 'do' block: x5 <- getChar x4
-    In the expression:
-      do { x1 <- getChar;
-           x2 <- getChar;
-           x3 <- const (return ()) x1;
-           x4 <- getChar;
-           x5 <- getChar x4;
-           return (x2, x4) }
+    • Couldn't match expected type ‘Char -> IO t0’
+                  with actual type ‘IO Char’
+    • The function ‘getChar’ is applied to one argument,
+      but its type ‘IO Char’ has none
+      In a stmt of a 'do' block: x5 <- getChar x4
+      In the expression:
+        do { x1 <- getChar;
+             x2 <- getChar;
+             x3 <- const (return ()) x1;
+             x4 <- getChar;
+             x5 <- getChar x4;
+             return (x2, x4) }
 
 ado002.hs:24:11: error:
-    Couldn't match expected type ‘Int’ with actual type ‘Char’
-    In the expression: x2
-    In a stmt of a 'do' block: return (x2, x4)
+    • Couldn't match expected type ‘Int’ with actual type ‘Char’
+    • In the expression: x2
+      In a stmt of a 'do' block: return (x2, x4)
+      In the expression:
+        do { x1 <- getChar;
+             x2 <- getChar;
+             x3 <- const (return ()) x1;
+             x4 <- getChar;
+             x5 <- getChar x4;
+             return (x2, x4) }
 
 ado002.hs:24:14: error:
-    Couldn't match expected type ‘Int’ with actual type ‘Char’
-    In the expression: x4
-    In a stmt of a 'do' block: return (x2, x4)
+    • Couldn't match expected type ‘Int’ with actual type ‘Char’
+    • In the expression: x4
+      In a stmt of a 'do' block: return (x2, x4)
+      In the expression:
+        do { x1 <- getChar;
+             x2 <- getChar;
+             x3 <- const (return ()) x1;
+             x4 <- getChar;
+             x5 <- getChar x4;
+             return (x2, x4) }
diff --git a/testsuite/tests/annotations/should_fail/annfail08.stderr b/testsuite/tests/annotations/should_fail/annfail08.stderr
index 6fafaf919e..47a54243fe 100644
--- a/testsuite/tests/annotations/should_fail/annfail08.stderr
+++ b/testsuite/tests/annotations/should_fail/annfail08.stderr
@@ -5,7 +5,7 @@ annfail08.hs:9:1: error:
         (maybe you haven't applied a function to enough arguments?)
     • In the annotation: {-# ANN f (id + 1) #-}
 
-annfail08.hs:9:15: error:
+annfail08.hs:9:12: error:
     • No instance for (Num (a0 -> a0)) arising from a use of ‘+’
         (maybe you haven't applied a function to enough arguments?)
     • In the annotation: {-# ANN f (id + 1) #-}
diff --git a/testsuite/tests/arrows/should_fail/T5380.stderr b/testsuite/tests/arrows/should_fail/T5380.stderr
index 2aeb01f1c0..0e258a2c28 100644
--- a/testsuite/tests/arrows/should_fail/T5380.stderr
+++ b/testsuite/tests/arrows/should_fail/T5380.stderr
@@ -8,6 +8,8 @@ T5380.hs:7:27: error:
         at T5380.hs:6:10
     • In the expression: b
       In the expression: proc () -> if b then f -< () else f -< ()
+      In an equation for ‘testB’:
+          testB b f = proc () -> if b then f -< () else f -< ()
     • Relevant bindings include
         b :: not_bool (bound at T5380.hs:7:7)
         testB :: not_bool -> (() -> ()) -> () -> not_unit
@@ -24,6 +26,7 @@ T5380.hs:7:34: error:
         Actual type: () -> ()
     • In the expression: f
       In the command: f -< ()
+      In the expression: proc () -> if b then f -< () else f -< ()
     • Relevant bindings include
         testB :: not_bool -> (() -> ()) -> () -> not_unit
           (bound at T5380.hs:7:1)
diff --git a/testsuite/tests/boxy/all.T b/testsuite/tests/boxy/all.T
index 0294d01629..d2be5e314b 100644
--- a/testsuite/tests/boxy/all.T
+++ b/testsuite/tests/boxy/all.T
@@ -1,6 +1,6 @@
 # Boxy-type tests
 
-test('Base1',    expect_broken(4295), compile, [''])
+test('Base1',    normal, compile, [''])
 test('Church1',  expect_broken(4295), compile, [''])
 test('Church2',  expect_broken(1330), compile_fail, [''])
 test('PList1',   expect_broken(4295), compile, [''])
@@ -8,4 +8,4 @@ test('PList2',   expect_broken(4295), compile, [''])
 test('SystemF',  expect_broken(4295), compile, [''])
 test('boxy',     expect_broken(4295), compile, [''])
 test('Compose',  normal, compile, [''])
-test('T2193',    normal, compile_and_run, [''])
+test('T2193',    expect_broken(4295), compile_and_run, [''])
diff --git a/testsuite/tests/deSugar/should_compile/T2431.stderr b/testsuite/tests/deSugar/should_compile/T2431.stderr
index 241a13c777..37bf170f28 100644
--- a/testsuite/tests/deSugar/should_compile/T2431.stderr
+++ b/testsuite/tests/deSugar/should_compile/T2431.stderr
@@ -37,7 +37,9 @@ a2 = GHC.Types.TrNameS "'Refl"#
 -- RHS size: {terms: 5, types: 0, coercions: 0}
 T2431.$tc'Refl :: GHC.Types.TyCon
 [GblId[ReflectionId], Caf=NoCafRefs, Str=DmdType]
-T2431.$tc'Refl = GHC.Types.TyCon 0## 0## T2431.$trModule a2
+T2431.$tc'Refl =
+  GHC.Types.TyCon
+    15026191172322750497## 3898273167927206410## T2431.$trModule a2
 
 -- RHS size: {terms: 2, types: 0, coercions: 0}
 a3 :: GHC.Types.TrName
@@ -47,7 +49,9 @@ a3 = GHC.Types.TrNameS ":~:"#
 -- RHS size: {terms: 5, types: 0, coercions: 0}
 T2431.$tc:~: :: GHC.Types.TyCon
 [GblId[ReflectionId], Caf=NoCafRefs, Str=DmdType]
-T2431.$tc:~: = GHC.Types.TyCon 0## 0## T2431.$trModule a3
+T2431.$tc:~: =
+  GHC.Types.TyCon
+    9759653149176674453## 12942818337407067047## T2431.$trModule a3
 
 -- RHS size: {terms: 4, types: 8, coercions: 0}
 absurd :: forall a. Int :~: Bool -> a
diff --git a/testsuite/tests/driver/T2182.stderr b/testsuite/tests/driver/T2182.stderr
index 0585e4c701..b5a5f1d349 100644
--- a/testsuite/tests/driver/T2182.stderr
+++ b/testsuite/tests/driver/T2182.stderr
@@ -5,7 +5,7 @@ T2182.hs:5:5: error:
     In the expression: show (\ x -> x)
     In an equation for ‘y’: y = show (\ x -> x)
 
-T2182.hs:6:15: error:
+T2182.hs:6:5: error:
     No instance for (Eq (t0 -> t0)) arising from a use of ‘==’
       (maybe you haven't applied a function to enough arguments?)
     In the expression: (\ x -> x) == (\ y -> y)
@@ -17,7 +17,7 @@ T2182.hs:5:5: error:
     In the expression: show (\ x -> x)
     In an equation for ‘y’: y = show (\ x -> x)
 
-T2182.hs:6:15: error:
+T2182.hs:6:5: error:
     No instance for (Eq (t0 -> t0)) arising from a use of ‘==’
       (maybe you haven't applied a function to enough arguments?)
     In the expression: (\ x -> x) == (\ y -> y)
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index b6d04ef6c1..4120e91d99 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -37,7 +37,8 @@ expectedGhcOnlyExtensions = ["RelaxedLayout",
                              "UndecidableSuperClasses",
                              "TemplateHaskellQuotes",
                              "MonadFailDesugaring",
-                             "TypeInType"]
+                             "TypeInType",
+                             "TypeApplications"]
 
 expectedCabalOnlyExtensions :: [String]
 expectedCabalOnlyExtensions = ["Generics",
diff --git a/testsuite/tests/driver/werror.stderr b/testsuite/tests/driver/werror.stderr
index ce6dba6347..a20dc5e689 100644
--- a/testsuite/tests/driver/werror.stderr
+++ b/testsuite/tests/driver/werror.stderr
@@ -1,30 +1,30 @@
 
-werror.hs:6:1: Warning:
+werror.hs:6:1: warning:
     Top-level binding with no type signature: main :: IO ()
 
-werror.hs:7:13: Warning:
+werror.hs:7:13: warning:
     This binding for ‘main’ shadows the existing binding
       defined at werror.hs:6:1
 
-werror.hs:7:13: Warning: Defined but not used: ‘main’
+werror.hs:7:13: warning: Defined but not used: ‘main’
 
-werror.hs:8:1: Warning:
+werror.hs:8:1: warning:
     Tab character found here.
     Please use spaces instead.
 
-werror.hs:10:1: Warning: Defined but not used: ‘f’
+werror.hs:10:1: warning: Defined but not used: ‘f’
 
-werror.hs:10:1: Warning:
+werror.hs:10:1: warning:
     Top-level binding with no type signature:
-      f :: forall r r1. [r] -> [r1]
+      f :: forall t t1. [t] -> [t1]
 
-werror.hs:10:1: Warning:
+werror.hs:10:1: warning:
     Pattern match(es) are redundant
     In an equation for ‘f’: f [] = ...
 
-werror.hs:10:1: Warning:
+werror.hs:10:1: warning:
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’: Patterns not matched: (_:_)
 
-<no location info>: 
+<no location info>: error: 
 Failing due to -Werror.
diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr
index 0ec531c526..4c9097eacd 100644
--- a/testsuite/tests/gadt/T3169.stderr
+++ b/testsuite/tests/gadt/T3169.stderr
@@ -9,6 +9,9 @@ T3169.hs:13:22: error:
         Actual type: Map (a, b) elt
     • 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 }
     • Relevant bindings include
         m :: Map (a, b) elt (bound at T3169.hs:12:17)
         b :: b (bound at T3169.hs:12:13)
diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index 829dfa0e2b..215426ed15 100644
--- a/testsuite/tests/gadt/gadt-escape1.stderr
+++ b/testsuite/tests/gadt/gadt-escape1.stderr
@@ -10,8 +10,10 @@ gadt-escape1.hs:19:58: error:
         the inferred type of weird1 :: r at gadt-escape1.hs:19:1
       Possible fix: add a type signature for ‘weird1’
       Expected type: r
-      Actual type: ExpGADT t
+        Actual type: ExpGADT t
     • In the expression: a
       In a case alternative: Hidden (ExpInt _) a -> a
+      In the expression:
+        case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }
     • Relevant bindings include
         weird1 :: r (bound at gadt-escape1.hs:19:1)
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index 44b100b059..57ee3fdc92 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -3,14 +3,15 @@ gadt13.hs:15:13: error:
     • Couldn't match expected type ‘r’
                   with actual type ‘String -> [Char]’
         ‘r’ is untouchable
-          inside the constraints: r1 ~ Int
+          inside the constraints: t ~ Int
           bound by a pattern with constructor: I :: Int -> Term Int,
                    in an equation for ‘shw’
           at gadt13.hs:15:6-8
       ‘r’ is a rigid type variable bound by
-        the inferred type of shw :: Term r1 -> r at gadt13.hs:15:1
+        the inferred type of shw :: Term t -> r at gadt13.hs:15:1
       Possible fix: add a type signature for ‘shw’
-    • In the expression: ("I " ++) . shows t
+    • Possible cause: ‘(.)’ is applied to too many arguments
+      In the expression: ("I " ++) . shows t
       In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
     • Relevant bindings include
-        shw :: Term r1 -> r (bound at gadt13.hs:15:1)
+        shw :: Term t -> r (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index 8720d7fe10..93b8c70c1f 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -13,6 +13,7 @@ gadt7.hs:16:38: error:
       Possible fix: add a type signature for ‘i1b’
     • In the expression: y1
       In a case alternative: K -> y1
+      In the expression: case t1 of { K -> y1 }
     • Relevant bindings include
         y1 :: r1 (bound at gadt7.hs:16:16)
         y :: r1 (bound at gadt7.hs:16:7)
diff --git a/testsuite/tests/gadt/rw.stderr b/testsuite/tests/gadt/rw.stderr
index 39529a7003..c79bb72b4c 100644
--- a/testsuite/tests/gadt/rw.stderr
+++ b/testsuite/tests/gadt/rw.stderr
@@ -13,16 +13,17 @@ rw.hs:14:47: error:
         v :: T a (bound at rw.hs:13:10)
         writeInt :: T a -> IORef a -> IO () (bound at rw.hs:13:1)
 
-rw.hs:19:51: error:
+rw.hs:19:43: error:
     • Couldn't match type ‘a’ with ‘Bool’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           readBool :: forall a. T a -> IORef a -> IO ()
         at rw.hs:16:12
-      Expected type: a -> Bool
-        Actual type: Bool -> Bool
-    • In the second argument of ‘(.)’, namely ‘not’
-      In the second argument of ‘(>>=)’, namely ‘(print . not)’
+      Expected type: a -> IO ()
+        Actual type: Bool -> IO ()
+    • In the second argument of ‘(>>=)’, namely ‘(print . not)’
+      In the expression: readIORef ref >>= (print . not)
+      In a case alternative: ~(Lb x) -> readIORef ref >>= (print . not)
     • Relevant bindings include
         ref :: IORef a (bound at rw.hs:17:12)
         v :: T a (bound at rw.hs:17:10)
diff --git a/testsuite/tests/ghc-api/annotations/T10280.stderr b/testsuite/tests/ghc-api/annotations/T10280.stderr
index f2a2a56e63..e5ec0774da 100644
--- a/testsuite/tests/ghc-api/annotations/T10280.stderr
+++ b/testsuite/tests/ghc-api/annotations/T10280.stderr
@@ -1,8 +1,8 @@
-
-Test10280.hs:4:8: error:
-    Variable not in scope:
-      atomicModifyIORef :: t0 -> (a0 -> (b0, ())) -> t
-
-Test10280.hs:4:26: error: Variable not in scope: ciTokens
-
-Test10280.hs:4:44: error: Variable not in scope: f :: a0 -> b0
+
+Test10280.hs:4:8: error:
+    Variable not in scope:
+      atomicModifyIORef :: t0 -> (a0 -> (t1, ())) -> t
+
+Test10280.hs:4:26: error: Variable not in scope: ciTokens
+
+Test10280.hs:4:44: error: Variable not in scope: f :: a0 -> t1
diff --git a/testsuite/tests/ghc-api/annotations/T10357.stderr b/testsuite/tests/ghc-api/annotations/T10357.stderr
index 09f29ddfb8..971657668f 100644
--- a/testsuite/tests/ghc-api/annotations/T10357.stderr
+++ b/testsuite/tests/ghc-api/annotations/T10357.stderr
@@ -4,34 +4,34 @@ Test10357.hs:4:13: error: Variable not in scope: one
 Test10357.hs:4:19: error: Variable not in scope: x
 
 Test10357.hs:5:7: error:
-    Variable not in scope: multPoly :: t0 -> t1 -> t
+    Variable not in scope: multPoly :: t0 -> t2 -> t
 
 Test10357.hs:6:10: error:
-    Variable not in scope: poly :: t2 -> [Double] -> t0
+    Variable not in scope: poly :: t1 -> [Double] -> t0
 
 Test10357.hs:6:15: error:
-    Data constructor not in scope: LE
-    Perhaps you meant ‘LT’ (imported from Prelude)
+    • Data constructor not in scope: LE
+    • Perhaps you meant ‘LT’ (imported from Prelude)
 
 Test10357.hs:7:10: error:
-    Variable not in scope: addPoly :: t3 -> t4 -> t1
+    Variable not in scope: addPoly :: t3 -> t6 -> t2
 
 Test10357.hs:7:19: error:
-    Variable not in scope: poly :: t6 -> [Double] -> t5
+    Variable not in scope: poly :: t5 -> [Double] -> t4
 
 Test10357.hs:7:24: error:
-    Data constructor not in scope: LE
-    Perhaps you meant ‘LT’ (imported from Prelude)
+    • Data constructor not in scope: LE
+    • Perhaps you meant ‘LT’ (imported from Prelude)
 
 Test10357.hs:7:43: error:
-    Variable not in scope: multPoly :: t5 -> t -> t3
+    Variable not in scope: multPoly :: t4 -> t -> t3
 
 Test10357.hs:8:19: error:
     Variable not in scope: poly :: t8 -> [Double] -> t7
 
 Test10357.hs:8:24: error:
-    Data constructor not in scope: LE
-    Perhaps you meant ‘LT’ (imported from Prelude)
+    • Data constructor not in scope: LE
+    • Perhaps you meant ‘LT’ (imported from Prelude)
 
 Test10357.hs:8:43: error:
-    Variable not in scope: multPoly :: t7 -> t -> t4
+    Variable not in scope: multPoly :: t7 -> t -> t6
diff --git a/testsuite/tests/ghci.debugger/scripts/break003.stderr b/testsuite/tests/ghci.debugger/scripts/break003.stderr
index c19e8b45ce..66310e5355 100644
--- a/testsuite/tests/ghci.debugger/scripts/break003.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/break003.stderr
@@ -1,5 +1,5 @@
 
 <interactive>:4:1: error:
-    No instance for (Show (t1 -> t)) arising from a use of ‘print’
-      (maybe you haven't applied a function to enough arguments?)
-    In a stmt of an interactive GHCi command: print it
+    • No instance for (Show (t -> a2)) arising from a use of ‘print’
+        (maybe you haven't applied a function to enough arguments?)
+    • In a stmt of an interactive GHCi command: print it
diff --git a/testsuite/tests/ghci.debugger/scripts/break003.stdout b/testsuite/tests/ghci.debugger/scripts/break003.stdout
index 1d0844c6cc..e1f4d351d1 100644
--- a/testsuite/tests/ghci.debugger/scripts/break003.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break003.stdout
@@ -1,6 +1,6 @@
 Breakpoint 0 activated at ../Test3.hs:2:18-31
 Stopped in Main.mymap, ../Test3.hs:2:18-31
-_result :: [t] = _
-f :: t1 -> t = _
-x :: t1 = _
-xs :: [t1] = [_]
+_result :: [a2] = _
+f :: t -> a2 = _
+x :: t = _
+xs :: [t] = [_]
diff --git a/testsuite/tests/ghci.debugger/scripts/break005.stdout b/testsuite/tests/ghci.debugger/scripts/break005.stdout
index 81eae63726..d6b287eb58 100644
--- a/testsuite/tests/ghci.debugger/scripts/break005.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break005.stdout
@@ -4,7 +4,7 @@ a :: Integer = 1
 left :: [Integer] = _
 right :: [Integer] = _
 Stopped in QSort.qsort, ../QSort.hs:5:17-26
-_result :: [t] = _
-left :: [t] = _
+_result :: [a2] = _
+left :: [a2] = _
 ()
 left = []
diff --git a/testsuite/tests/ghci.debugger/scripts/break006.stderr b/testsuite/tests/ghci.debugger/scripts/break006.stderr
index 3b57eb3a64..9098cc9c65 100644
--- a/testsuite/tests/ghci.debugger/scripts/break006.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/break006.stderr
@@ -1,9 +1,9 @@
 
 <interactive>:4:1: error:
-    • No instance for (Show t) arising from a use of ‘print’
-      Cannot resolve unknown runtime type ‘t’
+    • No instance for (Show a2) arising from a use of ‘print’
+      Cannot resolve unknown runtime type ‘a2’
       Use :print or :force to determine these types
-      Relevant bindings include it :: t (bound at <interactive>:4:1)
+      Relevant bindings include it :: a2 (bound at <interactive>:4:1)
       These potential instances exist:
         instance (Show a, Show b) => Show (Either a b)
           -- Defined in ‘Data.Either’
@@ -15,10 +15,10 @@
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:6:1: error:
-    • No instance for (Show t) arising from a use of ‘print’
-      Cannot resolve unknown runtime type ‘t’
+    • No instance for (Show a2) arising from a use of ‘print’
+      Cannot resolve unknown runtime type ‘a2’
       Use :print or :force to determine these types
-      Relevant bindings include it :: t (bound at <interactive>:6:1)
+      Relevant bindings include it :: a2 (bound at <interactive>:6:1)
       These potential instances exist:
         instance (Show a, Show b) => Show (Either a b)
           -- Defined in ‘Data.Either’
diff --git a/testsuite/tests/ghci.debugger/scripts/break006.stdout b/testsuite/tests/ghci.debugger/scripts/break006.stdout
index d8f1b65864..93326416e0 100644
--- a/testsuite/tests/ghci.debugger/scripts/break006.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break006.stdout
@@ -1,13 +1,13 @@
 Stopped in Main.mymap, ../Test3.hs:2:18-31
-_result :: [t] = _
-f :: Integer -> t = _
+_result :: [a2] = _
+f :: Integer -> a2 = _
 x :: Integer = 1
 xs :: [Integer] = [2,3]
 xs :: [Integer] = [2,3]
 x :: Integer = 1
-f :: Integer -> t = _
-_result :: [t] = _
-y = (_t1::t)
+f :: Integer -> a2 = _
+_result :: [a2] = _
+y = (_t1::a2)
 y = 2
 xs :: [Integer] = [2,3]
 x :: Integer = 1
diff --git a/testsuite/tests/ghci.debugger/scripts/hist001.stdout b/testsuite/tests/ghci.debugger/scripts/hist001.stdout
index 7ef5dc1e8e..c5b2787db5 100644
--- a/testsuite/tests/ghci.debugger/scripts/hist001.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/hist001.stdout
@@ -9,25 +9,25 @@ _result :: [a] = _
 -6  : mymap (../Test3.hs:2:18-31)
 <end of history>
 Logged breakpoint at ../Test3.hs:2:22-31
-_result :: [t]
-f :: t1 -> t
-xs :: [t1]
-xs :: [t1] = []
-f :: t1 -> t = _
-_result :: [t] = _
+_result :: [a2]
+f :: t -> a2
+xs :: [t]
+xs :: [t] = []
+f :: t -> a2 = _
+_result :: [a2] = _
 Logged breakpoint at ../Test3.hs:2:18-20
-_result :: t
-f :: Integer -> t
+_result :: a2
+f :: Integer -> a2
 x :: Integer
-xs :: [t1] = []
+xs :: [t] = []
 x :: Integer = 2
-f :: Integer -> t = _
-_result :: t = _
+f :: Integer -> a2 = _
+_result :: a2 = _
 _result = 3
 Logged breakpoint at ../Test3.hs:2:18-31
-_result :: [t]
-f :: Integer -> t
+_result :: [a2]
+f :: Integer -> a2
 x :: Integer
 xs :: [Integer]
 Logged breakpoint at ../Test3.hs:2:18-20
-_result :: t
+_result :: a2
diff --git a/testsuite/tests/ghci/scripts/Defer02.stderr b/testsuite/tests/ghci/scripts/Defer02.stderr
index ad39191d08..29feadd24b 100644
--- a/testsuite/tests/ghci/scripts/Defer02.stderr
+++ b/testsuite/tests/ghci/scripts/Defer02.stderr
@@ -12,7 +12,7 @@
     • In the expression: 'p'
       In an equation for ‘a’: a = 'p'
 
-../../typecheck/should_run/Defer01.hs:18:9: warning:
+../../typecheck/should_run/Defer01.hs:18:7: warning:
     • No instance for (Eq B) arising from a use of ‘==’
     • In the expression: x == x
       In an equation for ‘b’: b x = x == x
@@ -52,6 +52,7 @@
         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')
     • Relevant bindings include
         x :: a (bound at ../../typecheck/should_run/Defer01.hs:34:3)
         h :: a -> (Char, Char)
@@ -61,6 +62,7 @@
     • Couldn't match expected type ‘Bool’ with actual type ‘T a’
     • In the first argument of ‘not’, namely ‘(K a)’
       In the expression: (not (K a))
+      In the expression: seq (not (K a)) ()
     • Relevant bindings include
         a :: a (bound at ../../typecheck/should_run/Defer01.hs:39:3)
         i :: a -> () (bound at ../../typecheck/should_run/Defer01.hs:39:1)
@@ -110,6 +112,7 @@
     • Probable cause: ‘putChar’ is applied to too few arguments
       In the first argument of ‘(>>)’, namely ‘putChar’
       In the expression: putChar >> putChar 'p'
+      In an equation for ‘l’: l = putChar >> putChar 'p'
 *** Exception: ../../typecheck/should_run/Defer01.hs:11:40: error:
     • Couldn't match type ‘Char’ with ‘[Char]’
       Expected type: String
@@ -123,7 +126,7 @@
     • In the expression: 'p'
       In an equation for ‘a’: a = 'p'
 (deferred type error)
-*** Exception: ../../typecheck/should_run/Defer01.hs:18:9: error:
+*** Exception: ../../typecheck/should_run/Defer01.hs:18:7: error:
     • No instance for (Eq B) arising from a use of ‘==’
     • In the expression: x == x
       In an equation for ‘b’: b x = x == x
@@ -135,6 +138,7 @@
         Actual type: C Bool
     • In the first argument of ‘c’, namely ‘(C2 True)’
       In the first argument of ‘print’, namely ‘(c (C2 True))’
+      In the expression: print (c (C2 True))
 *** Exception: ../../typecheck/should_run/Defer01.hs:28:5: error:
     • No instance for (Num (a -> a)) arising from the literal ‘1’
         (maybe you haven't applied a function to enough arguments?)
@@ -158,6 +162,7 @@
         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')
     • Relevant bindings include
         x :: a (bound at ../../typecheck/should_run/Defer01.hs:34:3)
         h :: a -> (Char, Char)
@@ -167,6 +172,7 @@
     • Couldn't match expected type ‘Bool’ with actual type ‘T a’
     • In the first argument of ‘not’, namely ‘(K a)’
       In the expression: (not (K a))
+      In the expression: seq (not (K a)) ()
     • Relevant bindings include
         a :: a (bound at ../../typecheck/should_run/Defer01.hs:39:3)
         i :: a -> () (bound at ../../typecheck/should_run/Defer01.hs:39:1)
@@ -188,4 +194,5 @@
     • Probable cause: ‘putChar’ is applied to too few arguments
       In the first argument of ‘(>>)’, namely ‘putChar’
       In the expression: putChar >> putChar 'p'
+      In an equation for ‘l’: l = putChar >> putChar 'p'
 (deferred type error)
diff --git a/testsuite/tests/ghci/scripts/T10122.stdout b/testsuite/tests/ghci/scripts/T10122.stdout
index 84d8856c1b..8d6f0182dc 100644
--- a/testsuite/tests/ghci/scripts/T10122.stdout
+++ b/testsuite/tests/ghci/scripts/T10122.stdout
@@ -1,2 +1,2 @@
 T :: (k -> *) -> k -> *
-T :: forall k. (k -> *) -> k -> *
+T :: forall {k}. (k -> *) -> k -> *
diff --git a/testsuite/tests/ghci/scripts/T10508.stderr b/testsuite/tests/ghci/scripts/T10508.stderr
index 86ee279393..86cdc82e92 100644
--- a/testsuite/tests/ghci/scripts/T10508.stderr
+++ b/testsuite/tests/ghci/scripts/T10508.stderr
@@ -1,8 +1,12 @@
 
-<interactive>:1:15: error:
-    Couldn't match type ‘a0 -> a0’ with ‘[Char]’
-       Expected type: Prelude.String
-         Actual type: a0 -> a0
-    Probable cause: ‘id’ is applied to too few arguments
-    In the first argument of ‘return’, namely ‘id’
-    In the expression: return id
+<interactive>:1:8: error:
+    • Couldn't match type ‘a0 -> a0’ with ‘[Char]’
+      Expected type: IO Prelude.String
+        Actual type: IO (a0 -> a0)
+    • In the expression: return id
+      In the second argument of ‘(.)’, namely ‘\ _ -> return id’
+      In the expression:
+          (.)
+            (GHC.GHCi.ghciStepIO :: IO Prelude.String -> IO Prelude.String)
+            (\ _ -> return id) ::
+            Prelude.String -> IO Prelude.String
diff --git a/testsuite/tests/ghci/scripts/T7627.stdout b/testsuite/tests/ghci/scripts/T7627.stdout
index 81a360facb..4b16acc1a2 100644
--- a/testsuite/tests/ghci/scripts/T7627.stdout
+++ b/testsuite/tests/ghci/scripts/T7627.stdout
@@ -28,6 +28,12 @@ instance (Monoid a, Monoid b) => Monoid (a, b)
 data (#,#) (c :: TYPE a) (d :: TYPE b) = (#,#) c d
   	-- Defined in ‘GHC.Prim’
 (,) :: a -> b -> (a, b)
-(#,#) :: c -> d -> (# c, d #)
+(#,#)
+  :: forall (a :: GHC.Types.Levity) (b :: GHC.Types.Levity) (c :: TYPE
+                                                                    a) (d :: TYPE b).
+     c -> d -> (# c, d #)
 (  ,  ) :: a -> b -> (a, b)
-(#  ,  #) :: c -> d -> (# c, d #)
+(#  ,  #)
+  :: forall (a :: GHC.Types.Levity) (b :: GHC.Types.Levity) (c :: TYPE
+                                                                    a) (d :: TYPE b).
+     c -> d -> (# c, d #)
diff --git a/testsuite/tests/ghci/scripts/T8649.stderr b/testsuite/tests/ghci/scripts/T8649.stderr
index ae766e5aec..aa40d50c2e 100644
--- a/testsuite/tests/ghci/scripts/T8649.stderr
+++ b/testsuite/tests/ghci/scripts/T8649.stderr
@@ -6,3 +6,4 @@
         ‘Ghci1.X’ is defined at <interactive>:1:1-14
     In the first argument of ‘f’, namely ‘(Y 3)’
     In the expression: f (Y 3)
+    In an equation for ‘it’: it = f (Y 3)
diff --git a/testsuite/tests/ghci/scripts/T8959b.stderr b/testsuite/tests/ghci/scripts/T8959b.stderr
index 6a20f07421..d968f8ac56 100644
--- a/testsuite/tests/ghci/scripts/T8959b.stderr
+++ b/testsuite/tests/ghci/scripts/T8959b.stderr
@@ -1,16 +1,16 @@
 
-T8959b.hs:5:7:
-    Couldn't match expected type ‘Int → Int’ with actual type ‘()’
-    In the expression: ()
-    In an equation for ‘foo’: foo = ()
+T8959b.hs:5:7: error:
+    • Couldn't match expected type ‘Int → Int’ with actual type ‘()’
+    • In the expression: ()
+      In an equation for ‘foo’: foo = ()
 
-T8959b.hs:8:7:
-    Couldn't match expected type ‘()’ with actual type ‘t0 → m0 t0’
-    In the expression: proc x -> do { return ⤙ x }
-    In an equation for ‘bar’: bar = proc x -> do { return ⤙ x }
+T8959b.hs:8:7: error:
+    • Couldn't match expected type ‘()’ with actual type ‘t0 → m0 t0’
+    • In the expression: proc x -> do { return ⤙ x }
+      In an equation for ‘bar’: bar = proc x -> do { return ⤙ x }
 
-T8959b.hs:10:7:
-    Couldn't match expected type ‘(∀ a2. a2 → a2) → a1’
-                with actual type ‘()’
-    In the expression: () ∷ (∀ a. a -> a) -> a
-    In an equation for ‘baz’: baz = () ∷ (∀ a. a -> a) -> a
+T8959b.hs:10:7: error:
+    • Couldn't match expected type ‘(∀ a2. a2 → a2) → a1’
+                  with actual type ‘()’
+    • In the expression: () ∷ (∀ a. a -> a) -> a
+      In an equation for ‘baz’: baz = () ∷ (∀ a. a -> a) -> a
diff --git a/testsuite/tests/ghci/scripts/ghci013.stdout b/testsuite/tests/ghci/scripts/ghci013.stdout
index b7065c5169..d70c57fd67 100644
--- a/testsuite/tests/ghci/scripts/ghci013.stdout
+++ b/testsuite/tests/ghci/scripts/ghci013.stdout
@@ -1,2 +1,2 @@
 f :: (?callStack::GHC.Stack.Types.CallStack, Monad m) =>
-     (m a, r) -> m b
+     (m a, t) -> m b
diff --git a/testsuite/tests/ghci/scripts/ghci025.stdout b/testsuite/tests/ghci/scripts/ghci025.stdout
index 80c4d4b7a5..7cea3e97ef 100644
--- a/testsuite/tests/ghci/scripts/ghci025.stdout
+++ b/testsuite/tests/ghci/scripts/ghci025.stdout
@@ -96,24 +96,24 @@ c4 :: forall a b. C a b => forall a1. a1 -> b
 -- test :browse! <target> relative to different contexts
 :browse! Ghci025C -- from *Ghci025C>
 -- defined locally
-g :: forall a. Num a => a -> a
-h :: forall a. Integral a => a -> a
+g :: forall {a}. Num a => a -> a
+h :: forall {a}. Integral a => a -> a
 -- imported via Ghci025D
-f :: forall a. Num a => a -> a
+f :: forall {a}. Num a => a -> a
 :browse! Ghci025C -- from *Ghci025B>, after :add Ghci025B
 -- imported via Ghci025C
-g :: forall a. Num a => a -> a
-h :: forall a. Integral a => a -> a
-f :: forall a. Num a => a -> a
+g :: forall {a}. Num a => a -> a
+h :: forall {a}. Integral a => a -> a
+f :: forall {a}. Num a => a -> a
 :browse! Ghci025C -- from *Ghci025C>, after :m *Ghci025C
 -- defined locally
-g :: forall a. Num a => a -> a
-h :: forall a. Integral a => a -> a
+g :: forall {a}. Num a => a -> a
+h :: forall {a}. Integral a => a -> a
 -- imported via Ghci025D
-f :: forall a. Num a => a -> a
+f :: forall {a}. Num a => a -> a
 :browse! Ghci025C -- from *Ghci025D>, after :m *Ghci025D
 -- not currently imported
-Ghci025C.g :: forall a. Num a => a -> a
-Ghci025C.h :: forall a. Integral a => a -> a
+Ghci025C.g :: forall {a}. Num a => a -> a
+Ghci025C.h :: forall {a}. Integral a => a -> a
 -- defined locally
-f :: forall a. Num a => a -> a
+f :: forall {a}. Num a => a -> a
diff --git a/testsuite/tests/ghci/scripts/ghci047.stderr b/testsuite/tests/ghci/scripts/ghci047.stderr
index 7e696c02c4..badfc1ebb1 100644
--- a/testsuite/tests/ghci/scripts/ghci047.stderr
+++ b/testsuite/tests/ghci/scripts/ghci047.stderr
@@ -2,13 +2,11 @@
 <interactive>:38:1: error:
     • Couldn't match type ‘HFalse’ with ‘HTrue’
         arising from a use of ‘f’
-    • In the expression: f
-      In the expression: f $ Baz 'a'
+    • In the expression: f $ Baz 'a'
       In an equation for ‘it’: it = f $ Baz 'a'
 
 <interactive>:39:1: error:
     • Couldn't match type ‘HFalse’ with ‘HTrue’
         arising from a use of ‘f’
-    • In the expression: f
-      In the expression: f $ Quz
+    • In the expression: f $ Quz
       In an equation for ‘it’: it = f $ Quz
diff --git a/testsuite/tests/ghci/scripts/ghci050.stderr b/testsuite/tests/ghci/scripts/ghci050.stderr
index e8cc7971db..588d130172 100644
--- a/testsuite/tests/ghci/scripts/ghci050.stderr
+++ b/testsuite/tests/ghci/scripts/ghci050.stderr
@@ -1,14 +1,14 @@
 
 <interactive>:5:49: error:
-    Couldn't match expected type ‘ListableElem (a, a)’
-                with actual type ‘a’
-    ‘a’ is a rigid type variable bound by
+    • Couldn't match expected type ‘ListableElem (a, a)’
+                  with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
         the instance declaration at <interactive>:5:10
-    In the expression: a
-    In the expression: [a, b]
-    Relevant bindings include
-      b :: a (bound at <interactive>:5:43)
-      a :: a (bound at <interactive>:5:41)
-      asList :: (a, a) -> [ListableElem (a, a)]
-        (bound at <interactive>:5:33)
-
+    • In the expression: a
+      In the expression: [a, b]
+      In an equation for ‘asList’: asList (a, b) = [a, b]
+    • Relevant bindings include
+        b :: a (bound at <interactive>:5:43)
+        a :: a (bound at <interactive>:5:41)
+        asList :: (a, a) -> [ListableElem (a, a)]
+          (bound at <interactive>:5:33)
diff --git a/testsuite/tests/ghci/scripts/ghci052.stderr b/testsuite/tests/ghci/scripts/ghci052.stderr
index 4464891168..224726f822 100644
--- a/testsuite/tests/ghci/scripts/ghci052.stderr
+++ b/testsuite/tests/ghci/scripts/ghci052.stderr
@@ -6,6 +6,7 @@
         ‘Ghci1.Planet’ is defined at <interactive>:4:1-37
     In the first argument of ‘pn’, namely ‘Mercury’
     In the expression: pn Mercury
+    In an equation for ‘it’: it = pn Mercury
 
 <interactive>:9:4: error:
     Couldn't match expected type ‘Ghci1.Planet’
@@ -14,6 +15,7 @@
         ‘Ghci1.Planet’ is defined at <interactive>:4:1-37
     In the first argument of ‘pn’, namely ‘Venus’
     In the expression: pn Venus
+    In an equation for ‘it’: it = pn Venus
 
 <interactive>:10:4: error:
     Couldn't match expected type ‘Ghci1.Planet’
@@ -22,6 +24,7 @@
         ‘Ghci1.Planet’ is defined at <interactive>:4:1-37
     In the first argument of ‘pn’, namely ‘Mars’
     In the expression: pn Mars
+    In an equation for ‘it’: it = pn Mars
 
 <interactive>:12:44: error:
     Couldn't match expected type ‘Planet’
diff --git a/testsuite/tests/ghci/scripts/ghci053.stderr b/testsuite/tests/ghci/scripts/ghci053.stderr
index bb038faf23..76d5ae2548 100644
--- a/testsuite/tests/ghci/scripts/ghci053.stderr
+++ b/testsuite/tests/ghci/scripts/ghci053.stderr
@@ -6,6 +6,7 @@
         ‘Ghci1.Planet’ is defined at <interactive>:4:1-49
     In the second argument of ‘(==)’, namely ‘Mercury’
     In the expression: mercury == Mercury
+    In an equation for ‘it’: it = mercury == Mercury
 
 <interactive>:11:10: error:
     Couldn't match expected type ‘Planet’
@@ -14,3 +15,4 @@
         ‘Planet’ is defined at <interactive>:7:1-41
     In the second argument of ‘(==)’, namely ‘Earth’
     In the expression: Venus == Earth
+    In an equation for ‘it’: it = Venus == Earth
diff --git a/testsuite/tests/ghci/scripts/ghci055.stdout b/testsuite/tests/ghci/scripts/ghci055.stdout
index c7450d0def..e878582a2b 100644
--- a/testsuite/tests/ghci/scripts/ghci055.stdout
+++ b/testsuite/tests/ghci/scripts/ghci055.stdout
@@ -1,3 +1,3 @@
 x = _
-x :: ?callStack::GHC.Stack.Types.CallStack => r = _
+x :: ?callStack::GHC.Stack.Types.CallStack => a = _
 y :: Integer = 3
diff --git a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
index ce3f4f9048..37b1135c48 100644
--- a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
+++ b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
@@ -8,6 +8,7 @@ PushedInAsGivens.hs:10:31: error:
         at PushedInAsGivens.hs:9:13-44
     • In the expression: y
       In the first argument of ‘length’, namely ‘[x, y]’
+      In the expression: length [x, y]
     • Relevant bindings include
         x :: a1 (bound at PushedInAsGivens.hs:10:17)
         foo :: a1 -> Int (bound at PushedInAsGivens.hs:10:13)
diff --git a/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr b/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
index 7f806db271..5a0892ed31 100644
--- a/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
+++ b/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
@@ -11,6 +11,7 @@ GADTwrong1.hs:12:21: error:
         at GADTwrong1.hs:10:20
     • In the expression: y
       In a case alternative: T y -> y
+      In the expression: case T x :: T (Const b) of { T y -> y }
     • Relevant bindings include
         y :: c (bound at GADTwrong1.hs:12:16)
         coerce :: a -> b (bound at GADTwrong1.hs:11:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index e60cdab2a5..a296a36910 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,22 +1,24 @@
 
 T2544.hs:17:18: error:
-    Couldn't match type ‘IxMap i0’ with ‘IxMap l’
-    NB: ‘IxMap’ is a type function, and may not be injective
-    The type variable ‘i0’ is ambiguous
-    Expected type: IxMap l [Int]
-      Actual type: IxMap i0 [Int]
-    In the first argument of ‘BiApp’, namely ‘empty’
-    In the expression: BiApp empty empty
-    Relevant bindings include
-      empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
+    • Couldn't match type ‘IxMap i0’ with ‘IxMap l’
+      NB: ‘IxMap’ is a type function, and may not be injective
+      The type variable ‘i0’ is ambiguous
+      Expected type: IxMap l [Int]
+        Actual type: IxMap i0 [Int]
+    • In the first argument of ‘BiApp’, namely ‘empty’
+      In the expression: BiApp empty empty
+      In an equation for ‘empty’: empty = BiApp empty empty
+    • Relevant bindings include
+        empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
 
 T2544.hs:17:24: error:
-    Couldn't match type ‘IxMap i1’ with ‘IxMap r’
-    NB: ‘IxMap’ is a type function, and may not be injective
-    The type variable ‘i1’ is ambiguous
-    Expected type: IxMap r [Int]
-      Actual type: IxMap i1 [Int]
-    In the second argument of ‘BiApp’, namely ‘empty’
-    In the expression: BiApp empty empty
-    Relevant bindings include
-      empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
+    • Couldn't match type ‘IxMap i1’ with ‘IxMap r’
+      NB: ‘IxMap’ is a type function, and may not be injective
+      The type variable ‘i1’ is ambiguous
+      Expected type: IxMap r [Int]
+        Actual type: IxMap i1 [Int]
+    • In the second argument of ‘BiApp’, namely ‘empty’
+      In the expression: BiApp empty empty
+      In an equation for ‘empty’: empty = BiApp empty empty
+    • Relevant bindings include
+        empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
diff --git a/testsuite/tests/indexed-types/should_fail/T2693.stderr b/testsuite/tests/indexed-types/should_fail/T2693.stderr
index d3546c21ba..1d5ebefb9d 100644
--- a/testsuite/tests/indexed-types/should_fail/T2693.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2693.stderr
@@ -4,6 +4,7 @@ T2693.hs:12:15: error:
       The type variables ‘b1’, ‘a6’, ‘a8’ are ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the first argument of ‘(+)’, namely ‘fst x’
+      In the expression: fst x + fst x
     • Relevant bindings include n :: a8 (bound at T2693.hs:12:7)
 
 T2693.hs:12:23: error:
@@ -11,6 +12,7 @@ T2693.hs:12:23: error:
       The type variables ‘b2’, ‘a7’, ‘a8’ are ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the second argument of ‘(+)’, namely ‘fst x’
+      In the expression: fst x + fst x
     • Relevant bindings include n :: a8 (bound at T2693.hs:12:7)
 
 T2693.hs:19:15: error:
@@ -18,6 +20,7 @@ T2693.hs:19:15: error:
       The type variables ‘b0’, ‘a2’, ‘a5’ are ambiguous
     • In the first argument of ‘fst’, namely ‘x’
       In the first argument of ‘(+)’, namely ‘fst x’
+      In the expression: fst x + snd x
     • Relevant bindings include n :: a5 (bound at T2693.hs:19:7)
 
 T2693.hs:19:23: error:
@@ -25,6 +28,7 @@ T2693.hs:19:23: error:
       The type variables ‘a3’, ‘a4’, ‘a5’ are ambiguous
     • In the first argument of ‘snd’, namely ‘x’
       In the second argument of ‘(+)’, namely ‘snd x’
+      In the expression: fst x + snd x
     • Relevant bindings include n :: a5 (bound at T2693.hs:19:7)
 
 T2693.hs:29:20: error:
@@ -34,3 +38,7 @@ T2693.hs:29:20: error:
         Actual type: () -> Maybe (TFn a0)
     • In the first argument of ‘mapM’, namely ‘g’
       In a stmt of a 'do' block: pvs <- mapM g undefined
+      In the expression:
+        do { pvs <- mapM g undefined;
+             let n = (map pvrX pvs) `min` (map pvrX pvs);
+             undefined }
diff --git a/testsuite/tests/indexed-types/should_fail/T3330a.stderr b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
index f6a5deeeb7..c90ea43c9c 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
@@ -11,6 +11,7 @@ T3330a.hs:19:34: error:
         Actual type: s ix
     • In the first argument of ‘hmapM’, namely ‘p’
       In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
+      In the expression: execWriter (hmapM p collect x)
     • Relevant bindings include
         x :: PF s r ix (bound at T3330a.hs:19:12)
         p :: s ix (bound at T3330a.hs:19:10)
@@ -28,6 +29,7 @@ T3330a.hs:19:44: error:
         Actual type: PF s r ix
     • In the third argument of ‘hmapM’, namely ‘x’
       In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
+      In the expression: execWriter (hmapM p collect x)
     • Relevant bindings include
         x :: PF s r ix (bound at T3330a.hs:19:12)
         p :: s ix (bound at T3330a.hs:19:10)
diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
index 4d9e6d5be6..8526c17f5e 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
@@ -5,9 +5,10 @@ T3330c.hs:23:43: error:
         f1 :: * -> *
         Der f1 x :: *
       Expected type: Der ((->) x) (Der f1 x)
-      Actual type: R f1
+        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)
     • Relevant bindings include
         x :: x (bound at T3330c.hs:23:29)
         df :: Der f1 x (bound at T3330c.hs:23:25)
diff --git a/testsuite/tests/indexed-types/should_fail/T3440.stderr b/testsuite/tests/indexed-types/should_fail/T3440.stderr
index 7b29bb6f52..8289d144c2 100644
--- a/testsuite/tests/indexed-types/should_fail/T3440.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3440.stderr
@@ -17,6 +17,7 @@ T3440.hs:11:22: error:
         at T3440.hs:10:11
     • In the expression: x
       In the expression: (x, y)
+      In an equation for ‘unwrap’: unwrap (GADT x y) = (x, y)
     • Relevant bindings include
         y :: Fam a1 (bound at T3440.hs:11:16)
         x :: a1 (bound at T3440.hs:11:14)
diff --git a/testsuite/tests/indexed-types/should_fail/T4099.stderr b/testsuite/tests/indexed-types/should_fail/T4099.stderr
index c5b4245c17..a0ddc964ff 100644
--- a/testsuite/tests/indexed-types/should_fail/T4099.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4099.stderr
@@ -1,21 +1,23 @@
 
-T4099.hs:11:30:
-    Couldn't match expected type ‘T a0’ with actual type ‘T b’
-    NB: ‘T’ is a type function, and may not be injective
-    The type variable ‘a0’ is ambiguous
-    In the second argument of ‘foo’, namely ‘x’
-    In the expression: foo (error "urk") x
-    Relevant bindings include
-      x :: T b (bound at T4099.hs:11:8)
-      a :: b (bound at T4099.hs:11:6)
-      bar1 :: b -> T b -> Int (bound at T4099.hs:11:1)
+T4099.hs:11:30: error:
+    • Couldn't match expected type ‘T a0’ with actual type ‘T b’
+      NB: ‘T’ is a type function, and may not be injective
+      The type variable ‘a0’ is ambiguous
+    • In the second argument of ‘foo’, namely ‘x’
+      In the expression: foo (error "urk") x
+      In an equation for ‘bar1’: bar1 a x = foo (error "urk") x
+    • Relevant bindings include
+        x :: T b (bound at T4099.hs:11:8)
+        a :: b (bound at T4099.hs:11:6)
+        bar1 :: b -> T b -> Int (bound at T4099.hs:11:1)
 
-T4099.hs:14:30:
-    Couldn't match expected type ‘T a1’ with actual type ‘Maybe b’
-    The type variable ‘a1’ is ambiguous
-    In the second argument of ‘foo’, namely ‘x’
-    In the expression: foo (error "urk") x
-    Relevant bindings include
-      x :: Maybe b (bound at T4099.hs:14:8)
-      a :: b (bound at T4099.hs:14:6)
-      bar2 :: b -> Maybe b -> Int (bound at T4099.hs:14:1)
+T4099.hs:14:30: error:
+    • Couldn't match expected type ‘T a1’ with actual type ‘Maybe b’
+      The type variable ‘a1’ is ambiguous
+    • In the second argument of ‘foo’, namely ‘x’
+      In the expression: foo (error "urk") x
+      In an equation for ‘bar2’: bar2 a x = foo (error "urk") x
+    • Relevant bindings include
+        x :: Maybe b (bound at T4099.hs:14:8)
+        a :: b (bound at T4099.hs:14:6)
+        bar2 :: b -> Maybe b -> Int (bound at T4099.hs:14:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index 4173eff8da..1a2a18bebf 100644
--- a/testsuite/tests/indexed-types/should_fail/T4179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -1,15 +1,16 @@
 
 T4179.hs:26:16: error:
-    • Couldn't match type ‘A3 (x (A2 (FCon x) -> A3 (FCon x)))’
-                     with ‘A3 (FCon x)’
-      NB: ‘A3’ is a type function, and may not be injective
+    • Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
+                     with ‘A2 (FCon x)’
+      NB: ‘A2’ is a type function, and may not be injective
       Expected type: x (A2 (FCon x) -> A3 (FCon x))
                      -> A2 (FCon x) -> A3 (FCon x)
-      Actual type: x (A2 (FCon x) -> A3 (FCon x))
-                   -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-                   -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
+        Actual type: x (A2 (FCon x) -> A3 (FCon x))
+                     -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                     -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
     • In the first argument of ‘foldDoC’, namely ‘op’
       In the expression: foldDoC op
+      In an equation for ‘fCon’: fCon = foldDoC op
     • Relevant bindings include
         fCon :: Con x -> A2 (FCon x) -> A3 (FCon x)
           (bound at T4179.hs:26:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T4485.stderr b/testsuite/tests/indexed-types/should_fail/T4485.stderr
index 92d8efc3cd..4cf3b153fd 100644
--- a/testsuite/tests/indexed-types/should_fail/T4485.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4485.stderr
@@ -1,30 +1,31 @@
 
 T4485.hs:50:15: error:
-    Overlapping instances for EmbedAsChild
-                                (IdentityT IO) (XMLGenT m0 (XML m0))
-      arising from a use of ‘asChild’
-    Matching instances:
-      instance [overlapping] (EmbedAsChild m c, m1 ~ m) =>
-                             EmbedAsChild m (XMLGenT m1 c)
-        -- Defined at T4485.hs:28:30
-      instance [overlapping] EmbedAsChild
-                               (IdentityT IO) (XMLGenT Identity ())
-        -- Defined at T4485.hs:45:30
-    (The choice depends on the instantiation of ‘m0’
-     To pick the first instance above, use IncoherentInstances
-     when compiling the other instance declarations)
-    In the expression: asChild
-    In the expression: asChild $ (genElement "foo")
-    In an equation for ‘asChild’:
-        asChild b = asChild $ (genElement "foo")
+    • Overlapping instances for EmbedAsChild
+                                  (IdentityT IO) (XMLGenT m0 (XML m0))
+        arising from a use of ‘asChild’
+      Matching instances:
+        instance [overlapping] (EmbedAsChild m c, m1 ~ m) =>
+                               EmbedAsChild m (XMLGenT m1 c)
+          -- Defined at T4485.hs:28:30
+        instance [overlapping] EmbedAsChild
+                                 (IdentityT IO) (XMLGenT Identity ())
+          -- Defined at T4485.hs:45:30
+      (The choice depends on the instantiation of ‘m0’
+       To pick the first instance above, use IncoherentInstances
+       when compiling the other instance declarations)
+    • In the expression: asChild $ (genElement "foo")
+      In an equation for ‘asChild’:
+          asChild b = asChild $ (genElement "foo")
+      In the instance declaration for
+        ‘EmbedAsChild (IdentityT IO) FooBar’
 
 T4485.hs:50:26: error:
-    Ambiguous type variable ‘m0’ arising from a use of ‘genElement’
-    prevents the constraint ‘(XMLGen m0)’ from being solved.
-    Probable fix: use a type annotation to specify what ‘m0’ should be.
-    These potential instance exist:
-      instance XMLGen (IdentityT m) -- Defined at T4485.hs:37:10
-    In the second argument of ‘($)’, namely ‘(genElement "foo")’
-    In the expression: asChild $ (genElement "foo")
-    In an equation for ‘asChild’:
-        asChild b = asChild $ (genElement "foo")
+    • Ambiguous type variable ‘m0’ arising from a use of ‘genElement’
+      prevents the constraint ‘(XMLGen m0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘m0’ should be.
+      These potential instance exist:
+        instance XMLGen (IdentityT m) -- Defined at T4485.hs:37:10
+    • In the second argument of ‘($)’, namely ‘(genElement "foo")’
+      In the expression: asChild $ (genElement "foo")
+      In an equation for ‘asChild’:
+          asChild b = asChild $ (genElement "foo")
diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr
index 193b1536ec..f1ae705f5e 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -6,6 +6,8 @@ T5439.hs:82:28: error:
         Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
     • In the first argument of ‘complete’, namely ‘ev’
       In the expression: complete ev
+      In a stmt of a 'do' block:
+        c <- complete ev $ inj $ Failure (e :: SomeException)
     • Relevant bindings include
         register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
           (bound at T5439.hs:64:9)
@@ -23,3 +25,5 @@ T5439.hs:82:39: error:
         ‘Failure (e :: SomeException)’
       In the second argument of ‘($)’, namely
         ‘inj $ Failure (e :: SomeException)’
+      In a stmt of a 'do' block:
+        c <- complete ev $ inj $ Failure (e :: SomeException)
diff --git a/testsuite/tests/indexed-types/should_fail/T7010.stderr b/testsuite/tests/indexed-types/should_fail/T7010.stderr
index 9441b3857e..0da40f7a69 100644
--- a/testsuite/tests/indexed-types/should_fail/T7010.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7010.stderr
@@ -1,7 +1,8 @@
 
-T7010.hs:53:27:
-    Couldn't match type ‘IO Float’ with ‘Serial (IO Float)’
-    Expected type: (Float, ValueTuple Vector)
-      Actual type: (Float, ValueTuple Float)
-    In the first argument of ‘withArgs’, namely ‘plug’
-    In the expression: withArgs plug
+T7010.hs:53:27: error:
+    • Couldn't match type ‘IO Float’ with ‘Serial (IO Float)’
+      Expected type: (Float, ValueTuple Vector)
+        Actual type: (Float, ValueTuple Float)
+    • In the first argument of ‘withArgs’, namely ‘plug’
+      In the expression: withArgs plug
+      In an equation for ‘filterFormants’: filterFormants = withArgs plug
diff --git a/testsuite/tests/indexed-types/should_fail/T7194.stderr b/testsuite/tests/indexed-types/should_fail/T7194.stderr
index d8655f0146..c48a3de15d 100644
--- a/testsuite/tests/indexed-types/should_fail/T7194.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7194.stderr
@@ -8,6 +8,7 @@ T7194.hs:18:35: error:
         at T7194.hs:17:18-41
     • In the expression: foo y
       In the first argument of ‘length’, namely ‘[x, foo y]’
+      In the expression: length [x, foo y]
     • Relevant bindings include
         y :: a (bound at T7194.hs:18:20)
         g :: a -> Int (bound at T7194.hs:18:18)
diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr
index f115604b10..b56db1398f 100644
--- a/testsuite/tests/indexed-types/should_fail/T7354.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr
@@ -1,10 +1,11 @@
 
-T7354.hs:28:11:
-    Occurs check: cannot construct the infinite type:
-      a ~ Base t (Prim [a] a)
-    Expected type: Prim [a] a -> Base t (Prim [a] a)
-      Actual type: Prim [a] a -> a
-    In the first argument of ‘ana’, namely ‘alg’
-    In the expression: ana alg
-    Relevant bindings include
-      foo :: Prim [a] a -> t (bound at T7354.hs:28:1)
+T7354.hs:28:11: error:
+    • Occurs check: cannot construct the infinite type:
+        t1 ~ Base t (Prim [t1] t1)
+      Expected type: Prim [t1] t1 -> Base t (Prim [t1] t1)
+        Actual type: Prim [t1] t1 -> t1
+    • In the first argument of ‘ana’, namely ‘alg’
+      In the expression: ana alg
+      In an equation for ‘foo’: foo = ana alg
+    • Relevant bindings include
+        foo :: Prim [t1] t1 -> t (bound at T7354.hs:28:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T7354a.stderr b/testsuite/tests/indexed-types/should_fail/T7354a.stderr
index ed38da6ed2..a5ec40630e 100644
--- a/testsuite/tests/indexed-types/should_fail/T7354a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7354a.stderr
@@ -1,6 +1,7 @@
 
-T7354a.hs:5:13:
-    Couldn't match expected type ‘Base t t’ with actual type ‘()’
-    In the first argument of ‘embed’, namely ‘()’
-    In the expression: embed ()
-    Relevant bindings include foo :: t (bound at T7354a.hs:5:1)
+T7354a.hs:5:13: error:
+    • Couldn't match expected type ‘Base t t’ with actual type ‘()’
+    • In the first argument of ‘embed’, namely ‘()’
+      In the expression: embed ()
+      In an equation for ‘foo’: foo = embed ()
+    • Relevant bindings include foo :: t (bound at T7354a.hs:5:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T7729.stderr b/testsuite/tests/indexed-types/should_fail/T7729.stderr
index 6686f39ca0..e892eea3c0 100644
--- a/testsuite/tests/indexed-types/should_fail/T7729.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7729.stderr
@@ -1,11 +1,12 @@
 
 T7729.hs:36:14: error:
-    Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
-    The type variable ‘t0’ is ambiguous
-    Expected type: t0 (BasePrimMonad m) a -> Rand m a
-      Actual type: BasePrimMonad (Rand m) a -> Rand m a
-    In the first argument of ‘(.)’, namely ‘liftPrim’
-    In the expression: liftPrim . lift
-    Relevant bindings include
-      liftPrim :: BasePrimMonad (Rand m) a -> Rand m a
-        (bound at T7729.hs:36:3)
+    • Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
+      The type variable ‘t0’ is ambiguous
+      Expected type: t0 (BasePrimMonad m) a -> Rand m a
+        Actual type: BasePrimMonad (Rand m) a -> Rand m a
+    • In the first argument of ‘(.)’, namely ‘liftPrim’
+      In the expression: liftPrim . lift
+      In an equation for ‘liftPrim’: liftPrim = liftPrim . lift
+    • Relevant bindings include
+        liftPrim :: BasePrimMonad (Rand m) a -> Rand m a
+          (bound at T7729.hs:36:3)
diff --git a/testsuite/tests/indexed-types/should_fail/T7729a.stderr b/testsuite/tests/indexed-types/should_fail/T7729a.stderr
index ca5f29f2c7..513a132191 100644
--- a/testsuite/tests/indexed-types/should_fail/T7729a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7729a.stderr
@@ -1,12 +1,13 @@
 
-T7729a.hs:36:26:
-    Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
-    The type variable ‘t0’ is ambiguous
-    Expected type: BasePrimMonad (Rand m) a
-      Actual type: t0 (BasePrimMonad m) a
-    In the first argument of ‘liftPrim’, namely ‘(lift x)’
-    In the expression: liftPrim (lift x)
-    Relevant bindings include
-      x :: BasePrimMonad (Rand m) a (bound at T7729a.hs:36:12)
-      liftPrim :: BasePrimMonad (Rand m) a -> Rand m a
-        (bound at T7729a.hs:36:3)
+T7729a.hs:36:26: error:
+    • Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
+      The type variable ‘t0’ is ambiguous
+      Expected type: BasePrimMonad (Rand m) a
+        Actual type: t0 (BasePrimMonad m) a
+    • In the first argument of ‘liftPrim’, namely ‘(lift x)’
+      In the expression: liftPrim (lift x)
+      In an equation for ‘liftPrim’: liftPrim x = liftPrim (lift x)
+    • Relevant bindings include
+        x :: BasePrimMonad (Rand m) a (bound at T7729a.hs:36:12)
+        liftPrim :: BasePrimMonad (Rand m) a -> Rand m a
+          (bound at T7729a.hs:36:3)
diff --git a/testsuite/tests/indexed-types/should_fail/T7788.stderr b/testsuite/tests/indexed-types/should_fail/T7788.stderr
index 757c05089e..fa4f3ed260 100644
--- a/testsuite/tests/indexed-types/should_fail/T7788.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7788.stderr
@@ -1,10 +1,11 @@
 
 T7788.hs:19:20: error:
-    Reduction stack overflow; size = 201
-    When simplifying the following type: F (Id (Fix Id))
-    Use -freduction-depth=0 to disable this check
-    (any upper bound you could choose might fail unpredictably with
-     minor updates to GHC, so disabling the check is recommended if
-     you're sure that type checking should terminate)
-    In the first argument of ‘foo’, namely ‘Proxy’
-    In the second argument of ‘($)’, namely ‘foo Proxy’
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: F (Id (Fix Id))
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the first argument of ‘foo’, namely ‘Proxy’
+      In the second argument of ‘($)’, namely ‘foo Proxy’
+      In the expression: print $ foo Proxy
diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr
index 8ac3d94a55..6dec5d0191 100644
--- a/testsuite/tests/indexed-types/should_fail/T8227.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr
@@ -5,6 +5,8 @@ T8227.hs:16:44: error:
       NB: ‘Scalar’ is a type function, and may not be injective
     • In the first argument of ‘arcLengthToParam’, namely ‘eps’
       In the expression: arcLengthToParam eps eps
+      In an equation for ‘absoluteToParam’:
+          absoluteToParam eps seg = arcLengthToParam eps eps
     • Relevant bindings include
         seg :: a (bound at T8227.hs:16:21)
         eps :: Scalar (V a) (bound at T8227.hs:16:17)
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index 8a267d7bd0..0df2b3cf83 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -1,28 +1,32 @@
 
-T8518.hs:14:18:
-    Couldn't match expected type ‘Maybe (F c)’ with actual type ‘F c’
-    In the expression: rpt (4 :: Int) c z b
-    In an equation for ‘callCont’:
-        callCont c z b
-          = rpt (4 :: Int) c z b
-          where
-              rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
-              rpt i c' z' b' = let ... in rpt (i - 1) c''
-    Relevant bindings include
-      b :: B c (bound at T8518.hs:14:14)
-      z :: Z c (bound at T8518.hs:14:12)
-      c :: c (bound at T8518.hs:14:10)
-      callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
+T8518.hs:14:18: error:
+    • Couldn't match expected type ‘Maybe (F c)’ with actual type ‘F c’
+    • In the expression: rpt (4 :: Int) c z b
+      In an equation for ‘callCont’:
+          callCont c z b
+            = rpt (4 :: Int) c z b
+            where
+                rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
+                rpt i c' z' b' = let ... in rpt (i - 1) c''
+    • Relevant bindings include
+        b :: B c (bound at T8518.hs:14:14)
+        z :: Z c (bound at T8518.hs:14:12)
+        c :: c (bound at T8518.hs:14:10)
+        callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
 
-T8518.hs:17:78:
-    Couldn't match expected type ‘F a1’
-                with actual type ‘Z a1 -> B a1 -> F a1’
-    In the expression: rpt (i - 1) c''
-    In the expression:
-      let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i - 1) c''
-    Relevant bindings include
-      c'' :: a1 (bound at T8518.hs:17:30)
-      b' :: B a1 (bound at T8518.hs:17:21)
-      z' :: Z a1 (bound at T8518.hs:17:18)
-      c' :: a1 (bound at T8518.hs:17:15)
-      rpt :: a -> a1 -> Z a1 -> B a1 -> F a1 (bound at T8518.hs:16:9)
+T8518.hs:17:78: error:
+    • Couldn't match expected type ‘F a’
+                  with actual type ‘Z a -> B a -> F a’
+    • In the expression: rpt (i - 1) c''
+      In the expression:
+        let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i - 1) c''
+      In an equation for ‘rpt’:
+          rpt i c' z' b'
+            = let c'' = fromJust (snd <$> (continue c' z' b'))
+              in rpt (i - 1) c''
+    • Relevant bindings include
+        c'' :: a (bound at T8518.hs:17:30)
+        b' :: B a (bound at T8518.hs:17:21)
+        z' :: Z a (bound at T8518.hs:17:18)
+        c' :: a (bound at T8518.hs:17:15)
+        rpt :: a1 -> a -> Z a -> B a -> F a (bound at T8518.hs:16:9)
diff --git a/testsuite/tests/indexed-types/should_fail/T9554.stderr b/testsuite/tests/indexed-types/should_fail/T9554.stderr
index 0baf5d78ff..b62badda9d 100644
--- a/testsuite/tests/indexed-types/should_fail/T9554.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9554.stderr
@@ -1,22 +1,24 @@
 
-T9554.hs:11:9:
-    Reduction stack overflow; size = 201
-    When simplifying the following type:
-      F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-    Use -freduction-depth=0 to disable this check
-    (any upper bound you could choose might fail unpredictably with
-     minor updates to GHC, so disabling the check is recommended if
-     you're sure that type checking should terminate)
-    In the expression: x
-    In an equation for ‘foo’: foo x = x
+T9554.hs:11:9: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type:
+        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: x
+      In an equation for ‘foo’: foo x = x
 
-T9554.hs:13:17:
-    Reduction stack overflow; size = 201
-    When simplifying the following type:
-      F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-    Use -freduction-depth=0 to disable this check
-    (any upper bound you could choose might fail unpredictably with
-     minor updates to GHC, so disabling the check is recommended if
-     you're sure that type checking should terminate)
-    In the first argument of ‘foo’, namely ‘Proxy’
-    In the expression: foo Proxy
+T9554.hs:13:17: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type:
+        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the first argument of ‘foo’, namely ‘Proxy’
+      In the expression: foo Proxy
+      In the expression:
+        case foo Proxy of { Proxy -> putStrLn "Made it!" }
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 36b0716a9a..efa3a73bf5 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -6,7 +6,7 @@ T9662.hs:47:8: error:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
         at T9662.hs:44:9
-      Expected type: Exp (((sh :. k) :. m) :. n)
+      Expected type: Exp (((sh :. m) :. n) :. k)
                      -> Exp (((sh :. m) :. n) :. k)
         Actual type: Exp
                        (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
@@ -22,6 +22,13 @@ T9662.hs:47:8: error:
              (atom :. atom :. atom :. atom)
              (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))
           id
+      In an equation for ‘test’:
+          test
+            = backpermute
+                (modify
+                   (atom :. atom :. atom :. atom)
+                   (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))
+                id
     • Relevant bindings include
         test :: Shape (((sh :. k) :. m) :. n)
                 -> Shape (((sh :. m) :. n) :. k)
diff --git a/testsuite/tests/module/mod121.stderr b/testsuite/tests/module/mod121.stderr
index aa0a8cd4af..fda1dec212 100644
--- a/testsuite/tests/module/mod121.stderr
+++ b/testsuite/tests/module/mod121.stderr
@@ -1,4 +1,4 @@
-
-mod121.hs:5:5: error:
-    Variable not in scope: m2 :: Int -> t
-    Perhaps you meant ‘m1’ (imported from Mod121_A)
+
+mod121.hs:5:5: error:
+    • Variable not in scope: m2 :: Int -> t
+    • Perhaps you meant ‘m1’ (imported from Mod121_A)
diff --git a/testsuite/tests/module/mod147.stderr b/testsuite/tests/module/mod147.stderr
index 335dbd2211..39bf7d2dc7 100644
--- a/testsuite/tests/module/mod147.stderr
+++ b/testsuite/tests/module/mod147.stderr
@@ -1,3 +1,3 @@
-
-mod147.hs:6:5: error:
-    Data constructor not in scope: D :: Integer -> t
+
+mod147.hs:6:5: error:
+    Data constructor not in scope: D :: Integer -> t
diff --git a/testsuite/tests/module/mod160.stderr b/testsuite/tests/module/mod160.stderr
index a4b8669de8..d853c67e6b 100644
--- a/testsuite/tests/module/mod160.stderr
+++ b/testsuite/tests/module/mod160.stderr
@@ -1,6 +1,6 @@
-
-mod160.hs:12:5: error:
-    Variable not in scope: m3 :: Char -> t
-    Perhaps you meant one of these:
-      ‘m1’ (imported from Mod159_D), ‘m2’ (imported from Mod159_D)
-exit(1)
+
+mod160.hs:12:5: error:
+    • Variable not in scope: m3 :: Char -> t
+    • Perhaps you meant one of these:
+        ‘m1’ (imported from Mod159_D), ‘m2’ (imported from Mod159_D)
+exit(1)
diff --git a/testsuite/tests/module/mod69.stderr b/testsuite/tests/module/mod69.stderr
index d7f92be69a..db7487485e 100644
--- a/testsuite/tests/module/mod69.stderr
+++ b/testsuite/tests/module/mod69.stderr
@@ -1,2 +1,4 @@
 
-mod69.hs:3:7: Pattern syntax in expression context: x@1
+mod69.hs:3:7: error:
+    Pattern syntax in expression context: x@1
+    Did you mean to enable TypeApplications?
diff --git a/testsuite/tests/module/mod70.stderr b/testsuite/tests/module/mod70.stderr
index 110ff24afe..f0e3042d3d 100644
--- a/testsuite/tests/module/mod70.stderr
+++ b/testsuite/tests/module/mod70.stderr
@@ -1,2 +1,4 @@
 
-mod70.hs:3:8: Pattern syntax in expression context: ~1
+mod70.hs:3:8: error:
+    Pattern syntax in expression context: ~1
+    Did you mean to enable TypeApplications?
diff --git a/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr b/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr
index 87de242e4b..73a1b9b4d8 100644
--- a/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr
+++ b/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr
@@ -1,6 +1,7 @@
 
-overloadedrecfldsfail07.hs:7:7:
-    Couldn't match expected type ‘T’ with actual type ‘T -> Int’
-    Probable cause: ‘x’ is applied to too few arguments
-    In the first argument of ‘x’, namely ‘x’
-    In the expression: x x
+overloadedrecfldsfail07.hs:7:7: error:
+    • Couldn't match expected type ‘T’ with actual type ‘T -> Int’
+    • Probable cause: ‘x’ is applied to too few arguments
+      In the first argument of ‘x’, namely ‘x’
+      In the expression: x x
+      In an equation for ‘y’: y = x x
diff --git a/testsuite/tests/parser/should_compile/T2245.stderr b/testsuite/tests/parser/should_compile/T2245.stderr
index 1f5f87f7c7..783b751b34 100644
--- a/testsuite/tests/parser/should_compile/T2245.stderr
+++ b/testsuite/tests/parser/should_compile/T2245.stderr
@@ -13,10 +13,10 @@ T2245.hs:5:10: warning:
 
 T2245.hs:7:29: warning:
     • Defaulting the following constraints to type ‘T’
-        (Fractional b0)
+        (Fractional a0)
           arising from the literal ‘1e400’ at T2245.hs:7:29-33
-        (Ord b0) arising from a use of ‘<’ at T2245.hs:7:27
-        (Read b0) arising from a use of ‘read’ at T2245.hs:7:38-41
+        (Ord a0) arising from an operator section at T2245.hs:7:27-33
+        (Read a0) arising from a use of ‘read’ at T2245.hs:7:38-41
     • In the second argument of ‘(<)’, namely ‘1e400’
       In the first argument of ‘(.)’, namely ‘(< 1e400)’
       In the second argument of ‘(.)’, namely ‘(< 1e400) . read’
diff --git a/testsuite/tests/parser/should_compile/VtaParse.hs b/testsuite/tests/parser/should_compile/VtaParse.hs
new file mode 100644
index 0000000000..b1cfd7d4d0
--- /dev/null
+++ b/testsuite/tests/parser/should_compile/VtaParse.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE TypeApplications, RankNTypes, DataKinds, PolyKinds #-}
+
+module VtaParse where
+
+import Data.Proxy
+
+data Foo = Foo { first :: Int, second :: Bool} deriving Show
+
+f :: a -> b -> (a,b)
+f u v = (u, v)
+
+g :: Int -> Int -> (Int, Int)
+g u v = f @(Int) @Int u v
+
+dblTuple :: (a, b) -> ((a, b), b)
+dblTuple e@(_,y) = (e, y)
+
+
+-- interesting note:
+-- listpair :: forall a. [a] -> ([a], [a])
+-- therefore when explicitly applying, you do NOT put the type in "[ ]"
+
+listpair :: [a] -> ([a], [a])
+listpair [] = ([], [])
+listpair b@(_:_) = (b, b)
+
+-- suggested two cases by R. Eisenberg
+newtype N = MkN { unMkN :: forall a. Show a => a -> String }
+n = MkN show
+foo :: Bool -> String
+foo = unMkN n @Bool   -- Fails without parens! Not anymore!
+
+(&&) :: Bool -> Bool -> Bool
+(b@True) && True = True
+_ && _ = False
+
+(*@&) :: a -> a -> (a, a)
+x *@& y = (x, y)
+
+(@&) :: a -> a -> (a, a)
+x @& y = (x, y)
+
+main :: IO ()
+main = do
+         print $ g 5 12
+         print $ ((id @String (concat ["hello ", "world ", []])):"Hamidhasan":[])
+         print $ dblTuple @(Foo) @String ((Foo 5 True), "hello")
+         print $ listpair @(Maybe Int) [Just 12, Nothing]
+         print $ listpair @(Maybe Bool) $ (Just True) : (Just False) : (Nothing @Bool) : []
+         print $ dblTuple @Foo @[Maybe Int] ((Foo 7 False), ([Just 5, Nothing]))
+         print $ 12 @& 5
+
+pro :: Proxy a -> ()
+pro _ = ()
+
+x = pro @'True
+
+(@@) :: Int -> Int -> Int
+(@@) = (+)
+
+five = 3 @@ 2
+
+silly = pro {- hi! -}@Int
diff --git a/testsuite/tests/parser/should_compile/all.T b/testsuite/tests/parser/should_compile/all.T
index 0030040aed..9446bf1cfa 100644
--- a/testsuite/tests/parser/should_compile/all.T
+++ b/testsuite/tests/parser/should_compile/all.T
@@ -101,5 +101,6 @@ test('T5682', normal, compile, [''])
 test('T9723a', normal, compile, [''])
 test('T9723b', normal, compile, [''])
 test('T10188', normal, compile, [''])
+test('VtaParse', normal, compile, [''])
 test('T10196', normal, compile, [''])
 test('T10582', expect_broken(10582), compile, [''])
diff --git a/testsuite/tests/parser/should_compile/read014.stderr b/testsuite/tests/parser/should_compile/read014.stderr
index 5302b3476e..ebc07af88e 100644
--- a/testsuite/tests/parser/should_compile/read014.stderr
+++ b/testsuite/tests/parser/should_compile/read014.stderr
@@ -1,13 +1,13 @@
 
-read014.hs:4:1: Warning:
+read014.hs:4:1: warning:
     Top-level binding with no type signature:
       ng1 :: forall r a. Num a => r -> a -> a
 
-read014.hs:4:5: Warning: Defined but not used: ‘x’
+read014.hs:4:5: warning: Defined but not used: ‘x’
 
-read014.hs:6:10: Warning:
+read014.hs:6:10: warning:
     No explicit implementation for
       ‘+’, ‘*’, ‘abs’, ‘signum’, and ‘fromInteger’
     In the instance declaration for ‘Num (a, b)’
 
-read014.hs:8:53: Warning: Defined but not used: ‘x’
+read014.hs:8:53: warning: Defined but not used: ‘x’
diff --git a/testsuite/tests/parser/should_fail/readFail003.stderr b/testsuite/tests/parser/should_fail/readFail003.stderr
index 8b9b4d0295..e837eeedd1 100644
--- a/testsuite/tests/parser/should_fail/readFail003.stderr
+++ b/testsuite/tests/parser/should_fail/readFail003.stderr
@@ -1,7 +1,7 @@
 
 readFail003.hs:4:27: error:
     • Occurs check: cannot construct the infinite type:
-        r ~ (r, [a], [a1])
+        t ~ (t, [a], [a1])
     • In the expression: a
       In a pattern binding:
         ~(a, b, c)
@@ -11,6 +11,6 @@ readFail003.hs:4:27: error:
           where
               nullity = null
     • Relevant bindings include
-        a :: r (bound at readFail003.hs:4:3)
+        a :: t (bound at readFail003.hs:4:3)
         b :: [a] (bound at readFail003.hs:4:5)
         c :: [a1] (bound at readFail003.hs:4:7)
diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index 5337cc3d12..9cda918ae8 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -59,7 +59,7 @@ T10403.hs:28:8: warning:
           app2 :: H (B t)
         at T10403.hs:27:1-15
       Expected type: H (B t)
-      Actual type: H f0
+        Actual type: H f0
     • In the expression: h2 (H . I) (B ())
       In an equation for ‘app2’: app2 = h2 (H . I) (B ())
     • Relevant bindings include
@@ -73,8 +73,9 @@ T10403.hs:28:20: warning:
           app2 :: H (B t)
         at T10403.hs:27:1-15
       Expected type: f0 ()
-      Actual type: B t ()
+        Actual type: B t ()
     • In the second argument of ‘h2’, namely ‘(B ())’
       In the expression: h2 (H . I) (B ())
+      In an equation for ‘app2’: app2 = h2 (H . I) (B ())
     • Relevant bindings include
         app2 :: H (B t) (bound at T10403.hs:28:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T10438.stderr b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
index 5624d8dc9e..f26bfe7a8d 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10438.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
@@ -25,4 +25,4 @@ T10438.hs:7:22: warning:
         r :: r2 (bound at T10438.hs:6:11)
         g :: r2 -> r2 (bound at T10438.hs:6:9)
         f :: r (bound at T10438.hs:5:5)
-        foo :: r -> r1 -> r1 (bound at T10438.hs:5:1)
+        foo :: r -> forall r1. r1 -> r1 (bound at T10438.hs:5:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr
index f08e1807c0..9f04fc2cf2 100644
--- a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInExpressionSignature.stderr
@@ -1,4 +1,4 @@
-
-ExtraConstraintsWildcardInExpressionSignature.hs:3:20: error:
-    Extra-contraint wildcard ‘_’ not allowed
-      in an expression type signature
+
+ExtraConstraintsWildcardInExpressionSignature.hs:3:20: error:
+    Extra-constraint wildcard ‘_’ not allowed
+      in an expression type signature
diff --git a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSignature.stderr b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSignature.stderr
index 0e2a66a877..9711e34121 100644
--- a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSignature.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardInPatternSignature.stderr
@@ -1,4 +1,4 @@
-
-ExtraConstraintsWildcardInPatternSignature.hs:4:11: error:
-    Extra-contraint wildcard ‘_’ not allowed
-      in a pattern type-signature
+
+ExtraConstraintsWildcardInPatternSignature.hs:4:11: error:
+    Extra-constraint wildcard ‘_’ not allowed
+      in a pattern type-signature
diff --git a/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr b/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
index 266232cab0..26c895ef3c 100644
--- a/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
@@ -1,5 +1,5 @@
 
-Forall1Bad.hs:9:13:
-    Couldn't match expected type ‘Char’ with actual type ‘Bool’
-    In the first argument of ‘fall’, namely ‘True’
-    In the expression: fall True
+Forall1Bad.hs:9:8: error:
+    • Couldn't match expected type ‘Char’ with actual type ‘Bool’
+    • In the expression: fall True
+      In an equation for ‘test’: test = fall True
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
index bfe68d8718..83a9019401 100644
--- a/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
@@ -29,12 +29,13 @@ NamedWildcardExplicitForall.hs:13:26: error:
         baz :: _a -> Bool -> (_a, Bool)
           (bound at NamedWildcardExplicitForall.hs:14:1)
 
-NamedWildcardExplicitForall.hs:14:12: error:
-    • Couldn't match expected type ‘_a’ with actual type ‘Bool’
+NamedWildcardExplicitForall.hs:14:16: error:
+    • Couldn't match expected type ‘Bool’ with actual type ‘_a’
       ‘_a’ is a rigid type variable bound by
         the inferred type of baz :: _a -> Bool -> (_a, Bool)
         at NamedWildcardExplicitForall.hs:13:15
-    • In the expression: not x
+    • In the first argument of ‘not’, namely ‘x’
+      In the expression: not x
       In the expression: (not x, not y)
     • Relevant bindings include
         x :: _a (bound at NamedWildcardExplicitForall.hs:14:5)
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotEnabled.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotEnabled.stderr
index 0de48b4dcd..46cad28a12 100644
--- a/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotEnabled.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/NamedWildcardsNotEnabled.stderr
@@ -18,6 +18,7 @@ NamedWildcardsNotEnabled.hs:4:13: error:
         at NamedWildcardsNotEnabled.hs:3:8
     • In the first argument of ‘not’, namely ‘x’
       In the expression: not x
+      In an equation for ‘foo’: foo x = not x
     • Relevant bindings include
         x :: _a (bound at NamedWildcardsNotEnabled.hs:4:5)
         foo :: _a -> _b (bound at NamedWildcardsNotEnabled.hs:4:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr b/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr
index b943dfba2b..713bdc65c3 100644
--- a/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr
@@ -1,5 +1,6 @@
 
-ScopedNamedWildcardsBad.hs:8:21:
-    Couldn't match expected type ‘Bool’ with actual type ‘Char’
-    In the first argument of ‘not’, namely ‘x’
-    In the expression: not x
+ScopedNamedWildcardsBad.hs:8:21: error:
+    • Couldn't match expected type ‘Bool’ with actual type ‘Char’
+    • In the first argument of ‘not’, namely ‘x’
+      In the expression: not x
+      In an equation for ‘v’: v = not x
diff --git a/testsuite/tests/patsyn/should_fail/records-poly-update.stderr b/testsuite/tests/patsyn/should_fail/records-poly-update.stderr
index ed456ff171..44bee9b2c3 100644
--- a/testsuite/tests/patsyn/should_fail/records-poly-update.stderr
+++ b/testsuite/tests/patsyn/should_fail/records-poly-update.stderr
@@ -1,5 +1,6 @@
 
 records-poly-update.hs:11:14: error:
-    Couldn't match expected type ‘Bool’ with actual type ‘A’
-    In the ‘j’ field of a record
-    In the expression: p1 {j = A}
+    • Couldn't match expected type ‘Bool’ with actual type ‘A’
+    • In the ‘j’ field of a record
+      In the expression: p1 {j = A}
+      In an equation for ‘p6’: p6 = p1 {j = A}
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 42f2bc9c16..9c3daa71b1 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -394,7 +394,7 @@ test('T5631',
         # expected value: 392904228 (x86/Linux)
         # 2014-04-04:     346389856 (x86 Windows, 64 bit machine)
         # 2014-12-01:     390199244 (Windows laptop)
-           (wordsize(64), 1128828928, 5)]),
+           (wordsize(64), 1198327544, 5)]),
         # expected value: 774595008 (amd64/Linux):
         # expected value: 735486328 (amd64/Linux) 2012/12/12:
         # expected value: 690742040 (amd64/Linux) Call Arity improvements
@@ -402,6 +402,7 @@ test('T5631',
         # 2014-11-04:     776121120 (amd64/Linux) new-flatten-skolems
         # 2015-06-01:     812288344 (amd64/Linux) unknown cause
 	# 2015-12-11:     1128828928 (amd64/Linux) TypeInType (see #11196)
+	# 2015-12-21:     1198327544 (Mac) TypeApplications (will fix with #11196)
        only_ways(['normal'])
       ],
      compile,
diff --git a/testsuite/tests/polykinds/T10503.stderr b/testsuite/tests/polykinds/T10503.stderr
index 7c39c41738..141f16fc6e 100644
--- a/testsuite/tests/polykinds/T10503.stderr
+++ b/testsuite/tests/polykinds/T10503.stderr
@@ -9,8 +9,6 @@ T10503.hs:8:6: error:
         the type signature for:
           h :: forall k r. ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
         at T10503.hs:8:6
-      Expected type: ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
-        Actual type: ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
     • In the ambiguity check for ‘h’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
diff --git a/testsuite/tests/polykinds/T6068.stdout b/testsuite/tests/polykinds/T6068.stdout
index e096418727..f0fe7de899 100644
--- a/testsuite/tests/polykinds/T6068.stdout
+++ b/testsuite/tests/polykinds/T6068.stdout
@@ -1 +1 @@
-exists Nothing :: Floop a mp => Existential mp
+exists Nothing :: Floop a mp => Existential mp
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index 539d15d406..46b7181840 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -2,18 +2,18 @@
 T7438.hs:6:14: error:
     • Couldn't match expected type ‘r1’ with actual type ‘r’
         ‘r1’ is untouchable
-          inside the constraints: r3 ~ r2
+          inside the constraints: t1 ~ t
           bound by a pattern with constructor:
                      Nil :: forall k (a :: k). Thrist a a,
                    in an equation for ‘go’
           at T7438.hs:6:4-6
       ‘r1’ is a rigid type variable bound by
-        the inferred type of go :: Thrist r2 r3 -> r -> r1 at T7438.hs:6:1
+        the inferred type of go :: Thrist t t1 -> r -> r1 at T7438.hs:6:1
       ‘r’ is a rigid type variable bound by
-        the inferred type of go :: Thrist r2 r3 -> r -> r1 at T7438.hs:6:1
+        the inferred type of go :: Thrist t t1 -> r -> r1 at T7438.hs:6:1
       Possible fix: add a type signature for ‘go’
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
     • Relevant bindings include
         acc :: r (bound at T7438.hs:6:8)
-        go :: Thrist r2 r3 -> r -> r1 (bound at T7438.hs:6:1)
+        go :: Thrist t t1 -> r -> r1 (bound at T7438.hs:6:1)
diff --git a/testsuite/tests/polykinds/T7594.stderr b/testsuite/tests/polykinds/T7594.stderr
index 2f1844ecdb..be2acfebe0 100644
--- a/testsuite/tests/polykinds/T7594.stderr
+++ b/testsuite/tests/polykinds/T7594.stderr
@@ -13,4 +13,5 @@ T7594.hs:35:12: error:
         Actual type: a -> IO ()
     • In the first argument of ‘app’, namely ‘print’
       In the expression: app print q2
+      In an equation for ‘bar2’: bar2 = app print q2
     • Relevant bindings include bar2 :: b (bound at T7594.hs:35:1)
diff --git a/testsuite/tests/polykinds/T9144.stderr b/testsuite/tests/polykinds/T9144.stderr
index f2c65530ee..b62d1f175d 100644
--- a/testsuite/tests/polykinds/T9144.stderr
+++ b/testsuite/tests/polykinds/T9144.stderr
@@ -1,7 +1,9 @@
-
-T9144.hs:34:26:
-    Couldn't match type ‘Integer’ with ‘FooTerm’
-    Expected type: DemoteRep 'KProxy
-      Actual type: DemoteRep 'KProxy
-    In the first argument of ‘toSing’, namely ‘n’
-    In the expression: toSing n
+
+T9144.hs:34:26: error:
+    • Couldn't match type ‘Integer’ with ‘FooTerm’
+      Expected type: DemoteRep 'KProxy
+        Actual type: DemoteRep 'KProxy
+    • In the first argument of ‘toSing’, namely ‘n’
+      In the expression: toSing n
+      In the expression:
+        case toSing n of { SomeSing n' -> SomeSing (SBar n') }
diff --git a/testsuite/tests/polykinds/TidyClassKinds.hs b/testsuite/tests/polykinds/TidyClassKinds.hs
new file mode 100644
index 0000000000..83f6eaaea2
--- /dev/null
+++ b/testsuite/tests/polykinds/TidyClassKinds.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MultiParamTypeClasses, PolyKinds #-}
+{-# OPTIONS_GHC -fprint-explicit-kinds #-}
+
+module TidyClassKinds where
+
+import Data.Proxy
+
+class Poly a b
+
+type ProxySyn = Proxy
+
+instance Poly ProxySyn ProxySyn
+  -- output should really talk about k1 and k2, not about k and k!
diff --git a/testsuite/tests/polykinds/TidyClassKinds.stderr b/testsuite/tests/polykinds/TidyClassKinds.stderr
new file mode 100644
index 0000000000..69ca49c188
--- /dev/null
+++ b/testsuite/tests/polykinds/TidyClassKinds.stderr
@@ -0,0 +1,8 @@
+
+TidyClassKinds.hs:12:10: error:
+    • Illegal instance declaration for
+        ‘Poly (k1 -> *) (k1 -> *) (ProxySyn k1) (ProxySyn k1)’
+        (All instance types must be of the form (T t1 ... tn)
+         where T is not a synonym.
+         Use TypeSynonymInstances if you want to disable this.)
+    • In the instance declaration for ‘Poly ProxySyn ProxySyn’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 6387d1790d..5a8a9043ab 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -127,6 +127,7 @@ test('T11142', normal, compile_fail, [''])
 test('SigTvKinds', normal, compile, [''])
 test('SigTvKinds2', expect_broken(11203), compile_fail, [''])
 test('T9017', normal, compile_fail, [''])
+test('TidyClassKinds', normal, compile_fail, ['-fprint-explicit-kinds'])
 test('T11249', normal, compile, [''])
 test('T11248', normal, compile, [''])
 test('T11278', normal, compile, [''])
diff --git a/testsuite/tests/rename/should_compile/T3823.stderr b/testsuite/tests/rename/should_compile/T3823.stderr
index 8ab375fcd4..6287a3529f 100644
--- a/testsuite/tests/rename/should_compile/T3823.stderr
+++ b/testsuite/tests/rename/should_compile/T3823.stderr
@@ -1,5 +1,6 @@
 
-T3823B.hs:8:7:
+T3823B.hs:8:7: error:
     Couldn't match expected type ‘A’ with actual type ‘Bool’
     In the first argument of ‘y’, namely ‘a’
     In the expression: y a
+    In an equation for ‘b’: b = y a
diff --git a/testsuite/tests/rename/should_fail/T10618.stderr b/testsuite/tests/rename/should_fail/T10618.stderr
index 01e194877f..8b4dc2c28d 100644
--- a/testsuite/tests/rename/should_fail/T10618.stderr
+++ b/testsuite/tests/rename/should_fail/T10618.stderr
@@ -1,6 +1,6 @@
-
-T10618.hs:3:22: error:
-    Variable not in scope: (<>) :: Maybe (Maybe a0) -> Maybe a1 -> t
-    Perhaps you meant one of these:
-      ‘<$>’ (imported from Prelude), ‘*>’ (imported from Prelude),
-      ‘<$’ (imported from Prelude)
+
+T10618.hs:3:22: error:
+    • Variable not in scope: (<>) :: Maybe (Maybe a0) -> Maybe a1 -> t
+    • Perhaps you meant one of these:
+        ‘<$>’ (imported from Prelude), ‘*>’ (imported from Prelude),
+        ‘<$’ (imported from Prelude)
diff --git a/testsuite/tests/rename/should_fail/T2993.stderr b/testsuite/tests/rename/should_fail/T2993.stderr
index 257e9d434b..4cae65ae88 100644
--- a/testsuite/tests/rename/should_fail/T2993.stderr
+++ b/testsuite/tests/rename/should_fail/T2993.stderr
@@ -1,4 +1,4 @@
 
 T2993.hs:7:13: error:
-    Variable not in scope: (<**>) :: t -> (a -> a) -> t1
-    Perhaps you meant ‘<*>’ (imported from Prelude)
+    • Variable not in scope: (<**>) :: t -> (b -> b) -> t1
+    • Perhaps you meant ‘<*>’ (imported from Prelude)
diff --git a/testsuite/tests/rename/should_fail/T7937.stderr b/testsuite/tests/rename/should_fail/T7937.stderr
index 8a5edd37c7..7a65b0c06e 100644
--- a/testsuite/tests/rename/should_fail/T7937.stderr
+++ b/testsuite/tests/rename/should_fail/T7937.stderr
@@ -1,4 +1,4 @@
-
-T7937.hs:8:13: error:
-    Variable not in scope: (***) :: Bool -> Bool -> t
-    Perhaps you meant ‘**’ (imported from Prelude)
+
+T7937.hs:8:13: error:
+    • Variable not in scope: (***) :: Bool -> Bool -> t
+    • Perhaps you meant ‘**’ (imported from Prelude)
diff --git a/testsuite/tests/rename/should_fail/mc13.stderr b/testsuite/tests/rename/should_fail/mc13.stderr
index d4bc26b389..e55f179a46 100644
--- a/testsuite/tests/rename/should_fail/mc13.stderr
+++ b/testsuite/tests/rename/should_fail/mc13.stderr
@@ -1,2 +1,2 @@
-
-mc13.hs:12:37: error: Variable not in scope: f :: [a] -> m a
+
+mc13.hs:12:37: error: Variable not in scope: f :: [a] -> m a
diff --git a/testsuite/tests/rename/should_fail/rnfail016.stderr b/testsuite/tests/rename/should_fail/rnfail016.stderr
index eeeddfa58c..2193ffb068 100644
--- a/testsuite/tests/rename/should_fail/rnfail016.stderr
+++ b/testsuite/tests/rename/should_fail/rnfail016.stderr
@@ -1,4 +1,8 @@
 
-rnfail016.hs:6:7: Pattern syntax in expression context: x@x
+rnfail016.hs:6:7: error:
+    Pattern syntax in expression context: x@x
+    Did you mean to enable TypeApplications?
 
-rnfail016.hs:7:7: Pattern syntax in expression context: ~x
+rnfail016.hs:7:7: error:
+    Pattern syntax in expression context: ~x
+    Did you mean to enable TypeApplications?
diff --git a/testsuite/tests/rename/should_fail/rnfail051.stderr b/testsuite/tests/rename/should_fail/rnfail051.stderr
index 36eccc5724..a06ddc5265 100644
--- a/testsuite/tests/rename/should_fail/rnfail051.stderr
+++ b/testsuite/tests/rename/should_fail/rnfail051.stderr
@@ -1,3 +1,4 @@
 
-rnfail051.hs:7:17:
+rnfail051.hs:7:17: error:
     Pattern syntax in expression context: _ -> putStrLn "_"
+    Did you mean to enable TypeApplications?
diff --git a/testsuite/tests/roles/should_compile/Roles1.stderr b/testsuite/tests/roles/should_compile/Roles1.stderr
index 581b043286..ef67f90d8b 100644
--- a/testsuite/tests/roles/should_compile/Roles1.stderr
+++ b/testsuite/tests/roles/should_compile/Roles1.stderr
@@ -15,10 +15,10 @@ TYPE CONSTRUCTORS
     Kind: * -> *
   type role T6 phantom
   data T6 (a :: k) = K6
-    Kind: forall k1. k1 -> *
+    Kind: forall {k1}. k1 -> *
   type role T7 phantom representational
   data T7 (a :: k) b = K7 b
-    Kind: forall k1. k1 -> * -> *
+    Kind: forall {k1}. k1 -> * -> *
 COERCION AXIOMS
 Dependent modules: []
 Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
@@ -27,46 +27,88 @@ Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
 ==================== Typechecker ====================
 Roles1.$tcT7
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "T7"#)
+      12795488517584970699##
+      6852268802866176810##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "T7"#)
 Roles1.$tc'K7
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "'K7"#)
+      12022030613939361326##
+      11727141136040515167##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "'K7"#)
 Roles1.$tcT6
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "T6"#)
+      1052116432298682626##
+      4782516991847719023##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "T6"#)
 Roles1.$tc'K6
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "'K6"#)
+      14383224451764499060##
+      13586832700239872984##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "'K6"#)
 Roles1.$tcT5
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "T5"#)
+      10855726709479635304##
+      5574528370049939204##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "T5"#)
 Roles1.$tc'K5
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "'K5"#)
+      17986294396600628264##
+      15784122741796850983##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "'K5"#)
 Roles1.$tcT4
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "T4"#)
+      5809060867006837344##
+      8795972313583150301##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "T4"#)
 Roles1.$tc'K4
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "'K4"#)
+      6498964159768283182##
+      956453098475971212##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "'K4"#)
 Roles1.$tcT3
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "T3"#)
+      17827258502042208248##
+      10404219359416482652##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "T3"#)
 Roles1.$tc'K3
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "'K3"#)
+      18386915834109553575##
+      773967725306507064##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "'K3"#)
 Roles1.$tcT2
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "T2"#)
+      14324923875690440398##
+      17626224477681351106##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "T2"#)
 Roles1.$tc'K2
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "'K2"#)
+      17795591238510508397##
+      10155757471958311507##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "'K2"#)
 Roles1.$tcT1
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "T1"#)
+      12633763300352597178##
+      11103726621424210926##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "T1"#)
 Roles1.$tc'K1
   = GHC.Types.TyCon
-      0## 0## Roles1.$trModule (GHC.Types.TrNameS "'K1"#)
+      1949157551035372857##
+      3576433963139282451##
+      Roles1.$trModule
+      (GHC.Types.TrNameS "'K1"#)
 Roles1.$trModule
   = GHC.Types.Module
       (GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "Roles1"#)
diff --git a/testsuite/tests/roles/should_compile/T8958.stderr b/testsuite/tests/roles/should_compile/T8958.stderr
index 40633142f0..ba97e8a45f 100644
--- a/testsuite/tests/roles/should_compile/T8958.stderr
+++ b/testsuite/tests/roles/should_compile/T8958.stderr
@@ -44,6 +44,7 @@ T8958.$trModule
       (GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "T8958"#)
 AbsBinds [a] []
   {Exports: [T8958.$fRepresentationala <= $dRepresentational
+               <>
                <>]
    Exported types: T8958.$fRepresentationala
                      :: forall a. Representational a
@@ -52,6 +53,7 @@ AbsBinds [a] []
    Evidence: [EvBinds{}]}
 AbsBinds [a] []
   {Exports: [T8958.$fNominala <= $dNominal
+               <>
                <>]
    Exported types: T8958.$fNominala :: forall a. Nominal a
                    [LclIdX[DFunId], Str=DmdType]
diff --git a/testsuite/tests/rts/T9045.hs b/testsuite/tests/rts/T9045.hs
index f01bf84e38..abd236d985 100644
--- a/testsuite/tests/rts/T9045.hs
+++ b/testsuite/tests/rts/T9045.hs
@@ -15,7 +15,7 @@ main :: IO ()
 main = do
     hSetBuffering stdout NoBuffering
     [nthreads] <- fmap (map read) getArgs
-    tids <- replicateM nthreads . mask $ \_ -> forkIO $ return ()
+    tids <- replicateM nthreads (mask $ \_ -> forkIO $ return ())
     m <- newEmptyMVar
     -- do it in a subthread to avoid bound-thread overhead
     forkIO $ do mapM_ killThread tids; putMVar m ()
diff --git a/testsuite/tests/safeHaskell/ghci/p16.stderr b/testsuite/tests/safeHaskell/ghci/p16.stderr
index 893cf2d8ee..4b445166d2 100644
--- a/testsuite/tests/safeHaskell/ghci/p16.stderr
+++ b/testsuite/tests/safeHaskell/ghci/p16.stderr
@@ -3,13 +3,13 @@
     -XGeneralizedNewtypeDeriving is not allowed in Safe Haskell; ignoring -XGeneralizedNewtypeDeriving
 
 <interactive>:15:29: error:
-    Can't make a derived instance of ‘Op T2’:
-      ‘Op’ is not a standard derivable class (Eq, Show, etc.)
-      Try GeneralizedNewtypeDeriving for GHC's newtype-deriving extension
-    In the newtype declaration for ‘T2’
+    • Can't make a derived instance of ‘Op T2’:
+        ‘Op’ is not a standard derivable class (Eq, Show, etc.)
+        Try GeneralizedNewtypeDeriving for GHC's newtype-deriving extension
+    • In the newtype declaration for ‘T2’
 
 <interactive>:18:9: error:
-    Data constructor not in scope: T2 :: T -> t
-    Perhaps you meant ‘T1’ (line 12)
+    • Data constructor not in scope: T2 :: T -> t
+    • Perhaps you meant ‘T1’ (line 12)
 
 <interactive>:21:4: error: Variable not in scope: y
diff --git a/testsuite/tests/safeHaskell/ghci/p6.stderr b/testsuite/tests/safeHaskell/ghci/p6.stderr
index 8cca54eb2f..74beb053ca 100644
--- a/testsuite/tests/safeHaskell/ghci/p6.stderr
+++ b/testsuite/tests/safeHaskell/ghci/p6.stderr
@@ -1,10 +1,10 @@
-
-<interactive>:11:1: error:
-    Unacceptable result type in foreign declaration:
-      Safe Haskell is on, all FFI imports must be in the IO monad
-    When checking declaration:
-      foreign import ccall safe "static sin" c_sin :: Double -> Double
-
-<interactive>:12:1: error:
-    Variable not in scope: c_sin :: Integer -> t
-    Perhaps you meant ‘c_sin'’ (line 7)
+
+<interactive>:11:1: error:
+    • Unacceptable result type in foreign declaration:
+        Safe Haskell is on, all FFI imports must be in the IO monad
+    • When checking declaration:
+        foreign import ccall safe "static sin" c_sin :: Double -> Double
+
+<interactive>:12:1: error:
+    • Variable not in scope: c_sin :: Integer -> t
+    • Perhaps you meant ‘c_sin'’ (line 7)
diff --git a/testsuite/tests/simplCore/should_compile/T7360.stderr b/testsuite/tests/simplCore/should_compile/T7360.stderr
index 9ded9c1349..ca398ec6dc 100644
--- a/testsuite/tests/simplCore/should_compile/T7360.stderr
+++ b/testsuite/tests/simplCore/should_compile/T7360.stderr
@@ -66,7 +66,11 @@ T7360.$tc'Foo3 :: GHC.Types.TyCon
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
 T7360.$tc'Foo3 =
-  GHC.Types.TyCon 0## 0## T7360.$trModule T7360.$tc'Foo6
+  GHC.Types.TyCon
+    10507205234936349519##
+    8302184214013227554##
+    T7360.$trModule
+    T7360.$tc'Foo6
 
 -- RHS size: {terms: 2, types: 0, coercions: 0}
 T7360.$tc'Foo5 :: GHC.Types.TrName
@@ -85,7 +89,11 @@ T7360.$tc'Foo2 :: GHC.Types.TyCon
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
 T7360.$tc'Foo2 =
-  GHC.Types.TyCon 0## 0## T7360.$trModule T7360.$tc'Foo5
+  GHC.Types.TyCon
+    9825259700232563546##
+    11056638024476048052##
+    T7360.$trModule
+    T7360.$tc'Foo5
 
 -- RHS size: {terms: 2, types: 0, coercions: 0}
 T7360.$tc'Foo4 :: GHC.Types.TrName
@@ -104,7 +112,11 @@ T7360.$tc'Foo1 :: GHC.Types.TyCon
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
 T7360.$tc'Foo1 =
-  GHC.Types.TyCon 0## 0## T7360.$trModule T7360.$tc'Foo4
+  GHC.Types.TyCon
+    2058692068419561651##
+    9152017373001677943##
+    T7360.$trModule
+    T7360.$tc'Foo4
 
 -- RHS size: {terms: 2, types: 0, coercions: 0}
 T7360.$tcFoo1 :: GHC.Types.TrName
@@ -123,7 +135,11 @@ T7360.$tcFoo :: GHC.Types.TyCon
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 50}]
 T7360.$tcFoo =
-  GHC.Types.TyCon 0## 0## T7360.$trModule T7360.$tcFoo1
+  GHC.Types.TyCon
+    8358641983981300860##
+    582034888424804490##
+    T7360.$trModule
+    T7360.$tcFoo1
 
 -- RHS size: {terms: 5, types: 2, coercions: 0}
 fun1 [InlPrag=NOINLINE] :: Foo -> ()
diff --git a/testsuite/tests/simplCore/should_compile/simpl017.stderr b/testsuite/tests/simplCore/should_compile/simpl017.stderr
index 2d3c16ef71..bb74213dfe 100644
--- a/testsuite/tests/simplCore/should_compile/simpl017.stderr
+++ b/testsuite/tests/simplCore/should_compile/simpl017.stderr
@@ -1,38 +1,22 @@
 
-simpl017.hs:55:12:
-    Couldn't match expected type ‘forall v. [E m i] -> E' v m a’
-                with actual type ‘[E m i] -> E' v0 m a’
-    In the first argument of ‘return’, namely ‘f’
-    In a stmt of a 'do' block: return f
-    Relevant bindings include
-      f :: [E m i] -> E' v0 m a (bound at simpl017.hs:54:9)
-      ix :: [E m i] -> m i (bound at simpl017.hs:52:9)
-      a :: arr i a (bound at simpl017.hs:50:11)
-      liftArray :: arr i a -> E m (forall v. [E m i] -> E' v m a)
-        (bound at simpl017.hs:50:1)
-
-simpl017.hs:74:5:
-    Couldn't match expected type ‘[E (ST t0) Int] -> E (ST s) Int’
-                with actual type ‘forall v. [E (ST s) Int] -> E' v (ST s) Int’
-    The function ‘a’ is applied to one argument,
-    but its type ‘forall v. [E (ST s) Int] -> E' v (ST s) Int’ has none
-    In the first argument of ‘plus’, namely ‘a [one]’
-    In a stmt of a 'do' block: a [one] `plus` a [one]
-    Relevant bindings include
-      a :: forall v. [E (ST s) Int] -> E' v (ST s) Int
-        (bound at simpl017.hs:71:5)
-      ma :: STArray s Int Int (bound at simpl017.hs:70:5)
-      foo :: STArray s Int Int -> ST s Int (bound at simpl017.hs:70:1)
-
-simpl017.hs:74:19:
-    Couldn't match expected type ‘[E (ST t1) Int] -> E (ST s) Int’
-                with actual type ‘forall v. [E (ST s) Int] -> E' v (ST s) Int’
-    The function ‘a’ is applied to one argument,
-    but its type ‘forall v. [E (ST s) Int] -> E' v (ST s) Int’ has none
-    In the second argument of ‘plus’, namely ‘a [one]’
-    In a stmt of a 'do' block: a [one] `plus` a [one]
-    Relevant bindings include
-      a :: forall v. [E (ST s) Int] -> E' v (ST s) Int
-        (bound at simpl017.hs:71:5)
-      ma :: STArray s Int Int (bound at simpl017.hs:70:5)
-      foo :: STArray s Int Int -> ST s Int (bound at simpl017.hs:70:1)
+simpl017.hs:50:15: error:
+    • Couldn't match type ‘[E m i] -> E' v0 m a’
+                     with ‘forall v. [E m i] -> E' v m a’
+      Expected type: E m (forall v. [E m i] -> E' v m a)
+        Actual type: E' RValue m ([E m i] -> E' v0 m a)
+    • In the expression:
+        E (do { let ix :: [E m i] -> m i
+                    ix [i] = runE i
+                    {-# INLINE f #-}
+                    ....;
+                return f })
+      In an equation for ‘liftArray’:
+          liftArray a
+            = E (do { let ix :: [E m i] -> m i
+                          ix [i] = runE i
+                          ....;
+                      return f })
+    • Relevant bindings include
+        a :: arr i a (bound at simpl017.hs:50:11)
+        liftArray :: arr i a -> E m (forall v. [E m i] -> E' v m a)
+          (bound at simpl017.hs:50:1)
diff --git a/testsuite/tests/th/T10945.stderr b/testsuite/tests/th/T10945.stderr
index 0c1d949053..c84fa38b61 100644
--- a/testsuite/tests/th/T10945.stderr
+++ b/testsuite/tests/th/T10945.stderr
@@ -1,29 +1,32 @@
 
-T10945.hs:7:11:
-    Couldn't match expected type ‘TExp DecsQ’ with actual type ‘[Dec]’
-    In the first argument of ‘return’, namely
-      ‘[SigD
-          (mkName "m")
-          (ForallT
-             [PlainTV (mkName "a")]
-             []
-             (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
-        FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]]’
-    In the expression:
-      return
-        [SigD
-           (mkName "m")
-           (ForallT
-              [PlainTV (mkName "a")]
-              []
-              (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
-         FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]]
-    In the Template Haskell splice
-      $$(return
-           [SigD
-              (mkName "m")
-              (ForallT
-                 [PlainTV (mkName "a")]
-                 []
-                 (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
-            FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]])
+T10945.hs:7:4: error:
+    • Couldn't match type ‘[Dec]’ with ‘TExp DecsQ’
+      Expected type: Q (TExp DecsQ)
+        Actual type: Q [Dec]
+    • In the expression:
+        return
+          [SigD
+             (mkName "m")
+             (ForallT
+                [PlainTV (mkName "a")]
+                []
+                (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
+           FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]]
+      In the Template Haskell splice
+        $$(return
+             [SigD
+                (mkName "m")
+                (ForallT
+                   [PlainTV (mkName "a")]
+                   []
+                   (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
+              FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]])
+      In the expression:
+        $$(return
+             [SigD
+                (mkName "m")
+                (ForallT
+                   [PlainTV (mkName "a")]
+                   []
+                   (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
+              FunD (mkName "m") [Clause ... (NormalB (VarE (mkName "x"))) ...]])
diff --git a/testsuite/tests/th/T8577.stderr b/testsuite/tests/th/T8577.stderr
index 734007e6cc..ef95cc313d 100644
--- a/testsuite/tests/th/T8577.stderr
+++ b/testsuite/tests/th/T8577.stderr
@@ -1,7 +1,8 @@
 
-T8577.hs:9:11:
+T8577.hs:9:11: error:
     Couldn't match type ‘Int’ with ‘Bool’
     Expected type: Q (TExp (A Bool))
       Actual type: Q (TExp (A Int))
     In the expression: y
     In the Template Haskell splice $$y
+    In the expression: $$y
diff --git a/testsuite/tests/typecheck/bug1465/bug1465.stderr b/testsuite/tests/typecheck/bug1465/bug1465.stderr
index 1c67068762..4e31c7f195 100644
--- a/testsuite/tests/typecheck/bug1465/bug1465.stderr
+++ b/testsuite/tests/typecheck/bug1465/bug1465.stderr
@@ -6,3 +6,4 @@ C.hs:6:11: error:
         ‘bug1465-1.0:A.T’ is defined in ‘A’ in package ‘bug1465-1.0’
     In the expression: B2.f
     In the expression: [B1.f, B2.f]
+    In an equation for ‘x’: x = [B1.f, B2.f]
diff --git a/testsuite/tests/typecheck/should_compile/FD1.stderr b/testsuite/tests/typecheck/should_compile/FD1.stderr
index 19d698294a..395217af8b 100644
--- a/testsuite/tests/typecheck/should_compile/FD1.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD1.stderr
@@ -1,6 +1,6 @@
 
 FD1.hs:16:1: error:
-    • Couldn't match expected type ‘Int -> Int’ with actual type ‘a’
+    • Couldn't match expected type ‘a’ with actual type ‘Int -> Int’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           plus :: forall a. E a (Int -> Int) => Int -> a
diff --git a/testsuite/tests/typecheck/should_compile/FD2.stderr b/testsuite/tests/typecheck/should_compile/FD2.stderr
index 93997c52ec..ff3a923988 100644
--- a/testsuite/tests/typecheck/should_compile/FD2.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD2.stderr
@@ -1,15 +1,16 @@
 
-FD2.hs:26:34: error:
-    • Couldn't match expected type ‘e1’ with actual type ‘e’
-      ‘e’ is a rigid type variable bound by
-        the type signature for:
-          foldr1 :: forall e. Elem a e => (e -> e -> e) -> a -> e
-        at FD2.hs:21:13
+FD2.hs:26:36: error:
+    • Couldn't match expected type ‘e’ with actual type ‘e1’
       ‘e1’ is a rigid type variable bound by
         the type signature for:
           mf :: forall e1. Elem a e1 => e1 -> Maybe e1 -> Maybe e1
         at FD2.hs:24:18
-    • In the first argument of ‘Just’, namely ‘(f x y)’
+      ‘e’ is a rigid type variable bound by
+        the type signature for:
+          foldr1 :: forall e. Elem a e => (e -> e -> e) -> a -> e
+        at FD2.hs:21:13
+    • In the first argument of ‘f’, namely ‘x’
+      In the first argument of ‘Just’, namely ‘(f x y)’
       In the expression: Just (f x y)
     • Relevant bindings include
         y :: e1 (bound at FD2.hs:26:23)
diff --git a/testsuite/tests/typecheck/should_compile/PushHRIf.hs b/testsuite/tests/typecheck/should_compile/PushHRIf.hs
new file mode 100644
index 0000000000..f6839133a0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/PushHRIf.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes #-}
+
+module PushHRIf where
+
+foo = (if True then id else id) :: forall a. a -> a
+
+bar = (foo 'x', foo True)
diff --git a/testsuite/tests/typecheck/should_compile/T10072.stderr b/testsuite/tests/typecheck/should_compile/T10072.stderr
index ba15398874..eb14ad8de5 100644
--- a/testsuite/tests/typecheck/should_compile/T10072.stderr
+++ b/testsuite/tests/typecheck/should_compile/T10072.stderr
@@ -1,8 +1,8 @@
-
-T10072.hs:3:31: error:
-    Found type wildcard ‘_’ standing for ‘b’
-    Where: ‘b’ is a rigid type variable bound by
-               the RULE "map/empty" at T10072.hs:3:1
-    To use the inferred type, enable PartialTypeSignatures
-    In a RULE for ‘f’: a -> _
-    When checking the transformation rule "map/empty"
+
+T10072.hs:3:31: error:
+    • Found type wildcard ‘_’ standing for ‘b’
+      Where: ‘b’ is a rigid type variable bound by
+               the RULE "map/empty" at T10072.hs:3:1
+      To use the inferred type, enable PartialTypeSignatures
+    • In a RULE for ‘f’: a -> _
+      When checking the transformation rule "map/empty"
diff --git a/testsuite/tests/typecheck/should_compile/T10971a.stderr b/testsuite/tests/typecheck/should_compile/T10971a.stderr
index 7ca7680c52..eea8a11ea3 100644
--- a/testsuite/tests/typecheck/should_compile/T10971a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T10971a.stderr
@@ -34,9 +34,9 @@ T10971a.hs:9:6: warning:
 
 T10971a.hs:9:31: warning:
     • Defaulting the following constraints to type ‘[]’
-        (Foldable t0) arising from a use of ‘length’ at T10971a.hs:9:31-36
+        (Foldable t0) arising from a use of ‘length’ at T10971a.hs:9:31-38
         (Traversable t0)
-          arising from a use of ‘fmapDefault’ at T10971a.hs:9:14-24
+          arising from a use of ‘fmapDefault’ at T10971a.hs:9:14-28
     • In the expression: length x
       In the expression: (fmapDefault f x, length x)
       In the expression: \ f x -> (fmapDefault f x, length x)
diff --git a/testsuite/tests/typecheck/should_compile/T2494.stderr b/testsuite/tests/typecheck/should_compile/T2494.stderr
index 71351cba0a..b398459aa9 100644
--- a/testsuite/tests/typecheck/should_compile/T2494.stderr
+++ b/testsuite/tests/typecheck/should_compile/T2494.stderr
@@ -1,34 +1,36 @@
 
-T2494.hs:15:14:
-    Couldn't match type ‘b’ with ‘a’
+T2494.hs:15:14: error:
+    • Couldn't match type ‘b’ with ‘a’
       ‘b’ is a rigid type variable bound by
-          the RULE "foo/foo" at T2494.hs:14:16
+        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)
-    In the first argument of ‘foo’, namely ‘g’
-    In the second argument of ‘foo’, namely ‘(foo g x)’
-    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)
+        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)
+    • In the first argument of ‘foo’, namely ‘g’
+      In the second argument of ‘foo’, namely ‘(foo g x)’
+      In the expression: foo f (foo g x)
+    • 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)
 
-T2494.hs:15:30:
-    Couldn't match type ‘b’ with ‘a’
+T2494.hs:15:30: error:
+    • Couldn't match type ‘b’ with ‘a’
       ‘b’ is a rigid type variable bound by
-          the RULE "foo/foo" at T2494.hs:14:16
+        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)
-    In the second argument of ‘(.)’, namely ‘g’
-    In the first argument of ‘foo’, namely ‘(f . g)’
-    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)
+        the RULE "foo/foo" at T2494.hs:13:16
+      Expected type: Maybe (m b) -> Maybe (m a)
+        Actual type: Maybe (m b) -> Maybe (m b)
+    • In the second argument of ‘(.)’, namely ‘g’
+      In the first argument of ‘foo’, namely ‘(f . g)’
+      In the expression: foo (f . g) x
+    • 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)
diff --git a/testsuite/tests/typecheck/should_compile/Vta1.hs b/testsuite/tests/typecheck/should_compile/Vta1.hs
new file mode 100644
index 0000000000..c3ba43de54
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/Vta1.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE TypeApplications, ScopedTypeVariables, PolyKinds,
+             TypeFamilies, RankNTypes,
+             FlexibleContexts #-}
+-- tests about visible type application
+
+module Vta1 where
+
+quad :: a -> b -> c -> d -> (a, b, c, d)
+quad = (,,,)
+
+silly = quad @_ @Bool @Char @_ 5 True 'a' "Hello"
+
+pairup_nosig x y = (x, y)
+
+pairup_sig :: a -> b -> (a,b)
+pairup_sig u w = (u, w)
+
+answer_sig = pairup_sig @Bool @Int False 7 --
+-- (False, 7) :: (Bool, Int)
+
+answer_read = show (read @Int "3") -- "3" :: String
+answer_show = show @Integer (read "5") -- "5" :: String
+answer_showread = show @Int (read @Int "7") -- "7" :: String
+
+intcons a = (:) @Int a
+
+intpair x y = pairup_sig @Int x y
+
+answer_pairup = pairup_sig @Int 5 True -- (5, True) :: (Int, Bool)
+answer_intpair = intpair 1 "hello" -- (1, "hello") :: (Int, String)
+answer_intcons = intcons 7 []      -- [7] :: [Int]
+
+type family F a
+type instance F Char = Bool
+
+g :: F a -> a
+g _ = undefined
+
+f :: Char
+f = g True
+
+answer = g @Char False
+
+mapSame :: forall b. (forall a. a -> a) -> [b] -> [b]
+mapSame _ [] = []
+mapSame fun (x:xs) = fun @b x : (mapSame @b fun xs)
+
+pair :: forall a. a-> (forall b. b -> (a, b))
+pair x y = (x, y)
+
+b = pair @Int 3 @Bool True
+c = mapSame id [1,2,3]
+d = pair 3 @Bool True
+
+pairnum :: forall a. Num a => forall b. b -> (a, b)
+pairnum = pair 3
+
+e = (pair 3 :: forall a. Num a => forall b. b -> (a, b)) @Int @Bool True
+h = pairnum @Int @Bool True
+
+data First (a :: * -> *) = F
+data Proxy (a :: k) = P -- This expands to P (kind variable) (type variable)
+data Three (a :: * -> k -> *) = T
+
+foo :: Proxy a -> Int
+foo _ = 0
+
+first :: First a -> Int
+first _ = 0
+
+fTest = first F
+fMaybe = first @Maybe F
+
+test = foo P
+bar = foo @Bool P -- should work
+
+too :: Three a -> Int
+too _ = 3
+
+threeBase = too T
+threeOk = too @Either T
+
+blah = Nothing @Int
+
+newtype N = MkN { unMkN :: forall a. Show a => a -> String }
+
+n = MkN show
+
+boo = unMkN n @Bool
+
+boo2 :: forall (a :: * -> *) . Proxy a -> Bool
+boo2 _ = False
+
+base = boo2 P
+bar'= boo2 @Maybe P -- should work
diff --git a/testsuite/tests/typecheck/should_compile/Vta2.hs b/testsuite/tests/typecheck/should_compile/Vta2.hs
new file mode 100644
index 0000000000..2851b06469
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/Vta2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes, TypeApplications #-}
+
+
+module Vta2 where
+
+checkIf :: Bool -> (forall a. a -> a) -> (Bool, Int)
+checkIf _ = if True
+            then \f -> (f True, f 5)
+            else \f -> (f False, f @Int 3)
+
+checkCase :: Bool -> (forall a. a -> a) -> (Bool, Int)
+checkCase _ = case True of
+                True -> \f -> (f True, f 5)
+                False -> \f -> (f False, f @Int 3)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a969a4c6ac..8002299fb1 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -471,6 +471,9 @@ test('T10428', normal, compile, [''])
 test('RepArrow', normal, compile, [''])
 test('T10562', normal, compile, [''])
 test('T10564', normal, compile, [''])
+test('Vta1', normal, compile, [''])
+test('Vta2', normal, compile, [''])
+test('PushHRIf', normal, compile, [''])
 test('T10632', normal, compile, [''])
 test('T10642', normal, compile, [''])
 test('T10744', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/holes.stderr b/testsuite/tests/typecheck/should_compile/holes.stderr
index 5cb341709e..8551f66c3b 100644
--- a/testsuite/tests/typecheck/should_compile/holes.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes.stderr
@@ -1,33 +1,33 @@
-
-holes.hs:3:5: warning:
-    Found hole: _ :: t
-    Where: ‘t’ is a rigid type variable bound by
-               the inferred type of f :: t at holes.hs:3:1
-    In the expression: _
-    In an equation for ‘f’: f = _
-    Relevant bindings include f :: t (bound at holes.hs:3:1)
-
-holes.hs:6:7: warning:
-    Found hole: _ :: Char
-    In the expression: _
-    In an equation for ‘g’: g x = _
-    Relevant bindings include
-      x :: Int (bound at holes.hs:6:3)
-      g :: Int -> Char (bound at holes.hs:6:1)
-
-holes.hs:8:5: warning:
-    Found hole: _ :: [Char]
-    In the first argument of ‘(++)’, namely ‘_’
-    In the expression: _ ++ "a"
-    In an equation for ‘h’: h = _ ++ "a"
-    Relevant bindings include h :: [Char] (bound at holes.hs:8:1)
-
-holes.hs:11:15: warning:
-    Found hole: _ :: b0
-    Where: ‘b0’ is an ambiguous type variable
-    In the second argument of ‘const’, namely ‘_’
-    In the expression: const y _
-    In an equation for ‘z’: z y = const y _
-    Relevant bindings include
-      y :: [a] (bound at holes.hs:11:3)
-      z :: [a] -> [a] (bound at holes.hs:11:1)
+
+holes.hs:3:5: warning:
+    • Found hole: _ :: t
+      Where: ‘t’ is a rigid type variable bound by
+               the inferred type of f :: t at holes.hs:3:1
+    • In the expression: _
+      In an equation for ‘f’: f = _
+    • Relevant bindings include f :: t (bound at holes.hs:3:1)
+
+holes.hs:6:7: warning:
+    • Found hole: _ :: Char
+    • In the expression: _
+      In an equation for ‘g’: g x = _
+    • Relevant bindings include
+        x :: Int (bound at holes.hs:6:3)
+        g :: Int -> Char (bound at holes.hs:6:1)
+
+holes.hs:8:5: warning:
+    • Found hole: _ :: [Char]
+    • In the first argument of ‘(++)’, namely ‘_’
+      In the expression: _ ++ "a"
+      In an equation for ‘h’: h = _ ++ "a"
+    • Relevant bindings include h :: [Char] (bound at holes.hs:8:1)
+
+holes.hs:11:15: warning:
+    • Found hole: _ :: b0
+      Where: ‘b0’ is an ambiguous type variable
+    • In the second argument of ‘const’, namely ‘_’
+      In the expression: const y _
+      In an equation for ‘z’: z y = const y _
+    • Relevant bindings include
+        y :: [a] (bound at holes.hs:11:3)
+        z :: [a] -> [a] (bound at holes.hs:11:1)
diff --git a/testsuite/tests/typecheck/should_compile/holes3.stderr b/testsuite/tests/typecheck/should_compile/holes3.stderr
index a6e7c6194e..2d1261b278 100644
--- a/testsuite/tests/typecheck/should_compile/holes3.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes3.stderr
@@ -1,36 +1,36 @@
-
-holes3.hs:3:5: error:
-    Found hole: _ :: t
-    Where: ‘t’ is a rigid type variable bound by
-               the inferred type of f :: t at holes3.hs:3:1
-    In the expression: _
-    In an equation for ‘f’: f = _
-    Relevant bindings include f :: t (bound at holes3.hs:3:1)
-
-holes3.hs:6:7: error:
-    Found hole: _gr :: Char
-    Or perhaps ‘_gr’ is mis-spelled, or not in scope
-    In the expression: _gr
-    In an equation for ‘g’: g x = _gr
-    Relevant bindings include
-      x :: Int (bound at holes3.hs:6:3)
-      g :: Int -> Char (bound at holes3.hs:6:1)
-
-holes3.hs:8:5: error:
-    Found hole: _aa :: [Char]
-    Or perhaps ‘_aa’ is mis-spelled, or not in scope
-    In the first argument of ‘(++)’, namely ‘_aa’
-    In the expression: _aa ++ "a"
-    In an equation for ‘h’: h = _aa ++ "a"
-    Relevant bindings include h :: [Char] (bound at holes3.hs:8:1)
-
-holes3.hs:11:15: error:
-    Found hole: _x :: b0
-    Where: ‘b0’ is an ambiguous type variable
-    Or perhaps ‘_x’ is mis-spelled, or not in scope
-    In the second argument of ‘const’, namely ‘_x’
-    In the expression: const y _x
-    In an equation for ‘z’: z y = const y _x
-    Relevant bindings include
-      y :: [a] (bound at holes3.hs:11:3)
-      z :: [a] -> [a] (bound at holes3.hs:11:1)
+
+holes3.hs:3:5: error:
+    • Found hole: _ :: t
+      Where: ‘t’ is a rigid type variable bound by
+               the inferred type of f :: t at holes3.hs:3:1
+    • In the expression: _
+      In an equation for ‘f’: f = _
+    • Relevant bindings include f :: t (bound at holes3.hs:3:1)
+
+holes3.hs:6:7: error:
+    • Found hole: _gr :: Char
+      Or perhaps ‘_gr’ is mis-spelled, or not in scope
+    • In the expression: _gr
+      In an equation for ‘g’: g x = _gr
+    • Relevant bindings include
+        x :: Int (bound at holes3.hs:6:3)
+        g :: Int -> Char (bound at holes3.hs:6:1)
+
+holes3.hs:8:5: error:
+    • Found hole: _aa :: [Char]
+      Or perhaps ‘_aa’ is mis-spelled, or not in scope
+    • In the first argument of ‘(++)’, namely ‘_aa’
+      In the expression: _aa ++ "a"
+      In an equation for ‘h’: h = _aa ++ "a"
+    • Relevant bindings include h :: [Char] (bound at holes3.hs:8:1)
+
+holes3.hs:11:15: error:
+    • Found hole: _x :: b0
+      Where: ‘b0’ is an ambiguous type variable
+      Or perhaps ‘_x’ is mis-spelled, or not in scope
+    • In the second argument of ‘const’, namely ‘_x’
+      In the expression: const y _x
+      In an equation for ‘z’: z y = const y _x
+    • Relevant bindings include
+        y :: [a] (bound at holes3.hs:11:3)
+        z :: [a] -> [a] (bound at holes3.hs:11:1)
diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr
index 96858b1d3c..e0de74c945 100644
--- a/testsuite/tests/typecheck/should_compile/tc141.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc141.stderr
@@ -7,19 +7,20 @@ tc141.hs:11:12: error:
       In a pattern binding: (p :: a, q :: a) = x
 
 tc141.hs:11:31: error:
-    • Couldn't match expected type ‘a2’ with actual type ‘a’
-        because type variable ‘a2’ would escape its scope
+    • Couldn't match expected type ‘a1’ with actual type ‘a’
+        because type variable ‘a1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         an expression type signature:
-          a2
+          a1
         at tc141.hs:11:31-34
     • In the expression: q :: a
       In the expression: (q :: a, p)
+      In the expression: let (p :: a, q :: a) = x in (q :: a, p)
     • Relevant bindings include
         p :: a (bound at tc141.hs:11:12)
         q :: a (bound at tc141.hs:11:17)
         x :: (a, a) (bound at tc141.hs:11:3)
-        f :: (a, a) -> (a1, a) (bound at tc141.hs:11:1)
+        f :: (a, a) -> (t, a) (bound at tc141.hs:11:1)
 
 tc141.hs:13:13: error:
     • You cannot bind scoped type variable ‘a’
@@ -42,7 +43,12 @@ tc141.hs:15:18: error:
         at tc141.hs:14:14-19
     • In the expression: b
       In an equation for ‘v’: v = b
+      In the expression:
+        let
+          v :: a
+          v = b
+        in v
     • Relevant bindings include
         v :: a1 (bound at tc141.hs:15:14)
         b :: r1 (bound at tc141.hs:13:5)
-        g :: r -> r1 -> a (bound at tc141.hs:13:1)
+        g :: r -> r1 -> forall a. a (bound at tc141.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_compile/tc168.stderr b/testsuite/tests/typecheck/should_compile/tc168.stderr
index 7d992a48a0..16ba4b0446 100644
--- a/testsuite/tests/typecheck/should_compile/tc168.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc168.stderr
@@ -1,12 +1,12 @@
-
-tc168.hs:17:1: error:
-    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
-    In the ambiguity check for the inferred type for ‘g’
-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-    When checking the inferred type
-      g :: forall a b a1. C a1 (a, b) => a1 -> a
+
+tc168.hs:17:1: error:
+    • 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
+    • In the ambiguity check for the inferred type for ‘g’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the inferred type
+        g :: forall a b a1. C a1 (a, b) => a1 -> a
diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
index d802dffe4e..89c82c4f9a 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc211.stderr
@@ -1,61 +1,20 @@
 
-tc211.hs:17:8: error:
-    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: error:
-    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: error:
-    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: error:
-    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: error:
-    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)
+    • 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 (a1 -> a1) -> (a1 -> a1) -> a1 -> a1
+    • In the expression:
+          foo2 ::
+            List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)
+      In the expression:
+        (foo2 ::
+           List (forall a. a -> a)
+           -> (forall a. a -> a) -> (forall a. a -> a))
+          xs1 (\ x -> x)
+      In an equation for ‘bar4’:
+          bar4
+            = (foo2 ::
+                 List (forall a. a -> a)
+                 -> (forall a. a -> a) -> (forall a. a -> a))
+                xs1 (\ x -> x)
diff --git a/testsuite/tests/typecheck/should_compile/tc243.stderr b/testsuite/tests/typecheck/should_compile/tc243.stderr
index 98e0f5ae1e..0219817408 100644
--- a/testsuite/tests/typecheck/should_compile/tc243.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc243.stderr
@@ -1,3 +1,3 @@
 
-tc243.hs:10:1: Warning:
-    Top-level binding with no type signature: (.+.) :: forall r. r
+tc243.hs:10:1: warning:
+    Top-level binding with no type signature: (.+.) :: forall a. a
diff --git a/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr b/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
index d95de09530..18c45a12c0 100644
--- a/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
+++ b/testsuite/tests/typecheck/should_fail/CustomTypeErrors01.stderr
@@ -1,5 +1,5 @@
 
-CustomTypeErrors01.hs:12:11: error:
-    Values of type 'MyType' cannot be compared for equality.
-    In the expression: x == MyType
-    In an equation for ‘err’: err x = x == MyType
+CustomTypeErrors01.hs:12:9: error:
+    • Values of type 'MyType' cannot be compared for equality.
+    • In the expression: x == MyType
+      In an equation for ‘err’: err x = x == MyType
diff --git a/testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr b/testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr
index 6ded98e0bd..49e262cd3c 100644
--- a/testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr
+++ b/testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr
@@ -1,9 +1,12 @@
+
 ExpandSynsFail2.hs:19:37: error:
-    Couldn't match type ‘Int’ with ‘Bool’
-    Expected type: ST s Foo
-      Actual type: MyBarST s
-    Type synonyms expanded:
-    Expected type: ST s Int
-      Actual type: ST s Bool
-    In the first argument of ‘runST’, namely ‘barGen’
-    In the second argument of ‘(==)’, namely ‘runST barGen’
+    • Couldn't match type ‘Int’ with ‘Bool’
+      Expected type: ST s Foo
+        Actual type: MyBarST s
+      Type synonyms expanded:
+      Expected type: ST s Int
+        Actual type: ST s Bool
+    • In the first argument of ‘runST’, namely ‘barGen’
+      In the second argument of ‘(==)’, namely ‘runST barGen’
+      In the first argument of ‘print’, namely
+        ‘(runST fooGen == runST barGen)’
diff --git a/testsuite/tests/typecheck/should_fail/T10495.stderr b/testsuite/tests/typecheck/should_fail/T10495.stderr
index ee2060017e..e09e60af23 100644
--- a/testsuite/tests/typecheck/should_fail/T10495.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10495.stderr
@@ -1,7 +1,8 @@
 
-T10495.hs:5:7: error:
-    Couldn't match representation of type ‘a0’ with that of ‘b0’
-      arising from a use of ‘coerce’
-    In the expression: coerce
-    In an equation for ‘foo’: foo = coerce
-    Relevant bindings include foo :: a0 -> b0 (bound at T10495.hs:5:1)
+T10495.hs:5:1: error:
+    • Couldn't match representation of type ‘a0’ with that of ‘b0’
+        arising from a use of ‘coerce’
+    • When instantiating ‘foo’, initially inferred to have
+      this overly-general type:
+        forall a b. Coercible a b => a -> b
+      NB: This instantiation can be caused by the monomorphism restriction.
diff --git a/testsuite/tests/typecheck/should_fail/T10971d.stderr b/testsuite/tests/typecheck/should_fail/T10971d.stderr
index 244fff7098..c5ad886683 100644
--- a/testsuite/tests/typecheck/should_fail/T10971d.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10971d.stderr
@@ -1,17 +1,20 @@
 
 T10971d.hs:4:14: error:
-    Couldn't match expected type ‘[a0]’
-                with actual type ‘Maybe Integer’
-    In the first argument of ‘f’, namely ‘(Just 1)’
-    In the second argument of ‘($)’, namely ‘f (Just 1)’
+    • Couldn't match expected type ‘[a0]’
+                  with actual type ‘Maybe Integer’
+    • In the first argument of ‘f’, namely ‘(Just 1)’
+      In the second argument of ‘($)’, namely ‘f (Just 1)’
+      In a stmt of a 'do' block: print $ f (Just 1)
 
 T10971d.hs:5:19: error:
-    Couldn't match expected type ‘[Integer]’
-                with actual type ‘Maybe Integer’
-    In the second argument of ‘g’, namely ‘(Just 5)’
-    In the second argument of ‘($)’, namely ‘g (+ 1) (Just 5)’
+    • Couldn't match expected type ‘[Integer]’
+                  with actual type ‘Maybe Integer’
+    • In the second argument of ‘g’, namely ‘(Just 5)’
+      In the second argument of ‘($)’, namely ‘g (+ 1) (Just 5)’
+      In a stmt of a 'do' block: print $ g (+ 1) (Just 5)
 
 T10971d.hs:6:23: error:
-    Couldn't match expected type ‘[b0]’ with actual type ‘Maybe a1’
-    In the second argument of ‘h’, namely ‘Nothing’
-    In the second argument of ‘($)’, namely ‘h (const 5) Nothing’
+    • Couldn't match expected type ‘[b0]’ with actual type ‘Maybe a1’
+    • In the second argument of ‘h’, namely ‘Nothing’
+      In the second argument of ‘($)’, namely ‘h (const 5) Nothing’
+      In a stmt of a 'do' block: print $ h (const 5) Nothing
diff --git a/testsuite/tests/typecheck/should_fail/T11274.stderr b/testsuite/tests/typecheck/should_fail/T11274.stderr
index f73131704a..b6f1964c14 100644
--- a/testsuite/tests/typecheck/should_fail/T11274.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11274.stderr
@@ -1,5 +1,5 @@
 
-T11274.hs:10:25: error:
+T11274.hs:10:23: error:
     • No instance for (Eq Asd) arising from a use of ‘==’
     • In the expression: x == y
       In an equation for ‘missingInstance’: missingInstance x y = x == y
diff --git a/testsuite/tests/typecheck/should_fail/T1899.stderr b/testsuite/tests/typecheck/should_fail/T1899.stderr
index 8c2964cfc6..c4db8fe1e7 100644
--- a/testsuite/tests/typecheck/should_fail/T1899.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1899.stderr
@@ -9,6 +9,7 @@ T1899.hs:14:36: error:
         Actual type: [a]
     • In the first argument of ‘Auxiliary’, namely ‘varSet’
       In the first argument of ‘Prop’, namely ‘(Auxiliary varSet)’
+      In the expression: Prop (Auxiliary varSet)
     • Relevant bindings include
         varSet :: [a] (bound at T1899.hs:10:11)
         transRHS :: [a] -> Int -> Constraint a (bound at T1899.hs:10:2)
diff --git a/testsuite/tests/typecheck/should_fail/T2414.stderr b/testsuite/tests/typecheck/should_fail/T2414.stderr
index 0f797da713..bbbf5fce6a 100644
--- a/testsuite/tests/typecheck/should_fail/T2414.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2414.stderr
@@ -1,7 +1,8 @@
 
-T2414.hs:9:13:
-    Occurs check: cannot construct the infinite type: b0 ~ (Bool, b0)
-    Expected type: b0 -> Maybe (Bool, b0)
-      Actual type: (Bool, b0) -> Maybe (Bool, b0)
-    In the first argument of ‘unfoldr’, namely ‘Just’
-    In the expression: unfoldr Just
+T2414.hs:9:13: error:
+    • Occurs check: cannot construct the infinite type: b0 ~ (Bool, b0)
+      Expected type: b0 -> Maybe (Bool, b0)
+        Actual type: (Bool, b0) -> Maybe (Bool, b0)
+    • In the first argument of ‘unfoldr’, namely ‘Just’
+      In the expression: unfoldr Just
+      In an equation for ‘f’: f = unfoldr Just
diff --git a/testsuite/tests/typecheck/should_fail/T2534.stderr b/testsuite/tests/typecheck/should_fail/T2534.stderr
index fe6abae7b8..4e469f3cfd 100644
--- a/testsuite/tests/typecheck/should_fail/T2534.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2534.stderr
@@ -1,8 +1,9 @@
 
-T2534.hs:3:13:
-    Couldn't match type ‘[b]’ with ‘a0 -> [b]’
-    Expected type: [a0] -> [b] -> [b]
-      Actual type: [a0] -> (a0 -> [b]) -> [b]
-    In the first argument of ‘foldr’, namely ‘(>>=)’
-    In the expression: foldr (>>=) [] []
-    Relevant bindings include foo :: [b] (bound at T2534.hs:3:1)
+T2534.hs:3:13: error:
+    • Couldn't match type ‘[b]’ with ‘a0 -> [b]’
+      Expected type: [a0] -> [b] -> [b]
+        Actual type: [a0] -> (a0 -> [b]) -> [b]
+    • In the first argument of ‘foldr’, namely ‘(>>=)’
+      In the expression: foldr (>>=) [] []
+      In an equation for ‘foo’: foo = foldr (>>=) [] []
+    • Relevant bindings include foo :: [b] (bound at T2534.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/T2688.stderr b/testsuite/tests/typecheck/should_fail/T2688.stderr
index 1915c41812..2b2ca0d22a 100644
--- a/testsuite/tests/typecheck/should_fail/T2688.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2688.stderr
@@ -1,13 +1,13 @@
 
-T2688.hs:8:22:
-    Couldn't match expected type ‘v’ with actual type ‘s’
+T2688.hs:8:14: error:
+    • Couldn't match expected type ‘v’ with actual type ‘s’
       ‘s’ is a rigid type variable bound by
-          the class declaration for ‘VectorSpace’ at T2688.hs:5:21
+        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
-    In the second argument of ‘(/)’, namely ‘s’
-    In the second argument of ‘(*^)’, namely ‘(1 / s)’
-    Relevant bindings include
-      s :: s (bound at T2688.hs:8:10)
-      v :: v (bound at T2688.hs:8:5)
-      (^/) :: v -> s -> v (bound at T2688.hs:8:5)
+        the class declaration for ‘VectorSpace’ at T2688.hs:5:19
+    • In the expression: v *^ (1 / s)
+      In an equation for ‘^/’: v ^/ s = v *^ (1 / s)
+    • Relevant bindings include
+        s :: s (bound at T2688.hs:8:10)
+        v :: v (bound at T2688.hs:8:5)
+        (^/) :: v -> s -> v (bound at T2688.hs:8:5)
diff --git a/testsuite/tests/typecheck/should_fail/T2846b.stderr b/testsuite/tests/typecheck/should_fail/T2846b.stderr
index 0323283477..371d0ce5ca 100644
--- a/testsuite/tests/typecheck/should_fail/T2846b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2846b.stderr
@@ -1,6 +1,6 @@
 
 T2846b.hs:5:5: error:
-    No instance for (Show (Num a0 => a0)) arising from a use of ‘show’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: show ([1, 2, 3] :: [Num a => a])
-    In an equation for ‘f’: f = show ([1, 2, 3] :: [Num a => a])
+    • No instance for (Show (forall a. [Num a => a]))
+        arising from a use of ‘show’
+    • In the expression: show ([1, 2, 3] :: [Num a => a])
+      In an equation for ‘f’: f = show ([1, 2, 3] :: [Num a => a])
diff --git a/testsuite/tests/typecheck/should_fail/T3102.stderr b/testsuite/tests/typecheck/should_fail/T3102.stderr
index 925e80f7fc..a5a410efeb 100644
--- a/testsuite/tests/typecheck/should_fail/T3102.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3102.stderr
@@ -1,11 +1,12 @@
-
-T3102.hs:11:12: error:
-    Couldn't match type ‘a’ with ‘(?p::Int) => a0’
-    ‘a’ is a rigid type variable bound by
-    a type expected by the context:
-      forall a. a -> String
-    at T3102.hs:11:10
-    Expected type: a -> String
-      Actual type: ((?p::Int) => a0) -> String
-    In the first argument of ‘f’, namely ‘t’
-    In the expression: f t
+
+T3102.hs:11:12: error:
+    • Couldn't match type ‘a’ with ‘(?p::Int) => a0’
+      ‘a’ is a rigid type variable bound by
+        a type expected by the context:
+          forall a. a -> String
+        at T3102.hs:11:10
+      Expected type: a -> String
+        Actual type: ((?p::Int) => a0) -> String
+    • In the first argument of ‘f’, namely ‘t’
+      In the expression: f t
+      In an equation for ‘result’: result = f t
diff --git a/testsuite/tests/typecheck/should_fail/T3613.stderr b/testsuite/tests/typecheck/should_fail/T3613.stderr
index f7fa6d4871..b7ffd671c8 100644
--- a/testsuite/tests/typecheck/should_fail/T3613.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3613.stderr
@@ -1,14 +1,20 @@
 
-T3613.hs:14:20:
-    Couldn't match type ‘IO’ with ‘Maybe’
-    Expected type: Maybe ()
-      Actual type: IO ()
-    In the first argument of ‘(>>)’, namely ‘bar’
-    In the first argument of ‘fooThen’, namely ‘(bar >> undefined)’
+T3613.hs:14:20: error:
+    • Couldn't match type ‘IO’ with ‘Maybe’
+      Expected type: Maybe b
+        Actual type: IO b
+    • In the first argument of ‘fooThen’, namely ‘(bar >> undefined)’
+      In the expression: fooThen (bar >> undefined)
+      In the expression:
+        let fooThen m = foo >> m in fooThen (bar >> undefined)
 
-T3613.hs:17:24:
-    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;
-             undefined })’
+T3613.hs:17:24: error:
+    • 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;
+               undefined })’
+      In the expression:
+        fooThen
+          (do { bar;
+                undefined })
diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr
index fab70fd01b..ae50a74f3c 100644
--- a/testsuite/tests/typecheck/should_fail/T3950.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3950.stderr
@@ -1,12 +1,17 @@
 
-T3950.hs:15:13: error:
+T3950.hs:15:8: error:
     • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
         w :: (* -> * -> *) -> *
         Sealed :: (* -> *) -> *
-      Expected type: w (Id p)
-      Actual type: Sealed (Id p x0)
-    • In the first argument of ‘Just’, namely ‘rp'’
-      In the expression: Just rp'
+      Expected type: Maybe (w (Id p))
+        Actual type: Maybe (Sealed (Id p x0))
+    • In the expression: Just rp'
+      In an equation for ‘rp’:
+          rp _
+            = Just rp'
+            where
+                rp' :: Sealed (Id p x)
+                rp' = undefined
     • Relevant bindings include
         rp :: Bool -> Maybe (w (Id p)) (bound at T3950.hs:15:1)
diff --git a/testsuite/tests/typecheck/should_fail/T5095.stderr b/testsuite/tests/typecheck/should_fail/T5095.stderr
index cc338e7afa..c284cda9d0 100644
--- a/testsuite/tests/typecheck/should_fail/T5095.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5095.stderr
@@ -1,5 +1,5 @@
 
-T5095.hs:9:11: error:
+T5095.hs:9:9: error:
     • Overlapping instances for Eq a arising from a use of ‘==’
       Matching instances:
         instance [overlappable] Show a => Eq a -- Defined at T5095.hs:5:31
diff --git a/testsuite/tests/typecheck/should_fail/T5689.stderr b/testsuite/tests/typecheck/should_fail/T5689.stderr
index 6e3777d2ee..2c7eaa87d4 100644
--- a/testsuite/tests/typecheck/should_fail/T5689.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5689.stderr
@@ -1,8 +1,10 @@
 
 T5689.hs:10:36: error:
-    Couldn't match expected type ‘Bool’ with actual type ‘t’
-    In the expression: v
-    In the expression: if v then False else True
-    Relevant bindings include
-      v :: t (bound at T5689.hs:10:28)
-      r :: IORef (t -> t) (bound at T5689.hs:7:14)
+    • Couldn't match expected type ‘Bool’ with actual type ‘t’
+    • In the expression: v
+      In the expression: if v then False else True
+      In the second argument of ‘writeIORef’, namely
+        ‘(\ v -> if v then False else True)’
+    • Relevant bindings include
+        v :: t (bound at T5689.hs:10:28)
+        r :: IORef (t -> t) (bound at T5689.hs:7:14)
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index 33ae4e16ce..ab2ad30d6c 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,5 +1,5 @@
 
-T5853.hs:15:52: error:
+T5853.hs:15:46: error:
     • Could not deduce: Subst t2 (Elem t1) ~ t1
         arising from a use of ‘<$>’
       from the context: (F t,
diff --git a/testsuite/tests/typecheck/should_fail/T6069.stderr b/testsuite/tests/typecheck/should_fail/T6069.stderr
index eff2e8b5cf..e1c2e5653f 100644
--- a/testsuite/tests/typecheck/should_fail/T6069.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6069.stderr
@@ -1,21 +1,24 @@
 
-T6069.hs:13:15:
-    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:13:15: error:
+    • 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
+      In the expression: (print . runST) fourty_two
 
-T6069.hs:14:15:
-    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:14:15: error:
+    • 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)
+      In the expression: (print . runST) $ fourty_two
 
-T6069.hs:15:16:
-    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)’
+T6069.hs:15:16: error:
+    • 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)’
+      In the expression: (print . runST) $
diff --git a/testsuite/tests/typecheck/should_fail/T7264.stderr b/testsuite/tests/typecheck/should_fail/T7264.stderr
index 4b5b3557d9..b343d88cd1 100644
--- a/testsuite/tests/typecheck/should_fail/T7264.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7264.stderr
@@ -1,12 +1,13 @@
 
-T7264.hs:13:19:
-    Couldn't match type ‘a’ with ‘forall r. r -> String’
+T7264.hs:13:19: error:
+    • Couldn't match type ‘a’ with ‘forall r. r -> String’
       ‘a’ is a rigid type variable bound by
-          the inferred type of mkFoo2 :: a -> Maybe Foo at T7264.hs:13:1
-    Expected type: a -> Foo
-      Actual type: (forall r. r -> String) -> Foo
-    In the first argument of ‘mmap’, namely ‘Foo’
-    In the expression: mmap Foo (Just val)
-    Relevant bindings include
-      val :: a (bound at T7264.hs:13:8)
-      mkFoo2 :: a -> Maybe Foo (bound at T7264.hs:13:1)
+        the inferred type of mkFoo2 :: a -> Maybe Foo at T7264.hs:13:1
+      Expected type: a -> Foo
+        Actual type: (forall r. r -> String) -> Foo
+    • In the first argument of ‘mmap’, namely ‘Foo’
+      In the expression: mmap Foo (Just val)
+      In an equation for ‘mkFoo2’: mkFoo2 val = mmap Foo (Just val)
+    • Relevant bindings include
+        val :: a (bound at T7264.hs:13:8)
+        mkFoo2 :: a -> Maybe Foo (bound at T7264.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr
index 1c538ac7f9..f187aee61c 100644
--- a/testsuite/tests/typecheck/should_fail/T7368.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368.stderr
@@ -4,3 +4,4 @@ T7368.hs:3:10: error:
       When matching the kind of ‘Maybe’
     • In the first argument of ‘b’, namely ‘(l Nothing)’
       In the expression: b (l Nothing)
+      In an equation for ‘f’: f = b (l Nothing)
diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr
index efbc7497e5..47bfa78754 100644
--- a/testsuite/tests/typecheck/should_fail/T7453.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7453.stderr
@@ -13,6 +13,14 @@ T7453.hs:9:15: error:
           z = aux
             where
                 aux = Id v
+      In an equation for ‘cast1’:
+          cast1 v
+            = runId z
+            where
+                z :: Id t
+                z = aux
+                  where
+                      aux = Id v
     • Relevant bindings include
         aux :: Id r (bound at T7453.hs:10:21)
         z :: Id t (bound at T7453.hs:9:11)
@@ -33,6 +41,14 @@ T7453.hs:15:15: error:
           z = aux
             where
                 aux = const v
+      In an equation for ‘cast2’:
+          cast2 v
+            = z ()
+            where
+                z :: () -> t
+                z = aux
+                  where
+                      aux = const v
     • Relevant bindings include
         aux :: forall b. b -> r (bound at T7453.hs:16:21)
         z :: () -> t1 (bound at T7453.hs:15:11)
@@ -51,8 +67,16 @@ T7453.hs:21:15: error:
           z = v
             where
                 aux = const v
+      In an equation for ‘cast3’:
+          cast3 v
+            = z
+            where
+                z :: t
+                z = v
+                  where
+                      aux = const v
     • Relevant bindings include
         aux :: forall b. b -> r (bound at T7453.hs:22:21)
         z :: t1 (bound at T7453.hs:21:11)
         v :: r (bound at T7453.hs:19:7)
-        cast3 :: r -> t (bound at T7453.hs:19:1)
+        cast3 :: r -> forall t. t (bound at T7453.hs:19:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7734.stderr b/testsuite/tests/typecheck/should_fail/T7734.stderr
index d4efb614df..53536d1a13 100644
--- a/testsuite/tests/typecheck/should_fail/T7734.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7734.stderr
@@ -3,6 +3,7 @@ T7734.hs:4:13: error:
     • Occurs check: cannot construct the infinite type: r2 ~ r2 -> r1
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
+      In an equation for ‘f’: x `f` y = x x
     • Relevant bindings include
         x :: r2 -> r1 (bound at T7734.hs:4:1)
         f :: (r2 -> r1) -> r -> r1 (bound at T7734.hs:4:1)
@@ -11,6 +12,7 @@ T7734.hs:5:13: error:
     • Occurs check: cannot construct the infinite type: r2 ~ r2 -> r1
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
+      In an equation for ‘&’: (&) x y = x x
     • Relevant bindings include
         x :: r2 -> r1 (bound at T7734.hs:5:5)
         (&) :: (r2 -> r1) -> r -> r1 (bound at T7734.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7851.stderr b/testsuite/tests/typecheck/should_fail/T7851.stderr
index 64148511e7..14efa7c7c9 100644
--- a/testsuite/tests/typecheck/should_fail/T7851.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7851.stderr
@@ -1,8 +1,13 @@
 
-T7851.hs:5:10:
-    Couldn't match expected type ‘IO a0’ with actual type ‘a1 -> IO ()’
-    Probable cause: ‘print’ is applied to too few arguments
-    In a stmt of a 'do' block: print
-    In the expression:
-      do { print;
-           print "Hello" }
+T7851.hs:5:10: error:
+    • Couldn't match expected type ‘IO a0’
+                  with actual type ‘a1 -> IO ()’
+    • Probable cause: ‘print’ is applied to too few arguments
+      In a stmt of a 'do' block: print
+      In the expression:
+        do { print;
+             print "Hello" }
+      In an equation for ‘bar’:
+          bar
+            = do { print;
+                   print "Hello" }
diff --git a/testsuite/tests/typecheck/should_fail/T8142.stderr b/testsuite/tests/typecheck/should_fail/T8142.stderr
index 9ae86c5524..09a2a9677d 100644
--- a/testsuite/tests/typecheck/should_fail/T8142.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8142.stderr
@@ -1,25 +1,26 @@
 
 T8142.hs:6:18: error:
-    Couldn't match type ‘Nu g0’ with ‘Nu g’
-    NB: ‘Nu’ is a type function, and may not be injective
-    The type variable ‘g0’ is ambiguous
-    Expected type: Nu ((,) t) -> Nu g
-      Actual type: Nu ((,) t0) -> Nu g0
-    In the ambiguity check for the inferred type for ‘h’
-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-    When checking the inferred type
-      h :: forall t (g :: * -> *). Nu ((,) t) -> Nu g
-    In an equation for ‘tracer’:
-        tracer
-          = h
-          where
-              h = (\ (_, b) -> ((outI . fmap h) b)) . out
+    • Couldn't match type ‘Nu g0’ with ‘Nu g’
+      NB: ‘Nu’ is a type function, and may not be injective
+      The type variable ‘g0’ is ambiguous
+      Expected type: Nu ((,) t) -> Nu g
+        Actual type: Nu ((,) t0) -> Nu g0
+    • In the ambiguity check for the inferred type for ‘h’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the inferred type
+        h :: forall t (g :: * -> *). Nu ((,) t) -> Nu g
+      In an equation for ‘tracer’:
+          tracer
+            = h
+            where
+                h = (\ (_, b) -> ((outI . fmap h) b)) . out
 
 T8142.hs:6:57: error:
-    Couldn't match type ‘Nu ((,) t)’ with ‘g (Nu ((,) t))’
-    Expected type: Nu ((,) t) -> (t, g (Nu ((,) t)))
-      Actual type: Nu ((,) t) -> (t, Nu ((,) t))
-    In the second argument of ‘(.)’, namely ‘out’
-    In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
-    Relevant bindings include
-      h :: Nu ((,) t) -> Nu g (bound at T8142.hs:6:18)
+    • Couldn't match type ‘Nu ((,) t)’ with ‘g (Nu ((,) t))’
+      Expected type: Nu ((,) t) -> (t, g (Nu ((,) t)))
+        Actual type: Nu ((,) t) -> (t, Nu ((,) t))
+    • In the second argument of ‘(.)’, namely ‘out’
+      In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
+      In an equation for ‘h’: h = (\ (_, b) -> ((outI . fmap h) b)) . out
+    • Relevant bindings include
+        h :: Nu ((,) t) -> Nu g (bound at T8142.hs:6:18)
diff --git a/testsuite/tests/typecheck/should_fail/T8428.stderr b/testsuite/tests/typecheck/should_fail/T8428.stderr
index cb4724331c..97cd9f7806 100644
--- a/testsuite/tests/typecheck/should_fail/T8428.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8428.stderr
@@ -1,10 +1,8 @@
 
-T8428.hs:11:19:
-    Couldn't match type ‘(forall s. ST s) a’ with ‘forall s. ST s a’
-    Expected type: IdentityT (forall s. ST s) a -> forall s. ST s a
-      Actual type: IdentityT (forall s. ST s) a -> (forall s. ST s) a
-    In the second argument of ‘(.)’, namely ‘runIdentityT’
-    In the expression: runST . runIdentityT
-    Relevant bindings include
-      runIdST :: IdentityT (forall s. ST s) a -> a
-        (bound at T8428.hs:11:1)
+T8428.hs:11:19: error:
+    • Couldn't match type ‘forall s1. ST s1’ with ‘ST s’
+      Expected type: IdentityT (forall s. ST s) a -> forall s. ST s a
+        Actual type: IdentityT (forall s. ST s) a -> (forall s. ST s) a
+    • In the second argument of ‘(.)’, namely ‘runIdentityT’
+      In the expression: runST . runIdentityT
+      In an equation for ‘runIdST’: runIdST = runST . runIdentityT
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index 5bfd397167..53d4e422cb 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -5,22 +5,15 @@ T8603.hs:13:10: error:
     • In the instance declaration for ‘Monad RV’
 
 T8603.hs:29:17: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching the kind of ‘[[a0]]’
+    • Couldn't match type ‘RV a0’ with ‘StateT s RV t0’
+      Expected type: [Integer] -> StateT s RV t0
+        Actual type: (->) ((->) [a0]) (RV a0)
     • The function ‘lift’ is applied to two arguments,
-      but its type ‘[] [a0] (StateT s RV t0)
-                    -> (->) [[a0]] (StateT s RV t0)’
+      but its type ‘([a0] -> RV a0) -> (->) ((->) [a0]) (RV a0)’
       has only one
       In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
       In the expression:
         do { prize <- lift uniform [1, 2, ....];
              return False }
-
-T8603.hs:29:22: error:
-    • Couldn't match type ‘RV a0’ with ‘StateT s RV t0’
-      Expected type: [] [a0] (StateT s RV t0)
-        Actual type: [a0] -> RV a0
-    • In the first argument of ‘lift’, namely ‘uniform’
-      In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
     • Relevant bindings include
         testRVState1 :: RVState s Bool (bound at T8603.hs:28:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9109.stderr b/testsuite/tests/typecheck/should_fail/T9109.stderr
index defd77572e..f13b0fc310 100644
--- a/testsuite/tests/typecheck/should_fail/T9109.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9109.stderr
@@ -2,14 +2,13 @@
 T9109.hs:8:13: error:
     • Couldn't match expected type ‘r’ with actual type ‘Bool’
         ‘r’ is untouchable
-          inside the constraints: r1 ~ Bool
+          inside the constraints: t ~ Bool
           bound by a pattern with constructor: GBool :: G Bool,
                    in an equation for ‘foo’
           at T9109.hs:8:5-9
       ‘r’ is a rigid type variable bound by
-        the inferred type of foo :: G r1 -> r at T9109.hs:8:1
+        the inferred type of foo :: G t -> r at T9109.hs:8:1
       Possible fix: add a type signature for ‘foo’
     • In the expression: True
       In an equation for ‘foo’: foo GBool = True
-    • Relevant bindings include
-        foo :: G r1 -> r (bound at T9109.hs:8:1)
+    • Relevant bindings include foo :: G t -> r (bound at T9109.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9774.stderr b/testsuite/tests/typecheck/should_fail/T9774.stderr
index d75942bc59..28b1b58c4c 100644
--- a/testsuite/tests/typecheck/should_fail/T9774.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9774.stderr
@@ -1,8 +1,8 @@
 
-T9774.hs:5:29:
-    Couldn't match type ‘Char’ with ‘[Char]’
-    Expected type: String
-      Actual type: Char
-    In the second argument of ‘assert’, namely ‘'a'’
-    In the first argument of ‘putStrLn’, namely ‘(assert True 'a')’
-    In the expression: putStrLn (assert True 'a')
+T9774.hs:5:17: error:
+    • Couldn't match type ‘Char’ with ‘[Char]’
+      Expected type: String
+        Actual type: Char
+    • In the first argument of ‘putStrLn’, namely ‘(assert True 'a')’
+      In the expression: putStrLn (assert True 'a')
+      In an equation for ‘foo’: foo = putStrLn (assert True 'a')
diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
index 1767e8e976..32dac6a133 100644
--- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
@@ -2,8 +2,7 @@
 TcCoercibleFail.hs:11:8: error:
     • Couldn't match representation of type ‘Int’ with that of ‘()’
         arising from a use of ‘coerce’
-    • In the expression: coerce
-      In the expression: coerce $ one :: ()
+    • In the expression: coerce $ one :: ()
       In an equation for ‘foo1’: foo1 = coerce $ one :: ()
 
 TcCoercibleFail.hs:14:8: error:
@@ -12,8 +11,7 @@ TcCoercibleFail.hs:14:8: error:
         arising from a use of ‘coerce’
       NB: We cannot know what roles the parameters to ‘m’ have;
         we must assume that the role is nominal
-    • In the expression: coerce
-      In the expression: coerce $ (return one :: m Int)
+    • In the expression: coerce $ (return one :: m Int)
       In an equation for ‘foo2’: foo2 = coerce $ (return one :: m Int)
     • Relevant bindings include
         foo2 :: m Age (bound at TcCoercibleFail.hs:14:1)
@@ -21,8 +19,7 @@ TcCoercibleFail.hs:14:8: error:
 TcCoercibleFail.hs:16:8: error:
     • Couldn't match type ‘Int’ with ‘Age’
         arising from a use of ‘coerce’
-    • In the expression: coerce
-      In the expression: coerce $ Map one () :: Map Age ()
+    • In the expression: coerce $ Map one () :: Map Age ()
       In an equation for ‘foo3’: foo3 = coerce $ Map one () :: Map Age ()
 
 TcCoercibleFail.hs:18:8: error:
@@ -31,8 +28,7 @@ TcCoercibleFail.hs:18:8: error:
         arising from a use of ‘coerce’
       The data constructor ‘Data.Ord.Down’
         of newtype ‘Down’ is not in scope
-    • In the expression: coerce
-      In the expression: coerce $ one :: Down Int
+    • In the expression: coerce $ one :: Down Int
       In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int
 
 TcCoercibleFail.hs:21:8: error:
diff --git a/testsuite/tests/typecheck/should_fail/TcStaticPointersFail01.stderr b/testsuite/tests/typecheck/should_fail/TcStaticPointersFail01.stderr
index e41ec7443d..9b85edb110 100644
--- a/testsuite/tests/typecheck/should_fail/TcStaticPointersFail01.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcStaticPointersFail01.stderr
@@ -1,6 +1,7 @@
 
-TcStaticPointersFail01.hs:8:13:
-    Couldn't match expected type ‘Int’ with actual type ‘Int -> Int’
-    Probable cause: ‘g’ is applied to too few arguments
-    In the body of a static form: g
-    In the expression: static g
+TcStaticPointersFail01.hs:8:13: error:
+    • Couldn't match expected type ‘Int’ with actual type ‘Int -> Int’
+    • Probable cause: ‘g’ is applied to too few arguments
+      In the body of a static form: g
+      In the expression: static g
+      In an equation for ‘f0’: f0 = static g
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.hs b/testsuite/tests/typecheck/should_fail/VtaFail.hs
new file mode 100644
index 0000000000..250f9e273e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE TypeApplications, RankNTypes, PolyKinds #-}
+
+module VtaFail1 where
+
+pairup_nosig x y = (x, y)
+
+answer_nosig = pairup_nosig @Int @Bool 5 True
+
+addOne :: Num a => a -> a
+addOne x = x + 1
+
+answer_constraint_fail = addOne @Bool 5
+
+answer_lambda = (\x -> x) @Int 12
+
+pair :: forall a. a -> forall b. b -> (a, b)
+pair = (,)
+
+a = pair 3 @Int @Bool True
+
+data First (a :: * -> *) = F
+
+first :: First a -> Int
+first _ = 0
+
+fInt = first @Int F -- should fail
+
+data Proxy (a :: k) = P -- This expands to P (kind variable) (type variable)
+
+foo :: Proxy a -> Int
+foo _ = 0
+
+baz = foo @Bool (P :: Proxy Int) -- should fail
+
+data Three (a :: * -> k -> *) = T
+
+too :: Three a -> Int
+too _ = 3
+
+threeBad = too @Maybe T
+threeWorse = too @( -> ) (T :: Three Either)
+
+plus :: Int -> Int -> Int
+plus = (+)
+
+b = plus @Int 5 7
+c = plus @Rational 5 10
+d = (+) @Int @Int @Int 12 14
+
+
+e = show @Int @Float (read "5")
+f = show (read @Int @Bool @Float "3")
+
+silly :: a -> Bool
+silly _ = False
+
+g = silly @Maybe      -- should fail
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
new file mode 100644
index 0000000000..313d174b74
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -0,0 +1,94 @@
+
+VtaFail.hs:7:16: error:
+    • Cannot not apply expression of type ‘t1 -> t0 -> (t1, t0)’
+      to a visible type argument ‘Int’
+    • In the expression: pairup_nosig @Int @Bool 5 True
+      In an equation for ‘answer_nosig’:
+          answer_nosig = pairup_nosig @Int @Bool 5 True
+
+VtaFail.hs:12:26: error:
+    • No instance for (Num Bool) arising from a use of ‘addOne’
+    • In the expression: addOne @Bool 5
+      In an equation for ‘answer_constraint_fail’:
+          answer_constraint_fail = addOne @Bool 5
+
+VtaFail.hs:14:17: error:
+    • Cannot not apply expression of type ‘r0 -> r0’
+      to a visible type argument ‘Int’
+    • In the expression: (\ x -> x) @Int 12
+      In an equation for ‘answer_lambda’:
+          answer_lambda = (\ x -> x) @Int 12
+
+VtaFail.hs:19:5: error:
+    • Cannot not apply expression of type ‘Int -> (a0, Int)’
+      to a visible type argument ‘Bool’
+    • In the expression: pair 3 @Int @Bool True
+      In an equation for ‘a’: a = pair 3 @Int @Bool True
+
+VtaFail.hs:26:15: error:
+    • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
+    • In the type ‘Int’
+      In the expression: first @Int F
+      In an equation for ‘fInt’: fInt = first @Int F
+
+VtaFail.hs:33:18: error:
+    • Couldn't match type ‘Int’ with ‘Bool’
+      Expected type: Proxy Bool
+        Actual type: Proxy Int
+    • In the second argument of ‘foo’, namely ‘(P :: Proxy Int)’
+      In the expression: foo @Bool (P :: Proxy Int)
+      In an equation for ‘baz’: baz = foo @Bool (P :: Proxy Int)
+
+VtaFail.hs:40:17: error:
+    • Expected kind ‘* -> k0 -> *’, but ‘Maybe’ has kind ‘* -> *’
+    • In the type ‘Maybe’
+      In the expression: too @Maybe T
+      In an equation for ‘threeBad’: threeBad = too @Maybe T
+
+VtaFail.hs:41:27: error:
+    • Couldn't match type ‘Either’ with ‘(->)’
+      Expected type: Three (->)
+        Actual type: Three Either
+    • In the second argument of ‘too’, namely ‘(T :: Three Either)’
+      In the expression: too @(->) (T :: Three Either)
+      In an equation for ‘threeWorse’:
+          threeWorse = too @(->) (T :: Three Either)
+
+VtaFail.hs:46:5: error:
+    • Cannot not apply expression of type ‘Int -> Int -> Int’
+      to a visible type argument ‘Int’
+    • In the expression: plus @Int 5 7
+      In an equation for ‘b’: b = plus @Int 5 7
+
+VtaFail.hs:47:5: error:
+    • Cannot not apply expression of type ‘Int -> Int -> Int’
+      to a visible type argument ‘Rational’
+    • In the expression: plus @Rational 5 10
+      In an equation for ‘c’: c = plus @Rational 5 10
+
+VtaFail.hs:48:5: error:
+    • Cannot not apply expression of type ‘Int -> Int -> Int’
+      to a visible type argument ‘Int’
+    • In the expression: (+) @Int @Int @Int 12 14
+      In an equation for ‘d’: d = (+) @Int @Int @Int 12 14
+
+VtaFail.hs:51:5: error:
+    • Cannot not apply expression of type ‘Int -> String’
+      to a visible type argument ‘Float’
+    • In the expression: show @Int @Float (read "5")
+      In an equation for ‘e’: e = show @Int @Float (read "5")
+
+VtaFail.hs:52:11: error:
+    • Cannot not apply expression of type ‘String -> Int’
+      to a visible type argument ‘Bool’
+    • In the first argument of ‘show’, namely
+        ‘(read @Int @Bool @Float "3")’
+      In the expression: show (read @Int @Bool @Float "3")
+      In an equation for ‘f’: f = show (read @Int @Bool @Float "3")
+
+VtaFail.hs:57:12: error:
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the type ‘Maybe’
+      In the expression: silly @Maybe
+      In an equation for ‘g’: g = silly @Maybe
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 8d8d4306e7..aa43cce226 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -147,7 +147,7 @@ test('tcfail160', normal, compile_fail, [''])
 test('tcfail161', normal, compile_fail, [''])
 test('tcfail162', normal, compile_fail, [''])
 test('tcfail164', normal, compile_fail, [''])
-test('tcfail165', normal, compile_fail, [''])
+test('tcfail165', normal, compile, [''])
 test('tcfail166', normal, compile_fail, [''])
 test('tcfail167', normal, compile_fail, [''])
 test('tcfail168', normal, compile_fail, [''])
@@ -379,6 +379,7 @@ test('T10351', normal, compile_fail, [''])
 test('T10534', extra_clean(['T10534a.hi', 'T10534a.o']),
      multimod_compile_fail, ['T10534', '-v0'])
 test('T10495', normal, compile_fail, [''])
+test('VtaFail', normal, compile_fail, [''])
 
 test('ExpandSynsFail1', normal, compile_fail, ['-fprint-expanded-synonyms'])
 test('ExpandSynsFail2', normal, compile_fail, ['-fprint-expanded-synonyms'])
diff --git a/testsuite/tests/typecheck/should_fail/mc19.stderr b/testsuite/tests/typecheck/should_fail/mc19.stderr
index 8cdd4f456b..5f004dc4a8 100644
--- a/testsuite/tests/typecheck/should_fail/mc19.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc19.stderr
@@ -1,11 +1,12 @@
-
-mc19.hs:10:31: error:
-    Couldn't match type ‘a’ with ‘[a]’
-    ‘a’ is a rigid type variable bound by
-    a type expected by the context:
-      forall a. [a] -> [a]
-    at mc19.hs:10:10
-    Expected type: [a] -> [a]
-      Actual type: [a] -> [[a]]
-    In the expression: inits
-    In a stmt of a monad comprehension: then inits
+
+mc19.hs:10:31: error:
+    • Couldn't match type ‘a’ with ‘[a]’
+      ‘a’ is a rigid type variable bound by
+        a type expected by the context:
+          forall a. [a] -> [a]
+        at mc19.hs:10:10
+      Expected type: [a] -> [a]
+        Actual type: [a] -> [[a]]
+    • In the expression: inits
+      In a stmt of a monad comprehension: then inits
+      In the expression: [x | x <- [3, 2, 1], then inits]
diff --git a/testsuite/tests/typecheck/should_fail/mc21.stderr b/testsuite/tests/typecheck/should_fail/mc21.stderr
index 3017d2221c..74a13b14bc 100644
--- a/testsuite/tests/typecheck/should_fail/mc21.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc21.stderr
@@ -1,11 +1,13 @@
-
-mc21.hs:12:26: error:
-    Couldn't match type ‘a’ with ‘[a]’
-    ‘a’ is a rigid type variable bound by
-    a type expected by the context:
-      forall a. [a] -> [[a]]
-    at mc21.hs:11: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: error:
+    • Couldn't match type ‘a’ with ‘[a]’
+      ‘a’ is a rigid type variable bound by
+        a type expected by the context:
+          forall a. [a] -> [[a]]
+        at mc21.hs:11: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
+      In the expression:
+        [GHC.List.length x | x <- [Gnorf, Brain], then group using take 5]
diff --git a/testsuite/tests/typecheck/should_fail/mc22.stderr b/testsuite/tests/typecheck/should_fail/mc22.stderr
index 1c6dc386dd..5e369d7ffe 100644
--- a/testsuite/tests/typecheck/should_fail/mc22.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc22.stderr
@@ -1,24 +1,27 @@
-
-mc22.hs:9:9: error:
-    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: error:
-    Couldn't match type ‘a’ with ‘t a’
-    ‘a’ is a rigid type variable bound by
-    a type expected by the context:
-      forall a. [a] -> [t a]
-    at mc22.hs:9:9
-    Expected type: [a] -> [t a]
-      Actual type: [t a] -> [t a]
-    In the expression: take 5
-    In a stmt of a monad comprehension: then group using take 5
-    Relevant bindings include foo :: [t [Char]] (bound at mc22.hs:8:1)
+
+mc22.hs:9:9: error:
+    • 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: error:
+    • Couldn't match type ‘a’ with ‘t a’
+      ‘a’ is a rigid type variable bound by
+        a type expected by the context:
+          forall a. [a] -> [t a]
+        at mc22.hs:9:9
+      Expected type: [a] -> [t a]
+        Actual type: [t a] -> [t a]
+    • In the expression: take 5
+      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]
+    • Relevant bindings include
+        foo :: [t [Char]] (bound at mc22.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/mc23.stderr b/testsuite/tests/typecheck/should_fail/mc23.stderr
index 945d1a6db8..2f3ae27a98 100644
--- a/testsuite/tests/typecheck/should_fail/mc23.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc23.stderr
@@ -1,9 +1,10 @@
 
-mc23.hs:9:29:
-    Couldn't match type ‘[a0]’ with ‘[a] -> m a’
-    Expected type: (a -> b) -> [a] -> m a
-      Actual type: [a0] -> [a0]
-    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
-    Relevant bindings include z :: m b (bound at mc23.hs:9:1)
+mc23.hs:9:29: error:
+    • Couldn't match type ‘[a0]’ with ‘[a] -> m a’
+      Expected type: (a -> b) -> [a] -> m a
+        Actual type: [a0] -> [a0]
+    • 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
+      In the expression: [x | x <- [1 .. 10], then take 5 by x]
+    • Relevant bindings include z :: m b (bound at mc23.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/mc24.stderr b/testsuite/tests/typecheck/should_fail/mc24.stderr
index b14fd81162..7f016283b1 100644
--- a/testsuite/tests/typecheck/should_fail/mc24.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc24.stderr
@@ -1,9 +1,11 @@
 
-mc24.hs:10:31:
-    Couldn't match type ‘[a0]’ with ‘[a] -> m [a]’
-    Expected type: (a -> Integer) -> [a] -> m [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
-    Relevant bindings include foo :: m Int (bound at mc24.hs:8:1)
+mc24.hs:10:31: error:
+    • Couldn't match type ‘[a0]’ with ‘[a] -> m [a]’
+      Expected type: (a -> Integer) -> [a] -> m [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
+      In the expression:
+        [GHC.List.length x | x <- [1 .. 10], then group by x using take 2]
+    • Relevant bindings include foo :: m Int (bound at mc24.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/mc25.stderr b/testsuite/tests/typecheck/should_fail/mc25.stderr
index 0989dbcf70..406f89e719 100644
--- a/testsuite/tests/typecheck/should_fail/mc25.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc25.stderr
@@ -1,18 +1,20 @@
 
 mc25.hs:9:10: error:
-    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]
+    • 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: error:
-    Couldn't match type ‘a -> t’ with ‘Int’
-    Expected type: (a -> t) -> [a] -> [t1 a]
-      Actual type: Int -> [t1 a] -> [t1 a]
-    In the expression: take
-    In a stmt of a monad comprehension: then group by x using take
-    Relevant bindings include z :: [t1 t] (bound at mc25.hs:9:1)
+    • Couldn't match type ‘a -> t’ with ‘Int’
+      Expected type: (a -> t) -> [a] -> [t1 a]
+        Actual type: Int -> [t1 a] -> [t1 a]
+    • In the expression: take
+      In a stmt of a monad comprehension: then group by x using take
+      In the expression: [x | x <- [1 .. 10], then group by x using take]
+    • Relevant bindings include z :: [t1 t] (bound at mc25.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail001.stderr b/testsuite/tests/typecheck/should_fail/tcfail001.stderr
index b30d995455..0b0a799c04 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail001.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail001.stderr
@@ -1,7 +1,8 @@
 
-tcfail001.hs:9:2:
-    Couldn't match expected type ‘[t0] -> [t1]’ with actual type ‘[a]’
-    The equation(s) for ‘op’ have one argument,
-    but its type ‘[a]’ has none
-    In the instance declaration for ‘A [a]’
-    Relevant bindings include op :: [a] (bound at tcfail001.hs:9:2)
+tcfail001.hs:9:2: error:
+    • Couldn't match expected type ‘[a]’
+                  with actual type ‘[t0] -> [t1]’
+    • The equation(s) for ‘op’ have one argument,
+      but its type ‘[a]’ has none
+      In the instance declaration for ‘A [a]’
+    • Relevant bindings include op :: [a] (bound at tcfail001.hs:9:2)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail002.stderr b/testsuite/tests/typecheck/should_fail/tcfail002.stderr
index 285b6bf577..6755636682 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail002.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail002.stderr
@@ -1,8 +1,8 @@
 
 tcfail002.hs:4:7: error:
-    • Occurs check: cannot construct the infinite type: r ~ [r]
+    • Occurs check: cannot construct the infinite type: t ~ [t]
     • In the expression: z
       In an equation for ‘c’: c z = z
     • Relevant bindings include
-        z :: [r] (bound at tcfail002.hs:4:3)
-        c :: [r] -> r (bound at tcfail002.hs:3:1)
+        z :: [t] (bound at tcfail002.hs:4:3)
+        c :: [t] -> t (bound at tcfail002.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
index 2294a6166f..c575129cf5 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
@@ -1,9 +1,9 @@
 
 tcfail004.hs:3:9: error:
-    • Couldn't match expected type ‘(r, r1)’
+    • Couldn't match expected type ‘(t, t1)’
                   with actual type ‘(Integer, Integer, Integer)’
     • In the expression: (1, 2, 3)
       In a pattern binding: (f, g) = (1, 2, 3)
     • Relevant bindings include
-        f :: r (bound at tcfail004.hs:3:2)
-        g :: r1 (bound at tcfail004.hs:3:4)
+        f :: t (bound at tcfail004.hs:3:2)
+        g :: t1 (bound at tcfail004.hs:3:4)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail005.stderr b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
index 4c585af3da..77437cf583 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail005.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
@@ -1,9 +1,9 @@
 
 tcfail005.hs:3:9: error:
-    • Couldn't match expected type ‘[r]’
+    • Couldn't match expected type ‘[t]’
                   with actual type ‘(Integer, Char)’
     • In the expression: (1, 'a')
       In a pattern binding: (h : i) = (1, 'a')
     • Relevant bindings include
-        h :: r (bound at tcfail005.hs:3:2)
-        i :: [r] (bound at tcfail005.hs:3:4)
+        h :: t (bound at tcfail005.hs:3:2)
+        i :: [t] (bound at tcfail005.hs:3:4)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail007.stderr b/testsuite/tests/typecheck/should_fail/tcfail007.stderr
index 5ea9792256..4c1652fe50 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail007.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail007.stderr
@@ -1,8 +1,8 @@
 
-tcfail007.hs:3:15:
-    No instance for (Num Bool) arising from a use of ‘+’
-    In the expression: x + 1
-    In an equation for ‘n’:
-        n x
-          | True = x + 1
-          | False = True
+tcfail007.hs:3:14: error:
+    • No instance for (Num Bool) arising from a use of ‘+’
+    • In the expression: x + 1
+      In an equation for ‘n’:
+          n x
+            | True = x + 1
+            | False = True
diff --git a/testsuite/tests/typecheck/should_fail/tcfail010.stderr b/testsuite/tests/typecheck/should_fail/tcfail010.stderr
index 92ee3d8f8e..c22a05e777 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail010.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail010.stderr
@@ -1,6 +1,6 @@
 
-tcfail010.hs:3:17:
-    No instance for (Num [r0]) arising from a use of ‘+’
-    In the expression: z + 2
-    In the expression: \ (y : z) -> z + 2
-    In an equation for ‘q’: q = \ (y : z) -> z + 2
+tcfail010.hs:3:16: error:
+    • No instance for (Num [t0]) arising from a use of ‘+’
+    • In the expression: z + 2
+      In the expression: \ (y : z) -> z + 2
+      In an equation for ‘q’: q = \ (y : z) -> z + 2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail013.stderr b/testsuite/tests/typecheck/should_fail/tcfail013.stderr
index 332f10e729..ff7702213c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail013.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail013.stderr
@@ -1,7 +1,7 @@
 
 tcfail013.hs:4:3: error:
-    • Couldn't match expected type ‘[r]’ with actual type ‘Bool’
+    • Couldn't match expected type ‘[t1]’ with actual type ‘Bool’
     • In the pattern: True
       In an equation for ‘f’: f True = 2
     • Relevant bindings include
-        f :: [r] -> a (bound at tcfail013.hs:3:1)
+        f :: [t1] -> t (bound at tcfail013.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail014.stderr b/testsuite/tests/typecheck/should_fail/tcfail014.stderr
index 92307b3830..6b88e835ed 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail014.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail014.stderr
@@ -3,6 +3,7 @@ tcfail014.hs:5:33: error:
     • Occurs check: cannot construct the infinite type: r8 ~ r8 -> r7
     • In the first argument of ‘z’, namely ‘z’
       In the expression: z z
+      In an equation for ‘h’: h z = z z
     • Relevant bindings include
         z :: r8 -> r7 (bound at tcfail014.hs:5:27)
         h :: (r8 -> r7) -> r7 (bound at tcfail014.hs:5:25)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail016.stderr b/testsuite/tests/typecheck/should_fail/tcfail016.stderr
index 59c8fa4e3d..cb1fa945e7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail016.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail016.stderr
@@ -1,22 +1,24 @@
 
-tcfail016.hs:9:20:
-    Couldn't match type ‘(t, Expr t)’ with ‘Expr t’
-    Expected type: Expr t
-      Actual type: AnnExpr t
-    In the first argument of ‘g’, namely ‘e1’
-    In the first argument of ‘(++)’, namely ‘(g e1)’
-    Relevant bindings include
-      e2 :: AnnExpr t (bound at tcfail016.hs:9:11)
-      e1 :: AnnExpr t (bound at tcfail016.hs:9:8)
-      g :: Expr t -> [[Char]] (bound at tcfail016.hs:8:1)
+tcfail016.hs:9:20: error:
+    • Couldn't match type ‘(t, Expr t)’ with ‘Expr t’
+      Expected type: Expr t
+        Actual type: AnnExpr t
+    • In the first argument of ‘g’, namely ‘e1’
+      In the first argument of ‘(++)’, namely ‘(g e1)’
+      In the expression: (g e1) ++ (g e2)
+    • Relevant bindings include
+        e2 :: AnnExpr t (bound at tcfail016.hs:9:11)
+        e1 :: AnnExpr t (bound at tcfail016.hs:9:8)
+        g :: Expr t -> [[Char]] (bound at tcfail016.hs:8:1)
 
-tcfail016.hs:9:28:
-    Couldn't match type ‘(t, Expr t)’ with ‘Expr t’
-    Expected type: Expr t
-      Actual type: AnnExpr t
-    In the first argument of ‘g’, namely ‘e2’
-    In the second argument of ‘(++)’, namely ‘(g e2)’
-    Relevant bindings include
-      e2 :: AnnExpr t (bound at tcfail016.hs:9:11)
-      e1 :: AnnExpr t (bound at tcfail016.hs:9:8)
-      g :: Expr t -> [[Char]] (bound at tcfail016.hs:8:1)
+tcfail016.hs:9:28: error:
+    • Couldn't match type ‘(t, Expr t)’ with ‘Expr t’
+      Expected type: Expr t
+        Actual type: AnnExpr t
+    • In the first argument of ‘g’, namely ‘e2’
+      In the second argument of ‘(++)’, namely ‘(g e2)’
+      In the expression: (g e1) ++ (g e2)
+    • Relevant bindings include
+        e2 :: AnnExpr t (bound at tcfail016.hs:9:11)
+        e1 :: AnnExpr t (bound at tcfail016.hs:9:8)
+        g :: Expr t -> [[Char]] (bound at tcfail016.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail018.stderr b/testsuite/tests/typecheck/should_fail/tcfail018.stderr
index 88c08a8a8b..57060a87db 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail018.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail018.stderr
@@ -1,5 +1,5 @@
 
-tcfail018.hs:5:10:
-    No instance for (Num [r0]) arising from the literal ‘1’
-    In the expression: 1
-    In a pattern binding: (a : []) = 1
+tcfail018.hs:5:10: error:
+    • No instance for (Num [t0]) arising from the literal ‘1’
+    • In the expression: 1
+      In a pattern binding: (a : []) = 1
diff --git a/testsuite/tests/typecheck/should_fail/tcfail029.stderr b/testsuite/tests/typecheck/should_fail/tcfail029.stderr
index 5b794458e8..c31c5869b9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail029.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail029.stderr
@@ -1,5 +1,5 @@
 
-tcfail029.hs:6:9:
-    No instance for (Ord Foo) arising from a use of ‘>’
-    In the expression: x > Bar
-    In an equation for ‘f’: f x = x > Bar
+tcfail029.hs:6:7: error:
+    • No instance for (Ord Foo) arising from a use of ‘>’
+    • In the expression: x > Bar
+      In an equation for ‘f’: f x = x > Bar
diff --git a/testsuite/tests/typecheck/should_fail/tcfail032.stderr b/testsuite/tests/typecheck/should_fail/tcfail032.stderr
index 05d33a5e05..79ec408274 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail032.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail032.stderr
@@ -10,4 +10,4 @@ tcfail032.hs:14:8: error:
       In an equation for ‘f’: f x = (x :: (Eq a) => a -> Int)
     • Relevant bindings include
         x :: r (bound at tcfail032.hs:14:3)
-        f :: r -> a -> Int (bound at tcfail032.hs:14:1)
+        f :: r -> forall a. Eq a => a -> Int (bound at tcfail032.hs:14:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail033.stderr b/testsuite/tests/typecheck/should_fail/tcfail033.stderr
index fd2887de60..94e998f05f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail033.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail033.stderr
@@ -1,9 +1,10 @@
 
-tcfail033.hs:4:12:
-    Occurs check: cannot construct the infinite type: t ~ (t, t1)
-    In the expression: x
-    In the expression: [x | (x, y) <- buglet]
-    Relevant bindings include
-      y :: t1 (bound at tcfail033.hs:4:19)
-      x :: t (bound at tcfail033.hs:4:17)
-      buglet :: [(t, t1)] (bound at tcfail033.hs:4:1)
+tcfail033.hs:4:12: error:
+    • Occurs check: cannot construct the infinite type: t ~ (t, t1)
+    • In the expression: x
+      In the expression: [x | (x, y) <- buglet]
+      In an equation for ‘buglet’: buglet = [x | (x, y) <- buglet]
+    • Relevant bindings include
+        y :: t1 (bound at tcfail033.hs:4:19)
+        x :: t (bound at tcfail033.hs:4:17)
+        buglet :: [(t, t1)] (bound at tcfail033.hs:4:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail034.stderr b/testsuite/tests/typecheck/should_fail/tcfail034.stderr
index 1a8d6d7802..baf68da924 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail034.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail034.stderr
@@ -1,14 +1,14 @@
-
-tcfail034.hs:17:13: error:
-    Could not deduce (Integral a) arising from a use of ‘mod’
-    from the context: (Num a, Eq a)
-      bound by the type signature for:
-                 test :: (Num a, Eq a) => a -> Bool
-      at tcfail034.hs:16:1-32
-    Possible fix:
-      add (Integral a) to the context of
-        the type signature for:
-          test :: (Num a, Eq a) => a -> Bool
-    In the first argument of ‘(==)’, namely ‘(x `mod` 3)’
-    In the expression: (x `mod` 3) == 0
-    In an equation for ‘test’: test x = (x `mod` 3) == 0
+
+tcfail034.hs:17:11: error:
+    • Could not deduce (Integral a) arising from a use of ‘mod’
+      from the context: (Num a, Eq a)
+        bound by the type signature for:
+                   test :: (Num a, Eq a) => a -> Bool
+        at tcfail034.hs:16:1-32
+      Possible fix:
+        add (Integral a) to the context of
+          the type signature for:
+            test :: (Num a, Eq a) => a -> Bool
+    • In the first argument of ‘(==)’, namely ‘(x `mod` 3)’
+      In the expression: (x `mod` 3) == 0
+      In an equation for ‘test’: test x = (x `mod` 3) == 0
diff --git a/testsuite/tests/typecheck/should_fail/tcfail065.stderr b/testsuite/tests/typecheck/should_fail/tcfail065.stderr
index 65befaf29e..369b0807d7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail065.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail065.stderr
@@ -1,14 +1,17 @@
 
-tcfail065.hs:29:20: error:
-    • Couldn't match expected type ‘x’ with actual type ‘x1’
+tcfail065.hs:29:18: error:
+    • Couldn't match type ‘x1’ with ‘x’
       ‘x1’ is a rigid type variable bound by
         the type signature for:
           setX :: forall x1. 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
-    • In the first argument of ‘X’, namely ‘x’
-      In the expression: X x
+      Expected type: X x
+        Actual type: X x1
+    • In the expression: X x
+      In an equation for ‘setX’: setX x (X _) = X x
+      In the instance declaration for ‘HasX (X x)’
     • Relevant bindings include
         x :: x1 (bound at tcfail065.hs:29:8)
         setX :: x1 -> X x -> X x (bound at tcfail065.hs:29:3)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail068.stderr b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
index 5ca47f52ed..eb42f9a33b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail068.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
@@ -16,11 +16,13 @@ tcfail068.hs:14:9: error:
     • In the first argument of ‘runST’, namely
         ‘(newSTArray ((1, 1), n) x)’
       In the expression: runST (newSTArray ((1, 1), n) x)
+      In an equation for ‘itgen’:
+          itgen n x = runST (newSTArray ((1, 1), n) x)
     • Relevant bindings include
         itgen :: (Int, Int) -> a -> IndTree s a
           (bound at tcfail068.hs:12:1)
 
-tcfail068.hs:19:21: error:
+tcfail068.hs:19:9: error:
     • Couldn't match type ‘s’ with ‘s1’
       ‘s’ is a rigid type variable bound by
         the type signature for:
@@ -32,10 +34,20 @@ tcfail068.hs:19:21: error:
         a type expected by the context:
           forall s1. GHC.ST.ST s1 (IndTree s a)
         at tcfail068.hs:18:9
-      Expected type: STArray s1 (Int, Int) a
-        Actual type: IndTree s a
-    • In the first argument of ‘readSTArray’, namely ‘arr’
-      In the first argument of ‘(>>=)’, namely ‘readSTArray arr i’
+      Expected type: GHC.ST.ST s1 (IndTree s a)
+        Actual type: GHC.ST.ST s (IndTree s a)
+    • In the first argument of ‘runST’, namely
+        ‘(readSTArray arr i
+          >>= \ val -> writeSTArray arr i (f val) >> return arr)’
+      In the expression:
+        runST
+          (readSTArray arr i
+           >>= \ val -> writeSTArray arr i (f val) >> return arr)
+      In an equation for ‘itiap’:
+          itiap i f arr
+            = runST
+                (readSTArray arr i
+                 >>= \ val -> writeSTArray arr i (f val) >> return arr)
     • Relevant bindings include
         arr :: IndTree s a (bound at tcfail068.hs:17:11)
         itiap :: (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
@@ -57,6 +69,17 @@ tcfail068.hs:24:36: error:
         Actual type: GHC.ST.ST s (IndTree s a)
     • In the first argument of ‘runST’, namely ‘(itrap' i k)’
       In the expression: runST (itrap' i k)
+      In an equation for ‘itrap’:
+          itrap ((i, k), (j, l)) f arr
+            = runST (itrap' i k)
+            where
+                itrap' i k
+                  = if k > l then return arr else (itrapsnd i k >> itrap' i (k + 1))
+                itrapsnd i k
+                  = if i > j then
+                        return arr
+                    else
+                        (readSTArray arr (i, k) >>= \ val -> ...)
     • Relevant bindings include
         itrap' :: Int -> Int -> GHC.ST.ST s (IndTree s a)
           (bound at tcfail068.hs:26:9)
@@ -89,6 +112,20 @@ tcfail068.hs:36:46: error:
         Actual type: GHC.ST.ST s (c, IndTree s b)
     • In the first argument of ‘runST’, namely ‘(itrapstate' i k s)’
       In the expression: runST (itrapstate' i k s)
+      In an equation for ‘itrapstate’:
+          itrapstate ((i, k), (j, l)) f c d s arr
+            = runST (itrapstate' i k s)
+            where
+                itrapstate' i k s
+                  = if k > l then
+                        return (s, arr)
+                    else
+                        (itrapstatesnd i k s >>= \ (s, arr) -> ...)
+                itrapstatesnd i k s
+                  = if i > j then
+                        return (s, arr)
+                    else
+                        (readSTArray arr (i, k) >>= \ val -> ...)
     • Relevant bindings include
         itrapstate' :: Int -> Int -> c -> GHC.ST.ST s (c, IndTree s b)
           (bound at tcfail068.hs:38:9)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail076.stderr b/testsuite/tests/typecheck/should_fail/tcfail076.stderr
index 8283ef0458..242c62235e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail076.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail076.stderr
@@ -13,6 +13,7 @@ tcfail076.hs:18:82: error:
         Actual type: m res
     • In the expression: cont a
       In the first argument of ‘KContT’, namely ‘(\ cont' -> cont a)’
+      In the expression: KContT (\ cont' -> cont a)
     • Relevant bindings include
         cont' :: b -> m res1 (bound at tcfail076.hs:18:73)
         cont :: a -> m res (bound at tcfail076.hs:18:37)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail099.stderr b/testsuite/tests/typecheck/should_fail/tcfail099.stderr
index 687fafb6da..3ba8165766 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail099.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail099.stderr
@@ -8,6 +8,7 @@ tcfail099.hs:9:20: error:
         at tcfail099.hs:9:7-9
     • In the first argument of ‘f’, namely ‘arg’
       In the expression: f arg
+      In an equation for ‘call’: call (C f) arg = f arg
     • Relevant bindings include
         arg :: r (bound at tcfail099.hs:9:12)
         f :: a -> Int (bound at tcfail099.hs:9:9)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail103.stderr b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
index 627ef1158c..2d76dc588a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail103.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
@@ -1,19 +1,24 @@
-
-tcfail103.hs:15:23: error:
-    Couldn't match type ‘t’ with ‘s’
-    ‘t’ is a rigid type variable bound by
-    the type signature for:
-      f :: forall t. ST t Int
-    at tcfail103.hs:10:5
-    ‘s’ is a rigid type variable bound by
-    the type signature for:
-      g :: forall s. ST s Int
-    at tcfail103.hs:13:14
-    Expected type: STRef s Int
-      Actual type: STRef t Int
-    In the first argument of ‘readSTRef’, namely ‘v’
-    In the expression: readSTRef v
-    Relevant bindings include
-      g :: ST s Int (bound at tcfail103.hs:15:9)
-      v :: STRef t Int (bound at tcfail103.hs:12:5)
-      f :: ST t Int (bound at tcfail103.hs:11:1)
+
+tcfail103.hs:15:13: error:
+    • Couldn't match type ‘t’ with ‘s’
+      ‘t’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall t. ST t Int
+        at tcfail103.hs:10:5
+      ‘s’ is a rigid type variable bound by
+        the type signature for:
+          g :: forall s. ST s Int
+        at tcfail103.hs:13:14
+      Expected type: ST s Int
+        Actual type: ST t Int
+    • In the expression: readSTRef v
+      In an equation for ‘g’: g = readSTRef v
+      In the expression:
+        do { v <- newSTRef 5;
+             let g :: ST s Int
+                 g = readSTRef v;
+             g }
+    • Relevant bindings include
+        g :: ST s Int (bound at tcfail103.hs:15:9)
+        v :: STRef t Int (bound at tcfail103.hs:12:5)
+        f :: ST t Int (bound at tcfail103.hs:11:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail104.stderr b/testsuite/tests/typecheck/should_fail/tcfail104.stderr
index cb14d9af26..b6c21e5e82 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail104.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail104.stderr
@@ -1,12 +1,16 @@
 
-tcfail104.hs:16:19:
-    Couldn't match expected type ‘Char -> Char’
-                with actual type ‘forall a. a -> a’
-    In the expression: x
-    In the expression: (\ x -> x)
+tcfail104.hs:14:15: error:
+    • Couldn't match expected type ‘forall a. a -> a’
+                  with actual type ‘Char -> Char’
+    • When checking that the pattern signature: forall a. a -> a
+        fits the type of its context: Char -> Char
+      In the pattern: x :: forall a. a -> a
+      In the expression: (\ (x :: forall a. a -> a) -> x)
 
-tcfail104.hs:22:39:
-    Couldn't match expected type ‘forall a. a -> a’
-                with actual type ‘a0 -> a0’
-    In the expression: x
-    In the expression: (\ (x :: forall a. a -> a) -> x)
+tcfail104.hs:22:15: error:
+    • Couldn't match expected type ‘forall a. a -> a’
+                  with actual type ‘Char -> Char’
+    • When checking that the pattern signature: forall a. a -> a
+        fits the type of its context: Char -> Char
+      In the pattern: x :: forall a. a -> a
+      In the expression: (\ (x :: forall a. a -> a) -> x)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail131.stderr b/testsuite/tests/typecheck/should_fail/tcfail131.stderr
index 03bdc72eff..2ae70a0928 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail131.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail131.stderr
@@ -1,11 +1,12 @@
 
-tcfail131.hs:7:9: error:
-    • Couldn't match expected type ‘b’ with actual type ‘Integer’
+tcfail131.hs:7:11: error:
+    • Couldn't match expected type ‘Integer’ with actual type ‘b’
       ‘b’ is a rigid type variable bound by
         the type signature for:
           g :: forall b. Num b => b -> b
         at tcfail131.hs:6:8
-    • In the expression: f x x
+    • In the first argument of ‘f’, namely ‘x’
+      In the expression: f x x
       In an equation for ‘g’: g x = f x x
     • Relevant bindings include
         x :: b (bound at tcfail131.hs:7:5)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.stderr b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
index ac85d0be71..a178f02801 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.stderr
@@ -14,8 +14,7 @@ tcfail133.hs:68:7: error:
         ...plus 25 others
         ...plus three instance involving out-of-scope typess
         (use -fprint-potential-instances to see them all)
-    • In the expression: show
-      In the expression: show $ add (One :@ Zero) (One :@ One)
+    • In the expression: show $ add (One :@ Zero) (One :@ One)
       In an equation for ‘foo’:
           foo = show $ add (One :@ Zero) (One :@ One)
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
index 41268ec6df..b3bf602200 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
@@ -19,14 +19,14 @@ tcfail140.hs:12:10: error:
         rot :: r -> t (bound at tcfail140.hs:12:1)
 
 tcfail140.hs:14:15: error:
-    • Couldn't match expected type ‘a -> b’ with actual type ‘Int’
+    • Couldn't match expected type ‘t -> b’ with actual type ‘Int’
     • The operator ‘f’ takes two arguments,
       but its type ‘Int -> Int’ has only one
       In the first argument of ‘map’, namely ‘(3 `f`)’
       In the expression: map (3 `f`) xs
     • Relevant bindings include
-        xs :: [a] (bound at tcfail140.hs:14:5)
-        bot :: [a] -> [b] (bound at tcfail140.hs:14:1)
+        xs :: [t] (bound at tcfail140.hs:14:5)
+        bot :: [t] -> [b] (bound at tcfail140.hs:14:1)
 
 tcfail140.hs:16:8: error:
     • The constructor ‘Just’ should have 1 argument, but has been given none
@@ -35,6 +35,6 @@ tcfail140.hs:16:8: error:
       In the expression: ((\ Just x -> x) :: Maybe a -> a) (Just 1)
 
 tcfail140.hs:19:1: error:
-    • Couldn't match expected type ‘t0 -> Bool’ with actual type ‘Int’
+    • Couldn't match expected type ‘Int’ with actual type ‘t0 -> Bool’
     • The equation(s) for ‘g’ have two arguments,
       but its type ‘Int -> Int’ has only one
diff --git a/testsuite/tests/typecheck/should_fail/tcfail143.stderr b/testsuite/tests/typecheck/should_fail/tcfail143.stderr
index 14c73d98da..b94266978d 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail143.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail143.stderr
@@ -1,8 +1,8 @@
 
-tcfail143.hs:29:9: error:
-    Couldn't match type ‘S Z’ with ‘Z’
-    arising from a functional dependency between:
-      constraint ‘MinMax (S Z) Z Z Z’ arising from a use of ‘extend’
-      instance ‘MinMax a Z Z a’ at tcfail143.hs:11:10-23
-    In the expression: n1 `extend` n0
-    In an equation for ‘t2’: t2 = n1 `extend` n0
+tcfail143.hs:29:6: error:
+    • Couldn't match type ‘S Z’ with ‘Z’
+        arising from a functional dependency between:
+          constraint ‘MinMax (S Z) Z Z Z’ arising from a use of ‘extend’
+          instance ‘MinMax a Z Z a’ at tcfail143.hs:11:10-23
+    • In the expression: n1 `extend` n0
+      In an equation for ‘t2’: t2 = n1 `extend` n0
diff --git a/testsuite/tests/typecheck/should_fail/tcfail153.stderr b/testsuite/tests/typecheck/should_fail/tcfail153.stderr
index 8034a804fc..5f4ec3e013 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail153.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail153.stderr
@@ -1,18 +1,17 @@
-
-tcfail153.hs:6:7: error:
-    Couldn't match type ‘a’ with ‘Bool’
-    ‘a’ is a rigid type variable bound by
-    the type signature for:
-      f :: forall a. a -> [a]
-    at tcfail153.hs:5:6
-    Expected type: [a]
-      Actual type: [Bool]
-    In the expression: g x
-    In an equation for ‘f’:
-        f x
-          = g x
-          where
-              g y = if y then [] else [...]
-    Relevant bindings include
-      x :: a (bound at tcfail153.hs:6:3)
-      f :: a -> [a] (bound at tcfail153.hs:6:1)
+
+tcfail153.hs:6:9: error:
+    • Couldn't match expected type ‘Bool’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a. a -> [a]
+        at tcfail153.hs:5:6
+    • In the first argument of ‘g’, namely ‘x’
+      In the expression: g x
+      In an equation for ‘f’:
+          f x
+            = g x
+            where
+                g y = if y then [] else [...]
+    • Relevant bindings include
+        x :: a (bound at tcfail153.hs:6:3)
+        f :: a -> [a] (bound at tcfail153.hs:6:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail165.hs b/testsuite/tests/typecheck/should_fail/tcfail165.hs
index c23a7f39b4..8b4cabdc8e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail165.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail165.hs
@@ -11,6 +11,7 @@ import Control.Concurrent
 --
 -- In GHC 7.0 it fails again! (and rightly so)
 
+-- With the Visible Type Application patch, this succeeds again.
+
 foo = do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
          putMVar var (show :: forall b. Show b => b -> String)
-
diff --git a/testsuite/tests/typecheck/should_fail/tcfail165.stderr b/testsuite/tests/typecheck/should_fail/tcfail165.stderr
deleted file mode 100644
index 2b8b434385..0000000000
--- a/testsuite/tests/typecheck/should_fail/tcfail165.stderr
+++ /dev/null
@@ -1,12 +0,0 @@
-
-tcfail165.hs:15:23:
-    Couldn't match expected type ‘forall a. Show a => a -> String’
-                with actual type ‘b0 -> String’
-    In the second argument of ‘putMVar’, namely
-      ‘(show :: forall b. Show b => b -> String)’
-    In a stmt of a 'do' block:
-      putMVar var (show :: forall b. Show b => b -> String)
-    In the expression:
-      do { var <- newEmptyMVar ::
-                    IO (MVar (forall a. Show a => a -> String));
-           putMVar var (show :: forall b. Show b => b -> String) }
diff --git a/testsuite/tests/typecheck/should_fail/tcfail168.stderr b/testsuite/tests/typecheck/should_fail/tcfail168.stderr
index e8c6c313e1..5f4656b13f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail168.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail168.stderr
@@ -1,12 +1,18 @@
 
-tcfail168.hs:7:11:
-    Couldn't match expected type ‘IO a0’
-                with actual type ‘Char -> IO ()’
-    Probable cause: ‘putChar’ is applied to too few arguments
-    In a stmt of a 'do' block: putChar
-    In the expression:
-      do { putChar;
-           putChar 'a';
-           putChar 'a';
-           putChar 'a';
-           .... }
+tcfail168.hs:7:11: error:
+    • Couldn't match expected type ‘IO a0’
+                  with actual type ‘Char -> IO ()’
+    • Probable cause: ‘putChar’ is applied to too few arguments
+      In a stmt of a 'do' block: putChar
+      In the expression:
+        do { putChar;
+             putChar 'a';
+             putChar 'a';
+             putChar 'a';
+             .... }
+      In an equation for ‘foo’:
+          foo
+            = do { putChar;
+                   putChar 'a';
+                   putChar 'a';
+                   .... }
diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.hs b/testsuite/tests/typecheck/should_fail/tcfail174.hs
index 47c63d7248..41fc18fc66 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.hs
@@ -7,6 +7,7 @@ data Capture a = Base a
 
 g :: Capture (forall a . a ->  a)
 g = Base id  -- Fails; need a rigid signature on 'id'
+    -- Actually, succeeds now, with visible type application
 
 -- This function should definitely be rejected, with or without type signature
 
@@ -14,4 +15,3 @@ h1 = Capture g
 
 h2 :: Capture b
 h2 = Capture g
-
diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
index fec5748461..e7ad3ca813 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
@@ -1,35 +1,30 @@
-
-tcfail174.hs:9:10: error:
-    Couldn't match expected type ‘forall a. a -> a’
-                with actual type ‘a0 -> a0’
-    In the first argument of ‘Base’, namely ‘id’
-    In the expression: Base id
-
-tcfail174.hs:13:14: error:
-    Couldn't match type ‘a’ with ‘a1’
-      because type variable ‘a1’ would escape its scope
-    This (rigid, skolem) type variable is bound by
-      the type forall a2. a2 -> a2
-      at tcfail174.hs:13:1-14
-    Expected type: Capture (forall x. x -> a)
-      Actual type: Capture (forall a. a -> a)
-    In the first argument of ‘Capture’, namely ‘g’
-    In the expression: Capture g
-    Relevant bindings include
-      h1 :: Capture a (bound at tcfail174.hs:13:1)
-
-tcfail174.hs:16:14: error:
-    Couldn't match type ‘a’ with ‘b’
-    ‘a’ is a rigid type variable bound by
-    the type forall a1. a1 -> a1
-    at tcfail174.hs:1:1
-    ‘b’ is a rigid type variable bound by
-    the type signature for:
-      h2 :: forall b. Capture b
-    at tcfail174.hs:15:7
-    Expected type: Capture (forall x. x -> b)
-      Actual type: Capture (forall a. a -> a)
-    In the first argument of ‘Capture’, namely ‘g’
-    In the expression: Capture g
-    Relevant bindings include
-      h2 :: Capture b (bound at tcfail174.hs:16:1)
+
+tcfail174.hs:14:14: error:
+    • Couldn't match type ‘a’ with ‘a1’
+        because type variable ‘a1’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        the type forall a2. a2 -> a2
+        at tcfail174.hs:14:1-14
+      Expected type: Capture (forall x. x -> a)
+        Actual type: Capture (forall a. a -> a)
+    • In the first argument of ‘Capture’, namely ‘g’
+      In the expression: Capture g
+      In an equation for ‘h1’: h1 = Capture g
+    • Relevant bindings include
+        h1 :: Capture a (bound at tcfail174.hs:14:1)
+
+tcfail174.hs:17:14: error:
+    • Couldn't match type ‘a’ with ‘b’
+      ‘a’ is a rigid type variable bound by
+        the type forall a1. a1 -> a1 at tcfail174.hs:1:1
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          h2 :: forall b. Capture b
+        at tcfail174.hs:16:7
+      Expected type: Capture (forall x. x -> b)
+        Actual type: Capture (forall a. a -> a)
+    • In the first argument of ‘Capture’, namely ‘g’
+      In the expression: Capture g
+      In an equation for ‘h2’: h2 = Capture g
+    • Relevant bindings include
+        h2 :: Capture b (bound at tcfail174.hs:17:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail175.stderr b/testsuite/tests/typecheck/should_fail/tcfail175.stderr
index 82da98bc0c..c421684b8d 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail175.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail175.stderr
@@ -1,7 +1,7 @@
 
 tcfail175.hs:11:1: error:
-    • Couldn't match expected type ‘String -> String -> String’
-                  with actual type ‘a’
+    • Couldn't match expected type ‘a’
+                  with actual type ‘String -> String -> String’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           evalRHS :: forall a. Int -> a
diff --git a/testsuite/tests/typecheck/should_fail/tcfail178.stderr b/testsuite/tests/typecheck/should_fail/tcfail178.stderr
index 472e133098..98df425424 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail178.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail178.stderr
@@ -1,14 +1,16 @@
 
-tcfail178.hs:15:7:
-    Couldn't match type ‘()’ with ‘[a]’
-    Expected type: Bool -> [a]
-      Actual type: Bool -> ()
-    In the first argument of ‘a’, namely ‘y’
-    In the expression: a y
-    Relevant bindings include c :: [a] (bound at tcfail178.hs:15:1)
+tcfail178.hs:15:7: error:
+    • Couldn't match type ‘()’ with ‘[a]’
+      Expected type: Bool -> [a]
+        Actual type: Bool -> ()
+    • In the first argument of ‘a’, namely ‘y’
+      In the expression: a y
+      In an equation for ‘c’: c = a y
+    • Relevant bindings include c :: [a] (bound at tcfail178.hs:15:1)
 
-tcfail178.hs:18:7:
-    Couldn't match expected type ‘Bool -> [a]’ with actual type ‘()’
-    In the first argument of ‘a’, namely ‘()’
-    In the expression: a ()
-    Relevant bindings include d :: [a] (bound at tcfail178.hs:18:1)
+tcfail178.hs:18:7: error:
+    • Couldn't match expected type ‘Bool -> [a]’ with actual type ‘()’
+    • In the first argument of ‘a’, namely ‘()’
+      In the expression: a ()
+      In an equation for ‘d’: d = a ()
+    • Relevant bindings include d :: [a] (bound at tcfail178.hs:18:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail179.stderr b/testsuite/tests/typecheck/should_fail/tcfail179.stderr
index a50e75e6be..2a0a5bf614 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail179.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail179.stderr
@@ -1,6 +1,6 @@
 
-tcfail179.hs:14:39: error:
-    • Couldn't match expected type ‘s’ with actual type ‘x’
+tcfail179.hs:14:41: error:
+    • Couldn't match type ‘x’ with ‘s’
       ‘x’ is a rigid type variable bound by
         a pattern with constructor:
           T :: forall s x. (s -> (x -> s) -> (x, s, Int)) -> T s,
@@ -10,10 +10,13 @@ tcfail179.hs:14:39: error:
         the type signature for:
           run :: forall s. T s -> Int
         at tcfail179.hs:12:8
-    • In the first argument of ‘g’, namely ‘x’
+      Expected type: x -> s
+        Actual type: s -> s
+    • In the second argument of ‘g’, namely ‘id’
       In the expression: g x id
+      In a pattern binding: (x, _, b) = g x id
     • Relevant bindings include
-        x :: x (bound at tcfail179.hs:14:26)
+        x :: s (bound at tcfail179.hs:14:26)
         g :: s -> (x -> s) -> (x, s, Int) (bound at tcfail179.hs:14:16)
         ts :: T s (bound at tcfail179.hs:13:5)
         run :: T s -> Int (bound at tcfail179.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail181.stderr b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
index 18309c10d1..6cf22a9f61 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail181.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
@@ -1,16 +1,17 @@
 
 tcfail181.hs:17:9: error:
-    Could not deduce (Monad m0) arising from a use of ‘foo’
-    from the context: Monad m
-      bound by the inferred type of
-               wog :: Monad m => r -> Something (m Bool) e
-      at tcfail181.hs:17:1-30
-    The type variable ‘m0’ is ambiguous
-    These potential instances exist:
-      instance Monad IO -- Defined in ‘GHC.Base’
-      instance Monad Maybe -- Defined in ‘GHC.Base’
-      instance Monad ((->) r) -- Defined in ‘GHC.Base’
-      ...plus two others
-      (use -fprint-potential-instances to see them all)
-    In the expression: foo {bar = return True}
-    In an equation for ‘wog’: wog x = foo {bar = return True}
+    • Could not deduce (Monad m0) arising from a use of ‘foo’
+      from the context: Monad m
+        bound by the inferred type of
+                 wog :: Monad m => r -> Something (m Bool) e
+        at tcfail181.hs:17:1-30
+      The type variable ‘m0’ is ambiguous
+      These potential instances exist:
+        instance Monad IO -- Defined in ‘GHC.Base’
+        instance Monad Maybe -- Defined in ‘GHC.Base’
+        instance Monad ((->) r) -- Defined in ‘GHC.Base’
+        ...plus two others
+        (use -fprint-potential-instances to see them all)
+    • In the expression: foo
+      In the expression: foo {bar = return True}
+      In an equation for ‘wog’: wog x = foo {bar = return True}
diff --git a/testsuite/tests/typecheck/should_fail/tcfail185.stderr b/testsuite/tests/typecheck/should_fail/tcfail185.stderr
index 785b5d6dd0..f8c3c6cd99 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail185.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail185.stderr
@@ -1,11 +1,17 @@
 
-tcfail185.hs:7:46:
-    Couldn't match expected type ‘Int -> Int’ with actual type ‘Bool’
-    In the expression: x
-    In the expression:
-      let
-        y1 = y
-        y2 = y1
-        y3 = y2
-        ....
-      in x
+tcfail185.hs:7:46: error:
+    • Couldn't match expected type ‘Int -> Int’ with actual type ‘Bool’
+    • In the expression: x
+      In the expression:
+        let
+          y1 = y
+          y2 = y1
+          y3 = y2
+          ....
+        in x
+      In the expression:
+        \ x y
+          -> let
+               y1 = ...
+               ....
+             in x
diff --git a/testsuite/tests/typecheck/should_fail/tcfail189.stderr b/testsuite/tests/typecheck/should_fail/tcfail189.stderr
index 380b014947..f23243bdd0 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail189.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail189.stderr
@@ -1,8 +1,10 @@
 
-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
+tcfail189.hs:10:31: error:
+    • 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
+      In the expression:
+        [length x | x <- [1 .. 10], 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 bd1b04ca80..6b338eb5ed 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail191.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail191.stderr
@@ -1,11 +1,13 @@
-
-tcfail191.hs:11:26: error:
-    Couldn't match type ‘a’ with ‘[a]’
-    ‘a’ is a rigid type variable bound by
-    a type expected by the context:
-      forall a. [a] -> [[a]]
-    at tcfail191.hs:10:9
-    Expected type: [a] -> [[a]]
-      Actual type: [[a]] -> [[a]]
-    In the expression: take 5
-    In a stmt of a list comprehension: then group using take 5
+
+tcfail191.hs:11:26: error:
+    • Couldn't match type ‘a’ with ‘[a]’
+      ‘a’ is a rigid type variable bound by
+        a type expected by the context:
+          forall a. [a] -> [[a]]
+        at tcfail191.hs:10:9
+      Expected type: [a] -> [[a]]
+        Actual type: [[a]] -> [[a]]
+    • In the expression: take 5
+      In a stmt of a list comprehension: then group using take 5
+      In the expression:
+        [() | x <- [Gnorf, Brain], then group using take 5]
diff --git a/testsuite/tests/typecheck/should_fail/tcfail193.stderr b/testsuite/tests/typecheck/should_fail/tcfail193.stderr
index bd8ef5348a..4a96fa4aef 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail193.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail193.stderr
@@ -1,11 +1,12 @@
-
-tcfail193.hs:10:31: error:
-    Couldn't match type ‘a’ with ‘[a]’
-    ‘a’ is a rigid type variable bound by
-    a type expected by the context:
-      forall a. [a] -> [a]
-    at tcfail193.hs:10:10
-    Expected type: [a] -> [a]
-      Actual type: [a] -> [[a]]
-    In the expression: inits
-    In a stmt of a list comprehension: then inits
+
+tcfail193.hs:10:31: error:
+    • Couldn't match type ‘a’ with ‘[a]’
+      ‘a’ is a rigid type variable bound by
+        a type expected by the context:
+          forall a. [a] -> [a]
+        at tcfail193.hs:10:10
+      Expected type: [a] -> [a]
+        Actual type: [a] -> [[a]]
+    • In the expression: inits
+      In a stmt of a list comprehension: then inits
+      In the expression: [x | x <- [3, 2, 1], then inits]
diff --git a/testsuite/tests/typecheck/should_fail/tcfail198.stderr b/testsuite/tests/typecheck/should_fail/tcfail198.stderr
index 58cf260593..88469939f3 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail198.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail198.stderr
@@ -1,13 +1,15 @@
-
-tcfail198.hs:6:36: error:
-    Couldn't match expected type ‘a2’ with actual type ‘a1’
-      because type variable ‘a2’ would escape its scope
-    This (rigid, skolem) type variable is bound by
-      an expression type signature: a2
-      at tcfail198.hs:6:36-41
-    In the expression: x :: a
-    In the second argument of ‘(++)’, namely ‘[x :: a]’
-    Relevant bindings include
-      xs :: [a1] (bound at tcfail198.hs:6:21)
-      x :: a1 (bound at tcfail198.hs:6:19)
-      f3 :: [a1] -> [a1] (bound at tcfail198.hs:6:6)
+
+tcfail198.hs:6:36: error:
+    • Couldn't match expected type ‘a2’ with actual type ‘a1’
+        because type variable ‘a2’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        an expression type signature:
+          a2
+        at tcfail198.hs:6:36-41
+    • In the expression: x :: a
+      In the second argument of ‘(++)’, namely ‘[x :: a]’
+      In the expression: xs ++ [x :: a]
+    • Relevant bindings include
+        xs :: [a1] (bound at tcfail198.hs:6:21)
+        x :: a1 (bound at tcfail198.hs:6:19)
+        f3 :: [a1] -> [a1] (bound at tcfail198.hs:6:6)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index c19aa0c274..9aef660dbd 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,14 +1,17 @@
 
-tcfail201.hs:17:58: error:
-    • Couldn't match expected type ‘a’ with actual type ‘HsDoc id0’
+tcfail201.hs:17:56: error:
+    • Couldn't match type ‘a’ with ‘HsDoc id0’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           gfoldl' :: forall (c :: * -> *) a.
                      (forall a1 b. c (a1 -> b) -> a1 -> c b)
                      -> (forall g. g -> c g) -> a -> c a
         at tcfail201.hs:15:12
-    • In the first argument of ‘z’, namely ‘DocEmpty’
-      In the expression: z DocEmpty
+      Expected type: c a
+        Actual type: c (HsDoc id0)
+    • In the expression: z DocEmpty
+      In a case alternative: DocEmpty -> z DocEmpty
+      In the expression: case hsDoc of { DocEmpty -> z DocEmpty }
     • Relevant bindings include
         hsDoc :: a (bound at tcfail201.hs:16:13)
         gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail204.stderr b/testsuite/tests/typecheck/should_fail/tcfail204.stderr
index b6ef584387..f4b6ec791b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail204.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail204.stderr
@@ -4,7 +4,7 @@ tcfail204.hs:10:15: warning:
         (Fractional a0)
           arising from the literal ‘6.3’ at tcfail204.hs:10:15-17
         (RealFrac a0)
-          arising from a use of ‘ceiling’ at tcfail204.hs:10:7-13
+          arising from a use of ‘ceiling’ at tcfail204.hs:10:7-17
     • In the first argument of ‘ceiling’, namely ‘6.3’
       In the expression: ceiling 6.3
       In an equation for ‘foo’: foo = ceiling 6.3
diff --git a/testsuite/tests/typecheck/should_fail/tcfail206.stderr b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
index 687619c9eb..e60856aaf9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail206.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
@@ -1,55 +1,55 @@
-
-tcfail206.hs:5:5: error:
-    Couldn't match type ‘Bool’ with ‘Int’
-    Expected type: Bool -> (Int, Bool)
-      Actual type: Bool -> (Bool, Bool)
-    In the expression: (, True)
-    In an equation for ‘a’: a = (, True)
-
-tcfail206.hs:8:5: error:
-    Couldn't match type ‘(Integer, Int)’ with ‘Bool -> (Int, Bool)’
-    Expected type: Int -> Bool -> (Int, Bool)
-      Actual type: Int -> (Integer, Int)
-    In the expression: (1,)
-    In an equation for ‘b’: b = (1,)
-
-tcfail206.hs:11:5: error:
-    Couldn't match type ‘a’ with ‘Bool’
-    ‘a’ is a rigid type variable bound by
-    the type signature for:
-      c :: forall a. a -> (a, Bool)
-    at tcfail206.hs:10:6
-    Expected type: a -> (a, Bool)
-      Actual type: a -> (a, a)
-    In the expression: (True || False,)
-    In an equation for ‘c’: c = (True || False,)
-    Relevant bindings include
-      c :: a -> (a, Bool) (bound at tcfail206.hs:11:1)
-
-tcfail206.hs:14:5: error:
-    Couldn't match type ‘Bool’ with ‘Int’
-    Expected type: Bool -> (# Int, Bool #)
-      Actual type: Bool -> (# Bool, Bool #)
-    In the expression: (# , True #)
-    In an equation for ‘d’: d = (# , True #)
-
-tcfail206.hs:17:5: error:
-    Couldn't match type ‘(# Integer, Int #)’
-                   with ‘Bool -> (# Int, Bool #)’
-    Expected type: Int -> Bool -> (# Int, Bool #)
-      Actual type: Int -> (# Integer, Int #)
-    In the expression: (# 1, #)
-    In an equation for ‘e’: e = (# 1, #)
-
-tcfail206.hs:20:5: error:
-    Couldn't match type ‘a’ with ‘Bool’
-    ‘a’ is a rigid type variable bound by
-    the type signature for:
-      f :: forall a. a -> (# a, Bool #)
-    at tcfail206.hs:19:6
-    Expected type: a -> (# a, Bool #)
-      Actual type: a -> (# a, a #)
-    In the expression: (# True || False, #)
-    In an equation for ‘f’: f = (# True || False, #)
-    Relevant bindings include
-      f :: a -> (# a, Bool #) (bound at tcfail206.hs:20:1)
+
+tcfail206.hs:5:5: error:
+    • Couldn't match type ‘Bool’ with ‘Int’
+      Expected type: Bool -> (Int, Bool)
+        Actual type: Int -> (Int, Bool)
+    • In the expression: (, True)
+      In an equation for ‘a’: a = (, True)
+
+tcfail206.hs:8:5: error:
+    • Couldn't match type ‘(Integer, Int)’ with ‘Bool -> (Int, Bool)’
+      Expected type: Int -> Bool -> (Int, Bool)
+        Actual type: Int -> (Integer, Int)
+    • In the expression: (1,)
+      In an equation for ‘b’: b = (1,)
+
+tcfail206.hs:11:5: error:
+    • Couldn't match type ‘a’ with ‘Bool’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          c :: forall a. a -> (a, Bool)
+        at tcfail206.hs:10:6
+      Expected type: a -> (a, Bool)
+        Actual type: Bool -> (a, Bool)
+    • In the expression: (True || False,)
+      In an equation for ‘c’: c = (True || False,)
+    • Relevant bindings include
+        c :: a -> (a, Bool) (bound at tcfail206.hs:11:1)
+
+tcfail206.hs:14:5: error:
+    • Couldn't match type ‘Bool’ with ‘Int’
+      Expected type: Bool -> (# Int, Bool #)
+        Actual type: Int -> (# Int, Bool #)
+    • In the expression: (# , True #)
+      In an equation for ‘d’: d = (# , True #)
+
+tcfail206.hs:17:5: error:
+    • Couldn't match type ‘(# Integer, Int #)’
+                     with ‘Bool -> (# Int, Bool #)’
+      Expected type: Int -> Bool -> (# Int, Bool #)
+        Actual type: Int -> (# Integer, Int #)
+    • In the expression: (# 1, #)
+      In an equation for ‘e’: e = (# 1, #)
+
+tcfail206.hs:20:5: error:
+    • Couldn't match type ‘a’ with ‘Bool’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a. a -> (# a, Bool #)
+        at tcfail206.hs:19:6
+      Expected type: a -> (# a, Bool #)
+        Actual type: Bool -> (# a, Bool #)
+    • In the expression: (# True || False, #)
+      In an equation for ‘f’: f = (# True || False, #)
+    • Relevant bindings include
+        f :: a -> (# a, Bool #) (bound at tcfail206.hs:20:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail208.stderr b/testsuite/tests/typecheck/should_fail/tcfail208.stderr
index dd290d942c..45642a7548 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail208.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail208.stderr
@@ -1,9 +1,9 @@
-
-tcfail208.hs:4:19: error:
-    Could not deduce (Eq (m a)) arising from a use of ‘==’
-    from the context: (Monad m, Eq a)
-      bound by the type signature for:
-                 f :: (Monad m, Eq a) => a -> m a -> Bool
-      at tcfail208.hs:3:1-40
-    In the expression: (return x == y)
-    In an equation for ‘f’: f x y = (return x == y)
+
+tcfail208.hs:4:10: error:
+    • Could not deduce (Eq (m a)) arising from a use of ‘==’
+      from the context: (Monad m, Eq a)
+        bound by the type signature for:
+                   f :: (Monad m, Eq a) => a -> m a -> Bool
+        at tcfail208.hs:3:1-40
+    • In the expression: (return x == y)
+      In an equation for ‘f’: f x y = (return x == y)
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index 138ac58ecc..031dad6321 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -50,7 +50,7 @@ test('tcrun031', normal, compile_and_run, [''])
 test('tcrun032', normal, compile_and_run, [''])
 test('tcrun033', normal, compile_and_run, [''])
 test('tcrun034', normal, compile_and_run, [''])
-test('tcrun035', normal, compile_fail, [''])
+test('tcrun035', normal, compile_and_run, [''])
 test('tcrun036', normal, compile_and_run, [''])
 test('tcrun037', normal, compile_and_run, [''])
 
diff --git a/testsuite/tests/typecheck/should_run/tcrun035.stderr b/testsuite/tests/typecheck/should_run/tcrun035.stderr
deleted file mode 100644
index c72ef618ab..0000000000
--- a/testsuite/tests/typecheck/should_run/tcrun035.stderr
+++ /dev/null
@@ -1,11 +0,0 @@
-
-tcrun035.hs:13:7:
-    Couldn't match type ‘IO a’
-                  with ‘forall (m :: * -> *). Monad m => m a’
-    Expected type: (forall (m :: * -> *). Monad m => m a) -> IO a
-      Actual type: IO a -> IO a
-    In the expression: id . id
-    In an equation for ‘foo’: foo = id . id
-    Relevant bindings include
-      foo :: (forall (m :: * -> *). Monad m => m a) -> IO a
-        (bound at tcrun035.hs:13:1)
diff --git a/testsuite/tests/warnings/should_compile/PluralS.stderr b/testsuite/tests/warnings/should_compile/PluralS.stderr
index c013e7b73d..1c975abdb2 100644
--- a/testsuite/tests/warnings/should_compile/PluralS.stderr
+++ b/testsuite/tests/warnings/should_compile/PluralS.stderr
@@ -9,7 +9,7 @@ PluralS.hs:15:17: warning:
 PluralS.hs:17:29: warning:
     • Defaulting the following constraints to type ‘Integer’
         (Num a0) arising from the literal ‘123’ at PluralS.hs:17:29-31
-        (Show a0) arising from a use of ‘show’ at PluralS.hs:17:24-27
+        (Show a0) arising from a use of ‘show’ at PluralS.hs:17:24-31
     • In the first argument of ‘show’, namely ‘123’
       In the expression: show 123
       In an equation for ‘defaultingNumAndShow’:
diff --git a/testsuite/tests/warnings/should_compile/T11077.stderr b/testsuite/tests/warnings/should_compile/T11077.stderr
index b2cfa61546..84034f8c65 100644
--- a/testsuite/tests/warnings/should_compile/T11077.stderr
+++ b/testsuite/tests/warnings/should_compile/T11077.stderr
@@ -1,3 +1,3 @@
 
 T11077.hs:3:1: warning:
-    Top-level binding with no type signature: foo :: forall r. r
+    Top-level binding with no type signature: foo :: forall a. a
author	Richard Eisenberg <eir@cis.upenn.edu>	2015-12-24 14:33:19 -0500
committer	Richard Eisenberg <eir@cis.upenn.edu>	2015-12-24 14:37:39 -0500
commit	2db18b8135335da2da9918b722699df684097be9 (patch)
tree	660dd90916aa6568694bbe39cdab83c7af98c5d7 /testsuite
parent	48db13d279d592ed3044cbaf3513854bcb0d3dce (diff)
download	haskell-2db18b8135335da2da9918b722699df684097be9.tar.gz