Make implication tidying agree with Note [Tidying multiple names at once]wip/tidy-implic-mp

Note [Tidying multiple names at once] indicates that if multiple
variables have the same name then we shouldn't prioritise one of them
and instead rename them all to a1, a2, a3... etc

This patch implements that change, some error message changes as
expected.

Closes #20932

35 files changed, 201 insertions, 200 deletions

diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 2901078004..a6e8b4b477 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -82,7 +82,7 @@ import Control.Monad    ( unless, when, foldM, forM_ )
 import Data.Foldable    ( toList )
 import Data.Functor     ( (<&>) )
 import Data.Function    ( on )
-import Data.List        ( partition, mapAccumL, sort )
+import Data.List        ( partition, sort )
 import Data.List.NonEmpty ( NonEmpty(..), (<|) )
 import qualified Data.List.NonEmpty as NE ( map, reverse )
 import Data.List        ( sortBy )
@@ -357,7 +357,7 @@ reportImplic ctxt implic@(Implic { ic_skols  = tvs
          warnRedundantConstraints ctxt' tcl_env info' dead_givens }
   where
     insoluble    = isInsolubleStatus status
-    (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) $
+    (env1, tvs') = tidyVarBndrs (cec_tidy ctxt) $
                    scopedSort tvs
         -- scopedSort: the ic_skols may not be in dependency order
         -- (see Note [Skolems in an implication] in GHC.Tc.Types.Constraint)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
index caa062e392..b103b16187 100644
--- a/testsuite/tests/dependent/should_fail/T14066e.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -1,9 +1,9 @@
 
 T14066e.hs:13:65: error:
-    • Expected a type, but ‘c'’ has kind ‘k’
-      ‘k’ is a rigid type variable bound by
+    • Expected a type, but ‘c'’ has kind ‘k1’
+      ‘k1’ is a rigid type variable bound by
         the type signature for:
-          j :: forall {k} {k1} (c :: k) (b :: k1).
+          j :: forall {k1} {k2} (c :: k1) (b :: k2).
                Proxy a -> Proxy b -> Proxy c -> Proxy b
         at T14066e.hs:12:5-61
     • In the kind ‘c'’
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr b/testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr
index 9c1b305fbf..12fc6691a8 100644
--- a/testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr
+++ b/testsuite/tests/deriving/should_fail/deriving-via-fail4.stderr
@@ -6,13 +6,13 @@ deriving-via-fail4.hs:15:12: error:
     • When deriving the instance for (Eq F1)
 
 deriving-via-fail4.hs:18:13: error:
-    • Couldn't match representation of type ‘a’ with that of ‘a1’
+    • Couldn't match representation of type ‘a1’ with that of ‘a2’
         arising from the coercion of the method ‘c’
           from type ‘a -> a -> Bool’ to type ‘a -> F2 a1 -> Bool’
-      ‘a’ is a rigid type variable bound by
+      ‘a1’ is a rigid type variable bound by
         the deriving clause for ‘C a (F2 a1)’
         at deriving-via-fail4.hs:18:13-15
-      ‘a1’ is a rigid type variable bound by
+      ‘a2’ is a rigid type variable bound by
         the deriving clause for ‘C a (F2 a1)’
         at deriving-via-fail4.hs:18:13-15
     • When deriving the instance for (C a (F2 a1))
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index 478c410468..f36b44d09d 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,21 +1,21 @@
 
 gadt7.hs:16:38: error:
-    • Could not deduce (p ~ p1)
+    • Could not deduce (p1 ~ p2)
       from the context: a ~ Int
         bound by a pattern with constructor: K :: T Int,
                  in a case alternative
         at gadt7.hs:16:33
-      ‘p’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> p -> p1
-        at gadt7.hs:16:1-44
       ‘p1’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> p -> p1
+        the inferred type of i1b :: T a -> p1 -> p2
+        at gadt7.hs:16:1-44
+      ‘p2’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p1 -> p2
         at gadt7.hs:16:1-44
     • In the expression: y1
       In a case alternative: K -> y1
       In the expression: case t1 of K -> y1
     • Relevant bindings include
-        y1 :: p (bound at gadt7.hs:16:16)
-        y :: p (bound at gadt7.hs:16:7)
-        i1b :: T a -> p -> p1 (bound at gadt7.hs:16:1)
+        y1 :: p1 (bound at gadt7.hs:16:16)
+        y :: p1 (bound at gadt7.hs:16:7)
+        i1b :: T a -> p1 -> p2 (bound at gadt7.hs:16:1)
     Suggested fix: Consider giving ‘i1b’ a type signature
diff --git a/testsuite/tests/indexed-types/should_fail/T14369.stderr b/testsuite/tests/indexed-types/should_fail/T14369.stderr
index a3a9eb73f7..9ab572afcd 100644
--- a/testsuite/tests/indexed-types/should_fail/T14369.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14369.stderr
@@ -1,21 +1,21 @@
 
 T14369.hs:29:5: error:
-    • Couldn't match type ‘a’ with ‘a1’
-      Expected: Sing x -> Maybe (Demote a1)
-        Actual: Sing x -> Demote (Maybe a)
-      ‘a’ is a rigid type variable bound by
+    • Couldn't match type ‘a1’ with ‘a2’
+      Expected: Sing x -> Maybe (Demote a2)
+        Actual: Sing x -> Demote (Maybe a1)
+      ‘a1’ is a rigid type variable bound by
         the type signature for:
-          f :: forall {a} (x :: forall a1. Maybe a1) a1.
-               SingKind a1 =>
-               Sing x -> Maybe (Demote a1)
+          f :: forall {a1} (x :: forall a2. Maybe a2) a2.
+               SingKind a2 =>
+               Sing x -> Maybe (Demote a2)
         at T14369.hs:28:1-80
-      ‘a1’ is a rigid type variable bound by
+      ‘a2’ is a rigid type variable bound by
         the type signature for:
-          f :: forall {a} (x :: forall a1. Maybe a1) a1.
-               SingKind a1 =>
-               Sing x -> Maybe (Demote a1)
+          f :: forall {a1} (x :: forall a2. Maybe a2) a2.
+               SingKind a2 =>
+               Sing x -> Maybe (Demote a2)
         at T14369.hs:28:1-80
     • In the expression: fromSing
       In an equation for ‘f’: f = fromSing
     • Relevant bindings include
-        f :: Sing x -> Maybe (Demote a1) (bound at T14369.hs:29:1)
+        f :: Sing x -> Maybe (Demote a2) (bound at T14369.hs:29:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index 1f244f9ee2..b16ee1ef91 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -18,10 +18,10 @@ T8518.hs:14:18: error:
         callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
 
 T8518.hs:16:9: error:
-    • Couldn't match type: F t1
-                     with: Z t1 -> B t1 -> F t1
-      Expected: t -> t1 -> F t1
-        Actual: t -> t1 -> Z t1 -> B t1 -> F t1
+    • Couldn't match type: F t2
+                     with: Z t2 -> B t2 -> F t2
+      Expected: t1 -> t2 -> F t2
+        Actual: t1 -> t2 -> Z t2 -> B t2 -> F t2
     • In an equation for ‘callCont’:
           callCont c z b
             = rpt (4 :: Int) c z b
@@ -29,4 +29,4 @@ T8518.hs:16:9: error:
                 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
-        rpt :: t -> t1 -> F t1 (bound at T8518.hs:16:9)
+        rpt :: t1 -> t2 -> F t2 (bound at T8518.hs:16:9)
diff --git a/testsuite/tests/module/mod71.stderr b/testsuite/tests/module/mod71.stderr
index d877e397a0..003e0bb41c 100644
--- a/testsuite/tests/module/mod71.stderr
+++ b/testsuite/tests/module/mod71.stderr
@@ -1,13 +1,13 @@
 
 mod71.hs:4:9: error:
-    • Found hole: _ :: t1
-      Where: ‘t1’ is a rigid type variable bound by
-               the inferred type of f :: Num t => (t1 -> t -> t2) -> t2
+    • Found hole: _ :: t2
+      Where: ‘t2’ is a rigid type variable bound by
+               the inferred type of f :: Num t1 => (t2 -> t1 -> t3) -> t3
                at mod71.hs:4:1-11
     • In the first argument of ‘x’, namely ‘_’
       In the expression: x _ 1
       In an equation for ‘f’: f x = x _ 1
     • Relevant bindings include
-        x :: t1 -> t -> t2 (bound at mod71.hs:4:3)
-        f :: (t1 -> t -> t2) -> t2 (bound at mod71.hs:4:1)
-      Constraints include Num t (from mod71.hs:4:1-11)
+        x :: t2 -> t1 -> t3 (bound at mod71.hs:4:3)
+        f :: (t2 -> t1 -> t3) -> t3 (bound at mod71.hs:4:1)
+      Constraints include Num t1 (from mod71.hs:4:1-11)
diff --git a/testsuite/tests/module/mod72.stderr b/testsuite/tests/module/mod72.stderr
index 69246edb76..5f6dcc93f5 100644
--- a/testsuite/tests/module/mod72.stderr
+++ b/testsuite/tests/module/mod72.stderr
@@ -1,2 +1,2 @@
 
-mod72.hs:3:7: error: Variable not in scope: g :: t -> t1
+mod72.hs:3:7: error: Variable not in scope: g :: t1 -> t2
diff --git a/testsuite/tests/parser/should_fail/readFail003.stderr b/testsuite/tests/parser/should_fail/readFail003.stderr
index f43a759083..d969ba7df1 100644
--- a/testsuite/tests/parser/should_fail/readFail003.stderr
+++ b/testsuite/tests/parser/should_fail/readFail003.stderr
@@ -1,12 +1,12 @@
 
 readFail003.hs:4:27: error:
-    • Couldn't match expected type ‘(a, [a1], [a2])’
-                  with actual type ‘a’
-      ‘a’ is a rigid type variable bound by
+    • Couldn't match expected type ‘(a1, [a2], [a3])’
+                  with actual type ‘a1’
+      ‘a1’ is a rigid type variable bound by
         the inferred types of
-          a :: a
-          b :: [a1]
-          c :: [a2]
+          a :: a1
+          b :: [a2]
+          c :: [a3]
         at readFail003.hs:(4,1)-(8,26)
     • In the expression: a
       In a pattern binding:
@@ -17,6 +17,6 @@ readFail003.hs:4:27: error:
           where
               nullity = null
     • Relevant bindings include
-        a :: a (bound at readFail003.hs:4:3)
-        b :: [a1] (bound at readFail003.hs:4:5)
-        c :: [a2] (bound at readFail003.hs:4:7)
+        a :: a1 (bound at readFail003.hs:4:3)
+        b :: [a2] (bound at readFail003.hs:4:5)
+        c :: [a3] (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 e329410514..fd38a126c2 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -2,23 +2,23 @@
 T10403.hs:16:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found extra-constraints wildcard standing for ‘Functor f’
       Where: ‘f’ is a rigid type variable bound by
-               the inferred type of h1 :: Functor f => (a -> a1) -> f a -> H f
+               the inferred type of h1 :: Functor f => (a1 -> a2) -> f a1 -> H f
                at T10403.hs:18:1-41
     • In the type signature: h1 :: _ => _
 
 T10403.hs:16:12: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘(a -> a1) -> f a -> H f’
-      Where: ‘a1’, ‘a’, ‘f’ are rigid type variables bound by
-               the inferred type of h1 :: Functor f => (a -> a1) -> f a -> H f
+    • Found type wildcard ‘_’ standing for ‘(a1 -> a2) -> f a1 -> H f’
+      Where: ‘a2’, ‘a1’, ‘f’ are rigid type variables bound by
+               the inferred type of h1 :: Functor f => (a1 -> a2) -> f a1 -> H f
                at T10403.hs:18:1-41
     • In the type signature: h1 :: _ => _
 
 T10403.hs:20:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’
-        standing for ‘(a -> a1) -> B t0 a -> H (B t0)’
+        standing for ‘(a1 -> a2) -> B t0 a1 -> H (B t0)’
       Where: ‘t0’ is an ambiguous type variable
-             ‘a1’, ‘a’ are rigid type variables bound by
-               the inferred type of h2 :: (a -> a1) -> B t0 a -> H (B t0)
+             ‘a2’, ‘a1’ are rigid type variables bound by
+               the inferred type of h2 :: (a1 -> a2) -> B t0 a1 -> H (B t0)
                at T10403.hs:23:1-41
     • In the type signature: h2 :: _
 
@@ -26,11 +26,11 @@ T10403.hs:29:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type ‘t0’ with ‘t’
       Expected: H (B t)
         Actual: H (B t0)
-        because type variable ‘t’ would escape its scope
-      This (rigid, skolem) type variable is bound by
-        the type signature for:
-          app2 :: forall t. H (B t)
-        at T10403.hs:28:1-15
+    • because type variable ‘t’ would escape its scope
+    This (rigid, skolem) type variable is bound by
+      the type signature for:
+        app2 :: forall t. H (B t)
+      at T10403.hs:28:1-15
     • In the expression: h2 (H . I) (B ())
       In an equation for ‘app2’: app2 = h2 (H . I) (B ())
     • Relevant bindings include
diff --git a/testsuite/tests/partial-sigs/should_compile/T10438.stderr b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
index 164007679c..358fb52ba8 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10438.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
@@ -1,8 +1,8 @@
 
 T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘p2’
-      Where: ‘p2’ is a rigid type variable bound by
-               the inferred type of g :: p2 -> p2
+    • Found type wildcard ‘_’ standing for ‘p3’
+      Where: ‘p3’ is a rigid type variable bound by
+               the inferred type of g :: p3 -> p3
                at T10438.hs:(6,9)-(8,21)
     • In the type signature: x :: _
       In an equation for ‘g’:
@@ -21,7 +21,7 @@ T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
                       x :: _
                       x = r
     • Relevant bindings include
-        r :: p2 (bound at T10438.hs:6:11)
-        g :: p2 -> p2 (bound at T10438.hs:6:9)
-        f :: p (bound at T10438.hs:5:5)
-        foo :: p -> p1 -> p1 (bound at T10438.hs:5:1)
+        r :: p3 (bound at T10438.hs:6:11)
+        g :: p3 -> p3 (bound at T10438.hs:6:9)
+        f :: p1 (bound at T10438.hs:5:5)
+        foo :: p1 -> p2 -> p2 (bound at T10438.hs:5:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T11192.stderr b/testsuite/tests/partial-sigs/should_compile/T11192.stderr
index 8030276206..6cfbe62628 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11192.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11192.stderr
@@ -19,9 +19,9 @@ T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Relevant bindings include fails :: a (bound at T11192.hs:6:1)
 
 T11192.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘p -> p1 -> p1’
-      Where: ‘p’, ‘p1’ are rigid type variables bound by
-               the inferred type of go :: p -> p1 -> p1
+    • Found type wildcard ‘_’ standing for ‘p1 -> p2 -> p2’
+      Where: ‘p1’, ‘p2’ are rigid type variables bound by
+               the inferred type of go :: p1 -> p2 -> p2
                at T11192.hs:14:8-17
     • In the type signature: go :: _
       In the expression:
diff --git a/testsuite/tests/partial-sigs/should_compile/T12844.stderr b/testsuite/tests/partial-sigs/should_compile/T12844.stderr
index 331570aa93..52c0d8c7d1 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12844.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12844.stderr
@@ -2,7 +2,7 @@
 T12844.hs:12:9: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found extra-constraints wildcard standing for
         ‘(Head rngs ~ '(r, r'), Foo rngs)’
-      Where: ‘r’, ‘r'’, ‘k’, ‘k1’, ‘rngs’
+      Where: ‘r’, ‘r'’, ‘k1’, ‘k2’, ‘rngs’
                are rigid type variables bound by
                the inferred type of
                  bar :: (Head rngs ~ '(r, r'), Foo rngs) => FooData rngs
diff --git a/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr b/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
index fbbfc6e4c9..a7a5ee85be 100644
--- a/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
@@ -1,17 +1,17 @@
 
 TidyClash.hs:8:19: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of bar :: w_ -> (w_, w -> w1)
+    • Found type wildcard ‘_’ standing for ‘w1’
+      Where: ‘w1’ is a rigid type variable bound by
+               the inferred type of bar :: w_ -> (w_, w1 -> w2)
                at TidyClash.hs:9:1-28
       To use the inferred type, enable PartialTypeSignatures
     • In the type ‘w_ -> (w_, _ -> _)’
       In the type signature: bar :: w_ -> (w_, _ -> _)
 
 TidyClash.hs:8:24: error:
-    • Found type wildcard ‘_’ standing for ‘w1’
-      Where: ‘w1’ is a rigid type variable bound by
-               the inferred type of bar :: w_ -> (w_, w -> w1)
+    • Found type wildcard ‘_’ standing for ‘w2’
+      Where: ‘w2’ is a rigid type variable bound by
+               the inferred type of bar :: w_ -> (w_, w1 -> w2)
                at TidyClash.hs:9:1-28
       To use the inferred type, enable PartialTypeSignatures
     • In the type ‘w_ -> (w_, _ -> _)’
diff --git a/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr b/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
index 7e6b1da683..504fbf5094 100644
--- a/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
@@ -1,26 +1,26 @@
 
 TidyClash2.hs:13:20: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of barry :: w -> w1 -> t
+    • Found type wildcard ‘_’ standing for ‘w1’
+      Where: ‘w1’ is a rigid type variable bound by
+               the inferred type of barry :: w1 -> w2 -> t
                at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
     • In the type ‘_ -> _ -> t’
       In the type signature: barry :: forall t. _ -> _ -> t
 
 TidyClash2.hs:13:25: error:
-    • Found type wildcard ‘_’ standing for ‘w1’
-      Where: ‘w1’ is a rigid type variable bound by
-               the inferred type of barry :: w -> w1 -> t
+    • Found type wildcard ‘_’ standing for ‘w2’
+      Where: ‘w2’ is a rigid type variable bound by
+               the inferred type of barry :: w1 -> w2 -> t
                at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
     • In the type ‘_ -> _ -> t’
       In the type signature: barry :: forall t. _ -> _ -> t
 
 TidyClash2.hs:14:13: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of barry :: w -> w1 -> t
+    • Found type wildcard ‘_’ standing for ‘w1’
+      Where: ‘w1’ is a rigid type variable bound by
+               the inferred type of barry :: w1 -> w2 -> t
                at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: _
@@ -28,12 +28,12 @@ TidyClash2.hs:14:13: error:
       In an equation for ‘barry’:
           barry (x :: _) (y :: _) = undefined :: _
     • Relevant bindings include
-        barry :: w -> w1 -> t (bound at TidyClash2.hs:14:1)
+        barry :: w1 -> w2 -> t (bound at TidyClash2.hs:14:1)
 
 TidyClash2.hs:14:22: error:
-    • Found type wildcard ‘_’ standing for ‘w1’
-      Where: ‘w1’ is a rigid type variable bound by
-               the inferred type of barry :: w -> w1 -> t
+    • Found type wildcard ‘_’ standing for ‘w2’
+      Where: ‘w2’ is a rigid type variable bound by
+               the inferred type of barry :: w1 -> w2 -> t
                at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
     • In a pattern type signature: _
@@ -41,13 +41,13 @@ TidyClash2.hs:14:22: error:
       In an equation for ‘barry’:
           barry (x :: _) (y :: _) = undefined :: _
     • Relevant bindings include
-        x :: w (bound at TidyClash2.hs:14:8)
-        barry :: w -> w1 -> t (bound at TidyClash2.hs:14:1)
+        x :: w1 (bound at TidyClash2.hs:14:8)
+        barry :: w1 -> w2 -> t (bound at TidyClash2.hs:14:1)
 
 TidyClash2.hs:14:40: error:
-    • Found type wildcard ‘_’ standing for ‘w2’
-      Where: ‘w2’ is a rigid type variable bound by
-               the inferred type of <expression> :: w2
+    • Found type wildcard ‘_’ standing for ‘w3’
+      Where: ‘w3’ is a rigid type variable bound by
+               the inferred type of <expression> :: w3
                at TidyClash2.hs:14:40
       To use the inferred type, enable PartialTypeSignatures
     • In an expression type signature: _
@@ -55,6 +55,6 @@ TidyClash2.hs:14:40: error:
       In an equation for ‘barry’:
           barry (x :: _) (y :: _) = undefined :: _
     • Relevant bindings include
-        y :: w1 (bound at TidyClash2.hs:14:17)
-        x :: w (bound at TidyClash2.hs:14:8)
-        barry :: w -> w1 -> t (bound at TidyClash2.hs:14:1)
+        y :: w2 (bound at TidyClash2.hs:14:17)
+        x :: w1 (bound at TidyClash2.hs:14:8)
+        barry :: w1 -> w2 -> t (bound at TidyClash2.hs:14:1)
diff --git a/testsuite/tests/polykinds/T14265.stderr b/testsuite/tests/polykinds/T14265.stderr
index cf3ab9acf3..188430bdbb 100644
--- a/testsuite/tests/polykinds/T14265.stderr
+++ b/testsuite/tests/polykinds/T14265.stderr
@@ -10,9 +10,9 @@ T14265.hs:7:12: error:
       In the type signature: f :: proxy _ -> ()
 
 T14265.hs:10:15: error:
-    • Found type wildcard ‘_’ standing for ‘w’
-      Where: ‘w’ is a rigid type variable bound by
-               the inferred type of foo :: StateT w w1 ()
+    • Found type wildcard ‘_’ standing for ‘w1’
+      Where: ‘w1’ is a rigid type variable bound by
+               the inferred type of foo :: StateT w1 w2 ()
                at T14265.hs:11:1-15
       To use the inferred type, enable PartialTypeSignatures
     • In the first argument of ‘StateT’, namely ‘_’
@@ -20,9 +20,9 @@ T14265.hs:10:15: error:
       In the type signature: foo :: StateT _ _ ()
 
 T14265.hs:10:17: error:
-    • Found type wildcard ‘_’ standing for ‘w1 :: * -> *’
-      Where: ‘w1’ is a rigid type variable bound by
-               the inferred type of foo :: StateT w w1 ()
+    • Found type wildcard ‘_’ standing for ‘w2 :: * -> *’
+      Where: ‘w2’ is a rigid type variable bound by
+               the inferred type of foo :: StateT w1 w2 ()
                at T14265.hs:11:1-15
       To use the inferred type, enable PartialTypeSignatures
     • In the second argument of ‘StateT’, namely ‘_’
diff --git a/testsuite/tests/polykinds/T16244.stderr b/testsuite/tests/polykinds/T16244.stderr
index 4e83aa7b6f..3e9c229233 100644
--- a/testsuite/tests/polykinds/T16244.stderr
+++ b/testsuite/tests/polykinds/T16244.stderr
@@ -1,10 +1,10 @@
 
 T16244.hs:12:18: error:
-    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
-      ‘k1’ is a rigid type variable bound by
+    • Expected kind ‘k1’, but ‘b’ has kind ‘k2’
+      ‘k2’ is a rigid type variable bound by
         the class declaration for ‘C’
         at T16244.hs:12:26
-      ‘k’ is a rigid type variable bound by
+      ‘k1’ is a rigid type variable bound by
         the class declaration for ‘C’
         at T16244.hs:12:1-52
     • In the second argument of ‘SameKind’, namely ‘b’
diff --git a/testsuite/tests/polykinds/T16245.stderr b/testsuite/tests/polykinds/T16245.stderr
index 36f9d487e2..09cb055f3b 100644
--- a/testsuite/tests/polykinds/T16245.stderr
+++ b/testsuite/tests/polykinds/T16245.stderr
@@ -1,10 +1,10 @@
 
 T16245.hs:12:36: error:
-    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
-      ‘k1’ is a rigid type variable bound by
+    • Expected kind ‘k1’, but ‘b’ has kind ‘k2’
+      ‘k2’ is a rigid type variable bound by
         the class declaration for ‘C’
         at T16245.hs:12:45
-      ‘k’ is a rigid type variable bound by
+      ‘k1’ is a rigid type variable bound by
         the class declaration for ‘C’
         at T16245.hs:12:1-62
     • In the second argument of ‘SameKind’, namely ‘b’
diff --git a/testsuite/tests/polykinds/T16245a.stderr b/testsuite/tests/polykinds/T16245a.stderr
index c47e088434..00f300fdab 100644
--- a/testsuite/tests/polykinds/T16245a.stderr
+++ b/testsuite/tests/polykinds/T16245a.stderr
@@ -1,10 +1,10 @@
 
 T16245a.hs:11:66: error:
-    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
-      ‘k1’ is a rigid type variable bound by
+    • Expected kind ‘k1’, but ‘b’ has kind ‘k2’
+      ‘k2’ is a rigid type variable bound by
         the newtype declaration for ‘T’
         at T16245a.hs:11:12
-      ‘k’ is a rigid type variable bound by
+      ‘k1’ is a rigid type variable bound by
         the newtype declaration for ‘T’
         at T16245a.hs:11:1-67
     • In the second argument of ‘SameKind’, namely ‘b’
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index ff1e74cc27..f3ce4851ab 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -1,20 +1,20 @@
 
 T7438.hs:6:14: error:
-    • Could not deduce (p ~ p1)
+    • Could not deduce (p1 ~ p2)
       from the context: b ~ a
         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
-      ‘p’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> p -> p1
-        at T7438.hs:6:1-16
       ‘p1’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> p -> p1
+        the inferred type of go :: Thrist a b -> p1 -> p2
+        at T7438.hs:6:1-16
+      ‘p2’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> p1 -> p2
         at T7438.hs:6:1-16
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
     • Relevant bindings include
-        acc :: p (bound at T7438.hs:6:8)
-        go :: Thrist a b -> p -> p1 (bound at T7438.hs:6:1)
+        acc :: p1 (bound at T7438.hs:6:8)
+        go :: Thrist a b -> p1 -> p2 (bound at T7438.hs:6:1)
     Suggested fix: Consider giving ‘go’ a type signature
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index b18efe0111..2070ea667e 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -1,14 +1,15 @@
 
 T9017.hs:8:7: error:
-    • Couldn't match kind ‘k’ with ‘*’
+    • Couldn't match kind ‘k1’ with ‘*’
       When matching types
         a0 :: * -> * -> *
-        a :: k -> k1 -> *
+        a :: k1 -> k2 -> *
       Expected: a b (m b)
         Actual: a0 b0 (m0 b0)
-      ‘k’ is a rigid type variable bound by
+      ‘k1’ is a rigid type variable bound by
         the type signature for:
-          foo :: forall {k} {k1} (a :: k -> k1 -> *) (b :: k) (m :: k -> k1).
+          foo :: forall {k1} {k2} (a :: k1 -> k2 -> *) (b :: k1)
+                        (m :: k1 -> k2).
                  a b (m b)
         at T9017.hs:7:1-16
     • In the expression: arr return
diff --git a/testsuite/tests/rename/should_fail/T2993.stderr b/testsuite/tests/rename/should_fail/T2993.stderr
index 67dadf14bc..d993c398ca 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
+    Variable not in scope: (<**>) :: t1 -> (a -> a) -> t2
     Suggested fix: Perhaps use ‘<*>’ (imported from Prelude)
diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr
index b0d4ef7f25..dcf7573d8e 100644
--- a/testsuite/tests/typecheck/should_compile/tc141.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc141.stderr
@@ -37,13 +37,13 @@ tc141.hs:13:13: error:
         in v
 
 tc141.hs:15:18: error:
-    • Couldn't match expected type ‘a1’ with actual type ‘p1’
+    • Couldn't match expected type ‘a1’ with actual type ‘p2’
       ‘a1’ is a rigid type variable bound by
         the type signature for:
           v :: forall a1. a1
         at tc141.hs:14:14-19
-      ‘p1’ is a rigid type variable bound by
-        the inferred type of g :: p -> p1 -> a
+      ‘p2’ is a rigid type variable bound by
+        the inferred type of g :: p1 -> p2 -> a
         at tc141.hs:(13,1)-(16,13)
     • In the expression: b
       In an equation for ‘v’: v = b
@@ -54,5 +54,5 @@ tc141.hs:15:18: error:
         in v
     • Relevant bindings include
         v :: a1 (bound at tc141.hs:15:14)
-        b :: p1 (bound at tc141.hs:13:5)
-        g :: p -> p1 -> a (bound at tc141.hs:13:1)
+        b :: p2 (bound at tc141.hs:13:5)
+        g :: p1 -> p2 -> 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 762f666153..082cf3d96d 100644
--- a/testsuite/tests/typecheck/should_compile/tc168.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc168.stderr
@@ -1,9 +1,9 @@
 
 tc168.hs:17:1: error:
-    • Could not deduce (C a (a1, b0))
-      from the context: C a (a1, b)
+    • Could not deduce (C a1 (a2, b0))
+      from the context: C a1 (a2, b)
         bound by the inferred type for ‘g’:
-                   forall {a} {a1} {b}. C a (a1, b) => a -> a1
+                   forall {a1} {a2} {b}. C a1 (a2, b) => a1 -> a2
         at tc168.hs:17:1-16
       The type variable ‘b0’ is ambiguous
     • In the ambiguity check for the inferred type for ‘g’
diff --git a/testsuite/tests/typecheck/should_fail/T10619.stderr b/testsuite/tests/typecheck/should_fail/T10619.stderr
index 6f584b90db..0274ce91c7 100644
--- a/testsuite/tests/typecheck/should_fail/T10619.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10619.stderr
@@ -3,7 +3,7 @@ T10619.hs:10:14: error:
     • Couldn't match type ‘p1’ with ‘forall a. a -> a’
       Expected: (forall a. a -> a) -> forall b. b -> b
         Actual: p1 -> p1
-      Cannot instantiate unification variable ‘p1’
+    • Cannot instantiate unification variable ‘p1’
       with a type involving polytypes: forall a. a -> a
     • In the expression: \ y -> y
       In the expression:
@@ -19,13 +19,13 @@ T10619.hs:10:14: error:
                   \ y -> y
 
 T10619.hs:14:15: error:
-    • Couldn't match type ‘p2’ with ‘forall a. a -> a’
-      Expected: p2 -> p2
+    • Couldn't match type ‘p3’ with ‘forall a. a -> a’
+      Expected: p3 -> p3
         Actual: (forall a. a -> a) -> forall b. b -> b
-      Cannot equate type variable ‘p2’
+    • Cannot equate type variable ‘p3’
       with a type involving polytypes: forall a. a -> a
-      ‘p2’ is a rigid type variable bound by
-        the inferred type of bar :: p -> p2 -> p2
+      ‘p3’ is a rigid type variable bound by
+        the inferred type of bar :: p2 -> p3 -> p3
         at T10619.hs:(12,1)-(14,66)
     • In the expression:
           (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
@@ -41,13 +41,13 @@ T10619.hs:14:15: error:
               else
                   ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
     • Relevant bindings include
-        bar :: p -> p2 -> p2 (bound at T10619.hs:12:1)
+        bar :: p2 -> p3 -> p3 (bound at T10619.hs:12:1)
 
 T10619.hs:17:13: error:
     • Couldn't match type ‘p0’ with ‘forall a. a -> a’
       Expected: (forall a. a -> a) -> forall b. b -> b
         Actual: p0 -> p0
-      Cannot instantiate unification variable ‘p0’
+    • Cannot instantiate unification variable ‘p0’
       with a type involving polytypes: forall a. a -> a
     • In the expression: \ y -> y
       In an equation for ‘baz’: baz False = \ y -> y
@@ -56,7 +56,7 @@ T10619.hs:20:14: error:
     • Couldn't match type ‘p’ with ‘forall a. a -> a’
       Expected: p -> p
         Actual: (forall a. a -> a) -> forall b. b -> b
-      Cannot equate type variable ‘p’
+    • Cannot equate type variable ‘p’
       with a type involving polytypes: forall a. a -> a
       ‘p’ is a rigid type variable bound by
         the inferred type of quux :: Bool -> p -> p
diff --git a/testsuite/tests/typecheck/should_fail/T10709.stderr b/testsuite/tests/typecheck/should_fail/T10709.stderr
index aa4d505bfc..543cc05a38 100644
--- a/testsuite/tests/typecheck/should_fail/T10709.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10709.stderr
@@ -1,27 +1,27 @@
 
 T10709.hs:6:21: error:
-    • Couldn't match type ‘a’
-                     with ‘(forall a3. IO a3 -> IO a3) -> IO a2’
-      Expected: a -> IO a2
-        Actual: ((forall a. IO a -> IO a) -> IO a2) -> IO a2
-      Cannot equate type variable ‘a’
+    • Couldn't match type ‘a2’
+                     with ‘(forall a4. IO a4 -> IO a4) -> IO a3’
+      Expected: a2 -> IO a3
+        Actual: ((forall a. IO a -> IO a) -> IO a3) -> IO a3
+    • Cannot equate type variable ‘a2’
       with a type involving polytypes:
-        (forall a3. IO a3 -> IO a3) -> IO a2
-      ‘a’ is a rigid type variable bound by
-        the inferred type of x1 :: a -> IO [a2]
+        (forall a4. IO a4 -> IO a4) -> IO a3
+      ‘a2’ is a rigid type variable bound by
+        the inferred type of x1 :: a2 -> IO [a3]
         at T10709.hs:6:1-24
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: replicateM 2 . mask
       In an equation for ‘x1’: x1 = replicateM 2 . mask
     • Relevant bindings include
-        x1 :: a -> IO [a2] (bound at T10709.hs:6:1)
+        x1 :: a2 -> IO [a3] (bound at T10709.hs:6:1)
 
 T10709.hs:7:22: error:
     • Couldn't match type ‘a1’
                      with ‘(forall a2. IO a2 -> IO a2) -> IO a’
       Expected: a1 -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
-      Cannot instantiate unification variable ‘a1’
+    • Cannot instantiate unification variable ‘a1’
       with a type involving polytypes:
         (forall a2. IO a2 -> IO a2) -> IO a
     • In the second argument of ‘(.)’, namely ‘mask’
@@ -34,7 +34,7 @@ T10709.hs:8:22: error:
                      with ‘(forall a2. IO a2 -> IO a2) -> IO a’
       Expected: a0 -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
-      Cannot instantiate unification variable ‘a0’
+    • Cannot instantiate unification variable ‘a0’
       with a type involving polytypes:
         (forall a2. IO a2 -> IO a2) -> IO a
     • In the second argument of ‘(.)’, namely ‘mask’
diff --git a/testsuite/tests/typecheck/should_fail/T12177.stderr b/testsuite/tests/typecheck/should_fail/T12177.stderr
index 4ca175b5de..e3262d3e31 100644
--- a/testsuite/tests/typecheck/should_fail/T12177.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12177.stderr
@@ -1,26 +1,26 @@
 
 T12177.hs:3:19: error:
-    • Found hole: _ :: p2
-      Where: ‘p2’ is a rigid type variable bound by
-               the inferred type of bar :: p -> p1 -> p2
+    • Found hole: _ :: p3
+      Where: ‘p3’ is a rigid type variable bound by
+               the inferred type of bar :: p1 -> p2 -> p3
                at T12177.hs:3:1-19
     • 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 -> p2 (bound at T12177.hs:3:1)
+        x :: p2 (bound at T12177.hs:3:14)
+        bar :: p1 -> p2 -> p3 (bound at T12177.hs:3:1)
 
 T12177.hs:5:37: error:
-    • Found hole: _ :: p5
-      Where: ‘p5’ is a rigid type variable bound by
-               the inferred type of baz :: p -> p1 -> p2 -> p3 -> p4 -> p5
+    • Found hole: _ :: p6
+      Where: ‘p6’ is a rigid type variable bound by
+               the inferred type of baz :: p1 -> p2 -> p3 -> p4 -> p5 -> p6
                at T12177.hs:5:1-37
     • 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)
-        y :: p1 (bound at T12177.hs:5:14)
-        baz :: p -> p1 -> p2 -> p3 -> p4 -> p5 (bound at T12177.hs:5:1)
+        z :: p5 (bound at T12177.hs:5:32)
+        x :: p4 (bound at T12177.hs:5:26)
+        y :: p2 (bound at T12177.hs:5:14)
+        baz :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 (bound at T12177.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/T14904a.stderr b/testsuite/tests/typecheck/should_fail/T14904a.stderr
index 089e7bedeb..95aee86ee4 100644
--- a/testsuite/tests/typecheck/should_fail/T14904a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14904a.stderr
@@ -1,9 +1,9 @@
 
 T14904a.hs:10:6: error:
-    • Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k’
-      Cannot equate type variable ‘k’
-      with a kind involving polytypes: forall (a :: k1). g a
-      ‘k’ is a rigid type variable bound by
+    • Expected kind ‘forall (a :: k2). g a’, but ‘f’ has kind ‘k1’
+    • Cannot equate type variable ‘k1’
+      with a kind involving polytypes: forall (a :: k2). g a
+      ‘k1’ is a rigid type variable bound by
         a family instance declaration
         at T14904a.hs:10:3-30
     • In the first argument of ‘F’, namely ‘(f :: forall a. g a)’
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index 1cb76d317f..e35f71b28e 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,11 +1,11 @@
 
 T5853.hs:15:52: error:
-    • Could not deduce (Subst fa1 (Elem fb) ~ fb)
+    • Could not deduce (Subst fa2 (Elem fb) ~ fb)
         arising from a use of ‘<$>’
-      from the context: (F fa, Elem fb ~ Elem fb,
-                         Subst fa (Elem fb) ~ fb, Subst fb (Elem fa) ~ fa, F fa1,
-                         Elem fa1 ~ Elem fa1, Elem fa ~ Elem fa, Subst fa1 (Elem fa) ~ fa,
-                         Subst fa (Elem fa1) ~ fa1)
+      from the context: (F fa1, Elem fb ~ Elem fb,
+                         Subst fa1 (Elem fb) ~ fb, Subst fb (Elem fa1) ~ fa1, F fa2,
+                         Elem fa2 ~ Elem fa2, Elem fa1 ~ Elem fa1,
+                         Subst fa2 (Elem fa1) ~ fa1, Subst fa1 (Elem fa2) ~ fa2)
         bound by the RULE "map/map" at T5853.hs:15:2-57
       ‘fb’ is a rigid type variable bound by
         the RULE "map/map"
@@ -13,6 +13,6 @@ T5853.hs:15:52: error:
     • In the expression: (f . g) <$> xs
       When checking the rewrite rule "map/map"
     • Relevant bindings include
-        f :: Elem fa -> Elem fb (bound at T5853.hs:15:19)
-        g :: Elem fa1 -> Elem fa (bound at T5853.hs:15:21)
-        xs :: fa1 (bound at T5853.hs:15:23)
+        f :: Elem fa1 -> Elem fb (bound at T5853.hs:15:19)
+        g :: Elem fa2 -> Elem fa1 (bound at T5853.hs:15:21)
+        xs :: fa2 (bound at T5853.hs:15:23)
diff --git a/testsuite/tests/typecheck/should_fail/T7734.stderr b/testsuite/tests/typecheck/should_fail/T7734.stderr
index f47fd3b393..1dfe6b641c 100644
--- a/testsuite/tests/typecheck/should_fail/T7734.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7734.stderr
@@ -1,24 +1,24 @@
 
 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
+    • Couldn't match expected type ‘t1’ with actual type ‘t1 -> t2’
+      ‘t1’ is a rigid type variable bound by
+        the inferred type of f :: (t1 -> t2) -> p -> t2
         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
     • Relevant bindings include
-        x :: t -> t1 (bound at T7734.hs:4:1)
-        f :: (t -> t1) -> p -> t1 (bound at T7734.hs:4:3)
+        x :: t1 -> t2 (bound at T7734.hs:4:1)
+        f :: (t1 -> t2) -> p -> t2 (bound at T7734.hs:4:3)
 
 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
+    • Couldn't match expected type ‘t1’ with actual type ‘t1 -> t2’
+      ‘t1’ is a rigid type variable bound by
+        the inferred type of & :: (t1 -> t2) -> p -> t2
         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
     • Relevant bindings include
-        x :: t -> t1 (bound at T7734.hs:5:5)
-        (&) :: (t -> t1) -> p -> t1 (bound at T7734.hs:5:1)
+        x :: t1 -> t2 (bound at T7734.hs:5:5)
+        (&) :: (t1 -> t2) -> p -> t2 (bound at T7734.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/mc25.stderr b/testsuite/tests/typecheck/should_fail/mc25.stderr
index f4e992f9e7..fe1b08f152 100644
--- a/testsuite/tests/typecheck/should_fail/mc25.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc25.stderr
@@ -1,9 +1,9 @@
 
 mc25.hs:9:46: error:
-    • Couldn't match type ‘Int’ with ‘a -> t1’
-      Expected: (a -> t1) -> [a] -> [t a]
+    • Couldn't match type ‘Int’ with ‘a -> t2’
+      Expected: (a -> t2) -> [a] -> [t1 a]
         Actual: Int -> [a] -> [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 :: [t t1] (bound at mc25.hs:9:1)
+    • Relevant bindings include z :: [t1 t2] (bound at mc25.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail013.stderr b/testsuite/tests/typecheck/should_fail/tcfail013.stderr
index e870b18ced..ee3c128012 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 ‘[a]’ with actual type ‘Bool’
+    • Couldn't match expected type ‘[a1]’ with actual type ‘Bool’
     • In the pattern: True
       In an equation for ‘f’: f True = 2
     • Relevant bindings include
-        f :: [a] -> a1 (bound at tcfail013.hs:3:1)
+        f :: [a1] -> a2 (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 5525e01510..d33c12c69c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail014.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail014.stderr
@@ -1,12 +1,12 @@
 
 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
+    • Couldn't match expected type ‘t5’ with actual type ‘t5 -> t6’
+      ‘t5’ is a rigid type variable bound by
+        the inferred type of h :: (t5 -> t6) -> t6
         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
     • Relevant bindings include
-        z :: t4 -> t5 (bound at tcfail014.hs:5:27)
-        h :: (t4 -> t5) -> t5 (bound at tcfail014.hs:5:25)
+        z :: t5 -> t6 (bound at tcfail014.hs:5:27)
+        h :: (t5 -> t6) -> t6 (bound at tcfail014.hs:5:25)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail049.stderr b/testsuite/tests/typecheck/should_fail/tcfail049.stderr
index 1b74ce0070..864b3cc1d7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail049.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail049.stderr
@@ -1,2 +1,2 @@
 
-tcfail049.hs:3:7: error: Variable not in scope: g :: t -> t1
+tcfail049.hs:3:7: error: Variable not in scope: g :: t1 -> t2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail050.stderr b/testsuite/tests/typecheck/should_fail/tcfail050.stderr
index 2ca5065938..8ddfb10cfc 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail050.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail050.stderr
@@ -1,3 +1,3 @@
 
 tcfail050.hs:3:7: error:
-    Data constructor not in scope: B :: t -> t1
+    Data constructor not in scope: B :: t1 -> t2