Fix a bug in occurs checking

1. Trac #12593 exposed a long-standing bug in the occurs
   checking machinery.  When unifying two type variables
          a ~ b
   where a /= b, we were assuming that there could be
   no occurs-check error.  But there can: 'a' can occur
   in b's kind!  When the RHS was a non-tyvar we used
   occurCheckExpand, which /did/ look in kinds, but not
   when the RHS was a tyvar.

   This bug has been lurking ever since TypeInType, maybe
   longer.  And it was present both in TcUnify (the on-the-fly
   unifier), and in TcInteract.

   I ended up refactoring both so that the tyvar/tyvar
   path naturally goes through the same occurs-check as
   non-tyvar rhss.  It's simpler and more robust now.

   One good thing is that both unifiers now share
       TcType.swapOverVars
       TcType.canSolveByUnification
   previously they had different logic for the same goals

2. Fixing this bug exposed another!  In T11635 we end
   up unifying
   (alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
   Now that the occurs check is done for tyvars too, we
   look inside beta's kind.  And then reject the program
   becuase of the forall inside there.  But in fact that
   forall is fine -- it does not count as impredicative
   polymoprhism.   See Note [Checking for foralls]
   in TcType.

3. All this fuss around occurrence checking forced me
   to look at TcUnify.checkTauTvUpdate
          and TcType.occurCheckExpand
   There's a lot of duplication there, and I managed
   to elminate quite a bit of it. For example,
   checkTauTvUpdate called a local 'defer_me'; and then
   called occurCheckExpand, which then used a very
   similar 'fast_check'.

   Things are better, but there is more to do.

10 files changed, 370 insertions, 347 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index b6a76c762b..3f121bd898 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -10,6 +10,7 @@ module TcCanonical(
 #include "HsVersions.h"
 
 import TcRnTypes
+import TcUnify( swapOverTyVars )
 import TcType
 import Type
 import TcFlatten
@@ -22,7 +23,6 @@ import Coercion
 import FamInstEnv ( FamInstEnvs )
 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
 import Var
-import Name( isSystemName )
 import Outputable
 import DynFlags( DynFlags )
 import VarSet
@@ -654,13 +654,13 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
          `andWhenContinue` \ new_ev ->
          can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 
--- Type variable on LHS or RHS are last. We want only flat types sent
--- to canEqTyVar.
+-- Type variable on LHS or RHS are last.
+-- NB: pattern match on True: we want only flat types sent to canEqTyVar.
 -- See also Note [No top-level newtypes on RHS of representational equalities]
-can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
-  = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
-can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
-  = canEqTyVar ev eq_rel IsSwapped  tv2 ps_ty1
+can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2
+  = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2
+can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
+  = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1
 
 -- We've flattened and the types don't match. Give up.
 can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2
@@ -1335,18 +1335,26 @@ canCFunEqCan ev fn tys fsk
                                  , cc_tyargs = tys', cc_fsk = fsk }) } }
 
 ---------------------
-canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
-           -> TcTyVar             -- already flat
-           -> TcType              -- already flat
+canEqTyVar :: CtEvidence          -- ev :: lhs ~ rhs
+           -> EqRel -> SwapFlag
+           -> TcTyVar -> TcType   -- lhs: already flat, not a cast
+           -> TcType -> TcType    -- rhs: already flat, not a cast
            -> TcS (StopOrContinue Ct)
--- A TyVar on LHS, but so far un-zonked
-canEqTyVar ev eq_rel swapped tv1 ps_ty2              -- ev :: tv ~ s2
-  = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
+canEqTyVar ev eq_rel swapped tv1 ps_ty1 (TyVarTy tv2) _
+  | tv1 == tv2
+  = canEqReflexive ev eq_rel ps_ty1
+
+  | swapOverTyVars tv1 tv2
+  = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
          -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
          -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
          -- Flatten the RHS less vigorously, to avoid gratuitous flattening
          -- True <=> xi2 should not itself be a type-function application
        ; dflags <- getDynFlags
+       ; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 ps_ty1 }
+
+canEqTyVar ev eq_rel swapped tv1 _ _ ps_ty2
+  = do { dflags <- getDynFlags
        ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
 
 canEqTyVar2 :: DynFlags
@@ -1361,21 +1369,17 @@ canEqTyVar2 :: DynFlags
 -- preserved as much as possible
 
 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
-  | Just (tv2, kco2) <- getCastedTyVar_maybe xi2
-  = canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
-
   | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2  -- No occurs check
-     -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
-     -- to establish the invariant that a does not appear in the
-     -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
-     -- see Note [Occurs check expansion] in TcType
-  = rewriteEqEvidence ev swapped xi1 xi2' co1 (mkTcReflCo role xi2')
+     -- Must do the occurs check even on tyvar/tyvar
+     -- equalities, in case have  x ~ (y :: ..x...)
+     -- Trac #12593
+  = rewriteEqEvidence ev swapped xi1 xi2' co1 co2
     `andWhenContinue` \ new_ev ->
     homogeniseRhsKind new_ev eq_rel xi1 xi2' $ \new_new_ev xi2'' ->
     CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
              , cc_rhs = xi2'', cc_eq_rel = eq_rel }
 
