Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: a381c3c4 by Simon Peyton Jones at 2025-08-07T17:32:31+01:00 Wibbles to fundeps [skip ci] - - - - - 5 changed files: - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - testsuite/tests/typecheck/should_fail/tcfail143.stderr Changes: ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -648,69 +648,6 @@ on whether we apply this optimization when IncoherentInstances is in effect: The output of `main` if we avoid the optimization under the effect of IncoherentInstances is `1`. If we were to do the optimization, the output of `main` would be `2`. - - -Note [No Given/Given fundeps] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We do not create constraints from: -* Given/Given interactions via functional dependencies or type family - injectivity annotations. -* Given/instance fundep interactions via functional dependencies or - type family injectivity annotations. - -In this Note, all these interactions are called just "fundeps". - -We ingore such fundeps for several reasons: - -1. These fundeps will never serve a purpose in accepting more - programs: Given constraints do not contain metavariables that could - be unified via exploring fundeps. They *could* be useful in - discovering inaccessible code. However, the constraints will be - Wanteds, and as such will cause errors (not just warnings) if they - go unsolved. Maybe there is a clever way to get the right - inaccessible code warnings, but the path forward is far from - clear. #12466 has further commentary. - -2. Furthermore, here is a case where a Given/instance interaction is actively - harmful (from dependent/should_compile/RaeJobTalk): - - type family a == b :: Bool - type family Not a = r | r -> a where - Not False = True - Not True = False - - [G] Not (a == b) ~ True - - Reacting this Given with the equations for Not produces - - [W] a == b ~ False - - This is indeed a true consequence, and would make sense as a fresh Given. - But we don't have a way to produce evidence for fundeps, as a Wanted it - is /harmful/: we can't prove it, and so we'll report an error and reject - the program. (Previously fundeps gave rise to Deriveds, which - carried no evidence, so it didn't matter that they could not be proved.) - -3. #20922 showed a subtle different problem with Given/instance fundeps. - type family ZipCons (as :: [k]) (bssx :: [[k]]) = (r :: [[k]]) | r -> as bssx where - ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss - ... - - tclevel = 4 - [G] ZipCons is1 iss ~ (i : is2) : jss - - (The tclevel=4 means that this Given is at level 4.) The fundep tells us that - 'iss' must be of form (is2 : beta[4]) where beta[4] is a fresh unification - variable; we don't know what type it stands for. So we would emit - [W] iss ~ is2 : beta - - Again we can't prove that equality; and worse we'll rewrite iss to - (is2:beta) in deeply nested constraints inside this implication, - where beta is untouchable (under other equality constraints), leading - to other insoluble constraints. - -The bottom line: since we have no evidence for them, we should ignore Given/Given -and Given/instance fundeps entirely. -} tryInertDicts :: DictCt -> SolverStage () ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -313,7 +313,13 @@ doDictFunDepImprovement dict_ct doDictFunDepImprovementLocal :: DictCt -> SolverStage () -- Using functional dependencies, interact the DictCt with the -- inert Givens and Wanteds, to produce new equalities -doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = wanted_ev }) +doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) + | isGiven work_ev + = -- If work_ev is Given, there could in principle be some inert Wanteds + -- but in practice there never are because we solve Givens first + nopStage () + + | otherwise = Stage $ do { inerts <- getInertCans @@ -324,35 +330,44 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = wanted_ev } ; if imp then startAgainWith (CDictCan dict_ct) else continueWith () } where - wanted_pred = ctEvPred wanted_ev - wanted_loc = ctEvLoc wanted_ev + work_pred = ctEvPred work_ev + work_loc = ctEvLoc work_ev + work_is_given = isGiven work_ev do_interaction :: Cts -> DictCt -> TcS Cts - do_interaction new_eqs1 (DictCt { di_ev = all_ev }) -- This can be Given or Wanted + do_interaction new_eqs1 (DictCt { di_ev = inert_ev }) -- This can be Given or Wanted + | work_is_given && isGiven inert_ev + -- Do not create FDs from Given/Given interactions + -- See Note [No Given/Given fundeps] + -- It is possible for work_ev to be Given when inert_ev is Wanted: + -- this can happen if a Given is kicked out by a unification + = return new_eqs1 + + | otherwise = do { traceTcS "doLocalFunDepImprovement" $ - vcat [ ppr wanted_ev - , pprCtLoc wanted_loc, ppr (isGivenLoc wanted_loc) - , pprCtLoc all_loc, ppr (isGivenLoc all_loc) + vcat [ ppr work_ev + , pprCtLoc work_loc, ppr (isGivenLoc work_loc) + , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc) , pprCtLoc deriv_loc, ppr (isGivenLoc deriv_loc) ] - ; new_eqs2 <- unifyFunDepWanteds_new wanted_ev $ - improveFromAnother (deriv_loc, all_rewriters) - all_pred wanted_pred + ; new_eqs2 <- unifyFunDepWanteds_new work_ev $ + improveFromAnother (deriv_loc, inert_rewriters) + inert_pred work_pred ; return (new_eqs1 `unionBags` new_eqs2) } where - all_pred = ctEvPred all_ev - all_loc = ctEvLoc all_ev - all_rewriters = ctEvRewriters all_ev - deriv_loc = wanted_loc { ctl_depth = deriv_depth + inert_pred = ctEvPred inert_ev + inert_loc = ctEvLoc inert_ev + inert_rewriters = ctEvRewriters inert_ev + deriv_loc = work_loc { ctl_depth = deriv_depth , ctl_origin = deriv_origin } - deriv_depth = ctl_depth wanted_loc `maxSubGoalDepth` - ctl_depth all_loc - deriv_origin = FunDepOrigin1 wanted_pred - (ctLocOrigin wanted_loc) - (ctLocSpan wanted_loc) - all_pred - (ctLocOrigin all_loc) - (ctLocSpan all_loc) + deriv_depth = ctl_depth work_loc `maxSubGoalDepth` + ctl_depth inert_loc + deriv_origin = FunDepOrigin1 work_pred + (ctLocOrigin work_loc) + (ctLocSpan work_loc) + inert_pred + (ctLocOrigin inert_loc) + (ctLocSpan inert_loc) doDictFunDepImprovementTop :: DictCt -> SolverStage () doDictFunDepImprovementTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = xis }) @@ -389,6 +404,69 @@ solveFunDeps generate_eqs do { eqs <- generate_eqs ; solveSimpleWanteds eqs } +{- Note [No Given/Given fundeps] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We do not create constraints from: +* Given/Given interactions via functional dependencies or type family + injectivity annotations. +* Given/instance fundep interactions via functional dependencies or + type family injectivity annotations. + +In this Note, all these interactions are called just "fundeps". + +We ingore such fundeps for several reasons: + +1. These fundeps will never serve a purpose in accepting more + programs: Given constraints do not contain metavariables that could + be unified via exploring fundeps. They *could* be useful in + discovering inaccessible code. However, the constraints will be + Wanteds, and as such will cause errors (not just warnings) if they + go unsolved. Maybe there is a clever way to get the right + inaccessible code warnings, but the path forward is far from + clear. #12466 has further commentary. + +2. Furthermore, here is a case where a Given/instance interaction is actively + harmful (from dependent/should_compile/RaeJobTalk): + + type family a == b :: Bool + type family Not a = r | r -> a where + Not False = True + Not True = False + + [G] Not (a == b) ~ True + + Reacting this Given with the equations for Not produces + + [W] a == b ~ False + + This is indeed a true consequence, and would make sense as a fresh Given. + But we don't have a way to produce evidence for fundeps, as a Wanted it + is /harmful/: we can't prove it, and so we'll report an error and reject + the program. (Previously fundeps gave rise to Deriveds, which + carried no evidence, so it didn't matter that they could not be proved.) + +3. #20922 showed a subtle different problem with Given/instance fundeps. + type family ZipCons (as :: [k]) (bssx :: [[k]]) = (r :: [[k]]) | r -> as bssx where + ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss + ... + + tclevel = 4 + [G] ZipCons is1 iss ~ (i : is2) : jss + + (The tclevel=4 means that this Given is at level 4.) The fundep tells us that + 'iss' must be of form (is2 : beta[4]) where beta[4] is a fresh unification + variable; we don't know what type it stands for. So we would emit + [W] iss ~ is2 : beta + + Again we can't prove that equality; and worse we'll rewrite iss to + (is2:beta) in deeply nested constraints inside this implication, + where beta is untouchable (under other equality constraints), leading + to other insoluble constraints. + +The bottom line: since we have no evidence for them, we should ignore Given/Given +and Given/instance fundeps entirely. +-} + {- ************************************************************************ * * ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -1298,21 +1298,25 @@ nestFunDepsTcS (TcS thing_inside) , tcs_worklist = new_wl_var , tcs_unif_lvl = new_unif_lvl_var } + ; TcM.traceTc "nestFunDepsTcS {" empty ; (inner_lvl, _res) <- TcM.pushTcLevelM $ thing_inside nest_env + -- Increase the level so that unification variables allocated by + -- the fundep-creation itself don't count as useful unifications + ; TcM.traceTc "nestFunDepsTcS }" empty -- Figure out whether the fundeps did any useful unifications, -- and if so update the tcs_unif_lvl ; mb_new_lvl <- TcM.readTcRef new_unif_lvl_var ; case mb_new_lvl of - Just new_lvl - | inner_lvl `deeperThanOrSame` new_lvl + Just unif_lvl + | inner_lvl `deeperThanOrSame` unif_lvl -> -- Some useful unifications took place do { mb_old_lvl <- TcM.readTcRef unif_lvl_var ; case mb_old_lvl of - Just old_lvl | new_lvl `deeperThanOrSame` old_lvl + Just old_lvl | unif_lvl `deeperThanOrSame` old_lvl -> return () - _ -> TcM.writeTcRef unif_lvl_var (Just new_lvl) + _ -> TcM.writeTcRef unif_lvl_var (Just unif_lvl) ; return True } _ -> return False -- No unifications (except of vars ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -126,7 +126,7 @@ simplify_loop n limit definitely_redo_implications -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet ; wc2 <- if not definitely_redo_implications -- See Note [Superclass iteration] - && n_unifs1 == 0 -- for this conditional + && n_unifs1 == 0 -- for this conditional then return (wc { wc_simple = simples1 }) -- Short cut else do { implics1 <- solveNestedImplications implics ; return (wc { wc_simple = simples1 ===================================== testsuite/tests/typecheck/should_fail/tcfail143.stderr ===================================== @@ -1,8 +1,6 @@ - -tcfail143.hs:30:9: error: [GHC-18872] - • Couldn't match type ‘S Z’ with ‘Z’ - arising from a functional dependency between: - constraint ‘MinMax (S Z) Z Z Z’ arising from a use of ‘extend’ - instance ‘MinMax a Z Z a’ at tcfail143.hs:12:10-23 +tcfail143.hs:30:9: error: [GHC-39999] + • No instance for ‘MinMax (S Z) Z Z Z’ + arising from a use of ‘extend’ • In the expression: n1 `extend` n0 In an equation for ‘t2’: t2 = n1 `extend` n0 + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a381c3c47e7b7784f66b6cc82a12a5c8... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a381c3c47e7b7784f66b6cc82a12a5c8... You're receiving this email because of your account on gitlab.haskell.org.