Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: c5b6e511 by Simon Peyton Jones at 2025-12-28T23:41:16+00:00 Wibble to (CF5) - - - - - 1 changed file: - compiler/GHC/Tc/Solver/FunDeps.hs Changes: ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -23,7 +23,7 @@ import GHC.Tc.Types.Constraint import GHC.Core.FamInstEnv import GHC.Core.Coercion -import GHC.Core.Type( tyConAppTyCon_maybe ) +import GHC.Core.TyCo.Rep( Type(..) ) import GHC.Core.Predicate( EqRel(..) ) import GHC.Core.TyCon import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart ) @@ -634,8 +634,7 @@ mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunD -- type families without injectivity info -- See Note [Exploiting closed type families] mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) - | Just tc <- tyConAppTyCon_maybe work_rhs - , isGenerativeTyCon tc Nominal -- See (CF5) in Note [Exploiting closed type families] + | isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families] = Stage $ do { let branches = fromBranches (coAxiomBranches ax) ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs) @@ -646,6 +645,20 @@ mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) | otherwise = Stage $ continueWith [] +isGenerativeType :: Type -> Bool +-- True <=> This type cannot rewrite to, or be substituted to, +-- a saturated type-family application +-- See (CF5) in Note [Exploiting closed type families] +isGenerativeType ty | Just ty' <- coreView ty = isGenerativeType ty' +isGenerativeType (FunTy {}) = True +isGenerativeType (CastTy ty _) = isGenerativeType ty +isGenerativeType (ForAllTy {}) = True +isGenerativeType (TyConApp tc _) = isGenerativeTyCon tc Nominal +isGenerativeType (AppTy {}) = True +isGenerativeType (LitTy {}) = True +isGenerativeType (TyVarTy {}) = False +isGenerativeType (CoercionTy {}) = False + hasRelevantGiven :: [EqCt] -> [TcType] -> EqCt -> Bool -- See (CF1) in Note [Exploiting closed type families] -- A Given is relevant if it is not apart from the Wanted @@ -1121,30 +1134,34 @@ Key point: equations that are not relevant do not need to be considered for fund improvement in general. (CF5) Consider - type family F a where - F (Just x) = Int + type family F a where + F (Just x) = Int - [W] F alpha ~ F (G beta) - [W] alpha ~ G beta + [W] F alpha ~ F (G beta) + [W] alpha ~ G beta We can solve both Wanteds by `alpha := G beta`. But if we use fundeps on the first Wanted, we see that there is just one relevant equation, so we'll emit - [W] alpha ~ Just gamma - [W] F (G beta) ~ Int + [W] alpha ~ Just gamma + [W] F (G beta) ~ Int and try to solve them. We'll do `alpha := Just gamma`, and then it's game over; we end up with these constraints that we can't solve - [W] Just gamma ~ F (G beta) - [W] Just gamma ~ G beta + [W] Just gamma ~ F (G beta) + [W] Just gamma ~ G beta This actually happens when compiling the libarary `type-rows`, in Data.Row.Variants. Even if there is only one relevant equation, we can only use it /if/ we are sure that we cannot solve the current Wanted by reflexivity; that is, if we must do a type-family reduction to solve it. So if the Wanted is - ``` - [W] F tys ~ rhs - ``` + [W] F tys ~ rhs we must be sure that `rhs` can't turn into `F tys`. The only way to be sure of that - is if `rhs` is headed by a generative type constructor. See the test for - `isGenerativeTyCon` in `mkTopClosedFamEqFDs`. + is if `rhs` is headed by a generative type constructor. See `isGenerativeType`. + + It's important for `isGenerativeType` to look through casts. Consider T13822 + type I :: Ty k -> IK k + type family I t = res | res -> t where + I TInt = Int |> g -- where g :: Type ~# IK k + and [W] I alpha ~ Int |> g2 + Here we definiteily want to take advantage of injectivity. Note [Cache-caused loops] ~~~~~~~~~~~~~~~~~~~~~~~~~ View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c5b6e51164139edfd5c9460646cb3d4f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c5b6e51164139edfd5c9460646cb3d4f... You're receiving this email because of your account on gitlab.haskell.org.