Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: b8821d43 by Simon Peyton Jones at 2025-11-15T23:18:00+00:00 Better Fix Yikes 3 Ensure we do F a ~ F b for families with no eqns - - - - - 2 changed files: - compiler/GHC/Core/TyCon.hs - compiler/GHC/Tc/Solver/FunDeps.hs Changes: ===================================== compiler/GHC/Core/TyCon.hs ===================================== @@ -2448,8 +2448,9 @@ isOpenTypeFamilyTyCon (TyCon { tyConDetails = details }) | FamilyTyCon {famTcFlav = OpenSynFamilyTyCon } <- details = True | otherwise = False --- | Is this a non-empty closed type family? Returns 'Nothing' for --- abstract or empty closed families. +-- | Is this a /non-empty/ closed type family? +-- Returns 'Nothing' for closed type family with no equations, as well +-- as for open families, data famlilies, abstract families isClosedFamilyTyCon_maybe :: TyCon -> Maybe (CoAxiom Branched) isClosedFamilyTyCon_maybe (TyCon { tyConDetails = details }) | FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb} <- details = mb ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -25,6 +25,7 @@ import GHC.Core.FamInstEnv import GHC.Core.Coercion import GHC.Core.Predicate( EqRel(..) ) import GHC.Core.TyCon +import GHC.Core.Type( tyConAppTyCon_maybe ) import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart ) import GHC.Core.Coercion.Axiom import GHC.Core.TyCo.Subst( elemSubst ) @@ -467,7 +468,8 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs , eq_eq_rel = eq_rel }) | NomEq <- eq_rel , TyFamLHS fam_tc work_args <- work_lhs -- We have F args ~N# rhs - = do { eqs_for_me <- simpleStage$ getInertFamEqsFor fam_tc work_args work_rhs + = do { simpleStage $ traceTcS "tryEqFunDeps" (ppr work_item) + ; eqs_for_me <- simpleStage $ getInertFamEqsFor fam_tc work_args work_rhs ; tryFamEqFunDeps eqs_for_me fam_tc work_args work_item } | otherwise = nopStage () @@ -482,7 +484,7 @@ tryFamEqFunDeps eqs_for_me fam_tc work_args else do { -- Note [Do local fundeps before top-level instances] tryFDEqns fam_tc work_args work_item $ mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs - ; if null eqs_for_me + ; if all (isWanted . eqCtEvidence) eqs_for_me then tryFDEqns fam_tc work_args work_item $ mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs else nopStage () } @@ -492,38 +494,37 @@ tryFamEqFunDeps eqs_for_me fam_tc work_args -- Only Wanted constraints below here - | isOpenTypeFamilyTyCon fam_tc - , Injective inj_flags <- tyConInjectivityInfo fam_tc - = -- Open, injective type families - do { -- Note [Do local fundeps before top-level instances] - tryFDEqns fam_tc work_args work_item $ - mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs - - ; if null eqs_for_me - then tryFDEqns fam_tc work_args work_item $ - mkTopOpenFamEqFDs fam_tc inj_flags work_args work_rhs - else nopStage () } - - | 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 + | otherwise -- Wanted, user-defined type families + = do { -- Note [Do local fundeps before top-level instances] + case tyConInjectivityInfo fam_tc of NotInjective -> nopStage() Injective inj -> tryFDEqns fam_tc work_args work_item $ mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs - -- 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 - ; if null eqs_for_me + ; if all (isWanted . eqCtEvidence) eqs_for_me then tryFDEqns fam_tc work_args work_item $ - mkTopClosedFamEqFDs ax work_args work_rhs + mkTopFamEqFDs fam_tc work_args work_rhs else nopStage () } - | otherwise -- Data families, abstract families - = nopStage () +mkTopFamEqFDs :: TyCon -> [TcType] -> Xi -> TcS [FunDepEqns] +mkTopFamEqFDs fam_tc work_args work_rhs + | isOpenTypeFamilyTyCon fam_tc + , Injective inj_flags <- tyConInjectivityInfo fam_tc + = -- Open, injective type families + mkTopOpenFamEqFDs fam_tc inj_flags work_args work_rhs + + | Just ax <- isClosedFamilyTyCon_maybe fam_tc + = -- Closed 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 + mkTopClosedFamEqFDs ax work_args work_rhs + + | otherwise + = -- Data families, abstract families, + -- open families that are not injective, + -- closed type families with no equations (isClosedFamilyTyCon_maybe returns Nothing) + return [] tryFDEqns :: TyCon -> [TcType] -> EqCt -> TcS [FunDepEqns] -> SolverStage () tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eqns @@ -542,6 +543,8 @@ tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eq ----------------------------------------- mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> Xi -> TcS [FunDepEqns] mkTopClosedFamEqFDs ax work_args work_rhs + | Just tc <- tyConAppTyCon_maybe work_rhs -- Does RHS have anything useful to say? + , isGenerativeTyCon tc Nominal = do { let branches = fromBranches (coAxiomBranches ax) ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs) ; case getRelevantBranches ax work_args work_rhs of @@ -549,6 +552,8 @@ mkTopClosedFamEqFDs ax work_args work_rhs -> return [FDEqns { fd_qtvs = qtvs , fd_eqs = zipWith Pair (rhs_ty:lhs_tys) (work_rhs:work_args) }] _ -> return [] } + | otherwise + = return [] getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [CoAxBranch] @@ -727,12 +732,14 @@ mkInjectivityFDEqn inj_args qtvs lhs_args rhs_args | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ] getInertFamEqsFor :: TyCon -> [TcType] -> Xi -> TcS [EqCt] --- Returns a mixture of Given and Wanted -- Look in the InertSet, and return all inert equalities -- F tys ~N# rhs -- where F is the specified TyCon --- But filter out ones that can't possibly help, is apart from the Wanted --- Representational equalities don't interact with type family dependencies +-- But filter out ones that can't possibly help; +-- that is, ones that are "apart" from the Wanted +-- Returns a mixture of Given and Wanted +-- Nominal only, becaues Representational equalities don't interact +-- with type family dependencies getInertFamEqsFor fam_tc work_args work_rhs = do { IC {inert_funeqs = funeqs } <- getInertCans ; return [ funeq_ct | equal_ct_list <- findFunEqsByTyCon funeqs fam_tc View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b8821d43e28488206daff9db6fb13e1f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b8821d43e28488206daff9db6fb13e1f... You're receiving this email because of your account on gitlab.haskell.org.