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

   = let getInjArgs  = filterByList injectivity

         in_scope    = mkInScopeSetList (tvs1 ++ tvs2)

              -- True = two-way pre-unification

        Nothing -> InjectivityAccepted

          -- RHS are different, so equations are injective.

         -- Side-effect free unification

         tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger,

         BindTvFun, BindFamFun, BindFlag(..),

         matchBindTv, alwaysBindTv, alwaysBindFam, dontCareBindFam,

         UnifyResult, UnifyResultM(..), MaybeApartReason(..),

 (ATF7) There is one other, very special case of matching where we /do/ want to

    bind type families in `um_fam_env`, namely in GHC.Tc.Solver.Equality, the call

    Consider

    of a match. Consider

       type family G6 a = r | r -> a

 -- | Unify or match a type-family RHS with a type (possibly another type-family RHS)

 -- Precondition: kinds are the same

     :: AmIUnifying  -- ^ True <=> do two-way unification;

                     --   False <=> do one-way matching.

                     --   See end of sec 5.2 from the paper

     -> InScopeSet     -- Should include the free tyvars of both Type args

     -> Maybe Subst

 -- This algorithm is an implementation of the "Algorithm U" presented in

 -- the paper "Injective type families for Haskell", Figures 2 and 3.

 -- The code is incorporated with the standard unifier for convenience, but

 -- its operation should match the specification in the paper.

   = case tc_unify_tys alwaysBindFam alwaysBindTv

                        unif   -- Am I unifying?

                        True   -- Do injectivity checks

                        False  -- Don't check outermost kinds

                        RespectMultiplicities

                        rn_env emptyTvSubstEnv emptyCvSubstEnv

       Unifiable          (tv_subst, _cv_subst) -> Just $ maybe_fix tv_subst

       MaybeApart _reason (tv_subst, _cv_subst) -> Just $ maybe_fix tv_subst

                  -- We want to *succeed* in questionable cases.

 import GHC.Core.Coercion

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

 import GHC.Core.TyCon

 import GHC.Core.Coercion.Axiom

 import GHC.Core.TyCo.Subst( elemSubst )

 mkTopClosedFamEqFDs ax work_args work_rhs

   = do { let branches = fromBranches (coAxiomBranches ax)

        ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs)

               -> return [FDEqns { fd_qtvs = qtvs

                                 , fd_eqs = zipWith Pair lhs_tys work_args }]

            _  -> return [] }

   where

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

 -- Implements (INJFAM:Wanted/top)