[Git][ghc/ghc][wip/T26346] I think this works now

27 Aug 2025

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.

    

Simon Peyton Jones (＠simonpj)

tags

participants (1)