Major patch to introduce TyConBinder

Before this patch, following the TypeInType innovations,
each TyCon had two lists:
  - tyConBinders :: [TyBinder]
  - tyConTyVars  :: [TyVar]

They were in 1-1 correspondence and contained
overlapping information.  More broadly, there were many
places where we had to pass around this pair of lists,
instead of a single list.

This commit tidies all that up, by having just one list of
binders in a TyCon:

  - tyConBinders :: [TyConBinder]

The new data types look like this:

  Var.hs:
     data TyVarBndr tyvar vis = TvBndr tyvar vis
     data VisibilityFlag = Visible | Specified | Invisible
     type TyVarBinder = TyVarBndr TyVar VisibilityFlag

  TyCon.hs:
     type TyConBinder = TyVarBndr TyVar TyConBndrVis

     data TyConBndrVis
       = NamedTCB VisibilityFlag
       | AnonTCB

  TyCoRep.hs:
     data TyBinder
       = Named TyVarBinder
       | Anon Type

Note that Var.TyVarBdr has moved from TyCoRep and has been
made polymorphic in the tyvar and visiblity fields:

     type TyVarBinder = TyVarBndr TyVar VisibilityFlag
        -- Used in ForAllTy
     type TyConBinder = TyVarBndr TyVar TyConBndrVis
        -- Used in TyCon

     type IfaceForAllBndr  = TyVarBndr IfaceTvBndr VisibilityFlag
     type IfaceTyConBinder = TyVarBndr IfaceTvBndr TyConBndrVis
         -- Ditto, in interface files

There are a zillion knock-on changes, but everything
arises from these types.  It was a bit fiddly to get the
module loops to work out right!

Some smaller points
~~~~~~~~~~~~~~~~~~~
* Nice new functions
    TysPrim.mkTemplateKiTyVars
    TysPrim.mkTemplateTyConBinders
  which help you make the tyvar binders for dependently-typed
  TyCons.  See comments with their definition.

* The change showed up a bug in TcGenGenerics.tc_mkRepTy, where the code
  was making an assumption about the order of the kind variables in the
  kind of GHC.Generics.(:.:).  I fixed this; see TcGenGenerics.mkComp.

56 files changed, 436 insertions, 456 deletions

diff --git a/testsuite/tests/ado/ado002.stderr b/testsuite/tests/ado/ado002.stderr
index 9e7eba0a67..fe730f6c91 100644
--- a/testsuite/tests/ado/ado002.stderr
+++ b/testsuite/tests/ado/ado002.stderr
@@ -1,6 +1,6 @@
 
 ado002.hs:8:8: error:
-    • Couldn't match expected type ‘Char -> IO t1’
+    • Couldn't match expected type ‘Char -> IO b0’
                   with actual type ‘IO Char’
     • The function ‘getChar’ is applied to one argument,
       but its type ‘IO Char’ has none
diff --git a/testsuite/tests/driver/werror.stderr b/testsuite/tests/driver/werror.stderr
index 8f2e6035db..ae18bb62f0 100644
--- a/testsuite/tests/driver/werror.stderr
+++ b/testsuite/tests/driver/werror.stderr
@@ -18,7 +18,7 @@ werror.hs:10:1: warning: [-Wunused-top-binds (in -Wextra, -Wunused-binds)]
 
 werror.hs:10:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      f :: forall t t1. [t1] -> [t]
+      f :: forall a a1. [a1] -> [a]
 
 werror.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index 06b1f9c720..e304430b51 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -1,17 +1,17 @@
-

-gadt13.hs:15:13: error:

-    • Couldn't match expected type ‘t’

-                  with actual type ‘String -> [Char]’

-        ‘t’ is untouchable

-          inside the constraints: t1 ~ Int

-          bound by a pattern with constructor: I :: Int -> Term Int,

-                   in an equation for ‘shw’

-          at gadt13.hs:15:6-8

-      ‘t’ is a rigid type variable bound by

-        the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1-30

-      Possible fix: add a type signature for ‘shw’

-    • Possible cause: ‘(.)’ is applied to too many arguments

-      In the expression: ("I " ++) . shows t

-      In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t

-    • Relevant bindings include

-        shw :: Term t1 -> t (bound at gadt13.hs:15:1)

