Introducing a datatype for WorkLists that properly prioritizes equalities.

We were not prioritizing the interaction of equalities in the worklist, because
pre-canonicalization solved the constraints one by one, in their arrival order.
This patch fixes this, so it's a generally useful improvement, mainly for
efficiency. It makes #4981 go away, although it's not a definite answer to the
cause of the problem. See discussion on Trac.
parent 2d72a852
\begin{code} \begin{code}
module TcCanonical( module TcCanonical(
mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens, mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
canOccursCheck, canEq, canOccursCheck, canEqToWorkList,
rewriteWithFunDeps rewriteWithFunDeps
) where ) where
...@@ -218,28 +218,35 @@ flattenPred ctxt (EqPred ty1 ty2) ...@@ -218,28 +218,35 @@ flattenPred ctxt (EqPred ty1 ty2)
%************************************************************************ %************************************************************************
\begin{code} \begin{code}
canWanteds :: [WantedEvVar] -> TcS CanonicalCts canWanteds :: [WantedEvVar] -> TcS WorkList
canWanteds = fmap andCCans . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev) canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
canGivens :: GivenLoc -> [EvVar] -> TcS CanonicalCts canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens
; return (andCCans ccs) } ; return (unionWorkLists ccs) }
mkCanonicals :: CtFlavor -> [EvVar] -> TcS CanonicalCts mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
mkCanonicals fl vs = fmap andCCans (mapM (mkCanonical fl) vs) mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
mkCanonicalFEV :: FlavoredEvVar -> TcS CanonicalCts mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
mkCanonical :: CtFlavor -> EvVar -> TcS CanonicalCts mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
where -- Preserves order (shouldn't be important, but curently
-- is important for the vectoriser)
canon_one fev wl = do { wl' <- mkCanonicalFEV fev
; return (unionWorkList wl' wl) }
mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
mkCanonical fl ev = case evVarPred ev of mkCanonical fl ev = case evVarPred ev of
ClassP clas tys -> canClass fl ev clas tys ClassP clas tys -> canClassToWorkList fl ev clas tys
IParam ip ty -> canIP fl ev ip ty IParam ip ty -> canIPToWorkList fl ev ip ty
EqPred ty1 ty2 -> canEq fl ev ty1 ty2 EqPred ty1 ty2 -> canEqToWorkList fl ev ty1 ty2
canClass :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS CanonicalCts canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
canClass fl v cn tys canClassToWorkList fl v cn tys
= do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys = do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
; let no_flattening_happened = isEmptyCCan ccs ; let no_flattening_happened = isEmptyCCan ccs
dict_co = mkTyConCoercion (classTyCon cn) cos dict_co = mkTyConCoercion (classTyCon cn) cos
...@@ -256,10 +263,12 @@ canClass fl v cn tys ...@@ -256,10 +263,12 @@ canClass fl v cn tys
-- Add the superclasses of this one here, See Note [Adding superclasses]. -- Add the superclasses of this one here, See Note [Adding superclasses].
-- But only if we are not simplifying the LHS of a rule. -- But only if we are not simplifying the LHS of a rule.
; sctx <- getTcSContext ; sctx <- getTcSContext
; sc_cts <- if simplEqsOnly sctx then return emptyCCan ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
else newSCWorkFromFlavored v_new fl cn xis else newSCWorkFromFlavored v_new fl cn xis
; return (sc_cts `andCCan` ccs `extendCCans` CDictCan { cc_id = v_new ; return (sc_cts `unionWorkList`
workListFromEqs ccs `unionWorkList`
workListFromNonEq CDictCan { cc_id = v_new
, cc_flavor = fl , cc_flavor = fl
, cc_class = cn , cc_class = cn
, cc_tyargs = xis }) } , cc_tyargs = xis }) }
...@@ -330,11 +339,11 @@ happen. ...@@ -330,11 +339,11 @@ happen.
\begin{code} \begin{code}
newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
-- Returns superclasses, see Note [Adding superclasses] -- Returns superclasses, see Note [Adding superclasses]
newSCWorkFromFlavored ev orig_flavor cls xis newSCWorkFromFlavored ev orig_flavor cls xis
| isDerived orig_flavor | isDerived orig_flavor
= return emptyCCan -- Deriveds don't yield more superclasses because we will = return emptyWorkList -- Deriveds don't yield more superclasses because we will
-- add them transitively in the case of wanteds. -- add them transitively in the case of wanteds.
| isGiven orig_flavor | isGiven orig_flavor
...@@ -345,7 +354,7 @@ newSCWorkFromFlavored ev orig_flavor cls xis ...@@ -345,7 +354,7 @@ newSCWorkFromFlavored ev orig_flavor cls xis
; mkCanonicals flavor sc_vars } ; mkCanonicals flavor sc_vars }
| isEmptyVarSet (tyVarsOfTypes xis) | isEmptyVarSet (tyVarsOfTypes xis)
= return emptyCCan -- Wanteds with no variables yield no deriveds. = return emptyWorkList -- Wanteds with no variables yield no deriveds.
-- See Note [Improvement from Ground Wanteds] -- See Note [Improvement from Ground Wanteds]
| otherwise -- Wanted case, just add those SC that can lead to improvement. | otherwise -- Wanted case, just add those SC that can lead to improvement.
...@@ -366,16 +375,20 @@ is_improvement_pty _ = False ...@@ -366,16 +375,20 @@ is_improvement_pty _ = False
canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
-- See Note [Canonical implicit parameter constraints] to see why we don't -- See Note [Canonical implicit parameter constraints] to see why we don't
-- immediately canonicalize (flatten) IP constraints. -- immediately canonicalize (flatten) IP constraints.
canIP fl v nm ty canIPToWorkList fl v nm ty
= return $ singleCCan $ CIPCan { cc_id = v = return $ workListFromNonEq (CIPCan { cc_id = v
, cc_flavor = fl , cc_flavor = fl
, cc_ip_nm = nm , cc_ip_nm = nm
, cc_ip_ty = ty } , cc_ip_ty = ty })
----------------- -----------------
canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2
; return $ workListFromEqs cts }
canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
canEq fl cv ty1 ty2 canEq fl cv ty1 ty2
| tcEqType ty1 ty2 -- Dealing with equality here avoids | tcEqType ty1 ty2 -- Dealing with equality here avoids
...@@ -1020,15 +1033,15 @@ now!). ...@@ -1020,15 +1033,15 @@ now!).
\begin{code} \begin{code}
rewriteWithFunDeps :: [Equation] rewriteWithFunDeps :: [Equation]
-> [Xi] -> CtFlavor -> [Xi] -> CtFlavor
-> TcS (Maybe ([Xi], [Coercion], CanonicalCts)) -> TcS (Maybe ([Xi], [Coercion], WorkList))
rewriteWithFunDeps eqn_pred_locs xis fl rewriteWithFunDeps eqn_pred_locs xis fl
= do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
; let fd_ev_pos :: [(Int,FlavoredEvVar)] ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
fd_ev_pos = concat fd_ev_poss fd_ev_pos = concat fd_ev_poss
(rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis) (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
; let fd_work = unionManyBags fds ; let fd_work = unionWorkLists fds
; if isEmptyBag fd_work ; if isEmptyWorkList fd_work
then return Nothing then return Nothing
else return (Just (rewritten_xis, cos, fd_work)) } else return (Just (rewritten_xis, cos, fd_work)) }
......
...@@ -225,22 +225,6 @@ Note [Basic plan] ...@@ -225,22 +225,6 @@ Note [Basic plan]
type AtomicInert = CanonicalCt -- constraint pulled from InertSet type AtomicInert = CanonicalCt -- constraint pulled from InertSet
type WorkItem = CanonicalCt -- constraint pulled from WorkList type WorkItem = CanonicalCt -- constraint pulled from WorkList
-- A mixture of Given, Wanted, and Derived constraints.
-- We split between equalities and the rest to process equalities first.
type WorkList = CanonicalCts
unionWorkLists :: WorkList -> WorkList -> WorkList
unionWorkLists = andCCan
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList = isEmptyCCan
emptyWorkList :: WorkList
emptyWorkList = emptyCCan
workListFromCCan :: CanonicalCt -> WorkList
workListFromCCan = singleCCan
------------------------ ------------------------
data StopOrContinue data StopOrContinue
= Stop -- Work item is consumed = Stop -- Work item is consumed
...@@ -305,7 +289,7 @@ runSolverPipeline depth pipeline inerts workItem ...@@ -305,7 +289,7 @@ runSolverPipeline depth pipeline inerts workItem
, sr_stop = ContinueWith work_item }) , sr_stop = ContinueWith work_item })
= do { itr <- stage depth work_item inerts = do { itr <- stage depth work_item inerts
; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr) ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr } ; let itr' = itr { sr_new_work = accum_work `unionWorkList` sr_new_work itr }
; run_pipeline stages itr' } ; run_pipeline stages itr' }
\end{code} \end{code}
...@@ -365,8 +349,10 @@ solveInteract inert ws ...@@ -365,8 +349,10 @@ solveInteract inert ws
-> (ct,evVarPred ev)) ws) -> (ct,evVarPred ev)) ws)
, text "inert = " <+> ppr inert ] , text "inert = " <+> ppr inert ]
; (flag, inert_ret) <- foldrBagM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) ws ; can_ws <- mkCanonicalFEVs ws
-- use foldr to preserve the order
; (flag, inert_ret)
<- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws
; traceTcS "solveInteract, after clever canonicalization (and interaction):" $ ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
vcat [ text "No interaction happened = " <+> ppr flag vcat [ text "No interaction happened = " <+> ppr flag
...@@ -374,27 +360,32 @@ solveInteract inert ws ...@@ -374,27 +360,32 @@ solveInteract inert ws
; return (flag, inert_ret) } ; return (flag, inert_ret) }
tryPreSolveAndInteract :: SimplContext tryPreSolveAndInteract :: SimplContext
-> DynFlags -> DynFlags
-> FlavoredEvVar -> CanonicalCt
-> (Bool, InertSet) -> (Bool, InertSet)
-> TcS (Bool, InertSet) -> TcS (Bool, InertSet)
-- Returns: True if it was able to discharge this constraint AND all previous ones -- Returns: True if it was able to discharge this constraint AND all previous ones
tryPreSolveAndInteract sctx dyn_flags flavev@(EvVarX ev_var fl) (all_previous_discharged, inert) tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert)
= do { let inert_cts = get_inert_cts (evVarPred ev_var) = do { let inert_cts = get_inert_cts (evVarPred ev_var)
; this_one_discharged <- dischargeFromCCans inert_cts flavev ; this_one_discharged <-
if isCFrozenErr ct then
return False
else
dischargeFromCCans inert_cts ev_var fl
; if this_one_discharged ; if this_one_discharged
then return (all_previous_discharged, inert) then return (all_previous_discharged, inert)
else do else do
{ extra_cts <- mkCanonical fl ev_var { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert
; inert_ret <- solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) extra_cts inert
; return (False, inert_ret) } } ; return (False, inert_ret) } }
where where
ev_var = cc_id ct
fl = cc_flavor ct
get_inert_cts (ClassP clas _) get_inert_cts (ClassP clas _)
| simplEqsOnly sctx = emptyCCan | simplEqsOnly sctx = emptyCCan
| otherwise = fst (getRelevantCts clas (inert_dicts inert)) | otherwise = fst (getRelevantCts clas (inert_dicts inert))
...@@ -405,12 +396,12 @@ tryPreSolveAndInteract sctx dyn_flags flavev@(EvVarX ev_var fl) (all_previous_di ...@@ -405,12 +396,12 @@ tryPreSolveAndInteract sctx dyn_flags flavev@(EvVarX ev_var fl) (all_previous_di
get_inert_cts (EqPred {}) get_inert_cts (EqPred {})
= inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert) = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
dischargeFromCCans :: CanonicalCts -> FlavoredEvVar -> TcS Bool dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool
-- See if this (pre-canonicalised) work-item is identical to a -- See if this (pre-canonicalised) work-item is identical to a
-- one already in the inert set. Reasons: -- one already in the inert set. Reasons:
-- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints -- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints
-- b) Termination for improve_eqs in TcSimplify.simpl_loop -- b) Termination for improve_eqs in TcSimplify.simpl_loop
dischargeFromCCans cans (EvVarX ev fl) dischargeFromCCans cans ev fl
= Bag.foldrBag discharge_ct (return False) cans = Bag.foldrBag discharge_ct (return False) cans
where where
the_pred = evVarPred ev the_pred = evVarPred ev
...@@ -469,10 +460,8 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert ...@@ -469,10 +460,8 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert
, text "Max depth =" <+> ppr max_depth , text "Max depth =" <+> ppr max_depth
, text "ws =" <+> ppr ws ] , text "ws =" <+> ppr ws ]
-- Solve equalities first
; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws ; foldrWorkListM (solveOneWithDepth ctxt) inert ws }
; is_from_eqs <- Bag.foldrBagM (solveOneWithDepth ctxt) inert eqs
; Bag.foldrBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
-- use foldr to preserve the order -- use foldr to preserve the order
------------------ ------------------
...@@ -893,7 +882,7 @@ interactNext depth inert it ...@@ -893,7 +882,7 @@ interactNext depth inert it
= text rule <+> keep_doc = text rule <+> keep_doc
<+> vcat [ ptext (sLit "Inert =") <+> ppr inert <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
, ptext (sLit "Work =") <+> ppr work_item , ptext (sLit "Work =") <+> ppr work_item
, ppUnless (isEmptyBag new_work) $ , ppUnless (isEmptyWorkList new_work) $
ptext (sLit "New =") <+> ppr new_work ] ptext (sLit "New =") <+> ppr new_work ]
keep_doc = case inert_action of keep_doc = case inert_action of
KeepInert -> ptext (sLit "[keep]") KeepInert -> ptext (sLit "[keep]")
...@@ -909,7 +898,7 @@ interactNext depth inert it ...@@ -909,7 +898,7 @@ interactNext depth inert it
DropInert -> inerts DropInert -> inerts
; return $ SR { sr_inerts = inerts_new ; return $ SR { sr_inerts = inerts_new
, sr_new_work = sr_new_work it `unionWorkLists` new_work , sr_new_work = sr_new_work it `unionWorkList` new_work
, sr_stop = stop } } , sr_stop = stop } }
| otherwise | otherwise
= return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert } = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
...@@ -971,8 +960,8 @@ doInteractWithInert ...@@ -971,8 +960,8 @@ doInteractWithInert
-- and put it back into the work-list -- and put it back into the work-list
-- Maybe rather than starting again, we could *replace* the -- Maybe rather than starting again, we could *replace* the
-- inert item, but its safe and simple to restart -- inert item, but its safe and simple to restart
; mkIRStopD "Cls/Cls fundep (solved)" (inert_w `consBag` fd_work) } ; mkIRStopD "Cls/Cls fundep (solved)" $
workListFromNonEq inert_w `unionWorkList` fd_work }
| otherwise | otherwise
-> do { setDictBind d2 (EvCast d1 dict_co) -> do { setDictBind d2 (EvCast d1 dict_co)
; mkIRStopK "Cls/Cls fundep (solved)" fd_work } ; mkIRStopK "Cls/Cls fundep (solved)" fd_work }
...@@ -998,7 +987,8 @@ doInteractWithInert ...@@ -998,7 +987,8 @@ doInteractWithInert
Wanted {} -> setDictBind d2 (EvCast d2' dict_co) Wanted {} -> setDictBind d2 (EvCast d2' dict_co)
Derived {} -> return () Derived {} -> return ()
; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 } ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 }
; mkIRStopK "Cls/Cls fundep (partial)" (workItem' `consBag` fd_work) } ; mkIRStopK "Cls/Cls fundep (partial)" $
workListFromNonEq workItem' `unionWorkList` fd_work }
where where
dict_co = mkTyConCoercion (classTyCon cls1) cos2 dict_co = mkTyConCoercion (classTyCon cls1) cos2
...@@ -1020,7 +1010,7 @@ doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_t ...@@ -1020,7 +1010,7 @@ doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_t
| wfl `canRewrite` ifl | wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfTypes xis , tv `elemVarSet` tyVarsOfTypes xis
= do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis) = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
; mkIRContinue "Cls/Eq" workItem DropInert (workListFromCCan rewritten_dict) } ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) }
-- Class constraint and given equality: use the equality to rewrite -- Class constraint and given equality: use the equality to rewrite
-- the class constraint. -- the class constraint.
...@@ -1036,7 +1026,7 @@ doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_i ...@@ -1036,7 +1026,7 @@ doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_i
| wfl `canRewrite` ifl | wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfType ty , tv `elemVarSet` tyVarsOfType ty
= do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty) = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
; mkIRContinue "IP/Eq" workItem DropInert (workListFromCCan rewritten_ip) } ; mkIRContinue "IP/Eq" workItem DropInert (workListFromNonEq rewritten_ip) }
-- Two implicit parameter constraints. If the names are the same, -- Two implicit parameter constraints. If the names are the same,
-- but their types are not, we generate a wanted type equality -- but their types are not, we generate a wanted type equality
...@@ -1075,7 +1065,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_ ...@@ -1075,7 +1065,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_
| ifl `canRewrite` wfl | ifl `canRewrite` wfl
, tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
= do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
; mkIRStopK "Eq/FunEq" (workListFromCCan rewritten_funeq) } ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) }
-- Must Stop here, because we may no longer be inert after the rewritting. -- Must Stop here, because we may no longer be inert after the rewritting.
-- Inert: function equality, work item: equality -- Inert: function equality, work item: equality
...@@ -1085,7 +1075,7 @@ doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc ...@@ -1085,7 +1075,7 @@ doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
| wfl `canRewrite` ifl | wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
= do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromCCan rewritten_funeq) } ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromEq rewritten_funeq) }
-- One may think that we could (KeepTransformedInert rewritten_funeq) -- One may think that we could (KeepTransformedInert rewritten_funeq)
-- but that is wrong, because it may end up not being inert with respect -- but that is wrong, because it may end up not being inert with respect
-- to future inerts. Example: -- to future inerts. Example:
...@@ -1214,7 +1204,7 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) ...@@ -1214,7 +1204,7 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
| Just tv2' <- tcGetTyVar_maybe xi2' | Just tv2' <- tcGetTyVar_maybe xi2'
, tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
= do { when (isWanted gw) (setCoBind cv2 (mkSymCoercion co2')) = do { when (isWanted gw) (setCoBind cv2 (mkSymCoercion co2'))
; return emptyCCan } ; return emptyWorkList }
| otherwise | otherwise
= do { cv2' <- newCoVar (mkTyVarTy tv2) xi2' = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
; case gw of ; case gw of
...@@ -1223,7 +1213,7 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) ...@@ -1223,7 +1213,7 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
Given {} -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion` Given {} -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion`
co2' co2'
Derived {} -> return () Derived {} -> return ()
; canEq gw cv2' (mkTyVarTy tv2) xi2' } ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
where where
xi2' = substTyWith [tv1] [xi1] xi2 xi2' = substTyWith [tv1] [xi1] xi2
co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1] co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
...@@ -1269,7 +1259,7 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) ...@@ -1269,7 +1259,7 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
Derived {} -> return () Derived {} -> return ()
; return (singleCCan $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) } ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
where where
(ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b
ty2a' = substTyWith [tv1] [xi1] ty2a ty2a' = substTyWith [tv1] [xi1] ty2a
...@@ -1750,7 +1740,7 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc) ...@@ -1750,7 +1740,7 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl, ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
cc_class = cls, cc_tyargs = xis' } cc_class = cls, cc_tyargs = xis' }
; return $ ; return $
SomeTopInt { tir_new_work = singleCCan workItem' `andCCan` fd_work SomeTopInt { tir_new_work = workListFromNonEq workItem' `unionWorkList` fd_work
, tir_new_inert = Stop } } } , tir_new_inert = Stop } } }
GenInst wtvs ev_term -- Solved GenInst wtvs ev_term -- Solved
......
...@@ -8,6 +8,10 @@ module TcSMonad ( ...@@ -8,6 +8,10 @@ module TcSMonad (
isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe, isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
isCFrozenErr, isCFrozenErr,
WorkList, unionWorkList, unionWorkLists, isEmptyWorkList, emptyWorkList,
workListFromEq, workListFromNonEq,
workListFromEqs, workListFromNonEqs, foldrWorkListM,
CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
deCanonicalise, mkFrozenError, deCanonicalise, mkFrozenError,
...@@ -257,8 +261,58 @@ isCFunEqCan_Maybe _ = Nothing ...@@ -257,8 +261,58 @@ isCFunEqCan_Maybe _ = Nothing
isCFrozenErr :: CanonicalCt -> Bool isCFrozenErr :: CanonicalCt -> Bool
isCFrozenErr (CFrozenErr {}) = True isCFrozenErr (CFrozenErr {}) = True
isCFrozenErr _ = False isCFrozenErr _ = False
-- A mixture of Given, Wanted, and Derived constraints.
-- We split between equalities and the rest to process equalities first.
data WorkList = WorkList { weqs :: CanonicalCts
-- NB: weqs includes equalities /and/ family equalities
, wrest :: CanonicalCts }
unionWorkList :: WorkList -> WorkList -> WorkList
unionWorkList wl1 wl2
= WorkList { weqs = weqs wl1 `andCCan` weqs wl2
, wrest = wrest wl1 `andCCan` wrest wl2 }
unionWorkLists :: [WorkList] -> WorkList
unionWorkLists = foldr unionWorkList emptyWorkList
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList wl = isEmptyCCan (weqs wl) && isEmptyCCan (wrest wl)
emptyWorkList :: WorkList
emptyWorkList
= WorkList { weqs = emptyBag, wrest = emptyBag }
workListFromEq :: CanonicalCt -> WorkList
workListFromEq = workListFromEqs . singleCCan
workListFromNonEq :: CanonicalCt -> WorkList
workListFromNonEq = workListFromNonEqs . singleCCan
workListFromNonEqs :: CanonicalCts -> WorkList
workListFromNonEqs cts
= WorkList { weqs = emptyCCan, wrest = cts }
workListFromEqs :: CanonicalCts -> WorkList
workListFromEqs cts
= WorkList { weqs = cts, wrest = emptyCCan }
foldrWorkListM :: (Monad m) => (CanonicalCt -> r -> m r)
-> r -> WorkList -> m r
-- Prioritizes equalities
foldrWorkListM on_ct r (WorkList {weqs = eqs, wrest = rest })
= do { r1 <- foldrBagM on_ct r eqs
; foldrBagM on_ct r1 rest }
instance Outputable WorkList where
ppr wl = vcat [ text "WorkList (Equalities) = " <+> ppr (weqs wl)
, text "WorkList (Other) = " <+> ppr (wrest wl) ]
\end{code} \end{code}
%************************************************************************ %************************************************************************
%* * %* *
CtFlavor CtFlavor
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment