GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

97adaf89

by Simon Peyton Jones at 2026-10-14T00:07:27+01:00

Line up simpleUnifyCheck and check_ty_eq_rhs

Even after #26543 was allegedly fixed, the original repo case in the
Description continued to fail.  The reason was that the QuickLook
unifier, `qlUnify`, used `simpleUnifyCheck` for checking unification
invariants; and `simpleUnifyCheck` conservatively rejected any RHS
with a coercion hole in it.  The upshot was that QuickLook was not
as clever as it should be, wrongly failing to do an impredicative
instantiation.

Interestingly `check_ty_eq_rhs`, which does the same job during
constraint solving, was more liberal: it just looked at the free vars
of the coercion, and allowed coercion holes.

This MR lines them up, adding some careful notes.  See
    Note [simpleUnifyCheck]
    Note [Occurs check and coercions]
    Note [Unification preconditions] esp (COERCIONS)

Things are better than before, but I am still uncomfortable about the
possibilty that a hole might be filled with a coercion that mentions
the LHS type variable; for now I have left this discomfort documented
in Note [Occurs check and coercions].

Main changes

* `qlUnify` now only unifies /instantiation variables/ not regular unification
  variables.  This makes QuickLook more predictable.  See (UQL6) in
  Note [QuickLook unification].

* `qlUnify` no longer needs to call `simpleUnifyCheck`, so we can get rid of
  `UC_QuickLook` and its code in `simpleUnifyCheck`.

* I found I could get rid of `mkOccFolders` in favour of `anyFreeVarsOfType`.
  Hooray.

* Improve documentation of CycleBreakerTv, and rename it to GivenCycleBreakerTv
  because they are only uesd for Givens!

* I accepted a 9% worsening in compile time allocation on T5030
  because the newly-consistent story triggered #27934.

Other changes

* I refactored `atvFolder` so that it pairs the "interesting-var" function
  with the in-scope set, to avoid building a closure with a free variable.
  Now we get nice tight loops for `anyFreeVarsOfType` and friends.
  See Note [Any-free-var folder].

Metric Increase:
    T5030

5f7b3047

by Simon Peyton Jones at 2026-10-14T00:07:27+01:00

Fix order-dependence in QuickLook

Ticket #27917 pointed out that QuickLook was order-dependent
-- very bad!

The solution is in `qlUnify`: spot when we are unifying a type with a
definite monotype, and then monomorphise any free instantiation
variables of that type.

See (UQL8) and (UQL9) in Note [QuickLook unification].

c391c70c

by Simon Peyton Jones at 2026-10-14T00:07:28+01:00

Add some comments about RuntimeUnk

This commit just adds comments explaining why we don't need to worry about
RuntimeUnkTv in the constraint solver.

It also tightens up docmentation of earlier (overlapping) commits in
this MR.

24 changed files:

+ changelog.d/T26543
compiler/GHC/Core/FVs.hs
compiler/GHC/Core/TyCo/FVs.hs
compiler/GHC/Runtime/Heap/Inspect.hs
compiler/GHC/Tc/Gen/App.hs
compiler/GHC/Tc/Solver/Equality.hs
compiler/GHC/Tc/Solver/InertSet.hs
compiler/GHC/Tc/Solver/Monad.hs
compiler/GHC/Tc/Utils/TcMType.hs
compiler/GHC/Tc/Utils/TcType.hs
compiler/GHC/Tc/Utils/Unify.hs
compiler/GHC/Types/Var/FV.hs
testsuite/tests/default/default-fail05.stderr
testsuite/tests/ghci.debugger/scripts/T14628.stderr
+ testsuite/tests/impredicative/T27917.hs
testsuite/tests/impredicative/all.T
testsuite/tests/indexed-types/should_fail/T1897b.stderr
testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs
+ testsuite/tests/typecheck/should_compile/T26543_orig.hs
testsuite/tests/typecheck/should_compile/all.T
testsuite/tests/typecheck/should_fail/T22707.stderr
+ testsuite/tests/typecheck/should_fail/T26543a.hs
+ testsuite/tests/typecheck/should_fail/T26543a.stderr
testsuite/tests/typecheck/should_fail/all.T

Changes:

changelog.d/T26543

 +section: compiler
 +synopsis: Fix a bug in ImpredicativeTypes
 +description:
 +  The QuickLook algorithm (which implements `ImpredicativeTypes`) was defeated if there
 +  was a kind coercion in the types being unified.  That bug is now fixed.
 +mrs: !16566
 +issues: #26543

compiler/GHC/Core/FVs.hs

@@ -223,11 +223,11 @@ addCoreBndrsFV bndrs fv = foldr addCoreBndrFV fv bndrs
  unitFV :: Var -> SelectiveDFV
  -- Deals with an occurrence
  -- Shallow: does not look at the kind
 -unitFV v = MkFV (\bvs -> EndoOS (do_it bvs))
 +unitFV v = MkFV (\env -> EndoOS (do_it env))
    where
 -    do_it (is_interesting,bvs) acc
 +    do_it (bvs, is_interesting) acc
 +      | v `elemVarSet` bvs     = acc  -- First exclude the bound vars
        | not (is_interesting v) = acc  -- The "selective" bit
 -      | v `elemVarSet` bvs     = acc
        | v `elemDVarSet` acc    = acc
        | otherwise              = acc `extendDVarSet` v

compiler/GHC/Core/TyCo/FVs.hs

@@ -278,14 +278,15 @@ deepUnitFV :: (Type -> TyCoFV) -> TyCoVar -> TyCoFV
  -- Deal with a single TyCoVar
  -- Takes a function to find free vars of the kind
  -- See Note [Computing deep free variables]
 -deepUnitFV fvs_of_kind v
 -  = MkFV (\bvs -> EndoOS (do_it bvs))
 +{-# INLINE deepUnitFV #-}   -- INLINE to specialise on fvs_of_kind
 +deepUnitFV fvs_of_kind
 +  = \v -> MkFV (\bvs -> EndoOS (do_it bvs v))
    where
 -    do_it :: BoundVars -> TyCoVarSet -> TyCoVarSet
 -    do_it bvs acc | v `elemVarSet` bvs = acc
 -                  | v `elemVarSet` acc = acc
 -                  | otherwise          = runFVAcc (fvs_of_kind (varType v)) acc
 -                                         `extendVarSet` v
 +    do_it :: BoundVars -> TyCoVar -> TyCoVarSet -> TyCoVarSet
 +    do_it bvs v acc | v `elemVarSet` bvs = acc
 +                    | v `elemVarSet` acc = acc
 +                    | otherwise          = runFVAcc (fvs_of_kind (varType v)) acc
 +                                           `extendVarSet` v
                    -- Left-to-right: add the kind variables to the
                    --                accumulator before v itself
@@ -443,11 +444,11 @@ selectiveTcvFolder
                 , tcf_hole  = do_hole, tcf_lit = const mempty
                 , tcf_tycobinder = addBndrSelectiveFV }
    where
 -    do_tcv v = MkFV (\bvs -> EndoOS (do_it bvs))
 +    do_tcv v = MkFV (\env -> EndoOS (do_it env))
        where
 -        do_it (is_interesting,bvs) acc
 +        do_it (bvs,is_interesting) acc
 +          | v `elemVarSet` bvs     = acc  -- First exclude bound variables
            | not (is_interesting v) = acc  -- The "selective" bit
 -          | v `elemVarSet` bvs     = acc
            | v `elemDVarSet` acc    = acc
            | otherwise              = acc `extendDVarSet` v
@@ -848,43 +849,77 @@ invisibleVarsOfTypes = foldr (unionVarSet . invisibleVarsOfType) emptyVarSet
  *                                                                      *
  ********************************************************************* -}
 -{-# INLINE afvFolder #-}   -- so that specialization to (const True) works
 -afvFolder :: (TyCoVar -> Bool) -> TyCoFolder (FV TyCoVarSet DM.Any)
 +{- Note [Any-free-var folder]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +The "any-free-var" folders take a `check_fv` predicate (TyCoVar -> Bool) and
 +check if any /deep/ free variable of the type/coercion satisfies it. So
++
 +   anyFreeVarsOfType p ty = anyVarSet p (tyCoVarsOfType ty)
++
 +Our main folders look like:
++
 +   afv_type :: Type -> FV (BoundVars, TyVar -> Bool) Any
++
 +where we cleverly pair the predicate with the forall-bound variables of the type
 +in the "env" field of (FV env Any).  This way we can build the /folder/ once and
 +for all (independent of the `check_fv` predicate), and the loop passes down
 +the pair.
++
 +The same idiom is used in `exprFreeVarsDSet` and friends.
++
 +However we are careful to INLINE `atvFolder` and `runAny` so that we get those
 +nice tight loops.
 +-}
++
 +{-# INLINE afvFolder #-}   -- See Note [Any-free-var folder]
 +afvFolder :: TyCoFolder (FV (BoundVars, TyCoVar -> Bool) DM.Any)
  -- 'afvFolder' is short for "any-free-var folder", good for checking
 --- if any free var of a type satisfies a predicate `check_fv`
 -afvFolder check_fv = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]
 -                                , tcf_tyvar = do_tcv, tcf_covar = do_tcv
 -                                , tcf_hole = do_hole, tcf_lit = const mempty
 -                                , tcf_tycobinder = addBndrFV }
 +--   if any /deep/ free var of a type satisfies a predicate `check_fv`
 +-- The "env" of the (FV env Any) is a pair (bvs,pred) of
 +--    the bound variables (which are definitely not free), and
 +--    an "interesting var" predicate which the client supplies
 +afvFolder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]
 +                       , tcf_tyvar = do_tcv
 +                       , tcf_covar = do_tcv
 +                       , tcf_hole  = do_hole
 +                       , tcf_lit   = const mempty
 +                       , tcf_tycobinder = addBndrSelectiveFV }
    where
 -    do_tcv tv = MkFV $ \ bvs ->
 -                Any (not (tv `elemVarSet` bvs) && check_fv tv)
 -    do_hole _ = mempty    -- I'm unsure; probably never happens
 +    -- Check the variable itself with check_fv,
 +    -- and check its kind (this is a deep folder)
 +    do_tcv tcv = MkFV $ \ (bvs,check_fv) ->
 +                 Any (not (tcv `elemVarSet` bvs) &&
 +                      (check_fv tcv || runAny check_fv (afv_type (varType tcv))))
 +    do_hole hole = do_tcv (coHoleCoVar hole)
