X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=cb9d34266122da97e48b400278a743f40887009e;hb=25bff7fe1a22edbafa188af8d844c67057fa5eb8;hp=a403bc47c0941121a973223fa6a03cad148bebf7;hpb=d8cb9db585accf9ca6bbe5d4812cb2e943537f87;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index a403bc4..cb9d342 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -211,9 +211,6 @@ getFDImprovements :: InertSet -> FDImprovements getFDImprovements = inert_fds -isWantedCt :: CanonicalCt -> Bool -isWantedCt ct = isWanted (cc_flavor ct) - {- TODO: Later ... data Inert = IS { class_inerts :: FiniteMap Class Atomics ip_inerts :: FiniteMap Class Atomics @@ -287,50 +284,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 +332,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 +400,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 +420,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 +462,64 @@ 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 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 2: In Spontaneous Solving + Example 2a: + 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 it is tempting to just add (beta ~ alpha) instead, that is, + maintain the original orietnation of the constraint. + + But that does not work very well, because it may cause the + "double unification problem" (See Note [Avoid double unifications]). + For instance: + + Example 2b: + [w1] : fsk1 ~ alpha + [w2] : fsk2 ~ alpha + --- + At the end of the interaction suppose we spontaneously solve alpha := fsk1 + but keep [Given] fsk1 ~ alpha. Then, the second time around we see the + constraint (fsk2 ~ alpha), and we unify *again* alpha := fsk2, which is wrong. + + Our conclusion is that, while in some cases (Example 2a), it makes sense to + preserve the original orientation, it is hard to do this in a sound way. + So we *don't* do this for now, @solveWithIdentity@ outputs a constraint that + is oriented with the unified variable on the left. + +Case 3: Functional Dependencies and IP improvement work + TODO. Optimisation not yet implemented there. + \begin{code} spontaneousSolveStage :: SimplifierStage spontaneousSolveStage workItem inerts @@ -501,10 +530,27 @@ spontaneousSolveStage workItem inerts , sr_inerts = inerts , sr_stop = ContinueWith workItem } - Just workList' -> -- He has been solved; workList' are all givens - return $ SR { sr_new_work = workList' - , sr_inerts = inerts - , sr_stop = Stop } + Just (workItem', workList') + | not (isGivenCt workItem) + -- Original was wanted or derived but we have now made him + -- given so we have to interact him with the inerts due to + -- 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 + [ ("recursive interact with inert eqs", interactWithInertEqsStage) + , ("recursive interact with inerts", interactWithInertsStage) + ] inerts workItem' + ; return $ SR { sr_new_work = new_work `unionWorkLists` workList' + , sr_inerts = new_inert -- will include workItem' + , sr_stop = Stop } + } + | otherwise + -> -- Original was given; he must then be inert all right, and + -- workList' are all givens from flattening + return $ SR { sr_new_work = workList' + , sr_inerts = inerts `updInertSet` workItem' + , sr_stop = Stop } } -- @trySpontaneousSolve wi@ solves equalities where one side is a @@ -513,8 +559,8 @@ spontaneousSolveStage workItem inerts -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list. -- 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 -> InertSet -> TcS (Maybe (WorkItem, SWorkList)) +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 @@ -528,7 +574,9 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r | otherwise = do { tch1 <- isTouchableMetaTyVar tv1 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi - else return Nothing } + else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem) + ; return Nothing } + } -- No need for -- trySpontaneousSolve (CFunEqCan ...) = ... @@ -536,26 +584,29 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r trySpontaneousSolve _ _ = return Nothing ---------------- -trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi - -> TcS (Maybe SWorkList) +trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi + -> TcS (Maybe (WorkItem,SWorkList)) -- tv is a MetaTyVar, not untouchable trySpontaneousEqOneWay 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 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 ---------------- trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar - -> TcS (Maybe SWorkList) + -> TcS (Maybe (WorkItem,SWorkList)) -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here trySpontaneousEqTwoWay inerts cv gw tv1 tv2 | k1 `isSubKind` k2 @@ -582,6 +633,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 +673,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 +694,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 +714,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 +729,50 @@ 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. + +NB: This situation appears in the IndTypesPerf test case, inside indexed-types/. + +Caveat: You may wonder if we should be doing this for unification variables as well. +However, Note [Efficient Orientation], Case 2, demonstrates that this is not possible +at least for touchable unification variables which we have to keep oriented with the +touchable on the LHS to be able to eliminate it. So then, what about untouchables? + +Example 4a: +----------- + Untouchable = beta, Touchable = alpha + + [Wanted] w1: alpha ~ fsk + [Given] g1: F alpha ~ fsk + [Given] g2: beta ~ fsk + Flatten skolem equivalence class = [] + +Should we be able to unify alpha := beta to solve the constraint? Arguably yes, but +that implies that an *untouchable* unification variable (beta) is in the same equivalence +class as a flatten skolem that mentions @alpha@. I.e. g2 means that: + beta ~ F alpha +But I do not think that there is any way to produce evidence for such a constraint from +the outside other than beta := F alpha, which violates the OutsideIn-ness. + + Note [Avoid double unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -683,44 +796,67 @@ unification variables as RHS of type family equations: F xis ~ alpha. ---------------- solveWithIdentity :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi - -> TcS (Maybe SWorkList) + -> TcS (Maybe (WorkItem, SWorkList)) -- Solve with the identity coercion -- Precondition: kind(xi) is a sub-kind of kind(tv) -- Precondition: CtFlavor is Wanted or Derived -- See [New Wanted Superclass Work] to see why solveWithIdentity -- must work for Derived as well as Wanted +-- Returns: (workItem, workList) where +-- workItem = the new Given constraint +-- workList = some additional work that may have been produced as a result of flattening +-- in case we did some chasing through flatten skolem equivalence classes. solveWithIdentity inerts cv gw tv xi = do { tybnds <- getTcSTyBindsMap ; case occurCheck tybnds inerts tv xi of Nothing -> return Nothing Just (xi_unflat,coi) -> solve_with xi_unflat coi } where - solve_with xi_unflat coi -- coi : xi_unflat ~ xi + solve_with xi_unflat coi -- coi : xi_unflat ~ xi = do { traceTcS "Sneaky unification:" $ vcat [text "Coercion variable: " <+> ppr gw, text "Coercion: " <+> pprEq (mkTyVarTy 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 ; let flav = mkGivenFlavor gw UnkSkol - ; (cts, co) <- case coi of - ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat - ; 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) + ; (ct,cts, co) <- case coi of + ACo co -> do { (cc,ccs) <- canEqLeafTyVarLeft flav cv_given tv xi_unflat + ; return (cc, ccs, co) } + IdCo co -> return $ (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! + , emptyWorkList, 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) } + -- See Note [Avoid double unifications] + ; return $ Just (ct,cts) + } + +-- ; let flav = mkGivenFlavor gw UnkSkol +-- ; (cts, co) <- case coi of +-- -- TODO: Optimise this, along the way it used to be +-- ACo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat +-- ; setWantedTyBind tv xi_unflat +-- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat +-- ; return (can_eqs, co) } +-- IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi +-- ; setWantedTyBind tv xi +-- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi +-- ; return (can_eqs, 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 cts } occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet -> TcTyVar -> TcType -> Maybe (TcType,CoercionI) @@ -852,6 +988,7 @@ noInteraction :: Monad m => WorkItem -> m InteractResult noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList data WhichComesFromInert = LeftComesFromInert | RightComesFromInert + -- See Note [Efficient Orientation, Case 2] --------------------------------------------------- @@ -959,11 +1096,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)) @@ -1038,7 +1174,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 @@ -1077,10 +1213,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) @@ -1090,19 +1226,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 @@ -1169,7 +1305,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 @@ -1194,26 +1330,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) -> @@ -1664,20 +1794,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 @@ -1690,55 +1860,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 @@ -1766,8 +1891,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!" } @@ -1775,6 +1899,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] @@ -2043,26 +2180,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