X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=c03384f920c7589dc4cbc2dcf978a5cea4c0cda8;hb=162c7e780267c73495fb245a873f7e3b8431471b;hp=b46a5022e19090478ec51e6e294849d9583b3a11;hpb=8657bb00544468adc7ad63e962af71674c3b4500;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index b46a502..c03384f 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -287,50 +287,27 @@ Note [Basic plan] Superclass decomposition belongs in (4), see note [Superclasses] \begin{code} - 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. -data WorkList = WL { wl_eqs :: CanonicalCts -- Equalities (CTyEqCan, CFunEqCan) - , wl_other :: CanonicalCts -- Other - } -type SWorkList = WorkList -- A worklist of solved +type WorkList = CanonicalCts +type SWorkList = WorkList -- A worklist of solved unionWorkLists :: WorkList -> WorkList -> WorkList -unionWorkLists wl1 wl2 - = WL { wl_eqs = andCCan (wl_eqs wl1) (wl_eqs wl2) - , wl_other = andCCan (wl_other wl1) (wl_other wl2) } - -foldWorkListEqCtsM :: Monad m => (a -> WorkItem -> m a) -> a -> WorkList -> m a --- Fold over the equalities of a worklist -foldWorkListEqCtsM f r wl = Bag.foldlBagM f r (wl_eqs wl) - -foldWorkListOtherCtsM :: Monad m => (a -> WorkItem -> m a) -> a -> WorkList -> m a --- Fold over non-equality constraints of a worklist -foldWorkListOtherCtsM f r wl = Bag.foldlBagM f r (wl_other wl) +unionWorkLists = andCCan isEmptyWorkList :: WorkList -> Bool -isEmptyWorkList wl = isEmptyCCan (wl_eqs wl) && isEmptyCCan (wl_other wl) +isEmptyWorkList = isEmptyCCan emptyWorkList :: WorkList -emptyWorkList = WL { wl_eqs = emptyCCan, wl_other = emptyCCan } - -workListFromCCans :: CanonicalCts -> WorkList --- Generic, no precondition -workListFromCCans cts = WL eqs others - where (eqs, others) = Bag.partitionBag isTyEqCCan cts +emptyWorkList = emptyCCan workListFromCCan :: CanonicalCt -> WorkList -workListFromCCan ct | isTyEqCCan ct = WL (singleCCan ct) emptyCCan - | otherwise = WL emptyCCan (singleCCan ct) --- TODO: --- At the call sites of workListFromCCan(s), sometimes we know whether the new work --- involves equalities or not. It's probably a good idea to add specialized calls for --- those, to avoid asking whether 'isTyEqCCan' all the time. - +workListFromCCan = singleCCan +------------------------ data StopOrContinue = Stop -- Work item is consumed | ContinueWith WorkItem -- Not consumed @@ -358,9 +335,6 @@ instance Outputable StageResult where , ptext (sLit "new work =") <+> ppr work <> comma , ptext (sLit "stop =") <+> ppr stop]) -instance Outputable WorkList where - ppr (WL eqcts othercts) = vcat [ppr eqcts, ppr othercts] - type SimplifierStage = WorkItem -> InertSet -> TcS StageResult -- Combine a sequence of simplifier 'stages' to create a pipeline @@ -429,8 +403,7 @@ React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canoni solveInteract :: InertSet -> CanonicalCts -> TcS InertSet solveInteract inert ws = do { dyn_flags <- getDynFlags - ; let worklist = workListFromCCans ws - ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert worklist + ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws } solveOne :: InertSet -> WorkItem -> TcS InertSet solveOne inerts workItem @@ -450,12 +423,13 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws | otherwise = do { traceTcS "solveInteractWithDepth" $ - vcat [ text "Current depth =" <+> ppr n - , text "Max depth =" <+> ppr max_depth - ] - ; is_from_eqs <- foldWorkListEqCtsM (solveOneWithDepth ctxt) inert ws - ; foldWorkListOtherCtsM (solveOneWithDepth ctxt) is_from_eqs ws - } + vcat [ text "Current depth =" <+> ppr n + , text "Max depth =" <+> ppr max_depth ] + + -- Solve equalities first + ; let (eqs, non_eqs) = Bag.partitionBag isTyEqCCan ws + ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs + ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs } ------------------ -- Fully interact the given work item with an inert set, and return a @@ -491,6 +465,58 @@ thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage) * * ********************************************************************************* +Note [Efficient Orientation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +There are two cases where we have to be careful about +orienting equalities to get better efficiency. + +Case 1: In Spontaneous Solving + + The OrientFlag is used to preserve the original orientation of a + spontaneously solved equality (insofar the canonical constraints + invariants allow it). This way we hope to be more efficient since + when reaching the spontaneous solve stage, a particular + constraint has already been inert-ified wrt to the preexisting + inerts. + + Example: + Inerts: [w1] : D alpha + [w2] : C beta + [w3] : F alpha ~ Int + [w4] : H beta ~ Int + Untouchables = [beta] + Then a wanted (beta ~ alpha) comes along. + + 1) While interacting with the inerts it is going to kick w2,w4 + out of the inerts + 2) Then, it will spontaneoulsy be solved by (alpha := beta) + 3) Now (and here is the tricky part), to add him back as + solved (alpha ~ beta) is no good because, in the next + iteration, it will kick out w1,w3 as well so we will end up + with *all* the inert equalities back in the worklist! + + So, we instead solve (alpha := beta), but we preserve the + original orientation, so that we get a given (beta ~ alpha), + which will result in no more inerts getting kicked out of the + inert set in the next iteration. + +Case 2: In Rewriting Equalities (function rewriteEqLHS) + + When rewriting two equalities with the same LHS: + (a) (tv ~ xi1) + (b) (tv ~ xi2) + We have a choice of producing work (xi1 ~ xi2) (up-to the + canonicalization invariants) However, to prevent the inert items + from getting kicked out of the inerts first, we prefer to + canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2 + ~ xi1) if (a) comes from the inert set. + + This choice is implemented using the WhichComesFromInert flag. + +Case 3: Functional Dependencies and IP improvement work + TODO. Optimisation not yet implemented there. + \begin{code} spontaneousSolveStage :: SimplifierStage spontaneousSolveStage workItem inerts @@ -507,6 +533,10 @@ spontaneousSolveStage workItem inerts , sr_stop = Stop } } + +data OrientFlag = OrientThisWay + | OrientOtherWay -- See Note [Efficient Orientation] + -- @trySpontaneousSolve wi@ solves equalities where one side is a -- touchable unification variable. Returns: -- * Nothing if we were not able to solve it @@ -514,7 +544,7 @@ spontaneousSolveStage workItem inerts -- See Note [Touchables and givens] -- NB: just passing the inerts through for the skolem equivalence classes trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList) -trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts +trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts | isGiven gw = return Nothing | Just tv2 <- tcGetTyVar_maybe xi @@ -522,13 +552,15 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r ; tch2 <- isTouchableMetaTyVar tv2 ; case (tch1, tch2) of (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2 - (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi - (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1) + (True, False) -> trySpontaneousEqOneWay OrientThisWay inerts cv gw tv1 xi + (False, True) -> trySpontaneousEqOneWay OrientOtherWay inerts cv gw tv2 (mkTyVarTy tv1) _ -> return Nothing } | otherwise = do { tch1 <- isTouchableMetaTyVar tv1 - ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi - else return Nothing } + ; if tch1 then trySpontaneousEqOneWay OrientThisWay inerts cv gw tv1 xi + else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem) + ; return Nothing } + } -- No need for -- trySpontaneousSolve (CFunEqCan ...) = ... @@ -536,20 +568,26 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r trySpontaneousSolve _ _ = return Nothing ---------------- -trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi +trySpontaneousEqOneWay :: OrientFlag + -> InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS (Maybe SWorkList) --- tv is a MetaTyVar, not untouchable -trySpontaneousEqOneWay inerts cv gw tv xi +-- NB: The OrientFlag is there to help us recover the orientation of the original +-- constraint which is important for enforcing the canonical constraints invariants. +-- Also, tv is a MetaTyVar, not untouchable +trySpontaneousEqOneWay or_flag inerts cv gw tv xi | not (isSigTyVar tv) || isTyVarTy xi - = if typeKind xi `isSubKind` tyVarKind tv then - solveWithIdentity inerts cv gw tv xi - else if tyVarKind tv `isSubKind` typeKind xi then + = do { kxi <- zonkTcTypeTcS xi >>= return . typeKind -- Must look through the TcTyBinds + -- hence kxi and not typeKind xi + -- See Note [Kind Errors] + ; if kxi `isSubKind` tyVarKind tv then + solveWithIdentity or_flag inerts cv gw tv xi + else if tyVarKind tv `isSubKind` kxi then return Nothing -- kinds are compatible but we can't solveWithIdentity this way -- This case covers the a_touchable :: * ~ b_untouchable :: ?? -- which has to be deferred or floated out for someone else to solve -- it in a scope where 'b' is no longer untouchable. else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors] - + } | otherwise -- Still can't solve, sig tyvar and non-variable rhs = return Nothing @@ -559,9 +597,9 @@ trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here trySpontaneousEqTwoWay inerts cv gw tv1 tv2 | k1 `isSubKind` k2 - , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1) + , nicer_to_update_tv2 = solveWithIdentity OrientOtherWay inerts cv gw tv2 (mkTyVarTy tv1) | k2 `isSubKind` k1 - = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2) + = solveWithIdentity OrientThisWay inerts cv gw tv1 (mkTyVarTy tv2) | otherwise -- None is a subkind of the other, but they are both touchable! = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors] where @@ -582,6 +620,17 @@ constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately The same applies in canonicalization code in case of kind errors in the givens. +However, when we canonicalize givens we only check for compatibility (@compatKind@). +If there were a kind error in the givens, this means some form of inconsistency or dead code. + +When we spontaneously solve wanteds we may have to look through the bindings, hence we +call zonkTcTypeTcS above. The reason is that maybe xi is @alpha@ where alpha :: ? and +a previous spontaneous solving has set (alpha := f) with (f :: *). The reason that xi is +still alpha and not f is becasue the solved constraint may be oriented as (f ~ alpha) instead +of (alpha ~ f). Then we should be using @xi@s "real" kind, which is * and not ?, when we try +to detect whether spontaneous solving is possible. + + Note [Spontaneous solving and kind compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -611,8 +660,11 @@ Caveat: Whereas we would be able to apply the type instance, we would not be able to use the given (T Bool ~ (->)) in the body of 'flop' -Note [Loopy spontaneous solving] +Note [Loopy Spontaneous Solving] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Example 1: (The problem of loopy spontaneous solving) +**************************************************************************** Consider the original wanted: wanted : Maybe (E alpha) ~ alpha where E is a type family, such that E (T x) = x. After canonicalization, @@ -629,6 +681,8 @@ actually solving. But this occurs check *must look through* flatten skolems. However, it may be the case that the flatten skolem in hand is equal to some other flatten skolem whith *does not* mention our unification variable. Here's a typical example: +Example 2: (The need of keeping track of flatten skolem equivalence classes) +**************************************************************************** Original wanteds: g: F alpha ~ F beta w: alpha ~ F alpha @@ -647,6 +701,8 @@ We will look inside f2, which immediately mentions (F alpha), so it's not good t by looking at the equivalence class of the flatten skolems, we can see that it is fine to unify (alpha ~ f1) which solves our goals! +Example 3: (The need of looking through TyBinds for already spontaneously solved variables) +******************************************************************************************* A similar problem happens because of other spontaneous solving. Suppose we have the following wanteds, arriving in this exact order: (first) w: beta ~ alpha @@ -660,6 +716,27 @@ that is wrong since fsk mentions beta, which has already secretly been unified t To avoid this problem, the same occurs check must unveil rewritings that can happen because of spontaneously having solved other constraints. +Example 4: (Orientation of (tv ~ xi) equalities) +************************************************ +We orient equalities (tv ~ xi) so that flatten skolems appear on the left, if possible. Here +is an example of why this is needed: + + [Wanted] w1: alpha ~ fsk + [Given] g1: F alpha ~ fsk + [Given] g2: b ~ fsk + Flatten skolem equivalence class = [] + +Assume that g2 is *not* oriented properly, as shown above. Then we would like to spontaneously +solve w1 but we can't set alpha := fsk, since fsk hides the type F alpha. However, by using +the equation g2 it would be possible to solve w1 by setting alpha := b. In other words, it is +not enough to look at a flatten skolem equivalence class to try to find alternatives to unify +with. We may have to go to other variables. + +By orienting the equalities so that flatten skolems are in the LHS we are eliminating them +as much as possible from the RHS of other wanted equalities, and hence it suffices to look +in their flatten skolem equivalence classes. + +This situation appears in the IndTypesPerf test case, inside indexed-types/. Note [Avoid double unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -681,7 +758,8 @@ unification variables as RHS of type family equations: F xis ~ alpha. \begin{code} ---------------- -solveWithIdentity :: InertSet +solveWithIdentity :: OrientFlag + -> InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS (Maybe SWorkList) -- Solve with the identity coercion @@ -689,7 +767,7 @@ solveWithIdentity :: InertSet -- Precondition: CtFlavor is Wanted or Derived -- See [New Wanted Superclass Work] to see why solveWithIdentity -- must work for Derived as well as Wanted -solveWithIdentity inerts cv gw tv xi +solveWithIdentity or_flag inerts cv gw tv xi = do { tybnds <- getTcSTyBindsMap ; case occurCheck tybnds inerts tv xi of Nothing -> return Nothing @@ -702,25 +780,28 @@ solveWithIdentity inerts cv gw tv xi text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)), text "Right Kind is : " <+> ppr (typeKind xi) ] - ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat - ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat +-- ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat +-- ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat ; let flav = mkGivenFlavor gw UnkSkol ; (cts, co) <- case coi of - ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat + ACo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat + ; setWantedTyBind tv xi_unflat + ; can_eqs <- case or_flag of + OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi_unflat + OrientOtherWay -> canEq flav cv_given xi_unflat (mkTyVarTy tv) + ; return (can_eqs, co) } + IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi + ; setWantedTyBind tv xi + ; can_eqs <- case or_flag of + OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi + OrientOtherWay -> canEq flav cv_given xi (mkTyVarTy tv) ; return (can_eqs, co) } - IdCo co -> return $ - (singleCCan (CTyEqCan { cc_id = cv_given - , cc_flavor = mkGivenFlavor gw UnkSkol - , cc_tyvar = tv, cc_rhs = xi } - -- xi, *not* xi_unflat because - -- xi_unflat may require flattening! - ), co) ; case gw of Wanted {} -> setWantedCoBind cv co Derived {} -> setDerivedCoBind cv co _ -> pprPanic "Can't spontaneously solve *given*" empty -- See Note [Avoid double unifications] - ; return $ Just (workListFromCCans cts) } + ; return $ Just cts } occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet -> TcTyVar -> TcType -> Maybe (TcType,CoercionI) @@ -852,6 +933,7 @@ noInteraction :: Monad m => WorkItem -> m InteractResult noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList data WhichComesFromInert = LeftComesFromInert | RightComesFromInert + -- See Note [Efficient Orientation, Case 2] --------------------------------------------------- @@ -891,23 +973,22 @@ interactWithInertsStage workItem inert interactNext :: StageResult -> AtomicInert -> TcS StageResult interactNext it inert | ContinueWith workItem <- sr_stop it - = do { let inerts = sr_inerts it - fdimprs_old = getFDImprovements inerts + = do { let inerts = sr_inerts it + fdimprs_old = getFDImprovements inerts - ; ir <- interactWithInert fdimprs_old inert workItem + ; ir <- interactWithInert fdimprs_old 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 = updInertSetFDImprs upd_inert (ir_improvement ir) - upd_inert = if ir_inert_action ir == KeepInert - then inerts `updInertSet` inert else inerts + -- 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 = updInertSetFDImprs upd_inert (ir_improvement ir) + upd_inert = if ir_inert_action ir == KeepInert + then inerts `updInertSet` inert else inerts - ; return $ SR { sr_inerts = inerts_new - , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir - , sr_stop = ir_stop ir } } - | otherwise = return $ itrAddInert inert it - where itrAddInert :: AtomicInert -> StageResult -> StageResult - itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert } + ; return $ SR { sr_inerts = inerts_new + , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir + , sr_stop = ir_stop ir } } + | otherwise + = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert } -- Do a single interaction of two constraints. interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult @@ -960,11 +1041,10 @@ doInteractWithInert fdimprs eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs - ; fd_cts <- canWanteds wevvars - ; let fd_work = workListFromCCans fd_cts + ; fd_work <- canWanteds wevvars -- See Note [Generating extra equalities] ; traceTcS "Checking if improvements existed." (ppr fdimprs) - ; if isEmptyCCan fd_cts || haveBeenImproved fdimprs pty1 pty2 then + ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then -- Must keep going mkIRContinue workItem KeepInert fd_work else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2)) @@ -1039,7 +1119,7 @@ doInteractWithInert _fdimprs do { co_var <- newWantedCoVar ty1 ty2 ; let flav = Wanted (combineCtLoc ifl wfl) ; cans <- mkCanonical flav co_var - ; mkIRContinue workItem KeepInert (workListFromCCans cans) } + ; mkIRContinue workItem KeepInert cans } -- Inert: equality, work item: function equality @@ -1078,10 +1158,10 @@ doInteractWithInert _fdimprs , cc_tyargs = args2, cc_rhs = xi2 }) | fl1 `canSolve` fl2 && lhss_match = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert (workListFromCCans cans) } + ; mkIRStop KeepInert cans } | fl2 `canSolve` fl1 && lhss_match = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert (workListFromCCans cans) } + ; mkIRContinue workItem DropInert cans } where lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) @@ -1091,19 +1171,19 @@ doInteractWithInert _fdimprs -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert (workListFromCCans cans) } + ; mkIRStop KeepInert cans } | fl2 `canSolve` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert (workListFromCCans cans) } + ; mkIRContinue 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 (workListFromCCans rewritten_eq) } + ; mkIRStop KeepInert rewritten_eq } | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) - ; mkIRContinue workItem DropInert (workListFromCCans rewritten_eq) } + ; mkIRContinue workItem DropInert rewritten_eq } -- Finally, if workitem is a Flatten Equivalence Class constraint and the -- inert is a wanted constraint, even when the workitem cannot rewrite the @@ -1170,7 +1250,7 @@ rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) , cc_rhs = xi2 }) } -rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts +rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList -- Use the first equality to rewrite the second, flavors already checked. -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2 -- rewrites c2 to give @@ -1195,26 +1275,20 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) mkCoVarCoercion cv2 `mkTransCoercion` co2' ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2 - ; return (singleCCan $ CTyEqCan { cc_id = cv2' - , cc_flavor = gw - , cc_tyvar = tv2 - , cc_rhs = xi2'' }) + ; canEq 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 CanonicalCts +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 --- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This --- depends on whether the left or the right equality comes from the inert set. --- We must: --- prefer to create (xi2 ~ xi1) if the first comes from the inert --- prefer to create (xi1 ~ xi2) if the second comes from the inert +-- 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) -> @@ -1665,20 +1739,60 @@ allowedTopReaction _ _ = True doTopReact :: WorkItem -> TcS TopInteractResult -- The work item does not react with the inert set, -- so try interaction with top-level instances + +-- Given dictionary; just add superclasses +-- See Note [Given constraint that matches an instance declaration] +doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc + , cc_class = cls, cc_tyargs = xis }) + = do { sc_work <- newGivenSCWork dv loc cls xis + ; return $ SomeTopInt sc_work (ContinueWith workItem) } + +-- Derived dictionary +-- Do not add any further derived superclasses; their +-- full transitive closure has already been added. +-- But do look for functional dependencies +doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Derived loc _ + , cc_class = cls, cc_tyargs = xis }) + = do { fd_work <- findClassFunDeps dv cls xis loc + ; if isEmptyWorkList fd_work then + return NoTopInt + else return $ SomeTopInt { tir_new_work = fd_work + , tir_new_inert = ContinueWith workItem } } + doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = 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) - ; funDepReact } + NoInstance -> + do { traceTcS "doTopReact/ no class instance for" (ppr dv) + ; fd_work <- findClassFunDeps dv cls xis loc + ; if isEmptyWorkList fd_work then + do { sc_work <- newDerivedSCWork dv loc cls xis + -- See Note [Adding Derived Superclasses] + -- NB: workItem is inert, but it isn't solved + -- keep it as inert, although it's not solved + -- because we have now reacted all its + -- top-level fundep-induced equalities! + ; return $ SomeTopInt + { tir_new_work = fd_work `unionWorkLists` sc_work + , tir_new_inert = ContinueWith workItem } } + + else -- More fundep work produced, don't do any superclass stuff, + -- just thow him back in the worklist, which will prioritize + -- the solution of fd equalities + return $ SomeTopInt + { tir_new_work = fd_work `unionWorkLists` + workListFromCCan workItem + , 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 - ; workList <- canWanteds wtvs + ; inst_work <- canWanteds wtvs ; if null wtvs -- Solved in one step and no new wanted work produced. -- i.e we directly matched a top-level instance @@ -1691,55 +1805,10 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc else do { let solved = makeSolvedByInst workItem ; sc_work <- newDerivedSCWork dv loc cls xis -- See Note [Adding Derived Superclasses] - ; let inst_work = workListFromCCans workList ; return $ SomeTopInt { tir_new_work = inst_work `unionWorkLists` sc_work , tir_new_inert = ContinueWith solved } } - } - } - where - -- Try for a fundep reaction beween the wanted item - -- and a top-level instance declaration - funDepReact - = do { instEnvs <- getInstEnvs - ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs) - (ClassP cls xis, ppr dv) - ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs - -- NB: fundeps generate some wanted equalities, but - -- we don't use their evidence for anything - ; fd_cts <- canWanteds wevvars - ; let fd_work = workListFromCCans fd_cts - - ; if isEmptyCCan fd_cts then - do { sc_work <- newDerivedSCWork dv loc cls xis - -- See Note [Adding Derived Superclasses] - ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work - , tir_new_inert = ContinueWith workItem } - } - else -- More fundep work produced, don't do any superlcass stuff, just - -- thow him back in the worklist prioritizing the solution of fd equalities - return $ - SomeTopInt { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem - , tir_new_inert = Stop } - - -- NB: workItem is inert, but it isn't solved - -- keep it as inert, although it's not solved because we - -- have now reacted all its top-level fundep-induced equalities! - - -- See Note [FunDep Reactions] - } - --- Derived, do not add any further derived superclasses; their full transitive --- closure has already been added. -doTopReact (CDictCan { cc_flavor = fl }) - | isDerived fl - = return NoTopInt - -doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc - , cc_class = cls, cc_tyargs = xis }) - = do { sc_work <- newGivenSCWork dv loc cls xis - ; return $ SomeTopInt sc_work (ContinueWith workItem) } - -- See Note [Given constraint that matches an instance declaration] + } } -- Type functions doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl @@ -1767,8 +1836,7 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe ; can_cts <- mkCanonical fl cv' - ; let workList = workListFromCCans can_cts - ; return $ SomeTopInt workList Stop } + ; return $ SomeTopInt can_cts Stop } _ -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!" } @@ -1776,6 +1844,19 @@ 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 :: EvVar -> Class -> [Xi] -> WantedLoc -> TcS WorkList +-- Look for a fundep reaction beween the wanted item +-- and a top-level instance declaration +findClassFunDeps dv cls xis loc + = do { instEnvs <- getInstEnvs + ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs) + (ClassP cls xis, ppr dv) + ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs + -- NB: fundeps generate some wanted equalities, but + -- we don't use their evidence for anything + ; canWanteds wevvars } \end{code} Note [Adding Derived Superclasses] @@ -2044,26 +2125,26 @@ newGivenSCWork ev loc cls xis | NoScSkol <- ctLocOrigin loc -- Very important! = return emptyWorkList | otherwise - = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return . workListFromCCans + = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList newDerivedSCWork ev loc cls xis = do { ims <- newImmSCWorkFromFlavored ev flavor cls xis - ; final_cts <- rec_sc_work ims - ; return $ workListFromCCans final_cts } - where rec_sc_work :: CanonicalCts -> TcS CanonicalCts - rec_sc_work cts - = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c - ; recs_ims <- rec_sc_work ims - ; return $ consBag c recs_ims }) cts - ; return $ concatBag bg } - imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis }) - = newImmSCWorkFromFlavored dv fl cls xis - imm_sc_work _ct = return emptyCCan - - flavor = Derived loc DerSC - -newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts + ; rec_sc_work ims } + where + rec_sc_work :: CanonicalCts -> TcS CanonicalCts + rec_sc_work cts + = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c + ; recs_ims <- rec_sc_work ims + ; return $ consBag c recs_ims }) cts + ; return $ concatBag bg } + imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis }) + = newImmSCWorkFromFlavored dv fl cls xis + imm_sc_work _ct = return emptyCCan + + flavor = Derived loc DerSC + +newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList -- Returns immediate superclasses newImmSCWorkFromFlavored ev flavor cls xis = do { let (tyvars, sc_theta, _, _) = classBigSig cls