++
 +afv_type  :: Type     -> FV (BoundVars, TyVar -> Bool) DM.Any
 +afv_types :: [Type]   -> FV (BoundVars, TyVar -> Bool) DM.Any
 +afv_co    :: Coercion -> FV (BoundVars, TyVar -> Bool) DM.Any
 +(afv_type, afv_types, afv_co, _) = foldTyCo afvFolder
++
 +runAny :: (TyVar -> Bool) -> FV (BoundVars, TyCoVar -> Bool) DM.Any -> Bool
 +{-# INLINE runAny #-}
 +runAny check_fv fvs = DM.getAny (runFV fvs (emptyVarSet, check_fv))
  anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
 -anyFreeVarsOfType check_fv ty = DM.getAny (runFVTop (f ty))
 -  where (f, _, _, _) = foldTyCo (afvFolder check_fv)
 +{-# INLINE anyFreeVarsOfType #-}
 +anyFreeVarsOfType check_fv ty = runAny check_fv (afv_type ty)
  anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
 -anyFreeVarsOfTypes check_fv tys = DM.getAny (runFVTop (f tys))
 -  where (_, f, _, _) = foldTyCo (afvFolder check_fv)
 +{-# INLINE anyFreeVarsOfTypes #-}
 +anyFreeVarsOfTypes check_fv tys = runAny check_fv (afv_types tys)
  anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
 -anyFreeVarsOfCo check_fv co = DM.getAny (runFVTop (f co))
 -  where (_, _, f, _) = foldTyCo (afvFolder check_fv)
 +anyFreeVarsOfCo check_fv co = runAny check_fv (afv_co co)
  noFreeVarsOfType :: Type -> Bool
 -noFreeVarsOfType ty = not $ DM.getAny (runFVTop (f ty))
 -  where (f, _, _, _) = foldTyCo (afvFolder (const True))
 +noFreeVarsOfType ty = not $ runAny (const True) (afv_type ty)
  noFreeVarsOfTypes :: [Type] -> Bool
 -noFreeVarsOfTypes tys = not $ DM.getAny (runFVTop (f tys))
 -  where (_, f, _, _) = foldTyCo (afvFolder (const True))
 +noFreeVarsOfTypes tys = not $ runAny (const True) (afv_types tys)
  noFreeVarsOfCo :: Coercion -> Bool
 -noFreeVarsOfCo co = not $ DM.getAny (runFVTop (f co))
 -  where (_, _, f, _) = foldTyCo (afvFolder (const True))
+-
 +noFreeVarsOfCo co = not $ runAny (const True) (afv_co co)
  {-
  ************************************************************************

compiler/GHC/Runtime/Heap/Inspect.hs

@@ -628,18 +628,16 @@ be sigmas and not taus.
  {- Note [RuntimeUnkTv]
  ~~~~~~~~~~~~~~~~~~~~~~
 -In the GHCi debugger we use unification variables whose MetaInfo is
 -RuntimeUnkTv.  The special property of a RuntimeUnkTv is that it can
 -unify with a polytype (see GHC.Tc.Solver.Equality.checkTypeEqNoUnification).
 -If we don't do this `:print <term>` will fail if the type of <term>
 -has nested `forall`s or `=>`s.
+-
 -This is because the GHCi debugger's internals will attempt to unify a
 -metavariable with the type of <term> and then display the result, but
 -if the type has nested `forall`s or `=>`s, then unification will fail
 -unless we do something special.  As a result, `:print` will bail out
 -and the unhelpful result will be `<term> = (_t1::t1)` (where `t1` is a
 -metavariable).
 +In the GHCi debugger we use unification variables whose MetaInfo is RuntimeUnkTv.
 +The special property of a RuntimeUnkTv is that it can unify with a polytype (see
 +GHC.Tc.Utils.Unify.simpleUnifyCheck).  If we don't do this `:print <term>` will fail if
 +the type of <term> has nested `forall`s or `=>`s.
++
 +This is because the GHCi debugger's internals will attempt to unify a metavariable
 +with the type of <term> and then display the result, but if the type has nested
 +`forall`s or `=>`s, then unification will fail unless we do something special.  As
 +a result, `:print` will bail out and the unhelpful result will be `<term> =
 +(_t1::t1)` (where `t1` is a metavariable).
  Beware: <term> can have nested `forall`s even if its definition doesn't use
  RankNTypes! Here is an example from #14828:
@@ -654,13 +652,18 @@ We could envision deeply instantiating this type to get the type
  `forall f a b. Functor f => (a -> b) -> f a -> f b`,
  but this trick wouldn't work for higher-rank types.
 -Instead, we adopt a simpler fix: allow RuntimeUnkTv to unify with a
 -polytype (specifically, see ghci_tv in GHC.Tc.Utils.Unify.preCheck).
 -This allows metavariables to unify with types that have
 -nested (or higher-rank) `forall`s/`=>`s, which makes `:print fmap`
 -display as
 -`fmap = (_t1::forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b)`,
 +Instead, we adopt a simpler fix: allow RuntimeUnkTv to unify with a polytype
 +(specifically, see ghci_tv in GHC.Tc.Utils.Unify.preCheck).  This allows
 +metavariables to unify with types that have nested (or higher-rank)
 +`forall`s/`=>`s, which makes `:print fmap` display as
 +  `fmap = (_t1::forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b)`,
  as expected.
++
 +(RUT1) The debugger uses the "on-the-fly" unifier, namely
 +          GHC.Tc.Utils.Unify.unifyType
 +   and /ignores/ any constraints it generates: see `addConstraint`. It never
 +   calls the constraint solver, so the constraint solver does not need to
 +   understand about RuntimeUnkTvs.
  -}

compiler/GHC/Tc/Gen/App.hs

@@ -37,6 +37,7 @@ import GHC.Core.ConLike ( ConLike(..) )
  import GHC.Core.DataCon ( dataConConcreteTyVars, isNewDataCon, dataConOrigArgTys )
  import GHC.Core.TyCon
  import GHC.Core.TyCo.Rep
 +import GHC.Core.TyCo.FVs
  import GHC.Core.TyCo.Ppr
  import GHC.Core.TyCo.Subst ( substTyWithInScope )
  import GHC.Core.Type
@@ -631,11 +632,13 @@ tcInstFun :: QLFlag
  -- plus the modification in Fig 5, of the QL paper:
  -- "A quick look at impredicativity" (ICFP'20).
  tcInstFun do_ql inst_final rn_head@(_, fun_lspan) tc_fun fun_sigma rn_args
 -  = do { traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun
 +  = do { lvl <- getTcLevel
 +       ; traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun
                                     , text "rn_fun" <+> ppr rn_head
                                     , text "fun_sigma" <+> ppr fun_sigma
                                     , text "args:" <+> ppr rn_args
 -                                   , text "do_ql" <+> ppr do_ql])
 +                                   , text "do_ql" <+> ppr do_ql
 +                                   , text "lvl:" <+> ppr lvl ])
         ; fun_origin <- mk_origin rn_head
         ; res@(_, fun_ty) <- go fun_origin 1 [] fun_sigma rn_args
         ; traceTc "tcInstFun:ret" (ppr fun_ty)
@@ -1377,13 +1380,15 @@ tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty
                 -- is not fully zonked, because ty_arg is fully zonked.
                 -- See Note [Type application substitution].
 +       ; lvl <- getTcLevel
         ; traceTc "tc_inst_forall_arg (VTA/VDQ)" (
                    vcat [ text "fun_ty" <+> ppr fun_ty
                         , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind
                         , text "ty_arg" <+> debugPprType ty_arg <+> dcolon
                                         <+> debugPprType (typeKind ty_arg)
                         , text "inner_ty" <+> debugPprType inner_ty
 -                       , text "insted_ty" <+> debugPprType insted_ty ])
 +                       , text "insted_ty" <+> debugPprType insted_ty
 +                       , text "lvl:" <+> ppr lvl ])
         ; return (ty_arg, insted_ty) }
  {- Note [Visible type application and abstraction]
@@ -1934,11 +1939,13 @@ quickLookArg1 pos app_lspan rn_head larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_
           -- capture and save it in the `EValArgQL`.  See (QLA6) in
           -- Note [Quick Look at value arguments]
 +       ; lvl <- getTcLevel
         ; traceTc "quickLookArg {" $
           vcat [ text "arg:" <+> ppr arg
                , text "orig_arg_rho:" <+> ppr orig_arg_rho
                , text "head:" <+> ppr rn_fun_arg <+> dcolon <+> ppr mb_fun_ty
 -              , text "args:" <+> ppr rn_args ]
 +              , text "args:" <+> ppr rn_args
 +              , text "level:" <+> ppr lvl ]
         ; case mb_fun_ty of {
             Nothing -> skipQuickLook app_lspan larg sc_arg_ty ;    -- fun is too complicated
@@ -2048,6 +2055,8 @@ qlMonoHsWrapper (WpTyApp ty)      = qlMonoTcType ty
  qlMonoHsWrapper _                 = return ()
  qlMonoTcType :: TcType -> ZonkM ()
 +-- Monomorphise any free instantiation variables of `ty`
 +-- This functions zonks as it goes
  -- See Note [Monomorphise instantiation variables]
  qlMonoTcType ty
    = do { traceZonk "monomorphiseQLInstVars {" (ppr ty)
@@ -2152,8 +2161,7 @@ foldQLInstVars check_tv ty
  qlUnify ::  TcType -> TcType -> TcM ()
  -- Unify ty1 with ty2:
 ---   * It can unify both instantiation variables (possibly with polytypes),
 ---     and ordinary unification variables (but only with monotypes)
 +--   * It unifies /only/ instantiation variables (see (UQL6)), hopefully with polytypes
  --   * It does not return a coercion (unlike unifyType); it is called
  --     for the sole purpose of unifying instantiation variables, although it
  --     may also (opportunistically) unify regular unification variables.
@@ -2161,18 +2169,23 @@ qlUnify ::  TcType -> TcType -> TcM ()
  --   * It may return without having made the argument types equal, of course;
  --     it just makes best efforts.
  qlUnify ty1 ty2
 -  = do { traceTc "qlUnify" (ppr ty1 $$ ppr ty2)
 +  = do { lvl <- getTcLevel
 +       ; traceTc "qlUnify" (ppr lvl $$ ppr ty1 $$ ppr ty2)
         ; go ty1 ty2 }
    where
      go :: TcType -> TcType -> TcM ()
 +    go t1 t2 = do { traceTc "qlUinfy:go" (ppr t1 <+> char '~' <+> ppr t2)
 +                  ; go' t1 t2 }
++
      -- Decompose (arg1 -> res1) ~ (arg2 -> res2)
      -- and         (c1 => res1) ~   (c2 => res2)
      -- But for the latter we only learn instantiation info from res1~res2
 -    go (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1 })
 +    go' (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1 })
         (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2 })
        | af1 == af2 -- Match the arrow TyCon
 -      = do { when (isVisibleFunArg af1) (go arg1 arg2)
 +      = do { traceTc "go_fun" (ppr arg1 $$ ppr arg2)
 +           ; when (isVisibleFunArg af1) (go arg1 arg2)
          -- NB: we do not unify the multiplicities; that would be too strong.
          -- We might only require mult1 ⩽ mult2, as in Note [Multiplicity in deep subsumption].
@@ -2181,30 +2194,29 @@ qlUnify ty1 ty2
             ; go res1 res2 }
      -- Make sure to not unify "kappa := (a %1 -> b)". See (UQL5).
 -    go (FunTy { ft_mult = OneTy }) _ = return ()
 -    go _ (FunTy { ft_mult = OneTy }) = return ()
 -      -- NB: we do want to be able to unify "kappa := a => b", as that's
 -      -- the main point of QuickLook (allowing meta-variables to be unified
 -      -- with qualified types).
 +    -- NB: we /do/ want to be able to unify "kappa := a => b", as that's
 +    -- the main point of QuickLook (allowing meta-variables to be unified
 +    -- with qualified types).
 +    go' (FunTy { ft_mult = OneTy }) _ = return ()
 +    go' _ (FunTy { ft_mult = OneTy }) = return ()
 -    go (TyVarTy tv) ty2
 -      | isMetaTyVar tv = go_kappa tv ty2
 -    go ty1 (TyVarTy tv)
 -      | isMetaTyVar tv = go_kappa tv ty1
 +    -- Type variables; see (UQL6) in Note [QuickLook unification]
 +    go' (TyVarTy tv) ty2 | isMetaTyVar tv = go_meta tv ty2
 +    go' ty1 (TyVarTy tv) | isMetaTyVar tv = go_meta tv ty1
 -    go (CastTy ty1 _) ty2 = go ty1 ty2
 -    go ty1 (CastTy ty2 _) = go ty1 ty2
 +    go' (CastTy ty1 _) ty2 = go ty1 ty2
 +    go' ty1 (CastTy ty2 _) = go ty1 ty2
 -    go (TyConApp tc1 []) (TyConApp tc2 [])
 +    go' (TyConApp tc1 []) (TyConApp tc2 [])
        | tc1 == tc2 -- See GHC.Tc.Utils.Unify
        = return ()  -- Note [Expanding synonyms during unification]
      -- Now, and only now, expand synonyms
 -    go rho1 rho2
 +    go' rho1 rho2
        | Just rho1 <- coreView rho1 = go rho1 rho2
        | Just rho2 <- coreView rho2 = go rho1 rho2
 -    go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 +    go' (TyConApp tc1 tys1) (TyConApp tc2 tys2)
        | tc1 == tc2
        , not (isTypeFamilyTyCon tc1)
        , tys1 `equalLength` tys2
@@ -2212,67 +2224,79 @@ qlUnify ty1 ty2
      -- Don't allow unifying (a => b) with the AppTy 'arr[tau] a b'.
      -- To ensure this, use 'tcSplitAppTyNoView_maybe' which does not split (=>).
 -    go (AppTy t1a t1b) ty2
 +    go' (AppTy t1a t1b) ty2
        | Just (t2a, t2b) <- tcSplitAppTyNoView_maybe ty2
        = do { go t1a t2a; go t1b t2b }
 -    go ty1 (AppTy t2a t2b)
 +    go' ty1 (AppTy t2a t2b)
        | Just (t1a, t1b) <- tcSplitAppTyNoView_maybe ty1
        = do { go t1a t2a; go t1b t2b }
 -    go _ _ = return ()
 +    -- Type families have a monomorphic result, so if we see (say)
 +    --     Maybe kappa ~ F ty
 +    -- we know that kappa must be a monotype
 +    go' (TyConApp tc1 _) ty2 | isTypeFamilyTyCon tc1 = monomorphise ty2
 +    go' ty1 (TyConApp tc2 _) | isTypeFamilyTyCon tc2 = monomorphise ty1
++
 +    go' _ _ = return ()
         -- Don't look under foralls; see (UQL4) of Note [QuickLook unification]
      ----------------
 -    go_kappa kappa ty2
 -      = assertPpr (isMetaTyVar kappa) (ppr kappa) $
 -        do { info <- readMetaTyVar kappa
 -           ; case info of
 +    go_meta tv1 ty2
 +      = assertPpr (isMetaTyVar tv1) (ppr tv1) $
 +        do { info <- readMetaTyVar tv1
 +           ; case info of  -- See (UQL9)
                 Indirect ty1 -> go ty1 ty2
                 Flexi        -> do { ty2 <- liftZonkM $ zonkTcType ty2
 -                                  ; go_flexi kappa ty2 } }
 +                                  ; go_flexi tv1 ty2 } }
      ----------------
 -    -- Swap (kappa1[conc] ~ kappa2[tau])
 -    -- otherwise we'll fail to unify and emit a coercion.
 -    -- Just an optimisation: emitting a coercion is fine
 -    go_flexi kappa (TyVarTy tv2)
 -      | lhsPriority tv2 > lhsPriority kappa
 -      = go_flexi1 tv2 (TyVarTy kappa)
 -    go_flexi kappa ty2
 -      = go_flexi1 kappa ty2
+-
 -    go_flexi1 kappa ty2  -- ty2 is zonked
 -      = do { cur_lvl <- getTcLevel
 -              -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
 -              -- Here we are in the TcM monad, which does not track enclosing
 -              -- Given equalities; so for quick-look unification we conservatively
 -              -- treat /any/ level outside this one as untouchable. Hence cur_lvl.
 -           ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of
 -              SUC_CanUnify ->
 -                do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
 -                           -- unifyKind: see (UQL2) in Note [QuickLook unification]
 -                           --            and (MIV2) in Note [Monomorphise instantiation variables]
 -                   ; let ty2' = mkCastTy ty2 co
 -                   ; traceTc "qlUnify:update" $
 -                     ppr kappa <+> text ":=" <+> ppr ty2
 -                   ; liftZonkM $ writeMetaTyVar kappa ty2' }
 -              _ -> return () -- e.g. occurs-check or forall-bound variable
 -           }
 +    -- Both tv1 and ty2 are zonked; tv1 is a unfilled meta-tyvar
 +    -- Zonking ty2 makes the occurs-check easier
 +    go_flexi tv1 ty2
 +      | TyVarTy tv2 <- ty2
 +      , lhsPriority tv2 > lhsPriority tv1
 +      = go_flexi1 tv2 (TyVarTy tv1)
 +      | otherwise
 +      = go_flexi1 tv1 ty2
++
 +    -- Both tv1 and ty2 are zonked; tv1 is a unfilled meta-tyvar
 +    go_flexi1 tv1 ty2
 +      | isQLInstTyVar tv1 = go_kappa tv1 ty2
 +      | otherwise         = monomorphise ty2
++
 +    go_kappa kappa ty2
 +      | isConcreteTyVar kappa  -- See (UQL7) in Note [QuickLook unification]
 +      = return ()
 +      | anyFreeVarsOfType (== kappa) ty2
 +      = return ()  -- Occurs check.  See (UQL10) in Note [QuickLook unification]
 +      | otherwise
 +      = do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
 +                   -- unifyKind: see (UQL2) in Note [QuickLook unification]
 +                   --            and (MIV2) in Note [Monomorphise instantiation variables]
 +           ; let ty2' = mkCastTy ty2 co
 +           ; traceTc "qlUnify:update" $
 +             ppr kappa <+> text ":=" <+> ppr ty2
 +           ; liftZonkM $ writeMetaTyVar kappa ty2'
 +           ; return () }
        where
          kappa_kind = tyVarKind kappa
          ty2_kind   = typeKind ty2
 +    monomorphise :: TcType -> TcM ()
 +    monomorphise ty  -- See (UQL8)
 +      = do { _ <- liftZonkM $ qlMonoTcType ty; return () }
++
  {- Note [QuickLook unification]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
  That is the entire point of qlUnify!   Wrinkles:
 -(UQL1) Before unifying an instantiation variable in `go_flexi`, we must check
 -  the usual unification conditions, by calling `GHC.Tc.Utils.Unify.simpleUnifyCheck`.
 -  For example that checks for
 +(UQL1) Before unifying an instantiation variable in `go_kappa`, we must check
 +  the usual unification conditions. In particular:
      * An occurs-check
 -    * Level mis-match
      * An attempt to unify a concrete type variable with a non-concrete type.
 +  We don't need a level-check because the level of an instantiation variable
 +  is infinity -- see (UQL3).
  (UQL2) What if kappa and ty have different kinds?  We simply call the
    ordinary unifier and use the coercion to connect the two.
@@ -2345,6 +2369,47 @@ That is the entire point of qlUnify!   Wrinkles:
    constraint arrows =>, so that (UQL4) applies to them as well.
    See Note [Multiplicity in deep subsumption].
 +(UQL6) What if `qlUnify` sees a regular (monotyped) unification variable, `alpha`, rather
 +  than an instantiation variable `kappa`?  Thus (alpha ~ ty).   It's tempting to just
 +  unify it, but the regular, on-the-fly unifier has lots of careful checks (levels,
 +  concreteness etc).  In regular unification it doesn't matter whether we unify on-the-fly
 +  or later -- it's just an efficiency issue -- but we must maintain all the careful invariants.
++
 +  The simplest thing is to say that `qlUnify` unifies /only/ instantiation variables
 +  (see calls to `isQLInstTyVar`).  We could be more ambitious, perhaps, in future, but
 +  beware of accidentally causing obscure /user-visible/ consequences (#26543),
 +  e.g. via Note [Occurs check and coercions].
++
 +  Remember, though, that the /only/ reason for QuickLoook is to unify instantiation variables
 +  with polytypes; anything else is optional, and will be picked up with later "ordinary"
 +  typechecking.  So unifing only instantiation variables is enough.
++
 +(UQL7) If `qlUnify` sees a concrete `kaapa`, thus
 +            kappa[conc] ~ some-type
 +  we just give up. It's tiresome to do all the checks for concreteness; and concrete
 +  type variables are never unified with polytypes, so it's fine to leave it for the
 +  regular unifier.
++
 +(UQL8) If we see (Maybe kappa ~ alpha), where `kappa` is an instantiation variable
 +  and `alpha` is a regular unification variable, we know that `kappa` must be a
 +  monotype, so we can use `qlMonoTcType` to monomorphise it.  This is important,
 +  because rule APP-LIGHTNING in the QuickLook paper only fires when there are no free
 +  instantiation variables.  Unifying `kappa` with a monotype makes it more possible
 +  for APP-LIGHTNING to fire.
++
 +  Same if we see (Maybe kappa ~ F tya) where F is a type function, becuase the result
 +  of a type function is always a monotype.
++
 +(UQL9) If we have (Maybe kappa ~ alpha) and we have /already/ unified alpha:=Maybe beta,
 +  then it's more efficient to look through that unification and decompose, so that
 +  we get (kappa ~ alpha).  That way we don't have to monomorphise `kappa`.  So we
 +  "look through" all meta-tyvars, not just the instantiation vars.
++
 +(UQL10) For the occurs check in `qlUnify` we simply use `anyFreeVarsOfType`.  For
 +  coercions that looks at the free vars of the coercion; but for coercion /holes/
 +  all it can do is look at the free vars of the hole's type.
 +  See Note [Occurs check and coercions] in GHC.Tc.Utils.Unify
++
  Sadly discarded design alternative
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  It is very tempting to use `unifyType` rather than `qlUnify`, killing off the

compiler/GHC/Tc/Solver/Equality.hs

@@ -2390,7 +2390,7 @@ checkTypeEqNoUnification ev eq_rel lhs rhs =
          given_pred = mkNomEqPred fam_app new_ty
          given_term = evCoercion $ mkNomReflCo new_ty  -- See Detail (4) of Note
 -    -- See Detail (7) of the Note
 +    -- See Detail (7) of Note [Type equality cycles: implementation]
      cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
  ----------------------
@@ -2648,15 +2648,15 @@ turn controls the behaviour of the workhorse: GHC.Tc.Utils.Unify.checkTyEqRhs.
  The details depend on whether we're working with a Given or a Wanted.
 -Given
 ------
 +Note [Type equality cycles: Givens]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  We emit a new Given, [G] F a ~ cbv, equating the type family application
  to our new cbv. This is actually done by `BreakGiven` in the `given_flags`
  in `checkTypeEqNoUnification`.
 -Note its orientation: The type family ends up on the left; see
 -Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for
 -CycleBreakerTvs is necessary. This scenario is now easily soluble, by using
 +Note its orientation: The type family ends up on the left;
 +see Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for
 +GivenCycleBreakerTvs is necessary. This scenario is now easily soluble, by using
  the first Given to rewrite the Wanted, which can now be solved.
  (The first Given actually also rewrites the second one, giving
@@ -2677,10 +2677,11 @@ to
  Note that
  * `cbv` is a fresh cycle breaker variable.
 -* `cbv` is a meta-tyvar, but it is completely untouchable.
 +* `cbv` is a meta-tyvar, of flavour GivenCycleBreakerTv, but it is
 +  completely untouchable.
  * We track the cycle-breaker variables in inert_cycle_breakers in InertSet
 -* We eventually fill in the cycle-breakers, with `cbv := F lhs`.
 -  No one else fills in CycleBreakerTvs!
 +* We eventually fill in the cycle-breakers, with `cbv := F lhs`,
 +  via `restoreTyVarCycles`.  No one else fills in GivenCycleBreakerTvs!
  * The evidence for the new `F lhs ~ cbv` constraint is Refl, because we know
    this fill-in is ultimately going to happen.
  * In `inert_cycle_breakers`, we remember the (cbv, F lhs) pair; that is, we
@@ -2690,8 +2691,8 @@ Note that
  * This fill-in is done when solving is complete, by restoreTyVarCycles
    in nestImplicTcS and runTcSWithEvBinds.
 -Wanted
 -------
 +Note [Type equality cycles: Wanteds]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  First, we do not cycle-break unless the LHS is a unifiable type variable
  See Note [Don't cycle-break Wanteds when not unifying].
@@ -2750,9 +2751,9 @@ to unify the cbvs:
    [W] AllEqF '[Bool] alpha
  Without the logic detailed in this Note, we're stuck here, as AllEqF cannot
 -reduce and alpha cannot unify. Let's instead apply our cycle-breaker approach,
 -just as described above. We thus invent cbv1 and cbv2 and unify
 -alpha := cbv1 -> cbv2, yielding (after zonking)
 +reduce and alpha cannot unify (occurs check). Let's instead apply our
 +cycle-breaker approach, just as described above. We thus invent cbv1 and cbv2
 +and unify alpha := (cbv1 : cbv2), yielding (after zonking)
    [W] Head (cbv1 : cbv2) ~ cbv1
    [W] Tail (cbv1 : cbv2) ~ cbv2
@@ -2790,8 +2791,8 @@ Note that we need to unify the cbvs here; if we did not, there would be
  no way to solve those constraints. That's why the cycle-breakers are
  ordinary TauTvs.
 -How all this is implemented
 ----------------------------
 +Note [Type equality cycles: implementation]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  We implement all this via the `TEFA_Break` constructor of `TyEqFamApp`,
  itself stored in the `tef_fam_app` field of `TyEqFlags`, which controls
  the behaviour of `GHC.Tc.Utils.Unify.checkTyEqRhs`.  The `TEFA_Break`
@@ -2918,7 +2919,7 @@ More details:
       CycleBreakerOrigin. This works for both Givens and Wanteds, as we need the
       logic in the W case for e.g. typecheck/should_fail/T17139.  Because this
       logic needs to work for Wanteds, too, we cannot simply look for a
 -     CycleBreakerTv on the left: Wanteds don't use them.
 +     GivenCycleBreakerTv on the left: Wanteds don't use them.
  **********************************************************************

compiler/GHC/Tc/Solver/InertSet.hs

@@ -304,7 +304,7 @@ instance Outputable WorkList where
  ********************************************************************* -}
  type CycleBreakerVarStack = NE.NonEmpty (Bag (TcTyVar, TcType))
 -   -- ^ a stack of (CycleBreakerTv, original family applications) lists
 +   -- ^ A stack of (GivenCycleBreakerTv, original family applications) lists
     -- first element in the stack corresponds to current implication;
     --   later elements correspond to outer implications
     -- used to undo the cycle-breaking needed to handle
@@ -324,6 +324,8 @@ data InertSet
                -- See `resetInertCans`
         , inert_cycle_breakers :: CycleBreakerVarStack
 +              -- The equalities for /given/ cycle breakers, GivenCycleBreakerTvs
 +              -- See Note [
         , inert_famapp_cache :: FunEqMap Reduction
                -- Just a hash-cons cache for use when reducing family applications
@@ -1955,7 +1957,8 @@ prohibitedSuperClassSolve given_loc wanted_loc
  {- *********************************************************************
  *                                                                      *
 -    Cycle breakers
 +                 Given Cycle breakers
 +  See Note [Type equality cycles: Givens] in GHC.Tc.Solver.Equality
  *                                                                      *
  ********************************************************************* -}

compiler/GHC/Tc/Solver/Monad.hs

@@ -2325,7 +2325,7 @@ wrapUnifier rws loc role do_unifications
  -}
  -- | Fill in CycleBreakerTvs with the variables they stand for.
 --- See Note [Type equality cycles] in GHC.Tc.Solver.Equality
 +-- See Note [Type equality cycles: Givens] in GHC.Tc.Solver.Equality
  restoreTyVarCycles :: InertSet -> TcM ()
  restoreTyVarCycles is
    = TcM.liftZonkM

compiler/GHC/Tc/Utils/TcMType.hs

@@ -726,11 +726,11 @@ cloneMetaTyVarName name
  metaInfoToTyVarName :: MetaInfo -> FastString
  metaInfoToTyVarName  meta_info =
    case meta_info of
 -       TauTv          -> fsLit "t"
 -       TyVarTv        -> fsLit "a"
 -       RuntimeUnkTv   -> fsLit "r"
 -       CycleBreakerTv -> fsLit "b"
 -       ConcreteTv {}  -> fsLit "c"
 +       TauTv               -> fsLit "t"
 +       TyVarTv             -> fsLit "a"
 +       RuntimeUnkTv        -> fsLit "r"
 +       GivenCycleBreakerTv -> fsLit "b"
 +       ConcreteTv {}       -> fsLit "c"
  newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
  newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi
@@ -824,7 +824,7 @@ cloneAnonMetaTyVar info tv kind
  -- in GHC.Tc.Solver.Equality.
  newCycleBreakerTyVar :: TcKind -> TcM TcTyVar
  newCycleBreakerTyVar kind
 -  = do { details <- newMetaDetails CycleBreakerTv
 +  = do { details <- newMetaDetails GivenCycleBreakerTv
         ; name <- newMetaTyVarName (fsLit "cbv")
         ; return (mkTcTyVar name kind details) }

compiler/GHC/Tc/Utils/TcType.hs

@@ -688,9 +688,10 @@ data MetaInfo
     | RuntimeUnkTv  -- ^ A unification variable used in the GHCi debugger.
                     -- It /is/ allowed to unify with a polytype, unlike TauTv
 -   | CycleBreakerTv  -- ^ Used to fix occurs-check problems in Givens
 -                     -- See Note [Type equality cycles] in
 -                     -- GHC.Tc.Solver.Equality
 +   | GivenCycleBreakerTv  -- ^ Used to fix occurs-check problems in Givens
 +                          -- Never used for Wanteds
 +                          -- See Note [Type equality cycles] in
 +                          -- GHC.Tc.Solver.Equality
     | ConcreteTv ConcreteTvOrigin
          -- ^ A unification variable that can only be unified
@@ -705,11 +706,11 @@ instance Outputable MetaDetails where
    ppr (Indirect ty) = text "Indirect" <+> ppr ty
  instance Outputable MetaInfo where
 -  ppr TauTv           = text "tau"
 -  ppr TyVarTv         = text "tyv"
 -  ppr RuntimeUnkTv    = text "rutv"
 -  ppr CycleBreakerTv  = text "cbv"
 -  ppr (ConcreteTv {}) = text "conc"
 +  ppr TauTv               = text "tau"
 +  ppr TyVarTv             = text "tyv"
 +  ppr RuntimeUnkTv        = text "rutv"
 +  ppr GivenCycleBreakerTv = text "cbv"
 +  ppr (ConcreteTv {})     = text "conc"
  -- | What caused us to create a 'ConcreteTv' metavariable?
  -- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete.
@@ -1299,7 +1300,7 @@ isRuntimeUnkTyVar tv
  isCycleBreakerTyVar tv
    | isTyVar tv -- See Note [Coercion variables in free variable lists]
 -  , MetaTv { mtv_info = CycleBreakerTv } <- tcTyVarDetails tv
 +  , MetaTv { mtv_info = GivenCycleBreakerTv } <- tcTyVarDetails tv
    = True
    | otherwise
@@ -1350,8 +1351,8 @@ metaTyVarInfo tv
  isTouchableInfo :: MetaInfo -> Bool
  isTouchableInfo info
 -  | CycleBreakerTv <- info = False
 -  | otherwise              = True
 +  | GivenCycleBreakerTv <- info = False
 +  | otherwise                   = True
  metaTyVarTcLevel :: TcTyVar -> TcLevel
  metaTyVarTcLevel tv

compiler/GHC/Tc/Utils/Unify.hs

@@ -103,7 +103,6 @@ import GHC.Types.Id( idType )
  import GHC.Types.Var as Var
  import GHC.Types.Var.Set
  import GHC.Types.Var.Env
 -import GHC.Types.Var.FV
  import GHC.Types.Basic
  import GHC.Types.Unique.Set (nonDetEltsUniqSet)
@@ -120,7 +119,6 @@ import GHC.Data.Maybe (firstJusts)
  import Control.Monad
  import Data.Functor.Identity (Identity(..))
  import qualified Data.List.NonEmpty as NE
 -import Data.Monoid as DM ( Any(..) )
  import qualified Data.Semigroup as S ( (<>) )
  import Data.Traversable (for)
@@ -3143,6 +3141,7 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref, u_given_eq_lvl = given_eq_lvl })
      do { traceTc "uUnfilledVar2 not ok" $
               vcat [ text "tv1:" <+> ppr tv1
                    , text "ty2:" <+> ppr ty2
 +                  , text "given_eq_lvl:" <+> ppr given_eq_lvl
                    , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2)
+                   ]
                 -- Occurs check or an untouchable: just defer
@@ -3236,16 +3235,17 @@ lhsPriority tv
          -> 5  -- Eliminate instantiation variables first
          | otherwise
          -> case info of
 -             CycleBreakerTv -> 0
 -             TyVarTv        -> 1
 -             ConcreteTv {}  -> 2
 -             TauTv          -> 3
 -             RuntimeUnkTv   -> 4
 +             GivenCycleBreakerTv -> 0
 +             TyVarTv             -> 1
 +             ConcreteTv {}       -> 2
 +             TauTv               -> 3
 +             RuntimeUnkTv        -> 4
  {- Note [Unification preconditions]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Question: given a homogeneous equality (alpha ~# ty), when is it OK to
  unify alpha := ty?
++
  (This note only applies to /homogeneous/ equalities, in which both
  sides have the same kind.)
@@ -3285,7 +3285,7 @@ There are five reasons not to unify:
       structured type.  So if 'ty' is a structured type, such as (Maybe x),
       don't unify.
 -   * CycleBreakerTv: never unified, except by restoreTyVarCycles.
 +   * GivenCycleBreakerTv: never unified, except by restoreGivenCycles.
 . (CONCRETE) A ConcreteTv can only unify with a concrete type,
      by definition.
@@ -3354,6 +3354,14 @@ Needless to say, all there are wrinkles:
      GHC.Tc.Solver.floatEqualities, around Nov 2020.  It's much easier
      to unify in-place, with no floating.
 +* (COERCIONS) What if there are coercions in the RHS?  E.g.
 +        alpha ~ (ty |> co)
 +   or   alpha ~ (ty co)
 +   We only recurse into the `coercionType` of `co` rather than `co` itself.
 +   Why? Mainly because `co` might be a coercion hole, in which case we /can't/
 +   recurse into the coercion that will eventually fill the hole.  This came
 +   up in #26543.
++
  Note [TyVar/TyVar orientation]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  See also Note [Fundeps with instances, and equality orientation]
@@ -3382,7 +3390,7 @@ So we look for a positive reason to swap, using a three-step test:
    touchable and can be unified.
    Tie-breaking rules for MetaTvs:
 -  - CycleBreakerTv: This is essentially a stand-in for another type;
 +  - GivenCycleBreakerTv: This is essentially a stand-in for another type;
         it's untouchable and should have the same priority as a skolem: 0.
    - TyVarTv: These can unify only with another tyvar, but we can't unify
@@ -3588,7 +3596,6 @@ matchExpectedFunKind hs_ty n k = go n k
  data UnifyCheckCaller
    = UC_OnTheFly   -- Called from the on-the-fly unifier
 -  | UC_QuickLook  -- Called from Quick Look
    | UC_Solver     -- Called from constraint solver
  -- | The result type of 'simpleUnifyCheck'.
@@ -3619,40 +3626,22 @@ simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUn
  -- unification might still be OK, but it'll take more work to do
  -- (use the full 'checkTyEqRhs').
  --
 --- It returns SUC_CannotUnify for
 ---   * Touchability failure
 ---   * Top level-shape failure
 ---
 --- It returns SUC_NotSure for
 ---   * Occurs check: lhs_tv occurs in rhs_ty
 ---   * Type families unless fam_ok=True
 ---   * Foralls unless
 ---        lhs_tv is RuntimeUnk (used by GHCi debugger)
 ---            or is a QL instantiation variable
 ---   * Concreteness: lhs_tv is concrete and rhs is a non-concrete type
 ---   * Skolem-escape: a level-check for type variables, to avoid skolem escape
 +-- See Note [simpleUnifyCheck]
  --
  -- This function is pretty heavily used, so it's optimised not to allocate
  simpleUnifyCheck caller given_eq_lvl lhs_tv rhs
 -  | not $ touchabilityTest given_eq_lvl lhs_tv
 -  = SUC_CannotUnify
 -  | not $ checkTopShape lhs_info rhs
 -  = SUC_CannotUnify
 -  | rhs_is_ok rhs
 -  = SUC_CanUnify
 -  | otherwise
 -  = SUC_NotSure
 +  | not $ touchabilityTest given_eq_lvl lhs_tv = SUC_CannotUnify
 +  | not $ checkTopShape lhs_info rhs           = SUC_CannotUnify
 +  | not (rhs_is_bad rhs)                       = SUC_CanUnify
 +  | otherwise                                  = SUC_NotSure
    where
 -    lhs_info = metaTyVarInfo lhs_tv
+-
 -    !(occ_in_ty, occ_in_co) = mkOccFolders (tyVarName lhs_tv)
+-
 +    lhs_info           = metaTyVarInfo lhs_tv
      lhs_tv_lvl         = tcTyVarLevel lhs_tv
      lhs_tv_is_concrete = isConcreteTyVar lhs_tv
 +    lhs_tv_nm          = tyVarName lhs_tv
 -    forall_ok = case caller of
 -                   UC_QuickLook -> isQLInstTyVar lhs_tv
 -                   _            -> isRuntimeUnkTyVar lhs_tv
 +    -- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect, esp (RUT1).
 +    forall_ok = isRuntimeUnkTyVar lhs_tv
      -- This fam_ok thing relates to a very specific perf problem
      -- See Note [Prevent unification with type families]
@@ -3661,58 +3650,78 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs
      --   see if it bites us)
      fam_ok = case caller of
                 UC_Solver     -> True
 -               UC_QuickLook  -> True
                 UC_OnTheFly   -> False
 -    rhs_is_ok (TyVarTy tv)
 -      | lhs_tv == tv                                    = False
 -      | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False
 -      | lhs_tv_is_concrete, not (isConcreteTyVar tv)    = False
 -      | occ_in_ty $! (tyVarKind tv)                     = False
 -      | otherwise                                       = True
+-
 -    rhs_is_ok (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
 -      | not forall_ok, isInvisibleFunArg af = False
 -      | otherwise                           = rhs_is_ok w && rhs_is_ok a && rhs_is_ok r
+-
 -    rhs_is_ok (TyConApp tc tys)
 -      | lhs_tv_is_concrete, not (isConcreteTyCon tc) = False
 -      | not forall_ok, not (isTauTyCon tc)           = False
 -      | not fam_ok,    not (isFamFreeTyCon tc)       = False
 -      | otherwise                                    = all rhs_is_ok tys
+-
 -    rhs_is_ok (ForAllTy (Bndr tv _) ty)
 -      | forall_ok = rhs_is_ok (tyVarKind tv) && (tv == lhs_tv || rhs_is_ok ty)
 -      | otherwise = False
+-
 -    rhs_is_ok (AppTy t1 t2)    = rhs_is_ok t1 && rhs_is_ok t2
 -    rhs_is_ok (CastTy ty co)   = not (occ_in_co co) && rhs_is_ok ty
 -    rhs_is_ok (CoercionTy co)  = not (occ_in_co co)
 -    rhs_is_ok (LitTy {})       = True
+-
+-
 -mkOccFolders :: Name -> (TcType -> Bool, TcCoercion -> Bool)
 --- These functions return True
 ---   * if lhs_tv occurs (incl deeply, in the kind of variable)
 ---   * if there is a coercion hole
 --- No expansion of type synonyms
 -mkOccFolders lhs_tv = ( getAny . runFVTop . check_ty
 -                      , getAny . runFVTop . check_co)
 -  where
 -    check_ty :: Type -> FV BoundVars Any
 -    !(check_ty, _, check_co, _) = foldTyCo occ_folder
+-
 -    occ_folder :: TyCoFolder (FV BoundVars Any)
 -    occ_folder = TyCoFolder { tcf_view  = noView  -- Don't expand synonyms
 -                            , tcf_tyvar = do_tcv, tcf_covar = do_tcv
 -                            , tcf_lit = mempty, tcf_hole  = do_hole
 -                            , tcf_tycobinder = addBndrFV }
 +    rhs_tcv_is_bad tcv
 +       -- c.f. checkTyVar, the TEFTyVar case
 +       | isCoVar tcv                                      = occ_check
 +       | tcTyVarLevel tcv `strictlyDeeperThan` lhs_tv_lvl = True
 +       | lhs_tv_is_concrete, not (isConcreteTyVar tcv)    = True
 +       | occ_check                                        = True
 +       | otherwise                                        = False
 +       where
 +         occ_check = simpleOccursCheck lhs_tv_nm tcv
++
 +    rhs_is_bad (TyVarTy tv) = rhs_tcv_is_bad tv
++
 +    rhs_is_bad (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
 +      | not forall_ok, isInvisibleFunArg af = True
 +      | otherwise                           = rhs_is_bad w || rhs_is_bad a || rhs_is_bad r
++
 +    rhs_is_bad (TyConApp tc tys)
 +      | lhs_tv_is_concrete, not (isConcreteTyCon tc) = True
 +      | not forall_ok, not (isTauTyCon tc)           = True
 +      | not fam_ok,    not (isFamFreeTyCon tc)       = True
 +      | otherwise                                    = any rhs_is_bad tys
++
 +    rhs_is_bad (ForAllTy (Bndr tv _) ty)
 +      | not forall_ok               = True
 +      | rhs_is_bad (tyVarKind tv)   = True
 +      | tv /= lhs_tv, rhs_is_bad ty = True
 +      | otherwise                   = False
++
 +    rhs_is_bad (AppTy t1 t2)    = rhs_is_bad t1 || rhs_is_bad t2
 +    rhs_is_bad (CastTy ty co)   = co_is_bad co || rhs_is_bad ty
 +    rhs_is_bad (CoercionTy co)  = co_is_bad co
 +    rhs_is_bad (LitTy {})       = False
++
 +    -- Coercions: see Note [Occurs check and coercions]
 +    co_is_bad co = anyFreeVarsOfCo rhs_tcv_is_bad co
++
 +{- Note [simpleUnifyCheck]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~
 +The function `simpleUnifyCheck` is a simple, /fast/ check for unifying (tv ~ rhs).
 +It can return a definite decision (SUC_CannotUnify of SUC_CanUnify), or uncertainty
 +(SUC_NotSure).  In the latter case we will later use `checkTyEqRhs` to resolve.
 +In particular:
++
 +   It returns SUC_CannotUnify for
 +   * Touchability failure
 +   * Top level-shape failure
++
 +   It returns SUC_NotSure for
 +   * Occurs check: lhs_tv occurs in rhs_ty
 +   * Type families unless fam_ok=True
 +   * Foralls unless
 +        lhs_tv is RuntimeUnk (used by GHCi debugger)
 +            or is a QL instantiation variable
 +   * Concreteness: lhs_tv is concrete and rhs is a non-concrete type
 +   * Skolem-escape: a level-check for type variables, to avoid skolem escape
++
 +Note [Occurs check and coercions]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +What if we have
 +    alpha ~ Int |>  (CoHole ch :: Type ~ blah)
 -    do_tcv v = (MkFV $ \ bvs ->
 -                Any (not (v `elemVarSet` bvs) && tyVarName v == lhs_tv))
 -               `mappend` check_ty (varType v)
 +Clearly we want to check that `alpha` doesn't appear free in `blah`.  But even if
 +it doesn't, what if `ch` is later filled in with a coercion mentioning `alpha`?
 +Tht would be bad: we'd get an infinite structure.
 -    do_hole _hole = MkFV $ \ _bvs -> DM.Any True  -- Reject coercion holes
 +The Right Thing to do is to check for a loop when (later) filling in `ch`.
 +We don't do that right now, and it's very obscure.  But in `simpleUnifyCheck`
 +we just look in the free vars of the /kind/ of the hole, which is what
 +`anyFreeVarsOfCo` does.
 +-}
  {- *********************************************************************
  *                                                                      *
@@ -4086,13 +4095,14 @@ wantConcreteCheck = \case
  -- where @cbv@ is a fresh loop-breaker tyvar (for Given), or
  -- just a fresh 'TauTv' (for Wanted)
  famAppBreaker :: FamAppBreaker a -> TcType -> TcM (PuResult a Reduction)
 -famAppBreaker BreakGiven fam_app
 +famAppBreaker BreakGiven fam_app    -- Givens
     = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
          ; return (PuOK (unitBag (new_tv, fam_app))
                         (mkReflRedn Nominal (mkTyVarTy new_tv))) }
                   -- Why reflexive? See Detail (4) of Note [Type equality cycles]
                   -- in GHC.Tc.Solver.Equality
 -famAppBreaker (BreakWanted ev lhs_tv) fam_app
++
 +famAppBreaker (BreakWanted ev lhs_tv) fam_app   -- Wanteds
    -- Occurs check or skolem escape; so flatten
    = do { reason <- checkPromoteFreeVars cteInsolubleOccurs
                       (tyVarName lhs_tv) lhs_tv_lvl
@@ -4236,10 +4246,16 @@ the RHS by
  Its specific behaviour is governed by the `TyEqFlags` that are passed
  to it; see Note [TyEqFlags].
 -Note, however, that `checkTyEqRhs` specifically does /not/ check for:
 -  * Touchability of the LHS (in the case of a unification variable)
 -  * Shape of the LHS (e.g. we can't unify Int with a TyVarTv)
 -These things are checked by `simpleUnifyCheck`.
 +Wrinkles
++
 +(CTER1) Note, however, that `checkTyEqRhs` specifically does /not/ check for:
 +         * Touchability of the LHS (in the case of a unification variable)
 +         * Shape of the LHS (e.g. we can't unify Int with a TyVarTv)
 +    These things are checked by `simpleUnifyCheck`.
++
 +(CTER2) Also `checkTyEqRhs` does not need to worry about RuntimeUnkTvs, because
 +    the solver is never called on constraints involving them.  See (RUT1) in
 +    Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect.
  -}
@@ -4297,6 +4313,7 @@ check_ty_eq_rhs :: forall m a
                  => TyEqFlags m a
                  -> TcType           -- Already zonked
                  -> m (PuResult a Reduction)
 +{-# INLINEABLE check_ty_eq_rhs #-}
  check_ty_eq_rhs flags ty
    = case ty of
        LitTy {}        -> return $ okCheckRefl ty
@@ -4327,7 +4344,7 @@ check_ty_eq_rhs flags ty
                            ; return (mkReflCoRedn Nominal <$> co_res) }
        ForAllTy {}   -> return $ PuFail impredicativeProblem -- Not allowed (TyEq:F)
 -{-# INLINEABLE check_ty_eq_rhs #-}
 +         -- No need to worry about RuntimeUnkTv
  -------------------
  checkCo :: Monad m => TyEqFlags m a -> Coercion -> m (PuResult a Coercion)
@@ -4351,7 +4368,10 @@ checkCo flags co =
          -- Occurs check (can promote)
          | OC_Check lhs_tv occ_prob <- occ
          , LC_Promote { lc_lvlp = lhs_tv_lvl } <- lc
 -        -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
 +        -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl $
 +                          tyCoVarsOfCo co
 +                           -- See Note [Occurs check and coercions]
 +                          --  and Note [checkCo] (2)
                ; return $
                  if cterHasNoProblem reason
                  then pure co
@@ -4648,7 +4668,7 @@ checkTyVar flags occ_tv
                    -- so the only reason for a filled meta-tyvar is promotion
                  else do_rhs_checks
 -                     [ simpleOccursCheck      occ  occ_tv
 +                     [ tyVarOccursCheck      occ  occ_tv
                       , tyVarLevelCheck        lc   occ_tv
                       , tyVarConcretenessCheck conc occ_tv ]
+               }
@@ -4706,17 +4726,24 @@ promotionDone occ_tv _ (CC_Promote {}) = isFilledMetaTyVar occ_tv
  promotionDone _      _               _ = return False
  ---------------------
 -simpleOccursCheck :: OccursCheck -> TcTyVar -> TyVarCheckResult m
 +tyVarOccursCheck :: OccursCheck -> TcTyCoVar -> TyVarCheckResult m
  -- ^ The "interpreter" for 'OccursCheck'
 -simpleOccursCheck OC_None _
 -  = TyVarCheck_Success
 -simpleOccursCheck (OC_Check lhs_tv occ_prob) occ_tv
 -  | lhs_tv == tyVarName occ_tv || check_kind (tyVarKind occ_tv)
 -  = TyVarCheck_Error (cteProblem occ_prob)
 -  | otherwise
 +-- Check for an occurrence of lhs_tv in occ_tv /or/ its kind
 +tyVarOccursCheck OC_None _
    = TyVarCheck_Success
 +tyVarOccursCheck (OC_Check { occurs_tv_name = lhs_tv, occurs_problem = prob }) occ_tcv
 +  | simpleOccursCheck lhs_tv occ_tcv = TyVarCheck_Error (cteProblem prob)
 +  | otherwise                        = TyVarCheck_Success
++
 +simpleOccursCheck :: Name -> TyCoVar -> Bool
 +-- Check for an occurrence of lhs_tv in occ_tv /or/ its kind
 +-- True <=> occurs check fires
 +simpleOccursCheck lhs_tv occ_tcv
 +  = is_bad occ_tcv || anyFreeVarsOfType is_bad (varType occ_tcv)
 +    -- anyFreeVarsOfType looks at the /deep/ free vars of the type
    where
 -    (check_kind, _) = mkOccFolders lhs_tv
 +    is_bad :: TyCoVar -> Bool
 +    is_bad occ_tcv = lhs_tv == tyVarName occ_tcv
  -------------------------
  tyVarLevelCheck :: LevelCheck m -> TcTyVar -> TyVarCheckResult m
@@ -4836,7 +4863,7 @@ checkTopShape info xi
                          RuntimeUnk  -> True
                          MetaTv { mtv_info = TyVarTv } -> True
                          _                             -> False
 -      CycleBreakerTv -> False  -- We never unify these
 +      GivenCycleBreakerTv -> False  -- We never unify these
        _ -> True
  --------------------------------------------------------------------------------
@@ -5149,14 +5176,14 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
      -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars
      -- (as they can be unified)
 -    -- and also for CycleBreakerTvs that mentions meta-tyvars
 +    -- and also for GivenCycleBreakerTvs that mentions meta-tyvars
      mentions_meta_ty_var :: TyVar -> Bool
      mentions_meta_ty_var tv
        | isMetaTyVar tv
        = case metaTyVarInfo tv of
            -- See Examples 8 and 9 in the Note
 -          CycleBreakerTv -> anyFreeVarsOfType mentions_meta_ty_var
 -                              (lookupCycleBreakerVar tv inert_set)
 +          GivenCycleBreakerTv -> anyFreeVarsOfType mentions_meta_ty_var
 +                                    (lookupCycleBreakerVar tv inert_set)
            _ -> True
        | otherwise
        = False
@@ -5199,7 +5226,7 @@ We want to solve w1 using g1 and g2. The presence of g3 is irrelevant, because
  we cannot unify 'f[tau:1] v[tau:1]' and 'g[sk:1] x[sk:3]' due to skolem escape.
  -}
 --- | Return the type family application a CycleBreakerTv maps to.
 +-- | Return the type family application a GivenCycleBreakerTv maps to.
  lookupCycleBreakerVar :: TcTyVar    -- ^ cbv, must be a CycleBreakerTv
                        -> InertSet
                        -> TcType     -- ^ type family application the cbv maps to

compiler/GHC/Types/Var/FV.hs

@@ -9,7 +9,7 @@ module GHC.Types.Var.FV (
          runFVSelective, runFVSelectiveList, runFVSelectiveSet,
          InterestingVarFun,
 -        addBndrFV, addBndrsFV, addBndrSelectiveFV, addBndrsSelectiveFV,
 +        updEnvFV, addBndrFV, addBndrsFV, addBndrSelectiveFV, addBndrsSelectiveFV,
          emptyFV,   -- or `mempty`
          unionFV,   -- or `mappend`
          mapUnionFV
@@ -138,7 +138,7 @@ type BoundVars = TyCoVarSet
  type VarSetFV     = FV BoundVars (EndoOS TyCoVarSet)
  type DVarSetFV    = FV BoundVars (EndoOS DTyCoVarSet)
 -type SelectiveDFV = FV (InterestingVarFun, BoundVars) (EndoOS DVarSet)
 +type SelectiveDFV = FV (BoundVars, InterestingVarFun) (EndoOS DVarSet)
  -- VarSetFV:     collects a VarSet
  -- DVarSetFV:    collects a DVarSet (deterministic)
  -- SelectiveDFV: selectively collects a DVarSet
@@ -158,9 +158,14 @@ pattern MkFV :: (env -> acc) -> FV env acc
  {-# COMPLETE MkFV #-}
  pattern MkFV f <- MkFV' f
        where
 -        MkFV f = MkFV' (oneShot f)
 +        MkFV f = MkFV' (oneShot (\env -> env `seq` f env))
           -- oneShot: this is the core of the one-shot trick!
           -- Note [The one-shot state monad trick] in  GHC.Utils.Monad.
 +         --
 +         -- seq: this is /important/: it makes the function strict.
 +         -- When the `env` is a pair (as it is in anyFreeVarsOfType), that means
 +         -- we get good worker/wrapper splitting.  Without it we get extra boxed
 +         -- pairs allocated by `anyFreeVarsOfType`.
  instance Semigroup a => Semigroup (FV env a) where
    (<>) = unionFV
@@ -174,28 +179,28 @@ emptyFV = MkFV (\_ -> mempty)
  unionFV :: Semigroup a => FV env a -> FV env a -> FV env a
  unionFV (MkFV' f1) (MkFV' f2) = MkFV (\env -> f1 env <> f2 env)
 -upd_bndrs_fv :: (env -> env) -> FV env a -> FV env a
 -{-# INLINE addBndrFV #-}
 -upd_bndrs_fv upd f = MkFV (\bvs -> runFV f $! upd bvs)
 +updEnvFV :: (env -> env) -> FV env a -> FV env a
 +updEnvFV upd f = MkFV (\bvs -> runFV f $! upd bvs)
      -- Strict application to avoid making a thunk
  addBndrFV :: TyCoVar -> FV BoundVars a -> FV BoundVars a
 -addBndrFV tcv = upd_bndrs_fv (\bvs -> extendVarSet bvs tcv)
 +{-# INLINE addBndrFV #-}
 +addBndrFV tcv = updEnvFV (\bvs -> extendVarSet bvs tcv)
  addBndrsFV :: [Var] -> FV BoundVars a -> FV BoundVars a
 -addBndrsFV tcvs = upd_bndrs_fv (\bvs -> extendVarSetList bvs tcvs)
 +addBndrsFV tcvs = updEnvFV (\bvs -> extendVarSetList bvs tcvs)
 -addBndrSelectiveFV :: TyCoVar -> FV (f, BoundVars) a -> FV (f, BoundVars) a
 +addBndrSelectiveFV :: TyCoVar -> FV (BoundVars, f) a -> FV (BoundVars, f) a
  addBndrSelectiveFV tcv
 -  = upd_bndrs_fv (\(f,bvs) -> let !bvs' = extendVarSet bvs tcv
 +  = updEnvFV (\(bvs,f) -> let !bvs' = extendVarSet bvs tcv
                                    -- Strict let to avoid thunks
 -                              in (f,bvs'))
 +                          in (bvs',f))
 -addBndrsSelectiveFV :: [Var] -> FV (f, BoundVars) a -> FV (f, BoundVars) a
 +addBndrsSelectiveFV :: [Var] -> FV (BoundVars, f) a -> FV (BoundVars, f) a
  addBndrsSelectiveFV bs
 -  = upd_bndrs_fv (\(f,bvs) -> let !bvs' = extendVarSetList bvs bs
 +  = updEnvFV (\(bvs,f) -> let !bvs' = extendVarSetList bvs bs
                                    -- Strict let to avoid thunks
 -                              in (f,bvs'))
 +                          in (bvs',f))
  mapUnionFV :: (Foldable t, Monoid acc)
            => (a -> FV env acc) -> t a -> FV env acc
@@ -221,7 +226,7 @@ runTyCoVarsDSet f = runFVAcc f emptyDVarSet
  runFVSelective :: InterestingVarFun -> SelectiveDFV -> DVarSet
  runFVSelective interesting f
 -  = runEndoOS (runFV f (interesting, emptyVarSet)) emptyDVarSet
 +  = runEndoOS (runFV f (emptyVarSet, interesting)) emptyDVarSet
  runFVSelectiveList :: InterestingVarFun -> SelectiveDFV -> [Var]
  runFVSelectiveList interesting f = dVarSetElems (runFVSelective interesting f)

testsuite/tests/default/default-fail05.stderr

  default-fail05.hs:11:10: error: [GHC-39999]
 -    • Ambiguous type variable ‘f0’ arising from a use of ‘toList’
 -      prevents the constraint ‘(Foldable f0)’ from being solved.
 -      Probable fix: use a type annotation to specify what ‘f0’ should be.
 +    • Ambiguous type variable ‘t0’ arising from a use of ‘toList’
 +      prevents the constraint ‘(Foldable t0)’ from being solved.
 +      Probable fix: use a type annotation to specify what ‘t0’ should be.
        Potentially matching instances:
          instance Foldable (Either a)
            -- Defined in ‘GHC.Internal.Data.Foldable’
          instance Foldable Maybe -- Defined in ‘GHC.Internal.Data.Foldable’
          ...plus three others
 -        ...plus 26 instances involving out-of-scope types
 +        ...plus 11 instances involving out-of-scope types
          (use -fprint-potential-instances to see them all)
      • In the first argument of ‘($)’, namely ‘toList’
        In the first argument of ‘print’, namely ‘(toList $ pure 21)’
        In a stmt of a 'do' block: print (toList $ pure 21)
  default-fail05.hs:11:19: error: [GHC-39999]
 -    • Ambiguous type variable ‘f0’ arising from a use of ‘pure’
 -      prevents the constraint ‘(Applicative f0)’ from being solved.
 -      Probable fix: use a type annotation to specify what ‘f0’ should be.
 +    • Ambiguous type variable ‘t0’ arising from a use of ‘pure’
 +      prevents the constraint ‘(Applicative t0)’ from being solved.
 +      Probable fix: use a type annotation to specify what ‘t0’ should be.
        Potentially matching instances:
          instance Applicative IO -- Defined in ‘GHC.Internal.Base’
          instance Applicative Maybe -- Defined in ‘GHC.Internal.Base’
          ...plus six others
 -        ...plus 9 instances involving out-of-scope types
 +        ...plus five instances involving out-of-scope types
          (use -fprint-potential-instances to see them all)
      • In the second argument of ‘($)’, namely ‘pure 21’
        In the first argument of ‘print’, namely ‘(toList $ pure 21)’
        In a stmt of a 'do' block: print (toList $ pure 21)
  default-fail05.hs:12:3: error: [GHC-39999]
 -    • Ambiguous type variable ‘t0’ arising from a use of ‘traverse’
 -      prevents the constraint ‘(Traversable t0)’ from being solved.
 +    • Ambiguous type variable ‘t1’ arising from a use of ‘traverse’
 +      prevents the constraint ‘(Traversable t1)’ from being solved.
        Relevant bindings include
 -        main :: IO (t0 ()) (bound at default-fail05.hs:10:1)
 -      Probable fix: use a type annotation to specify what ‘t0’ should be.
 +        main :: IO (t1 ()) (bound at default-fail05.hs:10:1)
 +      Probable fix: use a type annotation to specify what ‘t1’ should be.
        Potentially matching instances:
          instance Traversable (Either a)
            -- Defined in ‘GHC.Internal.Data.Traversable’
          instance Traversable Maybe
            -- Defined in ‘GHC.Internal.Data.Traversable’
          ...plus three others
 -        ...plus 28 instances involving out-of-scope types
 +        ...plus 13 instances involving out-of-scope types
          (use -fprint-potential-instances to see them all)
      • In a stmt of a 'do' block: traverse print (pure 42)
        In the expression:
@@ -51,16 +51,16 @@ default-fail05.hs:12:3: error: [GHC-39999]
                   traverse print (pure 42)
  default-fail05.hs:12:19: error: [GHC-39999]
 -    • Ambiguous type variable ‘t0’ arising from a use of ‘pure’
 -      prevents the constraint ‘(Applicative t0)’ from being solved.
 +    • Ambiguous type variable ‘t1’ arising from a use of ‘pure’
 +      prevents the constraint ‘(Applicative t1)’ from being solved.
        Relevant bindings include
 -        main :: IO (t0 ()) (bound at default-fail05.hs:10:1)
 -      Probable fix: use a type annotation to specify what ‘t0’ should be.
 +        main :: IO (t1 ()) (bound at default-fail05.hs:10:1)
 +      Probable fix: use a type annotation to specify what ‘t1’ should be.
        Potentially matching instances:
          instance Applicative IO -- Defined in ‘GHC.Internal.Base’
          instance Applicative Maybe -- Defined in ‘GHC.Internal.Base’
          ...plus six others
 -        ...plus 9 instances involving out-of-scope types
 +        ...plus five instances involving out-of-scope types
          (use -fprint-potential-instances to see them all)
      • In the second argument of ‘traverse’, namely ‘(pure 42)’
        In a stmt of a 'do' block: traverse print (pure 42)

testsuite/tests/ghci.debugger/scripts/T14628.stderr

+-
 -<interactive>:4:17: error: [GHC-25897]
 +<interactive>:4:7: error: [GHC-25897]
      • Couldn't match type ‘m’ with ‘(,) a0’
 -      Expected: StateT Int ((,) a0) ()
 -        Actual: StateT Int m ()
 +      Expected: (a0, ((), Int))
 +        Actual: m ((), Int)
        ‘m’ is an interactive-debugger skolem
 -    • In the first argument of ‘runStateT’, namely ‘_result’
 -      In the second argument of ‘($)’, namely ‘runStateT _result 0’
 +    • In the second argument of ‘($)’, namely ‘runStateT _result 0’
        In the expression: snd $ runStateT _result 0
 +      In an equation for ‘it’: it = snd $ runStateT _result 0
++

testsuite/tests/impredicative/T27917.hs

 +{-# LANGUAGE ImpredicativeTypes #-}
 +module T27917 where
++
 +pair :: forall p q. Maybe p -> q -> (p, q)
 +pair _ _ = undefined
++
 +ids :: [forall a. a -> a]
 +ids = []
++
 +use :: forall s. s -> ()
 +use _ = ()
++
 +isMaybe :: Maybe a -> ()
 +isMaybe (Just {}) = ()
++
 +-- #27917 reported that foo1 was accepted but foo2 was rejected!
 +foo1 = \y -> (isMaybe y, use (pair y ids))
 +foo2 = \y -> (use (pair y ids), isMaybe y)
++
 +{-   y :: Maybe alpha
 +     pair @k1 @k2 y ids
++
 +Maybe k1 ~ Maybe alpha
 +k2 ~ [ forall a. a->a ]
++
 +use @ss (pair ...)
++
 +ss ~ (k1, [forall a. a->a])
 +-}

testsuite/tests/impredicative/all.T

@@ -22,3 +22,4 @@ test('T17332', normal, compile_fail, [''])
  test('expr-sig', normal, compile, [''])
  test('Dict', normal, compile, [''])
  test('T24676', normal, compile, [''])
 +test('T27917', normal, compile, [''])

testsuite/tests/indexed-types/should_fail/T1897b.stderr

  T1897b.hs:16:1: error: [GHC-83865]
 -    • Couldn't match type: Depend b0
 -                     with: Depend b
 -      Expected: t (Depend b) -> Bool
 -        Actual: t (Depend b0) -> Bool
 +    • Couldn't match type: Depend a0
 +                     with: Depend a
 +      Expected: t (Depend a) -> Bool
 +        Actual: t (Depend a0) -> Bool
        Note: ‘Depend’ is a non-injective type family.
 -      The type variable ‘b0’ is ambiguous
 +      The type variable ‘a0’ is ambiguous
      • In the ambiguity check for the inferred type for ‘isValid’
        To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
        When checking the inferred type
 -        isValid :: forall {t :: * -> *} {b}.
 -                   (Foldable t, Bug b) =>
 -                   t (Depend b) -> Bool
 +        isValid :: forall {t :: * -> *} {a}.
 +                   (Foldable t, Bug a) =>
 +                   t (Depend a) -> Bool

testsuite/tests/typecheck/should_compile/LocalGivenEqs.hs

@@ -22,7 +22,7 @@ it mentions b in its RHS. It thus triggers Note [Type equality cycles]
  in GHC.Tc.Solver.Equality. That Note says we change the situation to
    [G] b ~ cbv GhcPs
    [G] Body b ~ cbv
 -for some fresh CycleBreakerTv cbv. Now, our original equality looks to be let-like,
 +for some fresh GivenCycleBreakerTv cbv. Now, our original equality looks to be let-like,
  but the new cbv equality is *not* let-like -- note that the variable is on the RHS.
  The solution is to consider any equality whose free variables are all at the current
  level to not stop equalities from floating. These are called *local*. Because both

testsuite/tests/typecheck/should_compile/T26543_orig.hs

 +-- This test is from the Description of #26543
++
 +{-# LANGUAGE GHC2024, TypeAbstractions, AllowAmbiguousTypes, NoImplicitPrelude,
 +                      TypeFamilies, UndecidableInstances #-}
 +module T26543_orig where
++
 +import Data.Kind
 +import Control.Applicative (Applicative(..))
 +import Prelude (type (~), ($))
++
 +type CAT k = k -> k -> Type
++
 +type family (~>) :: CAT k
 +type family Ob (a :: k) :: Constraint
 +type family UN (w :: j -> k) (wa :: k) :: j
++
 +class HasBinaryProducts k where
 +  type (a :: k) && (b :: k) :: k
 +  withObProd :: (Ob (a :: k), Ob b) => ((Ob (a && b)) => r) -> r
 +  (&&&) :: ((a :: k) ~> x) -> (a ~> y) -> (a ~> (x && y))
++
 +data AP (f :: Type -> Type) k = A k
 +type instance UN A (A k) = k
++
 +type Ap :: CAT (AP f k)
 +data Ap a b where
 +  Ap :: forall {k} a b f. (Ob a, Ob b) => f (a ~> b) -> Ap (A a :: AP f k) (A b)
++
 +type instance (~>) = Ap
 +type instance Ob a = (a ~ A (UN A a), Ob (UN A a))
++
 +instance (Applicative f, HasBinaryProducts k) => HasBinaryProducts (AP f k) where
 +  type a && b = A (UN A a && UN A b)
 +  withObProd @(A a) @(A b) r = withObProd @k @a @b r
 +  -- (&&&) :: Ap (a :: AP f k) x -> Ap a y -> Ap a (x && y)
 +  Ap @_ @x f &&& Ap @_ @y g = withObProd @k @x @y $ Ap (liftA2 (&&&) f g)

testsuite/tests/typecheck/should_compile/all.T

@@ -971,3 +971,5 @@ test('LazyFieldAnnotations', normal, compile, [''])
  test('T27557', normal, compile, [''])
  test('T27664', normal, compile, [''])
  test('T27916', normal, compile, [''])
 +test('T26543_orig', normal, compile, [''])
++

testsuite/tests/typecheck/should_fail/T22707.stderr

 -T22707.hs:6:59: error: [GHC-25897]
 -    • Couldn't match expected type ‘i1’
 -                  with actual type ‘m0
 -                                      GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0’
 -      ‘i1’ is a rigid type variable bound by
 -        the type signature for:
 -          t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
 -        at T22707.hs:5:1-47
 -    • In the expression: evalCont (t1 c) >>== \ ati1 -> return ati1 xa
 -      In the second argument of ‘($)’, namely
 -        ‘\ xa -> evalCont (t1 c) >>== \ ati1 -> return ati1 xa’
 -      In the second argument of ‘runCont’, namely
 -        ‘(ati1tti2 $ \ xa -> evalCont (t1 c) >>== \ ati1 -> return ...)’
 -    • Relevant bindings include
 -        ati1tti2 :: (a -> i1) -> i2 (bound at T22707.hs:6:16)
 -        c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4)
 -        t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
 -          (bound at T22707.hs:6:1)
+-
  T22707.hs:6:72: error: [GHC-25897]
 -    • Couldn't match type ‘o’
 -                     with ‘m0
 -                             GHC.Internal.Types.LiftedRep
 -                             GHC.Internal.Types.LiftedRep
 -                             (m0 GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0)’
 +    • Couldn't match type ‘i2’ with ‘a -> i1’
        Expected: Cont
 -                  ((a -> i1)
 -                   -> m0
 -                        GHC.Internal.Types.LiftedRep
 -                        GHC.Internal.Types.LiftedRep
 -                        (m0 GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0))
 +                  ((a -> i1) -> m0 (a -> i1) (a -> i1) (m0 (a -> i1) (a -> i1) b0))
                    i1
+                   a
          Actual: Cont (i2 -> o) i1 a
 -      ‘o’ is a rigid type variable bound by
 +      ‘i2’ is a rigid type variable bound by
          the type signature for:
            t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
          at T22707.hs:5:1-47
@@ -40,6 +13,9 @@ T22707.hs:6:72: error: [GHC-25897]
        In the first argument of ‘evalCont’, namely ‘(t1 c)’
        In the first argument of ‘(>>==)’, namely ‘evalCont (t1 c)’
      • Relevant bindings include
 +        xa :: a (bound at T22707.hs:6:53)
 +        ati1tti2 :: (a -> m0 (a -> i1) (a -> i1) b0) -> a -> i1
 +          (bound at T22707.hs:6:16)
          c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4)
          t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
            (bound at T22707.hs:6:1)

testsuite/tests/typecheck/should_fail/T26543a.hs

 +{-# LANGUAGE ImpredicativeTypes, PolyKinds #-}
++
 +-- Should be rejected via an occurs-check in the kinds,
 +-- but was erroneously accpeted with ImpredicativeTypes
 +-- See !16566
++
 +module T26543a where
++
 +import Data.Kind
 +import Data.Proxy
++
 +h :: forall k (m :: k -> Type) (a :: k). (Proxy k, Proxy (m a))
 +h = (Proxy, Proxy)
++
 +use2 :: forall t. (Proxy t, Proxy t) -> ()
 +use2 _ = ()
++
 +test = use2 h

testsuite/tests/typecheck/should_fail/T26543a.stderr

 +T26543a.hs:18:13: error: [GHC-27958]
 +    • Couldn't match type ‘t0’ with ‘m0 a0’
 +      Expected: (Proxy t0, Proxy t0)
 +        Actual: (Proxy t0, Proxy (m0 a0))
 +      Type variable kinds:
 +        m0 :: t0 -> *
 +        a0 :: t0
 +    • In the first argument of ‘use2’, namely ‘h’
 +      In the expression: use2 h
 +      In an equation for ‘test’: test = use2 h

testsuite/tests/typecheck/should_fail/all.T

@@ -767,4 +767,4 @@ test('T27210', normal, compile_fail, [''])
  test('T26532', normal, compile_fail, [''])
  test('T27731', normal, compile_fail, [''])
  test('T27844', normal, compile_fail, [''])
+-
 +test('T26543a', normal, compile_fail, [''])