import GHC.Core.Coercion

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

 import GHC.Core.TyCon

 import GHC.Core.Coercion.Axiom

 import GHC.Core.TyCo.Subst( elemSubst )

   it doesn't matter which of the two we pick, but historically we have

   picked the local-fundeps first.

 (DFL2) Try solving from top-level instances before fundeps.

   From the definition `foo = op` we get

     [W] FD Int Bool

   We solve this from the top level instance before even trying fundeps.

   If we did try fundeps, we'd generate [W] b ~ Bool, which fails.

   a waste of effort.

   (DFL2) is achieved by trying fundeps only on /unsolved/ Wanteds.

 -}

 tryEqFunDeps :: EqCt -> SolverStage ()

   | NomEq <- eq_rel

   | otherwise

   = nopStage ()

   | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc

   = if isGiven ev

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

   | isGiven ev    -- See (INJFAM:Given)

   = nopStage ()

   , Injective inj_flags <- tyConInjectivityInfo fam_tc

   = -- Open, injective type families

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

   | Just ax <- isClosedFamilyTyCon_maybe fam_tc

   = -- Closed type families

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

          simpleStage $ traceTcS "fundep closed" (ppr fam_tc)

        ; case tyConInjectivityInfo fam_tc of

            NotInjective  -> nopStage()

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

   | otherwise -- Data families, abstract families

   = nopStage ()

     go (branch : later_branches)

       | CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys

                    , cab_rhs = rhs_ty, cab_incomps = incomps } <- branch

       = if all no_match_branch incomps && all no_match_branch later_branches

         then [FDEqns { fd_qtvs = qtvs, fd_eqs = zipWith Pair lhs_tys work_args }]

         else []

       = go later_branches

     no_match_branch (CoAxBranch { cab_lhs = lhs_tys, cab_rhs = rhs_ty })

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

 -- Implements (INJFAM:Wanted/top)

                                    !(subst', tvs') = trim_qtvs subst1 tvs

                                in (subst', tv':tvs')

              -- eqns_from_self: see (INJFAM:Wanted/Self)

              eqns_from_self   = case tcSplitTyConApp_maybe work_rhs of

                                   Just (tc,rhs_tys) | tc==fam_tc -> [mk_eqn rhs_tys]

 --  Built-in type families

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

 -- TyCon is definitely a built-in type family

 -- Built-in type families are special becase we can generate

 -- evidence from /Givens/. For example:

 --    from [G] x+4~7 we can deduce [G] x~7

 -- That's important!

 -- See Note [Given/Given fundeps for built-in type families]

   = Stage $

     do { traceTcS "tryBuiltinFamEqFDs" $

          vcat [ text "lhs:" <+> ppr fam_tc <+> ppr work_args

               , text "work_ev:" <+> ppr work_ev ]

        -- interact with inert Givens, emitting new Givens

        -- Interact with top-level instancs, emitting new Givens

        ; emitNewGivens (ctEvLoc work_ev) $

   = return [FDEqns { fd_qtvs = []

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

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

                | inert_rhs `tcEqType` work_rhs = [mk_eqn inert_args]

                | otherwise                     = []

                                    , fd_eqs = map snd $ tryInteractInertFam ops fam_tc

                                                                      work_args iargs }

              eqns_from_self   = case tcSplitTyConApp_maybe work_rhs of

                                   Just (tc,rhs_tys) | tc==fam_tc -> [mk_eqn rhs_tys]

                                   _                              -> []

     eqs = [ Pair lhs_arg rhs_arg

           | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ]

 -- Look in the InertSet, and return all inert equalities

 --    F tys ~N# rhs

 --    where F is the specified TyCon

 -- Representational equalities don't interact with type family dependencies

   = do { IC {inert_funeqs = funeqs } <- getInertCans

        ; return [ funeq_ct | equal_ct_list <- findFunEqsByTyCon funeqs fam_tc

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

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

   - When F is a built-in type family, we can do better;

     See Note [Given/Given fundeps for built-in type families]

     work item: [W] F s1 s2 ~ F t1 t2

   We can generate FunDepEqns: (s2 ~ t2)

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

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

   We can generate FunDepEqns: (s2 ~ t2)