Simon Peyton Jones pushed to branch wip/T26346 at Glasgow Haskell Compiler / GHC Commits: 2aab6148 by Simon Peyton Jones at 2025-08-27T00:20:42+01:00 Nearly there [skip ci] ... traces in Unify, test failing T5490... extend2 is bad - - - - - 2 changed files: - compiler/GHC/Core/TyCo/Compare.hs - compiler/GHC/Core/Unify.hs Changes: ===================================== compiler/GHC/Core/TyCo/Compare.hs ===================================== @@ -229,6 +229,8 @@ tcEqTyConApps tc1 args1 tc2 args2 = tc1 == tc2 && tcEqTyConAppArgs args1 args2 tcEqTyConAppArgs :: [Type] -> [Type] -> Bool +-- Args do not have to have equal length; +-- we discard the excess of the longer one tcEqTyConAppArgs args1 args2 = and (zipWith tcEqTypeNoKindCheck args1 args2) -- No kind check necessary: if both arguments are well typed, then ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -1792,7 +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 - ; 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. @@ -1903,7 +1908,8 @@ uVarOrFam env ty1 ty2 kco | BindMe <- um_bind_fam_fun env tc1 tys1 rhs = if uOccursCheck substs lhs rhs then maybeApart MARInfinite - else do { extendFamEnv tc1 tys1 rhs -- We don't substitue tys1; see (ATF13) + else do { pprTrace "extend1" (ppr tc1 <+> ppr tys1 $$ ppr rhs) $ + extendFamEnv tc1 tys1 rhs -- We don't substitue tys1; see (ATF13) ; maybeApart MARTypeFamily } -- Swap in case of (F a b) ~ (G c d e) @@ -1947,10 +1953,12 @@ uVarOrFam env ty1 ty2 kco | 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 - = extendFamEnv tc tys1 rhs1 + = pprTrace "extend2" (ppr tc <+> ppr tys1 $$ ppr rhs1) $ + extendFamEnv tc tys1 rhs1 | um_unif env , BindMe <- um_bind_fam_fun env tc tys2 rhs2 - = extendFamEnv tc tys2 rhs2 + = pprTrace "extend3" (ppr tc <+> ppr tys2 $$ ppr rhs2) $ + extendFamEnv tc tys2 rhs2 | otherwise = return () @@ -1965,7 +1973,8 @@ uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) lhs ty where go :: TyCoVarSet -- Bound by enclosing foralls -> Type -> Bool - go bvs ty | Just ty' <- coreView ty = go bvs ty' + go bvs ty | Just ty' <- pprTrace "uOccursCheck:go" (ppr lhs $$ ppr ty) $ + coreView ty = go bvs ty' go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv = go bvs ty' | TyVarLHS tv' <- lhs, tv==tv' @@ -1990,12 +1999,13 @@ 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) - = go bvs ty' || any (go bvs) (drop arity tys) + = pprTrace "lookup" (ppr tc <+> ppr tys $$ ppr ty') $ + go bvs ty' || any (go bvs) (drop arity tys) | TyFamLHS tc' tys' <- lhs , tc == tc' , tys `lengthAtLeast` arity -- Saturated, or over-saturated - , and (zipWith tcEqType tys tys') + , tcEqTyConAppArgs tys tys' = True | otherwise @@ -2158,6 +2168,7 @@ 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/2aab6148fcf032d80b8f7e075bfa54ec... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2aab6148fcf032d80b8f7e075bfa54ec... You're receiving this email because of your account on gitlab.haskell.org.