+
+gadt13.hs:15:13: error:
+    • Couldn't match expected type ‘t’
+                  with actual type ‘String -> [Char]’
+        ‘t’ is untouchable
+          inside the constraints: a ~ Int
+          bound by a pattern with constructor: I :: Int -> Term Int,
+                   in an equation for ‘shw’
+          at gadt13.hs:15:6-8
+      ‘t’ is a rigid type variable bound by
+        the inferred type of shw :: Term a -> t at gadt13.hs:15:1-30
+      Possible fix: add a type signature for ‘shw’
+    • Possible cause: ‘(.)’ is applied to too many arguments
+      In the expression: ("I " ++) . shows t
+      In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
+    • Relevant bindings include
+        shw :: Term a -> t (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index 6e1effa067..e66226eaea 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,20 +1,20 @@
-

-gadt7.hs:16:38: error:

-    • Couldn't match expected type ‘t’ with actual type ‘t1’

-        ‘t’ is untouchable

-          inside the constraints: t2 ~ Int

-          bound by a pattern with constructor: K :: T Int,

-                   in a case alternative

-          at gadt7.hs:16:33

-      ‘t’ is a rigid type variable bound by

-        the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1-44

-      ‘t1’ is a rigid type variable bound by

-        the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1-44

-      Possible fix: add a type signature for ‘i1b’

-    • In the expression: y1

-      In a case alternative: K -> y1

-      In the expression: case t1 of { K -> y1 }

-    • Relevant bindings include

-        y1 :: t1 (bound at gadt7.hs:16:16)

-        y :: t1 (bound at gadt7.hs:16:7)

-        i1b :: T t2 -> t1 -> t (bound at gadt7.hs:16:1)

+
+gadt7.hs:16:38: error:
+    • Couldn't match expected type ‘t’ with actual type ‘t1’
+        ‘t’ is untouchable
+          inside the constraints: a ~ Int
+          bound by a pattern with constructor: K :: T Int,
+                   in a case alternative
+          at gadt7.hs:16:33
+      ‘t’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44
+      ‘t1’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44
+      Possible fix: add a type signature for ‘i1b’
+    • In the expression: y1
+      In a case alternative: K -> y1
+      In the expression: case t1 of { K -> y1 }
+    • Relevant bindings include
+        y1 :: t1 (bound at gadt7.hs:16:16)
+        y :: t1 (bound at gadt7.hs:16:7)
+        i1b :: T a -> t1 -> t (bound at gadt7.hs:16:1)
diff --git a/testsuite/tests/generics/T10604/T10604_deriving.stderr b/testsuite/tests/generics/T10604/T10604_deriving.stderr
index b4168d1bdd..cecb2ce308 100644
--- a/testsuite/tests/generics/T10604/T10604_deriving.stderr
+++ b/testsuite/tests/generics/T10604/T10604_deriving.stderr
@@ -303,8 +303,8 @@ GHC.Generics representation types:
                                                                    'GHC.Generics.NoSourceStrictness
                                                                    'GHC.Generics.DecidedLazy)
                                                                 ((GHC.Generics.:.:)
-                                                                   (k -> GHC.Types.*)
                                                                    *
+                                                                   (k -> GHC.Types.*)
                                                                    (T10604_deriving.Proxy *)
                                                                    (GHC.Generics.Rec1
                                                                       (k -> GHC.Types.*)
diff --git a/testsuite/tests/ghci.debugger/scripts/break003.stderr b/testsuite/tests/ghci.debugger/scripts/break003.stderr
index d069493986..36398dfda1 100644
--- a/testsuite/tests/ghci.debugger/scripts/break003.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/break003.stderr
@@ -1,5 +1,5 @@
 
 <interactive>:4:1: error:
-    • No instance for (Show (t1 -> t)) arising from a use of ‘print’
+    • No instance for (Show (t -> a)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
diff --git a/testsuite/tests/ghci.debugger/scripts/break003.stdout b/testsuite/tests/ghci.debugger/scripts/break003.stdout
index 1d0844c6cc..d510a476ff 100644
--- a/testsuite/tests/ghci.debugger/scripts/break003.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break003.stdout
@@ -1,6 +1,6 @@
 Breakpoint 0 activated at ../Test3.hs:2:18-31
 Stopped in Main.mymap, ../Test3.hs:2:18-31
-_result :: [t] = _
-f :: t1 -> t = _
-x :: t1 = _
-xs :: [t1] = [_]
+_result :: [a] = _
+f :: t -> a = _
+x :: t = _
+xs :: [t] = [_]
diff --git a/testsuite/tests/ghci.debugger/scripts/break005.stdout b/testsuite/tests/ghci.debugger/scripts/break005.stdout
index 81eae63726..35e92d44f0 100644
--- a/testsuite/tests/ghci.debugger/scripts/break005.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break005.stdout
@@ -4,7 +4,7 @@ a :: Integer = 1
 left :: [Integer] = _
 right :: [Integer] = _
 Stopped in QSort.qsort, ../QSort.hs:5:17-26
-_result :: [t] = _
-left :: [t] = _
+_result :: [a] = _
+left :: [a] = _
 ()
 left = []
diff --git a/testsuite/tests/ghci.debugger/scripts/break006.stderr b/testsuite/tests/ghci.debugger/scripts/break006.stderr
index 463b66fcbf..7929e36cc2 100644
--- a/testsuite/tests/ghci.debugger/scripts/break006.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/break006.stderr
@@ -1,9 +1,9 @@
 
 <interactive>:4:1: error:
-    • No instance for (Show t) arising from a use of ‘print’
-      Cannot resolve unknown runtime type ‘t’
+    • No instance for (Show a) arising from a use of ‘print’
+      Cannot resolve unknown runtime type ‘a’
       Use :print or :force to determine these types
-      Relevant bindings include it :: t (bound at <interactive>:4:1)
+      Relevant bindings include it :: a (bound at <interactive>:4:1)
       These potential instances exist:
         instance (Show b, Show a) => Show (Either a b)
           -- Defined in ‘Data.Either’
@@ -15,10 +15,10 @@
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:6:1: error:
-    • No instance for (Show t) arising from a use of ‘print’
-      Cannot resolve unknown runtime type ‘t’
+    • No instance for (Show a) arising from a use of ‘print’
+      Cannot resolve unknown runtime type ‘a’
       Use :print or :force to determine these types
-      Relevant bindings include it :: t (bound at <interactive>:6:1)
+      Relevant bindings include it :: a (bound at <interactive>:6:1)
       These potential instances exist:
         instance (Show b, Show a) => Show (Either a b)
           -- Defined in ‘Data.Either’
diff --git a/testsuite/tests/ghci.debugger/scripts/break006.stdout b/testsuite/tests/ghci.debugger/scripts/break006.stdout
index d8f1b65864..35fa44564c 100644
--- a/testsuite/tests/ghci.debugger/scripts/break006.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break006.stdout
@@ -1,13 +1,13 @@
 Stopped in Main.mymap, ../Test3.hs:2:18-31
-_result :: [t] = _
-f :: Integer -> t = _
+_result :: [a] = _
+f :: Integer -> a = _
 x :: Integer = 1
 xs :: [Integer] = [2,3]
 xs :: [Integer] = [2,3]
 x :: Integer = 1
-f :: Integer -> t = _
-_result :: [t] = _
-y = (_t1::t)
+f :: Integer -> a = _
+_result :: [a] = _
+y = (_t1::a)
 y = 2
 xs :: [Integer] = [2,3]
 x :: Integer = 1
diff --git a/testsuite/tests/ghci.debugger/scripts/hist001.stdout b/testsuite/tests/ghci.debugger/scripts/hist001.stdout
index 7ef5dc1e8e..9ae5688cb0 100644
--- a/testsuite/tests/ghci.debugger/scripts/hist001.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/hist001.stdout
@@ -9,25 +9,25 @@ _result :: [a] = _
 -6  : mymap (../Test3.hs:2:18-31)
 <end of history>
 Logged breakpoint at ../Test3.hs:2:22-31
-_result :: [t]
-f :: t1 -> t
-xs :: [t1]
-xs :: [t1] = []
-f :: t1 -> t = _
-_result :: [t] = _
+_result :: [a]
+f :: t -> a
+xs :: [t]
+xs :: [t] = []
+f :: t -> a = _
+_result :: [a] = _
 Logged breakpoint at ../Test3.hs:2:18-20
-_result :: t
-f :: Integer -> t
+_result :: a
+f :: Integer -> a
 x :: Integer
-xs :: [t1] = []
+xs :: [t] = []
 x :: Integer = 2
-f :: Integer -> t = _
-_result :: t = _
+f :: Integer -> a = _
+_result :: a = _
 _result = 3
 Logged breakpoint at ../Test3.hs:2:18-31
-_result :: [t]
-f :: Integer -> t
+_result :: [a]
+f :: Integer -> a
 x :: Integer
 xs :: [Integer]
 Logged breakpoint at ../Test3.hs:2:18-20
-_result :: t
+_result :: a
diff --git a/testsuite/tests/ghci/prog010/ghci.prog010.stdout b/testsuite/tests/ghci/prog010/ghci.prog010.stdout
index 0cc49e23d5..8434b21e18 100644
--- a/testsuite/tests/ghci/prog010/ghci.prog010.stdout
+++ b/testsuite/tests/ghci/prog010/ghci.prog010.stdout
@@ -1,7 +1,7 @@
-f :: t -> [t]
+f :: a -> [a]
 g :: a -> Maybe a
-f :: t -> [t]
-f :: t -> [t]
+f :: a -> [a]
+f :: a -> [a]
 g :: a -> Maybe a
-f :: t -> [t]
+f :: a -> [a]
 g :: a -> Maybe a
diff --git a/testsuite/tests/ghci/scripts/T11524a.stdout b/testsuite/tests/ghci/scripts/T11524a.stdout
index 0a9dddbaec..164e0cf256 100644
--- a/testsuite/tests/ghci/scripts/T11524a.stdout
+++ b/testsuite/tests/ghci/scripts/T11524a.stdout
@@ -3,11 +3,11 @@ without -fprint-explicit-foralls
 pattern P :: Bool 	-- Defined at <interactive>:16:1
 pattern Pe :: a -> Ex 	-- Defined at <interactive>:17:1
 pattern Pu :: t -> t 	-- Defined at <interactive>:18:1
-pattern Pue :: t -> a -> (t, Ex) 	-- Defined at <interactive>:19:1
+pattern Pue :: a -> a1 -> (a, Ex) 	-- Defined at <interactive>:19:1
 pattern Pur :: (Num a, Eq a) => a -> [a]
   	-- Defined at <interactive>:20:1
-pattern Purp :: (Num a, Eq a) => Show t => a
-                                           -> t -> ([a], UnivProv t)
+pattern Purp :: (Num a1, Eq a1) => Show a => a1
+                                             -> a -> ([a1], UnivProv a)
   	-- Defined at <interactive>:21:1
 pattern Pure :: (Num a, Eq a) => a -> a1 -> ([a], Ex)
   	-- Defined at <interactive>:22:1
@@ -16,9 +16,9 @@ pattern Purep :: (Num a, Eq a) => Show a1 => a
   	-- Defined at <interactive>:23:1
 pattern Pep :: () => Show a => a -> ExProv
   	-- Defined at <interactive>:24:1
-pattern Pup :: () => Show t => t -> UnivProv t
+pattern Pup :: () => Show a => a -> UnivProv a
   	-- Defined at <interactive>:25:1
-pattern Puep :: () => Show a => a -> t -> (ExProv, t)
+pattern Puep :: () => Show a => a -> b -> (ExProv, b)
   	-- Defined at <interactive>:26:1
 
 with -fprint-explicit-foralls
@@ -27,12 +27,12 @@ pattern P :: Bool 	-- Defined at <interactive>:16:1
 pattern Pe :: () => forall {a}. a -> Ex
   	-- Defined at <interactive>:17:1
 pattern Pu :: forall {t}. t -> t 	-- Defined at <interactive>:18:1
-pattern Pue :: forall {t}. () => forall {a}. t -> a -> (t, Ex)
+pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex)
   	-- Defined at <interactive>:19:1
 pattern Pur :: forall {a}. (Num a, Eq a) => a -> [a]
   	-- Defined at <interactive>:20:1
-pattern Purp :: forall {t} {a}. (Num a, Eq a) => Show t => a
-                                                           -> t -> ([a], UnivProv t)
+pattern Purp :: forall {a} {a1}. (Num a1, Eq a1) => Show a => a1
+                                                              -> a -> ([a1], UnivProv a)
   	-- Defined at <interactive>:21:1
 pattern Pure :: forall {a}. (Num a, Eq a) => forall {a1}. a
                                                           -> a1 -> ([a], Ex)
@@ -42,8 +42,8 @@ pattern Purep :: forall {a}. (Num a, Eq a) => forall {a1}. Show
   	-- Defined at <interactive>:23:1
 pattern Pep :: () => forall {a}. Show a => a -> ExProv
   	-- Defined at <interactive>:24:1
-pattern Pup :: forall {t}. () => Show t => t -> UnivProv t
+pattern Pup :: forall {a}. () => Show a => a -> UnivProv a
   	-- Defined at <interactive>:25:1
-pattern Puep :: forall {t}. () => forall {a}. Show a => a
-                                                        -> t -> (ExProv, t)
+pattern Puep :: forall {b}. () => forall {a}. Show a => a
+                                                        -> b -> (ExProv, b)
   	-- Defined at <interactive>:26:1
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index f06760eed7..048f45d288 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -49,7 +49,7 @@
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    Kind variable ‘k1’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at <interactive>:60:15
diff --git a/testsuite/tests/ghci/scripts/T7627.stdout b/testsuite/tests/ghci/scripts/T7627.stdout
index 81a360facb..2dfae3749f 100644
--- a/testsuite/tests/ghci/scripts/T7627.stdout
+++ b/testsuite/tests/ghci/scripts/T7627.stdout
@@ -25,9 +25,9 @@ instance Foldable ((,) a) -- Defined in ‘Data.Foldable’
 instance Traversable ((,) a) -- Defined in ‘Data.Traversable’
 instance (Monoid a, Monoid b) => Monoid (a, b)
   -- Defined in ‘GHC.Base’
-data (#,#) (c :: TYPE a) (d :: TYPE b) = (#,#) c d
+data (#,#) (a :: TYPE k0) (b :: TYPE k1) = (#,#) a b
   	-- Defined in ‘GHC.Prim’
 (,) :: a -> b -> (a, b)
-(#,#) :: c -> d -> (# c, d #)
+(#,#) :: a -> b -> (# a, b #)
 (  ,  ) :: a -> b -> (a, b)
-(#  ,  #) :: c -> d -> (# c, d #)
+(#  ,  #) :: a -> b -> (# a, b #)
diff --git a/testsuite/tests/ghci/scripts/T8535.stdout b/testsuite/tests/ghci/scripts/T8535.stdout
index 6eb08cdfe4..2f35e23a77 100644
--- a/testsuite/tests/ghci/scripts/T8535.stdout
+++ b/testsuite/tests/ghci/scripts/T8535.stdout
@@ -1,4 +1,4 @@
-data (->) t1 t2 	-- Defined in ‘GHC.Prim’
+data (->) a b 	-- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/scripts/T8776.stdout b/testsuite/tests/ghci/scripts/T8776.stdout
index d0d9bd5240..1fe5d797b6 100644
--- a/testsuite/tests/ghci/scripts/T8776.stdout
+++ b/testsuite/tests/ghci/scripts/T8776.stdout
@@ -1,2 +1,2 @@
-pattern P :: () => (Num t1, Eq t) => A t1 t
+pattern P :: () => (Num x, Eq y) => A x y
   	-- Defined at T8776.hs:6:1
diff --git a/testsuite/tests/ghci/scripts/ghci013.stdout b/testsuite/tests/ghci/scripts/ghci013.stdout
index d6c3823fdd..695aaafc53 100644
--- a/testsuite/tests/ghci/scripts/ghci013.stdout
+++ b/testsuite/tests/ghci/scripts/ghci013.stdout
@@ -1 +1 @@
-f :: Monad m => (m a, t) -> m b
+f :: Monad m => (m a, b) -> m b1
diff --git a/testsuite/tests/ghci/scripts/ghci020.stdout b/testsuite/tests/ghci/scripts/ghci020.stdout
index 6eb08cdfe4..2f35e23a77 100644
--- a/testsuite/tests/ghci/scripts/ghci020.stdout
+++ b/testsuite/tests/ghci/scripts/ghci020.stdout
@@ -1,4 +1,4 @@
-data (->) t1 t2 	-- Defined in ‘GHC.Prim’
+data (->) a b 	-- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/scripts/ghci059.stdout b/testsuite/tests/ghci/scripts/ghci059.stdout
index fac61163f4..3cb103c9f5 100644
--- a/testsuite/tests/ghci/scripts/ghci059.stdout
+++ b/testsuite/tests/ghci/scripts/ghci059.stdout
@@ -1,4 +1,4 @@
 type role Coercible representational representational
-class a ~R# b => Coercible (a :: k) (b :: k)
+class a ~R# b => Coercible (a :: k0) (b :: k0)
   	-- Defined in ‘GHC.Types’
 coerce :: Coercible a b => a -> b 	-- Defined in ‘GHC.Prim’
diff --git a/testsuite/tests/ghci/should_run/T10145.stdout b/testsuite/tests/ghci/should_run/T10145.stdout
index 6eb08cdfe4..2f35e23a77 100644
--- a/testsuite/tests/ghci/should_run/T10145.stdout
+++ b/testsuite/tests/ghci/should_run/T10145.stdout
@@ -1,4 +1,4 @@
-data (->) t1 t2 	-- Defined in ‘GHC.Prim’
+data (->) a b 	-- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr
index a3489d23bd..29877bf2aa 100644
--- a/testsuite/tests/indexed-types/should_compile/T3017.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr
@@ -4,7 +4,7 @@ TYPE SIGNATURES
   emptyL :: forall a. ListColl a
   insert :: forall c. Coll c => Elem c -> c -> c
   test2 ::
-    forall t t1 c. (Elem c ~ (t, t1), Coll c, Num t, Num t1) => c -> c
+    forall a b c. (Elem c ~ (a, b), Coll c, Num a, Num b) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
     type family Elem c :: * open
diff --git a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
index f8cd07d0f7..0a1b9d37a9 100644
--- a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
@@ -1,18 +1,18 @@
 
 ExtraTcsUntch.hs:23:18: error:
-    Couldn't match expected type ‘F Int’ with actual type ‘[[t]]’
-    In the first argument of ‘h’, namely ‘[x]’
-    In the expression: h [x]
-    In an equation for ‘g1’: g1 _ = h [x]
-    Relevant bindings include
-      x :: [t] (bound at ExtraTcsUntch.hs:21:3)
-      f :: [t] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+    • Couldn't match expected type ‘F Int’ with actual type ‘[[a]]’
+    • In the first argument of ‘h’, namely ‘[x]’
+      In the expression: h [x]
+      In an equation for ‘g1’: g1 _ = h [x]
+    • Relevant bindings include
+        x :: [a] (bound at ExtraTcsUntch.hs:21:3)
+        f :: [a] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
 
 ExtraTcsUntch.hs:25:38: error:
-    Couldn't match expected type ‘F Int’ with actual type ‘[[t]]’
-    In the first argument of ‘h’, namely ‘[[undefined]]’
-    In the expression: h [[undefined]]
-    In the expression: (h [[undefined]], op x [y])
-    Relevant bindings include
-      x :: [t] (bound at ExtraTcsUntch.hs:21:3)
-      f :: [t] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+    • Couldn't match expected type ‘F Int’ with actual type ‘[[a]]’
+    • In the first argument of ‘h’, namely ‘[[undefined]]’
+      In the expression: h [[undefined]]
+      In the expression: (h [[undefined]], op x [y])
+    • Relevant bindings include
+        x :: [a] (bound at ExtraTcsUntch.hs:21:3)
+        f :: [a] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
diff --git a/testsuite/tests/parser/should_fail/T7848.stderr b/testsuite/tests/parser/should_fail/T7848.stderr
index e1a64e4668..f7617ee606 100644
--- a/testsuite/tests/parser/should_fail/T7848.stderr
+++ b/testsuite/tests/parser/should_fail/T7848.stderr
@@ -1,9 +1,9 @@
 
 T7848.hs:6:1: error:
     • Occurs check: cannot construct the infinite type:
-        t ~ t2 -> t1 -> A -> A -> A -> A -> t0 -> t
+        t ~ t0 -> t1 -> A -> A -> A -> A -> t2 -> t
     • When checking that:
-          t2 -> t1 -> A -> A -> A -> A -> forall t4. t4 -> t
+          t0 -> t1 -> A -> A -> A -> A -> forall t2. t2 -> t
         is more polymorphic than: t
     • Relevant bindings include x :: t (bound at T7848.hs:6:1)
 
diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index 3cebd8f92a..23c059e720 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -1,38 +1,34 @@
 
 T10403.hs:15:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    Found constraint wildcard ‘_’ standing for ‘Functor f’
-    In the type signature:
-      h1 :: _ => _
+    • Found type wildcard ‘_’ standing for ‘Functor f’
+      Where: ‘f’ is a rigid type variable bound by
+               the inferred type of h1 :: Functor f => (a -> b) -> f a -> H f
+               at T10403.hs:17:1-41
+    • In the type signature: h1 :: _ => _
 
 T10403.hs:15:12: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘(a -> b) -> f a -> H f’
       Where: ‘b’ is a rigid type variable bound by
                the inferred type of h1 :: Functor f => (a -> b) -> f a -> H f
-               at T10403.hs:17:1
+               at T10403.hs:17:1-41
              ‘a’ is a rigid type variable bound by
                the inferred type of h1 :: Functor f => (a -> b) -> f a -> H f
-               at T10403.hs:17:1
+               at T10403.hs:17:1-41
              ‘f’ is a rigid type variable bound by
                the inferred type of h1 :: Functor f => (a -> b) -> f a -> H f
-               at T10403.hs:17:1
-    • In the type signature:
-        h1 :: _ => _
-    • Relevant bindings include
-        h1 :: (a -> b) -> f a -> H f (bound at T10403.hs:17:1)
+               at T10403.hs:17:1-41
+    • In the type signature: h1 :: _ => _
 
 T10403.hs:19:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘(a -> b) -> f0 a -> H f0’
       Where: ‘b’ is a rigid type variable bound by
                the inferred type of h2 :: (a -> b) -> f0 a -> H f0
-               at T10403.hs:22:1
+               at T10403.hs:22:1-41
              ‘a’ is a rigid type variable bound by
                the inferred type of h2 :: (a -> b) -> f0 a -> H f0
-               at T10403.hs:22:1
+               at T10403.hs:22:1-41
              ‘f0’ is an ambiguous type variable
-    • In the type signature:
-        h2 :: _
-    • Relevant bindings include
-        h2 :: (a -> b) -> f0 a -> H f0 (bound at T10403.hs:22:1)
+    • In the type signature: h2 :: _
 
 T10403.hs:22:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Ambiguous type variable ‘f0’ arising from a use of ‘fmap’
@@ -79,4 +75,3 @@ T10403.hs:28:20: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘app2’: app2 = h2 (H . I) (B ())
     • Relevant bindings include
         app2 :: H (B t) (bound at T10403.hs:28:1)
-
diff --git a/testsuite/tests/partial-sigs/should_compile/T11192.stderr b/testsuite/tests/partial-sigs/should_compile/T11192.stderr
index c7420eb3d7..7abf6e5845 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11192.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11192.stderr
@@ -2,9 +2,8 @@
 T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Int -> t -> t’
       Where: ‘t’ is a rigid type variable bound by
-               the inferred type of go :: Int -> t -> t at T11192.hs:8:8
-    • In the type signature:
-        go :: _
+               the inferred type of go :: Int -> t -> t at T11192.hs:8:8-17
+    • In the type signature: go :: _
       In the expression:
         let
           go :: _
@@ -16,18 +15,15 @@ T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
                 go :: _
                 go 0 a = a
               in go (0 :: Int) undefined
-    • Relevant bindings include
-        go :: Int -> t -> t (bound at T11192.hs:8:8)
-        fails :: a (bound at T11192.hs:6:1)
+    • 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 ‘t -> t1 -> t1’
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of go :: t -> t1 -> t1 at T11192.hs:14:8
-             ‘t1’ is a rigid type variable bound by
-               the inferred type of go :: t -> t1 -> t1 at T11192.hs:14:8
-    • In the type signature:
-        go :: _
+    • Found type wildcard ‘_’ standing for ‘t1 -> t -> t’
+      Where: ‘t1’ is a rigid type variable bound by
+               the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17
+             ‘t’ is a rigid type variable bound by
+               the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17
+    • In the type signature: go :: _
       In the expression:
         let
           go :: _
@@ -39,7 +35,4 @@ T11192.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
                 go :: _
                 go _ a = a
               in go (0 :: Int) undefined
-    • Relevant bindings include
-        go :: t -> t1 -> t1 (bound at T11192.hs:14:8)
-        succeeds :: a (bound at T11192.hs:12:1)
-
+    • Relevant bindings include succeeds :: a (bound at T11192.hs:12:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T12033.stderr b/testsuite/tests/partial-sigs/should_compile/T12033.stderr
index 02a1233559..a3b293b0cc 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12033.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12033.stderr
@@ -1,24 +1,24 @@
-

-T12033.hs:12:22: warning: [-Wpartial-type-signatures (in -Wdefault)]

-    • Found type wildcard ‘_’ standing for ‘v -> t’

-      Where: ‘t’ is a rigid type variable bound by

-               the inferred type of

-               makeTuple :: v -> t

-               makeExpression :: v -> t

-               at T12033.hs:(11,4)-(13,39)

-             ‘v’ is a rigid type variable bound by

-               the type signature for:

-                 tripleStoreToRuleSet :: forall v. v -> v

-               at T12033.hs:6:1-30

-    • In the type signature: makeExpression :: _

-      In an equation for ‘tripleStoreToRuleSet’:

-          tripleStoreToRuleSet getAtom

-            = makeTuple getAtom

-            where

-                makeRule v = makeExpression v

-                makeTuple v = makeExpression v

-                makeExpression :: _

-                makeExpression v = makeTuple getAtom

-    • Relevant bindings include

-        getAtom :: v (bound at T12033.hs:7:22)

-        tripleStoreToRuleSet :: v -> v (bound at T12033.hs:7:1)

+
+T12033.hs:12:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘v -> t’
+      Where: ‘v’ is a rigid type variable bound by
+               the type signature for:
+                 tripleStoreToRuleSet :: forall v. v -> v
+               at T12033.hs:6:1-30
+             ‘t’ is a rigid type variable bound by
+               the inferred type of
+               makeTuple :: v -> t
+               makeExpression :: v -> t
+               at T12033.hs:(11,4)-(13,39)
+    • In the type signature: makeExpression :: _
+      In an equation for ‘tripleStoreToRuleSet’:
+          tripleStoreToRuleSet getAtom
+            = makeTuple getAtom
+            where
+                makeRule v = makeExpression v
+                makeTuple v = makeExpression v
+                makeExpression :: _
+                makeExpression v = makeTuple getAtom
+    • Relevant bindings include
+        getAtom :: v (bound at T12033.hs:7:22)
+        tripleStoreToRuleSet :: v -> v (bound at T12033.hs:7:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
index 60b5b11bde..a69c59b0dc 100644
--- a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
@@ -1,50 +1,50 @@
-TYPE SIGNATURES

-  bar :: forall w t. t -> (t -> w) -> w

-  foo :: forall a. (Show a, Enum a) => a -> String

-TYPE CONSTRUCTORS

-COERCION AXIOMS

-Dependent modules: []

-Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,

-                     integer-gmp-1.0.0.1]

-

-WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]

-    • Found type wildcard ‘_a’ standing for ‘a’

-      Where: ‘a’ is a rigid type variable bound by

-               the inferred type of foo :: (Show a, Enum a) => a -> String

-               at WarningWildcardInstantiations.hs:6:1-21

-    • In the type signature: foo :: (Show _a, _) => _a -> _

-

-WarningWildcardInstantiations.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]

-    • Found type wildcard ‘_’ standing for ‘Enum a’

-      Where: ‘a’ is a rigid type variable bound by

-               the inferred type of foo :: (Show a, Enum a) => a -> String

-               at WarningWildcardInstantiations.hs:6:1-21

-    • In the type signature: foo :: (Show _a, _) => _a -> _

-

-WarningWildcardInstantiations.hs:5:30: warning: [-Wpartial-type-signatures (in -Wdefault)]

-    • Found type wildcard ‘_’ standing for ‘String’

-    • In the type signature: foo :: (Show _a, _) => _a -> _

-

-WarningWildcardInstantiations.hs:8:8: warning: [-Wpartial-type-signatures (in -Wdefault)]

-    • Found type wildcard ‘_’ standing for ‘t’

-      Where: ‘t’ is a rigid type variable bound by

-               the inferred type of bar :: t -> (t -> w) -> w

-               at WarningWildcardInstantiations.hs:9:1-13

-    • In the type signature: bar :: _ -> _ -> _

-

-WarningWildcardInstantiations.hs:8:13: warning: [-Wpartial-type-signatures (in -Wdefault)]

-    • Found type wildcard ‘_’ standing for ‘t -> w’

-      Where: ‘w’ is a rigid type variable bound by

-               the inferred type of bar :: t -> (t -> w) -> w

-               at WarningWildcardInstantiations.hs:9:1-13

-             ‘t’ is a rigid type variable bound by

-               the inferred type of bar :: t -> (t -> w) -> w

-               at WarningWildcardInstantiations.hs:9:1-13

-    • In the type signature: bar :: _ -> _ -> _

-

-WarningWildcardInstantiations.hs:8:18: warning: [-Wpartial-type-signatures (in -Wdefault)]

-    • Found type wildcard ‘_’ standing for ‘w’

-      Where: ‘w’ is a rigid type variable bound by

-               the inferred type of bar :: t -> (t -> w) -> w

-               at WarningWildcardInstantiations.hs:9:1-13

-    • In the type signature: bar :: _ -> _ -> _

+TYPE SIGNATURES
+  bar :: forall w t. t -> (t -> w) -> w
+  foo :: forall a. (Show a, Enum a) => a -> String
+TYPE CONSTRUCTORS
+COERCION AXIOMS
+Dependent modules: []
+Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
+                     integer-gmp-1.0.0.1]
+
+WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_a’ standing for ‘a’
+      Where: ‘a’ is a rigid type variable bound by
+               the inferred type of foo :: (Show a, Enum a) => a -> String
+               at WarningWildcardInstantiations.hs:6:1-21
+    • In the type signature: foo :: (Show _a, _) => _a -> _
+
+WarningWildcardInstantiations.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Enum a’
+      Where: ‘a’ is a rigid type variable bound by
+               the inferred type of foo :: (Show a, Enum a) => a -> String
+               at WarningWildcardInstantiations.hs:6:1-21
+    • In the type signature: foo :: (Show _a, _) => _a -> _
+
+WarningWildcardInstantiations.hs:5:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘String’
+    • In the type signature: foo :: (Show _a, _) => _a -> _
+
+WarningWildcardInstantiations.hs:8:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘t’
+      Where: ‘t’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> w) -> w
+               at WarningWildcardInstantiations.hs:9:1-13
+    • In the type signature: bar :: _ -> _ -> _
+
+WarningWildcardInstantiations.hs:8:13: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘t -> w’
+      Where: ‘t’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> w) -> w
+               at WarningWildcardInstantiations.hs:9:1-13
+             ‘w’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> w) -> w
+               at WarningWildcardInstantiations.hs:9:1-13
+    • In the type signature: bar :: _ -> _ -> _
+
+WarningWildcardInstantiations.hs:8:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘w’
+      Where: ‘w’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> w) -> w
+               at WarningWildcardInstantiations.hs:9:1-13
+    • In the type signature: bar :: _ -> _ -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/T10045.stderr b/testsuite/tests/partial-sigs/should_fail/T10045.stderr
index e9cac55e9e..16a5bf876f 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10045.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10045.stderr
@@ -1,13 +1,12 @@
 
 T10045.hs:6:18: error:
-    • Found type wildcard ‘_’ standing for ‘t1 -> Bool -> t2’
-      Where: ‘t1’ is a rigid type variable bound by
-               the inferred type of copy :: t1 -> Bool -> t2 at T10045.hs:7:10
-             ‘t2’ is a rigid type variable bound by
-               the inferred type of copy :: t1 -> Bool -> t2 at T10045.hs:7:10
+    • Found type wildcard ‘_’ standing for ‘t2 -> Bool -> t1’
+      Where: ‘t2’ is a rigid type variable bound by
+               the inferred type of copy :: t2 -> Bool -> t1 at T10045.hs:7:10-34
+             ‘t1’ is a rigid type variable bound by
+               the inferred type of copy :: t2 -> Bool -> t1 at T10045.hs:7:10-34
       To use the inferred type, enable PartialTypeSignatures
-    • In the type signature:
-        copy :: _
+    • In the type signature: copy :: _
       In the expression:
         let
           copy :: _
@@ -20,7 +19,5 @@ T10045.hs:6:18: error:
                 copy w from = copy w True
               in copy ws1 False
     • Relevant bindings include
-        copy :: t1 -> Bool -> t2 (bound at T10045.hs:7:10)
         ws1 :: () (bound at T10045.hs:5:11)
         foo :: Meta -> t (bound at T10045.hs:5:1)
-
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
index d026cbc70d..440d8722de 100644
--- a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
@@ -1,48 +1,48 @@
-

-WildcardInstantiations.hs:5:14: error:

-    • Found type wildcard ‘_a’ standing for ‘a’

-      Where: ‘a’ is a rigid type variable bound by

-               the inferred type of foo :: (Show a, Enum a) => a -> String

-               at WildcardInstantiations.hs:6:1-21

-      To use the inferred type, enable PartialTypeSignatures

-    • In the type signature: foo :: (Show _a, _) => _a -> _

-

-WildcardInstantiations.hs:5:18: error:

-    • Found type wildcard ‘_’ standing for ‘Enum a’

-      Where: ‘a’ is a rigid type variable bound by

-               the inferred type of foo :: (Show a, Enum a) => a -> String

-               at WildcardInstantiations.hs:6:1-21

-      To use the inferred type, enable PartialTypeSignatures

-    • In the type signature: foo :: (Show _a, _) => _a -> _

-

-WildcardInstantiations.hs:5:30: error:

-    • Found type wildcard ‘_’ standing for ‘String’

-      To use the inferred type, enable PartialTypeSignatures

-    • In the type signature: foo :: (Show _a, _) => _a -> _

-

-WildcardInstantiations.hs:8:8: error:

-    • Found type wildcard ‘_’ standing for ‘t’

-      Where: ‘t’ is a rigid type variable bound by

-               the inferred type of bar :: t -> (t -> w) -> w

-               at WildcardInstantiations.hs:9:1-13

-      To use the inferred type, enable PartialTypeSignatures

-    • In the type signature: bar :: _ -> _ -> _

-

-WildcardInstantiations.hs:8:13: error:

-    • Found type wildcard ‘_’ standing for ‘t -> w’

-      Where: ‘w’ is a rigid type variable bound by

-               the inferred type of bar :: t -> (t -> w) -> w

-               at WildcardInstantiations.hs:9:1-13

-             ‘t’ is a rigid type variable bound by

-               the inferred type of bar :: t -> (t -> w) -> w

-               at WildcardInstantiations.hs:9:1-13

-      To use the inferred type, enable PartialTypeSignatures

-    • In the type signature: bar :: _ -> _ -> _

-

-WildcardInstantiations.hs:8:18: error:

-    • Found type wildcard ‘_’ standing for ‘w’

-      Where: ‘w’ is a rigid type variable bound by

-               the inferred type of bar :: t -> (t -> w) -> w

-               at WildcardInstantiations.hs:9:1-13

-      To use the inferred type, enable PartialTypeSignatures

-    • In the type signature: bar :: _ -> _ -> _

+
+WildcardInstantiations.hs:5:14: error:
+    • Found type wildcard ‘_a’ standing for ‘a’
+      Where: ‘a’ is a rigid type variable bound by
+               the inferred type of foo :: (Show a, Enum a) => a -> String
+               at WildcardInstantiations.hs:6:1-21
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type signature: foo :: (Show _a, _) => _a -> _
+
+WildcardInstantiations.hs:5:18: error:
+    • Found type wildcard ‘_’ standing for ‘Enum a’
+      Where: ‘a’ is a rigid type variable bound by
+               the inferred type of foo :: (Show a, Enum a) => a -> String
+               at WildcardInstantiations.hs:6:1-21
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type signature: foo :: (Show _a, _) => _a -> _
+
+WildcardInstantiations.hs:5:30: error:
+    • Found type wildcard ‘_’ standing for ‘String’
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type signature: foo :: (Show _a, _) => _a -> _
+
+WildcardInstantiations.hs:8:8: error:
+    • Found type wildcard ‘_’ standing for ‘t’
+      Where: ‘t’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> w) -> w
+               at WildcardInstantiations.hs:9:1-13
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type signature: bar :: _ -> _ -> _
+
+WildcardInstantiations.hs:8:13: error:
+    • Found type wildcard ‘_’ standing for ‘t -> w’
+      Where: ‘t’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> w) -> w
+               at WildcardInstantiations.hs:9:1-13
+             ‘w’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> w) -> w
+               at WildcardInstantiations.hs:9:1-13
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type signature: bar :: _ -> _ -> _
+
+WildcardInstantiations.hs:8:18: error:
+    • Found type wildcard ‘_’ standing for ‘w’
+      Where: ‘w’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> w) -> w
+               at WildcardInstantiations.hs:9:1-13
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type signature: bar :: _ -> _ -> _
diff --git a/testsuite/tests/patsyn/should_compile/T11213.stderr b/testsuite/tests/patsyn/should_compile/T11213.stderr
index 7a0af54b67..72f67e3a26 100644
--- a/testsuite/tests/patsyn/should_compile/T11213.stderr
+++ b/testsuite/tests/patsyn/should_compile/T11213.stderr
@@ -11,7 +11,7 @@ T11213.hs:21:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11213.hs:22:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      Pue :: forall t. () => forall a. t -> a -> (t, Ex)
+      Pue :: forall a. () => forall a1. a -> a1 -> (a, Ex)
 
 T11213.hs:23:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
