Skip to content

Commit

Permalink
Introducing a datatype for WorkLists that properly prioritizes equali…
Browse files Browse the repository at this point in the history 
…ties.

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.
  • Loading branch information
dimitris@microsoft.com committed Mar 31, 2011
1 parent 2d72a85 commit 5cfe9e9
Show file tree
Hide file tree
Showing 3 changed files with 137 additions and 80 deletions.
81 changes: 47 additions & 34 deletions compiler/typecheck/TcCanonical.lhs
View file
Original file line number Original file line Diff line number Diff line change
@@ -1,7 +1,7 @@
\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
Expand Down Expand Up @@ -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
Expand All @@ -256,13 +263,15 @@ 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`
, cc_flavor = fl workListFromEqs ccs `unionWorkList`
, cc_class = cn workListFromNonEq CDictCan { cc_id = v_new
, cc_tyargs = xis }) } , cc_flavor = fl
, cc_class = cn
, cc_tyargs = xis }) }
\end{code} \end{code}


Note [Adding superclasses] Note [Adding superclasses]
Expand Down Expand Up @@ -330,12 +339,12 @@ 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
= do { let sc_theta = immSuperClasses cls xis = do { let sc_theta = immSuperClasses cls xis
Expand All @@ -345,8 +354,8 @@ 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.
= do { let sc_rec_theta = transSuperClasses cls xis = do { let sc_rec_theta = transSuperClasses cls xis
Expand All @@ -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
Expand Down Expand Up @@ -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)) }
Expand Down
82 changes: 36 additions & 46 deletions compiler/typecheck/TcInteract.lhs
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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}


Expand Down Expand Up @@ -365,36 +349,43 @@ 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
, text "inert_ret = " <+> ppr inert_ret ] , text "inert_ret = " <+> ppr inert_ret ]
; 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))
Expand All @@ -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
Expand Down Expand Up @@ -469,11 +460,9 @@ 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 -- use foldr to preserve the order
; Bag.foldrBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
-- use foldr to preserve the order
------------------ ------------------
-- Fully interact the given work item with an inert set, and return a -- Fully interact the given work item with an inert set, and return a
Expand Down Expand Up @@ -834,7 +823,7 @@ data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
interactWithInertEqsStage :: SimplifierStage interactWithInertEqsStage :: SimplifierStage
interactWithInertEqsStage depth workItem inert interactWithInertEqsStage depth workItem inert
= Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert) = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert)
-- use foldr to preserve the order -- use foldr to preserve the order
where where
initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan } initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan }
, sr_new_work = emptyWorkList , sr_new_work = emptyWorkList
Expand Down Expand Up @@ -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]")
Expand All @@ -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 }
Expand Down Expand Up @@ -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 }
Expand All @@ -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
Expand All @@ -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.
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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:
Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit 5cfe9e9

Please sign in to comment.