From 7a08a025eecb0cca494757fc83099a9decb052ad Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simon.peytonjones@gmail.com>
Date: Tue, 11 Jun 2024 12:34:24 +0100
Subject: [PATCH] Various fixes to type-tidying

This MR was triggered by #24868, but I found a number of bugs
and infelicities in type-tidying as I went along.  Highlights:

* Fix to #24868 is in GHC.Tc.Errors.report_unsolved: avoid
  using the OccNames of /bound/ variables when tidying /free/
  variables; see the call to `tidyAvoiding`.  That avoid the
  gratuitous renaming which was the cause of #24868. See
     Note [tidyAvoiding] in GHC.Core.TyCo.Tidy

* Refactor and document the tidying of open types.
  See GHC.Core.TyCo.Tidy
     Note [Tidying open types]
     Note [Tidying is idempotent]

* Tidy the coercion variable in HoleCo. That's important so
  that tidied types have tidied kinds.

* Some small renaming to make things consistent.  In particular
  the "X" forms return a new TidyEnv.  E.g.
     tidyOpenType  :: TidyEnv -> Type -> Type
     tidyOpenTypeX :: TidyEnv -> Type -> (TidyEnv, Type)
---
 compiler/GHC/Core/TyCo/FVs.hs                 |   3 +
 compiler/GHC/Core/TyCo/Ppr.hs                 |  18 +-
 compiler/GHC/Core/TyCo/Tidy.hs                | 229 +++++++++++++-----
 compiler/GHC/Core/Type.hs                     |   6 +-
 compiler/GHC/Iface/Tidy/StaticPtrTable.hs     |   2 +
 compiler/GHC/Rename/Names.hs                  |   2 +-
 compiler/GHC/Runtime/Debugger.hs              |   2 +-
 compiler/GHC/Runtime/Eval.hs                  |   4 +-
 compiler/GHC/Tc/Errors.hs                     |   8 +-
 compiler/GHC/Tc/Errors/Ppr.hs                 |   2 +-
 compiler/GHC/Tc/Gen/Bind.hs                   |   4 +-
 compiler/GHC/Tc/Gen/Expr.hs                   |   4 +-
 compiler/GHC/Tc/Solver/Monad.hs               |   3 +-
 compiler/GHC/Tc/Types/Constraint.hs           |  15 ++
 compiler/GHC/Tc/Utils/TcMType.hs              |   9 +-
 compiler/GHC/Tc/Validity.hs                   |   6 +-
 compiler/GHC/Tc/Zonk/TcType.hs                |  11 +-
 compiler/GHC/Types/Name/Occurrence.hs         |  28 ++-
 compiler/GHC/Types/Var/Env.hs                 |   2 +-
 .../dependent/should_compile/T15743e.stderr   |   2 +-
 .../dependent/should_fail/T16326_Fail4.stderr |   2 +-
 .../dependent/should_fail/T16326_Fail5.stderr |   2 +-
 .../indexed-types/should_fail/T13877.stderr   |   6 +-
 .../indexed-types/should_fail/T14369.stderr   |   2 +-
 .../tests/patsyn/should_fail/T15695.stderr    |  12 +-
 testsuite/tests/polykinds/T11520.stderr       |   6 +-
 testsuite/tests/polykinds/T14846.stderr       |   2 +-
 testsuite/tests/polykinds/T15787.stderr       |   6 +-
 testsuite/tests/polykinds/T7278.stderr        |   6 +-
 testsuite/tests/rep-poly/RepPolyNPlusK.stderr |  10 +-
 testsuite/tests/rep-poly/T13233.stderr        |   2 +-
 testsuite/tests/rep-poly/T21906.stderr        |   4 +-
 testsuite/tests/th/T21050.stderr              |   6 +-
 .../typecheck/no_skolem_info/T13499.stderr    |  14 +-
 .../typecheck/no_skolem_info/T20063.stderr    |  18 +-
 .../typecheck/should_compile/T9834.stderr     |   2 +-
 .../typecheck/should_compile/tc214.stderr     |   2 +-
 .../should_fail/GivenForallLoop.stderr        |  10 +-
 .../tests/typecheck/should_fail/T10709.stderr |  12 +-
 .../typecheck/should_fail/T10709b.stderr      |  18 +-
 .../tests/typecheck/should_fail/T13909.stderr |   2 +-
 .../typecheck/should_fail/T16059c.stderr      |   4 +-
 .../tests/typecheck/should_fail/T17077.stderr |   4 +-
 .../tests/typecheck/should_fail/T19415.stderr |   6 +-
 .../tests/typecheck/should_fail/T24868.hs     |  19 ++
 .../tests/typecheck/should_fail/T24868.stderr |  37 +++
 .../tests/typecheck/should_fail/T9196.stderr  |   4 +-
 .../should_fail/TcStaticPointersFail03.stderr |   4 +-
 testsuite/tests/typecheck/should_fail/all.T   |   1 +
 .../typecheck/should_fail/tcfail201.stderr    |   2 +-
 50 files changed, 400 insertions(+), 185 deletions(-)
 create mode 100644 testsuite/tests/typecheck/should_fail/T24868.hs
 create mode 100644 testsuite/tests/typecheck/should_fail/T24868.stderr

diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 07d0af01836c..96cf863ede6c 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -303,16 +303,19 @@ runTyCoVars f = appEndo f emptyVarSet
 ********************************************************************* -}
 
 tyCoVarsOfType :: Type -> TyCoVarSet
+-- The "deep" TyCoVars of the the type
 tyCoVarsOfType ty = runTyCoVars (deep_ty ty)
 -- Alternative:
 --   tyCoVarsOfType ty = closeOverKinds (shallowTyCoVarsOfType ty)
 
 tyCoVarsOfTypes :: [Type] -> TyCoVarSet
+-- The "deep" TyCoVars of the the type
 tyCoVarsOfTypes tys = runTyCoVars (deep_tys tys)
 -- Alternative:
 --   tyCoVarsOfTypes tys = closeOverKinds (shallowTyCoVarsOfTypes tys)
 
 tyCoVarsOfCo :: Coercion -> TyCoVarSet
+-- The "deep" TyCoVars of the the coercion
 -- See Note [Free variables of types]
 tyCoVarsOfCo co = runTyCoVars (deep_co co)
 
diff --git a/compiler/GHC/Core/TyCo/Ppr.hs b/compiler/GHC/Core/TyCo/Ppr.hs
index c0bd184beca7..137f74061633 100644
--- a/compiler/GHC/Core/TyCo/Ppr.hs
+++ b/compiler/GHC/Core/TyCo/Ppr.hs
@@ -93,6 +93,13 @@ pprPrecTypeX env prec ty
     -- NB: debug-style is used for -dppr-debug
     --     dump-style  is used for -ddump-tc-trace etc
 
+tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType
+tidyToIfaceTypeStyX env ty sty
+  | userStyle sty = tidyToIfaceTypeX env ty
+  | otherwise     = toIfaceTypeX (tyCoVarsOfType ty) ty
+     -- in latter case, don't tidy, as we'll be printing uniques.
+
+
 pprTyLit :: TyLit -> SDoc
 pprTyLit = pprIfaceTyLit . toIfaceTyLit
 
@@ -100,12 +107,6 @@ pprKind, pprParendKind :: Kind -> SDoc
 pprKind       = pprType
 pprParendKind = pprParendType
 
-tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType
-tidyToIfaceTypeStyX env ty sty
-  | userStyle sty = tidyToIfaceTypeX env ty
-  | otherwise     = toIfaceTypeX (tyCoVarsOfType ty) ty
-     -- in latter case, don't tidy, as we'll be printing uniques.
-
 tidyToIfaceType :: Type -> IfaceType
 tidyToIfaceType = tidyToIfaceTypeX emptyTidyEnv
 
@@ -117,9 +118,12 @@ tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType
 -- leave them as IfaceFreeTyVar.  This is super-important
 -- for debug printing.
 tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty)
+  -- NB: if the type has /already/ been tidied (for example by the typechecker)
+  --     the tidy step here is a no-op.  See Note [Tidying is idempotent]
+  --     in GHC.Core.TyCo.Tidy
   where
     env'      = tidyFreeTyCoVars env free_tcvs
-    free_tcvs = tyCoVarsOfTypeWellScoped ty
+    free_tcvs = tyCoVarsOfTypeList ty
 
 ------------
 pprCo, pprParendCo :: Coercion -> SDoc
diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs
index d6aa28e5c703..c572f4a1e9dc 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -4,23 +4,25 @@
 module GHC.Core.TyCo.Tidy
   (
         -- * Tidying type related things up for printing
-        tidyType,      tidyTypes,
-        tidyOpenType,  tidyOpenTypes,
-        tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes,
-        tidyOpenTyCoVar, tidyOpenTyCoVars,
-        tidyTyCoVarOcc,
+        tidyType, tidyTypes,
+        tidyCo,   tidyCos,
         tidyTopType,
-        tidyCo, tidyCos,
-        tidyForAllTyBinder, tidyForAllTyBinders
+
+        tidyOpenType,  tidyOpenTypes,
+        tidyOpenTypeX, tidyOpenTypesX,
+        tidyFreeTyCoVars, tidyFreeTyCoVarX, tidyFreeTyCoVarsX,
+
+        tidyAvoiding,
+        tidyVarBndr, tidyVarBndrs, avoidNameClashes,
+        tidyForAllTyBinder, tidyForAllTyBinders,
+        tidyTyCoVarOcc
   ) where
 
 import GHC.Prelude
 import GHC.Data.FastString
 
 import GHC.Core.TyCo.Rep