@@ -19,9 +19,9 @@ T11213.hs:23:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11213.hs:24:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      Purp :: forall t a.
-              (Num a, Eq a) =>
-              Show t => a -> t -> ([a], UnivProv t)
+      Purp :: forall a a1.
+              (Num a1, Eq a1) =>
+              Show a => a1 -> a -> ([a1], UnivProv a)
 
 T11213.hs:25:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
@@ -39,8 +39,8 @@ T11213.hs:27:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11213.hs:28:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      Pup :: forall t. () => Show t => t -> UnivProv t
+      Pup :: forall a. () => Show a => a -> UnivProv a
 
 T11213.hs:29:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      Puep :: forall t. () => forall a. Show a => a -> t -> (ExProv, t)
+      Puep :: forall b. () => forall a. Show a => a -> b -> (ExProv, b)
diff --git a/testsuite/tests/patsyn/should_fail/T11053.stderr b/testsuite/tests/patsyn/should_fail/T11053.stderr
index e583aa1b08..40dae30ba1 100644
--- a/testsuite/tests/patsyn/should_fail/T11053.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11053.stderr
@@ -4,16 +4,16 @@ T11053.hs:7:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11053.hs:9:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      J :: forall t. t -> Maybe t
+      J :: forall a. a -> Maybe a
 
 T11053.hs:11:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      J1 :: forall t. t -> Maybe t
