X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=b968d7b4530c636247dc7ddae612386a95d442e4;hb=bdd74e54712349f9c7605cb1e763514a8b99f66f;hp=fe19d46f88d1eb17393867be864400e86db3edd2;hpb=0430775a77e219740b66bf4f1db82d7596fa6744;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index fe19d46..b968d7b 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -108,10 +108,52 @@ class of each flatten skolem, which is much needed to correctly do spontaneous solving. See Note [Loopy Spontaneous Solving] \begin{code} +data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts + -- Invariant: all Given or Derived + , cts_wanted :: Map.Map a CanonicalCts } + -- Invariant: all Wanted +cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts +cCanMapToBag cmap = Map.fold unionBags rest_cts (cts_givder cmap) + where rest_cts = Map.fold unionBags emptyCCan (cts_wanted cmap) + +emptyCCanMap :: CCanMap a +emptyCCanMap = CCanMap { cts_givder = Map.empty, cts_wanted = Map.empty } + +updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a +updCCanMap (a,ct) cmap + = case cc_flavor ct of + Wanted {} + -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) } + _ + -> cmap { cts_givder = Map.insertWith unionBags a this_ct (cts_givder cmap) } + where this_ct = singleCCan ct + +getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a) +-- Gets the relevant constraints and returns the rest of the CCanMap +getRelevantCts a cmap + = let relevant = unionBags (Map.findWithDefault emptyCCan a (cts_wanted cmap)) + (Map.findWithDefault emptyCCan a (cts_givder cmap)) + residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap) + , cts_givder = Map.delete a (cts_givder cmap) } + in (relevant, residual_map) + +extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a) +-- Gets the wanted constraints and returns a residual CCanMap +extractUnsolvedCMap cmap = + let unsolved = Map.fold unionBags emptyCCan (cts_wanted cmap) + in (unsolved, cmap { cts_wanted = Map.empty}) + -- See Note [InertSet invariants] data InertSet - = IS { inert_eqs :: Bag.Bag CanonicalCt -- Equalities only **CTyEqCan** - , inert_cts :: Bag.Bag CanonicalCt -- Other constraints + = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan) + + , inert_dicts :: CCanMap Class -- Dictionaries only + , inert_ips :: CCanMap (IPName Name) -- Implicit parameters + , inert_funeqs :: CCanMap TyCon -- Type family equalities only + -- This representation allows us to quickly get to the relevant + -- inert constraints when interacting a work item with the inert set. + + , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already -- and reside either in the worklist or in the inerts , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] } @@ -122,19 +164,24 @@ type FDImprovements = [(PredType,PredType)] instance Outputable InertSet where ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is)) - , vcat (map ppr (Bag.bagToList $ inert_cts is)) + , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is))) + , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is))) + , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is))) , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest)) (Map.toList $ inert_fsks is) ) ] emptyInert :: InertSet -emptyInert = IS { inert_eqs = Bag.emptyBag - , inert_cts = Bag.emptyBag, inert_fsks = Map.empty, inert_fds = [] } +emptyInert = IS { inert_eqs = Bag.emptyBag + , inert_dicts = emptyCCanMap + , inert_ips = emptyCCanMap + , inert_funeqs = emptyCCanMap + , inert_fsks = Map.empty, inert_fds = [] } updInertSet :: InertSet -> AtomicInert -> InertSet -- Introduces an element in the inert set for the first time -updInertSet (IS { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks, inert_fds = fdis }) +updInertSet is@(IS { inert_eqs = eqs, inert_fsks = fsks }) item@(CTyEqCan { cc_id = cv , cc_tyvar = tv1 , cc_rhs = xi }) @@ -144,15 +191,19 @@ updInertSet (IS { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks, inert_fds = let eqs' = eqs `Bag.snocBag` item fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks -- See Note [InertSet FlattenSkolemEqClass] - in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks', inert_fds = fdis } -updInertSet (IS { inert_eqs = eqs, inert_cts = cts - , inert_fsks = fsks, inert_fds = fdis }) item - | isTyEqCCan item - = let eqs' = eqs `Bag.snocBag` item - in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks, inert_fds = fdis } + in is { inert_eqs = eqs', inert_fsks = fsks' } +updInertSet is item + | isCTyEqCan item -- Other equality + = let eqs' = inert_eqs is `Bag.snocBag` item + in is { inert_eqs = eqs' } + | Just cls <- isCDictCan_Maybe item -- Dictionary + = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) } + | Just x <- isCIPCan_Maybe item -- IP + = is { inert_ips = updCCanMap (x,item) (inert_ips is) } + | Just tc <- isCFunEqCan_Maybe item -- Function equality + = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) } | otherwise - = let cts' = cts `Bag.snocBag` item - in IS { inert_eqs = eqs, inert_cts = cts', inert_fsks = fsks, inert_fds = fdis } + = pprPanic "Unknown form of constraint!" (ppr item) updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is } @@ -163,25 +214,26 @@ foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a foldISEqCtsM k z IS { inert_eqs = eqs } = Bag.foldlBagM k z eqs -foldISOtherCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a --- Fold over other constraints in the inerts -foldISOtherCtsM k z IS { inert_cts = cts } - = Bag.foldlBagM k z cts - extractUnsolved :: InertSet -> (InertSet, CanonicalCts) -extractUnsolved is@(IS {inert_eqs = eqs, inert_cts = cts, inert_fds = fdis }) - = let is_init = is { inert_eqs = emptyCCan - , inert_cts = solved_cts, inert_fsks = Map.empty, inert_fds = fdis } +extractUnsolved is@(IS {inert_eqs = eqs}) + = let is_init = is { inert_eqs = emptyCCan + , inert_dicts = solved_dicts + , inert_ips = solved_ips + , inert_funeqs = solved_funeqs } is_final = Bag.foldlBag updInertSet is_init solved_eqs -- Add equalities carefully - in (is_final, unsolved) - where (unsolved_cts, solved_cts) = Bag.partitionBag isWantedCt cts - (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs - unsolved = unsolved_cts `unionBags` unsolved_eqs + in (is_final, unsolved) + where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs + (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is) + (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is) + (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is) + + unsolved = unsolved_eqs `unionBags` + unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)] -- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass] -getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv +getFskEqClass (IS { inert_eqs = cts, inert_fsks = fsks }) tv = case lkpTyEqCanByLhs of Nothing -> fromMaybe [] (Map.lookup tv fsks) Just ceq -> @@ -200,29 +252,15 @@ haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool haveBeenImproved [] _ _ = False haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2' | tcEqPred pty1 pty1' && tcEqPred pty2 pty2' - = True + = True | tcEqPred pty1 pty2' && tcEqPred pty2 pty1' - = True - | otherwise - = haveBeenImproved fdimprs pty1' pty2' + = True + | otherwise + = haveBeenImproved fdimprs pty1' pty2' -getFDImprovements :: InertSet -> FDImprovements +getFDImprovements :: InertSet -> FDImprovements -- Return a list of the improvements that have kicked in so far -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 - tyfun_inerts :: FiniteMap TyCon Atomics - tyvar_inerts :: FiniteMap TyVar Atomics - } - -Later should we also separate out givens and wanteds? --} +getFDImprovements = inert_fds \end{code} @@ -427,7 +465,7 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws , text "Max depth =" <+> ppr max_depth ] -- Solve equalities first - ; let (eqs, non_eqs) = Bag.partitionBag isTyEqCCan ws + ; 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 } @@ -465,6 +503,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 @@ -475,10 +571,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 @@ -487,8 +600,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 @@ -502,7 +615,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 ...) = ... @@ -510,26 +625,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 @@ -556,6 +674,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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -585,8 +714,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, @@ -603,6 +735,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 @@ -621,6 +755,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 @@ -634,6 +770,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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -657,44 +837,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 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) @@ -818,7 +1021,6 @@ mkIRStop keep newWork = return $ IR Stop keep newWork Nothing mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr) - dischargeWorkItem :: Monad m => m InteractResult dischargeWorkItem = mkIRStop KeepInert emptyWorkList @@ -826,6 +1028,7 @@ noInteraction :: Monad m => WorkItem -> m InteractResult noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList data WhichComesFromInert = LeftComesFromInert | RightComesFromInert + -- See Note [Efficient Orientation, Case 2] --------------------------------------------------- @@ -838,8 +1041,10 @@ interactWithInertEqsStage workItem inert = foldISEqCtsM interactNext initITR inert where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- We will fold over the equalities , inert_fsks = Map.empty -- which will generate those two again - , inert_cts = inert_cts inert - , inert_fds = inert_fds inert + , inert_dicts = inert_dicts inert + , inert_ips = inert_ips inert + , inert_funeqs = inert_funeqs inert + , inert_fds = inert_fds inert } , sr_new_work = emptyWorkList , sr_stop = ContinueWith workItem } @@ -849,18 +1054,36 @@ interactWithInertEqsStage workItem inert -- Interact a single WorkItem with *non-equality* constraints in the inert set. -- Precondition: equality interactions must have already happened, hence we have -- to pick up some information from the incoming inert, before folding over the --- "Other" constraints it contains! +-- "Other" constraints it contains! + interactWithInertsStage :: SimplifierStage interactWithInertsStage workItem inert - = foldISOtherCtsM interactNext initITR 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 where - initITR = SR { -- Pick up: (1) equations, (2) FD improvements, (3) FlatSkol equiv. classes - sr_inerts = IS { inert_eqs = inert_eqs inert - , inert_cts = emptyCCan - , inert_fds = inert_fds inert - , inert_fsks = inert_fsks inert } - , sr_new_work = emptyWorkList - , sr_stop = ContinueWith workItem } + getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) + getISRelevant (CDictCan { cc_class = cls } ) is + = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is) + in (relevant, is { inert_dicts = residual_map }) + getISRelevant (CFunEqCan { cc_fun = tc } ) is + = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is) + in (relevant, is { inert_funeqs = residual_map }) + getISRelevant (CIPCan { cc_ip_nm = nm }) is + = let (relevant, residual_map) = getRelevantCts nm (inert_ips is) + in (relevant, is { inert_ips = residual_map }) + -- An equality, finally, may kick everything except equalities out + -- because we have already interacted the equalities in interactWithInertEqsStage + getISRelevant _eq_ct is -- Equality, everything is relevant for this one + -- TODO: if we were caching variables, we'd know that only + -- some are relevant. Experiment with this for now. + = let cts = cCanMapToBag (inert_ips is) `unionBags` + cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is) + in (cts, is { inert_dicts = emptyCCanMap + , inert_ips = emptyCCanMap + , inert_funeqs = emptyCCanMap }) interactNext :: StageResult -> AtomicInert -> TcS StageResult interactNext it inert @@ -935,7 +1158,7 @@ doInteractWithInert fdimprs ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs ; fd_work <- canWanteds wevvars -- See Note [Generating extra equalities] - ; traceTcS "Checking if improvements existed." (ppr fdimprs) + ; traceTcS "Checking if improvements existed." (ppr fdimprs) ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then -- Must keep going mkIRContinue workItem KeepInert fd_work @@ -943,7 +1166,7 @@ doInteractWithInert fdimprs ; mkIRStop_RecordImprovement KeepInert (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2) } - -- See Note [FunDep Reactions] + -- See Note [FunDep Reactions] } -- Class constraint and given equality: use the equality to rewrite @@ -1167,10 +1390,7 @@ 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 @@ -1182,11 +1402,8 @@ rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> T -- 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) ->