Simon Peyton Jones pushed to branch wip/T26004 at Glasgow Haskell Compiler / GHC Commits: 99fc2a5b by Simon Peyton Jones at 2025-05-01T12:09:28+01:00 Wibbles - - - - - 3 changed files: - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs Changes: ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -915,21 +915,22 @@ simplifyInfer top_lvl rhs_tclvl infer_mode sigs name_taus wanteds ; let psig_theta = concatMap sig_inst_theta partial_sigs -- First do full-blown solving - -- NB: we must gather up all the bindings from doing - -- this solving; hence (runTcSWithEvBinds ev_binds_var). - -- And note that since there are nested implications, - -- calling solveWanteds will side-effect their evidence - -- bindings, so we can't just revert to the input - -- constraint. - + -- NB: we must gather up all the bindings from doing this solving; hence + -- (runTcSWithEvBinds ev_binds_var). And note that since there are + -- nested implications, calling solveWanteds will side-effect their + -- evidence bindings, so we can't just revert to the input constraint. + -- + -- See also Note [Inferring principal types] ; ev_binds_var <- TcM.newTcEvBinds ; psig_evs <- newWanteds AnnOrigin psig_theta ; wanted_transformed <- runTcSWithEvBinds ev_binds_var $ - setTcLevelTcS rhs_tclvl $ -- ToDo: describe subtle placement + setTcLevelTcS rhs_tclvl $ solveWanteds (mkSimpleWC psig_evs `andWC` wanteds) + -- setLevelTcS: we do setLevel /inside/ the runTcS, so that + -- we initialise the InertSet inert_given_eq_lvl as far + -- out as possible, maximising oppportunities to unify -- psig_evs : see Note [Add signature contexts as wanteds] - -- See Note [Inferring principal types] -- Find quant_pred_candidates, the predicates that -- we'll consider quantifying over ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -678,6 +678,23 @@ should update inert_given_eq_lvl? imply nominal ones. For example, if (G a ~R G b) and G's argument's role is nominal, then we can deduce a ~N b. +(TEG6) A subtle point is this: when initialising the solver, giving it + an empty InertSet, we must conservatively initialise `inert_given_lvl` + to the /current/ TcLevel. This matters when doing let-generalisation. + Consider #26004: + f w e = case e of + T1 -> let y = not w in False -- T1 is a GADT + T2 -> True + When let-generalising `y`, we will have (w :: alpha[1]) in the type + envt; and we are under GADT pattern match. So when we solve the + constraints from y's RHS, in simplifyInfer, we must NOT unify + alpha[1] := Bool + Since we don't know what enclosing equalities there are, we just + conservatively assume that there are some. + + This initialisation in done in `runTcSWithEvBinds`, which passes + the current TcLevl to `emptyInert`. + Historical note: prior to #24938 we also ignored Given equalities that did not mention an "outer" type variable. But that is wrong, as #24938 showed. Another example is immortalised in test LocalGivenEqs2 ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -1224,8 +1224,13 @@ runTcSWithEvBinds' :: TcSMode runTcSWithEvBinds' mode ev_binds_var tcs = do { unified_var <- TcM.newTcRef 0 ; step_count <- TcM.newTcRef 0 + + -- Make a fresh, empty inert set + -- Subtle point: see (TEG6) in Note [Tracking Given equalities] + -- in GHC.Tc.Solver.InertSet ; tc_lvl <- TcM.getTcLevel ; inert_var <- TcM.newTcRef (emptyInert tc_lvl) + ; wl_var <- TcM.newTcRef emptyWorkList ; unif_lvl_var <- TcM.newTcRef Nothing ; let env = TcSEnv { tcs_ev_binds = ev_binds_var View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/99fc2a5b545cad180859a55109afb587... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/99fc2a5b545cad180859a55109afb587... You're receiving this email because of your account on gitlab.haskell.org.