+      J1 :: forall a. a -> Maybe a
 
 T11053.hs:13:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      J2 :: forall t. t -> Maybe t
+      J2 :: forall a. a -> Maybe a
 
 T11053.hs:15:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      J3 :: forall t. t -> Maybe t
+      J3 :: forall a. a -> Maybe a
diff --git a/testsuite/tests/patsyn/should_run/ghci.stdout b/testsuite/tests/patsyn/should_run/ghci.stdout
index 3dcecbc7a6..d3e6c0edbf 100644
--- a/testsuite/tests/patsyn/should_run/ghci.stdout
+++ b/testsuite/tests/patsyn/should_run/ghci.stdout
@@ -1,3 +1,3 @@
-pattern Single :: t -> [t] 	-- Defined at <interactive>:3:1
+pattern Single :: a -> [a] 	-- Defined at <interactive>:3:1
 foo :: [Bool] -> [Bool]
 [False]
diff --git a/testsuite/tests/polykinds/T7328.stderr b/testsuite/tests/polykinds/T7328.stderr
index 58e883e142..95b3a7782f 100644
--- a/testsuite/tests/polykinds/T7328.stderr
+++ b/testsuite/tests/polykinds/T7328.stderr
@@ -1,7 +1,6 @@
 
 T7328.hs:8:34: error:
