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

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

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

              -- True = two-way pre-unification

        Nothing -> InjectivityAccepted

          -- RHS are different, so equations are injective.

                   -- Payload of InjectivityUnified used only for check 1B2, only

                   -- for closed type families

         where

           lhs1Subst = Type.substTys subst (getInjArgs lhs1)

           lhs2Subst = Type.substTys subst (getInjArgs lhs2)

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

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

                     --   See end of sec 5.2 from the paper

     -> [Type] -> [Type]   -- Types to unify

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

       SurelyApart      -> Nothing

   where

     rn_env   = mkRnEnv2 in_scope

     maybe_fix | unif      = niFixSubst in_scope

               | otherwise = mkTvSubst in_scope -- when matching, don't confuse

 import GHC.Builtin.Types.Literals( tryInteractTopFam, tryInteractInertFam )

 import GHC.Types.Var.Set

 import GHC.Utils.Outputable

 import GHC.Utils.Panic

 import GHC.Data.Pair

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

   = do { let branches = fromBranches (coAxiomBranches ax)

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

        ; case getRelevantBranches ax work_args work_rhs of

               -> return [FDEqns { fd_qtvs = qtvs

            _  -> return [] }

 getRelevantBranches ax work_args work_rhs

   = go [] (fromBranches (coAxiomBranches ax))

   where

     work_tys = work_rhs : work_args

             = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys)

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

 -- Implements (INJFAM:Wanted/top)

     do_one branch@(CoAxBranch { cab_tvs = branch_tvs

                               , cab_lhs = branch_lhs_tys

                               , cab_rhs = branch_rhs })

                       -- False: matching, not unifying

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

             branch_lhs_tys' = substTys subst' branch_lhs_tys

       | otherwise

       = Nothing

     trim_qtvs :: Subst -> [TcTyVar] -> (Subst,[TcTyVar])

     -- Tricky stuff: see (TIF1) in

     -- Note [Type inference for type families with injectivity]