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

 During axiom application, we need to be aware of which branches are compatible

 with which others. The full explanation is in Note [Compatibility] in

 GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could

 theoretically compute compatibility on the fly, this is silly, so we store it

 in a CoAxiom.

 CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk

 stored in cab_incomps. The incompatibilities are properly a property of the

         FamInstMatch(..),

         lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,

         -- Injectivity

         InjectivityCheckResult(..),

 Note [Compatibility]

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

 Two patterns are /compatible/ if either of the following conditions hold:

 For open type families, only compatible instances are allowed. For closed

 type families, the story is slightly more complicated. Consider the following:

                   ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })

                   ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })

   -- See Note [Verifying injectivity annotation], case 1.

        Nothing -> InjectivityAccepted

          -- RHS are different, so equations are injective.

          -- This is case 1A from Note [Verifying injectivity annotation]

     isSurelyApart SurelyApart = True

     isSurelyApart _           = False

 {-

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

 *                                                                      *

         tcMatchTyX_BM, ruleMatchTyKiX,

         -- Side-effect free unification

         tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger,

         tcUnifyTysFG, tcUnifyTysForInjectivity,

         BindTvFun, BindFamFun, BindFlag(..),

               => BindTvFun -> Subst

               -> Type -> Type -> Maybe Subst

 tcMatchTyX_BM bind_tv subst ty1 ty2

 -- | Like 'tcMatchTy', but allows the kinds of the types to differ,

 -- and thus matches them as well.

 -- See also Note [tcMatchTy vs tcMatchTyKi]

 tcMatchTyKi :: HasDebugCallStack => Type -> Type -> Maybe Subst

 tcMatchTyKi ty1 ty2

 -- | This is similar to 'tcMatchTy', but extends a substitution

 -- See also Note [tcMatchTy vs tcMatchTyKi]

            -> Type                -- ^ Target

            -> Maybe Subst

 tcMatchTyX subst ty1 ty2

 -- | Like 'tcMatchTy' but over a list of types.

 -- See also Note [tcMatchTy vs tcMatchTyKi]

                              -- variables could be free in the target

                              -- See (CU6) in Note [The Core unifier]

 tcMatchTys tys1 tys2

 -- | Like 'tcMatchTyKi' but over a list of types.

 -- See also Note [tcMatchTy vs tcMatchTyKi]

              -> Maybe Subst    -- ^ One-shot substitution

                                -- See (CU6) in Note [The Core unifier]

 tcMatchTyKis tys1 tys2

 -- | Like 'tcMatchTys', but extending a substitution

 -- See also Note [tcMatchTy vs tcMatchTyKi]

             -> [Type]         -- ^ Target

             -> Maybe Subst    -- ^ One-shot substitution

 tcMatchTysX subst tys1 tys2

 -- | Like 'tcMatchTyKis', but extending a substitution

 -- See also Note [tcMatchTy vs tcMatchTyKi]

               -> [Type]       -- ^ Target

               -> Maybe Subst  -- ^ One-shot substitution

 tcMatchTyKisX subst tys1 tys2

 -- | Same as tc_match_tys_x, but starts with an empty substitution

 tc_match_tys :: HasDebugCallStack

              => BindTvFun

              -> [Type]

              -> [Type]

              -> Maybe Subst

 -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'

 tc_match_tys_x :: HasDebugCallStack

                => BindTvFun

                -> Subst

                -> [Type]

                -> [Type]

 tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2

   = case tc_unify_tys neverBindFam  -- (ATF7) in Note [Apartness and type families]

                       bind_tv

                       match_kis

                       RespectMultiplicities

                       (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of

       -- But even if it did, (ATF8) in Note [Apartness and type families]

       -- says it doesn't matter becuase here we only care about Unifiable.

       -- So neverBindFam is efficient, and sufficient.

                       False    -- No doing an injectivity check

                       IgnoreMultiplicities

                         -- See Note [Rewrite rules ignore multiplicities in FunTy]

                       rn_env tenv emptyCvSubstEnv [tmpl] [target] of

 tcUnifyDebugger :: Type -> Type -> Maybe Subst

 tcUnifyDebugger t1 t2

   = case tc_unify_tys_fg

              neverBindFam    -- Does not affect Unifiable, so pick max efficient

                              -- See (ATF8) in Note [Apartness and type families]

              alwaysBindTv

                -> Maybe Subst

 tcUnifyFunDeps qtvs tys1 tys2

   = case tc_unify_tys_fg

              dontCareBindFam    -- Class-instance heads never mention type families

              (matchBindTv qtvs)

              tys1 tys2 of

   = case tc_unify_tys alwaysBindFam alwaysBindTv

                        unif   -- Am I unifying?

                        True   -- Do injectivity checks

                        RespectMultiplicities

                        rn_env emptyTvSubstEnv emptyCvSubstEnv

                        tys1 tys2 of

                -- should never actually be done

     maybe_fix tv_subst

       -- When matching, don't confuse domain with range; no fixpoint!

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

              -> [Type] -> [Type]

              -> UnifyResult

 tcUnifyTysFG bind_fam bind_tv tys1 tys2

                 -> BindFamFun -> BindTvFun

                 -> [Type] -> [Type]

                 -> UnifyResult

 tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2

   = do { (tv_env, _) <- tc_unify_tys bind_fam bind_tv

                                   False      -- Not doing an injectivity check

                                   match_kis  -- Match outer kinds

                                   RespectMultiplicities rn_env

 -- | This function is actually the one to call the unifier -- a little

 -- too general for outside clients, though.

 tc_unify_tys :: BindFamFun -> BindTvFun

              -> RnEnv2

              -> TvSubstEnv  -- ^ substitution to extend

              -> CvSubstEnv

 -- See also Note [tcMatchTy vs tcMatchTyKi].

 tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env cv_env tys1 tys2

   = initUM tv_env cv_env $

        ; unify_tys env tys1 tys2 }

   where

     env = UMEnv { um_bind_tv_fun  = bind_tv

     kis2 = map typeKind tys2

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

 *                                                                      *

                 UnifyResult, MaybeApart etc

 -------------- unify_ty: the main workhorse -----------

 type InType      = Type       -- Before applying the RnEnv2

 type OutCoercion = Coercion   -- After applying the RnEnv2

     -- See (KCU1) in Note [Kind coercions in Unify]

   = maybeApart MARCast  -- See (KCU2)

   = unify_ty env ty1 ty2 (co1 `mkTransCo` kco)

   | otherwise -- We are matching, not unifying

   = do { c_subst <- getCvSubstEnv

        ; case co1 of

            CoVarCo cv

              , not (cv `elemVarEnv` c_subst)   -- Not forall-bound

              , let (_mult_co, co_l, co_r) = decomposeFunCo kco

                      -- Because the coercion is used in a type, it should be safe to

   = uVarOrFam env (TyVarLHS tv1) ty2 kco

 unify_ty env ty1 (TyVarTy tv2) kco

   = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco)

 -- Deal with TyConApps

   | Just (tc,tys) <- mb_sat_fam_app1

   = uVarOrFam env (TyFamLHS tc tys) ty2 kco

   , Just (tc,tys) <- mb_sat_fam_app2

   = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco)

     go swapped substs lhs@(TyVarLHS tv1) ty2 kco

       | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1'

       = -- We already have a substitution for tv1

            | (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return ()

            | otherwise                            -> surelyApart

            -- Unifying: recurse into unify_ty

       | TyVarTy tv2 <- ty2

       , let tv2' = umRnOccR env tv2

       , tv1' == tv2'

       | tv1_is_bindable

       , not (mentionsForAllBoundTyVarsR env ty2_fvs)

       -- e.g.   a    ~ F p q       with `a` not bindable: we might succeed with go_fam

       -- e.g.   a    ~ beta        with `a` not bindable: we might be able to bind `beta`

       -- e.g.   beta ~ F beta Int  occurs check; but MaybeApart after swapping

       , NotSwapped <- swapped  -- If we have swapped already, don't do so again

       = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco)

       | occurs_check = maybeApart MARInfinite   -- Occurs check

                         | otherwise

                         = False

           -- Occurs check, only when unifying

           -- see Note [Infinitary substitutions]

           -- Make sure you include `kco` in rhs #14846

       -- Hence the RnEnv2 is empty

       | not under_forall

       , Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1

            -- Below here we are matching

            -- The return () case deals with:

            --    Template:   (F a)..(F a)

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

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

       -- (Only worth doing this if we are not under a forall.)

       , NotSwapped <- swapped

       = go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco)

       | otherwise   -- See (ATF5) in Note [Apartness and type families]

        (inj_tys2, noninj_tys2) = partitionByList inj tys2

        bind_fam_if_poss

          = return ()

          = return ()

          | BindMe <- um_bind_fam_fun env tc tys1 rhs1

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

 import GHC.Core.TyCo.Rep( Type(..) )

 import GHC.Core.Predicate( EqRel(..) )

 import GHC.Core.TyCon

 import GHC.Core.Coercion.Axiom

 import GHC.Core.TyCo.Subst( elemSubst )

     relevant (EqCt { eq_ev = ev, eq_lhs = lhs, eq_rhs = rhs_ty })

        | isGiven ev

        , TyFamLHS _ lhs_tys <- lhs

        | otherwise

        = False

 -- Return the FunDepEqns that arise from each relevant branch

 -- Implements Definition [Relevance]

 getRelevantBranches ax work_args work_rhs

   where

     work_tys = work_rhs : work_args

          is_relevant branch@(CoAxBranch { cab_tvs = qtvs

                                         , cab_lhs = lhs_tys

                                         , cab_rhs = rhs_ty })

               -- See (RW1)-(RW3) in Note [Relevance]

               -- This is a pre-/unification/ check (not matching)

               -- so `subst` can bind both `qtvs` and fvs(work_tys)

                   lhs_tys'       = substTys subst' lhs_tys

                   rhs_ty'        = substTy  subst' rhs_ty

                   branch_tys'    = rhs_ty' : lhs_tys'

             = Just (FDEqns { fd_qtvs = qtvs'

                            , fd_eqs  = zipWith Pair branch_tys' work_tys })

                               -- Do not apply the substition to `work_tys`;

     do_one (CoAxBranch { cab_tvs = branch_qtvs

                        , cab_lhs = branch_lhs_tys

                        , cab_rhs = branch_rhs })

       , let (subst', qtvs') = trim_qtvs subst branch_qtvs

             branch_lhs_tys' = substTys subst' branch_lhs_tys

 -- ToDo

     A watertight proof that this is the Right Thing is not very easy.  See more

     discussion in #23162, and Section 5.2 of the paper.

 Note [Exploiting open type families]

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