More wibbleswip/T15809

and rebase on today's master

19 files changed, 98 insertions, 76 deletions

diff --git a/compiler/basicTypes/OccName.hs b/compiler/basicTypes/OccName.hs
index 3032c0ccd8..c4c5db4767 100644
--- a/compiler/basicTypes/OccName.hs
+++ b/compiler/basicTypes/OccName.hs
@@ -858,10 +858,15 @@ avoidClashesOccEnv env occs = go env emptyUFM occs
 
 tidyOccName :: TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
 tidyOccName env occ@(OccName occ_sp fs)
+{-
   | not (fs `elemUFM` env)
     && (fs /= fsLit "_")
         -- See Note [Always number wildcard types when tidying]
   = (addToUFM env fs 1, occ)   -- Desired OccName is free
+-}
+  | isUnderscoreFS fs
+  = (env, occ)
+
   | otherwise
   = case lookupUFM env base1 of
        Nothing -> (addToUFM env base1 2, OccName occ_sp base1)
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 6f5ea359e5..63513a0e84 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -789,7 +789,7 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi
                bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
                do { stupid_theta <- tcHsContext hs_ctxt
                   ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc mb_clsinfo hs_pats
-                  ; mapM_ (wrapLocM kcConDecl) hs_cons
+                  ; mapM_ (wrapLocM_ kcConDecl) hs_cons
                   ; res_kind <- tc_kind_sig m_ksig
                   ; lhs_ty <- checkExpectedKindX pp_lhs lhs_ty lhs_kind res_kind
                   ; return (stupid_theta, lhs_ty, res_kind) }
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 2f553c51cc..5925fc8975 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -325,8 +325,8 @@ tcPatSynSig name sig_ty
   , (ex_hs_tvs,   hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1
   = do {  traceTc "tcPatSynSig 1" (ppr sig_ty)
        ; (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
-           <- solveEqualities                   $
-                -- See Note [solveEqualities in tcPatSynSig]
+           <- pushTcLevelM_   $
+              solveEqualities $ -- See Note [solveEqualities in tcPatSynSig]
               bindImplicitTKBndrs_Skol implicit_hs_tvs $
               bindExplicitTKBndrs_Skol univ_hs_tvs     $
               bindExplicitTKBndrs_Skol ex_hs_tvs       $
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index a52dc5eb3f..2c23681203 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1189,7 +1189,8 @@ reifyInstances th_nm th_tys
                do { (rn_ty, fvs) <- rnLHsType doc rdr_ty
                   ; return ((tv_names, rn_ty), fvs) }
         ; (_tvs, ty)
-            <- solveEqualities                  $ -- Avoid error cascade if there are unsolved
+            <- pushTcLevelM_   $
+               solveEqualities $ -- Avoid error cascade if there are unsolved
                bindImplicitTKBndrs_Skol tv_names $
                fst <$> tcLHsType rn_ty
         ; ty <- zonkTcTypeToType ty
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 9e869c3db9..9bd419a15a 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -909,7 +909,7 @@ getInitialKind :: Bool -> TyClDecl GhcRn -> TcM [TcTyCon]
 -- No family instances are passed to getInitialKinds
 
 getInitialKind cusk
-    (ClassDecl { tcdLName = dl->L _ name
+    (ClassDecl { tcdLName = dL->L _ name
                , tcdTyVars = ktvs
                , tcdATs = ats })
   = do { tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $
@@ -921,7 +921,7 @@ getInitialKind cusk
        ; return (tycon : inner_tcs) }
 
 getInitialKind cusk
-    (DataDecl { tcdLName = dl->L _ name
+    (DataDecl { tcdLName = dL->L _ name
               , tcdTyVars = ktvs
               , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                          , dd_ND = new_or_data } })
@@ -936,7 +936,7 @@ getInitialKind _ (FamDecl { tcdFam = decl })
   = do { tc <- getFamDeclInitialKind Nothing decl
        ; return [tc] }
 
-getInitialKind cusk (SynDecl { tcdLName = dl->L _ name
+getInitialKind cusk (SynDecl { tcdLName = dL->L _ name
                              , tcdTyVars = ktvs
                              , tcdRhs = rhs })
   = do  { tycon <- kcLHsQTyVars name TypeSynonymFlavour cusk ktvs $
@@ -994,7 +994,7 @@ getFamDeclInitialKind _ (XFamilyDecl _) = panic "getFamDeclInitialKind"
 ------------------------------------------------------------------------
 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
   -- See Note [Kind checking for type and class decls]
-kcLTyClDecl (dl->L loc decl)
+kcLTyClDecl (dL->L loc decl)
   = setSrcSpan loc $
     tcAddDeclCtxt decl $
     do { traceTc "kcTyClDecl {" (ppr tc_name)
@@ -1026,7 +1026,7 @@ kcTyClDecl (DataDecl { tcdLName    = (dL->L _ name)
     do  { _ <- tcHsContext ctxt
         ; mapM_ (wrapLocM_ kcConDecl) cons }
 
-kcTyClDecl (SynDecl { tcdLName = dl->L _ name, tcdRhs = rhs })
+kcTyClDecl (SynDecl { tcdLName = dL->L _ name, tcdRhs = rhs })
   = bindTyClTyVars name $ \ _ res_kind ->
     discardResult $ tcCheckLHsType rhs res_kind
         -- NB: check against the result kind that we allocated
@@ -1311,7 +1311,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
              roles = roles_info tycon_name  -- for TyCon and Class
 
        ; (ctxt, fds, sig_stuff, at_stuff)
-            <- solveEqualities $
+            <- pushTcLevelM_   $
+               solveEqualities $
                do { ctxt <- tcHsContext hs_ctxt
                   ; fds  <- mapM (addLocM tc_fundep) fundeps
                   ; sig_stuff <- tcClassSigs class_name sigs meths
@@ -1638,7 +1639,9 @@ tcTySynRhs :: RolesInfo
 tcTySynRhs roles_info tc_name binders res_kind hs_ty
   = do { env <- getLclEnv
        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
-       ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
+       ; rhs_ty <- pushTcLevelM_   $
+                   solveEqualities $
+                   tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType rhs_ty
        ; let roles = roles_info tc_name
              tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
@@ -1664,7 +1667,7 @@ tcDataDefn roles_info
        ; unless (mk_permissive_kind hsc_src cons) $
          checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind)
 
-       ; stupid_tc_theta <- solveEqualities $ tcHsContext ctxt
+       ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt
        ; stupid_theta    <- zonkTcTypesToTypes stupid_tc_theta
        ; kind_signatures <- xoptM LangExt.KindSignatures
 
@@ -1718,11 +1721,11 @@ kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
 -- Used for the equations of a closed type family only
 -- Not used for data/type instances
 kcTyFamInstEqn tc_fam_tc
-    (dl->L loc (HsIB { hsib_ext = imp_vars
-                 , hsib_body = FamEqn { feqn_tycon = dL->L _ eqn_tc_name
-                                      , feqn_bndrs = mb_expl_bndrs
-                                      , feqn_pats  = hs_pats
-                                      , feqn_rhs   = hs_rhs_ty }}))
+    (dL->L loc (HsIB { hsib_ext = imp_vars
+                     , hsib_body = FamEqn { feqn_tycon = dL->L _ eqn_tc_name
+                                          , feqn_bndrs = mb_expl_bndrs
+                                          , feqn_pats  = hs_pats
+                                          , feqn_rhs   = hs_rhs_ty }}))
   = setSrcSpan loc $
     do { traceTc "kcTyFamInstEqn" (vcat
            [ text "tc_name ="    <+> ppr eqn_tc_name
@@ -1750,8 +1753,8 @@ kcTyFamInstEqn tc_fam_tc
     fam_name  = tyConName tc_fam_tc
     vis_arity = length (tyConVisibleTyVars tc_fam_tc)
 
-kcTyFamInstEqn _ (dl->L _ (XHsImplicitBndrs _)) = panic "kcTyFamInstEqn"
-kcTyFamInstEqn _ (dl->L _ (HsIB _ (XFamEqn _))) = panic "kcTyFamInstEqn"
+kcTyFamInstEqn _ (dL->L _ (XHsImplicitBndrs _)) = panic "kcTyFamInstEqn"
+kcTyFamInstEqn _ (dL->L _ (HsIB _ (XFamEqn _))) = panic "kcTyFamInstEqn"
 kcTyFamInstEqn _ _ = panic "kcTyFamInstEqn: Impossible Match" -- due to #15884
 
 
@@ -1762,7 +1765,7 @@ tcTyFamInstEqn :: TcTyCon -> AssocInstInfo -> LTyFamInstEqn GhcRn
 -- (typechecked here) have TyFamInstEqns
 
 tcTyFamInstEqn fam_tc mb_clsinfo
-    (dl->L loc (HsIB { hsib_ext = imp_vars
+    (dL->L loc (HsIB { hsib_ext = imp_vars
                  , hsib_body = FamEqn { feqn_tycon  = L _ eqn_tc_name
                                       , feqn_bndrs  = mb_expl_bndrs
                                       , feqn_pats   = hs_pats
@@ -1789,8 +1792,7 @@ tcTyFamInstEqn fam_tc mb_clsinfo
                               (map (const Nominal) qtvs)
                               loc) }
 
-tcTyFamInstEqn _ _ (dL->L _ (XHsImplicitBndrs _)) = panic "tcTyFamInstEqn"
-tcTyFamInstEqn _ _ (dL->L _ (HsIB _ (XFamEqn _))) = panic "tcTyFamInstEqn"
+tcTyFamInstEqn _ _ _ = panic "tcTyFamInstEqn"
 
 {-
 Kind check type patterns and kind annotate the embedded type variables.
@@ -2231,7 +2233,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
            , hsq_explicit = explicit_tkv_nms } <- qtvs
   = addErrCtxt (dataConCtxtName names) $
     do { traceTc "tcConDecl 1 gadt" (ppr names)
-       ; let (dl->L _ name : _) = names
+       ; let ((dL->L _ name) : _) = names
 
        ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
            <- pushTcLevelM_    $  -- We are going to generalise
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 92697ca4f9..374d82242a 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1791,7 +1791,8 @@ checkFamPatBinders :: TyCon
 --     cause a crash; notably in tcConDecl in tcDataFamInstDecl
 checkFamPatBinders fam_tc qtvs pats rhs
   = do { traceTc "checkFamPatBinders" $
-         vcat [ ppr (mkTyConApp fam_tc pats)
+         vcat [ debugPprType (mkTyConApp fam_tc pats)
+              , ppr (mkTyConApp fam_tc pats)
               , text "qtvs:" <+> ppr qtvs
               , text "rhs_tvs:" <+> ppr (fvVarSet rhs_fvs)
               , text "pat_tvs:" <+> ppr pat_tvs
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 529f90a964..819973e4b1 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -935,8 +935,8 @@ mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
 mkTransCo co1 co2                 = TransCo co1 co2
 
 mkNthCo :: HasDebugCallStack
-        => Role  -- the role of the coercion you're creating
-        -> Int
+        => Role  -- The role of the coercion you're creating
+        -> Int   -- Zero-indexed
         -> Coercion
         -> Coercion
 mkNthCo r n co
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index d727250c00..5989902313 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -690,10 +690,27 @@ mkCoAxBranch tvs cvs lhs rhs roles loc
                , cab_loc     = loc
                , cab_incomps = placeHolderIncomps }
   where
-    (env1, tvs1) = tidyVarBndrs emptyTidyEnv tvs
-    (env,  cvs1) = tidyVarBndrs env1         cvs
+    used = tyCoVarsOfTypes (map varType tvs) `unionVarSet`
+           tyCoVarsOfTypes (map varType cvs) `unionVarSet`
+           tyCoVarsOfType rhs
+    (env1, tvs1) = mapAccumL tidy_bndr emptyTidyEnv tvs
+    (env,  cvs1) = mapAccumL tidy_bndr env1         cvs
     -- See Note [Tidy axioms when we build them]
 
+    tidy_bndr env bndr
+      | isUnderscoreFS (occNameFS old_occ) = tidy_wildcard
+      | otherwise                          = tidyVarBndr env bndr
+      where
+        tidy_wildcard | bndr `elemVarSet` used
+                      = tidyVarBndr env (bndr `setVarName` new_name)
+                      | otherwise
+                      = (env, bndr)
+
+        old_name = Var.varName bndr
+        old_occ  = getOccName old_name
+        new_name = tidyNameOcc old_name new_occ
+        new_occ  = mkOccName (occNameSpace old_occ) "x"
+
 -- all of the following code is here to avoid mutual dependencies with
 -- Coercion
 mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index aa67e06a2a..623d4c4984 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1341,7 +1341,7 @@ interfaces.  Notably this plays a role in tcTySigs in TcBinds.hs.
                                 ~~~~~~~~
 -}
 
--- | Make a dependent forall over an Inferred variable
+-- | Make a dependent forall over an Inferred variablem
 mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
 mkTyCoInvForAllTy tv ty
   | isCoVar tv
@@ -1439,15 +1439,6 @@ splitTyVarForAllTys ty = split ty ty []
     split _ (ForAllTy (Bndr tv _) ty) tvs | isTyVar tv = split ty ty (tv:tvs)
     split orig_ty _                   tvs              = (reverse tvs, orig_ty)
 
--- | Like 'splitPiTys' but split off only /named/ binders.
-splitForAllVarBndrs :: Type -> ([TyCoVarBinder], Type)
-splitForAllVarBndrs ty = split ty ty []
-  where
-    split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
-    split _       (ForAllTy b res) bs = split res res (b:bs)
-    split orig_ty _                bs = (reverse bs, orig_ty)
-{-# INLINE splitForAllVarBndrs #-}
-
 -- | Checks whether this is a proper forall (with a named binder)
 isForAllTy :: Type -> Bool
 isForAllTy ty | Just ty' <- coreView ty = isForAllTy ty'
@@ -1531,19 +1522,29 @@ splitPiTy ty
 -- | Split off all TyCoBinders to a type, splitting both proper foralls
 -- and functions
 splitPiTys :: Type -> ([TyCoBinder], Type)
-splitPiTys ty = split ty ty
+splitPiTys ty = split ty ty []
+  where
+    split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
+    split _       (ForAllTy b res) bs = split res res (Named b  : bs)
+    split _       (FunTy arg res)  bs = split res res (Anon arg : bs)
+    split orig_ty _                bs = (reverse bs, orig_ty)
+
+-- | Like 'splitPiTys' but split off only /named/ binders
+--   and returns TyCoVarBinders rather than TyCoBinders
+splitForAllVarBndrs :: Type -> ([TyCoVarBinder], Type)
+splitForAllVarBndrs ty = split ty ty []
   where
-    split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty'
-    split _       (ForAllTy b res) = let (bs, ty) = split res res
-                                     in  (Named b : bs, ty)
-    split _       (FunTy arg res)  = let (bs, ty) = split res res
-                                     in  (Anon arg : bs, ty)
-    split orig_ty _                = ([], orig_ty)
+    split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
+    split _       (ForAllTy b res) bs = split res res (b:bs)
+    split orig_ty _                bs = (reverse bs, orig_ty)
+{-# INLINE splitForAllVarBndrs #-}
 
 invisibleTyBndrCount :: Type -> Int
 -- Returns the number of leading invisible forall'd binders in the type
-invisibleTyBndrCount ty = countWhile (isInvisibleArgFlag . binderArgFlag) $
-                          fst $ splitForAllVarBndrs ty
+-- Includes invisible predicate arguments; e.g. for
+--    e.g.  forall {k}. (k ~ *) => k -> k
+-- returns 2 not 1
+invisibleTyBndrCount ty = length (fst (splitPiTysInvisible ty))
 
 -- Like splitPiTys, but returns only *invisible* binders, including constraints
 -- Stops at the first visible binder
diff --git a/compiler/utils/FastString.hs b/compiler/utils/FastString.hs
index f9fbeb0e6e..588486bf46 100644
--- a/compiler/utils/FastString.hs
+++ b/compiler/utils/FastString.hs
@@ -71,6 +71,7 @@ module FastString
         concatFS,
         consFS,
         nilFS,
+        isUnderscoreFS,
 
         -- ** Outputing
         hPutFS,
@@ -603,6 +604,9 @@ uniqueOfFS (FastString u _ _ _) = u
 nilFS :: FastString
 nilFS = mkFastString ""
 
+isUnderscoreFS :: FastString -> Bool
+isUnderscoreFS fs = fs == fsLit "_"
+
 -- -----------------------------------------------------------------------------
 -- Stats
 
diff --git a/testsuite/tests/dependent/should_compile/T13910.hs b/testsuite/tests/dependent/should_compile/T13910.hs
index e0e2955614..b3707dd365 100644
--- a/testsuite/tests/dependent/should_compile/T13910.hs
+++ b/testsuite/tests/dependent/should_compile/T13910.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{- # LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
@@ -15,13 +15,6 @@ module T13910 where
 import Data.Kind
 import Data.Type.Equality
 
-class SingKind k where
-  type Demote k = (r :: Type) | r -> k
-
-instance SingKind (a :~: b) where
-  type Demote (a :~: b) = a :~: b
-
-{-
 data family Sing (a :: k)
 
 class SingKind k where
@@ -153,4 +146,3 @@ leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
              -> f @@ a
              -> f @@ b
 leibnizTyFun = leibnizPoly @(:~>) @_ @f
--}
\ No newline at end of file
diff --git a/testsuite/tests/dependent/should_compile/T15725.hs b/testsuite/tests/dependent/should_compile/T15725.hs
index 1e2e1710c3..a5f259ea9e 100644
--- a/testsuite/tests/dependent/should_compile/T15725.hs
+++ b/testsuite/tests/dependent/should_compile/T15725.hs
@@ -23,12 +23,12 @@ instance SC Identity
 
 -------------------------------------------------------------------------------
 
-data family Sing :: k -> Type
-data instance Sing ::  Identity a -> Type where
+data family Sing :: forall k. k -> Type
+data instance Sing :: forall a. Identity a -> Type where
   SIdentity :: Sing x -> Sing ('Identity x)
 
 newtype Par1 p = Par1 p
-data instance Sing ::  Par1 p -> Type where
+data instance Sing :: forall p. Par1 p -> Type where
   SPar1 :: Sing x -> Sing ('Par1 x)
 
 type family Rep1 (f :: Type -> Type) :: Type -> Type
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index ef5465f020..c6698d2944 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -41,7 +41,7 @@
     Type family equation violates injectivity annotation.
     Kind variable ‘k1’ cannot be inferred from the right-hand side.
     In the type family equation:
-      PolyKindVarsF @{[k2]} @[k1] ('[] @k2) = '[] @k1
+      PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2
         -- Defined at <interactive>:55:41
 
 <interactive>:60:15: error:
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr
index bc5fd2a72e..074424b98e 100644
--- a/testsuite/tests/indexed-types/should_compile/T15852.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T15852.stderr
@@ -1,13 +1,13 @@
 TYPE CONSTRUCTORS
   type role DF nominal nominal nominal
-  DF :: forall k. * -> k -> *
+  DF{3} :: forall k. * -> k -> *
 COERCION AXIOMS
   axiom T15852.D:R:DFProxyProxy0 ::
-    forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).
-      DF (Proxy c) a = T15852.R:DFProxyProxy k1 k2 c j a
+    forall k1 k2 (j :: k1) (c :: k2) (a :: Proxy j).
+      DF (Proxy c) a = T15852.R:DFProxyProxy k1 k2 j c a
         -- Defined at T15852.hs:10:15
 FAMILY INSTANCES
-  data instance DF (Proxy c) c j a
+  data instance DF (Proxy c) j c a
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
index c488f45a65..2d21177b6a 100644
--- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
+++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs
@@ -4,9 +4,10 @@
 module ExplicitForAllFams4 where
 
 type family J a
-type instance forall a b. J [a]    = Float
-type instance forall b.   J _      = Maybe b
+type instance forall a . J [a]    = Float
+type instance forall .   J _      = Int
 
+{-
 data family K a
 data instance forall a b. K (a, Bool) = K5 Float
 data instance forall b.   K _         = K6 (Maybe b)
@@ -25,3 +26,4 @@ instance C Int where
 
   data forall a b. CD [a] (a,a)     = CD5 Float
   data forall b.   CD _ _           = CD6 (Maybe b)
+-}
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/T12041.stderr b/testsuite/tests/indexed-types/should_fail/T12041.stderr
index c12f8857b6..234524f60e 100644
--- a/testsuite/tests/indexed-types/should_fail/T12041.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T12041.stderr
@@ -1,8 +1,7 @@
 
 T12041.hs:12:8: error:
     • Type indexes must match class instance head
-      Expected: Ob I
-        Actual: Ob I
-      Use -fprint-explicit-kinds to see the kind arguments
+      Expected: Ob @i (I @{i} @{i})
+        Actual: Ob @* (I @{*} @{*})
     • In the type instance declaration for ‘Ob’
       In the instance declaration for ‘Category I’
diff --git a/testsuite/tests/indexed-types/should_fail/T9160.stderr b/testsuite/tests/indexed-types/should_fail/T9160.stderr
index fe56587387..a6ccaa497c 100644
--- a/testsuite/tests/indexed-types/should_fail/T9160.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9160.stderr
@@ -1,8 +1,7 @@
 
 T9160.hs:20:8: error:
     • Type indexes must match class instance head
-      Expected: F
-        Actual: F
-      Use -fprint-explicit-kinds to see the kind arguments
+      Expected: F @*
+        Actual: F @(* -> *)
     • In the type instance declaration for ‘F’
       In the instance declaration for ‘C (a :: *)’
diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr
index 29185377a9..31a37fec63 100644
--- a/testsuite/tests/polykinds/T14450.stderr
+++ b/testsuite/tests/polykinds/T14450.stderr
@@ -1,8 +1,7 @@
 
 T14450.hs:33:8: error:
     • Type indexes must match class instance head
-      Expected: Dom IddSym0
-        Actual: Dom IddSym0
-      Use -fprint-explicit-kinds to see the kind arguments
+      Expected: Dom @k @k (IddSym0 @k)
+        Actual: Dom @* @* (IddSym0 @*)
     • In the type instance declaration for ‘Dom’
       In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 9dc8c55d3b..84af180b20 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -61,7 +61,7 @@ T6018fail.hs:61:10: error:
     Type family equation violates injectivity annotation.
     Kind variable ‘k1’ cannot be inferred from the right-hand side.
     In the type family equation:
-      PolyKindVarsF @{[k2]} @[k1] ('[] @k2) = '[] @k1
+      PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2
         -- Defined at T6018fail.hs:61:10
 
 T6018fail.hs:64:15: error: