Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC Commits: b9431ef2 by Simon Peyton Jones at 2026-09-24T15:42:33+01:00 Add cab_overlaps Needs some documentation; fixes bug discovered by Fable - - - - - 8 changed files: - changelog.d/T27828 - compiler/GHC/Builtin/WiredIn/Types/Box.hs - compiler/GHC/Core/Coercion/Axiom.hs - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/TyCl.hs - testsuite/tests/indexed-types/should_compile/all.T Changes: ===================================== changelog.d/T27828 ===================================== @@ -4,5 +4,5 @@ issues: #27828 mrs: !16714 description: { - There was a bug in the implemenation of functional dependencies for type families. + There was a bug in the implementation of functional dependencies for type families. } ===================================== compiler/GHC/Builtin/WiredIn/Types/Box.hs ===================================== @@ -329,7 +329,8 @@ mkWiredInNewTyCon tc_name dc_name nt_co_uniq bndrs roles nt_fld_ty = , cab_roles = roles , cab_lhs = mkTyVarTys tvs , cab_rhs = nt_fld_ty - , cab_incomps = [] } + , cab_overlaps = [] + , cab_incomps = [] } -- | The wired-in @Box@ newtype: -- ===================================== compiler/GHC/Core/Coercion/Axiom.hs ===================================== @@ -18,7 +18,7 @@ module GHC.Core.Coercion.Axiom ( coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars, coAxBranchRoles, coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps, - placeHolderIncomps, + placeHolderIncomps, placeHolderOverlaps, Role(..), @@ -275,8 +275,15 @@ data CoAxBranch , cab_rhs :: Type -- ^ Right-hand side of the equality -- See Note [CoAxioms are homogeneous] + + , cab_overlaps :: [CoAxBranch] + -- ^ The preceding branches whose LHSs are /unify with/ this one + -- Order is unimportant + -- See Note [Storing compatibility] + , cab_incomps :: [CoAxBranch] - -- ^ The previous incompatible branches + -- ^ The preceding branches that are /incompatible/ with this one + -- Order is unimportant -- See Note [Storing compatibility] } deriving Data.Data @@ -349,8 +356,9 @@ coAxBranchIncomps :: CoAxBranch -> [CoAxBranch] coAxBranchIncomps = cab_incomps -- See Note [Compatibility] in GHC.Core.FamInstEnv -placeHolderIncomps :: [CoAxBranch] -placeHolderIncomps = panic "placeHolderIncomps" +placeHolderIncomps, placeHolderOverlaps :: [CoAxBranch] +placeHolderIncomps = panic "placeHolderIncomps" +placeHolderOverlaps = panic "placeHolderOverlaps" {- Note [CoAxBranch type variables] ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -487,22 +487,45 @@ in GHC.Core.Unify.) Note [Compatibility] ~~~~~~~~~~~~~~~~~~~~ -Two patterns are /compatible/ if either of the following conditions hold: +Consider a closed type family with two equations (X1) and (X2) + type family F a where + F lhs1 = rhs1 -- (X1) + ... + F lhs2 = rhs2 -- (X2) + ... +Then equations (X1) and (X2) are /compatible/ if any target (F ty) that +matches both equations yields the very same right hand side. Example: + And True True = True + And a True = a +The target (And True True) matches both equations but they then both +produce the same reduct True. + +More precisely (X1) and (X2) are /compatible/ iff + If LHSs unify with a substitution S, then S(rhs1) = S(rhs2) + +Conversely, (X1) and (X2) are /incompatible/ if + Their LHSs unify with S, and S(rhs1) /= S(rhs2) - 1) The patterns are apart. +For open type families, only compatible instances are allowed. For closed +families, we use the Closed Family Matching Rule (see function `findBranch`): - 2) The patterns unify with a substitution S, and their right hand sides - are equal under that substitution. + When looking up a target (F ty) in a closed type family F, + find an equation (branch) such that: + * the LHS matches the target + * the target is apart from every previous /incompatible/ equation for F -For open type families, only compatible instances are allowed. For closed -type families, the story is slightly more complicated. Consider the following: +We don't need to check the earlier equations that are compatible with the +matching equation, because they are either irrelevant (clause 1 of compatible) +or benign (clause 2 of compatible). + +Some examples: -type family F a where - F Int = Bool - F a = Int + type family F a where + F Int = Bool + F a = Int -g :: Show a => a -> F a -g x = length (show x) + g :: Show a => a -> F a + g x = length (show x) Should that type-check? No. We need to allow for the possibility that 'a' might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int @@ -518,12 +541,12 @@ potentially-overlapping group is closed. As another example, consider this: -type family G x where - G Int = Bool - G a = Double + type family G x where + G Int = Bool + G a = Double -type family H y --- no instances + type family H y + -- no instances Now, we want to simplify (G (H Char)). We can't, because (H Char) might later simplify to be Int. So, (G (H Char)) is stuck, for now. @@ -531,18 +554,13 @@ simplify to be Int. So, (G (H Char)) is stuck, for now. While everything above is quite sound, it isn't as expressive as we'd like. Consider this: -type family J a where - J Int = Int - J a = a + type family J a where + J Int = Int + J a = a Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if b is instantiated with Int, but the RHSs coincide there, so it's all OK. - -So, the rule is this: when looking up a branch in a closed type family, we -find a branch that matches the target, but then we make sure that the target -is apart from every previous *incompatible* branch. We don't check the -branches that are compatible with the matching branch, because they are either -irrelevant (clause 1 of compatible) or benign (clause 2 of compatible). +Hence the Closed Family Matching Rule. Note [Compatibility of eta-reduced axioms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -574,15 +592,30 @@ fails anyway. -- See Note [Compatibility] compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool -compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) - (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) +compatibleBranches b1 b2 + = case compareBranches b1 b2 of + BC_Apart -> True + BC_Compat -> True + BC_Incompat -> False + +data BranchCompatibility + = BC_Apart -- LHSs are apart + | BC_Compat -- LHSs unify with S, and S(rhs1)=S(rhs2) + | BC_Incompat -- LHSs unify with S, and S(rhs1)/=S(rhs2) + +compareBranches :: CoAxBranch -> CoAxBranch -> BranchCompatibility +compareBranches b1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 }) + b2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 }) = case tcUnifyTysFG alwaysBindFam alwaysBindTv commonlhs1 commonlhs2 of -- Here we need the cab_tvs of the two branches to be disinct. -- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom. - SurelyApart -> True - MaybeApart {} -> False - Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType` + SurelyApart -> BC_Apart + MaybeApart {} -> pprPanic "compareBranches" (ppr b1 $$ ppr b2) + Unifiable subst | Type.substTyAddInScope subst rhs1 `eqType` Type.substTyAddInScope subst rhs2 + -> BC_Compat + | otherwise + -> BC_Incompat where (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2 -- See Note [Compatibility of eta-reduced axioms] @@ -630,10 +663,10 @@ injectiveBranches injectivity lhs1Subst = Type.substTys subst (getInjArgs lhs1) lhs2Subst = Type.substTys subst (getInjArgs lhs2) --- takes a CoAxiom with unknown branch incompatibilities and computes --- the compatibilities --- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch] +-- Takes a CoAxiom for a closed type family with place-holder +-- `cab_incomps` and `cab_overlaps` fields, and computes those fields +-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom computeAxiomIncomps branches = snd (mapAccumL go [] branches) where @@ -641,11 +674,23 @@ computeAxiomIncomps branches go prev_brs cur_br = (new_br : prev_brs, new_br) where - new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br } - - mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch] - mk_incomps prev_brs cur_br - = filter (not . compatibleBranches cur_br) prev_brs + (overlaps,incomps) = get_cab [] [] prev_brs + new_br = cur_br { cab_overlaps = overlaps, cab_incomps = incomps } + + get_cab :: [CoAxBranch] -> [CoAxBranch] -- Accumulators + -> [CoAxBranch] + -> ([CoAxBranch], [CoAxBranch]) + get_cab overlaps incomps [] = (overlaps,incomps) + get_cab overlaps incomps (br:brs) + = case compareBranches cur_br br of + BC_Apart -> get_cab overlaps incomps brs + BC_Compat -> get_cab (br:overlaps) incomps brs + BC_Incompat -> get_cab (br:overlaps) (br:incomps) brs + +noAxiomIncomps :: CoAxBranch -> CoAxBranch +-- Overwrite the placeholders for `cab_incomps` and `cab_overlaps` +-- with [], because unbranched axioms have no "preceding" equations +noAxiomIncomps branch = branch { cab_incomps = [], cab_overlaps = [] } {- ************************************************************************ @@ -716,14 +761,15 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars -> SrcSpan -> CoAxBranch mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc - = CoAxBranch { cab_tvs = tvs' - , cab_eta_tvs = eta_tvs' - , cab_cvs = cvs' - , cab_lhs = tidyTypes env lhs - , cab_roles = roles - , cab_rhs = tidyType env rhs - , cab_loc = loc - , cab_incomps = placeHolderIncomps } + = CoAxBranch { cab_tvs = tvs' + , cab_eta_tvs = eta_tvs' + , cab_cvs = cvs' + , cab_lhs = tidyTypes env lhs + , cab_roles = roles + , cab_rhs = tidyType env rhs + , cab_loc = loc + , cab_overlaps = placeHolderOverlaps + , cab_incomps = placeHolderIncomps } where (env1, tvs') = tidyVarBndrs init_tidy_env tvs (env2, eta_tvs') = tidyVarBndrs env1 eta_tvs @@ -737,12 +783,12 @@ mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc -- all of the following code is here to avoid mutual dependencies with -- Coercion -mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched -mkBranchedCoAxiom ax_name fam_tc branches +mkBranchedCoAxiom :: Role -> Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched +mkBranchedCoAxiom role ax_name fam_tc branches = CoAxiom { co_ax_unique = nameUnique ax_name , co_ax_name = ax_name , co_ax_tc = fam_tc - , co_ax_role = Nominal + , co_ax_role = role , co_ax_implicit = False , co_ax_branches = manyBranches (computeAxiomIncomps branches) } @@ -753,7 +799,7 @@ mkUnbranchedCoAxiom ax_name fam_tc branch , co_ax_tc = fam_tc , co_ax_role = Nominal , co_ax_implicit = False - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } mkSingleCoAxiom :: Role -> Name -> [TyVar] -> [TyVar] -> [CoVar] @@ -768,7 +814,7 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty , co_ax_tc = fam_tc , co_ax_role = role , co_ax_implicit = False - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } where branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty (map (const Nominal) tvs) @@ -786,7 +832,7 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty , co_ax_implicit = True -- See Note [Implicit axioms] in GHC.Core.TyCon , co_ax_role = Representational , co_ax_tc = tycon - , co_ax_branches = unbranched (branch { cab_incomps = [] }) } + , co_ax_branches = unbranched (noAxiomIncomps branch) } where branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty roles (getSrcSpan name) @@ -1224,7 +1270,9 @@ findBranch :: Array BranchIndex CoAxBranch -> Maybe (BranchIndex, [Type], [Coercion]) -- coercions relate requested types to returned axiom LHS at role N findBranch branches target_tys - = foldr go Nothing (assocs branches) + = -- Implements the Closed Family Matching Rule + -- in Note [Compatibility] + foldr go Nothing (assocs branches) where go :: (BranchIndex, CoAxBranch) -> Maybe (BranchIndex, [Type], [Coercion]) @@ -1264,8 +1312,8 @@ noEarlierMatchCheck :: [Type] -> CoAxBranch -- ^ The candidate equation we wish to use -> Bool -- ^ True <=> equation can fire -noEarlierMatchCheck target (CoAxBranch { cab_incomps = incomps }) - = not (any matches incomps) +noEarlierMatchCheck target (CoAxBranch { cab_overlaps = overlaps }) + = not (any matches overlaps) where matches earlier_branch = isJust (tcMatchTys (coAxBranchLHS earlier_branch) target) ===================================== compiler/GHC/IfaceToCore.hs ===================================== @@ -903,12 +903,7 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc -- See #13803 ; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name) $ tc_ax_branches branches - ; let axiom = CoAxiom { co_ax_unique = nameUnique tc_name - , co_ax_name = tc_name - , co_ax_tc = tc_tycon - , co_ax_role = role - , co_ax_branches = manyBranches tc_branches - , co_ax_implicit = False } + ; let axiom = mkBranchedCoAxiom role tc_name tc_tycon tc_branches ; return (ACoAxiom axiom) } tc_iface_decl _ _ (IfacePatSyn{ ifName = name @@ -1124,7 +1119,7 @@ tc_ax_branch prev_branches , ifaxbEtaTyVars = eta_tv_bndrs , ifaxbCoVars = cv_bndrs , ifaxbLHS = lhs, ifaxbRHS = rhs - , ifaxbRoles = roles, ifaxbIncomps = incomps }) + , ifaxbRoles = roles, ifaxbIncomps = _incomps }) = bindIfaceTyConBinders_AT (map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs -> -- The _AT variant is needed here; see Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom @@ -1135,14 +1130,15 @@ tc_ax_branch prev_branches ; this_mod <- getIfModule ; let loc = mkGeneralSrcSpan (fsLit "module " `appendFS` moduleNameFS (moduleName this_mod)) - br = CoAxBranch { cab_loc = loc - , cab_tvs = binderVars tvs - , cab_eta_tvs = eta_tvs - , cab_cvs = cvs - , cab_lhs = tc_lhs - , cab_roles = roles - , cab_rhs = tc_rhs - , cab_incomps = map (prev_branches `getNth`) incomps } + br = CoAxBranch { cab_loc = loc + , cab_tvs = binderVars tvs + , cab_eta_tvs = eta_tvs + , cab_cvs = cvs + , cab_lhs = tc_lhs + , cab_roles = roles + , cab_rhs = tc_rhs + , cab_overlaps = placeHolderOverlaps + , cab_incomps = placeHolderIncomps } ; return (prev_branches ++ [br]) } tcIfaceDataCons :: Name -> TyCon -> IfaceConDecls -> IfL AlgTyConRhs ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -1047,7 +1047,7 @@ Note [Exploiting closed type families]. You might think that (B3) could be instantiated to Bak Char ~ Char; but actually that instantiation will never fire because (B2) Bak Char ~ Int would fire first. So the only way to return a Char is via (B1); so we - can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B2) is relevant. + can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B1) is relevant. That is the reason for condition (R2) in the definition of Relevance above. A watertight proof that this is the Right Thing is not very easy. See more @@ -1072,6 +1072,23 @@ Note [Exploiting closed type families]. TMessage @SC @Req alpha and equation (T1) does not match that. (It does unify, but we don't care.) +(RW5) `noEarlierMatchCheck`: in (RW4) We really do need to check that /no/ + earlier equation matches, not just no earlier /incompatible/ equation + matches. Consider T27282a: + type family F a where + F Int = Int -- B1 + F Char = Bool -- B2 + F a = a -- B3 + + [W] F alpha ~ Int + + (B1) is relevant, and (B2) is not. What about (B3)? It pre-unifies with + the Wanted via [alpha :-> Int, a :-> Int]. But under that substitution + (B1) would fire, so (B3) is not relevant. + + And yet, (B1) is /compatible/ with (B3), so it's no good just looking at + the `cab_incomps` of (B3). Instead we look at `cab_overlaps`. + Note [Exploiting open type families] see `mkTopOpenFamEqFDs` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Generating fundeps from a top-level type instance is covered in Section 5.2 in @@ -1451,6 +1468,8 @@ solveFunDeps work_ev fd_eqns ; uPairsTcM uenv eqs } instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn] +-- See GHC.Tc.Instance.Fundeps Note [Improving against instances] +-- Wrinkle (IMP1) instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }) | null qtvs = return rev_eqs @@ -1463,11 +1482,9 @@ instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }) -- (reverse eqs): See Note [Reverse order of fundep equations] subst_pair subst (Pair ty1 ty2) - = Pair (substTy subst' ty1) (substTy subst' ty2) --- ToDo not correct! + = Pair (substTy subst' ty1) ty2 -- ty2 does not mention fd_qtvs, so no need to subst it. - -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] - -- Wrinkle (IMP1) + -- See invariant on `fv_eqs` in `data FunDepEqns`. where subst' = extendSubstInScopeSet subst (tyCoVarsOfTypes [ty1,ty2]) -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result ===================================== compiler/GHC/Tc/TyCl.hs ===================================== @@ -3462,7 +3462,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info ; let mb_co_ax | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list - | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches) + | otherwise = Just (mkBranchedCoAxiom Nominal co_ax_name fam_tc branches) fam_tc = mkFamilyTyCon tc_name kind tc_bndrs 0 res_kind (resultVariableName sig) (ClosedTypeFamilyTyCon $ CTF mb_co_ax) parent inj' ===================================== testsuite/tests/indexed-types/should_compile/all.T ===================================== @@ -317,3 +317,4 @@ test('T25611c', normal, compile, ['']) test('T25611d', normal, compile, ['']) test('T25657', normal, compile, ['']) test('T27828', normal, compile, ['']) +test('T27828a', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b9431ef21af13163fdfde045cd1f5008... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b9431ef21af13163fdfde045cd1f5008... You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help