Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: 0b6d14a9 by Simon Peyton Jones at 2025-12-28T14:47:49+00:00 Add (CF5) - - - - - 1 changed file: - compiler/GHC/Tc/Solver/FunDeps.hs Changes: ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -23,6 +23,7 @@ import GHC.Tc.Types.Constraint import GHC.Core.FamInstEnv import GHC.Core.Coercion +import GHC.Core.Type( tyConAppTyCon_maybe ) import GHC.Core.Predicate( EqRel(..) ) import GHC.Core.TyCon import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart ) @@ -633,6 +634,8 @@ 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] = Stage $ do { let branches = fromBranches (coAxiomBranches ax) ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs) @@ -640,6 +643,8 @@ mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) [] -> insolubleFunDep True ev -- See (IFD0) in Note [Insoluble fundeps] [eqn] -> continueWith [eqn] -- If there is just one relevant equation, use it _ -> continueWith [] } + | otherwise + = Stage $ continueWith [] hasRelevantGiven :: [EqCt] -> [TcType] -> EqCt -> Bool -- See (CF1) in Note [Exploiting closed type families] @@ -1115,6 +1120,32 @@ Key point: equations that are not relevant do not need to be considered for fund I was looking at non-termination for closed type families, but it's a small improvement in general. +(CF5) Consider + type family F a where + F (Just x) = Int + + [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 + 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 + 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 + ``` + 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`. + Note [Cache-caused loops] ~~~~~~~~~~~~~~~~~~~~~~~~~ It is very dangerous to cache a rewritten wanted family equation as 'solved' in our View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0b6d14a97a1f0b7f6fe3d283664759c1... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0b6d14a97a1f0b7f6fe3d283664759c1... You're receiving this email because of your account on gitlab.haskell.org.