The details depend on whether we're working with a Given or a Wanted.

 We emit a new Given, [G] F a ~ cbv, equating the type family application

 to our new cbv. This is actually done by `break_given` in

 `GHC.Tc.Solver.Monad.checkTypeEq`.

 the first Given to rewrite the Wanted, which can now be solved.

 (The first Given actually also rewrites the second one, giving

 Note that

 * `cbv` is a fresh cycle breaker variable.

 * We track the cycle-breaker variables in inert_cycle_breakers in InertSet

 * 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

 * This fill-in is done when solving is complete, by restoreTyVarCycles

   in nestImplicTcS and runTcSWithEvBinds.

 First, we do not cycle-break unless the LHS is a unifiable type variable

 See Note [Don't cycle-break Wanteds when not unifying] in GHC.Tc.Solver.Monad.

   [W] AllEqF '[Bool] alpha

 Without the logic detailed in this Note, we're stuck here, as AllEqF cannot

   [W] Head (cbv1 : cbv2) ~ cbv1

   [W] Tail (cbv1 : cbv2) ~ cbv2

 no way to solve those constraints. That's why the cycle-breakers are

 ordinary TauTvs.

 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`

      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

 **********************************************************************

 ********************************************************************* -}

 type CycleBreakerVarStack = NE.NonEmpty (Bag (TcTyVar, TcType))

    -- first element in the stack corresponds to current implication;

    --   later elements correspond to outer implications

    -- used to undo the cycle-breaking needed to handle

               -- See `resetInertCans`

        , inert_cycle_breakers :: CycleBreakerVarStack

        , inert_famapp_cache :: FunEqMap Reduction

               -- Just a hash-cons cache for use when reducing family applications

 {- *********************************************************************

 *                                                                      *

 *                                                                      *

 ********************************************************************* -}

         given_pred = mkNomEqPred fam_app new_ty

         given_term = evCoercion $ mkNomReflCo new_ty  -- See Detail (4) of Note

     cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin

 -------------------------

 -- | Fill in CycleBreakerTvs with the variables they stand for.

 restoreTyVarCycles :: InertSet -> TcM ()

 restoreTyVarCycles is

   = TcM.liftZonkM

 metaInfoToTyVarName :: MetaInfo -> FastString

 metaInfoToTyVarName  meta_info =

   case meta_info of

 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar

 newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi

 -- in GHC.Tc.Solver.Equality.

 newCycleBreakerTyVar :: TcKind -> TcM TcTyVar

 newCycleBreakerTyVar kind

        ; name <- newMetaTyVarName (fsLit "cbv")

        ; return (mkTcTyVar name kind details) }

    | RuntimeUnkTv  -- ^ A unification variable used in the GHCi debugger.

                    -- It /is/ allowed to unify with a polytype, unlike TauTv

    | ConcreteTv ConcreteTvOrigin

         -- ^ A unification variable that can only be unified

   ppr (Indirect ty) = text "Indirect" <+> ppr ty

 instance Outputable MetaInfo where

 -- | What caused us to create a 'ConcreteTv' metavariable?

 -- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete.

 isCycleBreakerTyVar tv

   | isTyVar tv -- See Note [Coercion variables in free variable lists]

   = True

   | otherwise

 isTouchableInfo :: MetaInfo -> Bool

 isTouchableInfo info

 metaTyVarTcLevel :: TcTyVar -> TcLevel

 metaTyVarTcLevel tv

         -> 5  -- Eliminate instantiation variables first

         | otherwise

         -> case info of

 {- Note [Unification preconditions]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

      structured type.  So if 'ty' is a structured type, such as (Maybe x),

      don't unify.

 4. (CONCRETE) A ConcreteTv can only unify with a concrete type,

     by definition.

   touchable and can be unified.

   Tie-breaking rules for MetaTvs:

        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

 -- 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)

    = 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

   -- Occurs check or skolem escape; so flatten

   = do { reason <- checkPromoteFreeVars cteInsolubleOccurs

                      (tyVarName lhs_tv) lhs_tv_lvl

                         RuntimeUnk  -> True

                         MetaTv { mtv_info = TyVarTv } -> True

                         _                             -> False

       _ -> True

 --------------------------------------------------------------------------------

     -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars

     -- (as they can be unified)

     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

           _ -> True

       | otherwise

       = False

 we cannot unify 'f[tau:1] v[tau:1]' and 'g[sk:1] x[sk:3]' due to skolem escape.

 -}

 lookupCycleBreakerVar :: TcTyVar    -- ^ cbv, must be a CycleBreakerTv

                       -> InertSet

                       -> TcType     -- ^ type family application the cbv maps to

 in GHC.Tc.Solver.Equality. That Note says we change the situation to

   [G] b ~ cbv GhcPs

   [G] Body b ~ cbv

 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