X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=4a049aa3eee6ab0233f7c5a3a674897d85286c0a;hp=f9d3d97cdca23eee6c19fe67ce66b34b3cd3f4b4;hb=5cfe9e92a92201043d5dbb1c4e10fef0ed0d9f49;hpb=27310213397bb89555bb03585e057ba1b017e895 diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index f9d3d97..4a049aa 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -20,7 +20,6 @@ import TcType import HsBinds import Inst( tyVarsOfEvVar ) -import InstEnv import Class import TyCon import Name @@ -226,22 +225,6 @@ Note [Basic plan] type AtomicInert = CanonicalCt -- constraint pulled from InertSet 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 = Stop -- Work item is consumed @@ -270,21 +253,24 @@ instance Outputable StageResult where , ptext (sLit "new work =") <+> ppr work <> comma , ptext (sLit "stop =") <+> ppr stop]) -type SimplifierStage = WorkItem -> InertSet -> TcS StageResult +type SubGoalDepth = Int -- Starts at zero; used to limit infinite + -- recursion of sub-goals +type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult -- Combine a sequence of simplifier 'stages' to create a pipeline -runSolverPipeline :: [(String, SimplifierStage)] - -> InertSet -> WorkItem +runSolverPipeline :: SubGoalDepth + -> [(String, SimplifierStage)] + -> InertSet -> WorkItem -> TcS (InertSet, WorkList) -- Precondition: non-empty list of stages -runSolverPipeline pipeline inerts workItem +runSolverPipeline depth pipeline inerts workItem = do { traceTcS "Start solver pipeline" $ vcat [ ptext (sLit "work item =") <+> ppr workItem , ptext (sLit "inerts =") <+> ppr inerts] ; let itr_in = SR { sr_inerts = inerts - , sr_new_work = emptyWorkList - , sr_stop = ContinueWith workItem } + , sr_new_work = emptyWorkList + , sr_stop = ContinueWith workItem } ; itr_out <- run_pipeline pipeline itr_in ; let new_inert = case sr_stop itr_out of @@ -301,9 +287,9 @@ runSolverPipeline pipeline inerts workItem (SR { sr_new_work = accum_work , sr_inerts = inerts , sr_stop = ContinueWith work_item }) - = do { itr <- stage work_item inerts + = do { itr <- stage depth work_item inerts ; 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' } \end{code} @@ -363,7 +349,10 @@ solveInteract inert ws -> (ct,evVarPred ev)) ws) , text "inert = " <+> ppr inert ] - ; (flag, inert_ret) <- foldlBagM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) ws + ; can_ws <- mkCanonicalFEVs ws + + ; (flag, inert_ret) + <- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $ vcat [ text "No interaction happened = " <+> ppr flag @@ -371,29 +360,32 @@ solveInteract inert ws ; return (flag, inert_ret) } - tryPreSolveAndInteract :: SimplContext -> DynFlags + -> CanonicalCt -> (Bool, InertSet) - -> FlavoredEvVar -> TcS (Bool, InertSet) -- Returns: True if it was able to discharge this constraint AND all previous ones -tryPreSolveAndInteract sctx dyn_flags (all_previous_discharged, inert) - flavev@(EvVarX ev_var fl) +tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert) = 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 then return (all_previous_discharged, inert) else do - { extra_cts <- mkCanonical fl ev_var - ; inert_ret <- solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) - inert extra_cts + { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert ; return (False, inert_ret) } } where + ev_var = cc_id ct + fl = cc_flavor ct + get_inert_cts (ClassP clas _) | simplEqsOnly sctx = emptyCCan | otherwise = fst (getRelevantCts clas (inert_dicts inert)) @@ -404,21 +396,30 @@ tryPreSolveAndInteract sctx dyn_flags (all_previous_discharged, inert) get_inert_cts (EqPred {}) = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert) -dischargeFromCCans :: CanonicalCts -> FlavoredEvVar -> TcS Bool -dischargeFromCCans cans (EvVarX ev fl) - = Bag.foldlBagM discharge_ct False cans - where discharge_ct :: Bool -> CanonicalCt -> TcS Bool - discharge_ct True _ct = return True - discharge_ct False ct - | evVarPred (cc_id ct) `tcEqPred` evVarPred ev - , cc_flavor ct `canSolve` fl - = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) - ; return True } - where set_ev_bind x y - | EqPred {} <- evVarPred y - = setEvBind x (EvCoercion (mkCoVarCoercion y)) - | otherwise = setEvBind x (EvId y) - discharge_ct False _ct = return False +dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool +-- See if this (pre-canonicalised) work-item is identical to a +-- one already in the inert set. Reasons: +-- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints +-- b) Termination for improve_eqs in TcSimplify.simpl_loop +dischargeFromCCans cans ev fl + = Bag.foldrBag discharge_ct (return False) cans + where + the_pred = evVarPred ev + + discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool + discharge_ct ct _rest + | evVarPred (cc_id ct) `tcEqPred` the_pred + , cc_flavor ct `canSolve` fl + = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) + -- Deriveds need no evidence + -- For Givens, we already have evidence, and we don't need it twice + ; return True } + where + set_ev_bind x y + | EqPred {} <- evVarPred y = setEvBind x (EvCoercion (mkCoVarCoercion y)) + | otherwise = setEvBind x (EvId y) + + discharge_ct _ct rest = rest \end{code} Note [Avoiding the superclass explosion] @@ -437,16 +438,16 @@ canonicals. If so, we add nothing to the returned canonical constraints. \begin{code} -solveOne :: InertSet -> WorkItem -> TcS InertSet -solveOne inerts workItem +solveOne :: WorkItem -> InertSet -> TcS InertSet +solveOne workItem inerts = do { dyn_flags <- getDynFlags - ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem + ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts } ----------------- solveInteractWithDepth :: (Int, Int, [WorkItem]) - -> InertSet -> WorkList -> TcS InertSet -solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws + -> WorkList -> InertSet -> TcS InertSet +solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert | isEmptyWorkList ws = return inert @@ -456,33 +457,29 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws | otherwise = do { traceTcS "solveInteractWithDepth" $ vcat [ text "Current depth =" <+> ppr n - , text "Max depth =" <+> ppr max_depth ] + , text "Max depth =" <+> ppr max_depth + , text "ws =" <+> ppr ws ] + - -- Solve equalities first - ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws - ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs - ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs } + ; foldrWorkListM (solveOneWithDepth ctxt) inert ws } + -- use foldr to preserve the order ------------------ -- Fully interact the given work item with an inert set, and return a -- new inert set which has assimilated the new information. solveOneWithDepth :: (Int, Int, [WorkItem]) - -> InertSet -> WorkItem -> TcS InertSet -solveOneWithDepth (max_depth, n, stack) inert work - = do { traceTcS0 (indent ++ "Solving {") (ppr work) - ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work + -> WorkItem -> InertSet -> TcS InertSet +solveOneWithDepth (max_depth, depth, stack) work inert + = do { traceFireTcS depth (text "Solving {" <+> ppr work) + ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work - ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work) - -- Recursively solve the new work generated -- from workItem, with a greater depth - ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack) - new_inert new_work + ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_work new_inert + + ; traceFireTcS depth (text "Done }" <+> ppr work) - ; traceTcS0 (indent ++ "Done }") (ppr work) ; return res_inert } - where - indent = replicate (2*n) ' ' thePipeline :: [(String,SimplifierStage)] thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage) @@ -524,7 +521,7 @@ Case 3: IP improvement work \begin{code} spontaneousSolveStage :: SimplifierStage -spontaneousSolveStage workItem inerts +spontaneousSolveStage depth workItem inerts = do { mSolve <- trySpontaneousSolve workItem ; case mSolve of @@ -540,7 +537,9 @@ spontaneousSolveStage workItem inerts -- its status change. This in turn may produce more work. -- We do this *right now* (rather than just putting workItem' -- back into the work-list) because we've solved - -> do { (new_inert, new_work) <- runSolverPipeline + -> do { bumpStepCountTcS + ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem) + ; (new_inert, new_work) <- runSolverPipeline depth [ ("recursive interact with inert eqs", interactWithInertEqsStage) , ("recursive interact with inerts", interactWithInertsStage) ] inerts workItem' @@ -551,9 +550,11 @@ spontaneousSolveStage workItem inerts | otherwise -> -- Original was given; he must then be inert all right, and -- workList' are all givens from flattening - return $ SR { sr_new_work = emptyWorkList - , sr_inerts = inerts `updInertSet` workItem' - , sr_stop = Stop } + do { bumpStepCountTcS + ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem) + ; return $ SR { sr_new_work = emptyWorkList + , sr_inerts = inerts `updInertSet` workItem' + , sr_stop = Stop } } SPError -> -- Return with no new work return $ SR { sr_new_work = emptyWorkList , sr_inerts = inerts @@ -584,7 +585,8 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = | otherwise = do { tch1 <- isTouchableMetaTyVar tv1 ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi - else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem) + else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" + (ppr workItem) ; return SPCantSolve } } @@ -725,7 +727,7 @@ solveWithIdentity cv wd tv xi ; setWantedTyBind tv xi ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi - ; when (isWanted wd) (setWantedCoBind cv xi) + ; when (isWanted wd) (setCoBind cv xi) -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)' ; return $ SPSolved (CTyEqCan { cc_id = cv_given @@ -734,14 +736,37 @@ solveWithIdentity cv wd tv xi \end{code} - - ********************************************************************************* * * The interact-with-inert Stage * * ********************************************************************************* +Note [The Solver Invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We always add Givens first. So you might think that the solver has +the invariant + + If the work-item is Given, + then the inert item must Given + +But this isn't quite true. Suppose we have, + c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int +After processing the first two, we get + c1: [G] beta ~ [alpha], c2 : [W] blah +Now, c3 does not interact with the the given c1, so when we spontaneously +solve c3, we must re-react it with the inert set. So we can attempt a +reaction between inert c2 [W] and work-item c3 [G]. + +It *is* true that [Solver Invariant] + If the work-item is Given, + AND there is a reaction + then the inert item must Given +or, equivalently, + If the work-item is Given, + and the inert item is Wanted/Derived + then there is no reaction + \begin{code} -- Interaction result of WorkItem <~> AtomicInert data InteractResult @@ -758,24 +783,32 @@ data InteractResult , ir_new_work :: WorkList -- new work items to add to the WorkList + + , ir_fire :: Maybe String -- Tells whether a rule fired, and if so what } -- What to do with the inert reactant. -data InertAction = KeepInert - | DropInert - | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert +data InertAction = KeepInert | DropInert -mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult -mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork +mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult +mkIRContinue rule wi keep newWork + = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep + , ir_new_work = newWork, ir_fire = Just rule } -mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult -mkIRStop keep newWork = return $ IR Stop keep newWork +mkIRStopK :: String -> WorkList -> TcS InteractResult +mkIRStopK rule newWork + = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert + , ir_new_work = newWork, ir_fire = Just rule } -dischargeWorkItem :: Monad m => m InteractResult -dischargeWorkItem = mkIRStop KeepInert emptyWorkList +mkIRStopD :: String -> WorkList -> TcS InteractResult +mkIRStopD rule newWork + = return $ IR { ir_stop = Stop, ir_inert_action = DropInert + , ir_new_work = newWork, ir_fire = Just rule } noInteraction :: Monad m => WorkItem -> m InteractResult -noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList +noInteraction wi + = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert + , ir_new_work = emptyWorkList, ir_fire = Nothing } data WhichComesFromInert = LeftComesFromInert | RightComesFromInert -- See Note [Efficient Orientation] @@ -788,8 +821,9 @@ data WhichComesFromInert = LeftComesFromInert | RightComesFromInert -- interact the WorkItem with the entire equalities of the InertSet interactWithInertEqsStage :: SimplifierStage -interactWithInertEqsStage workItem inert - = Bag.foldlBagM interactNext initITR (inert_eqs inert) +interactWithInertEqsStage depth workItem inert + = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert) + -- use foldr to preserve the order where initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan } , sr_new_work = emptyWorkList @@ -802,12 +836,13 @@ interactWithInertEqsStage workItem inert -- "Other" constraints it contains! interactWithInertsStage :: SimplifierStage -interactWithInertsStage workItem inert +interactWithInertsStage depth workItem inert = let (relevant, inert_residual) = getISRelevant workItem inert initITR = SR { sr_inerts = inert_residual , sr_new_work = emptyWorkList , sr_stop = ContinueWith workItem } - in Bag.foldlBagM interactNext initITR relevant + in Bag.foldrBagM (interactNext depth) initITR relevant + -- use foldr to preserve the order where getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) getISRelevant (CFrozenErr {}) is = (emptyCCan, is) @@ -834,37 +869,51 @@ interactWithInertsStage workItem inert , inert_ips = emptyCCanMap , inert_funeqs = emptyCCanMap }) -interactNext :: StageResult -> AtomicInert -> TcS StageResult -interactNext it inert - | ContinueWith workItem <- sr_stop it - = do { let inerts = sr_inerts it - - ; ir <- interactWithInert inert workItem - - -- New inerts depend on whether we KeepInert or not and must - -- be updated with FD improvement information from the interaction result (ir) - ; let inerts_new = case ir_inert_action ir of - KeepInert -> inerts `updInertSet` inert - DropInert -> inerts - KeepTransformedInert inert' -> inerts `updInertSet` inert' +interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult +interactNext depth inert it + | ContinueWith work_item <- sr_stop it + = do { let inerts = sr_inerts it + + ; IR { ir_new_work = new_work, ir_inert_action = inert_action + , ir_fire = fire_info, ir_stop = stop } + <- interactWithInert inert work_item + + ; let mk_msg rule + = text rule <+> keep_doc + <+> vcat [ ptext (sLit "Inert =") <+> ppr inert + , ptext (sLit "Work =") <+> ppr work_item + , ppUnless (isEmptyWorkList new_work) $ + ptext (sLit "New =") <+> ppr new_work ] + keep_doc = case inert_action of + KeepInert -> ptext (sLit "[keep]") + DropInert -> ptext (sLit "[drop]") + ; case fire_info of + Just rule -> do { bumpStepCountTcS + ; traceFireTcS depth (mk_msg rule) } + Nothing -> return () + + -- New inerts depend on whether we KeepInert or not + ; let inerts_new = case inert_action of + KeepInert -> inerts `updInertSet` inert + DropInert -> inerts ; return $ SR { sr_inerts = inerts_new - , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir - , sr_stop = ir_stop ir } } + , sr_new_work = sr_new_work it `unionWorkList` new_work + , sr_stop = stop } } | otherwise = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert } -- Do a single interaction of two constraints. interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult -interactWithInert inert workitem - = do { ctxt <- getTcSContext - ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem +interactWithInert inert workItem + = do { ctxt <- getTcSContext + ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workItem - ; if is_allowed then - doInteractWithInert inert workitem + ; if is_allowed then + doInteractWithInert inert workItem else - noInteraction workitem - } + noInteraction workItem + } allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool -- Allowed interactions @@ -877,27 +926,73 @@ doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult -- Identical class constraints. doInteractWithInert - (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) - workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) + inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) + workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2) - = solveOneFromTheOther (d1,fl1) workItem + = solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2)) = -- See Note [When improvement happens] do { let pty1 = ClassP cls1 tys1 pty2 = ClassP cls2 tys2 - work_item_pred_loc = (pty2, pprFlavorArising fl2) inert_pred_loc = (pty1, pprFlavorArising fl1) - loc = combineCtLoc fl1 fl2 - eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc - -- See Note [Efficient Orientation] - - ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs - ; fd_work <- mapM mkCanonicalFEV derived_evs - -- See Note [Generating extra equalities] - - ; mkIRContinue workItem KeepInert (unionManyBags fd_work) - } + work_item_pred_loc = (pty2, pprFlavorArising fl2) + fd_eqns = improveFromAnother + inert_pred_loc -- the template + work_item_pred_loc -- the one we aim to rewrite + -- See Note [Efficient Orientation] + + ; m <- rewriteWithFunDeps fd_eqns tys2 fl2 + ; case m of + Nothing -> noInteraction workItem + Just (rewritten_tys2, cos2, fd_work) + | tcEqTypes tys1 rewritten_tys2 + -> -- Solve him on the spot in this case + case fl2 of + Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem) + Derived {} -> mkIRStopK "Cls/Cls fundep (solved)" fd_work + Wanted {} + | isDerived fl1 + -> do { setDictBind d2 (EvCast d1 dict_co) + ; let inert_w = inertItem { cc_flavor = fl2 } + -- A bit naughty: we take the inert Derived, + -- turn it into a Wanted, use it to solve the work-item + -- and put it back into the work-list + -- Maybe rather than starting again, we could *replace* the + -- inert item, but its safe and simple to restart + ; mkIRStopD "Cls/Cls fundep (solved)" $ + workListFromNonEq inert_w `unionWorkList` fd_work } + | otherwise + -> do { setDictBind d2 (EvCast d1 dict_co) + ; mkIRStopK "Cls/Cls fundep (solved)" fd_work } + + | otherwise + -> -- We could not quite solve him, but we still rewrite him + -- Example: class C a b c | a -> b + -- Given: C Int Bool x, Wanted: C Int beta y + -- Then rewrite the wanted to C Int Bool y + -- but note that is still not identical to the given + -- The important thing is that the rewritten constraint is + -- inert wrt the given. + -- However it is not necessarily inert wrt previous inert-set items. + -- class C a b c d | a -> b, b c -> d + -- Inert: c1: C b Q R S, c2: C P Q a b + -- Work: C P alpha R beta + -- Does not react with c1; reacts with c2, with alpha:=Q + -- NOW it reacts with c1! + -- So we must stop, and put the rewritten constraint back in the work list + do { d2' <- newDictVar cls1 rewritten_tys2 + ; case fl2 of + Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem) + Wanted {} -> setDictBind d2 (EvCast d2' dict_co) + Derived {} -> return () + ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 } + ; mkIRStopK "Cls/Cls fundep (partial)" $ + workListFromNonEq workItem' `unionWorkList` fd_work } + + where + dict_co = mkTyConCoercion (classTyCon cls1) cos2 + } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. @@ -908,14 +1003,14 @@ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_r = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis) -- Continue with rewritten Dictionary because we can only be in the -- interactWithEqsStage, so the dictionary is inert. - ; mkIRContinue rewritten_dict KeepInert emptyWorkList } + ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList } doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi }) | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfTypes xis = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis) - ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) } + ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. @@ -924,14 +1019,14 @@ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_r | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfType ty = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty) - ; mkIRContinue rewritten_ip KeepInert emptyWorkList } + ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList } doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi }) | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfType ty = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty) - ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) } + ; mkIRContinue "IP/Eq" workItem DropInert (workListFromNonEq rewritten_ip) } -- Two implicit parameter constraints. If the names are the same, -- but their types are not, we generate a wanted type equality @@ -944,19 +1039,19 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i = -- See Note [Overriding implicit parameters] -- Dump the inert item, override totally with the new one -- Do not require type equality - mkIRContinue workItem DropInert emptyWorkList + -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ... + -- we must *override* the outer one with the inner one + mkIRContinue "IP/IP override" workItem DropInert emptyWorkList | nm1 == nm2 && ty1 `tcEqType` ty2 - = solveOneFromTheOther (id1,ifl) workItem + = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem | nm1 == nm2 = -- See Note [When improvement happens] - do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation] + do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation] ; let flav = Wanted (combineCtLoc ifl wfl) ; cans <- mkCanonical flav co_var - ; mkIRContinue workItem KeepInert cans } - - + ; mkIRContinue "IP/IP fundep" workItem KeepInert cans } -- Never rewrite a given with a wanted equality, and a type function -- equality can never rewrite an equality. We rewrite LHS *and* RHS @@ -970,7 +1065,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_ | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) - ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) } + ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) } -- Must Stop here, because we may no longer be inert after the rewritting. -- Inert: function equality, work item: equality @@ -980,7 +1075,7 @@ doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) - ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) } + ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromEq 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 -- to future inerts. Example: @@ -996,10 +1091,10 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 , cc_tyargs = args2, cc_rhs = xi2 }) | fl1 `canSolve` fl2 && lhss_match = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert cans } + ; mkIRStopK "FunEq/FunEq" cans } | fl2 `canSolve` fl1 && lhss_match = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert cans } + ; mkIRContinue "FunEq/FunEq" workItem DropInert cans } where lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) @@ -1008,30 +1103,32 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert cans } + ; mkIRStopK "Eq/Eq lhs" cans } | fl2 `canSolve` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert cans } + ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans } + -- Check for rewriting RHS | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2) - ; mkIRStop KeepInert rewritten_eq } + ; mkIRStopK "Eq/Eq rhs" rewritten_eq } + | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) - ; mkIRContinue workItem DropInert rewritten_eq } + ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq } doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) (CFrozenErr { cc_id = cv2, cc_flavor = fl2 }) | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) - ; mkIRStop KeepInert rewritten_frozen } + ; mkIRStopK "Frozen/Eq" rewritten_frozen } doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 }) workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) - ; mkIRContinue workItem DropInert rewritten_frozen } + ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen } -- Fall-through case for all other situations doInteractWithInert _ workItem = noInteraction workItem @@ -1078,16 +1175,16 @@ rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F ar xi2' = substTyWith [tv] [xi1] xi2 xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2' - ; cv2' <- case gw of - Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2' - ; setWantedCoBind cv2 $ - fun_co `mkTransCoercion` - mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co - ; return cv2' } - Given {} -> newGivenCoVar (mkTyConApp tc args') xi2' $ - mkSymCoercion fun_co `mkTransCoercion` - mkCoVarCoercion cv2 `mkTransCoercion` xi2_co - Derived {} -> newDerivedId (EqPred (mkTyConApp tc args') xi2') + + ; cv2' <- newCoVar (mkTyConApp tc args') xi2' + ; case gw of + Wanted {} -> setCoBind cv2 (fun_co `mkTransCoercion` + mkCoVarCoercion cv2' `mkTransCoercion` + mkSymCoercion xi2_co) + Given {} -> setCoBind cv2' (mkSymCoercion fun_co `mkTransCoercion` + mkCoVarCoercion cv2 `mkTransCoercion` + xi2_co) + Derived {} -> return () ; return (CFunEqCan { cc_id = cv2' , cc_flavor = gw @@ -1106,79 +1203,63 @@ rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkLis rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) | Just tv2' <- tcGetTyVar_maybe xi2' , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2 - = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2')) - ; return emptyCCan } + = do { when (isWanted gw) (setCoBind cv2 (mkSymCoercion co2')) + ; return emptyWorkList } | otherwise - = do { cv2' <- - case gw of - Wanted {} - -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2' - ; setWantedCoBind cv2 $ - mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2' - ; return cv2' } - Given {} - -> newGivenCoVar (mkTyVarTy tv2) xi2' $ - mkCoVarCoercion cv2 `mkTransCoercion` co2' - Derived {} - -> newDerivedId (EqPred (mkTyVarTy tv2) xi2') - - ; canEq gw cv2' (mkTyVarTy tv2) xi2' - } + = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2' + ; case gw of + Wanted {} -> setCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion` + mkSymCoercion co2' + Given {} -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion` + co2' + Derived {} -> return () + ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' } where xi2' = substTyWith [tv1] [xi1] xi2 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1] - rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList -- Used to ineract two equalities of the following form: -- First Equality: co1: (XXX ~ xi1) -- Second Equality: cv2: (XXX ~ xi2) --- Where the cv1 `canSolve` cv2 equality +-- Where the cv1 `canRewrite` cv2 equality -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1), -- See Note [Efficient Orientation] for that -rewriteEqLHS which (co1,xi1) (cv2,gw,xi2) - = do { cv2' <- case (isWanted gw, which) of - (True,LeftComesFromInert) -> - do { cv2' <- newWantedCoVar xi2 xi1 - ; setWantedCoBind cv2 $ - co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2') - ; return cv2' } - (True,RightComesFromInert) -> - do { cv2' <- newWantedCoVar xi1 xi2 - ; setWantedCoBind cv2 $ - co1 `mkTransCoercion` mkCoVarCoercion cv2' - ; return cv2' } - (False,LeftComesFromInert) -> - if isGiven gw then - newGivenCoVar xi2 xi1 $ - mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 - else newDerivedId (EqPred xi2 xi1) - (False,RightComesFromInert) -> - if isGiven gw then - newGivenCoVar xi1 xi2 $ - mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 - else newDerivedId (EqPred xi1 xi2) +rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2) + = do { cv2' <- newCoVar xi2 xi1 + ; case gw of + Wanted {} -> setCoBind cv2 $ + co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2') + Given {} -> setCoBind cv2' $ + mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 + Derived {} -> return () + ; mkCanonical gw cv2' } + +rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2) + = do { cv2' <- newCoVar xi1 xi2 + ; case gw of + Wanted {} -> setCoBind cv2 $ + co1 `mkTransCoercion` mkCoVarCoercion cv2' + Given {} -> setCoBind cv2' $ + mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 + Derived {} -> return () ; mkCanonical gw cv2' } - + rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) - = do { cv2' <- - case fl2 of - Wanted {} -> do { cv2' <- newWantedCoVar ty2a' ty2b' - -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1] - ; setWantedCoBind cv2 $ - co2a' `mkTransCoercion` - mkCoVarCoercion cv2' `mkTransCoercion` - mkSymCoercion co2b' - ; return cv2' } - - Given {} -> newGivenCoVar ty2a' ty2b' $ - mkSymCoercion co2a' `mkTransCoercion` - mkCoVarCoercion cv2 `mkTransCoercion` - co2b' - - Derived {} -> newDerivedId (EqPred ty2a' ty2b') - ; return (singleCCan $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) } + = do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1] + ; case fl2 of + Wanted {} -> setCoBind cv2 $ co2a' `mkTransCoercion` + mkCoVarCoercion cv2' `mkTransCoercion` + mkSymCoercion co2b' + + Given {} -> setCoBind cv2' $ mkSymCoercion co2a' `mkTransCoercion` + mkCoVarCoercion cv2 `mkTransCoercion` + co2b' + + Derived {} -> return () + + ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) } where (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b ty2a' = substTyWith [tv1] [xi1] ty2a @@ -1187,28 +1268,29 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a -- ty2a ~ ty2a[xi1/tv1] co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1] -solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult --- First argument inert, second argument workitem. They both represent --- wanted/given/derived evidence for the *same* predicate so we try here to --- discharge one directly from the other. +solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult +-- First argument inert, second argument work-item. They both represent +-- wanted/given/derived evidence for the *same* predicate so +-- we can discharge one directly from the other. -- -- Precondition: value evidence only (implicit parameters, classes) -- not coercion -solveOneFromTheOther (iid,ifl) workItem - | ifl `canSolve` wfl - = do { when (isWanted wfl) $ setEvBind wid (EvId iid) - -- Overwrite the binding, if one exists - -- For Givens, which are lambda-bound, nothing to overwrite, - ; dischargeWorkItem } - | wfl `canSolve` ifl - = do { when (isWanted ifl) $ setEvBind iid (EvId wid) - ; mkIRContinue workItem DropInert emptyWorkList } - - | otherwise -- One of the two is Derived, we can just throw it away, - -- preferrably the work item. - = if isDerived wfl then dischargeWorkItem - else mkIRContinue workItem DropInert emptyWorkList +solveOneFromTheOther info (ev_term,ifl) workItem + | isDerived wfl + = mkIRStopK ("Solved[DW] " ++ info) emptyWorkList + + | isDerived ifl -- The inert item is Derived, we can just throw it away, + -- The workItem is inert wrt earlier inert-set items, + -- so it's safe to continue on from this point + = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert emptyWorkList + | otherwise + = ASSERT( ifl `canSolve` wfl ) + -- Because of Note [The Solver Invariant], plus Derived dealt with + do { when (isWanted wfl) $ setEvBind wid ev_term + -- Overwrite the binding, if one exists + -- If both are Given, we already have evidence; no need to duplicate + ; mkIRStopK ("Solved " ++ info) emptyWorkList } where wfl = cc_flavor workItem wid = cc_id workItem @@ -1577,7 +1659,7 @@ data TopInteractResult -- arising from top-level instances. topReactionsStage :: SimplifierStage -topReactionsStage workItem inerts +topReactionsStage depth workItem inerts = do { tir <- tryTopReact workItem ; case tir of NoTopInt -> @@ -1585,10 +1667,14 @@ topReactionsStage workItem inerts , sr_new_work = emptyWorkList , sr_stop = ContinueWith workItem } SomeTopInt tir_new_work tir_new_inert -> - return $ SR { sr_inerts = inerts - , sr_new_work = tir_new_work - , sr_stop = tir_new_inert - } + do { bumpStepCountTcS + ; traceFireTcS depth (ptext (sLit "Top react") + <+> vcat [ ptext (sLit "Work =") <+> ppr workItem + , ptext (sLit "New =") <+> ppr tir_new_work ]) + ; return $ SR { sr_inerts = inerts + , sr_new_work = tir_new_work + , sr_stop = tir_new_inert + } } } tryTopReact :: WorkItem -> TcS TopInteractResult @@ -1618,47 +1704,69 @@ doTopReact (CDictCan { cc_flavor = Given {} }) = return NoTopInt -- NB: Superclasses already added since it's canonical -- Derived dictionary: just look for functional dependencies -doTopReact workItem@(CDictCan { cc_flavor = Derived loc +doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc) , cc_class = cls, cc_tyargs = xis }) - = do { fd_work <- findClassFunDeps cls xis loc - ; if isEmptyWorkList fd_work then - return NoTopInt - else return $ SomeTopInt { tir_new_work = fd_work - , tir_new_inert = ContinueWith workItem } } + = do { instEnvs <- getInstEnvs + ; let fd_eqns = improveFromInstEnv instEnvs + (ClassP cls xis, pprArisingAt loc) + ; m <- rewriteWithFunDeps fd_eqns xis fl + ; case m of + Nothing -> return NoTopInt + Just (xis',_,fd_work) -> + let workItem' = workItem { cc_tyargs = xis' } + -- Deriveds are not supposed to have identity (cc_id is unused!) + in return $ SomeTopInt { tir_new_work = fd_work + , tir_new_inert = ContinueWith workItem' } } + -- Wanted dictionary -doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc - , cc_class = cls, cc_tyargs = xis }) +doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc) + , cc_class = cls, cc_tyargs = xis }) = do { -- See Note [MATCHING-SYNONYMS] ; lkp_inst_res <- matchClassInst cls xis loc - ; case lkp_inst_res of - NoInstance -> - do { traceTcS "doTopReact/ no class instance for" (ppr dv) - ; fd_work <- findClassFunDeps cls xis loc - ; return $ SomeTopInt - { tir_new_work = fd_work - , tir_new_inert = ContinueWith workItem } } - - GenInst wtvs ev_term -> -- Solved + ; case lkp_inst_res of + NoInstance -> + do { traceTcS "doTopReact/ no class instance for" (ppr dv) + + ; instEnvs <- getInstEnvs + ; let fd_eqns = improveFromInstEnv instEnvs + (ClassP cls xis, pprArisingAt loc) + ; m <- rewriteWithFunDeps fd_eqns xis fl + ; case m of + Nothing -> return NoTopInt + Just (xis',cos,fd_work) -> + do { let dict_co = mkTyConCoercion (classTyCon cls) cos + ; dv'<- newDictVar cls xis' + ; setDictBind dv (EvCast dv' dict_co) + ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl, + cc_class = cls, cc_tyargs = xis' } + ; return $ + SomeTopInt { tir_new_work = workListFromNonEq workItem' `unionWorkList` fd_work + , tir_new_inert = Stop } } } + + GenInst wtvs ev_term -- Solved -- No need to do fundeps stuff here; the instance -- matches already so we won't get any more info -- from functional dependencies - do { traceTcS "doTopReact/ found class instance for" (ppr dv) - ; setDictBind dv ev_term - ; inst_work <- canWanteds wtvs - ; if null wtvs + | null wtvs + -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) + ; setDictBind dv ev_term -- Solved in one step and no new wanted work produced. -- i.e we directly matched a top-level instance -- No point in caching this in 'inert'; hence Stop - then return $ SomeTopInt { tir_new_work = emptyWorkList - , tir_new_inert = Stop } - - -- Solved and new wanted work produced, you may cache the - -- (tentatively solved) dictionary as Given! (used to be: Derived) - else do { let solved = makeSolvedByInst workItem - ; return $ SomeTopInt - { tir_new_work = inst_work - , tir_new_inert = ContinueWith solved } } - } } + ; return $ SomeTopInt { tir_new_work = emptyWorkList + , tir_new_inert = Stop } } + + | otherwise + -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) + ; setDictBind dv ev_term + -- Solved and new wanted work produced, you may cache the + -- (tentatively solved) dictionary as Given! (used to be: Derived) + ; let solved = workItem { cc_flavor = given_fl } + given_fl = Given (setCtLocOrigin loc UnkSkol) + ; inst_work <- canWanteds wtvs + ; return $ SomeTopInt { tir_new_work = inst_work + , tir_new_inert = ContinueWith solved } } + } -- Type functions doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl @@ -1677,8 +1785,8 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl -- See Note [Type synonym families] in TyCon coe = mkTyConApp coe_tc rep_tys ; cv' <- case fl of - Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi - ; setWantedCoBind cv $ + Wanted {} -> do { cv' <- newCoVar rhs_ty xi + ; setCoBind cv $ coe `mkTransCoercion` mkCoVarCoercion cv' ; return cv' } @@ -1694,20 +1802,6 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl -- Any other work item does not react with any top-level equations doTopReact _workItem = return NoTopInt - ----------------------- -findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList --- Look for a fundep reaction beween the wanted item --- and a top-level instance declaration -findClassFunDeps cls xis loc - = do { instEnvs <- getInstEnvs - ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs) - (ClassP cls xis, pprArisingAt loc) - ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs - -- NB: fundeps generate some wanted equalities, but - -- we don't use their evidence for anything - ; cts <- mapM mkCanonicalFEV derived_evs - ; return $ unionManyBags cts } \end{code}