(ATF3) What about foralls?   For example, supppose we are unifying

            (forall a. F a) -> (forall a. F a)

    So to keep things simple, the entire family-substitution machinery is used

    `uSatFamApp`).  That's fine, because the apartness business is used only for

    reducing type-family applications, and class instances, and their arguments

    can't have foralls anyway.

           instance (Generic1 f, Ord (Rep1 f a))

                 => Ord (Generically1 f a) where ...

               -- The "..." gives rise to [W] Ord (Generically1 f a)

    We must use the instance decl (recursively) to simplify the [W] constraint;

    we do /not/ want to worry that the `[G] Ord (Rep1 f a)` might be an

    alternative path.  So `noMatchableGivenDicts` must return False;

    `DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`.  See

    `go` in `uVarOrFam`

 (ATF6) When /matching/ can we ever have a type-family application on the LHS, in

    the template?  You might think not, because type-class-instance and

    type-family-instance heads can't include type families.  E.g.

    But you'd be wrong: even when matching, we can see type families in the LHS template:

    * In `checkValidClass`, in `check_dm` we check that the default method has the

       right type, using matching, both ways.  And that type may have type-family

    * In the specialiser: see the call to `tcMatchTy` in

      `GHC.Core.Opt.Specialise.beats_or_same`

          RULE forall a (d :: Eq (Maybe (F a))) .

                  f @(Maybe (F a)) d = ...

      See #25965.

     type variables/ that makes the match work.  So we simply want to recurse into

     the arguments of the type family.  E.g.

        Template:   forall a.  Maybe (F a)

     We want to succeed with substitution [a :-> Int].  See (ATF9).

     Conclusion: where we enter via `tcMatchTy`, `tcMatchTys`, `tc_match_tys`,

       type family G6 a = r | r -> a

       type instance G6 [a]  = [G a]

       type instance G6 Bool = Int

       [W] G6 alpha ~ [Int]

         Template: [G a]    Target: [Int]

    and we want to succeed with MaybeApart, so that we can generate the improvement

    constraint

 (ATF9) Decomposition.  Consider unifying

           F a  ~  F Int

           F Int ~ F Bool

 (ATF10) Injectivity.  Consider (AFT9) where F is known to be injective.  Then if we

   are unifying

 --           , text "fam_env" <+> ppr (um_fam_env substs) ]) $

        ; go NotSwapped substs ty1 ty2 kco }

   where

     -- `go` takes two bites at the cherry; if the first one fails

     -- it swaps the arguments and tries again; and then it fails.

     -- The SwapFlag argument tells `go` whether it is on the first

                         | otherwise

                         = False

         occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs

           -- Occurs check, only when unifying

           -- see Note [Infinitary substitutions]

     -- LHS is a saturated type-family application

     -- Invariant: ty2 is not a TyVarTy

     go swapped substs lhs@(TyFamLHS tc1 tys1) ty2 kco

       -- Check if we have an existing substitution for the LHS; if so, recurse

       = if | um_unif env                          -> unify_ty env ty1' ty2 kco

            -- Below here we are matching

            -- The return () case deals with:

            | otherwise                            -> maybeApart MARTypeFamily

       -- Check for equality  F tys1 ~ F tys2

       | Just (tc2, tys2) <- isSatTyFamApp ty2

       , tc1 == tc2

       = go_fam_fam substs tc1 tys1 tys2 kco

       -- Now check if we can bind the (F tys) to the RHS

       -- This can happen even when matching: see (ATF7)

       | BindMe <- um_bind_fam_fun env tc1 tys1 rhs

       = if uOccursCheck substs emptyVarSet lhs rhs

       -- Maybe um_bind_fam_fun is False of (F a b) but true of (G c d e)

       -- NB: a type family can appear on the template when matching

       --     see (ATF6) in Note [Apartness and type families]

       | um_unif env

       , NotSwapped <- swapped

       , Just lhs2 <- canEqLHS_maybe ty2

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

     -- go_fam_fam: LHS and RHS are both saturated type-family applications,

     --             for the same type-family F

     go_fam_fam substs tc tys1 tys2 kco

        -- Decompose (F tys1 ~ F tys2): (ATF9)

        -- Use injectivity information of F: (ATF10)

       = do { bind_fam_if_poss                 -- (ATF11)

            ; unify_tys env inj_tys1 inj_tys2  -- (ATF10)

            ; unless (um_inj_tf env) $         -- (ATF12)

              unify_tys env noninj_tys1 noninj_tys2 }

      where

        inj = case tyConInjectivityInfo tc of

        bind_fam_if_poss

          | not (um_unif env)  -- Not when matching (ATF11-1)

          = return ()

          | BindMe <- um_bind_fam_fun env tc tys1 rhs1

          = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $

            extendFamEnv tc tys1 rhs1

 test('T26358', expect_broken(26358), compile, [''])

 test('T26345', normal, compile, [''])

 test('T26376', normal, compile, [''])