-  | otherwise  -- Occurs check error
+  | otherwise  -- Occurs check error (or a forall)
   = do { traceTcS "canEqTyVar2 occurs check error" (ppr tv1 $$ ppr xi2)
        ; rewriteEqEvidence ev swapped xi1 xi2 co1 co2
          `andWhenContinue` \ new_ev ->
@@ -1394,117 +1398,13 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
              -- canonical, and we might loop if we were to use it in rewriting.
          else do { traceTcS "Occurs-check in representational equality"
                            (ppr xi1 $$ ppr xi2)
-                      ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
+                 ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
   where
     role = eqRelRole eq_rel
     xi1  = mkTyVarTy tv1
     co1  = mkTcReflCo role xi1
     co2  = mkTcReflCo role xi2
 
-canEqTyVarTyVar :: CtEvidence           -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
-                -> EqRel
-                -> SwapFlag
-                -> TcTyVar -> TcTyVar   -- tv1, tv2
-                -> Coercion             -- the co in (rhs = tv2 |> co)
-                -> TcS (StopOrContinue Ct)
--- Both LHS and RHS rewrote to a type variable
--- See Note [Canonical orientation for tyvar/tyvar equality constraints]
-canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
-  | tv1 == tv2
-  = do { let mk_coh = case swapped of IsSwapped  -> mkTcCoherenceLeftCo
-                                      NotSwapped -> mkTcCoherenceRightCo
-       ; setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1 `mk_coh` kco2)
-       ; stopWith ev "Equal tyvars" }
-
--- We don't do this any more
--- See Note [Orientation of equalities with fmvs] in TcFlatten
---  | isFmvTyVar tv1  = do_fmv swapped            tv1 xi1 xi2 co1 co2
---  | isFmvTyVar tv2  = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
-
-  | swap_over       = do_swap
-  | otherwise       = no_swap
-  where
-    role = eqRelRole eq_rel
-    xi1 = mkTyVarTy tv1
-    co1 = mkTcReflCo role xi1
-    xi2 = mkTyVarTy tv2
-    co2 = mkTcReflCo role xi2 `mkTcCoherenceRightCo` kco2
-
-    no_swap = canon_eq swapped            tv1 xi1 xi2 co1 co2
-    do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
-
-    canon_eq swapped tv1 ty1 ty2 co1 co2
-        -- ev  : tv1 ~ orhs  (not swapped) or   orhs ~ tv1   (swapped)
-        -- co1 : xi1 ~ tv1
-        -- co2 : xi2 ~ tv2
-      = do { traceTcS "canEqTyVarTyVar"
-               (vcat [ ppr swapped
-                     , ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
-                     , ppr ty1 <+> dcolon <+> ppr (typeKind ty1)
-                     , ppr ty2 <+> dcolon <+> ppr (typeKind ty2)
-                     , ppr co1 <+> dcolon <+> ppr (tcCoercionKind co1)
-                     , ppr co2 <+> dcolon <+> ppr (tcCoercionKind co2) ])
-           ; rewriteEqEvidence ev swapped ty1 ty2 co1 co2
-             `andWhenContinue` \ new_ev ->
-             homogeniseRhsKind new_ev eq_rel ty1 ty2 $ \new_new_ev ty2' ->
-             CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
-                      , cc_rhs = ty2', cc_eq_rel = eq_rel } }
-
-{- We don't do this any more
-   See Note [Orientation of equalities with fmvs] in TcFlatten
-    -- tv1 is the flatten meta-var
-    do_fmv swapped tv1 xi1 xi2 co1 co2
-      | same_kind
-      = canon_eq swapped tv1 xi1 xi2 co1 co2
-      | otherwise  -- Presumably tv1 :: *, since it is a flatten meta-var,
-                   -- at a kind that has some interesting sub-kind structure.
-                   -- Since the two kinds are not the same, we must have
-                   -- tv1 `subKind` tv2, which is the wrong way round
-                   --   e.g.  (fmv::*) ~ (a::OpenKind)
-                   -- So make a new meta-var and use that:
-                   --         fmv ~ (beta::*)
-                   --         (a::OpenKind) ~ (beta::*)
-      = ASSERT2( k1_sub_k2,
-                 ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
-                 ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
-        ASSERT2( isWanted ev, ppr ev )  -- Only wanteds have flatten meta-vars
-        do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
-           ; new_ev <- newWantedEvVarNC (ctEvLoc ev)
-                                        (mkPrimEqPredRole (eqRelRole eq_rel)
-                                           g           tv_ty xi2)
-           ; emitWorkNC [new_ev]
-           ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
--}
-
-    swap_over
-      -- If tv1 is touchable, swap only if tv2 is also
-      -- touchable and it's strictly better to update the latter
-      -- But see Note [Avoid unnecessary swaps]
-      | Just lvl1 <- metaTyVarTcLevel_maybe tv1
-      = case metaTyVarTcLevel_maybe tv2 of
-          Nothing   -> False
-          Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
-                    | lvl1 `strictlyDeeperThan` lvl2 -> False
-                    | otherwise                      -> nicer_to_update_tv2
-
-      -- So tv1 is not a meta tyvar
-      -- If only one is a meta tyvar, put it on the left
-      -- This is not because it'll be solved; but because
-      -- the floating step looks for meta tyvars on the left
-      | isMetaTyVar tv2 = True
-
-      -- So neither is a meta tyvar (including FlatMetaTv)
-
-      -- If only one is a flatten skolem, put it on the left
-      -- See Note [Eliminate flat-skols]
-      | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
-
-      | otherwise = False
-
-    nicer_to_update_tv2
-      =  (isSigTyVar tv1                 && not (isSigTyVar tv2))
-      || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
-
 -- | Solve a reflexive equality constraint
 canEqReflexive :: CtEvidence    -- ty ~ ty
                -> EqRel
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 583ca622f9..75224d8001 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -13,6 +13,7 @@ import BasicTypes ( infinity, IntWithInf, intGtLimit )
 import HsTypes ( HsIPName(..) )
 import TcCanonical
 import TcFlatten
+import TcUnify( canSolveByUnification )
 import VarSet
 import Type
 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
@@ -1124,56 +1125,33 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
 
        ; stopWith ev "Solved from inert (r)" }
 
+  | ReprEq <- eq_rel   -- We never solve representational
+  = unsolved_inert     -- equalities by unification
+
+  | isGiven ev         -- See Note [Touchables and givens]
+  = unsolved_inert
+
   | otherwise
   = do { tclvl <- getTcLevel
-       ; if canSolveByUnification tclvl ev eq_rel tv rhs
+       ; if canSolveByUnification tclvl tv rhs
          then do { solveByUnification ev tv rhs
                  ; n_kicked <- kickOutAfterUnification tv
                  ; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) }
 
-         else do { traceTcS "Can't solve tyvar equality"
-                       (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
-                             , ppWhen (isMetaTyVar tv) $
-                               nest 4 (text "TcLevel of" <+> ppr tv
-                                       <+> text "is" <+> ppr (metaTyVarTcLevel tv))
-                             , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
-                             , text "TcLevel =" <+> ppr tclvl ])
-                 ; addInertEq workItem
-                 ; return (Stop ev (text "Kept as inert")) } }
-
-interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
+         else unsolved_inert }
 