-import GHC.Core.TyCo.FVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
-
-import GHC.Data.Maybe (orElse)
+import GHC.Core.TyCo.FVs
 import GHC.Types.Name hiding (varName)
 import GHC.Types.Var
 import GHC.Types.Var.Env
@@ -29,12 +31,76 @@ import GHC.Utils.Misc (strictMap)
 
 import Data.List (mapAccumL)
 
-{-
-%************************************************************************
-%*                                                                      *
-\subsection{TidyType}
-%*                                                                      *
-%************************************************************************
+{- **********************************************************************
+
+                  TidyType
+
+********************************************************************** -}
+
+{- Note [Tidying open types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When tidying some open types [t1,..,tn], we find their free vars, and tidy them first.
+
+But (tricky point) we restrict the occ_env part of inner_env to just the /free/
+vars of [t1..tn], so that we don't gratuitously rename the /bound/ variables.
+
+Example: assume the TidyEnv
+      ({"a1","b"} , [a_4 :-> a1, b_7 :-> b])
+and call tidyOpenTypes on
+      [a_1, forall a_2. Maybe (a_2,a_4), forall b. (b,a_1)]
+All the a's have the same OccName, but different uniques.
+
+The TidyOccEnv binding for "b" relates b_7, which doesn't appear free in the
+these types at all, so we don't want that to mess up the tidying for the
+(forall b...).
+
+So we proceed as follows:
+  1. Find the free vars.
+     In our example:the free vars are a_1 and a_4:
+
+  2. Use tidyFreeTyCoVars to tidy them (workhorse: `tidyFreeCoVarX`)
+     In our example:
+      * a_4 already has a tidy form, a1, so don't change that
+      * a_1 gets tidied to a2
+
+  3. Trim the TidyOccEnv to OccNames of the tidied free vars (`trimTidyEnv`)
+     In our example "a1" and "a2"
+
+  4. Now tidy the types.  In our example we get
+      [a2, forall a3. Maybe (a3,a1), forall b. (b, a2)]
+
+Note [Tidying is idempotent]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Key invariant: tidyFreeTyCoVars is idempotent, at least if you start with
+an empty TidyEnv. This is important because:
+
+  * The typechecker error message processing carefully tidies types, using
+    global knowledge; see for example calls to `tidyCt` in GHC.Tc.Errors.
+
+  * Then the type pretty-printer, GHC.Core.TyCo.Ppr.pprType tidies the type
+    again, because that's important for pretty-printing types in general.
+
+But the second tidying is a no-op if the first step has happened, because
+all the free vars will have distinct OccNames, so no renaming needs to happen.
+
+Note [tidyAvoiding]
+~~~~~~~~~~~~~~~~~~~
+Consider tidying this unsolved constraint in GHC.Tc.Errors.report_unsolved.
+    C a_33, (forall a. Eq a => D a)
+Here a_33 is a free unification variable.  If we firs tidy [a_33 :-> "a"]
+then we have no choice but to tidy the `forall a` to something else. But it
+is confusing (sometimes very confusing) to gratuitously rename skolems in
+this way -- see #24868.  So it is better to :
+
+  * Find the /bound/ skolems (just `a` in this case)
+  * Initialise the TidyOccEnv to avoid using "a"
+  * Now tidy the free a_33 to, say, "a1"
+  * Delete "a" from the TidyOccEnv
+
+This is done by `tidyAvoiding`.
+
+The last step is very important; if we leave "a" in the TidyOccEnv, when
+we get to the (forall a. blah) we'll rename `a` to "a2", avoiding "a".
 -}
 
 -- | This tidies up a type for printing in an error message, or in
@@ -95,31 +161,38 @@ tidyForAllTyBinders tidy_env tvbs
 tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
 -- ^ Add the free 'TyVar's to the env in tidy form,
 -- so that we can tidy the type they are free in
-tidyFreeTyCoVars tidy_env tyvars
-  = fst (tidyOpenTyCoVars tidy_env tyvars)
+-- Precondition: input free vars are closed over kinds and
+-- This function does a scopedSort, so that tidied variables
+-- have tidied kinds.
+-- See Note [Tidying is idempotent]
+tidyFreeTyCoVars tidy_env tyvars = fst (tidyFreeTyCoVarsX tidy_env tyvars)
 
 ---------------
-tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
-tidyOpenTyCoVars env tyvars = mapAccumL tidyOpenTyCoVar env tyvars
+tidyFreeTyCoVarsX :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
+-- Precondition: input free vars are closed over kinds and
+-- This function does a scopedSort, so that tidied variables
+-- have tidied kinds.
+-- See Note [Tidying is idempotent]
+tidyFreeTyCoVarsX env tyvars = mapAccumL tidyFreeTyCoVarX env $
+                               scopedSort tyvars
 
 ---------------
-tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
+tidyFreeTyCoVarX :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
 -- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name
 -- using the environment if one has not already been allocated. See
 -- also 'tidyVarBndr'
-tidyOpenTyCoVar env@(_, subst) tyvar
+-- See Note [Tidying is idempotent]
+tidyFreeTyCoVarX env@(_, subst) tyvar
   = case lookupVarEnv subst tyvar of
-        Just tyvar' -> (env, tyvar')              -- Already substituted
-        Nothing     ->
-          let env' = tidyFreeTyCoVars env (tyCoVarsOfTypeList (tyVarKind tyvar))
-          in tidyVarBndr env' tyvar  -- Treat it as a binder
+        Just tyvar' -> (env, tyvar')           -- Already substituted
+        Nothing     -> tidyVarBndr env tyvar  -- Treat it as a binder
 
 ---------------
 tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
-tidyTyCoVarOcc env@(_, subst) tv
-  = case lookupVarEnv subst tv of
-        Nothing  -> updateVarType (tidyType env) tv
-        Just tv' -> tv'
+tidyTyCoVarOcc env@(_, subst) tcv
+  = case lookupVarEnv subst tcv of
+        Nothing   -> updateVarType (tidyType env) tcv
+        Just tcv' -> tcv'
 
 ---------------
 
@@ -157,22 +230,26 @@ tidyTypes env tys = strictMap (tidyType env) tys
 --
 -- See Note [Strictness in tidyType and friends]
 tidyType :: TidyEnv -> Type -> Type
