Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: 827aaf71 by Simon Peyton Jones at 2025-11-13T17:32:23+00:00 WIP [skip ci] improving the injectivity calculation - - - - - 3 changed files: - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Tc/Solver/FunDeps.hs Changes: ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -611,7 +611,7 @@ injectiveBranches injectivity -- See Note [Verifying injectivity annotation], case 1. = let getInjArgs = filterByList injectivity in_scope = mkInScopeSetList (tvs1 ++ tvs2) - in case tcUnifyTyForInjectivity True in_scope rhs1 rhs2 of + in case tcUnifyTysForInjectivity True in_scope [rhs1] [rhs2] of -- True = two-way pre-unification Nothing -> InjectivityAccepted -- RHS are different, so equations are injective. ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -12,7 +12,7 @@ module GHC.Core.Unify ( -- Side-effect free unification tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger, - tcUnifyTysFG, tcUnifyTyForInjectivity, + tcUnifyTysFG, tcUnifyTysForInjectivity, BindTvFun, BindFamFun, BindFlag(..), matchBindTv, alwaysBindTv, alwaysBindFam, dontCareBindFam, UnifyResult, UnifyResultM(..), MaybeApartReason(..), @@ -381,7 +381,7 @@ Wrinkles (ATF7) There is one other, very special case of matching where we /do/ want to bind type families in `um_fam_env`, namely in GHC.Tc.Solver.Equality, the call - to `tcUnifyTyForInjectivity False` in `improve_injective_wanted_top`. + to `tcUnifyTysForInjectivity False` in `improve_injective_wanted_top`. Consider of a match. Consider type family G6 a = r | r -> a @@ -814,25 +814,25 @@ tcUnifyFunDeps qtvs tys1 tys2 -- | Unify or match a type-family RHS with a type (possibly another type-family RHS) -- Precondition: kinds are the same -tcUnifyTyForInjectivity +tcUnifyTysForInjectivity :: AmIUnifying -- ^ True <=> do two-way unification; -- False <=> do one-way matching. -- See end of sec 5.2 from the paper -> InScopeSet -- Should include the free tyvars of both Type args - -> Type -> Type -- Types to unify + -> [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. -tcUnifyTyForInjectivity unif in_scope t1 t2 +tcUnifyTysForInjectivity unif in_scope tys1 tys2 = case tc_unify_tys alwaysBindFam alwaysBindTv unif -- Am I unifying? True -- Do injectivity checks False -- Don't check outermost kinds RespectMultiplicities rn_env emptyTvSubstEnv emptyCvSubstEnv - [t1] [t2] of + tys1 tys2 of Unifiable (tv_subst, _cv_subst) -> Just $ maybe_fix tv_subst MaybeApart _reason (tv_subst, _cv_subst) -> Just $ maybe_fix tv_subst -- We want to *succeed* in questionable cases. ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -25,7 +25,7 @@ import GHC.Core.FamInstEnv import GHC.Core.Coercion import GHC.Core.Predicate( EqRel(..) ) import GHC.Core.TyCon -import GHC.Core.Unify( tcUnifyTyForInjectivity, typeListsAreApart ) +import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart ) import GHC.Core.Coercion.Axiom import GHC.Core.TyCo.Subst( elemSubst ) @@ -545,14 +545,35 @@ mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> Xi -> TcS [FunDepEqns] mkTopClosedFamEqFDs ax work_args work_rhs = do { let branches = fromBranches (coAxiomBranches ax) ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs) - ; case filter relevant_branch branches of - [CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys }] + ; case getRelevantBranches ax work_args work_rhs of + [CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys }] -> return [FDEqns { fd_qtvs = qtvs , fd_eqs = zipWith Pair lhs_tys work_args }] _ -> return [] } + +getRelevantBranches ax work_args work_rhs + = go [] (fromBranches (coAxiomBranches ax)) where - relevant_branch (CoAxBranch { cab_lhs = lhs_tys, cab_rhs = rhs_ty }) - = eqnIsRelevant lhs_tys rhs_ty work_args work_rhs + work_tys = work_rhs : work_args + work_fvs = tyCoVarsOfTypes work_tys + + go preceding [] = [] + go preceding (CoAxBranch { cab_qtvs = qtvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty } : rest) + | is_relevant = br : go (br:preceding) rest + | otherwise = go (br:preceding) rest + where + is_relevant = case tcUnifyTysForInjectivity True branch_fvs work_tys (rhs_ty:lhs_tys) of + Nothing -> False + Just subst -> no_match (substTy subst lhs_tys) preceding + + branch_fvs = extendVarSetList work_fvs qtvs + + no_match lhs_tys [] = True + no_match lhs_tys (CoAxBranch { cab_qtvs = qtvs1, cab_lhs = lhs_tys1 }) + = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys) + where + all_fvs = branch_fvs `extendVarSetList` qtvs1 + mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> Xi -> TcS [FunDepEqns] -- Implements (INJFAM:Wanted/top) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/827aaf71386a685c00ff5dcaaa975549... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/827aaf71386a685c00ff5dcaaa975549... You're receiving this email because of your account on gitlab.haskell.org.