--- @trySpontaneousSolve wi@ solves equalities where one side is a
--- touchable unification variable.
--- Returns True <=> spontaneous solve happened
-canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
-                      -> TcTyVar -> Xi -> Bool
-canSolveByUnification tclvl gw eq_rel tv xi
-  | ReprEq <- eq_rel   -- we never solve representational equalities this way.
-  = False
-
-  | isGiven gw   -- See Note [Touchables and givens]
-  = False
-
-  | isTouchableMetaTyVar tclvl tv
-  = case metaTyVarInfo tv of
-      SigTv -> is_tyvar xi
-      _     -> True
-
-  | otherwise    -- Untouchable
-  = False
   where
-    is_tyvar xi
-      = case tcGetTyVar_maybe xi of
-          Nothing -> False
-          Just tv -> case tcTyVarDetails tv of
-                       MetaTv { mtv_info = info }
-                                   -> case info of
-                                        SigTv -> True
-                                        _     -> False
-                       SkolemTv {} -> True
-                       FlatSkol {} -> False
-                       RuntimeUnk  -> True
+    unsolved_inert
+      = do { traceTcS "Can't solve tyvar equality"
+                (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+                      , ppWhen (isMetaTyVar tv) $
+                        nest 4 (text "TcLevel of" <+> ppr tv
+                                <+> text "is" <+> ppr (metaTyVarTcLevel tv))
+                      , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ])
+           ; addInertEq workItem
+           ; return (Stop ev (text "Kept as inert")) }
+
+interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
 
 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
 -- Solve with the identity coercion