-    • Occurs check: cannot construct the infinite kind: k0 ~ k1 -> k0
+    • Occurs check: cannot construct the infinite kind: k1 ~ k0 -> k1
     • In the first argument of ‘Foo’, namely ‘f’
       In the first argument of ‘Proxy’, namely ‘Foo f’
-      In the type signature:
-        foo :: a ~ f i => Proxy (Foo f)
+      In the type signature: foo :: a ~ f i => Proxy (Foo f)
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index 31ac2a356e..9f8f62e25e 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -1,21 +1,19 @@
-

-T7438.hs:6:14: error:

-    • Couldn't match expected type ‘t2’ with actual type ‘t3’

-        ‘t2’ is untouchable

-          inside the constraints: t ~ t1

-          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

-      ‘t2’ is a rigid type variable bound by

-        the inferred type of go :: Thrist t1 t -> t3 -> t2

-        at T7438.hs:6:1-16

-      ‘t3’ is a rigid type variable bound by

-        the inferred type of go :: Thrist t1 t -> t3 -> t2

-        at T7438.hs:6:1-16

-      Possible fix: add a type signature for ‘go’

-    • In the expression: acc

-      In an equation for ‘go’: go Nil acc = acc

-    • Relevant bindings include

-        acc :: t3 (bound at T7438.hs:6:8)

