Commit f2bb550e authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari
Browse files

Fix isDroppableCt (Trac #14763)

When finishing up an implication constraint, it's a bit tricky to
decide which Derived constraints to retain (for error reporting) and
which to discard.  I got this wrong in commit
   f20cf982
   (Remove wc_insol from WantedConstraints)

The particular problem in Trac #14763 was that we were reporting as an
error a fundep-generated constraint
  (ex ~ T)
where 'ex' is an existentially-bound variable in a pattern match.
But this isn't really an error at all.

This patch fixes the problem. Indeed, since I had to understand
this rather tricky code, I took the opportunity to clean it up
and document better.  See
  isDroppableCt :: Ct -> Bool
and Note [Dropping derived constraints]

I also removed wl_deriv altogether from the WorkList data type.  It
was there in the hope of gaining efficiency by not even processing
lots of derived constraints, but it has turned out that most derived
constraints (notably equalities) must be processed anyway; see
Note [Prioritise equalities] in TcSMonad.

The two are coupled because to decide which constraints to put in
wl_deriv I was using another variant of isDroppableCt.  Now it's much
simpler -- and perhaps even more efficient too.

(cherry picked from commit 6edafe3b)
parent 4e0b4b36
...@@ -1688,11 +1688,16 @@ is embarrassing. See #11198 for more tales of destruction. ...@@ -1688,11 +1688,16 @@ is embarrassing. See #11198 for more tales of destruction.
The reason for this odd behavior is much the same as The reason for this odd behavior is much the same as
Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the
new `co` is a Wanted. The solution is then not to use `co` to "rewrite" new `co` is a Wanted.
-- that is, cast -- `w`, but instead to keep `w` heterogeneous and irreducible.
Given that we're not using `co`, there is no reason to collect evidence The solution is then not to use `co` to "rewrite" -- that is, cast
for it, so `co` is born a Derived. When the Derived is solved (by unification), -- `w`, but instead to keep `w` heterogeneous and
the original wanted (`w`) will get kicked out. irreducible. Given that we're not using `co`, there is no reason to
collect evidence for it, so `co` is born a Derived, with a CtOrigin
of KindEqOrigin.
When the Derived is solved (by unification), the original wanted (`w`)
will get kicked out.
Note that, if we had [G] co1 :: k ~ Type available, then none of this code would Note that, if we had [G] co1 :: k ~ Type available, then none of this code would
trigger, because flattening would have rewritten k to Type. That is, trigger, because flattening would have rewritten k to Type. That is,
......
...@@ -687,7 +687,7 @@ we'll complain about ...@@ -687,7 +687,7 @@ we'll complain about
f :: ((Int ~ Bool) => a -> a) -> Int f :: ((Int ~ Bool) => a -> a) -> Int
which arguably is OK. It's more debatable for which arguably is OK. It's more debatable for
g :: (Int ~ Bool) => Int -> Int g :: (Int ~ Bool) => Int -> Int
but it's tricky to distinguish these cases to we don't report but it's tricky to distinguish these cases so we don't report
either. either.
The bottom line is this: find_gadt_match looks for an enclosing The bottom line is this: find_gadt_match looks for an enclosing
......
...@@ -670,7 +670,7 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble }) ...@@ -670,7 +670,7 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
-- which can happen with solveOneFromTheOther, so that -- which can happen with solveOneFromTheOther, so that
-- we get distinct error messages with -fdefer-type-errors -- we get distinct error messages with -fdefer-type-errors
-- See Note [Do not add duplicate derived insolubles] -- See Note [Do not add duplicate derived insolubles]
, not (isDroppableDerivedCt workItem) , not (isDroppableCt workItem)
= continueWith workItem = continueWith workItem
| let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
...@@ -1859,7 +1859,8 @@ improveTopFunEqs ev fam_tc args fsk ...@@ -1859,7 +1859,8 @@ improveTopFunEqs ev fam_tc args fsk
, ppr eqns ]) , ppr eqns ])
; mapM_ (unifyDerived loc Nominal) eqns } ; mapM_ (unifyDerived loc Nominal) eqns }
where where
loc = ctEvLoc ev loc = ctEvLoc ev -- ToDo: this location is wrong; it should be FunDepOrigin2
-- See Trac #14778
improve_top_fun_eqs :: FamInstEnvs improve_top_fun_eqs :: FamInstEnvs
-> TyCon -> [TcType] -> TcType -> TyCon -> [TcType] -> TcType
......
...@@ -87,7 +87,7 @@ module TcRnTypes( ...@@ -87,7 +87,7 @@ module TcRnTypes(
addInsols, insolublesOnly, addSimples, addImplics, addInsols, insolublesOnly, addSimples, addImplics,
tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt, tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt,
isDroppableDerivedLoc, isDroppableDerivedCt, insolubleImplic, isDroppableCt, insolubleImplic,
arisesFromGivens, arisesFromGivens,
Implication(..), newImplication, Implication(..), newImplication,
...@@ -1923,13 +1923,10 @@ dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples ...@@ -1923,13 +1923,10 @@ dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples
dropDerivedCt :: Ct -> Maybe Ct dropDerivedCt :: Ct -> Maybe Ct
dropDerivedCt ct dropDerivedCt ct
= case ctEvFlavour ev of = case ctEvFlavour ev of
Given -> Just ct -- Presumably insoluble; keep
Wanted WOnly -> Just (ct' { cc_ev = ev_wd }) Wanted WOnly -> Just (ct' { cc_ev = ev_wd })
Wanted _ -> Just ct' Wanted _ -> Just ct'
Derived | isDroppableDerivedLoc (ctLoc ct) _ | isDroppableCt ct -> Nothing
-> Nothing | otherwise -> Just ct
| otherwise
-> Just ct
where where
ev = ctEvidence ct ev = ctEvidence ct
ev_wd = ev { ctev_nosh = WDeriv } ev_wd = ev { ctev_nosh = WDeriv }
...@@ -1945,26 +1942,41 @@ we might miss some fundeps. Trac #13662 showed this up. ...@@ -1945,26 +1942,41 @@ we might miss some fundeps. Trac #13662 showed this up.
See Note [The superclass story] in TcCanonical. See Note [The superclass story] in TcCanonical.
-} -}
isDroppableDerivedCt :: Ct -> Bool isDroppableCt :: Ct -> Bool
isDroppableDerivedCt ct isDroppableCt ct
| isDerivedCt ct = isDroppableDerivedLoc (ctLoc ct) = isDerived ev && not keep_deriv
| otherwise = False -- Drop only derived constraints, and then only if they
-- obey Note [Dropping derived constraints]
isDroppableDerivedLoc :: CtLoc -> Bool where
-- See Note [Dropping derived constraints] ev = ctEvidence ct
isDroppableDerivedLoc loc loc = ctEvLoc ev
= case ctLocOrigin loc of orig = ctLocOrigin loc
HoleOrigin {} -> False
KindEqOrigin {} -> False keep_deriv
GivenOrigin {} -> False = case ct of
CHoleCan {} -> True
-- See Note [Dropping derived constraints] CIrredCan { cc_insol = insoluble }
-- For fundeps, drop wanted/wanted interactions -> keep_eq insoluble
FunDepOrigin2 {} -> False _ -> keep_eq False
FunDepOrigin1 _ loc1 _ loc2
| isGivenLoc loc1 || isGivenLoc loc2 -> False keep_eq definitely_insoluble
| otherwise -> True | isGivenOrigin orig -- Arising only from givens
_ -> True = definitely_insoluble -- Keep only definitely insoluble
| otherwise
= case orig of
KindEqOrigin {} -> True -- Why?
-- See Note [Dropping derived constraints]
-- For fundeps, drop wanted/wanted interactions
FunDepOrigin2 {} -> True -- Top-level/Wanted
FunDepOrigin1 _ loc1 _ loc2
| g1 || g2 -> True -- Given/Wanted errors: keep all
| otherwise -> False -- Wanted/Wanted errors: discard
where
g1 = isGivenLoc loc1
g2 = isGivenLoc loc2
_ -> False
arisesFromGivens :: Ct -> Bool arisesFromGivens :: Ct -> Bool
arisesFromGivens ct arisesFromGivens ct
...@@ -1987,30 +1999,43 @@ isGivenOrigin _ = False ...@@ -1987,30 +1999,43 @@ isGivenOrigin _ = False
In general we discard derived constraints at the end of constraint solving; In general we discard derived constraints at the end of constraint solving;
see dropDerivedWC. For example see dropDerivedWC. For example
* If we have an unsolved [W] (Ord a), we don't want to complain about * Superclasses: if we have an unsolved [W] (Ord a), we don't want to
an unsolved [D] (Eq a) as well. complain about an unsolved [D] (Eq a) as well.
* If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate
[D] Int ~ Bool, and we don't want to report that because it's incomprehensible. [D] Int ~ Bool, and we don't want to report that because it's
That is why we don't rewrite wanteds with wanteds! incomprehensible. That is why we don't rewrite wanteds with wanteds!
But (tiresomely) we do keep *some* Derived insolubles: But (tiresomely) we do keep *some* Derived constraints:
* Type holes are derived constraints, because they have no evidence * Type holes are derived constraints, because they have no evidence
and we want to keep them, so we get the error report and we want to keep them, so we get the error report
* Insoluble derived equalities (e.g. [D] Int ~ Bool) may arise from * Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with
functional dependency interactions: KindEqOrigin, may arise from a type equality a ~ Int#, say. See
- Given or Wanted interacting with an instance declaration (FunDepOrigin2) Note [Equalities with incompatible kinds] in TcCanonical.
- Given/Given interactions (FunDepOrigin1); this reflects unreachable code
* We keep most derived equalities arising from functional dependencies
- Given/Given interactions (subset of FunDepOrigin1):
The definitely-insoluble ones reflect unreachable code.
Others not-definitely-insoluble ones like [D] a ~ Int do not
reflect unreachable code; indeed if fundeps generated proofs, it'd
be a useful equality. See Trac #14763. So we discard them.
- Given/Wanted interacGiven or Wanted interacting with an
instance declaration (FunDepOrigin2)
- Given/Wanted interactions (FunDepOrigin1); see Trac #9612 - Given/Wanted interactions (FunDepOrigin1); see Trac #9612
But for Wanted/Wanted interactions we do /not/ want to report an - But for Wanted/Wanted interactions we do /not/ want to report an
error (Trac #13506). Consider [W] C Int Int, [W] C Int Bool, with error (Trac #13506). Consider [W] C Int Int, [W] C Int Bool, with
a fundep on class C. We don't want to report an insoluble Int~Bool; a fundep on class C. We don't want to report an insoluble Int~Bool;
c.f. "wanteds do not rewrite wanteds". c.f. "wanteds do not rewrite wanteds".
To distinguish these cases we use the CtOrigin.
Moreover, we keep *all* derived insolubles under some circumstances: NB: we keep *all* derived insolubles under some circumstances:
* They are looked at by simplifyInfer, to decide whether to * They are looked at by simplifyInfer, to decide whether to
generalise. Example: [W] a ~ Int, [W] a ~ Bool generalise. Example: [W] a ~ Int, [W] a ~ Bool
...@@ -2018,8 +2043,6 @@ Moreover, we keep *all* derived insolubles under some circumstances: ...@@ -2018,8 +2043,6 @@ Moreover, we keep *all* derived insolubles under some circumstances:
and we want simplifyInfer to see that, even though we don't and we want simplifyInfer to see that, even though we don't
ultimately want to generate an (inexplicable) error message from it ultimately want to generate an (inexplicable) error message from it
To distinguish these cases we use the CtOrigin.
************************************************************************ ************************************************************************
* * * *
...@@ -3290,7 +3313,7 @@ data CtOrigin ...@@ -3290,7 +3313,7 @@ data CtOrigin
-- visible.) Only used for prioritizing error messages. -- visible.) Only used for prioritizing error messages.
} }
| KindEqOrigin | KindEqOrigin -- See Note [Equalities with incompatible kinds] in TcCanonical.
TcType (Maybe TcType) -- A kind equality arising from unifying these two types TcType (Maybe TcType) -- A kind equality arising from unifying these two types
CtOrigin -- originally arising from this CtOrigin -- originally arising from this
(Maybe TypeOrKind) -- the level of the eq this arises from (Maybe TypeOrKind) -- the level of the eq this arises from
......
...@@ -5,7 +5,7 @@ module TcSMonad ( ...@@ -5,7 +5,7 @@ module TcSMonad (
-- The work list -- The work list
WorkList(..), isEmptyWorkList, emptyWorkList, WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt, extendWorkListDerived, extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListEq, extendWorkListFunEq, extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
appendWorkList, extendWorkListImplic, appendWorkList, extendWorkListImplic,
selectNextWorkItem, selectNextWorkItem,
...@@ -36,7 +36,7 @@ module TcSMonad ( ...@@ -36,7 +36,7 @@ module TcSMonad (
setEvBind, setWantedEq, setEqIfWanted, setEvBind, setWantedEq, setEqIfWanted,
setWantedEvTerm, setWantedEvBind, setEvBindIfWanted, setWantedEvTerm, setWantedEvBind, setEvBindIfWanted,
newEvVar, newGivenEvVar, newGivenEvVars, newEvVar, newGivenEvVar, newGivenEvVars,
emitNewDerived, emitNewDeriveds, emitNewDerivedEq, emitNewDeriveds, emitNewDerivedEq,
checkReductionDepth, checkReductionDepth,
getInstEnvs, getFamInstEnvs, -- Getting the environments getInstEnvs, getFamInstEnvs, -- Getting the environments
...@@ -190,7 +190,8 @@ consider using this depth for prioritization as well in the future. ...@@ -190,7 +190,8 @@ consider using this depth for prioritization as well in the future.
As a simple form of priority queue, our worklist separates out As a simple form of priority queue, our worklist separates out
* equalities (wl_eqs); see Note [Prioritise equalities] * equalities (wl_eqs); see Note [Prioritise equalities]
* non-equality deriveds (wl_derivs); see Note [Process derived items last] * type-function equalities (wl_funeqs)
* all the rest (wl_rest)
Note [Prioritise equalities] Note [Prioritise equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
...@@ -201,10 +202,6 @@ It's very important to process equalities /first/: ...@@ -201,10 +202,6 @@ It's very important to process equalities /first/:
and then kicking it out later. That's extra work compared to just and then kicking it out later. That's extra work compared to just
doing the equality first. doing the equality first.
* (Derived equalities) Notwithstanding Note [Process derived items
last], we want to process /Derived/ equalities eagerly, for the
(Efficiency) reason above.
* (Avoiding fundep iteration) As Trac #14723 showed, it's possible to * (Avoiding fundep iteration) As Trac #14723 showed, it's possible to
get non-termination if we get non-termination if we
- Emit the Derived fundep equalities for a class constraint, - Emit the Derived fundep equalities for a class constraint,
...@@ -215,15 +212,21 @@ It's very important to process equalities /first/: ...@@ -215,15 +212,21 @@ It's very important to process equalities /first/:
equalities in the work-list), but generates yet more fundeps equalities in the work-list), but generates yet more fundeps
Solution: prioritise derived equalities over class constraints Solution: prioritise derived equalities over class constraints
* (Class equalities) We need to prioritise equalities even if they are * (Class equalities) We need to prioritise equalities even if they
hidden inside a class constraint; see Note [Prioritise class are hidden inside a class constraint;
equalities] see Note [Prioritise class equalities]
* (Kick-out) We want to apply this priority scheme to kicked-out * (Kick-out) We want to apply this priority scheme to kicked-out
constraints too (see the call to extendWorkListCt in kick_out_rewritable constraints too (see the call to extendWorkListCt in kick_out_rewritable
E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
homo-kinded when kicked out, and hence we want to priotitise it. homo-kinded when kicked out, and hence we want to priotitise it.
* (Derived equalities) Originally we tried to postpone processing
Derived equalities, in the hope that we might never need to deal
with them at all; but in fact we must process Derived equalities
eagerly, partly for the (Efficiency) reason, and more importantly
for (Avoiding fundep iteration).
Note [Prioritise class equalities] Note [Prioritise class equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We prioritise equalities in the solver (see selectWorkItem). But class We prioritise equalities in the solver (see selectWorkItem). But class
...@@ -240,13 +243,6 @@ So we arrange to put these particular class constraints in the wl_eqs. ...@@ -240,13 +243,6 @@ So we arrange to put these particular class constraints in the wl_eqs.
NB: since we do not currently apply the substitution to the NB: since we do not currently apply the substitution to the
inert_solved_dicts, the knot-tying still seems a bit fragile. inert_solved_dicts, the knot-tying still seems a bit fragile.
But this makes it better. But this makes it better.
Note [Process derived items last]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We can often solve all goals without processing *any* derived constraints.
The derived constraints are just there to help us if we get stuck. So
we keep them in a separate list.
-} -}
-- See Note [WorkList priorities] -- See Note [WorkList priorities]
...@@ -262,29 +258,23 @@ data WorkList ...@@ -262,29 +258,23 @@ data WorkList
, wl_rest :: [Ct] , wl_rest :: [Ct]
, wl_deriv :: [CtEvidence]
-- Implicitly non-canonical
-- No equalities in here (they are in wl_eqs)
-- See Note [Process derived items last]
, wl_implics :: Bag Implication -- See Note [Residual implications] , wl_implics :: Bag Implication -- See Note [Residual implications]
} }
appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList appendWorkList
(WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1 (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1
, wl_deriv = ders1, wl_implics = implics1 }) , wl_implics = implics1 })
(WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2 (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2
, wl_deriv = ders2, wl_implics = implics2 }) , wl_implics = implics2 })
= WL { wl_eqs = eqs1 ++ eqs2 = WL { wl_eqs = eqs1 ++ eqs2
, wl_funeqs = funeqs1 ++ funeqs2 , wl_funeqs = funeqs1 ++ funeqs2
, wl_rest = rest1 ++ rest2 , wl_rest = rest1 ++ rest2
, wl_deriv = ders1 ++ ders2
, wl_implics = implics1 `unionBags` implics2 } , wl_implics = implics1 `unionBags` implics2 }
workListSize :: WorkList -> Int workListSize :: WorkList -> Int
workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest = rest }) workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
= length eqs + length funeqs + length rest + length ders = length eqs + length funeqs + length rest
workListWantedCount :: WorkList -> Int workListWantedCount :: WorkList -> Int
-- Count the things we need to solve -- Count the things we need to solve
...@@ -301,9 +291,6 @@ workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest }) ...@@ -301,9 +291,6 @@ workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
extendWorkListEq :: Ct -> WorkList -> WorkList extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl } extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
extendWorkListEqs :: [Ct] -> WorkList -> WorkList
extendWorkListEqs cts wl = wl { wl_eqs = cts ++ wl_eqs wl }
extendWorkListFunEq :: Ct -> WorkList -> WorkList extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl } extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
...@@ -311,15 +298,9 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList ...@@ -311,15 +298,9 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality -- Extension by non equality
extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
extendWorkListDerived :: CtLoc -> CtEvidence -> WorkList -> WorkList extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
extendWorkListDerived loc ev wl extendWorkListDeriveds evs wl
| isDroppableDerivedLoc loc = wl { wl_deriv = ev : wl_deriv wl } = extendWorkListCts (map mkNonCanonical evs) wl
| otherwise = extendWorkListEq (mkNonCanonical ev) wl
extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds loc evs wl
| isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl }
| otherwise = extendWorkListEqs (map mkNonCanonical evs) wl
extendWorkListImplic :: Bag Implication -> WorkList -> WorkList extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl } extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl }
...@@ -349,12 +330,12 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts ...@@ -349,12 +330,12 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
, wl_rest = rest, wl_deriv = ders, wl_implics = implics }) , wl_rest = rest, wl_implics = implics })
= null eqs && null rest && null funeqs && isEmptyBag implics && null ders = null eqs && null rest && null funeqs && isEmptyBag implics
emptyWorkList :: WorkList emptyWorkList :: WorkList
emptyWorkList = WL { wl_eqs = [], wl_rest = [] emptyWorkList = WL { wl_eqs = [], wl_rest = []
, wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag } , wl_funeqs = [], wl_implics = emptyBag }
selectWorkItem :: WorkList -> Maybe (Ct, WorkList) selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
-- See Note [Prioritise equalities] -- See Note [Prioritise equalities]
...@@ -369,39 +350,23 @@ getWorkList :: TcS WorkList ...@@ -369,39 +350,23 @@ getWorkList :: TcS WorkList
getWorkList = do { wl_var <- getTcSWorkListRef getWorkList = do { wl_var <- getTcSWorkListRef
; wrapTcS (TcM.readTcRef wl_var) } ; wrapTcS (TcM.readTcRef wl_var) }
selectDerivedWorkItem :: WorkList -> Maybe (Ct, WorkList)
selectDerivedWorkItem wl@(WL { wl_deriv = ders })
| ev:evs <- ders = Just (mkNonCanonical ev, wl { wl_deriv = evs })
| otherwise = Nothing
selectNextWorkItem :: TcS (Maybe Ct) selectNextWorkItem :: TcS (Maybe Ct)
-- Pick which work item to do next -- Pick which work item to do next
-- See Note [Prioritise equalities] -- See Note [Prioritise equalities]
-- See Note [Process derived items last]
selectNextWorkItem selectNextWorkItem
= do { wl_var <- getTcSWorkListRef = do { wl_var <- getTcSWorkListRef
; wl <- wrapTcS (TcM.readTcRef wl_var) ; wl <- wrapTcS (TcM.readTcRef wl_var)
; case selectWorkItem wl of {
; let try :: Maybe (Ct,WorkList) -> TcS (Maybe Ct) -> TcS (Maybe Ct) Nothing -> return Nothing ;
try mb_work do_this_if_fail Just (ct, new_wl) ->
| Just (ct, new_wl) <- mb_work do { checkReductionDepth (ctLoc ct) (ctPred ct)
= do { checkReductionDepth (ctLoc ct) (ctPred ct) ; wrapTcS (TcM.writeTcRef wl_var new_wl)
; wrapTcS (TcM.writeTcRef wl_var new_wl) ; return (Just ct) } } }
; return (Just ct) }
| otherwise
= do_this_if_fail
; try (selectWorkItem wl) $
do { ics <- getInertCans
; if inert_count ics == 0
then return Nothing
else try (selectDerivedWorkItem wl) (return Nothing) } }
-- Pretty printing -- Pretty printing
instance Outputable WorkList where instance Outputable WorkList where
ppr (WL { wl_eqs = eqs, wl_funeqs = feqs ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
, wl_rest = rest, wl_implics = implics, wl_deriv = ders }) , wl_rest = rest, wl_implics = implics })
= text "WL" <+> (braces $ = text "WL" <+> (braces $
vcat [ ppUnless (null eqs) $ vcat [ ppUnless (null eqs) $
text "Eqs =" <+> vcat (map ppr eqs) text "Eqs =" <+> vcat (map ppr eqs)
...@@ -409,8 +374,6 @@ instance Outputable WorkList where ...@@ -409,8 +374,6 @@ instance Outputable WorkList where
text "Funeqs =" <+> vcat (map ppr feqs) text "Funeqs =" <+> vcat (map ppr feqs)
, ppUnless (null rest) $ , ppUnless (null rest) $
text "Non-eqs =" <+> vcat (map ppr rest) text "Non-eqs =" <+> vcat (map ppr rest)
, ppUnless (null ders) $
text "Derived =" <+> vcat (map ppr ders)
, ppUnless (isEmptyBag implics) $ , ppUnless (isEmptyBag implics) $
ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics))) ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics)))
(text "(Implics omitted)") (text "(Implics omitted)")
...@@ -2679,7 +2642,7 @@ buildImplication skol_info skol_tvs givens (TcS thing_inside) ...@@ -2679,7 +2642,7 @@ buildImplication skol_info skol_tvs givens (TcS thing_inside)
do { env <- TcM.getLclEnv do { env <- TcM.getLclEnv
; ev_binds_var <- TcM.newTcEvBinds ; ev_binds_var <- TcM.newTcEvBinds
; let wc = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) && ; let wc = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
null (wl_deriv wl) && null (wl_implics wl), ppr wl ) null (wl_implics wl), ppr wl )
WC { wc_simple = listToCts eqs WC { wc_simple = listToCts eqs
, wc_impl = emptyBag } , wc_impl = emptyBag }
imp = newImplication { ic_tclvl = new_tclvl imp = newImplication { ic_tclvl = new_tclvl
...@@ -3172,12 +3135,6 @@ newWantedNC loc pty ...@@ -3172,12 +3135,6 @@ newWantedNC loc pty
| otherwise | otherwise
= newWantedEvVarNC loc pty = newWantedEvVarNC loc pty
emitNewDerived :: CtLoc -> TcPredType -> TcS ()
emitNewDerived loc pred
= do { ev <- newDerivedNC loc pred
; traceTcS "Emitting new derived" (ppr ev)
; updWorkListTcS (extendWorkListDerived loc ev) }
emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS () emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
emitNewDeriveds loc preds emitNewDeriveds loc preds
| null preds | null preds
...@@ -3185,7 +3142,7 @@ emitNewDeriveds loc preds ...@@ -3185,7 +3142,7 @@ emitNewDeriveds loc preds
| otherwise | otherwise
= do { evs <- mapM (newDerivedNC loc) preds = do { evs <- mapM (newDerivedNC loc) preds
; traceTcS "Emitting new deriveds" (ppr evs) ; traceTcS "Emitting new deriveds" (ppr evs)
; updWorkListTcS (extendWorkListDeriveds loc evs) } ; updWorkListTcS (extendWorkListDeriveds evs) }
emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS () emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
-- Create new equality Derived and put it in the work list -- Create new equality Derived and put it in the work list
...@@ -3194,7 +3151,7 @@ emitNewDerivedEq loc role ty1 ty2 ...@@ -3194,7 +3151,7 @@ emitNewDerivedEq loc role ty1 ty2
= do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2) = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2)
; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc) ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc)
; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) } ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) }
-- Very important: put in the wl_eqs, /not/ wl_derivs -- Very important: put in the wl_eqs
-- See Note [Prioritise equalities] (Avoiding fundep iteration) -- See Note [Prioritise equalities] (Avoiding fundep iteration)
newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
......