-tidyType _   t@(LitTy {})          = t -- Preserve sharing
-tidyType env (TyVarTy tv)          = TyVarTy $! tidyTyCoVarOcc env tv
-tidyType _   t@(TyConApp _ [])     = t -- Preserve sharing if possible
-tidyType env (TyConApp tycon tys)  = TyConApp tycon $! tidyTypes env tys
-tidyType env (AppTy fun arg)       = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
-tidyType env ty@(FunTy _ w arg res)  = let { !w'   = tidyType env w
-                                           ; !arg' = tidyType env arg
-                                           ; !res' = tidyType env res }
-                                       in ty { ft_mult = w', ft_arg = arg', ft_res = res' }
-tidyType env (ty@(ForAllTy{}))     = (mkForAllTys' $! (zip tvs' vis)) $! tidyType env' body_ty
+tidyType _   t@(LitTy {})           = t -- Preserve sharing
+tidyType env (TyVarTy tv)           = TyVarTy $! tidyTyCoVarOcc env tv
+tidyType _   t@(TyConApp _ [])      = t -- Preserve sharing if possible
+tidyType env (TyConApp tycon tys)   = TyConApp tycon $! tidyTypes env tys
+tidyType env (AppTy fun arg)        = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
+tidyType env (CastTy ty co)         = (CastTy $! tidyType env ty) $! (tidyCo env co)
+tidyType env (CoercionTy co)        = CoercionTy $! (tidyCo env co)
+tidyType env ty@(FunTy _ w arg res) = let { !w'   = tidyType env w
+                                          ; !arg' = tidyType env arg
+                                          ; !res' = tidyType env res }
+                                      in ty { ft_mult = w', ft_arg = arg', ft_res = res' }
+tidyType env (ty@(ForAllTy{}))      = tidyForAllType env ty
+
+
+tidyForAllType :: TidyEnv -> Type -> Type
+tidyForAllType env ty
+   = (mkForAllTys' $! (zip tcvs' vis)) $! tidyType body_env body_ty
   where
-    (tvs, vis, body_ty) = splitForAllTyCoVars' ty
-    (env', tvs') = tidyVarBndrs env tvs
-tidyType env (CastTy ty co)       = (CastTy $! tidyType env ty) $! (tidyCo env co)
-tidyType env (CoercionTy co)      = CoercionTy $! (tidyCo env co)
-
+    (tcvs, vis, body_ty) = splitForAllTyCoVars' ty
+    (body_env, tcvs') = tidyVarBndrs env tcvs
 
 -- The following two functions differ from mkForAllTys and splitForAllTyCoVars in that
 -- they expect/preserve the ForAllTyFlag argument. These belong to "GHC.Core.Type", but
@@ -189,24 +266,53 @@ splitForAllTyCoVars' ty = go ty [] []
     go ty                          tvs viss = (reverse tvs, reverse viss, ty)
 
 
+---------------
+tidyAvoiding :: [OccName]
+             -> (TidyEnv -> a -> TidyEnv)
+             -> a -> TidyEnv
+-- Initialise an empty TidyEnv with some bound vars to avoid,
+-- run the do_tidy function, and then remove the bound vars again.
+-- See Note [tidyAvoiding]
+tidyAvoiding bound_var_avoids do_tidy thing
+  = (occs' `delTidyOccEnvList` bound_var_avoids, vars')
+  where
+    (occs', vars') = do_tidy init_tidy_env thing
+    init_tidy_env  = mkEmptyTidyEnv (initTidyOccEnv bound_var_avoids)
+
+---------------
+trimTidyEnv :: TidyEnv -> [TyCoVar] -> TidyEnv
+trimTidyEnv (occ_env, var_env) tcvs
+  = (trimTidyOccEnv occ_env (map getOccName tcvs), var_env)
+
 ---------------
 -- | Grabs the free type variables, tidies them
 -- and then uses 'tidyType' to work over the type itself
-tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
-tidyOpenTypes env tys
-  = (env', tidyTypes (trimmed_occ_env, var_env) tys)
+tidyOpenTypesX :: TidyEnv -> [Type] -> (TidyEnv, [Type])
+-- See Note [Tidying open  types]
+tidyOpenTypesX env tys
+  = (env1, tidyTypes inner_env tys)
+  where
+    free_tcvs :: [TyCoVar] -- Closed over kinds
+    free_tcvs          = tyCoVarsOfTypesList tys
+    (env1, free_tcvs') = tidyFreeTyCoVarsX env free_tcvs
+    inner_env          = trimTidyEnv env1 free_tcvs'
+
+---------------
+tidyOpenTypeX :: TidyEnv -> Type -> (TidyEnv, Type)
+-- See Note [Tidying open  types]
+tidyOpenTypeX env ty
+  = (env1, tidyType inner_env ty)
   where
-    (env'@(_, var_env), tvs') = tidyOpenTyCoVars env $
-                                tyCoVarsOfTypesWellScoped tys
-    trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
-      -- The idea here was that we restrict the new TidyEnv to the
-      -- _free_ vars of the types, so that we don't gratuitously rename
-      -- the _bound_ variables of the types.
+    free_tcvs          = tyCoVarsOfTypeList ty
+    (env1, free_tcvs') = tidyFreeTyCoVarsX env free_tcvs
+    inner_env          = trimTidyEnv env1 free_tcvs'
 
 ---------------
-tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
-tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in
-                      (env', ty')
+tidyOpenTypes :: TidyEnv -> [Type] -> [Type]
+tidyOpenTypes env ty = snd (tidyOpenTypesX env ty)
+
+tidyOpenType :: TidyEnv -> Type -> Type
+tidyOpenType env ty = snd (tidyOpenTypeX env ty)
 
 ---------------
 -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
@@ -219,7 +325,7 @@ tidyTopType ty = tidyType emptyTidyEnv ty
 --
 -- See Note [Strictness in tidyType and friends]
 tidyCo :: TidyEnv -> Coercion -> Coercion
-tidyCo env@(_, subst) co
+tidyCo env co
   = go co
   where
     go_mco MRefl    = MRefl
@@ -236,7 +342,7 @@ tidyCo env@(_, subst) co
             -- of tv. But the alternative is to use coercionKind, which seems worse.
     go (FunCo r afl afr w co1 co2) = ((FunCo r afl afr $! go w) $! go co1) $! go co2
     go (CoVarCo cv)          = CoVarCo $! go_cv cv
-    go (HoleCo h)            = HoleCo h
+    go (HoleCo h)            = HoleCo $! go_hole h
     go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! strictMap go cos
     go (UnivCo p r t1 t2)    = (((UnivCo $! (go_prov p)) $! r) $!
                                 tidyType env t1) $! tidyType env t2
@@ -249,7 +355,10 @@ tidyCo env@(_, subst) co
     go (SubCo co)            = SubCo $! go co
     go (AxiomRuleCo ax cos)  = AxiomRuleCo ax $ strictMap go cos
 
-    go_cv cv = lookupVarEnv subst cv `orElse` cv
+    go_cv cv = tidyTyCoVarOcc env cv
+
+    go_hole (CoercionHole cv r h) = (CoercionHole $! go_cv cv) r h
+    -- Tidy even the holes; tidied types should have tidied kinds
 
     go_prov (PhantomProv co)    = PhantomProv $! go co
     go_prov (ProofIrrelProv co) = ProofIrrelProv $! go co
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 862b934fd1ce..f7be5d244596 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -226,8 +226,10 @@ module GHC.Core.Type (
         -- * Tidying type related things up for printing
         tidyType,      tidyTypes,
         tidyOpenType,  tidyOpenTypes,
-        tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars,
-        tidyOpenTyCoVar, tidyOpenTyCoVars,
+        tidyOpenTypeX, tidyOpenTypesX,
+        tidyVarBndr, tidyVarBndrs,
+        tidyFreeTyCoVars,
+        tidyFreeTyCoVarX, tidyFreeTyCoVarsX,
         tidyTyCoVarOcc,
         tidyTopType,
         tidyForAllTyBinder, tidyForAllTyBinders,
diff --git a/compiler/GHC/Iface/Tidy/StaticPtrTable.hs b/compiler/GHC/Iface/Tidy/StaticPtrTable.hs
index 0b72f57f56bf..cf8b962747db 100644
--- a/compiler/GHC/Iface/Tidy/StaticPtrTable.hs
+++ b/compiler/GHC/Iface/Tidy/StaticPtrTable.hs
@@ -71,6 +71,8 @@ Here is a running example:
   IdBindingInfo] in GHC.Tc.Types).  In our example, 'k' is floatable.
   Even though it is bound in a nested let, we are fine.
 
+  See the call to `checkClosedInStaticForm` in the HsStatic case of `tcExpr`.
+
 * The desugarer replaces the static form with an application of the
   function 'makeStatic' (defined in module GHC.StaticPtr.Internal of
   base).  So we get
diff --git a/compiler/GHC/Rename/Names.hs b/compiler/GHC/Rename/Names.hs
index 1041f6f3c8cd..ffc86cc745ca 100644
--- a/compiler/GHC/Rename/Names.hs
+++ b/compiler/GHC/Rename/Names.hs
@@ -1754,7 +1754,7 @@ warnMissingSignatures gbl_env
              add_binding_warn id =
                when (not_ghc_generated name) $
                do { env <- liftZonkM $ tcInitTidyEnv -- Why not use emptyTidyEnv?
-                  ; let (_, ty) = tidyOpenType env (idType id)
+                  ; let ty = tidyOpenType env (idType id)
                         missing = MissingTopLevelBindingSig name ty
                         diag = TcRnMissingSignature missing exported
                   ; addDiagnosticAt (getSrcSpan name) diag }
diff --git a/compiler/GHC/Runtime/Debugger.hs b/compiler/GHC/Runtime/Debugger.hs
index 5856143b2696..7c6084ba7861 100644
--- a/compiler/GHC/Runtime/Debugger.hs
+++ b/compiler/GHC/Runtime/Debugger.hs
@@ -138,7 +138,7 @@ pprintClosureCommand bindThings force str = do
            -- It's OK to use nonDetEltsUniqSet here because initTidyOccEnv
            -- forgets the ordering immediately by creating an env
                         , getUniqSet $ env_tvs `intersectVarSet` my_tvs)
-     return $ mapTermType (snd . tidyOpenType tidyEnv) t
+     return $ mapTermType (tidyOpenType tidyEnv) t
 
 -- | Give names, and bind in the interactive environment, to all the suspensions
 --   included (inductively) in a term
diff --git a/compiler/GHC/Runtime/Eval.hs b/compiler/GHC/Runtime/Eval.hs
index ac79de089a5d..e8d6c93ae676 100644
--- a/compiler/GHC/Runtime/Eval.hs
+++ b/compiler/GHC/Runtime/Eval.hs
@@ -597,8 +597,8 @@ bindLocalsAtBreakpoint hsc_env apStack_fhv (Just ibi) = do
    let tv_subst     = newTyVars us free_tvs
        (filtered_ids, occs'') = unzip         -- again, sync the occ-names
           [ (id, occ) | (id, Just _hv, occ) <- zip3 ids mb_hValues occs' ]
-       (_,tidy_tys) = tidyOpenTypes emptyTidyEnv $
-                      map (substTy tv_subst . idType) filtered_ids
+       tidy_tys = tidyOpenTypes emptyTidyEnv $
+                  map (substTy tv_subst . idType) filtered_ids
 
    new_ids     <- zipWith3M mkNewId occs'' tidy_tys filtered_ids
    result_name <- newInteractiveBinder hsc_env (mkVarOccFS result_fs) span
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index e911d1059321..c21b95970651 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -61,6 +61,7 @@ import GHC.Core.Predicate
 import GHC.Core.Type
 import GHC.Core.Coercion
 import GHC.Core.TyCo.Ppr     ( pprTyVars )
+import GHC.Core.TyCo.Tidy    ( tidyAvoiding )
 import GHC.Core.InstEnv
 import GHC.Core.TyCon
 import GHC.Core.DataCon
@@ -218,7 +219,8 @@ report_unsolved type_errors expr_holes
 
        ; wanted <- liftZonkM $ zonkWC wanted   -- Zonk to reveal all information
 
-       ; let tidy_env = tidyFreeTyCoVars emptyTidyEnv free_tvs
+       ; let tidy_env = tidyAvoiding bound_occs tidyFreeTyCoVars free_tvs
+                        -- See Note [tidyAvoiding] in GHC.Core.TyCo.Tidy
              free_tvs = filterOut isCoVar $
                         tyCoVarsOfWCList wanted
                         -- tyCoVarsOfWC returns free coercion *holes*, even though
@@ -227,8 +229,12 @@ report_unsolved type_errors expr_holes
                         -- no sense. Really we should not return those holes at all;
                         -- for now we just filter them out.
 
+             bound_occs :: [OccName]
+             bound_occs = boundOccNamesOfWC wanted
+
        ; traceTc "reportUnsolved (after zonking):" $
          vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
+              , text "Bound occs:" <+> ppr bound_occs
               , text "Tidy env:" <+> ppr tidy_env
               , text "Wanted:" <+> ppr wanted ]
 
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 6588b07c4785..1d9970494223 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -3420,7 +3420,7 @@ format_frr_err :: Type  -- ^ the type which doesn't have a fixed runtime represe
 format_frr_err ty
   = (bullet <+> ppr tidy_ty <+> dcolon <+> ppr tidy_ki)
   where
-    (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
+    (tidy_env, tidy_ty) = tidyOpenTypeX emptyTidyEnv ty
     tidy_ki             = tidyType tidy_env (typeKind ty)
 
 pprField :: (FieldLabelString, TcType) -> SDoc
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 4c97a3c99dfb..cdcad7c32534 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -59,7 +59,7 @@ import GHC.Core.Multiplicity
 import GHC.Core.FamInstEnv( normaliseType )
 import GHC.Core.Class   ( Class )
 import GHC.Core.Coercion( mkSymCo )
-import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy)
+import GHC.Core.Type (mkStrLitTy, tidyOpenTypeX, mkCastTy)
 import GHC.Core.TyCo.Ppr( pprTyVars )
 
 import GHC.Builtin.Types ( mkConstraintTupleTy, multiplicityTy, oneDataConTy  )
@@ -1179,7 +1179,7 @@ localSigWarn id mb_sig
 warnMissingSignatures :: Id -> TcM ()
 warnMissingSignatures id
   = do  { env0 <- liftZonkM $ tcInitTidyEnv
-        ; let (env1, tidy_ty) = tidyOpenType env0 (idType id)
+        ; let (env1, tidy_ty) = tidyOpenTypeX env0 (idType id)
         ; let dia = TcRnPolymorphicBinderMissingSig (idName id) tidy_ty
         ; addDiagnosticTcM (env1, dia) }
 
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index ccfcd3dbe040..5084ca3d6da6 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -536,7 +536,9 @@ tcExpr (HsStatic fvs expr) res_ty
                              [liftedTypeKind, expr_ty]
 
         -- Insert the constraints of the static form in a global list for later
-        -- validation.
+        -- validation.  See #13499 for an explanation of why this really isn't the
+        -- right thing to do: the enclosing skolems aren't in scope any more!
+        -- Static forms really aren't well worked out yet.
         ; emitStaticConstraints lie
 
         -- Wrap the static form with the 'fromStaticPtr' call.
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 3b7307a23dd4..4cc228ec57b3 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -1889,8 +1889,7 @@ solverDepthError loc ty
            do { ty   <- TcM.zonkTcType ty
               ; env0 <- TcM.tcInitTidyEnv
               ; return (ty, env0) }
-       ; let tidy_env     = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)
-             tidy_ty      = tidyType tidy_env ty
+       ; let (tidy_env, tidy_ty)  = tidyOpenTypeX env0 ty
              msg = TcRnSolverDepthError tidy_ty depth
        ; TcM.failWithTcM (tidy_env, msg) }
   where
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 86ea603691fb..35b22fbe3ea2 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -22,6 +22,7 @@ module GHC.Tc.Types.Constraint (
         mkNonCanonical, mkGivens,
         tyCoVarsOfCt, tyCoVarsOfCts,
         tyCoVarsOfCtList, tyCoVarsOfCtsList,
+        boundOccNamesOfWC,
 
         -- Particular forms of constraint
         EqCt(..),    eqCtEvidence, eqCtLHS,
@@ -847,6 +848,20 @@ eqCanEqLHS _ _ = False
 ************************************************************************
 -}
 
+---------------- Getting bound tyvars -------------------------
+boundOccNamesOfWC :: WantedConstraints -> [OccName]
+-- Return the OccNames of skolem-bound type variables
+-- We could recurse into types, and get the forall-bound ones too,
+-- but I'm going wait until that is needed
+-- See Note [tidyAvoiding] in GHC.Core.TyCo.Tidy
+boundOccNamesOfWC wc = bagToList (go_wc wc)
+  where
+    go_wc (WC { wc_impl = implics })
+      = concatMapBag go_implic implics
+    go_implic (Implic { ic_skols = tvs, ic_wanted = wc })
+      = listToBag (map getOccName tvs) `unionBags` go_wc wc
+
+
 ---------------- Getting free tyvars -------------------------
 
 -- | Returns free variables of constraints as a non-deterministic set
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 0196988aa018..898fa2b96c30 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1914,7 +1914,8 @@ defaultTyVar def_strat tv
            ; liftZonkM $ writeMetaTyVar kv liftedTypeKind
            ; return True }
       | otherwise
-      = do { addErr $ TcRnCannotDefaultKindVar kv' (tyVarKind kv')
+      = do { let (tidy_env, kv') = tidyFreeTyCoVarX emptyTidyEnv kv
+           ; addErrTcM $ (tidy_env, TcRnCannotDefaultKindVar kv' (tyVarKind kv'))
            -- We failed to default it, so return False to say so.
            -- Hence, it'll get skolemised.  That might seem odd, but we must either
            -- promote, skolemise, or zap-to-Any, to satisfy GHC.Tc.Gen.HsType
@@ -1923,8 +1924,6 @@ defaultTyVar def_strat tv
            -- because we are in an error situation anyway.
            ; return False
         }
-      where
-        (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
 
 -- | Default some unconstrained type variables, as specified
 -- by the defaulting options:
@@ -2130,7 +2129,7 @@ doNotQuantifyTyVars dvs where_found
           -- are OK
        ; let leftover_metas = filter isMetaTyVar undefaulted
        ; unless (null leftover_metas) $
-         do { let (tidy_env1, tidied_tvs) = tidyOpenTyCoVars emptyTidyEnv leftover_metas
+         do { let (tidy_env1, tidied_tvs) = tidyFreeTyCoVarsX emptyTidyEnv leftover_metas
             ; (tidy_env2, where_doc) <- liftZonkM $ where_found tidy_env1
             ; let msg = TcRnUninferrableTyVar tidied_tvs where_doc
             ; failWithTcM (tidy_env2, msg) }
@@ -2491,7 +2490,7 @@ naughtyQuantification orig_ty tv escapees
                              -- we'll just be printing, so no harmful non-determinism
               ; return (orig_ty1, escapees') }
 
-       ; let fvs  = tyCoVarsOfTypeWellScoped orig_ty1
+       ; let fvs  = tyCoVarsOfTypeList orig_ty1
              env0 = tidyFreeTyCoVars emptyTidyEnv fvs
              env  = env0 `delTidyEnvList` escapees'
                     -- this avoids gratuitous renaming of the escaped
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index d8a8919970cd..a02ea15d4f5e 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -290,7 +290,7 @@ checkUserTypeError ctxt ty
 
   | Just msg <- deepUserTypeError_maybe ty
   = do { env0 <- liftZonkM tcInitTidyEnv
-       ; let (env1, tidy_msg) = tidyOpenType env0 msg
+       ; let (env1, tidy_msg) = tidyOpenTypeX env0 msg
        ; failWithTcM (env1, TcRnUserTypeError tidy_msg) }
   | otherwise
   = return ()
@@ -793,7 +793,9 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env
                           , ve_rank = rank, ve_expand = expand }) ty
   | not (null tvbs && null theta)
   = do  { traceTc "check_type" (ppr ty $$ ppr rank)
-        ; checkTcM (forAllAllowed rank) (env, TcRnForAllRankErr rank (tidyType env ty))
+        ; checkTcM (forAllAllowed rank) $
+          let (env1, tidy_ty) = tidyOpenTypeX env ty
+          in  (env1, TcRnForAllRankErr rank tidy_ty)
                 -- Reject e.g. (Maybe (?x::Int => Int)),
                 -- with a decent error message
 
diff --git a/compiler/GHC/Tc/Zonk/TcType.hs b/compiler/GHC/Tc/Zonk/TcType.hs
index 5a19945f070a..471623762a12 100644
--- a/compiler/GHC/Tc/Zonk/TcType.hs
+++ b/compiler/GHC/Tc/Zonk/TcType.hs
@@ -564,12 +564,11 @@ tcInitTidyEnv
 tcInitOpenTidyEnv :: [TyCoVar] -> ZonkM TidyEnv
 tcInitOpenTidyEnv tvs
   = do { env1 <- tcInitTidyEnv
-       ; let env2 = tidyFreeTyCoVars env1 tvs
-       ; return env2 }
+       ; return (tidyFreeTyCoVars env1 tvs) }
 
 zonkTidyTcType :: TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
-                           ; return (tidyOpenType env ty') }
+                           ; return (tidyOpenTypeX env ty') }
 
 zonkTidyTcTypes :: TidyEnv -> [TcType] -> ZonkM (TidyEnv, [TcType])
 zonkTidyTcTypes = zonkTidyTcTypes' []
@@ -646,7 +645,7 @@ zonkTidyFRRInfos = go []
 
     go_mb_not_conc env Nothing = return (env, Nothing)
     go_mb_not_conc env (Just (tv, ty))
-      = do { (env, tv) <- return $ tidyOpenTyCoVar env tv
+      = do { (env, tv) <- return $ tidyFreeTyCoVarX env tv
            ; (env, ty) <- zonkTidyTcType env ty
            ; return (env, Just (tv, ty)) }
 
@@ -658,12 +657,12 @@ tidyCt env = updCtEvidence (tidyCtEvidence env)
 tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
      -- NB: we do not tidy the ctev_evar field because we don't
      --     show it in error messages
-tidyCtEvidence env ctev = ctev { ctev_pred = tidyType env ty }
+tidyCtEvidence env ctev = ctev { ctev_pred = tidyOpenType env ty }
   where
     ty  = ctev_pred ctev
 
 tidyHole :: TidyEnv -> Hole -> Hole
-tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty }
+tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyOpenType env ty }
 
 tidyDelayedError :: TidyEnv -> DelayedError -> DelayedError
 tidyDelayedError env (DE_Hole hole)
diff --git a/compiler/GHC/Types/Name/Occurrence.hs b/compiler/GHC/Types/Name/Occurrence.hs
index 75dff8458104..258d27377dee 100644
--- a/compiler/GHC/Types/Name/Occurrence.hs
+++ b/compiler/GHC/Types/Name/Occurrence.hs
@@ -106,7 +106,7 @@ module GHC.Types.Name.Occurrence (
         mainOcc, ppMainFn,
 
         -- * Tidying up
-        TidyOccEnv, emptyTidyOccEnv, initTidyOccEnv,
+        TidyOccEnv, emptyTidyOccEnv, initTidyOccEnv, trimTidyOccEnv,
         tidyOccName, avoidClashesOccEnv, delTidyOccEnvList,
 
         -- FsEnv
@@ -1142,7 +1142,7 @@ tack on the '1', if necessary.
 
 Note [TidyOccEnv]
 ~~~~~~~~~~~~~~~~~
-type TidyOccEnv = UniqFM Int
+type TidyOccEnv = UniqFM FastString Int
 
 * Domain = The OccName's FastString. These FastStrings are "taken";
            make sure that we don't re-use
@@ -1197,7 +1197,15 @@ would like to see is
 To achieve this, the function avoidClashesOccEnv can be used to prepare the
 TidyEnv, by “blocking” every name that occurs twice in the map. This way, none
 of the "a"s will get the privilege of keeping this name, and all of them will
-get a suitable number by tidyOccName.
+get a suitable number by tidyOccName.  Thus
+
+   avoidNameClashesOccEnv ["a" :-> 7] ["b", "a", "c", "b", "a"]
+     = ["a" :-> 7, "b" :-> 1]
+
+Here
+* "a" is already the TidyOccEnv, and so is unaffected
+* "b" occurs twice, so is blocked by adding "b" :-> 1
+* "c" occurs only once, and so is not affected.
 
 This prepared TidyEnv can then be used with tidyOccName. See tidyTyCoVarBndrs
 for an example where this is used.
@@ -1217,8 +1225,8 @@ initTidyOccEnv = foldl' add emptyUFM
   where
     add env (OccName _ fs) = addToUFM env fs 1
 
-delTidyOccEnvList :: TidyOccEnv -> [FastString] -> TidyOccEnv
-delTidyOccEnvList = delListFromUFM
+delTidyOccEnvList :: TidyOccEnv -> [OccName] -> TidyOccEnv
+delTidyOccEnvList env occs = env `delListFromUFM` map occNameFS occs
 
 -- see Note [Tidying multiple names at once]
 avoidClashesOccEnv :: TidyOccEnv -> [OccName] -> TidyOccEnv
@@ -1262,6 +1270,16 @@ tidyOccName env occ@(OccName occ_sp fs)
                      -- If they are the same (n==1), the former wins
                      -- See Note [TidyOccEnv]
 
+trimTidyOccEnv :: TidyOccEnv -> [OccName] -> TidyOccEnv
+-- Restrict the env to just the [OccName]
+trimTidyOccEnv env vs
+  = foldl' add emptyUFM vs
+  where
+    add :: TidyOccEnv -> OccName -> TidyOccEnv
+    add so_far (OccName _ fs)
+      = case lookupUFM env fs of
+          Just n  -> addToUFM so_far fs n
+          Nothing -> so_far
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Types/Var/Env.hs b/compiler/GHC/Types/Var/Env.hs
index 66a63e1b8de9..bd5c2970ab05 100644
--- a/compiler/GHC/Types/Var/Env.hs
+++ b/compiler/GHC/Types/Var/Env.hs
@@ -470,7 +470,7 @@ mkEmptyTidyEnv occ_env = (occ_env, emptyVarEnv)
 delTidyEnvList :: TidyEnv -> [Var] -> TidyEnv
 delTidyEnvList (occ_env, var_env) vs = (occ_env', var_env')
   where
-    occ_env' = occ_env `delTidyOccEnvList` map (occNameFS . getOccName) vs
+    occ_env' = occ_env `delTidyOccEnvList` map getOccName vs
     var_env' = var_env `delVarEnvList` vs
 
 {-
diff --git a/testsuite/tests/dependent/should_compile/T15743e.stderr b/testsuite/tests/dependent/should_compile/T15743e.stderr
index 923d4bd21b88..5653d37a8c0a 100644
--- a/testsuite/tests/dependent/should_compile/T15743e.stderr
+++ b/testsuite/tests/dependent/should_compile/T15743e.stderr
@@ -54,4 +54,4 @@ DATA CONSTRUCTORS
                 (d :: Proxy k5) (e :: Proxy k7).
          f c -> T k8 a b f c d e
 Dependent modules: []
-Dependent packages: [base-4.19.0.0]
+Dependent packages: [base-4.20.0.0]
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr
index c904a286644b..8302964f1412 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail4.stderr
@@ -1,4 +1,3 @@
-
 T16326_Fail4.hs:6:30: error: [GHC-51580]
     • Illegal visible, dependent quantification in the type of a term:
         forall a1 -> Maybe a1 -> Maybe a1 -> Maybe a1
@@ -10,3 +9,4 @@ T16326_Fail4.hs:6:30: error: [GHC-51580]
         zipWith ((<>) :: forall a -> Maybe a -> Maybe a -> Maybe a) xs ys
     Suggested fix:
       Perhaps you intended to use the ‘RequiredTypeArguments’ extension
+
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr
index 225ca46dd2af..ac0b402e627b 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail5.stderr
@@ -1,4 +1,3 @@
-
 T16326_Fail5.hs:7:20: error: [GHC-51580]
     • Illegal visible, dependent quantification in the type of a term:
         forall a1 -> Maybe a1
@@ -8,3 +7,4 @@ T16326_Fail5.hs:7:20: error: [GHC-51580]
           isJust (Nothing :: forall a -> Maybe a) = False
     Suggested fix:
       Perhaps you intended to use the ‘RequiredTypeArguments’ extension
+
diff --git a/testsuite/tests/indexed-types/should_fail/T13877.stderr b/testsuite/tests/indexed-types/should_fail/T13877.stderr
index 559f2249c714..a63d249370db 100644
--- a/testsuite/tests/indexed-types/should_fail/T13877.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T13877.stderr
@@ -1,7 +1,6 @@
-
 T13877.hs:65:41: error: [GHC-83865]
     • Expecting one more argument to ‘p’
-      Expected kind ‘(-?>) [a] (*) (:->)’, but ‘p’ has kind ‘[a] ~> *’
+      Expected kind ‘(-?>) [a1] (*) (:->)’, but ‘p’ has kind ‘[a1] ~> *’
     • In the type ‘p’
       In the expression: listElimPoly @(:->) @a @p @l
       In an equation for ‘listElimTyFun’:
@@ -9,7 +8,8 @@ T13877.hs:65:41: error: [GHC-83865]
     • Relevant bindings include
         listElimTyFun :: Sing l
                          -> (p @@ '[])
-                         -> (forall (x :: a) (xs :: [a]).
+                         -> (forall (x :: a1) (xs :: [a1]).
                              Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
                          -> p @@ l
           (bound at T13877.hs:65:1)
+
diff --git a/testsuite/tests/indexed-types/should_fail/T14369.stderr b/testsuite/tests/indexed-types/should_fail/T14369.stderr
index 8dcf45bd3060..9bcda7ddcf9b 100644
--- a/testsuite/tests/indexed-types/should_fail/T14369.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14369.stderr
@@ -1,4 +1,3 @@
-
 T14369.hs:29:5: error: [GHC-25897]
     • Couldn't match type ‘a1’ with ‘a2’
       Expected: Sing x -> Maybe (Demote a2)
@@ -19,3 +18,4 @@ T14369.hs:29:5: error: [GHC-25897]
       In an equation for ‘f’: f = fromSing
     • Relevant bindings include
         f :: Sing x -> Maybe (Demote a2) (bound at T14369.hs:29:1)
+
diff --git a/testsuite/tests/patsyn/should_fail/T15695.stderr b/testsuite/tests/patsyn/should_fail/T15695.stderr
index f7f065b024b1..5b18cfd11802 100644
--- a/testsuite/tests/patsyn/should_fail/T15695.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15695.stderr
@@ -1,8 +1,7 @@
-
 T15695.hs:40:14: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce ‘a2 ~ NA VO’
+    • Could not deduce ‘a1 ~ NA VO’
       from the context: ((* -> * -> *) ~ (k -> k1 -> *), Either ~~ f,
-                         ctx ~~ (a2 :&: (a3 :&: E)), f a2 ~~ f1, f1 a3 ~~ a4)
+                         ctx ~~ (a1 :&: (a2 :&: E)), f a1 ~~ f1, f1 a2 ~~ a3)
         bound by a pattern with pattern synonym:
                    ASSO :: forall kind (a :: kind) (b :: Ctx kind).
                            () =>
@@ -13,9 +12,9 @@ T15695.hs:40:14: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
                            a3 -> ApplyT kind a b,
                  in an equation for ‘from'’
         at T15695.hs:40:8-21
-      Expected: a4
-        Actual: Either (NA VO) a3
-      ‘a2’ is a rigid type variable bound by
+      Expected: a3
+        Actual: Either (NA VO) a2
+      ‘a1’ is a rigid type variable bound by
         a pattern with pattern synonym:
           ASSO :: forall kind (a :: kind) (b :: Ctx kind).
                   () =>
@@ -45,3 +44,4 @@ T15695.hs:41:33: warning: [GHC-83865] [-Wdeferred-type-errors (in -Wdefault)]
     • Relevant bindings include
         from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[VO]]
           (bound at T15695.hs:40:1)
+
diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr
index d29fd443e5af..e2f6d0202f01 100644
--- a/testsuite/tests/polykinds/T11520.stderr
+++ b/testsuite/tests/polykinds/T11520.stderr
@@ -1,9 +1,9 @@
-
 T11520.hs:18:77: error: [GHC-25897]
-    • Expected kind ‘k2 -> k1’, but ‘g’ has kind ‘k4’
-      ‘k4’ is a rigid type variable bound by
+    • Expected kind ‘k2 -> k1’, but ‘g’ has kind ‘k’
+      ‘k’ is a rigid type variable bound by
         an instance declaration
         at T11520.hs:18:10-78
     • In the second argument of ‘Compose’, namely ‘g’
       In the first argument of ‘Typeable’, namely ‘(Compose f g)’
       In the instance declaration for ‘Typeable (Compose f g)’
+
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 5b8ca760844f..f3f750869f9f 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -1,4 +1,3 @@
-
 T14846.hs:38:8: error: [GHC-25897]
     • Couldn't match type ‘ríki’ with ‘Hom riki’
       Expected: ríki a a
@@ -34,3 +33,4 @@ T14846.hs:39:44: error: [GHC-25897]
       In an expression type signature: AStruct (Structured a cls)
     • Relevant bindings include
         i :: Hom riki a a (bound at T14846.hs:39:3)
+
diff --git a/testsuite/tests/polykinds/T15787.stderr b/testsuite/tests/polykinds/T15787.stderr
index 5eceea0c8871..5c92f89780b1 100644
--- a/testsuite/tests/polykinds/T15787.stderr
+++ b/testsuite/tests/polykinds/T15787.stderr
@@ -1,9 +1,9 @@
-
 T15787.hs:17:14: error: [GHC-25897]
-    • Expected a type, but ‘k’ has kind ‘ob1’
-      ‘ob1’ is a rigid type variable bound by
+    • Expected a type, but ‘k’ has kind ‘ob’
+      ‘ob’ is a rigid type variable bound by
         the type signature for ‘Kl’
         at T15787.hs:17:3-43
     • In the type ‘k’
       In the definition of data constructor ‘Kl’
       In the data declaration for ‘Kl_kind’
+
diff --git a/testsuite/tests/polykinds/T7278.stderr b/testsuite/tests/polykinds/T7278.stderr
index 52ff5ad28757..98d0dc65e740 100644
--- a/testsuite/tests/polykinds/T7278.stderr
+++ b/testsuite/tests/polykinds/T7278.stderr
@@ -1,8 +1,8 @@
-
 T7278.hs:9:43: error: [GHC-25897]
-    • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k1’
-      ‘k1’ is a rigid type variable bound by
+    • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k’
+      ‘k’ is a rigid type variable bound by
         the type signature for ‘f’
         at T7278.hs:9:1-49
     • In the type signature:
         f :: (C (t :: k) (TF t)) => TF t p1 p0 -> t p1 p0
+
diff --git a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr
index de44490235af..6f6ab60bb910 100644
--- a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr
+++ b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr
@@ -1,24 +1,24 @@
-
 RepPolyNPlusK.hs:22:1: error: [GHC-55287]
     The first pattern in the equation for ‘foo’
     does not have a fixed runtime representation.
     Its type is:
-      a :: TYPE rep2
+      a :: TYPE rep1
 
 RepPolyNPlusK.hs:22:6: error: [GHC-55287]
     • • The first argument of the rebindable syntax operator ‘(>=)’
           arising from the literal ‘2’
         does not have a fixed runtime representation.
         Its type is:
-          a1 :: TYPE rep1
-        Cannot unify ‘rep2’ with the type variable ‘rep1’
+          a1 :: TYPE rep2
+        Cannot unify ‘rep1’ with the type variable ‘rep2’
         because the former is not a concrete ‘RuntimeRep’.
       • The first argument of the rebindable syntax operator ‘(-)’
           arising from the literal ‘2’
         does not have a fixed runtime representation.
         Its type is:
           a0 :: TYPE rep0
-        Cannot unify ‘rep2’ with the type variable ‘rep0’
+        Cannot unify ‘rep1’ with the type variable ‘rep0’
         because the former is not a concrete ‘RuntimeRep’.
     • In the pattern: bndr_a+2
       In an equation for ‘foo’: foo (bndr_a+2) = ()
+
diff --git a/testsuite/tests/rep-poly/T13233.stderr b/testsuite/tests/rep-poly/T13233.stderr
index f25b31228826..d40aee3850bd 100644
--- a/testsuite/tests/rep-poly/T13233.stderr
+++ b/testsuite/tests/rep-poly/T13233.stderr
@@ -1,4 +1,3 @@
-
 T13233.hs:14:11: error: [GHC-55287]
     • • The first component of the unboxed tuple
         does not have a fixed runtime representation.
@@ -32,3 +31,4 @@ T13233.hs:22:16: error: [GHC-55287]
     • In the first argument of ‘obscure’, namely ‘(#,#)’
       In the expression: obscure (#,#)
       In an equation for ‘quux’: quux = obscure (#,#)
+
diff --git a/testsuite/tests/rep-poly/T21906.stderr b/testsuite/tests/rep-poly/T21906.stderr
index 6b891d999044..19d1fe8e02cc 100644
--- a/testsuite/tests/rep-poly/T21906.stderr
+++ b/testsuite/tests/rep-poly/T21906.stderr
@@ -1,4 +1,3 @@
-
 T21906.hs:14:17: error: [GHC-55287]
     • The return type of the third argument of the primop ‘keepAlive#’
       does not have a fixed runtime representation.
@@ -13,7 +12,7 @@ T21906.hs:21:25: error: [GHC-55287]
     • The return type of the first argument of the primop ‘catch#’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE q0
+        a :: TYPE q1
       Cannot unify ‘r’ with the type variable ‘q1’
       because the former is not a concrete ‘RuntimeRep’.
     • In the expression: catch# action handle s
@@ -40,3 +39,4 @@ T21906.hs:35:19: error: [GHC-55287]
     • In the first argument of ‘fork#’, namely ‘f’
       In the expression: fork# f s
       In an equation for ‘test4’: test4 f s = fork# f s
+
diff --git a/testsuite/tests/th/T21050.stderr b/testsuite/tests/th/T21050.stderr
index 4d2a84e27435..2cb78089abf1 100644
--- a/testsuite/tests/th/T21050.stderr
+++ b/testsuite/tests/th/T21050.stderr
@@ -1,4 +1,3 @@
-
 T21050.hs:8:18: error: [GHC-25897]
     • Couldn't match expected type ‘Code m a1’ with actual type ‘p’
       ‘p’ is a rigid type variable bound by
@@ -12,11 +11,11 @@ T21050.hs:8:18: error: [GHC-25897]
         f :: p -> Code m T (bound at T21050.hs:8:1)
 
 T21050.hs:11:18: error: [GHC-91028]
-    • Couldn't match type ‘a’ with ‘forall a2. a2’
+    • Couldn't match type ‘a’ with ‘forall a1. a1’
       Expected: Code Q a
         Actual: Code Q (forall a. a)
       Cannot equate type variable ‘a’
-      with a type involving polytypes: forall a2. a2
+      with a type involving polytypes: forall a1. a1
       ‘a’ is a rigid type variable bound by
         a type expected by the context:
           forall a. a
@@ -24,3 +23,4 @@ T21050.hs:11:18: error: [GHC-91028]
     • In the expression: x
       In the Template Haskell splice $$(x)
       In the first argument of ‘MkT’, namely ‘$$(x)’
+
diff --git a/testsuite/tests/typecheck/no_skolem_info/T13499.stderr b/testsuite/tests/typecheck/no_skolem_info/T13499.stderr
index 5b1f358f54a6..efc97f7f1393 100644
--- a/testsuite/tests/typecheck/no_skolem_info/T13499.stderr
+++ b/testsuite/tests/typecheck/no_skolem_info/T13499.stderr
@@ -1,14 +1,14 @@
-
 T13499.hs:7:19: error: [GHC-88464]
-    • Found hole: _ :: a
-      Where: ‘a’ is a rigid type variable bound by
+    • Found hole: _ :: a1
+      Where: ‘a1’ is a rigid type variable bound by
                the type signature for:
-                 f :: forall a. Typeable a => StaticPtr (a -> a)
+                 f :: forall a1. Typeable a1 => StaticPtr (a1 -> a1)
                at T13499.hs:6:1-37
     • In the body of a static form: (\ a -> _)
       In the expression: static (\ a -> _)
       In an equation for ‘f’: f = static (\ a -> _)
     • Relevant bindings include
-        a :: a (bound at T13499.hs:7:14)
-        f :: StaticPtr (a -> a) (bound at T13499.hs:7:1)
-      Valid hole fits include a :: a (bound at T13499.hs:7:14)
+        a :: a1 (bound at T13499.hs:7:14)
+        f :: StaticPtr (a1 -> a1) (bound at T13499.hs:7:1)
+      Valid hole fits include a :: a1 (bound at T13499.hs:7:14)
+
diff --git a/testsuite/tests/typecheck/no_skolem_info/T20063.stderr b/testsuite/tests/typecheck/no_skolem_info/T20063.stderr
index dc52976fe093..e9b8decef209 100644
--- a/testsuite/tests/typecheck/no_skolem_info/T20063.stderr
+++ b/testsuite/tests/typecheck/no_skolem_info/T20063.stderr
@@ -1,27 +1,27 @@
-
 T20063.hs:25:21: error: [GHC-25897]
-    • Could not deduce ‘ctx4 ~ (ctx0 :*& l0)’
-      from the context: (ctx1 ~ Extend ctx7, ctx2 ~ Extend ctx8)
+    • Could not deduce ‘ctx6 ~ (ctx0 :*& l0)’
+      from the context: (ctx4 ~ Extend ctx1, ctx5 ~ Extend ctx2)
         bound by a pattern with constructor:
                    U :: forall {k} (ctx1 :: Context) (ctx2 :: Context) (l :: k).
                         Rn ctx1 ctx2 -> Rn (ctx1 :*& l) (ctx2 :*& l),
                  in an equation for ‘rnRename’
         at T20063.hs:25:11-13
-      Expected: Idx ctx4
+      Expected: Idx ctx6
         Actual: Idx (ctx0 :*& l0)
-      ‘ctx4’ is a rigid type variable bound by
+      ‘ctx6’ is a rigid type variable bound by
         the type signature for:
-          rnRename :: forall (ctx1 :: Context) (ctx2 :: Context)
-                             (ctx3 :: Context) (ctx4 :: Context).
-                      Rn ctx1 ctx2 -> Idx ctx3 -> Idx ctx4
+          rnRename :: forall (ctx4 :: Context) (ctx5 :: Context)
+                             (ctx3 :: Context) (ctx6 :: Context).
+                      Rn ctx4 ctx5 -> Idx ctx3 -> Idx ctx6
         at T20063.hs:24:1-48
     • In the expression: T _
       In an equation for ‘rnRename’: rnRename (U _) _ = T _
     • Relevant bindings include
-        rnRename :: Rn ctx1 ctx2 -> Idx ctx3 -> Idx ctx4
+        rnRename :: Rn ctx4 ctx5 -> Idx ctx3 -> Idx ctx6
           (bound at T20063.hs:25:1)
 
 T20063.hs:26:17: error: [GHC-27346]
     • The data constructor ‘T’ should have 1 argument, but has been given none
     • In the pattern: T
       In an equation for ‘rnRename’: rnRename _ T = undefined
+
diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr
index a73dfff4f107..978e370ebc3d 100644
--- a/testsuite/tests/typecheck/should_compile/T9834.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9834.stderr
@@ -1,4 +1,3 @@
-
 T9834.hs:23:12: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type ‘a’ with ‘p a0’
       Expected: p a
@@ -51,3 +50,4 @@ T9834.hs:23:23: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
                  Comp p q a -> Comp p q a)
                 -> p a
           (bound at T9834.hs:23:3)
+
diff --git a/testsuite/tests/typecheck/should_compile/tc214.stderr b/testsuite/tests/typecheck/should_compile/tc214.stderr
index 6751f31a5ccf..396713b4405d 100644
--- a/testsuite/tests/typecheck/should_compile/tc214.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc214.stderr
@@ -1,4 +1,3 @@
-
 tc214.hs:19:1: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
     Pattern match has inaccessible right hand side
     In an equation for ‘bar2’: bar2 (F2 _) = ...
@@ -16,3 +15,4 @@ tc214.hs:19:7: warning: [GHC-40564] [-Winaccessible-code (in -Wdefault)]
         at tc214.hs:19:7-10
     • In the pattern: F2 _
       In an equation for ‘bar2’: bar2 (F2 _) = ()
+
diff --git a/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr b/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
index ae71b40a9161..8c08d4afad54 100644
--- a/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
+++ b/testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
@@ -1,20 +1,20 @@
-
 GivenForallLoop.hs:8:11: error: [GHC-25897]
     • Could not deduce ‘a ~ b’
-      from the context: a ~ (forall b1. F a b1)
+      from the context: a ~ (forall b. F a b)
         bound by the type signature for:
-                   loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+                   loopy :: forall a b. (a ~ (forall b. F a b)) => a -> b
         at GivenForallLoop.hs:7:1-42
       ‘a’ is a rigid type variable bound by
         the type signature for:
-          loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+          loopy :: forall a b. (a ~ (forall b. F a b)) => a -> b
         at GivenForallLoop.hs:7:1-42
       ‘b’ is a rigid type variable bound by
         the type signature for:
-          loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+          loopy :: forall a b. (a ~ (forall b. F a b)) => a -> b
         at GivenForallLoop.hs:7:1-42
     • In the expression: x
       In an equation for ‘loopy’: loopy x = x
     • Relevant bindings include
         x :: a (bound at GivenForallLoop.hs:8:7)
         loopy :: a -> b (bound at GivenForallLoop.hs:8:1)
+
diff --git a/testsuite/tests/typecheck/should_fail/T10709.stderr b/testsuite/tests/typecheck/should_fail/T10709.stderr
index b27ed794a1a2..1c2e5908cc2c 100644
--- a/testsuite/tests/typecheck/should_fail/T10709.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10709.stderr
@@ -1,12 +1,9 @@
-
 T10709.hs:6:21: error: [GHC-91028]
-    • Couldn't match type ‘a2’
-                     with ‘(forall a4. IO a4 -> IO a4) -> IO a3’
+    • Couldn't match type ‘a2’ with ‘(forall a. IO a -> IO a) -> 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 a4. IO a4 -> IO a4) -> IO a3
+      with a type involving polytypes: (forall a. IO a -> IO a) -> IO a3
       ‘a2’ is a rigid type variable bound by
         the inferred type of x1 :: a2 -> IO [a3]
         at T10709.hs:6:1-24
@@ -31,13 +28,14 @@ T10709.hs:7:22: error: [GHC-91028]
 
 T10709.hs:8:22: error: [GHC-91028]
     • Couldn't match type ‘a0’
-                     with ‘(forall a2. IO a2 -> IO a2) -> IO a’
+                     with ‘(forall a1. IO a1 -> IO a1) -> IO a’
       Expected: a0 -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘a0’
       with a type involving polytypes:
-        (forall a2. IO a2 -> IO a2) -> IO a
+        (forall a1. IO a1 -> IO a1) -> IO a
     • In the second argument of ‘(.)’, namely ‘mask’
       In the first argument of ‘($)’, namely ‘(replicateM 2 . mask)’
       In the expression: (replicateM 2 . mask) $ undefined
     • Relevant bindings include x3 :: IO [a] (bound at T10709.hs:8:1)
+
diff --git a/testsuite/tests/typecheck/should_fail/T10709b.stderr b/testsuite/tests/typecheck/should_fail/T10709b.stderr
index e4741ddcc188..ff36de6226e4 100644
--- a/testsuite/tests/typecheck/should_fail/T10709b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10709b.stderr
@@ -1,4 +1,3 @@
-
 T10709b.hs:6:22: error: [GHC-91028]
     • Couldn't match type ‘t2’ with ‘forall a. IO a -> IO a’
       Expected: (t2 -> IO ()) -> IO ()
@@ -11,46 +10,47 @@ T10709b.hs:6:22: error: [GHC-91028]
           x4 = (replicateM 2 . mask) (\ _ -> return ())
 
 T10709b.hs:7:22: error: [GHC-91028]
-    • Couldn't match type ‘t1’ with ‘forall a1. IO a1 -> IO a1’
+    • Couldn't match type ‘t1’ with ‘forall a. IO a -> IO a’
       Expected: (t1 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘t1’
-      with a type involving polytypes: forall a1. IO a1 -> IO a1
+      with a type involving polytypes: forall a. IO a -> IO a
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (\ x -> undefined x)
       In an equation for ‘x5’:
           x5 = (replicateM 2 . mask) (\ x -> undefined x)
 
 T10709b.hs:8:22: error: [GHC-91028]
-    • Couldn't match type ‘t0’ with ‘forall a1. IO a1 -> IO a1’
+    • Couldn't match type ‘t0’ with ‘forall a. IO a -> IO a’
       Expected: (t0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘t0’
-      with a type involving polytypes: forall a1. IO a1 -> IO a1
+      with a type involving polytypes: forall a. IO a -> IO a
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (id (\ _ -> undefined))
       In an equation for ‘x6’:
           x6 = (replicateM 2 . mask) (id (\ _ -> undefined))
 
 T10709b.hs:9:22: error: [GHC-91028]
-    • Couldn't match type ‘b0’ with ‘forall a1. IO a1 -> IO a1’
+    • Couldn't match type ‘b0’ with ‘forall a. IO a -> IO a’
       Expected: (b0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘b0’
-      with a type involving polytypes: forall a1. IO a1 -> IO a1
+      with a type involving polytypes: forall a. IO a -> IO a
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression: (replicateM 2 . mask) (const undefined)
       In an equation for ‘x7’:
           x7 = (replicateM 2 . mask) (const undefined)
 
 T10709b.hs:10:22: error: [GHC-91028]
-    • Couldn't match type ‘a0’ with ‘forall a1. IO a1 -> IO a1’
+    • Couldn't match type ‘a0’ with ‘forall a. IO a -> IO a’
       Expected: (a0 -> IO a) -> IO a
         Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
       Cannot instantiate unification variable ‘a0’
-      with a type involving polytypes: forall a1. IO a1 -> IO a1
+      with a type involving polytypes: forall a. IO a -> IO a
     • In the second argument of ‘(.)’, namely ‘mask’
       In the expression:
         (replicateM 2 . mask) ((\ x -> undefined x) :: a -> b)
       In an equation for ‘x8’:
           x8 = (replicateM 2 . mask) ((\ x -> undefined x) :: a -> b)
+
diff --git a/testsuite/tests/typecheck/should_fail/T13909.stderr b/testsuite/tests/typecheck/should_fail/T13909.stderr
index 02067ba714d6..58f290a52343 100644
--- a/testsuite/tests/typecheck/should_fail/T13909.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13909.stderr
@@ -1,4 +1,3 @@
-
 T13909.hs:11:18: error: [GHC-91028]
     • Expecting two more arguments to ‘Hm’
       Expected kind ‘k’, but ‘Hm’ has kind ‘forall k -> k -> *’
@@ -9,3 +8,4 @@ T13909.hs:11:18: error: [GHC-91028]
         at T13909.hs:11:10-19
     • In the first argument of ‘HasName’, namely ‘Hm’
       In the instance declaration for ‘HasName Hm’
+
diff --git a/testsuite/tests/typecheck/should_fail/T16059c.stderr b/testsuite/tests/typecheck/should_fail/T16059c.stderr
index bcd19e928550..b31859edff53 100644
--- a/testsuite/tests/typecheck/should_fail/T16059c.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16059c.stderr
@@ -1,7 +1,7 @@
-
 T16059c.hs:6:6: error: [GHC-91510]
-    • Illegal polymorphic type: forall a1. a1
+    • Illegal polymorphic type: forall a. a
     • In the expansion of type synonym ‘Foo’
       In the type signature: f :: Foo -> a -> f
     Suggested fix:
       Perhaps you intended to use the ‘RankNTypes’ extension (implied by ‘ImpredicativeTypes’)
+
diff --git a/testsuite/tests/typecheck/should_fail/T17077.stderr b/testsuite/tests/typecheck/should_fail/T17077.stderr
index d20a2226bef3..fc9102c30e5e 100644
--- a/testsuite/tests/typecheck/should_fail/T17077.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17077.stderr
@@ -1,7 +1,7 @@
-
 T17077.hs:7:13: error: [GHC-91028]
     • Expected kind ‘forall (k :: k1). a’, but ‘z’ has kind ‘k0’
       Cannot instantiate unification variable ‘k0’
-      with a kind involving polytypes: forall (k2 :: k1). a
+      with a kind involving polytypes: forall (k :: k1). a
     • In the first argument of ‘Proxy’, namely ‘(z :: forall k. a)’
       In the type signature: t :: Proxy (z :: forall k. a)
+
diff --git a/testsuite/tests/typecheck/should_fail/T19415.stderr b/testsuite/tests/typecheck/should_fail/T19415.stderr
index 7135b2caffa6..fc6315d6614a 100644
--- a/testsuite/tests/typecheck/should_fail/T19415.stderr
+++ b/testsuite/tests/typecheck/should_fail/T19415.stderr
@@ -1,10 +1,10 @@
-
 T19415.hs:27:8: error: [GHC-18872]
     • Couldn't match type ‘[Char]’ with ‘Char’
         arising from a functional dependency between:
-          constraint ‘SetField "name" (Pet a) (Pet b) Char’
+          constraint ‘SetField "name" (Pet a1) (Pet b) Char’
             arising from a use of ‘setField’
-          instance ‘SetField "name" (Pet a1) (Pet b1) String’
+          instance ‘SetField "name" (Pet a) (Pet b1) String’
             at T19415.hs:(23,3)-(24,60)
     • In the expression: setField @"name" 'c' (Pet "hi")
       In an equation for ‘loop’: loop = setField @"name" 'c' (Pet "hi")
+
diff --git a/testsuite/tests/typecheck/should_fail/T24868.hs b/testsuite/tests/typecheck/should_fail/T24868.hs
new file mode 100644
index 000000000000..2c708a06d399
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T24868.hs
@@ -0,0 +1,19 @@
+module BadErr where
+
+data T f a = T (f a)
+
+class C f where
+  method :: f a -> r
+
+-- badErr :: C c1 => T c1 b -> r
+-- badErr = method
+
+worseErr :: (C c1, C c2) => T c1 b -> T c2 b -> r
+worseErr = method
+
+foo :: T c a -> r
+foo = undefined
+
+bar1, bar2 :: C f => f a -> r
+bar1 = foo
+bar2 = foo
diff --git a/testsuite/tests/typecheck/should_fail/T24868.stderr b/testsuite/tests/typecheck/should_fail/T24868.stderr
new file mode 100644
index 000000000000..f3ced7159c86
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T24868.stderr
@@ -0,0 +1,37 @@
+T24868.hs:12:12: error: [GHC-39999]
+    • Could not deduce ‘C (T c1)’ arising from a use of ‘method’
+      from the context: (C c1, C c2)
+        bound by the type signature for:
+                   worseErr :: forall {k} (c1 :: k -> *) (c2 :: k -> *) (b :: k) r.
+                               (C c1, C c2) =>
+                               T c1 b -> T c2 b -> r
+        at T24868.hs:11:1-49
+    • In the expression: method
+      In an equation for ‘worseErr’: worseErr = method
+
+T24868.hs:18:8: error: [GHC-25897]
+    • Couldn't match type ‘f’ with ‘T c0’
+      Expected: f a -> r
+        Actual: T c0 a -> r
+      ‘f’ is a rigid type variable bound by
+        the type signature for:
+          bar1 :: forall {k} (f :: k -> *) (a :: k) r. C f => f a -> r
+        at T24868.hs:17:1-29
+    • In the expression: foo
+      In an equation for ‘bar1’: bar1 = foo
+    • Relevant bindings include
+        bar1 :: f a -> r (bound at T24868.hs:18:1)
+
+T24868.hs:19:8: error: [GHC-25897]
+    • Couldn't match type ‘f’ with ‘T c4’
+      Expected: f a -> r
+        Actual: T c4 a -> r
+      ‘f’ is a rigid type variable bound by
+        the type signature for:
+          bar2 :: forall {k} (f :: k -> *) (a :: k) r. C f => f a -> r
+        at T24868.hs:17:1-29
+    • In the expression: foo
+      In an equation for ‘bar2’: bar2 = foo
+    • Relevant bindings include
+        bar2 :: f a -> r (bound at T24868.hs:19:1)
+
diff --git a/testsuite/tests/typecheck/should_fail/T9196.stderr b/testsuite/tests/typecheck/should_fail/T9196.stderr
index d008378e9593..d7fb08bb1149 100644
--- a/testsuite/tests/typecheck/should_fail/T9196.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9196.stderr
@@ -1,6 +1,5 @@
-
 T9196.hs:4:6: error: [GHC-91510]
-    • Illegal polymorphic type: forall a1. Eq a1
+    • Illegal polymorphic type: forall a. Eq a
       A constraint must be a monotype
     • In the type signature: f :: (forall a. Eq a) => a -> a
     Suggested fix:
@@ -12,3 +11,4 @@ T9196.hs:7:6: error: [GHC-91510]
     • In the type signature: g :: (Eq a => Ord a) => a -> a
     Suggested fix:
       Perhaps you intended to use the ‘QuantifiedConstraints’ extension
+
diff --git a/testsuite/tests/typecheck/should_fail/TcStaticPointersFail03.stderr b/testsuite/tests/typecheck/should_fail/TcStaticPointersFail03.stderr
index 169b2d2a02f2..0c3e806d81a5 100644
--- a/testsuite/tests/typecheck/should_fail/TcStaticPointersFail03.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcStaticPointersFail03.stderr
@@ -1,6 +1,6 @@
-
 TcStaticPointersFail03.hs:9:29: error: [GHC-39999]
-    • No instance for ‘Monad m’ arising from a use of ‘return’
+    • No instance for ‘Monad m1’ arising from a use of ‘return’
     • In the body of a static form: return
       In the first argument of ‘deRefStaticPtr’, namely ‘(static return)’
       In the expression: deRefStaticPtr (static return)
+
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 9670111fc479..6ccf9ef7efc4 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -727,3 +727,4 @@ test('T17594g', normal, compile_fail, [''])
 test('T24470a', normal, compile_fail, [''])
 test('T24553', normal, compile_fail, [''])
 test('T23739b', normal, compile_fail, [''])
+test('T24868', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index a09795f1debf..bd50f5e51091 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,4 +1,3 @@
-
 tcfail201.hs:17:27: error: [GHC-25897]
     • Couldn't match expected type ‘a’ with actual type ‘HsDoc id0’
       ‘a’ is a rigid type variable bound by
@@ -15,3 +14,4 @@ tcfail201.hs:17:27: error: [GHC-25897]
         gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
                    -> (forall g. g -> c g) -> a -> c a
           (bound at tcfail201.hs:16:1)
+
-- 
GitLab