-        go :: Thrist t1 t -> t3 -> t2 (bound at T7438.hs:6:1)

+
+T7438.hs:6:14: error:
+    • Couldn't match expected type ‘t’ with actual type ‘t1’
+        ‘t’ is untouchable
+          inside the constraints: 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
+      ‘t’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16
+      ‘t1’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16
+      Possible fix: add a type signature for ‘go’
+    • In the expression: acc
+      In an equation for ‘go’: go Nil acc = acc
+    • Relevant bindings include
+        acc :: t1 (bound at T7438.hs:6:8)
+        go :: Thrist a b -> t1 -> t (bound at T7438.hs:6:1)
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index 409e66ae6c..79a9a4617f 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -1,14 +1,13 @@
 
 T9017.hs:8:7: error:
-    • Couldn't match kind ‘k1’ with ‘*’
-      ‘k1’ is a rigid type variable bound by
+    • Couldn't match kind ‘k’ with ‘*’
+      ‘k’ is a rigid type variable bound by
         the type signature for:
           foo :: forall k k1 (a :: k -> k1 -> *) (b :: k) (m :: k -> k1).
                  a b (m b)
-        at T9017.hs:7:8
+        at T9017.hs:7:1-16
       When matching the kind of ‘a’
     • In the expression: arr return
       In an equation for ‘foo’: foo = arr return
     • Relevant bindings include
         foo :: a b (m b) (bound at T9017.hs:8:1)
-
diff --git a/testsuite/tests/rebindable/rebindable6.stderr b/testsuite/tests/rebindable/rebindable6.stderr
index 8667f318bf..241cf76962 100644
--- a/testsuite/tests/rebindable/rebindable6.stderr
+++ b/testsuite/tests/rebindable/rebindable6.stderr
@@ -25,7 +25,7 @@ rebindable6.hs:110:17: error:
                    return b }
 
 rebindable6.hs:111:17: error:
