Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: 1783c632 by Simon Peyton Jones at 2025-11-14T15:43:23+00:00 Solve Yikes1 and Yikes2 - - - - - 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 ===================================== @@ -609,9 +609,7 @@ injectiveBranches injectivity ax1@(CoAxBranch { cab_tvs = tvs1, cab_lhs = lhs1, cab_rhs = rhs1 }) ax2@(CoAxBranch { cab_tvs = tvs2, cab_lhs = lhs2, cab_rhs = rhs2 }) -- See Note [Verifying injectivity annotation], case 1. - = let getInjArgs = filterByList injectivity - in_scope = mkInScopeSetList (tvs1 ++ tvs2) - in case tcUnifyTysForInjectivity True in_scope [rhs1] [rhs2] of + = case tcUnifyTysForInjectivity True [rhs1] [rhs2] of -- True = two-way pre-unification Nothing -> InjectivityAccepted -- RHS are different, so equations are injective. @@ -633,6 +631,7 @@ injectiveBranches injectivity -- Payload of InjectivityUnified used only for check 1B2, only -- for closed type families where + getInjArgs = filterByList injectivity lhs1Subst = Type.substTys subst (getInjArgs lhs1) lhs2Subst = Type.substTys subst (getInjArgs lhs2) ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -818,14 +818,13 @@ 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 -> 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. -tcUnifyTysForInjectivity unif in_scope tys1 tys2 +tcUnifyTysForInjectivity unif tys1 tys2 = case tc_unify_tys alwaysBindFam alwaysBindTv unif -- Am I unifying? True -- Do injectivity checks @@ -840,6 +839,10 @@ tcUnifyTysForInjectivity unif in_scope tys1 tys2 SurelyApart -> Nothing where rn_env = mkRnEnv2 in_scope + in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2) + -- The types we are unifying never contain foralls, so the + -- in-scope set is never looked at, so this free-var stuff + -- should never actually be done maybe_fix | unif = niFixSubst in_scope | otherwise = mkTvSubst in_scope -- when matching, don't confuse ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -31,14 +31,13 @@ import GHC.Core.TyCo.Subst( elemSubst ) import GHC.Builtin.Types.Literals( tryInteractTopFam, tryInteractInertFam ) -import GHC.Types.Var.Env import GHC.Types.Var.Set import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Data.Pair -import Data.Maybe( mapMaybe ) +import Data.Maybe( isNothing, mapMaybe ) {- Note [Overview of functional dependencies in type inference] @@ -546,34 +545,30 @@ mkTopClosedFamEqFDs ax work_args work_rhs = do { let branches = fromBranches (coAxiomBranches ax) ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs) ; case getRelevantBranches ax work_args work_rhs of - [CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys }] + [CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty }] -> return [FDEqns { fd_qtvs = qtvs - , fd_eqs = zipWith Pair lhs_tys work_args }] + , fd_eqs = zipWith Pair (rhs_ty:lhs_tys) (work_rhs:work_args) }] _ -> return [] } + +getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [CoAxBranch] getRelevantBranches ax work_args work_rhs = go [] (fromBranches (coAxiomBranches ax)) where 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 + go _ [] = [] + go preceding (branch:branches) + | is_relevant branch = branch : go (branch:preceding) branches + | otherwise = go (branch:preceding) branches + where + is_relevant (CoAxBranch { cab_lhs = lhs_tys, cab_rhs = rhs_ty }) + = case tcUnifyTysForInjectivity True work_tys (rhs_ty:lhs_tys) of + Nothing -> False + Just subst -> all (no_match (substTys subst lhs_tys)) preceding - no_match lhs_tys [] = True - no_match lhs_tys (CoAxBranch { cab_qtvs = qtvs1, cab_lhs = lhs_tys1 }) + no_match lhs_tys (CoAxBranch { 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) @@ -588,8 +583,7 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args work_rhs do_one branch@(CoAxBranch { cab_tvs = branch_tvs , cab_lhs = branch_lhs_tys , cab_rhs = branch_rhs }) - | let in_scope1 = in_scope `extendInScopeSetList` branch_tvs - , Just subst <- tcUnifyTyForInjectivity False in_scope1 branch_rhs work_rhs + | Just subst <- tcUnifyTysForInjectivity False [branch_rhs] [work_rhs] -- False: matching, not unifying , let (subst', qtvs) = trim_qtvs subst branch_tvs branch_lhs_tys' = substTys subst' branch_lhs_tys @@ -599,8 +593,6 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args work_rhs | otherwise = Nothing - in_scope = mkInScopeSet (tyCoVarsOfType work_rhs) - trim_qtvs :: Subst -> [TcTyVar] -> (Subst,[TcTyVar]) -- Tricky stuff: see (TIF1) in -- Note [Type inference for type families with injectivity] View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1783c632468a58f03670da6c59154a8a... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1783c632468a58f03670da6c59154a8a... You're receiving this email because of your account on gitlab.haskell.org.