isTypeDataTyCon,

         isEnumerationTyCon,

         isNewTyCon, isAbstractTyCon,

         isTypeFamilyTyCon, isDataFamilyTyCon,

         isOpenTypeFamilyTyCon, isClosedFamilyTyCon_maybe,

         tyConInjectivityInfo,

   | FamilyTyCon {famTcFlav = BuiltInSynFamTyCon ops} <- details = Just ops

   | otherwise                                                   = Nothing

 -- | Extract type variable naming the result of injective type family

 tyConFamilyResVar_maybe :: TyCon -> Maybe Name

 tyConFamilyResVar_maybe (TyCon { tyConDetails = details })

 import GHC.Utils.Outputable

 import GHC.Utils.Panic

 import GHC.Data.Pair

 import Data.Maybe( isNothing, isJust, mapMaybe )

       | otherwise

       = improveFromAnother (ctEvPred inert_ev) work_pred

 -- The fundeps generated an insoluble constraint.

 -- It's valuable to flag such constraints as insoluble becuase that improves

 -- pattern-match overlap checking

 insolubleFunDep ev

   = if isGiven ev

     then tryGivenBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_item

     else do { -- Note [Do local fundeps before top-level instances]

   -- Only Wanted constraints below here

   = do { -- Note [Do local fundeps before top-level instances]

          case tyConInjectivityInfo fam_tc of

            NotInjective  -> nopStage ()

   | isOpenTypeFamilyTyCon fam_tc

   , Injective inj_flags <- tyConInjectivityInfo fam_tc

   = -- Open, injective type families

   | Just ax <- isClosedFamilyTyCon_maybe fam_tc

   = -- Closed type families

   | otherwise

   = -- Data families, abstract families,

     -- closed type families with no equations (isClosedFamilyTyCon_maybe returns Nothing)

     return []

   = Stage $

                                     , text "rhs:" <+> ppr rhs

                                     , text "eqns:" <+> ppr fd_eqns ])

        ; (insoluble, unif_happened) <- solveFunDeps ev fd_eqns

        ; if | unif_happened -> startAgainWith (CEqCan work_item)

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

 --  User-defined type families

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

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

 -- so we don't need tyConInjectivtyInfo.  This works fine for closed

 -- type families without injectivity info

 -- See Note [Exploiting closed type families]

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

        ; case getRelevantBranches ax work_args work_rhs of

 hasRelevantGiven :: [EqCt] -> [TcType] -> EqCt -> Bool

 -- A Given is relevant if it is not apart from the Wanted

          no_match lhs_tys (CoAxBranch { cab_lhs = lhs_tys1 })

             = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys)

 -- Implements (INJFAM:Wanted/top)

   = do { fam_envs <- getFamInstEnvs

        ; let branches :: [CoAxBranch]

              branches = concatMap (fromBranches . coAxiomBranches . fi_axiom) $

       | otherwise

       = Nothing

 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

     do_one _ = return ()

 mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs

   = return [FDEqns { fd_qtvs = []

                    , fd_eqs = map snd $ tryInteractTopFam ops fam_tc work_args work_rhs }]

 mkLocalBuiltinFamEqFDs :: [EqCt] -> TyCon -> BuiltInSynFamily

 mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs

   = do { let do_one :: EqCt -> [FunDepEqns]

              do_one (EqCt { eq_lhs = TyFamLHS _ inert_args, eq_rhs = inert_rhs })

       * (KK3b) If the role of `fs` is Representational:

            kick out if `rhs_s` is of form `(lhs_w t1 .. tn)`

 Rationale

 * (KK0) kick out only if `fw` can rewrite `fs`.

 * (KK3) see Note [KK3: completeness of solving]

 The above story is a bit vague wrt roles, but the code is not.

 See Note [Flavours with roles]

   by the inert item.  And too much kick-out is positively harmful.

   (Historical example #14363.)

   (KK3b) is that we treat an inert item

         a -f-> b

   in the same way as

          -- The above check redundantly checks the role & flavour,

          -- but it's very convenient

       -- (KK2)

       | let where_to_look | fs_can_rewrite_fr = LookOnlyUnderFamApps

                           | otherwise         = LookEverywhere

              n_kicked = lengthBag kicked_out

        ; setInertCans ics'

        ; unless (isEmptyBag kicked_out) $

          do { emitWork kicked_out

 T15767.hs:7:5: error: [GHC-39999]

     • In the expression: x

       In an equation for ‘y’:

           y = x