Improve kind generalisation, error messages

This patch does two things:

* It refactors GHC.Tc.Errors a bit.  In debugging Quick Look I was
  forced to look in detail at error messages, and ended up doing a bit
  of refactoring, esp in mkTyVarEqErr'.  It's still quite a mess, but
  a bit better, I think.

* It makes a significant improvement to the kind checking of type and
  class declarations. Specifically, we now ensure that if kind
  checking fails with an unsolved constraint, all the skolems are in
  scope.  That wasn't the case before, which led to some obscure error
  messages; and occasional failures with "no skolem info" (eg #16245).

Both of these, and the main Quick Look patch itself, affect a /lot/ of
error messages, as you can see from the number of files changed.  I've
checked them all; I think they are as good or better than before.

Smaller things

* I documented the various instances of VarBndr better.
  See Note [The VarBndr tyep and its uses] in GHC.Types.Var

* Renamed GHC.Tc.Solver.simpl_top to simplifyTopWanteds

* A bit of refactoring in bindExplicitTKTele, to avoid the
  footwork with Either.  Simpler now.

* Move promoteTyVar from GHC.Tc.Solver to GHC.Tc.Utils.TcMType

Fixes #16245 (comment 211369), memorialised as
  typecheck/polykinds/T16245a
Also fixes the three bugs in #18640

67 files changed, 324 insertions, 230 deletions

diff --git a/testsuite/tests/typecheck/should_compile/PolytypeDecomp.hs b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.hs
index 69e4fb31c7..dbbec52eaa 100644
--- a/testsuite/tests/typecheck/should_compile/PolytypeDecomp.hs
+++ b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.hs
@@ -1,32 +1,34 @@
 {-# LANGUAGE TypeFamilies, LiberalTypeSynonyms, ImpredicativeTypes #-}
-module PolyTypeDecomp where 
+module PolyTypeDecomp where
 
 
-{- The purpose of this test is to check if decomposition of wanted 
+{- The purpose of this test is to check if decomposition of wanted
    equalities in the /constraint solver/ (vs. the unifier) works properly.
-   Unfortunately most equalities between polymorphic types are converted to 
+   Unfortunately most equalities between polymorphic types are converted to
    implication constraints early on in the unifier, so we have to make things
-   a bit more convoluted by introducing the myLength function. The wanted 
+   a bit more convoluted by introducing the myLength function. The wanted
    constraints we get for this program are:
       [forall a. Maybe a] ~ Id alpha
-      [forall a. F [a]]   ~ Id alpha 
-   Which, /after reactions/ should create a fresh implication: 
+      [forall a. F [a]]   ~ Id alpha
+   Which, /after reactions/ should create a fresh implication:
       forall a. Maybe a ~ F [a]
    that is perfectly soluble.
 -}
- 
+
 type family F a
-type instance F [a] = Maybe a 
+type instance F [a] = Maybe a
 
-type family Id a 
+type family Id a
 type instance Id a = a
 
 f :: [forall a. F [a]]
 f = undefined
 
 
+-- This can't possibly work, even with Quick Look
 g :: [forall a. Maybe a] -> Int
 g x = myLength [x,f]
+-- [x,f] :: [[forall a. Maybe a]]
 
-myLength :: [Id a] -> Int 
+myLength :: [Id a] -> Int
 myLength = undefined
diff --git a/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr
new file mode 100644
index 0000000000..bde2a0d703
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr
@@ -0,0 +1,20 @@
+
+PolytypeDecomp.hs:30:17: error:
+    • Couldn't match type ‘a0’ with ‘[forall a. Maybe a]’
+      Expected: Id a0
+        Actual: [forall a. Maybe a]
+      Cannot instantiate unification variable ‘a0’
+      with a type involving polytypes: [forall a. Maybe a]
+    • In the expression: x
+      In the first argument of ‘myLength’, namely ‘[x, f]’
+      In the expression: myLength [x, f]
+
+PolytypeDecomp.hs:30:19: error:
+    • Couldn't match type ‘a0’ with ‘[forall a. F [a]]’
+      Expected: Id a0
+        Actual: [forall a. F [a]]
+      Cannot instantiate unification variable ‘a0’
+      with a type involving polytypes: [forall a. F [a]]
+    • In the expression: f
+      In the first argument of ‘myLength’, namely ‘[x, f]’
+      In the expression: myLength [x, f]
diff --git a/testsuite/tests/typecheck/should_compile/T10971a.stderr b/testsuite/tests/typecheck/should_compile/T10971a.stderr
index 96330fd61a..800dc84efa 100644
--- a/testsuite/tests/typecheck/should_compile/T10971a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T10971a.stderr
@@ -35,8 +35,8 @@ T10971a.hs:9:6: warning: [-Wname-shadowing (in -Wall)]
 T10971a.hs:9:14: warning: [-Wtype-defaults (in -Wall)]
     • Defaulting the following constraints to type ‘[]’
         (Traversable t0)
-          arising from a use of ‘fmapDefault’ at T10971a.hs:9:14-28
-        (Foldable t0) arising from a use of ‘length’ at T10971a.hs:9:31-38
+          arising from a use of ‘fmapDefault’ at T10971a.hs:9:14-24
+        (Foldable t0) arising from a use of ‘length’ at T10971a.hs:9:31-36
     • In the expression: fmapDefault f 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/T13050.stderr b/testsuite/tests/typecheck/should_compile/T13050.stderr
index 89f2b80d3b..92db8e2b63 100644
--- a/testsuite/tests/typecheck/should_compile/T13050.stderr
+++ b/testsuite/tests/typecheck/should_compile/T13050.stderr
@@ -1,8 +1,7 @@
 
 T13050.hs:4:9: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Int -> Int -> Int
-    • In the expression: _
-      In the expression: _ x y
+    • In the expression: _ x y
       In an equation for ‘f’: f x y = _ x y
     • Relevant bindings include
         y :: Int (bound at T13050.hs:4:5)
diff --git a/testsuite/tests/typecheck/should_compile/T9404b.hs b/testsuite/tests/typecheck/should_compile/T9404b.hs
index f9db0a3897..2fe837f70e 100644
--- a/testsuite/tests/typecheck/should_compile/T9404b.hs
+++ b/testsuite/tests/typecheck/should_compile/T9404b.hs
@@ -11,5 +11,5 @@ bar _ = ()
 myconst :: ((forall r. ListTF r -> Int) -> ()) -> x -> (forall r. ListTF r -> Int) -> ()
 myconst x _ = x
 
-foo = (bar `myconst` ()) $ length
+foo  = (bar `myconst` ()) $ length
 foo2 = (myconst bar ()) $ length
diff --git a/testsuite/tests/typecheck/should_compile/T9497a.stderr b/testsuite/tests/typecheck/should_compile/T9497a.stderr
index d24849df79..114a7046ca 100644
--- a/testsuite/tests/typecheck/should_compile/T9497a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9497a.stderr
@@ -2,8 +2,7 @@
 T9497a.hs:2:8: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _main :: IO ()
       Or perhaps ‘_main’ is mis-spelled, or not in scope
-    • In the expression: _main
-      In an equation for ‘main’: main = _main
+    • In an equation for ‘main’: main = _main
     • Relevant bindings include main :: IO () (bound at T9497a.hs:2:1)
       Valid hole fits include
         main :: IO () (bound at T9497a.hs:2:1)
diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
index 8182d7c992..57214ba181 100644
--- a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
@@ -1,8 +1,7 @@
 
 abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: [Integer] -> Integer
-    • In the expression: _
-      In an equation for ‘f’: f = _
+    • In an equation for ‘f’: f = _
     • Relevant bindings include
         f :: [Integer] -> Integer
           (bound at abstract_refinement_hole_fits.hs:4:1)
@@ -125,8 +124,7 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
 
 abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Integer -> [Integer] -> Integer
-    • In the expression: _
-      In the expression: _ 0
+    • In the expression: _ 0
       In an equation for ‘g’: g = _ 0
     • Relevant bindings include
         g :: [Integer] -> Integer
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9e4e80dba8..a74a84f461 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -216,7 +216,7 @@ test('tc207', normal, compile, [''])
 test('tc208', normal, compile, [''])
 test('tc209', normal, compile, [''])
 test('tc210', normal, compile, [''])
-test('tc211', normal, compile_fail, [''])
+test('tc211', normal, compile, [''])
 test('tc212', normal, compile, [''])
 test('tc213', normal, compile, [''])
 test('tc214', normal, compile, [''])
@@ -364,7 +364,7 @@ test('T3108', normal, compile, [''])
 
 test('T5792',normal, makefile_test, [])
 
-test('PolytypeDecomp', normal, compile, [''])
+test('PolytypeDecomp', normal, compile_fail, [''])
 test('T6011', normal, compile, [''])
 test('T6055', normal, compile, [''])
 test('DfltProb1', normal, compile, ['-O'])
diff --git a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
index adb507ea92..ffc02228f2 100644
--- a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
@@ -5,8 +5,7 @@ constraint_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
                the type signature for:
                  g :: forall a. Ord a => [a] -> a
                at constraint_hole_fits.hs:3:1-22
-    • In the expression: _
-      In an equation for ‘g’: g = _
+    • In an equation for ‘g’: g = _
     • Relevant bindings include
         g :: [a] -> a (bound at constraint_hole_fits.hs:4:1)
       Constraints include Ord a (from constraint_hole_fits.hs:3:1-22)
diff --git a/testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr
index 851e92e5fd..eee461b708 100644
--- a/testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr
@@ -10,9 +10,9 @@ free_monad_hole_fits.hs:14:28: warning: [-Wtyped-holes (in -Wdefault)]
                the instance declaration
                at free_monad_hole_fits.hs:10:10-38
       Or perhaps ‘_a’ is mis-spelled, or not in scope
-    • In the expression: _a
-      In the first argument of ‘Free’, namely ‘(_a go fa)’
+    • In the first argument of ‘Free’, namely ‘(_a go fa)’
       In the expression: Free (_a go fa)
+      In an equation for ‘go’: go (Free fa) = Free (_a go fa)
     • Relevant bindings include
         fa :: f (Free f a) (bound at free_monad_hole_fits.hs:14:16)
         go :: Free f a -> Free f b (bound at free_monad_hole_fits.hs:12:7)
diff --git a/testsuite/tests/typecheck/should_compile/hole_constraints.stderr b/testsuite/tests/typecheck/should_compile/hole_constraints.stderr
index c1796aad12..2e32b1b92a 100644
--- a/testsuite/tests/typecheck/should_compile/hole_constraints.stderr
+++ b/testsuite/tests/typecheck/should_compile/hole_constraints.stderr
@@ -5,8 +5,7 @@ hole_constraints.hs:8:6: warning: [-Wtyped-holes (in -Wdefault)]
                the type signature for:
                  f1 :: forall a. Eq a => a
                at hole_constraints.hs:7:1-15
-    • In the expression: _
-      In an equation for ‘f1’: f1 = _
+    • In an equation for ‘f1’: f1 = _
     • Relevant bindings include
         f1 :: a (bound at hole_constraints.hs:8:1)
       Constraints include Eq a (from hole_constraints.hs:7:1-15)
@@ -18,8 +17,7 @@ hole_constraints.hs:12:6: warning: [-Wtyped-holes (in -Wdefault)]
                the type signature for:
                  f2 :: forall a. (Show a, Eq a) => a
                at hole_constraints.hs:11:1-25
-    • In the expression: _
-      In an equation for ‘f2’: f2 = _
+    • In an equation for ‘f2’: f2 = _
     • Relevant bindings include
         f2 :: a (bound at hole_constraints.hs:12:1)
       Constraints include
@@ -34,8 +32,7 @@ hole_constraints.hs:16:35: warning: [-Wtyped-holes (in -Wdefault)]
       Where: ‘a’ is a rigid type variable bound by
                the instance declaration
                at hole_constraints.hs:16:10-22
-    • In the expression: _
-      In an equation for ‘f3’: f3 = _
+    • In an equation for ‘f3’: f3 = _
       In the instance declaration for ‘C [a]’
     • Relevant bindings include
         f3 :: [a] (bound at hole_constraints.hs:16:30)
@@ -52,8 +49,7 @@ hole_constraints.hs:20:19: warning: [-Wtyped-holes (in -Wdefault)]
                the type signature for:
                  castWith :: forall a b. (a :~: b) -> a -> b
                at hole_constraints.hs:19:1-29
-    • In the expression: _
-      In an equation for ‘castWith’: castWith Refl x = _
+    • In an equation for ‘castWith’: castWith Refl x = _
     • Relevant bindings include
         x :: a (bound at hole_constraints.hs:20:15)
         castWith :: (a :~: b) -> a -> b (bound at hole_constraints.hs:20:1)
@@ -62,9 +58,9 @@ hole_constraints.hs:20:19: warning: [-Wtyped-holes (in -Wdefault)]
 
 hole_constraints.hs:27:32: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: String
-    • In the expression: _
-      In a case alternative: AnyShow x -> _
+    • In a case alternative: AnyShow x -> _
       In the expression: case a of { AnyShow x -> _ }
+      In an equation for ‘foo’: foo a = case a of { AnyShow x -> _ }
     • Relevant bindings include
         x :: a (bound at hole_constraints.hs:27:27)
         a :: AnyShow (bound at hole_constraints.hs:27:5)
diff --git a/testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr b/testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr
index 46c0c22a34..6ca50b65b4 100644
--- a/testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr
+++ b/testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr
@@ -1,9 +1,9 @@
 
 hole_constraints_nested.hs:12:16: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Int
-    • In the expression: _
-      In a case alternative: EqOrd -> _
+    • In a case alternative: EqOrd -> _
       In the expression: case d2 of { EqOrd -> _ }
+      In a case alternative: Refl -> case d2 of { EqOrd -> _ }
     • Relevant bindings include
         d2 :: EqOrd a (bound at hole_constraints_nested.hs:9:6)
         d1 :: a :~: b (bound at hole_constraints_nested.hs:9:3)
diff --git a/testsuite/tests/typecheck/should_compile/holes.stderr b/testsuite/tests/typecheck/should_compile/holes.stderr
index 77a6fc9a40..a4f106ab82 100644
--- a/testsuite/tests/typecheck/should_compile/holes.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes.stderr
@@ -4,15 +4,13 @@ holes.hs:3:5: warning: [-Wtyped-holes (in -Wdefault)]
       Where: ‘t’ is a rigid type variable bound by
                the inferred type of f :: t
                at holes.hs:3:1-5
-    • In the expression: _
-      In an equation for ‘f’: f = _
+    • In an equation for ‘f’: f = _
     • Relevant bindings include f :: t (bound at holes.hs:3:1)
       Valid hole fits include f :: forall {t}. t
 
 holes.hs:6:7: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Char
-    • In the expression: _
-      In an equation for ‘g’: g x = _
+    • 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)
diff --git a/testsuite/tests/typecheck/should_compile/holes3.stderr b/testsuite/tests/typecheck/should_compile/holes3.stderr
index 874fd4459f..2210fc5dea 100644
--- a/testsuite/tests/typecheck/should_compile/holes3.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes3.stderr
@@ -4,16 +4,14 @@ holes3.hs:3:5: error:
       Where: ‘t’ is a rigid type variable bound by
                the inferred type of f :: t
                at holes3.hs:3:1-5
-    • In the expression: _
-      In an equation for ‘f’: f = _
+    • In an equation for ‘f’: f = _
     • Relevant bindings include f :: t (bound at holes3.hs:3:1)
       Valid hole fits include f :: forall {t}. t
 
 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
+    • 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)
diff --git a/testsuite/tests/typecheck/should_compile/local_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/local_hole_fits.stderr
index 5485d05bef..2cf85f3c1e 100644
--- a/testsuite/tests/typecheck/should_compile/local_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/local_hole_fits.stderr
@@ -5,8 +5,7 @@ local_hole_fits.hs:4:15: warning: [-Wtyped-holes (in -Wdefault)]
                the type signature for:
                  head :: forall a. [a] -> a
                at local_hole_fits.hs:3:1-16
-    • In the expression: _
-      In an equation for ‘head’: head (x : xs) = _
+    • In an equation for ‘head’: head (x : xs) = _
     • Relevant bindings include
         xs :: [a] (bound at local_hole_fits.hs:4:9)
         x :: a (bound at local_hole_fits.hs:4:7)
@@ -19,8 +18,7 @@ local_hole_fits.hs:8:11: warning: [-Wtyped-holes (in -Wdefault)]
                the type signature for:
                  mshow :: forall a. Show a => a -> a
                at local_hole_fits.hs:7:1-25
-    • In the expression: _
-      In an equation for ‘mshow’: mshow a = _
+    • In an equation for ‘mshow’: mshow a = _
     • Relevant bindings include
         a :: a (bound at local_hole_fits.hs:8:7)
         mshow :: a -> a (bound at local_hole_fits.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
index 9e97fb51ff..9ed1615215 100644
--- a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
@@ -1,8 +1,7 @@
 
 refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: [Integer] -> Integer
-    • In the expression: _
-      In an equation for ‘f’: f = _
+    • In an equation for ‘f’: f = _
     • Relevant bindings include
         f :: [Integer] -> Integer (bound at refinement_hole_fits.hs:4:1)
       Valid hole fits include
@@ -114,8 +113,7 @@ refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
 
 refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Integer -> [Integer] -> Integer
-    • In the expression: _
-      In the expression: _ 0
+    • In the expression: _ 0
       In an equation for ‘g’: g = _ 0
     • Relevant bindings include
         g :: [Integer] -> Integer (bound at refinement_hole_fits.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr
index 6007ab4d0b..7799aad239 100644
--- a/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr
@@ -1,8 +1,7 @@
 
 subsumption_sort_hole_fits.hs:2:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: String -> [String]
-    • In the expression: _
-      In the expression: _ "hello, world"
+    • In the expression: _ "hello, world"
       In an equation for ‘f’: f = _ "hello, world"
     • Relevant bindings include
         f :: [String] (bound at subsumption_sort_hole_fits.hs:2:1)
diff --git a/testsuite/tests/typecheck/should_compile/tc211.hs b/testsuite/tests/typecheck/should_compile/tc211.hs
index e132cd8c80..0e23ed1640 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.hs
+++ b/testsuite/tests/typecheck/should_compile/tc211.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XScopedTypeVariables -XGADTs #-}
+{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, GADTs #-}
 
 -- Nov 2014: impredicative types are very dodgy so I am
 --           FAR from confident that these tests give the right errors
diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
deleted file mode 100644
index bbffa16943..0000000000
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ /dev/null
@@ -1,17 +0,0 @@
-
-tc211.hs:21:17: error:
-    • Couldn't match expected type: a -> a
-                  with actual type: forall a. a -> a
-    • In the first argument of ‘(:) ::
-                                  (forall a. a -> a)
-                                  -> [forall a. a -> a] -> [forall a. a -> a]’, namely
-        ‘(head foo)’
-      In the expression:
-        ((:) ::
-           (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
-          (head foo) foo
-      In an equation for ‘bar’:
-          bar
-            = ((:) ::
-                 (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
-                (head foo) foo
diff --git a/testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr
index 4757d4915c..9f96ea3505 100644
--- a/testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr
@@ -3,8 +3,7 @@ type_in_type_hole_fits.hs:79:11: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole:
         _a :: [Integer] -> Sorted (O ('NLogN 2 0)) (O N) 'True Integer
       Or perhaps ‘_a’ is mis-spelled, or not in scope
-    • In the expression: _a
-      In the expression: _a [3, 1, 2]
+    • In the expression: _a [3, 1, 2]
       In an equation for ‘mySortA’: mySortA = _a [3, 1, 2]
     • Relevant bindings include
         mySortA :: Sorted (O (N ^. 2)) (O N) 'True Integer
@@ -32,8 +31,7 @@ type_in_type_hole_fits.hs:82:11: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole:
         _b :: [Integer] -> Sorted (O ('NLogN 1 1)) (O N) 'False Integer
       Or perhaps ‘_b’ is mis-spelled, or not in scope
-    • In the expression: _b
-      In the expression: _b [3, 1, 2]
+    • In the expression: _b [3, 1, 2]
       In an equation for ‘mySortB’: mySortB = _b [3, 1, 2]
     • Relevant bindings include
         mySortB :: Sorted (O (N *. LogN)) (O N) 'False Integer
@@ -65,8 +63,7 @@ type_in_type_hole_fits.hs:85:11: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole:
         _c :: [Integer] -> Sorted (O ('NLogN 1 1)) (O One) 'False Integer
       Or perhaps ‘_c’ is mis-spelled, or not in scope
-    • In the expression: _c
-      In the expression: _c [3, 1, 2]
+    • In the expression: _c [3, 1, 2]
       In an equation for ‘mySortC’: mySortC = _c [3, 1, 2]
     • Relevant bindings include
         mySortC :: Sorted (O (N *. LogN)) (O One) 'False Integer
diff --git a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
index 116a18f42f..5830ecb7d7 100644
--- a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
@@ -11,12 +11,16 @@ valid_hole_fits.hs:9:6: warning: [-Wdeferred-out-of-scope-variables (in -Wdefaul
 
 valid_hole_fits.hs:17:17: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Int -> IO Int
-    • In the expression: _
-      In a stmt of a 'do' block: y <- _ x
+    • In a stmt of a 'do' block: y <- _ x
       In the expression:
         do x <- a 0
            y <- _ x
            return y
+      In an equation for ‘c’:
+          c _
+            = do x <- a 0
+                 y <- _ x
+                 return y
     • Relevant bindings include
         x :: Int (bound at valid_hole_fits.hs:16:12)
         c :: Int -> IO Int (bound at valid_hole_fits.hs:16:1)
@@ -39,8 +43,7 @@ valid_hole_fits.hs:21:8: warning: [-Wtyped-holes (in -Wdefault)]
                the type signature for:
                  test :: forall a. [Maybe a] -> [a]
                at valid_hole_fits.hs:20:1-24
-    • In the expression: _
-      In an equation for ‘test’: test = _
+    • In an equation for ‘test’: test = _
     • Relevant bindings include
         test :: [Maybe a] -> [a] (bound at valid_hole_fits.hs:21:1)
       Valid hole fits include
@@ -55,8 +58,7 @@ valid_hole_fits.hs:21:8: warning: [-Wtyped-holes (in -Wdefault)]
 
 valid_hole_fits.hs:24:9: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Integer -> ValidHoleFits.Moo
-    • In the expression: _
-      In an equation for ‘test2’: test2 = _
+    • In an equation for ‘test2’: test2 = _
     • Relevant bindings include
         test2 :: Integer -> ValidHoleFits.Moo
           (bound at valid_hole_fits.hs:24:1)
@@ -70,8 +72,7 @@ valid_hole_fits.hs:24:9: warning: [-Wtyped-holes (in -Wdefault)]
 valid_hole_fits.hs:27:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: t0 -> Maybe Integer
       Where: ‘t0’ is an ambiguous type variable
-    • In the expression: _
-      In the expression: _ 2
+    • In the expression: _ 2
       In an equation for ‘k’: k = _ 2
     • Relevant bindings include
         k :: Maybe Integer (bound at valid_hole_fits.hs:27:1)
@@ -128,9 +129,9 @@ valid_hole_fits.hs:30:10: warning: [-Wtyped-holes (in -Wdefault)]
 valid_hole_fits.hs:34:11: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Bool -> a0
       Where: ‘a0’ is an ambiguous type variable
-    • In the expression: _
-      In the first argument of ‘show’, namely ‘(_ (_ :: Bool))’
+    • In the first argument of ‘show’, namely ‘(_ (_ :: Bool))’
       In the expression: show (_ (_ :: Bool))
+      In an equation for ‘h’: h = show (_ (_ :: Bool))
     • Relevant bindings include
         h :: String (bound at valid_hole_fits.hs:34:1)
       Valid hole fits include
@@ -202,8 +203,7 @@ valid_hole_fits.hs:38:10: warning: [-Wtyped-holes (in -Wdefault)]
                the type signature for:
                  myCons :: forall a. a -> [a] -> [a]
                at valid_hole_fits.hs:37:1-25
-    • In the expression: _
-      In an equation for ‘myCons’: myCons = _
+    • In an equation for ‘myCons’: myCons = _
     • Relevant bindings include
         myCons :: a -> [a] -> [a] (bound at valid_hole_fits.hs:38:1)
       Valid hole fits include
@@ -226,8 +226,7 @@ valid_hole_fits.hs:38:10: warning: [-Wtyped-holes (in -Wdefault)]
 
 valid_hole_fits.hs:41:8: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: String -> IO ()
-    • In the expression: _
-      In the expression: _ "hello, world"
+    • In the expression: _ "hello, world"
       In an equation for ‘main’: main = _ "hello, world"
     • Relevant bindings include
         main :: IO () (bound at valid_hole_fits.hs:41:1)
diff --git a/testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr b/testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr
index ac4fdc94c7..90f7943f09 100644
--- a/testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr
+++ b/testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr
@@ -1,8 +1,7 @@
 
 valid_hole_fits_interactions.hs:15:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: SBool 'True
-    • In the expression: _
-      In an equation for ‘f’: f = _
+    • In an equation for ‘f’: f = _
     • Relevant bindings include
         f :: SBool 'True (bound at valid_hole_fits_interactions.hs:15:1)
       Valid hole fits include
diff --git a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
index 255b3ad702..6345e2ab1c 100644
--- a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
+++ b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
@@ -1,6 +1,9 @@
 
 FrozenErrorTests.hs:26:9: error:
     • Couldn't match type ‘a’ with ‘[a]’ arising from a use of ‘goo1’
+      ‘a’ is a rigid type variable bound by
+        the inferred type of test1 :: a
+        at FrozenErrorTests.hs:26:1-28
     • In the expression: goo1 False undefined
       In an equation for ‘test1’: test1 = goo1 False undefined
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/T12177.stderr b/testsuite/tests/typecheck/should_fail/T12177.stderr
index 0c810f4185..16056e3e27 100644
--- a/testsuite/tests/typecheck/should_fail/T12177.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12177.stderr
@@ -4,9 +4,9 @@ T12177.hs:3:19: error:
       Where: ‘t’ is a rigid type variable bound by
                the inferred type of bar :: p -> p1 -> t
                at T12177.hs:3:1-19
-    • In the expression: _
-      In the expression: \ x -> _
+    • In the expression: \ x -> _
       In the expression: \ x -> \ x -> _
+      In an equation for ‘bar’: bar = \ x -> \ x -> _
     • Relevant bindings include
         x :: p1 (bound at T12177.hs:3:14)
         bar :: p -> p1 -> t (bound at T12177.hs:3:1)
@@ -16,9 +16,9 @@ T12177.hs:5:37: error:
       Where: ‘t’ is a rigid type variable bound by
                the inferred type of baz :: p -> p1 -> p2 -> p3 -> p4 -> t
                at T12177.hs:5:1-37
-    • In the expression: _
-      In the expression: \ z -> _
+    • In the expression: \ z -> _
       In the expression: \ x -> \ z -> _
+      In the expression: \ z -> \ x -> \ z -> ...
     • Relevant bindings include
         z :: p4 (bound at T12177.hs:5:32)
         x :: p3 (bound at T12177.hs:5:26)
diff --git a/testsuite/tests/typecheck/should_fail/T14884.stderr b/testsuite/tests/typecheck/should_fail/T14884.stderr
index e1738891a7..c901811f6f 100644
--- a/testsuite/tests/typecheck/should_fail/T14884.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14884.stderr
@@ -2,8 +2,7 @@
 T14884.hs:4:5: error:
     • Found hole: _ :: (a0 -> IO ()) -> String -> IO ()
       Where: ‘a0’ is an ambiguous type variable
-    • In the expression: _
-      In the expression: _ print "abc"
+    • In the expression: _ print "abc"
       In an equation for ‘x’: x = _ print "abc"
     • Relevant bindings include x :: IO () (bound at T14884.hs:4:1)
       Valid hole fits include
diff --git a/testsuite/tests/typecheck/should_fail/T14904a.stderr b/testsuite/tests/typecheck/should_fail/T14904a.stderr
index c0e2b84a80..3b8d005bab 100644
--- a/testsuite/tests/typecheck/should_fail/T14904a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14904a.stderr
@@ -1,7 +1,8 @@
 
 T14904a.hs:9:6: error:
-    • Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k0’
-      Cannot instantiate unification variable ‘k0’
-      with a kind involving polytypes: forall (a :: k1). g a
+    • Expected kind ‘forall (a :: k). g a’, but ‘f’ has kind ‘k1’
+      ‘k1’ is a rigid type variable bound by
+        a family instance declaration
+        at T14904a.hs:9:3-30
     • In the first argument of ‘F’, namely ‘(f :: forall a. g a)’
       In the type family declaration for ‘F’
diff --git a/testsuite/tests/typecheck/should_fail/T15799.stderr b/testsuite/tests/typecheck/should_fail/T15799.stderr
index f93e043471..4e6d7b4dfd 100644
--- a/testsuite/tests/typecheck/should_fail/T15799.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15799.stderr
@@ -2,6 +2,3 @@
 T15799.hs:46:62: error:
     • Expected kind ‘Op Nat’, but ‘UnOp b’ has kind ‘Nat’
     • In the first argument of ‘(<=)’, namely ‘UnOp b’
-
-T15799.hs:46:62: error:
-    Expected a constraint, but ‘UnOp b <= a’ has kind ‘*’
diff --git a/testsuite/tests/typecheck/should_fail/T15807.stderr b/testsuite/tests/typecheck/should_fail/T15807.stderr
index 809398ade0..bac4b5596e 100644
--- a/testsuite/tests/typecheck/should_fail/T15807.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15807.stderr
@@ -1,6 +1,9 @@
 
-T15807.hs:12:12: error:
-    • Expected kind ‘f -> *’, but ‘f’ has kind ‘*’
-    • In the type ‘f a’
-      In the definition of data constructor ‘MkApp’
+T15807.hs:12:3: error:
+    • Cannot generalise type; skolem ‘f’ would escape its scope
+      if I tried to quantify (f0 :: f -> *) in this type:
+        forall f (a :: f). f a #-> App @f @f0 a
+      (Indeed, I sometimes struggle even printing this correctly,
+       due to its ill-scoped nature.)
+    • In the definition of data constructor ‘MkApp’
       In the data declaration for ‘App’
diff --git a/testsuite/tests/typecheck/should_fail/T15862.stderr b/testsuite/tests/typecheck/should_fail/T15862.stderr
index 97fbfab166..aeb0f73b9b 100644
--- a/testsuite/tests/typecheck/should_fail/T15862.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15862.stderr
@@ -1,28 +1,7 @@
 
-T15862.hs:17:7: error:
-    • No instance for (Typeable 'MkFoo) arising from a use of ‘typeRep’
-        GHC can't yet do polykinded
-          Typeable ('MkFoo :: (forall a. a) -> Foo)
-    • In the expression: typeRep @MkFoo
-      In an equation for ‘foo’: foo = typeRep @MkFoo
-
-T15862.hs:25:7: error:
-    • No instance for (Typeable 'MkBar) arising from a use of ‘typeRep’
-        GHC can't yet do polykinded Typeable ('MkBar :: Bool -> Bar)
-    • In the expression: typeRep
-      In an equation for ‘bar’: bar = typeRep
-
-T15862.hs:30:8: error:
-    • No instance for (Typeable 'MkQuux)
-        arising from a use of ‘typeRep’
-        GHC can't yet do polykinded
-          Typeable ('MkQuux :: (# Bool | Int #) -> Quux)
-    • In the expression: typeRep
-      In an equation for ‘quux’: quux = typeRep
-
-T15862.hs:36:8: error:
-    • No instance for (Typeable 'MkQuuz)
-        arising from a use of ‘typeRep’
-        GHC can't yet do polykinded Typeable ('MkQuuz :: Quuz)
-    • In the expression: typeRep
-      In an equation for ‘quuz’: quuz = typeRep
+T15862.hs:16:16: error:
+    • Expected kind ‘k0’, but ‘MkFoo’ has kind ‘(forall a. a) -> Foo’
+      Cannot instantiate unification variable ‘k0’
+      with a kind involving polytypes: (forall a. a) -> Foo
+    • In the first argument of ‘TypeRep’, namely ‘MkFoo’
+      In the type signature: foo :: TypeRep MkFoo
diff --git a/testsuite/tests/typecheck/should_fail/T15962.stderr b/testsuite/tests/typecheck/should_fail/T15962.stderr
index ffab68c98e..49dbb8ce96 100644
--- a/testsuite/tests/typecheck/should_fail/T15962.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15962.stderr
@@ -1,18 +1,18 @@
-T15962.hs:27:11:
-     Found hole: _ :: Big ks -> Big (Eval (Map Dual ks))
+
+T15962.hs:27:11: error:
+    • Found hole: _ :: Big ks -> Big (Eval (Map Dual ks))
       Where: ‘ks’ is a rigid type variable bound by
                the type signature for:
                  dualBig :: forall (ks :: [OpKind]).
                             Big ks -> Big (Eval (Map Dual ks))
                at T15962.hs:26:1-45
-     In the expression: _
-      In an equation for ‘dualBig’: dualBig = _
-     Relevant bindings include
+    • In an equation for ‘dualBig’: dualBig = _
+    • Relevant bindings include
         dualBig :: Big ks -> Big (Eval (Map Dual ks))
           (bound at T15962.hs:27:1)
       Valid hole fits include
         dualBig :: Big ks -> Big (Eval (Map Dual ks))
           (bound at T15962.hs:27:1)
 
-T15962.hs:33:12:
+T15962.hs:33:12: error:
     Variable not in scope: iDontExist :: Big ('Conjunction : ks)
diff --git a/testsuite/tests/typecheck/should_fail/T16456.stderr b/testsuite/tests/typecheck/should_fail/T16456.stderr
index fbc0cc6ed5..5e69b9352a 100644
--- a/testsuite/tests/typecheck/should_fail/T16456.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16456.stderr
@@ -1,8 +1,7 @@
 
 T16456.hs:7:7: error:
     • Found hole: _ :: T Int
-    • In the expression: _
-      In an equation for ‘foo’: foo = _
+    • In an equation for ‘foo’: foo = _
     • Relevant bindings include foo :: T Int (bound at T16456.hs:7:1)
       Valid hole fits include
         foo :: T Int (bound at T16456.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/T17773.stderr b/testsuite/tests/typecheck/should_fail/T17773.stderr
index 401fcc494a..22b3d5577e 100644
--- a/testsuite/tests/typecheck/should_fail/T17773.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17773.stderr
@@ -8,8 +8,7 @@ T17773.hs:16:22: error:
                                    Proxy x -> Proxy y -> Mzero x y :~: (x <|> y)
                at T17773.hs:(13,1)-(15,41)
       Or perhaps ‘_Refl’ is mis-spelled, or not in scope
-    • In the expression: _Refl
-      In an equation for ‘monadPlusMplus’: monadPlusMplus _ _ = _Refl
+    • In an equation for ‘monadPlusMplus’: monadPlusMplus _ _ = _Refl
     • Relevant bindings include
         monadPlusMplus :: Proxy x -> Proxy y -> Mzero x y :~: (x <|> y)
           (bound at T17773.hs:16:1)
diff --git a/testsuite/tests/typecheck/should_fail/T18640a.hs b/testsuite/tests/typecheck/should_fail/T18640a.hs
new file mode 100644
index 0000000000..b208cfadaa
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18640a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T18640a where
+
+import Data.Kind
+
+type F2 :: forall a b. Type -> a
+type family F2 :: forall b. Type -> Type where
diff --git a/testsuite/tests/typecheck/should_fail/T18640a.stderr b/testsuite/tests/typecheck/should_fail/T18640a.stderr
new file mode 100644
index 0000000000..edc9a83c25
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18640a.stderr
@@ -0,0 +1,9 @@
+
+T18640a.hs:11:1: error:
+    • Couldn't match kind ‘a’ with ‘*’
+      Expected: forall (b :: k). * -> *
+        Actual: forall (b :: k). * -> a
+      ‘a’ is a rigid type variable bound by
+        the type family declaration for ‘F2’
+        at T18640a.hs:10:19
+    • In the type family declaration for ‘F2’
diff --git a/testsuite/tests/typecheck/should_fail/T18640b.hs b/testsuite/tests/typecheck/should_fail/T18640b.hs
new file mode 100644
index 0000000000..f722805ca9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18640b.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T18640b where
+
+import Data.Kind
+
+data family F1 (k :: Type) :: k
+
+type F3 :: forall (a :: Type) -> forall (b :: Type) -> a
+type family F3 a where
+  F3 a = F1
diff --git a/testsuite/tests/typecheck/should_fail/T18640b.stderr b/testsuite/tests/typecheck/should_fail/T18640b.stderr
new file mode 100644
index 0000000000..2a84295a73
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18640b.stderr
@@ -0,0 +1,12 @@
+
+T18640b.hs:14:10: error:
+    • Couldn't match kind ‘k’ with ‘a’
+      Expected kind ‘forall b -> a’, but ‘F1’ has kind ‘forall k -> k’
+      ‘k’ is a rigid type variable bound by
+        the type k
+        at T18640b.hs:14:3-11
+      ‘a’ is a rigid type variable bound by
+        a family instance declaration
+        at T18640b.hs:14:6
+    • In the type ‘F1’
+      In the type family declaration for ‘F3’
diff --git a/testsuite/tests/typecheck/should_fail/T18640c.hs b/testsuite/tests/typecheck/should_fail/T18640c.hs
new file mode 100644
index 0000000000..eb6479cc3b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18640c.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T18640c where
+
+import Data.Kind
+
+type F1 :: forall k -> Type
+type family F1 k :: Type
+
+type F2 :: forall x. forall k -> x
+type F2 = F1
diff --git a/testsuite/tests/typecheck/should_fail/T18640c.stderr b/testsuite/tests/typecheck/should_fail/T18640c.stderr
new file mode 100644
index 0000000000..447882717f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18640c.stderr
@@ -0,0 +1,10 @@
+
+T18640c.hs:14:11: error:
+    • Couldn't match kind ‘x’ with ‘*’
+      Expected kind ‘forall (k1 :: k) -> x’,
+        but ‘F1’ has kind ‘forall (k1 :: k) -> *’
+      ‘x’ is a rigid type variable bound by
+        the type synonym declaration for ‘F2’
+        at T18640c.hs:13:19
+    • In the type ‘F1’
+      In the type declaration for ‘F2’
diff --git a/testsuite/tests/typecheck/should_fail/T1899.stderr b/testsuite/tests/typecheck/should_fail/T1899.stderr
index eb84cba7b4..bd4aceed9e 100644
--- a/testsuite/tests/typecheck/should_fail/T1899.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1899.stderr
@@ -1,5 +1,5 @@
 
-T1899.hs:14:36: error:
+T1899.hs:15:36: error:
     • Couldn't match type ‘a’ with ‘Proposition a0’
       Expected: [Proposition a0]
         Actual: [a]
diff --git a/testsuite/tests/typecheck/should_fail/T2846b.hs b/testsuite/tests/typecheck/should_fail/T2846b.hs
index 87468df87e..07f24e7627 100644
--- a/testsuite/tests/typecheck/should_fail/T2846b.hs
+++ b/testsuite/tests/typecheck/should_fail/T2846b.hs
@@ -3,4 +3,6 @@ module T2846 where
 
 f :: String
 f = show ([1,2,3] :: [Num a => a])
-
+-- Rejected with Quick Look
+-- The arg of 'show' is a naked 'a'
+-- And the actual arg has type (forall a. [Num a => a]), which is polymorphic
diff --git a/testsuite/tests/typecheck/should_fail/T2846b.stderr b/testsuite/tests/typecheck/should_fail/T2846b.stderr
index 8c52fd7d33..95b30407f2 100644
--- a/testsuite/tests/typecheck/should_fail/T2846b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2846b.stderr
@@ -1,7 +1,10 @@
 
-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])
+T2846b.hs:5:11: error:
+    • Couldn't match expected type ‘a1’
+                  with actual type ‘[Num a0 => a0]’
+      Cannot instantiate unification variable ‘a1’
+      with a type involving polytypes: [Num a0 => a0]
+    • In the first argument of ‘show’, namely
+        ‘([1, 2, 3] :: [Num a => a])’
+      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/T5570.stderr b/testsuite/tests/typecheck/should_fail/T5570.stderr
index 710104012d..0c12be680e 100644
--- a/testsuite/tests/typecheck/should_fail/T5570.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5570.stderr
@@ -1,6 +1,6 @@
 
 T5570.hs:7:16: error:
     • Expecting a lifted type, but ‘Double#’ is unlifted
-    • In the second argument of ‘($)’, namely ‘D# $ 3.0##’
+    • In the first argument of ‘($)’, namely ‘D#’
+      In the second argument of ‘($)’, namely ‘D# $ 3.0##’
       In the expression: print $ D# $ 3.0##
-      In an equation for ‘main’: main = print $ D# $ 3.0##
diff --git a/testsuite/tests/typecheck/should_fail/T6069.stderr b/testsuite/tests/typecheck/should_fail/T6069.stderr
index c70939fee5..ffad9a9534 100644
--- a/testsuite/tests/typecheck/should_fail/T6069.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6069.stderr
@@ -5,8 +5,8 @@ T6069.hs:13:15: error:
       Expected: ST s0 Int -> b0
         Actual: (forall s. ST s b0) -> b0
     • In the second argument of ‘(.)’, namely ‘runST’
-      In the expression: print . runST
       In the expression: (print . runST) fourty_two
+      In an equation for ‘f1’: f1 = (print . runST) fourty_two
 
 T6069.hs:14:15: error:
     • Couldn't match type: forall s. ST s b1
diff --git a/testsuite/tests/typecheck/should_fail/T7734.stderr b/testsuite/tests/typecheck/should_fail/T7734.stderr
index bf199cb4c2..f47fd3b393 100644
--- a/testsuite/tests/typecheck/should_fail/T7734.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7734.stderr
@@ -1,6 +1,9 @@
 
 T7734.hs:4:13: error:
     • Couldn't match expected type ‘t’ with actual type ‘t -> t1’
+      ‘t’ is a rigid type variable bound by
+        the inferred type of f :: (t -> t1) -> p -> t1
+        at T7734.hs:4:1-13
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘f’: x `f` y = x x
@@ -10,6 +13,9 @@ T7734.hs:4:13: error:
 
 T7734.hs:5:13: error:
     • Couldn't match expected type ‘t’ with actual type ‘t -> t1’
+      ‘t’ is a rigid type variable bound by
+        the inferred type of & :: (t -> t1) -> p -> t1
+        at T7734.hs:5:1-13
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘&’: (&) x y = x x
diff --git a/testsuite/tests/typecheck/should_fail/T8450.stderr b/testsuite/tests/typecheck/should_fail/T8450.stderr
index a75d0703c6..9ac0d63643 100644
--- a/testsuite/tests/typecheck/should_fail/T8450.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8450.stderr
@@ -1,5 +1,5 @@
 
-T8450.hs:8:20: error:
+T8450.hs:8:19: error:
     • Couldn't match type ‘a’ with ‘Bool’
       Expected: Either Bool ()
         Actual: Either a ()
diff --git a/testsuite/tests/typecheck/should_fail/T8570.stderr b/testsuite/tests/typecheck/should_fail/T8570.stderr
index d79ea6581f..183001b577 100644
--- a/testsuite/tests/typecheck/should_fail/T8570.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8570.stderr
@@ -1,10 +1,4 @@
 
-T8570.hs:6:11: error:
-    • Couldn't match expected type ‘Image’ with actual type ‘Field’
-    • In the pattern: Image {filepath = x}
-      In a pattern binding: Image {filepath = x} = logo
-      In the expression: let Image {filepath = x} = logo in x
-
 T8570.hs:6:18: error:
     • Constructor ‘Image’ does not have field ‘filepath’
     • In the pattern: Image {filepath = x}
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index 4776253f52..e202ca2610 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -1,15 +1,29 @@
 
 T8603.hs:33:17: error:
-    • Couldn't match type: RV a1
-                     with: StateT s RV a0
+    • Couldn't match kind ‘*’ with ‘* -> *’
+      When matching types
+        (->) [a1] :: * -> *
+        [a2] :: *
       Expected: [a2] -> StateT s RV a0
-        Actual: t0 ((->) [a1]) (RV a1)
+        Actual: t0 ((->) [a1]) (StateT s RV a0)
     • The function ‘lift’ is applied to two value arguments,
-        but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’
+        but its type ‘([a1] -> StateT s RV a0)
+                      -> t0 ((->) [a1]) (StateT s 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:33:22: error:
+    • Couldn't match type: RV a1
+                     with: StateT s RV a0
+      Expected: [a1] -> StateT s RV a0
+        Actual: [a1] -> RV a1
+    • In the first argument of ‘lift’, namely ‘uniform’
+      In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
+      In the expression:
+        do prize <- lift uniform [1, 2, ....]
+           return False
     • Relevant bindings include
         testRVState1 :: RVState s Bool (bound at T8603.hs:32:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9109.stderr b/testsuite/tests/typecheck/should_fail/T9109.stderr
index f30c49bde6..6a4d4988de 100644
--- a/testsuite/tests/typecheck/should_fail/T9109.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9109.stderr
@@ -1,13 +1,13 @@
 
 T9109.hs:8:13: error:
-    • Couldn't match expected type ‘p’ with actual type ‘Bool’
-        ‘p’ is untouchable
-          inside the constraints: a ~ Bool
-          bound by a pattern with constructor: GBool :: G Bool,
-                   in an equation for ‘foo’
-          at T9109.hs:8:5-9
+    • Could not deduce: p ~ Bool
+      from the context: a ~ Bool
+        bound by a pattern with constructor: GBool :: G Bool,
+                 in an equation for ‘foo’
+        at T9109.hs:8:5-9
       ‘p’ is a rigid type variable bound by
-        the inferred type of foo :: G a -> p at T9109.hs:8:1-16
+        the inferred type of foo :: G a -> p
+        at T9109.hs:8:1-16
       Possible fix: add a type signature for ‘foo’
     • In the expression: True
       In an equation for ‘foo’: foo GBool = True
diff --git a/testsuite/tests/typecheck/should_fail/T9497d.stderr b/testsuite/tests/typecheck/should_fail/T9497d.stderr
index fff9e2e6a8..42da4bf430 100644
--- a/testsuite/tests/typecheck/should_fail/T9497d.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9497d.stderr
@@ -2,8 +2,7 @@
 T9497d.hs:2:8: error:
     • Found hole: _main :: IO ()
       Or perhaps ‘_main’ is mis-spelled, or not in scope
-    • In the expression: _main
-      In an equation for ‘main’: main = _main
+    • In an equation for ‘main’: main = _main
     • Relevant bindings include main :: IO () (bound at T9497d.hs:2:1)
       Valid hole fits include
         main :: IO () (bound at T9497d.hs:2:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9858e.stderr b/testsuite/tests/typecheck/should_fail/T9858e.stderr
index f397723a02..0ea9d4736a 100644
--- a/testsuite/tests/typecheck/should_fail/T9858e.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9858e.stderr
@@ -1,5 +1,5 @@
 
-T9858e.hs:9:8: error:
+T9858e.hs:9:7: error:
     • Couldn't match type: Eq Int => Int
                      with: a0 b0
       Expected: Proxy (a0 b0)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 6b10777f12..bc325be674 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -580,3 +580,7 @@ test('T18357b', normal, compile_fail, [''])
 test('T18455', normal, compile_fail, [''])
 test('T18534', normal, compile_fail, [''])
 test('T18714', normal, compile_fail, [''])
+test('too-many', normal, compile_fail, [''])
+test('T18640a', normal, compile_fail, [''])
+test('T18640b', normal, compile_fail, [''])
+test('T18640c', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail002.stderr b/testsuite/tests/typecheck/should_fail/tcfail002.stderr
index 7de2d04c08..4e14032d62 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail002.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail002.stderr
@@ -1,6 +1,9 @@
 
 tcfail002.hs:4:7: error:
     • Couldn't match expected type ‘a’ with actual type ‘[a]’
+      ‘a’ is a rigid type variable bound by
+        the inferred type of c :: [a] -> a
+        at tcfail002.hs:(3,1)-(4,7)
     • In the expression: z
       In an equation for ‘c’: c z = z
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/tcfail014.stderr b/testsuite/tests/typecheck/should_fail/tcfail014.stderr
index 65b217ef1f..5525e01510 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail014.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail014.stderr
@@ -1,6 +1,9 @@
 
 tcfail014.hs:5:33: error:
     • Couldn't match expected type ‘t4’ with actual type ‘t4 -> t5’
+      ‘t4’ is a rigid type variable bound by
+        the inferred type of h :: (t4 -> t5) -> t5
+        at tcfail014.hs:5:25-33
     • In the first argument of ‘z’, namely ‘z’
       In the expression: z z
       In an equation for ‘h’: h z = z z
diff --git a/testsuite/tests/typecheck/should_fail/tcfail032.stderr b/testsuite/tests/typecheck/should_fail/tcfail032.stderr
index a09941d284..bb7eafc6fb 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail032.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail032.stderr
@@ -1,11 +1,9 @@
 
 tcfail032.hs:14:8: error:
     • Couldn't match expected type ‘a1 -> Int’ with actual type ‘p’
-        because type variable ‘a1’ would escape its scope
-      This (rigid, skolem) type variable is bound by
-        an expression type signature:
-          forall a1. Eq a1 => a1 -> Int
-        at tcfail032.hs:14:13-30
+      ‘p’ is a rigid type variable bound by
+        the inferred type of f :: Eq a => p -> a -> Int
+        at tcfail032.hs:14:1-31
     • In the expression: x :: (Eq a) => a -> Int
       In an equation for ‘f’: f x = (x :: (Eq a) => a -> Int)
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/tcfail033.stderr b/testsuite/tests/typecheck/should_fail/tcfail033.stderr
index a1c5e7d7d0..2b2089d8ec 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail033.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail033.stderr
@@ -1,6 +1,9 @@
 
 tcfail033.hs:4:12: error:
     • Couldn't match expected type ‘(a, b)’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        the inferred type of buglet :: [(a, b)]
+        at tcfail033.hs:4:1-32
     • In the expression: x
       In the expression: [x | (x, y) <- buglet]
       In an equation for ‘buglet’: buglet = [x | (x, y) <- buglet]
diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
index 8de86280e1..4e1ced2fc9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
@@ -9,7 +9,7 @@ tcfail140.hs:10:7: error:
 
 tcfail140.hs:12:10: error:
     • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’
-    • The operator ‘f’ takes two value arguments,
+    • The function ‘f’ is applied to two value arguments,
         but its type ‘Int -> Int’ has only one
       In the expression: 3 `f` 4
       In an equation for ‘rot’: rot xs = 3 `f` 4
@@ -19,7 +19,7 @@ tcfail140.hs:12:10: error:
 tcfail140.hs:14:15: error:
     • Couldn't match expected type ‘a -> b’ with actual type ‘Int’
     • The operator ‘f’ takes two value arguments,
-      but its type ‘Int -> Int’ has only one
+        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
diff --git a/testsuite/tests/typecheck/should_fail/tcfail165.stderr b/testsuite/tests/typecheck/should_fail/tcfail165.stderr
index b1f173f447..ecbec54fb5 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail165.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail165.stderr
@@ -1,12 +1,17 @@
 
-tcfail165.hs:19:23: error:
-    • 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)
+tcfail165.hs:18:17: error:
+    • Couldn't match type: forall a. Show a => a -> String
+                     with: b0 -> String
+      Expected: IO (MVar (b0 -> String))
+        Actual: IO (MVar (forall a. Show a => a -> String))
+    • In a stmt of a 'do' block:
+        var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
       In the expression:
         do var <- newEmptyMVar ::
                     IO (MVar (forall a. Show a => a -> String))
            putMVar var (show :: forall b. Show b => b -> String)
+      In an equation for ‘foo’:
+          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/tcfail174.hs b/testsuite/tests/typecheck/should_fail/tcfail174.hs
index c3328ea4e7..226a9ee36e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.hs
@@ -6,12 +6,16 @@ data Capture a = Base a
                | Capture (Capture (forall x . x -> a))
 
 g :: Capture (forall a . a ->  a)
-g = Base id  -- Fails; need a rigid signature on 'id'
+g = Base id
+    -- Fails; need a rigid signature on 'id'
     -- Actually, succeeds now, with visible type application
     -- Disagree: should not succeed because it instantiates
     --           Base with a forall type
+    -- May 20: succeeds with Quick Look
 
--- This function should definitely be rejected, with or without type signature
+
+-- h should definitely be rejected,
+-- with (h2) or without (h1) type signature
 
 h1 = Capture g
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
index 5747a270ef..8ac8d3f9d5 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
@@ -1,29 +1,21 @@
 
-tcfail174.hs:9:5: error:
-    • Couldn't match type: a0 -> a0
-                     with: forall a. a -> a
-      Expected: Capture (forall a. a -> a)
-        Actual: Capture (a0 -> a0)
-    • In the expression: Base id
-      In an equation for ‘g’: g = Base id
-
-tcfail174.hs:16:14: error:
+tcfail174.hs:20:14: error:
     • Couldn't match type ‘a1’ with ‘a’
       Expected: Capture (forall x. x -> a)
         Actual: Capture (forall a. a -> a)
       ‘a1’ is a rigid type variable bound by
         the type a -> a
-        at tcfail174.hs:16:1-14
+        at tcfail174.hs:20:1-14
       ‘a’ is a rigid type variable bound by
         the inferred type of h1 :: Capture a
-        at tcfail174.hs:16:1-14
+        at tcfail174.hs:20:1-14
     • 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:16:1)
+        h1 :: Capture a (bound at tcfail174.hs:20:1)
 
-tcfail174.hs:19:14: error:
+tcfail174.hs:23:14: error:
     • Couldn't match type ‘a’ with ‘b’
       Expected: Capture (forall x. x -> b)
         Actual: Capture (forall a. a -> a)
@@ -33,9 +25,9 @@ tcfail174.hs:19:14: error:
       ‘b’ is a rigid type variable bound by
         the type signature for:
           h2 :: forall b. Capture b
-        at tcfail174.hs:18:1-15
+        at tcfail174.hs:22:1-15
     • 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:19:1)
+        h2 :: Capture b (bound at tcfail174.hs:23:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail204.stderr b/testsuite/tests/typecheck/should_fail/tcfail204.stderr
index 8083ffce60..a1ab99c445 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail204.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail204.stderr
@@ -2,7 +2,7 @@
 tcfail204.hs:10:7: error: [-Wtype-defaults (in -Wall), -Werror=type-defaults]
     • Defaulting the following constraints to type ‘Double’
         (RealFrac a0)
-          arising from a use of ‘ceiling’ at tcfail204.hs:10:7-17
+          arising from a use of ‘ceiling’ at tcfail204.hs:10:7-13
         (Fractional a0)
           arising from the literal ‘6.3’ at tcfail204.hs:10:15-17
     • In the expression: ceiling 6.3
diff --git a/testsuite/tests/typecheck/should_fail/tcfail218.stderr b/testsuite/tests/typecheck/should_fail/tcfail218.stderr
index efb6c4c9d3..f591b09b2a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail218.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail218.stderr
@@ -1,11 +1,11 @@
 
-tcfail218.hs:16:5:
-    Overlapping instances for C [a] Bool arising from a use of ‘foo’
-    Matching instances:
-      instance C [a] b -- Defined at tcfail218.hs:8:29
-      instance C [Int] Bool -- Defined at tcfail218.hs:7:29
-    (The choice depends on the instantiation of ‘a’
-     To pick the first instance above, use IncoherentInstances
-     when compiling the other instance declarations)
-    In the expression: foo
-    In an equation for ‘x’: x = foo
+tcfail218.hs:16:5: error:
+    • Overlapping instances for C [a] Bool arising from a use of ‘foo’
+      Matching instances:
+        instance C [a] b -- Defined at tcfail218.hs:8:29
+        instance C [Int] Bool -- Defined at tcfail218.hs:7:29
+      (The choice depends on the instantiation of ‘a’
+       To pick the first instance above, use IncoherentInstances
+       when compiling the other instance declarations)
+    • In the expression: foo
+      In an equation for ‘x’: x = foo
diff --git a/testsuite/tests/typecheck/should_fail/too-many.hs b/testsuite/tests/typecheck/should_fail/too-many.hs
new file mode 100644
index 0000000000..e3a4e2ba04
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/too-many.hs
@@ -0,0 +1,18 @@
+module TooMany where
+
+foo :: (Int -> Int -> Bool) -> Int
+foo = error "urk"
+
+f1 :: Int -> Int -> Int -> Bool
+f1 = f1
+
+g1 = foo (f1 2 3)
+     -- Here is is sensible to report
+     -- f1 is applied to too many arguments
+
+f2 :: Int -> Bool
+f2 = f2
+
+g2 = foo (f2 2)
+     -- Here is is /not/ sensible to report
+     -- f2 is applied to too many arguments
diff --git a/testsuite/tests/typecheck/should_fail/too-many.stderr b/testsuite/tests/typecheck/should_fail/too-many.stderr
new file mode 100644
index 0000000000..01e50050ff
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/too-many.stderr
@@ -0,0 +1,16 @@
+
+too-many.hs:9:11: error:
+    • Couldn't match type ‘Bool’ with ‘Int -> Bool’
+      Expected: Int -> Int -> Bool
+        Actual: Int -> Bool
+    • Possible cause: ‘f1’ is applied to too many arguments
+      In the first argument of ‘foo’, namely ‘(f1 2 3)’
+      In the expression: foo (f1 2 3)
+      In an equation for ‘g1’: g1 = foo (f1 2 3)
+
+too-many.hs:16:11: error:
+    • Couldn't match expected type ‘Int -> Int -> Bool’
+                  with actual type ‘Bool’
+    • In the first argument of ‘foo’, namely ‘(f2 2)’
+      In the expression: foo (f2 2)
+      In an equation for ‘g2’: g2 = foo (f2 2)
diff --git a/testsuite/tests/typecheck/should_run/T9497a-run.stderr b/testsuite/tests/typecheck/should_run/T9497a-run.stderr
index 6461d98b10..7f05844778 100644
--- a/testsuite/tests/typecheck/should_run/T9497a-run.stderr
+++ b/testsuite/tests/typecheck/should_run/T9497a-run.stderr
@@ -1,8 +1,7 @@
 T9497a-run: T9497a-run.hs:2:8: error:
     • Found hole: _main :: IO ()
       Or perhaps ‘_main’ is mis-spelled, or not in scope
-    • In the expression: _main
-      In an equation for ‘main’: main = _main
+    • In an equation for ‘main’: main = _main
     • Relevant bindings include
         main :: IO () (bound at T9497a-run.hs:2:1)
       Valid hole fits include
diff --git a/testsuite/tests/typecheck/should_run/T9497b-run.stderr b/testsuite/tests/typecheck/should_run/T9497b-run.stderr
index a73b71981c..e6155ddae5 100644
--- a/testsuite/tests/typecheck/should_run/T9497b-run.stderr
+++ b/testsuite/tests/typecheck/should_run/T9497b-run.stderr
@@ -1,8 +1,7 @@
 T9497b-run: T9497b-run.hs:2:8: error:
     • Found hole: _main :: IO ()
       Or perhaps ‘_main’ is mis-spelled, or not in scope
-    • In the expression: _main
-      In an equation for ‘main’: main = _main
+    • In an equation for ‘main’: main = _main
     • Relevant bindings include
         main :: IO () (bound at T9497b-run.hs:2:1)
       Valid hole fits include
diff --git a/testsuite/tests/typecheck/should_run/T9497c-run.stderr b/testsuite/tests/typecheck/should_run/T9497c-run.stderr
index 8666900b4e..6ce2781031 100644
--- a/testsuite/tests/typecheck/should_run/T9497c-run.stderr
+++ b/testsuite/tests/typecheck/should_run/T9497c-run.stderr
@@ -1,8 +1,7 @@
 T9497c-run: T9497c-run.hs:2:8: error:
     • Found hole: _main :: IO ()
       Or perhaps ‘_main’ is mis-spelled, or not in scope
-    • In the expression: _main
-      In an equation for ‘main’: main = _main
+    • In an equation for ‘main’: main = _main
     • Relevant bindings include
         main :: IO () (bound at T9497c-run.hs:2:1)
       Valid hole fits include
diff --git a/testsuite/tests/typecheck/should_run/tcrun042.hs b/testsuite/tests/typecheck/should_run/tcrun042.hs
index 30c67601ed..82add262b1 100644
--- a/testsuite/tests/typecheck/should_run/tcrun042.hs
+++ b/testsuite/tests/typecheck/should_run/tcrun042.hs
@@ -22,4 +22,5 @@ e = (,"Hello" ++ "World",)
 dropFunction :: (a, String, forall c. c -> c -> c) -> (a, String, Int)
 dropFunction (x, y, z) = (x, y, z 10 20)
 
-main = print (dropFunction $ e "Meh" (flip const), dropFunction $ e 10 const)
+main = print ( dropFunction (e "Meh" (flip const))
+             , dropFunction (e 10 const))