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

 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

 -- If you edit this type, you may need to update the GHC formalism

 -- See Note [GHC Formalism] in GHC.Core.Lint

 data CoAxiom br

     { co_ax_unique   :: Unique        -- Unique identifier

     , co_ax_name     :: Name          -- Name for pretty-printing

     , co_ax_role     :: Role          -- Role of the axiom's equality

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

 -- | Find instances visible from the given set of imports

 hugInstancesBelow :: HscEnv -> UnitId -> ModuleNameWithIsBoot -> IO (InstEnv, [FamInst])

 hugInstancesBelow hsc_env uid mnwib = do

  (insts, famInsts) <-

      unzip . concat <$>

        hugSomeThingsBelowUs (\mod_info ->

                                   let details = hm_details mod_info

                                   -- Don't include instances for the current module

                                        then []

                                        else [(md_insts details, md_fam_insts details)])

                           True -- Include -hi-boot

                                  --   to fresh unification vars,

                                  -- See (IMP2) in Note [Improving against instances]

            }

 instance Outputable FunDepEqns where

 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 )

 import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam )

 import GHC.Types.Var.Set

 import GHC.Utils.Outputable

 import Control.Monad( unless )

 import GHC.Data.Pair

 {- Note [Overview of functional dependencies in type inference]

   from fundeps, but that would require new evidence forms, and an extension to

   FC, so we don't do that right now (Dec 14).

 Note [FunDep and implicit parameter reactions]

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

 Currently, our story of interacting two dictionaries (or a dictionary

 tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage ()

 tryFamEqFunDeps mode eqs_for_me fam_tc work_args

                 work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs })

   | Just ops <- builtInClosedTyFamTyCon_maybe fam_tc

             ; tryFDEqns False fam_tc work_args work_item eqns

             ; unless (hasRelevantGiven eqs_for_me work_args work_item) $

               do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs

                  ; tryFDEqns True fam_tc work_args work_item eqns } }

            NotInjective  -> nopStage ()

            Injective inj -> do { eqns <- mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs

                                ; tryFDEqns False fam_tc work_args work_item eqns }

        ; unless (hasRelevantGiven eqs_for_me work_args work_item) $

          do { eqns <- mkTopFamEqFDs fam_tc work_args work_item

             ; tryFDEqns True fam_tc work_args work_item eqns } }

 --  User-defined type families

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

 mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunDepEqns]

 -- Look at the top-level axioms; we effectively infer injectivity,

 -- type families without injectivity info

 mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs })

   | isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families]

   = Stage $

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

        | isGiven ev

        , TyFamLHS _ lhs_tys <- lhs

        | otherwise

        = False

 getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns]

 -- Return the FunDepEqns that arise from each relevant branch

 getRelevantBranches ax work_args work_rhs

   where

     work_tys = work_rhs : work_args

       = case is_relevant branch of

       where

             = Just (FDEqns { fd_qtvs = qtvs'

             | otherwise

             = Nothing

 mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns]

 mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })

   = do { fam_envs <- getFamInstEnvs

        ; let branches :: [CoAxBranch]

        ; return (mapMaybe do_one branches) }

   where

     do_one :: CoAxBranch -> Maybe FunDepEqns

             branch_lhs_tys' = substTys subst' branch_lhs_tys

       | otherwise

       = Nothing

 mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> SolverStage [FunDepEqns]

 -- Wanted constraints only

 -- Both open and closed type families, but only ones with declared injectivity

 mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs

   = do { let -- eqns_from_inerts: see (INJFAM:Wanted/other)

              eqns_from_inerts = mapMaybe do_one eqs_for_me

     mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs

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

 --  Built-in type families

 * (INJFAM:Wanted/other) see `mkLocalFamEqFDs`

     work item: [W]   F s1 s2 ~ rhs   -- Wanted

     inert:     [G/W] F t2 t2 ~ rhs   -- Same `rhs`, Given or Wanted

 For /built-in/ type families, it's pretty similar, except that

    * mkLocalBuiltinFamEqFDs

    * mkTopBuiltinFamEqFDs

       type family F a | r -> a where { .... }

       [W] F t1 ~ a

       [W] F t2 ~ a

 We say that a closed-type-family equation `F lhs = rhs` is

    /relevant/ for a Wanted [W] F wlhs ~ wrhs

 iff

   (R2) There is no earlier equation that matches S(lhs).  See (RW4) below.

 (RW1) Pre-unification treats type-family applications as binding to anything,

     rather like type variables.  If two types don't even pre-unify, we say that they

     are /apart/.  It is done by `tcUnifyTysForInjectivity`.

     Clearly the RHS is apart from the first equation and we want to fire injectivity

     on the second equation.

           type family Bak a = r where

              Bak Int  = Char   -- B1

              Bak Char = Int    -- B2

              Bak a    = a      -- B3

     You might think that (B3) could be instantiated to Bak Char ~ Char; but

     actually that instantiation will never fire because (B2) Bak Char ~ Int would

     can emit [W] alpha ~ Int.  Hence (B3) is not relevant; only (B2) is relevant.

     That is the reason for condition (R2) in the definition of Relevance above.

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