Simon Peyton Jones pushed to branch wip/T26346 at Glasgow Haskell Compiler / GHC Commits: 632594f5 by Simon Peyton Jones at 2025-08-27T10:17:57+01:00 I think this works now - - - - - 1 changed file: - compiler/GHC/Core/Unify.hs Changes: ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -1792,12 +1792,12 @@ uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM () -- Why saturated? See (ATF4) in Note [Apartness and type families] uVarOrFam env ty1 ty2 kco = do { substs <- getSubstEnvs - ; pprTrace "uVarOrFam" (vcat - [ text "ty1" <+> ppr ty1 - , text "ty2" <+> ppr ty2 - , text "tv_env" <+> ppr (um_tv_env substs) - , text "fam_env" <+> ppr (um_fam_env substs) ]) $ - go NotSwapped substs ty1 ty2 kco } +-- ; pprTrace "uVarOrFam" (vcat +-- [ text "ty1" <+> ppr ty1 +-- , text "ty2" <+> ppr ty2 +-- , text "tv_env" <+> ppr (um_tv_env substs) +-- , text "fam_env" <+> ppr (um_fam_env substs) ]) $ + ; go NotSwapped substs ty1 ty2 kco } where -- `go` takes two bites at the cherry; if the first one fails -- it swaps the arguments and tries again; and then it fails. @@ -1901,15 +1901,14 @@ uVarOrFam env ty1 ty2 kco -- Check for equality F tys1 ~ F tys2 | Just (tc2, tys2) <- isSatFamApp ty2 , tc1 == tc2 - = go_fam_fam tc1 tys1 tys2 kco + = go_fam_fam substs tc1 tys1 tys2 kco -- Now check if we can bind the (F tys) to the RHS -- This can happen even when matching: see (ATF7) | BindMe <- um_bind_fam_fun env tc1 tys1 rhs = if uOccursCheck substs lhs rhs then maybeApart MARInfinite - else do { pprTrace "extend1" (ppr tc1 <+> ppr tys1 $$ ppr rhs) $ - extendFamEnv tc1 tys1 rhs -- We don't substitue tys1; see (ATF13) + else do { extendFamEnv tc1 tys1 rhs -- We don't substitue tys1; see (ATF13) ; maybeApart MARTypeFamily } -- Swap in case of (F a b) ~ (G c d e) @@ -1930,7 +1929,7 @@ uVarOrFam env ty1 ty2 kco ----------------------------- -- go_fam_fam: LHS and RHS are both saturated type-family applications, -- for the same type-family F - go_fam_fam tc tys1 tys2 kco + go_fam_fam substs tc tys1 tys2 kco -- Decompose (F tys1 ~ F tys2): (ATF9) -- Use injectivity information of F: (ATF10) -- But first bind the type-fam if poss: (ATF11) @@ -1950,14 +1949,12 @@ uVarOrFam env ty1 ty2 kco bind_fam_if_poss | not (um_unif env) -- Not when matching (ATF11-1) = return () - | tcEqTyConAppArgs tys1 tys2 -- Detect (F tys ~ F tys); - = return () -- otherwise we'd build an infinite substitution | BindMe <- um_bind_fam_fun env tc tys1 rhs1 - = pprTrace "extend2" (ppr tc <+> ppr tys1 $$ ppr rhs1) $ + = unless (uOccursCheck substs (TyFamLHS tc tys1) rhs1) $ extendFamEnv tc tys1 rhs1 - | um_unif env - , BindMe <- um_bind_fam_fun env tc tys2 rhs2 - = pprTrace "extend3" (ppr tc <+> ppr tys2 $$ ppr rhs2) $ + -- At this point um_unif=True, so we can unify either way + | BindMe <- um_bind_fam_fun env tc tys2 rhs2 + = unless (uOccursCheck substs (TyFamLHS tc tys2) rhs2) $ extendFamEnv tc tys2 rhs2 | otherwise = return () @@ -1967,14 +1964,13 @@ uVarOrFam env ty1 ty2 kco uOccursCheck :: UMState -> CanEqLHS -> Type -> Bool --- See Note [The occurs check in the Core unifier] and (ATF13) +-- See Note [The occurs check in the Core unifier] and (ATF14) uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) lhs ty = go emptyVarSet ty where go :: TyCoVarSet -- Bound by enclosing foralls -> Type -> Bool - go bvs ty | Just ty' <- pprTrace "uOccursCheck:go" (ppr lhs $$ ppr ty) $ - coreView ty = go bvs ty' + go bvs ty | Just ty' <- coreView ty = go bvs ty' go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv = go bvs ty' | TyVarLHS tv' <- lhs, tv==tv' @@ -1999,8 +1995,7 @@ uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) lhs ty go_tc bvs tc tys | isTypeFamilyTyCon tc , Just ty' <- lookupFamEnv fam_env tc (take arity tys) - = pprTrace "lookup" (ppr tc <+> ppr tys $$ ppr ty') $ - go bvs ty' || any (go bvs) (drop arity tys) + = go bvs ty' || any (go bvs) (drop arity tys) | TyFamLHS tc' tys' <- lhs , tc == tc' @@ -2168,7 +2163,6 @@ extendCvEnv cv co = UM $ \state -> extendFamEnv :: TyCon -> [Type] -> Type -> UM () extendFamEnv tc tys ty = UM $ \state -> - pprTrace "Adding fam env" (ppr tc <+> ppr tys $$ text ":->" <+> ppr ty) $ Unifiable (state { um_fam_env = extend (um_fam_env state) tc }, ()) where extend :: FamSubstEnv -> TyCon -> FamSubstEnv View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/632594f5764e01658543b3af842c8efb... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/632594f5764e01658543b3af842c8efb... You're receiving this email because of your account on gitlab.haskell.org.