@@ -1449,7 +1427,9 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty
        ; dischargeFmv old_ev fsk final_co alpha_ty
        ; traceTcS "doTopReactFunEq (occurs)" $
          vcat [ text "old_ev:" <+> ppr old_ev
-              , nest 2 (text ":=") <+> ppr final_co
+              , nest 2 (text ":=") <+>
+                   if isDerived old_ev then text "(derived)"
+                   else ppr final_co
               , text "new_ev:" <+> ppr new_ev ]
        ; stopWith old_ev "Fun/Top (wanted)" }
   where
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index e4d6a4b05e..bd64f541ac 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -83,6 +83,7 @@ module TcType (
   ---------------------------------
   -- Misc type manipulators
   deNoteType, occurCheckExpand, OccCheckResult(..),
+  occCheckExpand,
   orphNamesOfType, orphNamesOfCo,
   orphNamesOfTypes, orphNamesOfCoCon,
   getDFunTyKey,
@@ -1564,7 +1565,49 @@ The two variants of the function are to support TcUnify.checkTauTvUpdate,
 which wants to prevent unification with type families. For more on this
 point, see Note [Prevent unification with type families] in TcUnify.
 
-See also Note [occurCheckExpand] in TcCanonical
+Note [Occurrence checking: look inside kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are considering unifying
+   (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
+This may be an error (what is that alpha doing inside beta's kind?),
+but we must not make the mistake of actuallyy unifying or we'll
+build an infinite data structure.  So when looking for occurrences
+of alpha in the rhs, we must look in the kinds of type variables
+that occur there.
+
+NB: we may be able to remove the problem via expansion; see
+    Note [Occurs check expansion].  So we have to try that.
+
+Note [Checking for foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Unless we have -XImpredicativeTypes (which is a totally unsupported
+feature), we do not want to unify
+    alpha ~ (forall a. a->a) -> Int
+So we look for foralls hidden inside the type, and it's convenient
+to do that at the same time as the occurs check (which looks for
+occurrences of alpha).
+
+However, it's not just a question of looking for foralls /anywhere/!
+Consider
+   (alpha :: forall k. k->*)  ~  (beta :: forall k. k->*)
+This is legal; e.g. dependent/should_compile/T11635.
+
+We don't want to reject it because of the forall in beta's kind,
+but (see Note [Occurrence checking: look inside kinds]) we do
+need to look in beta's kind.  So we carry a flag saying if a 'forall'
+is OK, and sitch the flag on when stepping inside a kind.
+
+Why is it OK?  Why does it not count as impredicative polymorphism?
+The reason foralls are bad is because we reply on "seeing" foralls
+when doing implicit instantiation.  But the forall inside the kind is
+fine.  We'll generate a kind equality constraint
+  (forall k. k->*) ~ (forall k. k->*)
+to check that the kinds of lhs and rhs are compatible.  If alpha's
+kind had instead been
+  (alpha :: kappa)
+then this kind equality would rightly complain about unifying kappa
+with (forall k. k->*)
+
 -}
 
 data OccCheckResult a
@@ -1602,39 +1645,63 @@ occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
 --        - TcUnify.checkTauTvUpdate (on-the-fly unifier)
 --        - TcInteract.canSolveByUnification (main constraint solver)
 occurCheckExpand dflags tv ty
-  | fast_check ty = return ty
-  | otherwise     = go emptyVarEnv ty
+  = case fast_check impredicative ty of
+      OC_OK _   -> OC_OK ty
+      OC_Forall -> OC_Forall
+      OC_Occurs -> case occCheckExpand tv ty of
+                     Nothing  -> OC_Occurs
+                     Just ty' -> OC_OK ty'
   where
-    details = tcTyVarDetails tv
-
+    details       = tcTyVarDetails tv
     impredicative = canUnifyWithPolyType dflags details
 
-    -- True => fine
-    fast_check (LitTy {})          = True
-    fast_check (TyVarTy tv')       = tv /= tv' && fast_check (tyVarKind tv')
-    fast_check (TyConApp tc tys)   = all fast_check tys
-                                     && (isTauTyCon tc || impredicative)
-    fast_check (FunTy a r)         = fast_check a && fast_check r
-    fast_check (AppTy fun arg)     = fast_check fun && fast_check arg
-    fast_check (ForAllTy (TvBndr tv' _) ty)
-                                   = impredicative
-                                   && fast_check (tyVarKind tv')
-                                   && (tv == tv' || fast_check ty)
-    fast_check (CastTy ty co)      = fast_check ty && fast_check_co co
-    fast_check (CoercionTy co)     = fast_check_co co
+    ok :: OccCheckResult ()
+    ok = OC_OK ()
+
+    fast_check :: Bool -> TcType -> OccCheckResult ()
+      -- True <=> Foralls are ok; otherwise stop with OC_Forall
+      -- See Note [Checking for foralls]
+
+    fast_check _ (TyVarTy tv')
+      | tv == tv' = OC_Occurs
+      | otherwise = fast_check True (tyVarKind tv')
+           -- See Note [Occurrence checking: look inside kinds]
+
+    fast_check b (TyConApp tc tys)
+      | not (b || isTauTyCon tc) = OC_Forall
+      | otherwise                = mapM (fast_check b) tys >> ok
+    fast_check _ (LitTy {})      = ok
+    fast_check b (FunTy a r)     = fast_check b a   >> fast_check b r
+    fast_check b (AppTy fun arg) = fast_check b fun >> fast_check b arg
+    fast_check b (CastTy ty co)  = fast_check b ty >> fast_check_co co
+    fast_check _ (CoercionTy co) = fast_check_co co
+    fast_check b (ForAllTy (TvBndr tv' _) ty)
+       | not b     = OC_Forall
+       | tv == tv' = ok
+       | otherwise = do { fast_check True (tyVarKind tv')
+                        ; fast_check b ty }
 
      -- we really are only doing an occurs check here; no bother about
      -- impredicativity in coercions, as they're inferred
-    fast_check_co co = not (tv `elemVarSet` tyCoVarsOfCo co)
+    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
+                     | otherwise                       = ok
 
-    go :: VarEnv TyVar  -- carries mappings necessary because of kind expansion
-       -> Type -> OccCheckResult Type
+
+occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
+occCheckExpand tv ty
+  = go emptyVarEnv ty
+  where
+    go :: VarEnv TyVar -> Type -> Maybe Type
+          -- The Varenv carries mappings necessary
+          -- because of kind expansion
     go env (TyVarTy tv')
-      | tv == tv'                         = OC_Occurs
+      | tv == tv'                         = Nothing
       | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
       | otherwise                         = do { k' <- go env (tyVarKind tv')
                                                ; return (mkTyVarTy $
                                                          setTyVarKind tv' k') }
+           -- See Note [Occurrence checking: look inside kinds]
+
     go _   ty@(LitTy {}) = return ty
     go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
                                 ; ty2' <- go env ty2
@@ -1643,29 +1710,22 @@ occurCheckExpand dflags tv ty
                                 ; ty2' <- go env ty2
                                 ; return (mkFunTy ty1' ty2') }
     go env ty@(ForAllTy (TvBndr tv' vis) body_ty)
-       | not impredicative = OC_Forall
        | tv == tv'         = return ty
-       | otherwise         = do { ki' <- go env ki
+       | otherwise         = do { ki' <- go env (tyVarKind tv')
                                 ; let tv'' = setTyVarKind tv' ki'
                                       env' = extendVarEnv env tv' tv''
                                 ; body' <- go env' body_ty
                                 ; return (ForAllTy (TvBndr tv'' vis) body') }
-      where ki = tyVarKind tv'
 
     -- For a type constructor application, first try expanding away the
     -- offending variable from the arguments.  If that doesn't work, next
     -- see if the type constructor is a type synonym, and if so, expand
     -- it and try again.
     go env ty@(TyConApp tc tys)
-      = case do { tys <- mapM (go env) tys
-                ; return (mkTyConApp tc tys) } of
-          OC_OK ty
-              | impredicative || isTauTyCon tc
-              -> return ty  -- First try to eliminate the tyvar from the args
-              | otherwise
-              -> OC_Forall  -- A type synonym with a forall on the RHS
-          bad | Just ty' <- coreView ty -> go env ty'
-              | otherwise               -> bad
+      = case mapM (go env) tys of
+          Just tys' -> return (mkTyConApp tc tys')
+          Nothing | Just ty' <- coreView ty -> go env ty'
+                  | otherwise               -> Nothing
                       -- Failing that, try to expand a synonym
 
     go env (CastTy ty co) =  do { ty' <- go env ty
@@ -1683,7 +1743,6 @@ occurCheckExpand dflags tv ty
                                              ; arg' <- go_co env arg
                                              ; return (mkAppCo co' arg') }
     go_co env co@(ForAllCo tv' kind_co body_co)
-      | not impredicative = OC_Forall
       | tv == tv'         = return co
       | otherwise         = do { kind_co' <- go_co env kind_co
                                ; let tv'' = setTyVarKind tv' $
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index ca3347861b..b564f9fd9a 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -18,6 +18,7 @@ module TcUnify (
   -- Various unifications
   unifyType, unifyTheta, unifyKind, noThing,
   uType, unifyExpType,
+  swapOverTyVars, canSolveByUnification,
 
   --------------------------------
   -- Holes
@@ -1116,13 +1117,13 @@ uType origin t_or_k orig_ty1 orig_ty2
            ; case lookup_res of
                Filled ty1   -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
                                   ; go ty1 ty2 }
-               Unfilled ds1 -> uUnfilledVar origin t_or_k NotSwapped tv1 ds1 ty2 }
+               Unfilled _ -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
     go ty1 (TyVarTy tv2)
       = do { lookup_res <- lookupTcTyVar tv2
            ; case lookup_res of
                Filled ty2   -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
                                   ; go ty1 ty2 }
-               Unfilled ds2 -> uUnfilledVar origin t_or_k IsSwapped tv2 ds2 ty1 }
+               Unfilled _ -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
 
       -- See Note [Expanding synonyms during unification]
     go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
@@ -1304,87 +1305,77 @@ of the substitution; rather, notice that @uVar@ (defined below) nips
 back into @uTys@ if it turns out that the variable is already bound.
 -}
 
+----------
 uUnfilledVar :: CtOrigin
              -> TypeOrKind
              -> SwapFlag
-             -> TcTyVar -> TcTyVarDetails       -- Tyvar 1
-             -> TcTauType                       -- Type 2
+             -> TcTyVar        -- Tyvar 1
+             -> TcTauType      -- Type 2
              -> TcM Coercion
 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
 --            It might be a skolem, or untouchable, or meta
 
-uUnfilledVar origin t_or_k swapped tv1 details1 (TyVarTy tv2)
-  | tv1 == tv2  -- Same type variable => no-op
-  = return (mkNomReflCo (mkTyVarTy tv1))
-
-  | otherwise  -- Distinct type variables
-  = do  { lookup2 <- lookupTcTyVar tv2
-        ; case lookup2 of
-            Filled ty2'
-              -> uUnfilledVar origin t_or_k swapped tv1 details1 ty2'
-            Unfilled details2
-              -> uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
-        }
-
-uUnfilledVar origin t_or_k swapped tv1 details1 non_var_ty2
--- ty2 is not a type variable
-  = case details1 of
-      MetaTv { mtv_ref = ref1 }
-        -> do { dflags <- getDynFlags
-              ; mb_ty2' <- checkTauTvUpdate dflags origin t_or_k tv1 non_var_ty2
-              ; case mb_ty2' of
-                  Just (ty2', co_k) -> maybe_sym swapped <$>
-                                       updateMeta tv1 ref1 ty2' co_k
-                  Nothing   -> do { traceTc "Occ/type-family defer"
-                                        (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
-                                         $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
-                                  ; defer }
-              }
-
-      _other -> do { traceTc "Skolem defer" (ppr tv1); defer }  -- Skolems of all sorts
+uUnfilledVar origin t_or_k swapped tv1 ty2
+  = do { ty2 <- zonkTcType ty2
+             -- Zonk to expose things to the
+             -- occurs check, and so that if ty2
+             -- looks like a type variable then it
+             -- is a type variable
+       ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
+
+----------
+uUnfilledVar1 :: CtOrigin
+              -> TypeOrKind
+              -> SwapFlag
+              -> TcTyVar        -- Tyvar 1
+              -> TcTauType      -- Type 2, zonked
+              -> TcM Coercion
+uUnfilledVar1 origin t_or_k swapped tv1 ty2
+  | Just tv2 <- tcGetTyVar_maybe ty2
+  = go tv2
+
+  | otherwise
+  = uUnfilledVar2 origin t_or_k swapped tv1 ty2
+
   where
-    defer = unSwap swapped (uType_defer origin t_or_k) (mkTyVarTy tv1) non_var_ty2
-               -- Occurs check or an untouchable: just defer
-               -- NB: occurs check isn't necessarily fatal:
-               --     eg tv1 occured in type family parameter
+    -- 'go' handles the case where both are
+    -- tyvars so we might want to swap
+    go tv2 | tv1 == tv2  -- Same type variable => no-op
+           = return (mkNomReflCo (mkTyVarTy tv1))
 
-----------------
-uUnfilledVars :: CtOrigin
+           | swapOverTyVars tv1 tv2   -- Distinct type variables
+           = uUnfilledVar2 origin t_or_k (flipSwap swapped)
+                           tv2 (mkTyVarTy tv1)
+
+           | otherwise
+           = uUnfilledVar2 origin t_or_k swapped tv1 ty2
+
+----------
+uUnfilledVar2 :: CtOrigin
               -> TypeOrKind
               -> SwapFlag
-              -> TcTyVar -> TcTyVarDetails      -- Tyvar 1
-              -> TcTyVar -> TcTyVarDetails      -- Tyvar 2
+              -> TcTyVar        -- Tyvar 1
+              -> TcTauType      -- Type 2, zonked
               -> TcM Coercion
--- Invarant: The type variables are distinct,
---           Neither is filled in yet
-
-uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
-  = do { traceTc "uUnfilledVars for" (ppr tv1 <+> text "and" <+> ppr tv2)
-       ; traceTc "uUnfilledVars" (    text "trying to unify" <+> ppr k1
-                                  <+> text "with"            <+> ppr k2)
-       ; co_k <- uType kind_origin KindLevel k1 k2
-       ; let no_swap ref = maybe_sym swapped <$>
-                           updateMeta tv1 ref ty2 (mkSymCo co_k)
-             do_swap ref = maybe_sym (flipSwap swapped) <$>
-                           updateMeta tv2 ref ty1 co_k
-       ; case (details1, details2) of
-         { ( MetaTv { mtv_info = i1, mtv_ref = ref1 }
-           , MetaTv { mtv_info = i2, mtv_ref = ref2 } )
-             | nicer_to_update_tv1 tv1 i1 i2 -> no_swap ref1
-             | otherwise                     -> do_swap ref2
-         ; (MetaTv { mtv_ref = ref1 }, _) -> no_swap ref1
-         ; (_, MetaTv { mtv_ref = ref2 }) -> do_swap ref2
-
-           -- Can't do it in-place, so defer
-           -- This happens for skolems of all sorts
-         ; _ -> do { traceTc "deferring because I can't find a meta-tyvar:"
-                       (pprTcTyVarDetails details1 <+> pprTcTyVarDetails details2)
-                   ; unSwap swapped (uType_defer origin t_or_k) ty1 ty2 } } }
+uUnfilledVar2 origin t_or_k swapped tv1 ty2
+  = do { dflags  <- getDynFlags
+       ; cur_lvl <- getTcLevel
+       ; go dflags cur_lvl }
   where
-    k1  = tyVarKind tv1
-    k2  = tyVarKind tv2
+    go dflags cur_lvl
+      | canSolveByUnification cur_lvl tv1 ty2
+      , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
+      = do { co_k <- uType kind_origin KindLevel (typeKind ty2') (tyVarKind tv1)
+           ; co   <- updateMeta tv1 ty2' co_k
+           ; return (maybe_sym swapped co) }
+
+      | otherwise
+      = unSwap swapped (uType_defer origin t_or_k) ty1 ty2
+               -- Occurs check or an untouchable: just defer
+               -- NB: occurs check isn't necessarily fatal:
+               --     eg tv1 occured in type family parameter
+
     ty1 = mkTyVarTy tv1
-    ty2 = mkTyVarTy tv2
     kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
 
 -- | apply sym iff swapped
@@ -1392,27 +1383,16 @@ maybe_sym :: SwapFlag -> Coercion -> Coercion
 maybe_sym IsSwapped  = mkSymCo
 maybe_sym NotSwapped = id
 
-nicer_to_update_tv1 :: TcTyVar -> MetaInfo -> MetaInfo -> Bool
-nicer_to_update_tv1 _   _     SigTv = True
-nicer_to_update_tv1 _   SigTv _     = False
-        -- Try not to update SigTvs; and try to update sys-y type
-        -- variables in preference to ones gotten (say) by
-        -- instantiating a polymorphic function with a user-written
-        -- type sig
-nicer_to_update_tv1 tv1 _     _     = isSystemName (Var.varName tv1)
-
 ----------------
-checkTauTvUpdate :: DynFlags
-                 -> CtOrigin
-                 -> TypeOrKind
-                 -> TcTyVar             -- tv :: k1
-                 -> TcType              -- ty :: k2
-                 -> TcM (Maybe ( TcType        -- possibly-expanded ty
-                               , Coercion )) -- :: k2 ~N k1
---    (checkTauTvUpdate tv ty)
--- We are about to update the TauTv tv with ty.
+metaTyVarUpdateOK :: DynFlags
+                  -> TcTyVar             -- tv :: k1
+                  -> TcType              -- ty :: k2
+                  -> Maybe TcType        -- possibly-expanded ty
+-- (metaTyFVarUpdateOK tv ty)
+-- We are about to update the meta-tyvar tv with ty.
 -- Check (a) that tv doesn't occur in ty (occurs check)
---       (b) that kind(ty) matches kind(tv)
+--       (b) that ty does not have any foralls
+--           (in the impredicative case), or type functions
 --
 -- We have two possible outcomes:
 -- (1) Return the type to update the type variable with,
@@ -1429,48 +1409,106 @@ checkTauTvUpdate :: DynFlags
 -- we return Nothing, leaving it to the later constraint simplifier to
 -- sort matters out.
 
-checkTauTvUpdate dflags origin t_or_k tv ty
-  | SigTv <- info
-  = ASSERT( not (isTyVarTy ty) )
-    return Nothing
-  | otherwise
-  = do { ty   <- zonkTcType ty
-       ; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv)
-       ; if | defer_me ty ->  -- Quick test
-                -- Failed quick test so try harder
-                case occurCheckExpand dflags tv ty of
-                   OC_OK ty2 | defer_me ty2 -> return Nothing
-                             | otherwise    -> return (Just (ty2, co_k))
-                   _                        -> return Nothing
-            | otherwise   -> return (Just (ty, co_k)) }
-
+metaTyVarUpdateOK dflags tv ty
+  = case defer_me impredicative ty of
+      OC_OK _   -> Just ty
+      OC_Forall -> Nothing  -- forall or type function
+      OC_Occurs -> occCheckExpand tv ty
   where
-    kind_origin   = KindEqOrigin (mkTyVarTy tv) (Just ty) origin (Just t_or_k)
     details       = tcTyVarDetails tv
-    info          = mtv_info details
-
     impredicative = canUnifyWithPolyType dflags details
 
-    defer_me :: TcType -> Bool
+    defer_me :: Bool    -- True <=> foralls are ok
+             -> TcType
+             -> OccCheckResult ()
     -- Checks for (a) occurrence of tv
     --            (b) type family applications
-    --            (c) foralls
+    --            (c) foralls if the Bool is false
     -- See Note [Prevent unification with type families]
     -- See Note [Refactoring hazard: checkTauTvUpdate]
-    defer_me (LitTy {})        = False
-    defer_me (TyVarTy tv')     = tv == tv' || defer_me (tyVarKind tv')
-    defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
-                                 || not (impredicative || isTauTyCon tc)
-    defer_me (ForAllTy bndr t) = defer_me (binderKind bndr) || defer_me t
-                                 || not impredicative
-    defer_me (FunTy fun arg)   = defer_me fun || defer_me arg
-    defer_me (AppTy fun arg)   = defer_me fun || defer_me arg
-    defer_me (CastTy ty co)    = defer_me ty || defer_me_co co
-    defer_me (CoercionTy co)   = defer_me_co co
+    -- See Note [Checking for foralls] in TcType
+
+    defer_me _ (TyVarTy tv')
+       | tv == tv' = OC_Occurs
+       | otherwise = defer_me True (tyVarKind tv')
+    defer_me b (TyConApp tc tys)
+       | isTypeFamilyTyCon tc = OC_Forall   -- We use OC_Forall to signal
+                                            -- forall /or/ type function
+       | not (isTauTyCon tc)  = OC_Forall
+       | otherwise            = mapM (defer_me b) tys >> OC_OK ()
+
+    defer_me b (ForAllTy (TvBndr tv' _) t)
+       | not b     = OC_Forall
+       | tv == tv' = OC_OK ()
+       | otherwise = do { defer_me True (tyVarKind tv'); defer_me b t }
+
+    defer_me _ (LitTy {})        = OC_OK ()
+    defer_me b (FunTy fun arg)   = defer_me b fun >> defer_me b arg
+    defer_me b (AppTy fun arg)   = defer_me b fun >> defer_me b arg
+    defer_me b (CastTy ty co)    = defer_me b ty  >> defer_me_co co
+    defer_me _ (CoercionTy co)   = defer_me_co co
 
       -- We don't really care if there are type families in a coercion,
       -- but we still can't have an occurs-check failure
-    defer_me_co co = tv `elemVarSet` tyCoVarsOfCo co
+    defer_me_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
+                   | otherwise                       = OC_OK ()
+
+swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
+-- See Note [Canonical orientation for tyvar/tyvar equality constraints]
+swapOverTyVars tv1 tv2
+  | Just lvl1 <- metaTyVarTcLevel_maybe tv1
+      -- If tv1 is touchable, swap only if tv2 is also
+      -- touchable and it's strictly better to update the latter
+      -- But see Note [Avoid unnecessary swaps]
+  = case metaTyVarTcLevel_maybe tv2 of
+      Nothing   -> False
+      Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
+                | lvl1 `strictlyDeeperThan` lvl2 -> False
+                | otherwise                      -> nicer_to_update tv2
+
+  -- So tv1 is not a meta tyvar
+  -- If only one is a meta tyvar, put it on the left
+  -- This is not because it'll be solved; but because
+  -- the floating step looks for meta tyvars on the left
+  | isMetaTyVar tv2 = True
+
+  -- So neither is a meta tyvar (including FlatMetaTv)
+
+  -- If only one is a flatten skolem, put it on the left
+  -- See Note [Eliminate flat-skols]
+  | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
+
+  | otherwise = False
+
+  where
+    nicer_to_update tv2
+      =  (isSigTyVar tv1                 && not (isSigTyVar tv2))
+      || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
+
+-- @trySpontaneousSolve wi@ solves equalities where one side is a
+-- touchable unification variable.
+-- Returns True <=> spontaneous solve happened
+canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
+canSolveByUnification tclvl tv xi
+  | isTouchableMetaTyVar tclvl tv
+  = case metaTyVarInfo tv of
+      SigTv -> is_tyvar xi
+      _     -> True
+
+  | otherwise    -- Untouchable
+  = False
+  where
+    is_tyvar xi
+      = case tcGetTyVar_maybe xi of
+          Nothing -> False
+          Just tv -> case tcTyVarDetails tv of
+                       MetaTv { mtv_info = info }
+                                   -> case info of
+                                        SigTv -> True
+                                        _     -> False
+                       SkolemTv {} -> True
+                       FlatSkol {} -> False
+                       RuntimeUnk  -> True
 
 {-
 Note [Prevent unification with type families]
@@ -1508,14 +1546,15 @@ with type families].) So I checked the result of occurCheckExpand for any
 type family occurrences and deferred if there were any. This was done
 in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 .
 
-This approach turned out not to be performant, because the expanded type
-was bigger than the original type, and tyConsOfType looks through type
-synonyms. So it then struck me that we could dispense with the defer_me
-check entirely. This simplified the code nicely, and it cut the allocations
-in T5030 by half. But, as documented in Note [Prevent unification with
-type families], this destroyed performance in T3064. Regardless, I missed this
-regression and the change was committed as
-3f5d1a13f112f34d992f6b74656d64d95a3f506d .
+This approach turned out not to be performant, because the expanded
+type was bigger than the original type, and tyConsOfType (needed to
+see if there are any type family occurrences) looks through type
+synonyms. So it then struck me that we could dispense with the
+defer_me check entirely. This simplified the code nicely, and it cut
+the allocations in T5030 by half. But, as documented in Note [Prevent
+unification with type families], this destroyed performance in
+T3064. Regardless, I missed this regression and the change was
+committed as 3f5d1a13f112f34d992f6b74656d64d95a3f506d .
 
 Bottom lines:
  * defer_me is back, but now fixed w.r.t. #11407.
@@ -1598,15 +1637,14 @@ lookupTcTyVar tyvar
 
 -- | Fill in a meta-tyvar
 updateMeta :: TcTyVar            -- ^ tv to fill in, tv :: k1
-           -> TcRef MetaDetails  -- ^ ref to tv's metadetails
            -> TcType             -- ^ ty2 :: k2
            -> Coercion           -- ^ kind_co :: k2 ~N k1
            -> TcM Coercion       -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2)
-updateMeta tv1 ref1 ty2 kind_co
-  = do { let ty2_refl   = mkNomReflCo ty2
-             (ty2', co) = ( ty2 `mkCastTy` kind_co
-                          , mkCoherenceLeftCo ty2_refl kind_co )
-       ; writeMetaTyVarRef tv1 ref1 ty2'
+updateMeta tv1 ty2 kind_co
+  = do { let ty2'     = ty2 `mkCastTy` kind_co
+             ty2_refl = mkNomReflCo ty2
+             co       = mkCoherenceLeftCo ty2_refl kind_co
+       ; writeMetaTyVar tv1 ty2'
        ; return co }
 
 {-
diff --git a/testsuite/tests/polykinds/T12593.hs b/testsuite/tests/polykinds/T12593.hs
new file mode 100644
index 0000000000..867fb89284
--- /dev/null
+++ b/testsuite/tests/polykinds/T12593.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTs, ConstraintKinds, PolyKinds, TypeInType,  KindSignatures, RankNTypes #-}
+
+module T12593 where
+
+import Data.Kind
+
+newtype Free k p a b where
+   Free :: (forall q. k q => (forall c d. p c d -> q c d) -> q a b)
+        -> Free k p a b
+
+run :: k2 q => Free k k1 k2 p a b
+             -> (forall (c :: k) (d :: k1). p c d -> q c d)
+             -> q a b
+run (Free cat) = cat
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
new file mode 100644
index 0000000000..4b551558a1
--- /dev/null
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -0,0 +1,31 @@
+
+T12593.hs:11:16: error:
+    • Expecting two fewer arguments to ‘Free k k4 k5 p’
+      Expected kind ‘k0 -> k1 -> *’, but ‘Free k k4 k5 p’ has kind ‘*’
+    • In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:31: error:
+    • Expecting one more argument to ‘k’
+      Expected a type, but
+      ‘k’ has kind
+      ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+       -> Constraint’
+    • In the kind ‘k’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:40: error:
+    • Expecting two more arguments to ‘k4’
+      Expected a type, but
+      ‘k4’ has kind
+      ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’
+    • In the kind ‘k1’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 1c27dfd82e..6da6ae4439 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -151,3 +151,4 @@ test('T11640', normal, compile, [''])
 test('T11554', normal, compile_fail, [''])
 test('T12055', normal, compile, [''])
 test('T12055a', normal, compile_fail, [''])
+test('T12593', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr
index cf206a11ae..d205fa9ced 100644
--- a/testsuite/tests/typecheck/should_compile/tc141.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc141.stderr
@@ -35,11 +35,11 @@ tc141.hs:13:13: error:
         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
+    • Couldn't match expected type ‘a2’ with actual type ‘t’
+        because type variable ‘a2’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
-          v :: a1
+          v :: a2
         at tc141.hs:14:14-19
     • In the expression: b
       In an equation for ‘v’: v = b
@@ -49,6 +49,6 @@ tc141.hs:15:18: error:
           v = b
         in v
     • Relevant bindings include
-        v :: a1 (bound at tc141.hs:15:14)
+        v :: a2 (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)
+        g :: a1 -> t -> forall a. a (bound at tc141.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9605.stderr b/testsuite/tests/typecheck/should_fail/T9605.stderr
index 38da1c46a3..db65629fba 100644
--- a/testsuite/tests/typecheck/should_fail/T9605.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9605.stderr
@@ -1,11 +1,11 @@
 
 T9605.hs:7:6: error:
     • Couldn't match type ‘Bool’ with ‘m Bool’
-      Expected type: t1 -> m Bool
-        Actual type: t1 -> Bool
+      Expected type: t0 -> m Bool
+        Actual type: t0 -> Bool
     • The function ‘f1’ is applied to one argument,
       its type is ‘m0 Bool’,
-      it is specialized to ‘t1 -> Bool’
+      it is specialized to ‘t0 -> Bool’
       In the expression: f1 undefined
       In an equation for ‘f2’: f2 = f1 undefined
     • Relevant bindings include f2 :: m Bool (bound at T9605.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
index ab743441f9..a6fbc86c49 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
@@ -1,6 +1,6 @@
 
 tcfail122.hs:8:9: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
+    • Couldn't match kind ‘*’ with ‘* -> *’
       When matching the kind of ‘a’
     • In the expression:
           undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d