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
3 changed files:
Changes:
| ... | ... | @@ -915,21 +915,22 @@ simplifyInfer top_lvl rhs_tclvl infer_mode sigs name_taus wanteds |
| 915 | 915 | ; let psig_theta = concatMap sig_inst_theta partial_sigs
|
| 916 | 916 | |
| 917 | 917 | -- First do full-blown solving
|
| 918 | - -- NB: we must gather up all the bindings from doing
|
|
| 919 | - -- this solving; hence (runTcSWithEvBinds ev_binds_var).
|
|
| 920 | - -- And note that since there are nested implications,
|
|
| 921 | - -- calling solveWanteds will side-effect their evidence
|
|
| 922 | - -- bindings, so we can't just revert to the input
|
|
| 923 | - -- constraint.
|
|
| 924 | - |
|
| 918 | + -- NB: we must gather up all the bindings from doing this solving; hence
|
|
| 919 | + -- (runTcSWithEvBinds ev_binds_var). And note that since there are
|
|
| 920 | + -- nested implications, calling solveWanteds will side-effect their
|
|
| 921 | + -- evidence bindings, so we can't just revert to the input constraint.
|
|
| 922 | + --
|
|
| 923 | + -- See also Note [Inferring principal types]
|
|
| 925 | 924 | ; ev_binds_var <- TcM.newTcEvBinds
|
| 926 | 925 | ; psig_evs <- newWanteds AnnOrigin psig_theta
|
| 927 | 926 | ; wanted_transformed
|
| 928 | 927 | <- runTcSWithEvBinds ev_binds_var $
|
| 929 | - setTcLevelTcS rhs_tclvl $ -- ToDo: describe subtle placement
|
|
| 928 | + setTcLevelTcS rhs_tclvl $
|
|
| 930 | 929 | solveWanteds (mkSimpleWC psig_evs `andWC` wanteds)
|
| 930 | + -- setLevelTcS: we do setLevel /inside/ the runTcS, so that
|
|
| 931 | + -- we initialise the InertSet inert_given_eq_lvl as far
|
|
| 932 | + -- out as possible, maximising oppportunities to unify
|
|
| 931 | 933 | -- psig_evs : see Note [Add signature contexts as wanteds]
|
| 932 | - -- See Note [Inferring principal types]
|
|
| 933 | 934 | |
| 934 | 935 | -- Find quant_pred_candidates, the predicates that
|
| 935 | 936 | -- we'll consider quantifying over
|
| ... | ... | @@ -678,6 +678,23 @@ should update inert_given_eq_lvl? |
| 678 | 678 | imply nominal ones. For example, if (G a ~R G b) and G's argument's
|
| 679 | 679 | role is nominal, then we can deduce a ~N b.
|
| 680 | 680 | |
| 681 | +(TEG6) A subtle point is this: when initialising the solver, giving it
|
|
| 682 | + an empty InertSet, we must conservatively initialise `inert_given_lvl`
|
|
| 683 | + to the /current/ TcLevel. This matters when doing let-generalisation.
|
|
| 684 | + Consider #26004:
|
|
| 685 | + f w e = case e of
|
|
| 686 | + T1 -> let y = not w in False -- T1 is a GADT
|
|
| 687 | + T2 -> True
|
|
| 688 | + When let-generalising `y`, we will have (w :: alpha[1]) in the type
|
|
| 689 | + envt; and we are under GADT pattern match. So when we solve the
|
|
| 690 | + constraints from y's RHS, in simplifyInfer, we must NOT unify
|
|
| 691 | + alpha[1] := Bool
|
|
| 692 | + Since we don't know what enclosing equalities there are, we just
|
|
| 693 | + conservatively assume that there are some.
|
|
| 694 | + |
|
| 695 | + This initialisation in done in `runTcSWithEvBinds`, which passes
|
|
| 696 | + the current TcLevl to `emptyInert`.
|
|
| 697 | + |
|
| 681 | 698 | Historical note: prior to #24938 we also ignored Given equalities that
|
| 682 | 699 | did not mention an "outer" type variable. But that is wrong, as #24938
|
| 683 | 700 | showed. Another example is immortalised in test LocalGivenEqs2
|
| ... | ... | @@ -1224,8 +1224,13 @@ runTcSWithEvBinds' :: TcSMode |
| 1224 | 1224 | runTcSWithEvBinds' mode ev_binds_var tcs
|
| 1225 | 1225 | = do { unified_var <- TcM.newTcRef 0
|
| 1226 | 1226 | ; step_count <- TcM.newTcRef 0
|
| 1227 | + |
|
| 1228 | + -- Make a fresh, empty inert set
|
|
| 1229 | + -- Subtle point: see (TEG6) in Note [Tracking Given equalities]
|
|
| 1230 | + -- in GHC.Tc.Solver.InertSet
|
|
| 1227 | 1231 | ; tc_lvl <- TcM.getTcLevel
|
| 1228 | 1232 | ; inert_var <- TcM.newTcRef (emptyInert tc_lvl)
|
| 1233 | + |
|
| 1229 | 1234 | ; wl_var <- TcM.newTcRef emptyWorkList
|
| 1230 | 1235 | ; unif_lvl_var <- TcM.newTcRef Nothing
|
| 1231 | 1236 | ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
|