-    • Ambiguous type variables ‘t0’, ‘t1’ arising from a do statement
+    • Ambiguous type variables ‘t1’, ‘t0’ arising from a do statement
       prevents the constraint ‘(HasBind
                                   (IO (Maybe b) -> (Maybe b -> t1) -> t0))’ from being solved.
         (maybe you haven't applied a function to enough arguments?)
@@ -33,7 +33,7 @@ rebindable6.hs:111:17: error:
         g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
         test_do :: IO a -> IO (Maybe b) -> IO b
           (bound at rebindable6.hs:108:9)
-      Probable fix: use a type annotation to specify what ‘t0’, ‘t1’ should be.
+      Probable fix: use a type annotation to specify what ‘t1’, ‘t0’ should be.
       These potential instance exist:
         instance HasBind (IO a -> (a -> IO b) -> IO b)
           -- Defined at rebindable6.hs:51:18
diff --git a/testsuite/tests/rename/should_fail/T10618.stderr b/testsuite/tests/rename/should_fail/T10618.stderr
index 21c35471dd..8b4dc2c28d 100644
--- a/testsuite/tests/rename/should_fail/T10618.stderr
+++ b/testsuite/tests/rename/should_fail/T10618.stderr
@@ -1,6 +1,6 @@
 
 T10618.hs:3:22: error:
-    • Variable not in scope: (<>) :: Maybe (Maybe a1) -> Maybe a0 -> t
+    • Variable not in scope: (<>) :: Maybe (Maybe a0) -> Maybe a1 -> t
     • Perhaps you meant one of these:
         ‘<$>’ (imported from Prelude), ‘*>’ (imported from Prelude),
         ‘<$’ (imported from Prelude)
diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr
index ab778a0133..cf206a11ae 100644
--- a/testsuite/tests/typecheck/should_compile/tc141.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc141.stderr
@@ -1,54 +1,54 @@
-

-tc141.hs:11:12: error:

-    • You cannot bind scoped type variable ‘a’

-        in a pattern binding signature

-    • In the pattern: p :: a

-      In the pattern: (p :: a, q :: a)

-      In a pattern binding: (p :: a, q :: a) = x

-

-tc141.hs:11:31: error:

-    • Couldn't match expected type ‘a1’ with actual type ‘a’

-        because type variable ‘a1’ would escape its scope

-      This (rigid, skolem) type variable is bound by

-        an expression type signature:

-          a1

-        at tc141.hs:11:34

-    • In the expression: q :: a

-      In the expression: (q :: a, p)

-      In the expression: let (p :: a, q :: a) = x in (q :: a, p)

-    • Relevant bindings include

-        p :: a (bound at tc141.hs:11:12)

-        q :: a (bound at tc141.hs:11:17)

-        x :: (a, a) (bound at tc141.hs:11:3)

-        f :: (a, a) -> (t, a) (bound at tc141.hs:11:1)

-

-tc141.hs:13:13: error:

-    • You cannot bind scoped type variable ‘a’

-        in a pattern binding signature

-    • In the pattern: y :: a

-      In a pattern binding: y :: a = a

-      In the expression:

-        let y :: a = a in

-        let

-          v :: a

-          v = b

-        in v

-

-tc141.hs:15:18: error:

-    • Couldn't match expected type ‘a1’ with actual type ‘t’

-        because type variable ‘a1’ would escape its scope

-      This (rigid, skolem) type variable is bound by

-        the type signature for:

-          v :: a1

-        at tc141.hs:14:14-19

-    • In the expression: b

-      In an equation for ‘v’: v = b

-      In the expression:

-        let

-          v :: a

-          v = b

-        in v

-    • Relevant bindings include

-        v :: a1 (bound at tc141.hs:15:14)

-        b :: t (bound at tc141.hs:13:5)

-        g :: t1 -> t -> forall a. a (bound at tc141.hs:13:1)

+
+tc141.hs:11:12: error:
+    • You cannot bind scoped type variable ‘a’
+        in a pattern binding signature
+    • In the pattern: p :: a
+      In the pattern: (p :: a, q :: a)
+      In a pattern binding: (p :: a, q :: a) = x
+
+tc141.hs:11:31: error:
+    • Couldn't match expected type ‘a2’ with actual type ‘a1’
+        because type variable ‘a2’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        an expression type signature:
+          a2
+        at tc141.hs:11:34
+    • In the expression: q :: a
+      In the expression: (q :: a, p)
+      In the expression: let (p :: a, q :: a) = x in (q :: a, p)
+    • Relevant bindings include
+        p :: a1 (bound at tc141.hs:11:12)
+        q :: a1 (bound at tc141.hs:11:17)
+        x :: (a1, a1) (bound at tc141.hs:11:3)
+        f :: (a1, a1) -> (a, a1) (bound at tc141.hs:11:1)
+
+tc141.hs:13:13: error:
+    • You cannot bind scoped type variable ‘a’
+        in a pattern binding signature
+    • In the pattern: y :: a
+      In a pattern binding: y :: a = a
+      In the expression:
+        let y :: a = a in
+        let
+          v :: a
+          v = b
+        in v
+
+tc141.hs:15:18: error:
+    • Couldn't match expected type ‘a1’ with actual type ‘t’
+        because type variable ‘a1’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        the type signature for:
+          v :: a1
+        at tc141.hs:14:14-19
+    • In the expression: b
+      In an equation for ‘v’: v = b
+      In the expression:
+        let
+          v :: a
+          v = b
+        in v
+    • Relevant bindings include
+        v :: a1 (bound at tc141.hs:15:14)
+        b :: t (bound at tc141.hs:13:5)
+        g :: t1 -> t -> forall a. a (bound at tc141.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/FailDueToGivenOverlapping.stderr b/testsuite/tests/typecheck/should_fail/FailDueToGivenOverlapping.stderr
index f30ceecff9..651aad6c57 100644
--- a/testsuite/tests/typecheck/should_fail/FailDueToGivenOverlapping.stderr
+++ b/testsuite/tests/typecheck/should_fail/FailDueToGivenOverlapping.stderr
@@ -1,6 +1,6 @@
 
 FailDueToGivenOverlapping.hs:27:9: error:
-    • Overlapping instances for E [t0] arising from a use of ‘eop’
+    • Overlapping instances for E [a0] arising from a use of ‘eop’
       Matching givens (or their superclasses):
         E [Int]
           bound by the type signature for:
@@ -8,6 +8,6 @@ FailDueToGivenOverlapping.hs:27:9: error:
           at FailDueToGivenOverlapping.hs:26:1-26
       Matching instances:
         instance E [a] -- Defined at FailDueToGivenOverlapping.hs:21:10
-      (The choice depends on the instantiation of ‘t0’)
+      (The choice depends on the instantiation of ‘a0’)
     • In the expression: eop [undefined]
       In an equation for ‘bar’: bar _ = eop [undefined]
diff --git a/testsuite/tests/typecheck/should_fail/T10351.stderr b/testsuite/tests/typecheck/should_fail/T10351.stderr
index b6a16d3723..782d6e39d8 100644
--- a/testsuite/tests/typecheck/should_fail/T10351.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10351.stderr
@@ -1,6 +1,6 @@
 
 T10351.hs:6:1: error:
-    • Non type-variable argument in the constraint: C [t]
+    • Non type-variable argument in the constraint: C [a]
       (Use FlexibleContexts to permit this)
     • When checking the inferred type
-        f :: forall t. C [t] => t -> ()
+        f :: forall a. C [a] => a -> ()
diff --git a/testsuite/tests/typecheck/should_fail/T11355.stderr b/testsuite/tests/typecheck/should_fail/T11355.stderr
index 6c649e4187..68375400a8 100644
--- a/testsuite/tests/typecheck/should_fail/T11355.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11355.stderr
@@ -1,6 +1,6 @@
 
 T11355.hs:5:7: error:
-    • Illegal polymorphic type: forall (a :: TYPE t1). a
+    • Illegal polymorphic type: forall (a :: TYPE t0). a
       GHC doesn't yet support impredicative polymorphism
     • In the expression:
         const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))
diff --git a/testsuite/tests/typecheck/should_fail/T5858.stderr b/testsuite/tests/typecheck/should_fail/T5858.stderr
index 08de48888a..dc3ee90189 100644
--- a/testsuite/tests/typecheck/should_fail/T5858.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5858.stderr
@@ -1,9 +1,9 @@
 
 T5858.hs:11:7: error:
-    • Ambiguous type variables ‘t0’, ‘t1’ arising from a use of ‘infer’
+    • Ambiguous type variables ‘a0’, ‘a1’ arising from a use of ‘infer’
       prevents the constraint ‘(InferOverloaded
-                                  ([t0], [t1]))’ from being solved.
-      Probable fix: use a type annotation to specify what ‘t0’, ‘t1’ should be.
+                                  ([a0], [a1]))’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’, ‘a1’ should be.
       These potential instance exist:
         instance t1 ~ String => InferOverloaded (t1, t1)
           -- Defined at T5858.hs:8:10
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 3bd6b40a82..758acfff05 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -69,7 +69,7 @@ T6018fail.hs:59:10: error:
 
 T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k’ cannot be inferred from the right-hand side.
+    Kind variable ‘k1’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at T6018fail.hs:62:15
diff --git a/testsuite/tests/typecheck/should_fail/T8142.stderr b/testsuite/tests/typecheck/should_fail/T8142.stderr
index 53e6798a5e..4200268c24 100644
--- a/testsuite/tests/typecheck/should_fail/T8142.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8142.stderr
@@ -1,14 +1,14 @@
 
 T8142.hs:6:18: error:
     • Couldn't match type ‘Nu g0’ with ‘Nu g’
-      Expected type: Nu ((,) t) -> Nu g
-        Actual type: Nu ((,) t0) -> Nu g0
+      Expected type: Nu ((,) a) -> Nu g
+        Actual type: Nu ((,) a0) -> Nu g0
       NB: ‘Nu’ is a type function, and may not be injective
       The type variable ‘g0’ is ambiguous
     • In the ambiguity check for the inferred type for ‘h’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
-        h :: forall (g :: * -> *) t. Nu ((,) t) -> Nu g
+        h :: forall (g :: * -> *) a. Nu ((,) a) -> Nu g
       In an equation for ‘tracer’:
           tracer
             = h
@@ -16,11 +16,11 @@ T8142.hs:6:18: error:
                 h = (\ (_, b) -> ((outI . fmap h) b)) . out
 
 T8142.hs:6:57: error:
-    • Couldn't match type ‘Nu ((,) t)’ with ‘g (Nu ((,) t))’
-      Expected type: Nu ((,) t) -> (t, g (Nu ((,) t)))
-        Actual type: Nu ((,) t) -> (t, Nu ((,) t))
+    • Couldn't match type ‘Nu ((,) a)’ with ‘g (Nu ((,) a))’
+      Expected type: Nu ((,) a) -> (a, g (Nu ((,) a)))
+        Actual type: Nu ((,) a) -> (a, Nu ((,) a))
     • In the second argument of ‘(.)’, namely ‘out’
       In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
       In an equation for ‘h’: h = (\ (_, b) -> ((outI . fmap h) b)) . out
     • Relevant bindings include
-        h :: Nu ((,) t) -> Nu g (bound at T8142.hs:6:18)
+        h :: Nu ((,) a) -> Nu g (bound at T8142.hs:6:18)
diff --git a/testsuite/tests/typecheck/should_fail/T9109.stderr b/testsuite/tests/typecheck/should_fail/T9109.stderr
index 996da6e534..ce1b09d51c 100644
--- a/testsuite/tests/typecheck/should_fail/T9109.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9109.stderr
@@ -1,15 +1,14 @@
-

-T9109.hs:8:13: error:

-    • Couldn't match expected type ‘t’ with actual type ‘Bool’

-        ‘t’ is untouchable

-          inside the constraints: t1 ~ Bool

-          bound by a pattern with constructor: GBool :: G Bool,

-                   in an equation for ‘foo’

-          at T9109.hs:8:5-9

-      ‘t’ is a rigid type variable bound by

-        the inferred type of foo :: G t1 -> t 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

-    • Relevant bindings include

-        foo :: G t1 -> t (bound at T9109.hs:8:1)

+
+T9109.hs:8:13: error:
+    • Couldn't match expected type ‘t’ with actual type ‘Bool’
+        ‘t’ 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
+      ‘t’ is a rigid type variable bound by
+        the inferred type of foo :: G a -> t 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
+    • Relevant bindings include foo :: G a -> t (bound at T9109.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
index 03671b0b04..ff90a738c9 100644
--- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -1,6 +1,6 @@
 
 VtaFail.hs:7:16: error:
-    • Cannot apply expression of type ‘t0 -> t1 -> (t0, t1)’
+    • Cannot apply expression of type ‘a0 -> b0 -> (a0, b0)’
       to a visible type argument ‘Int’
     • In the expression: pairup_nosig @Int @Bool 5 True
       In an equation for ‘answer_nosig’:
diff --git a/testsuite/tests/typecheck/should_fail/tcfail001.stderr b/testsuite/tests/typecheck/should_fail/tcfail001.stderr
index 61604469e5..56c28d98b5 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail001.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail001.stderr
@@ -1,7 +1,7 @@
 
 tcfail001.hs:9:2: error:
     • Couldn't match expected type ‘[a]’
-                  with actual type ‘[t1] -> [t0]’
+                  with actual type ‘[a0] -> [a1]’
     • The equation(s) for ‘op’ have one argument,
       but its type ‘[a]’ has none
       In the instance declaration for ‘A [a]’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail010.stderr b/testsuite/tests/typecheck/should_fail/tcfail010.stderr
index c22a05e777..11e529084f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail010.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail010.stderr
@@ -1,6 +1,6 @@
 
 tcfail010.hs:3:16: error:
-    • No instance for (Num [t0]) arising from a use of ‘+’
+    • No instance for (Num [a0]) arising from a use of ‘+’
     • In the expression: z + 2
       In the expression: \ (y : z) -> z + 2
       In an equation for ‘q’: q = \ (y : z) -> z + 2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail012.stderr b/testsuite/tests/typecheck/should_fail/tcfail012.stderr
index 572c7a677c..ea5a2a72cd 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail012.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail012.stderr
@@ -1,5 +1,5 @@
 
-tcfail012.hs:3:8:
-    Couldn't match expected type ‘Bool’ with actual type ‘[t0]’
-    In the expression: []
-    In a pattern binding: True = []
+tcfail012.hs:3:8: error:
+    • Couldn't match expected type ‘Bool’ with actual type ‘[a0]’
+    • In the expression: []
+      In a pattern binding: True = []
diff --git a/testsuite/tests/typecheck/should_fail/tcfail013.stderr b/testsuite/tests/typecheck/should_fail/tcfail013.stderr
index ff7702213c..f3e815bb6e 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 ‘[t1]’ with actual type ‘Bool’
+    • Couldn't match expected type ‘[a]’ with actual type ‘Bool’
     • In the pattern: True
       In an equation for ‘f’: f True = 2
     • Relevant bindings include
-        f :: [t1] -> t (bound at tcfail013.hs:3:1)
+        f :: [a] -> t (bound at tcfail013.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail016.stderr b/testsuite/tests/typecheck/should_fail/tcfail016.stderr
index 949cb65855..3430c2d830 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail016.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail016.stderr
@@ -1,7 +1,7 @@
 
 tcfail016.hs:8:1: error:
-    • Couldn't match type ‘(t, Expr t)’ with ‘Expr t’
-      Expected type: AnnExpr t -> [[Char]]
-        Actual type: Expr t -> [[Char]]
+    • Couldn't match type ‘(a, Expr a)’ with ‘Expr a’
+      Expected type: AnnExpr a -> [[Char]]
+        Actual type: Expr a -> [[Char]]
     • Relevant bindings include
-        g :: AnnExpr t -> [[Char]] (bound at tcfail016.hs:8:1)
+        g :: AnnExpr a -> [[Char]] (bound at tcfail016.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail033.stderr b/testsuite/tests/typecheck/should_fail/tcfail033.stderr
index e349ab1116..bc346c2aac 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail033.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail033.stderr
@@ -1,10 +1,10 @@
 
 tcfail033.hs:4:12: error:
-    • Occurs check: cannot construct the infinite type: t1 ~ (t1, t)
+    • Occurs check: cannot construct the infinite type: a ~ (a, b)
     • In the expression: x
       In the expression: [x | (x, y) <- buglet]
       In an equation for ‘buglet’: buglet = [x | (x, y) <- buglet]
     • Relevant bindings include
-        y :: t (bound at tcfail033.hs:4:19)
-        x :: t1 (bound at tcfail033.hs:4:17)
-        buglet :: [(t1, t)] (bound at tcfail033.hs:4:1)
+        y :: b (bound at tcfail033.hs:4:19)
+        x :: a (bound at tcfail033.hs:4:17)
+        buglet :: [(a, b)] (bound at tcfail033.hs:4:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail069.stderr b/testsuite/tests/typecheck/should_fail/tcfail069.stderr
index 195119d26d..fcaf3e9542 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail069.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail069.stderr
@@ -1,7 +1,7 @@
 
-tcfail069.hs:21:7:
-    Couldn't match expected type ‘([Int], [Int])’
-                with actual type ‘[t0]’
-    In the pattern: []
-    In a case alternative: [] -> error "foo"
-    In the expression: case (list1, list2) of { [] -> error "foo" }
+tcfail069.hs:21:7: error:
+    • Couldn't match expected type ‘([Int], [Int])’
+                  with actual type ‘[a0]’
+    • In the pattern: []
+      In a case alternative: [] -> error "foo"
+      In the expression: case (list1, list2) of { [] -> error "foo" }
diff --git a/testsuite/tests/typecheck/should_fail/tcfail182.stderr b/testsuite/tests/typecheck/should_fail/tcfail182.stderr
index 4103c3a0fa..6bd7b156ab 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail182.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail182.stderr
@@ -1,10 +1,10 @@
 
 tcfail182.hs:9:3: error:
-    Couldn't match expected type ‘Prelude.Maybe a’
-                with actual type ‘Maybe t0’
-    NB: ‘Maybe’ is defined at tcfail182.hs:6:1-18
-        ‘Prelude.Maybe’ is defined in ‘GHC.Base’ in package ‘base-4.9.0.0’
-    In the pattern: Foo
-    In an equation for ‘f’: f Foo = 3
-    Relevant bindings include
-      f :: Prelude.Maybe a -> Int (bound at tcfail182.hs:9:1)
+    • Couldn't match expected type ‘Prelude.Maybe a’
+                  with actual type ‘Maybe a0’
+      NB: ‘Maybe’ is defined at tcfail182.hs:6:1-18
+          ‘Prelude.Maybe’ is defined in ‘GHC.Base’ in package ‘base-4.9.0.0’
+    • In the pattern: Foo
+      In an equation for ‘f’: f Foo = 3
+    • Relevant bindings include
+        f :: Prelude.Maybe a -> Int (bound at tcfail182.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index 9df11cafff..77349e29f4 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,19 +1,19 @@
-

-tcfail201.hs:17:56: error:

-    • Couldn't match type ‘a’ with ‘HsDoc t0’

-      ‘a’ is a rigid type variable bound by

-        the type signature for:

-          gfoldl' :: forall (c :: * -> *) a.

-                     (forall a1 b. c (a1 -> b) -> a1 -> c b)

-                     -> (forall g. g -> c g) -> a -> c a

-        at tcfail201.hs:15:1-85

-      Expected type: c a

-        Actual type: c (HsDoc t0)

-    • In the expression: z DocEmpty

-      In a case alternative: DocEmpty -> z DocEmpty

-      In the expression: case hsDoc of { DocEmpty -> z DocEmpty }

-    • Relevant bindings include

-        hsDoc :: a (bound at tcfail201.hs:16:13)

-        gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)

-                   -> (forall g. g -> c g) -> a -> c a

-          (bound at tcfail201.hs:16:1)

+
+tcfail201.hs:17:56: error:
+    • Couldn't match type ‘a’ with ‘HsDoc id0’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          gfoldl' :: forall (c :: * -> *) a.
+                     (forall a1 b. c (a1 -> b) -> a1 -> c b)
+                     -> (forall g. g -> c g) -> a -> c a
+        at tcfail201.hs:15:1-85
+      Expected type: c a
+        Actual type: c (HsDoc id0)
+    • In the expression: z DocEmpty
+      In a case alternative: DocEmpty -> z DocEmpty
+      In the expression: case hsDoc of { DocEmpty -> z DocEmpty }
+    • Relevant bindings include
+        hsDoc :: a (bound at tcfail201.hs:16:13)
+        gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
+                   -> (forall g. g -> c g) -> a -> c a
+          (bound at tcfail201.hs:16:1)