X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=b968d7b4530c636247dc7ddae612386a95d442e4;hb=2f4e210fae842d3f0cb6cb01ee66805487c65c2e;hp=e7b03d1e1b97e22494a385fbc1334e1480f78901;hpb=44674ca1081895c95e04707d74779d3f887c430e;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index e7b03d1..b968d7b 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -108,28 +108,80 @@ 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,CFunEqCan) - , 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)] } -- See Note [InertSet FlattenSkolemEqClass] +type FDImprovement = (PredType,PredType) +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 } +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 }) +updInertSet is@(IS { inert_eqs = eqs, inert_fsks = fsks }) item@(CTyEqCan { cc_id = cv , cc_tyvar = tv1 , cc_rhs = xi }) @@ -139,36 +191,49 @@ updInertSet (IS { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks }) = 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' } -updInertSet (IS { inert_eqs = eqs, inert_cts = cts - , inert_fsks = fsks }) item - | isEqCCan item - = let eqs' = eqs `Bag.snocBag` item - in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks } + 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 } + = pprPanic "Unknown form of constraint!" (ppr item) + +updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet +updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is } +updInertSetFDImprs is Nothing = is -foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a --- Prioritize over the equalities see Note [Prioritizing Equalities] -foldlInertSetM k z (IS { inert_eqs = eqs, inert_cts = cts }) - = do { z' <- Bag.foldlBagM k z eqs - ; Bag.foldlBagM k z' cts } +foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a +-- Fold over the equalities of the inerts +foldISEqCtsM k z IS { inert_eqs = eqs } + = Bag.foldlBagM k z eqs extractUnsolved :: InertSet -> (InertSet, CanonicalCts) -extractUnsolved is@(IS {inert_eqs = eqs, inert_cts = cts}) - = let is_init = is { inert_eqs = emptyCCan - , inert_cts = solved_cts, inert_fsks = Map.empty } +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 -> @@ -183,19 +248,19 @@ getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct lkp other _ct = other +haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool +haveBeenImproved [] _ _ = False +haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2' + | tcEqPred pty1 pty1' && tcEqPred pty2 pty2' + = True + | tcEqPred pty1 pty2' && tcEqPred pty2 pty1' + = True + | otherwise + = haveBeenImproved fdimprs pty1' pty2' -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 :: InertSet -> FDImprovements +-- Return a list of the improvements that have kicked in so far +getFDImprovements = inert_fds \end{code} @@ -251,59 +316,36 @@ Note [Basic plan] 2. Pairwise interaction (binary) * Take one from work list * Try all pair-wise interactions with each constraint in inert + + As an optimisation, we prioritize the equalities both in the + worklist and in the inerts. + 3. Try to solve spontaneously for equalities involving touchables 4. Top-level interaction (binary wrt top-level) 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) } - -foldlWorkListM :: (Monad m) => (a -> WorkItem -> m a) -> a -> WorkList -> m a --- This fold prioritizes equalities -foldlWorkListM f r wl - = do { r' <- Bag.foldlBagM f r (wl_eqs 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 } - -mkEqWorkList :: CanonicalCts -> WorkList --- Precondition: *ALL* equalities -mkEqWorkList eqs = WL { wl_eqs = eqs, wl_other = emptyCCan } - -mkNonEqWorkList :: CanonicalCts -> WorkList --- Precondition: *NO* equalities -mkNonEqWorkList cts = WL { wl_eqs = emptyCCan, wl_other = cts } - -workListFromCCans :: CanonicalCts -> WorkList --- Generic, no precondition -workListFromCCans cts = WL eqs others - where (eqs, others) = Bag.partitionBag isEqCCan cts - --- Convenience -singleEqWL :: CanonicalCt -> WorkList -singleNonEqWL :: CanonicalCt -> WorkList -singleEqWL = mkEqWorkList . singleCCan -singleNonEqWL = mkNonEqWorkList . singleCCan +emptyWorkList = emptyCCan +workListFromCCan :: CanonicalCt -> WorkList +workListFromCCan = singleCCan +------------------------ data StopOrContinue = Stop -- Work item is consumed | ContinueWith WorkItem -- Not consumed @@ -331,9 +373,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 @@ -367,8 +406,7 @@ runSolverPipeline pipeline inerts workItem , sr_stop = ContinueWith work_item }) = do { itr <- stage work_item inerts ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr) - ; let itr' = itr { sr_new_work = sr_new_work itr - `unionWorkLists` accum_work } + ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr } ; run_pipeline stages itr' } \end{code} @@ -403,8 +441,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 @@ -424,10 +461,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 - ] - ; foldlWorkListM (solveOneWithDepth ctxt) inert ws } + vcat [ text "Current depth =" <+> ppr n + , text "Max depth =" <+> ppr max_depth ] + + -- 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 } ------------------ -- Fully interact the given work item with an inert set, and return a @@ -451,9 +491,10 @@ solveOneWithDepth (max_depth, n, stack) inert work indent = replicate (2*n) ' ' thePipeline :: [(String,SimplifierStage)] -thePipeline = [ ("interact with inerts", interactWithInertsStage) - , ("spontaneous solve", spontaneousSolveStage) - , ("top-level reactions", topReactionsStage) ] +thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage) + , ("interact with inerts", interactWithInertsStage) + , ("spontaneous solve", spontaneousSolveStage) + , ("top-level reactions", topReactionsStage) ] \end{code} ********************************************************************************* @@ -462,6 +503,64 @@ thePipeline = [ ("interact with inerts", interactWithInertsStage) * * ********************************************************************************* +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 @@ -472,55 +571,37 @@ 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 } } -{-- This is all old code, but does not quite work now. The problem is that due to - Note [Loopy Spontaneous Solving] we may have unflattened a type, to be able to - perform a sneaky unification. This unflattening means that we may have to recanonicalize - a given (solved) equality, this is why the result of trySpontaneousSolve is now a list - of constraints (instead of an atomic solved constraint). We would have to react all of - them once again with the worklist but that is very tiresome. Instead we throw them back - in the worklist. - - | isWantedCt workItem - -- Original was wanted we have now made him given so - -- we have to ineract him with the inerts again because - -- of the change in his status. This may produce some work. - -> do { traceTcS "recursive interact with inerts {" $ vcat - [ text "work = " <+> ppr workItem' - , text "inerts = " <+> ppr inerts ] - ; itr_again <- interactWithInertsStage workItem' inerts - ; case sr_stop itr_again of - Stop -> pprPanic "BUG: Impossible to happen" $ - vcat [ text "Original workitem:" <+> ppr workItem - , text "Spontaneously solved:" <+> ppr workItem' - , text "Solved was consumed, when reacting with inerts:" - , nest 2 (ppr inerts) ] - ContinueWith workItem'' -- Now *this* guy is inert wrt to inerts - -> do { traceTcS "end recursive interact }" $ ppr workItem'' - ; return $ SR { sr_new_work = sr_new_work itr_again - , sr_inerts = sr_inerts itr_again - `extendInertSet` workItem'' - , sr_stop = Stop } } - } - | otherwise - -> return $ SR { sr_new_work = emptyWorkList - , sr_inerts = inerts `extendInertSet` workItem' - , sr_stop = Stop } } ---} - -- @trySpontaneousSolve wi@ solves equalities where one side is a -- touchable unification variable. Returns: -- * Nothing if we were not able to solve it -- * 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 @@ -534,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 ...) = ... @@ -542,33 +625,65 @@ 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, - typeKind xi `isSubKind` tyVarKind tv - = solveWithIdentity inerts cv gw tv xi - | otherwise - = return Nothing + | not (isSigTyVar tv) || isTyVarTy xi + = 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) --- Both tyvars are *touchable* MetaTyvars --- By the CTyEqCan invariant, k2 `isSubKind` k1 + -> 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 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1) | k2 `isSubKind` k1 = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2) - | otherwise = return Nothing + | otherwise -- None is a subkind of the other, but they are both touchable! + = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors] where k1 = tyVarKind tv1 k2 = tyVarKind tv2 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2) \end{code} +Note [Kind errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the wanted problem: + alpha ~ (# Int, Int #) +where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint, +but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay' +simply returns @Nothing@ then that wanted constraint is going to propagate all the way and +get quantified over in inference mode. That's bad because we do know at this point that the +constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails. + +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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -580,12 +695,14 @@ or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds. Given equalities can be freely used to rewrite inside other types or constraints. - We do not have to do the same for wanteds because: - First, wanted equations (tv ~ xi) where tv is a touchable unification variable - may have kinds that do not agree (the kind of xi must be a sub kind of the kind of tv). - Second, any potential kind mismatch will result in the constraint not being soluble, - which will be reported anyway. This is the reason that @trySpontaneousOneWay@ and - @trySpontaneousTwoWay@ will perform a kind compatibility check, and only then will - they proceed to @solveWithIdentity@. + First, wanted equations (tv ~ xi) where tv is a touchable + unification variable may have kinds that do not agree (the + kind of xi must be a sub kind of the kind of tv). Second, any + potential kind mismatch will result in the constraint not + being soluble, which will be reported anyway. This is the + reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@ + will perform a kind compatibility check, and only then will + they proceed to @solveWithIdentity@. Caveat: - Givens from higher-rank, such as: @@ -597,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, @@ -615,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 @@ -633,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 @@ -646,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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -669,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 (mkEqWorkList 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) @@ -813,6 +1004,8 @@ data InteractResult , ir_new_work :: WorkList -- new work items to add to the WorkList + + , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in } -- What to do with the inert reactant. @@ -820,10 +1013,13 @@ data InertAction = KeepInert | DropInert deriving Eq mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult -mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork +mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult -mkIRStop keep newWork = return $ IR Stop keep newWork +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 @@ -832,43 +1028,86 @@ noInteraction :: Monad m => WorkItem -> m InteractResult noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList data WhichComesFromInert = LeftComesFromInert | RightComesFromInert + -- See Note [Efficient Orientation, Case 2] + --------------------------------------------------- --- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop --- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've --- interacted the WorkItem with the entire InertSet. --- --- Postcondition: the new InertSet in the resulting StageResult is subset --- of the input InertSet. +-- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we +-- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've +-- interact the WorkItem with the entire equalities of the InertSet + +interactWithInertEqsStage :: SimplifierStage +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_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 } + + +--------------------------------------------------- +-- 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! interactWithInertsStage :: SimplifierStage interactWithInertsStage workItem inert - = foldlInertSetM 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 { sr_inerts = emptyInert - , sr_new_work = emptyWorkList - , sr_stop = ContinueWith workItem } - - - interactNext :: StageResult -> AtomicInert -> TcS StageResult - interactNext it inert - | ContinueWith workItem <- sr_stop it - = do { ir <- interactWithInert inert workItem - ; let inerts = sr_inerts it - ; return $ SR { sr_inerts = if ir_inert_action ir == KeepInert - then inerts `updInertSet` inert - else inerts - , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir - , sr_stop = ir_stop ir } } - | otherwise = return $ itrAddInert inert it - - - itrAddInert :: AtomicInert -> StageResult -> StageResult - itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert } + 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 + | ContinueWith workItem <- sr_stop it + = do { let inerts = sr_inerts it + fdimprs_old = getFDImprovements inerts + + ; 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 + + ; 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 :: AtomicInert -> WorkItem -> TcS InteractResult -interactWithInert inert workitem +interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult +interactWithInert fdimprs inert workitem = do { ctxt <- getTcSContext ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem inert_ev = cc_id inert @@ -881,12 +1120,12 @@ interactWithInert inert workitem -- We don't have to do this for givens, as we fully know the evidence for them. ; rec_ev_ok <- case (cc_flavor inert, cc_flavor workitem) of - (Wanted loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc) - (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc) - _ -> return True + (Wanted loc, Derived {}) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc) + (Derived {}, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc) + _ -> return True ; if is_allowed && rec_ev_ok then - doInteractWithInert inert workitem + doInteractWithInert fdimprs inert workitem else noInteraction workitem } @@ -898,10 +1137,10 @@ allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only allowedInteraction _ _ _ = True -------------------------------------------- -doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult +doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult -- Identical class constraints. -doInteractWithInert +doInteractWithInert fdimprs (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) @@ -909,87 +1148,77 @@ doInteractWithInert | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2)) = -- See Note [When improvement happens] - do { let work_item_pred_loc = (ClassP cls2 tys2, ppr d2) - inert_pred_loc = (ClassP cls1 tys1, ppr d1) + do { let pty1 = ClassP cls1 tys1 + pty2 = ClassP cls2 tys2 + work_item_pred_loc = (pty2, ppr d2) + inert_pred_loc = (pty1, ppr d1) loc = combineCtLoc fl1 fl2 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs - ; fd_cts <- canWanteds wevvars - ; let fd_work = mkEqWorkList fd_cts + ; fd_work <- canWanteds wevvars -- See Note [Generating extra equalities] - ; if isEmptyCCan fd_cts || not (isWanted fl2) then -- || or impr. had previously kicked in - -- No improvement kicked in, keep going + ; traceTcS "Checking if improvements existed." (ppr fdimprs) + ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then + -- Must keep going mkIRContinue workItem KeepInert fd_work - else -- Improvement kicked in, throw him back into the worklist so that he - -- gets rewritten. The reason is that we do not want to let him fall off - -- at the end and then add its potential un-improved superclasses. This - -- optimisation crucially relies on prioritizing the equalities in the - -- worklist. - - -- The termination of this relies on wanteds being able to rewrite wanteds. - -- Since the class may be at the bottom of an equality worklist, which may - -- consist of insoluble wanteds, if these wanteds *never* become solved or given - -- (because they mention untouchables), the workitem will *never* be rewritten - -- so next time we meet him we will be once again producing FunDep equalities - -- for ever and ever! - mkIRStop KeepInert $ fd_work `unionWorkLists` singleNonEqWL workItem - - -- See Note [FunDep Reactions] + else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2)) + ; mkIRStop_RecordImprovement KeepInert + (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2) + } + -- See Note [FunDep Reactions] } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. -doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) +doInteractWithInert _fdimprs + (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis }) | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes xis - -- substitute for tv in xis. Note that the resulting class - -- constraint is still canonical, since substituting xi-types in - -- xi-types generates xi-types. However, it may no longer be - -- inert with respect to the inert set items we've already seen. - -- For example, consider the inert set - -- - -- D Int (g) - -- a ~g Int - -- - -- and the work item D a (w). D a does not interact with D Int. - -- Next, it does interact with a ~g Int, getting rewritten to D - -- Int (w). But now we must go back through the rest of the inert - -- set again, to find that it can now be discharged by the given D - -- Int instance. - = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis) - ; mkIRStop KeepInert $ singleNonEqWL rewritten_dict } + = if isDerivedSC wfl then + mkIRStop KeepInert $ emptyWorkList -- See Note [Adding Derived Superclasses] + else 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 } -doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) +doInteractWithInert _fdimprs + (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 (singleNonEqWL rewritten_dict) } + = if isDerivedSC ifl then + mkIRContinue workItem DropInert emptyWorkList -- No need to do any rewriting, + -- see Note [Adding Derived Superclasses] + else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis) + ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. -doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) +doInteractWithInert _fdimprs + (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty }) | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfType ty = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty) - ; mkIRStop KeepInert (singleNonEqWL rewritten_ip) } + ; mkIRContinue rewritten_ip KeepInert emptyWorkList } -doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) +doInteractWithInert _fdimprs + (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 (singleNonEqWL rewritten_ip) } + ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) } -- Two implicit parameter constraints. If the names are the same, -- but their types are not, we generate a wanted type equality -- that equates the type (this is "improvement"). -- However, we don't actually need the coercion evidence, -- so we just generate a fresh coercion variable that isn't used anywhere. -doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) +doInteractWithInert _fdimprs + (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 }) | nm1 == nm2 && isGiven wfl && isGiven ifl = -- See Note [Overriding implicit parameters] @@ -1005,7 +1234,7 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i do { co_var <- newWantedCoVar ty1 ty2 ; let flav = Wanted (combineCtLoc ifl wfl) ; cans <- mkCanonical flav co_var - ; mkIRContinue workItem KeepInert (mkEqWorkList cans) } + ; mkIRContinue workItem KeepInert cans } -- Inert: equality, work item: function equality @@ -1017,56 +1246,59 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i -- we will ``expose'' x2 and x4 to rewriting. -- Otherwise, we can try rewriting the type function equality with the equality. -doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 }) +doInteractWithInert _fdimprs + (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 }) (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc , cc_tyargs = args, cc_rhs = xi2 }) | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes args = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) - ; mkIRStop KeepInert (singleEqWL rewritten_funeq) } + ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) } + -- must Stop here, because we may no longer be inert after the rewritting. -- Inert: function equality, work item: equality - -doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc +doInteractWithInert _fdimprs + (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc , cc_tyargs = args, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 }) | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfTypes args = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) - ; mkIRContinue workItem DropInert (singleEqWL rewritten_funeq) } + ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) } -doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 +doInteractWithInert _fdimprs + (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 , cc_tyargs = args1, cc_rhs = xi1 }) workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2 , cc_tyargs = args2, cc_rhs = xi2 }) | fl1 `canSolve` fl2 && lhss_match = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert (mkEqWorkList cans) } + ; mkIRStop KeepInert cans } | fl2 `canSolve` fl1 && lhss_match = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert (mkEqWorkList cans) } + ; mkIRContinue workItem DropInert cans } where lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) -doInteractWithInert +doInteractWithInert _fdimprs inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 }) -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert (mkEqWorkList cans) } + ; mkIRStop KeepInert cans } | fl2 `canSolve` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert (mkEqWorkList 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 (mkEqWorkList 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 (mkEqWorkList 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 @@ -1078,11 +1310,11 @@ doInteractWithInert isMetaTyVar tv1, -- and has a unification variable lhs FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2' - = mkIRContinue workItem DropInert (singleEqWL inert) + = mkIRContinue workItem DropInert (workListFromCCan inert) -- Fall-through case for all other situations -doInteractWithInert _ workItem = noInteraction workItem +doInteractWithInert _fdimprs _ workItem = noInteraction workItem ------------------------- -- Equational Rewriting @@ -1133,7 +1365,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 @@ -1158,26 +1390,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 --- Used to ineratct two equalities of the following form: +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) -> @@ -1628,20 +1854,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 @@ -1651,51 +1917,13 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc -- Solved and new wanted work produced, you may cache the -- (tentatively solved) dictionary as Derived and its superclasses - else do { let solved = makeSolved workItem - ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis - ; let inst_work = workListFromCCans workList + else do { let solved = makeSolvedByInst workItem + ; sc_work <- newDerivedSCWork dv loc cls xis + -- See Note [Adding Derived Superclasses] ; 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 = mkEqWorkList fd_cts - - ; if isEmptyCCan fd_cts then - do { sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis - ; 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` singleNonEqWL 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] - } - --- Otherwise, we have a given or derived -doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl - , cc_class = cls, cc_tyargs = xis }) - = do { sc_work <- newSCWorkFromFlavored dv fl 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 @@ -1723,8 +1951,7 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe ; can_cts <- mkCanonical fl cv' - ; let workList = mkEqWorkList can_cts - ; return $ SomeTopInt workList Stop } + ; return $ SomeTopInt can_cts Stop } _ -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!" } @@ -1732,8 +1959,80 @@ 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] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Generally speaking, we want to be able to add derived superclasses of +unsolved wanteds, and wanteds that have been partially being solved +via an instance. This is important to be able to simplify the inferred +constraints more (and to allow for recursive dictionaries, less +importantly). Example: + +Inferred wanted constraint is (Eq a, Ord a), but we'd only like to +quantify over Ord a, hence we would like to be able to add the +superclass of Ord a as Derived and use it to solve the wanted Eq a. + +Hence we will add Derived superclasses in the following two cases: + (1) When we meet an unsolved wanted in top-level reactions + (2) When we partially solve a wanted in top-level reactions using an instance decl. + +At that point, we have two options: + (1) Add transitively add *ALL* of the superclasses of the Derived + (2) Add only the immediate ones, but whenever we meet a Derived in + the future, add its own superclasses as Derived. + +Option (2) is terrible, because deriveds may be rewritten or kicked +out of the inert set, which will result in slightly rewritten +superclasses being reintroduced in the worklist and the inert set. Eg: + + class C a => B a + instance Foo a => B [a] + +Original constraints: +[Wanted] d : B [a] +[Given] co : a ~ Int + +We apply the instance to the wanted and put it and its superclasses as +as Deriveds in the inerts: + +[Derived] d : B [a] +[Derived] (sel d) : C [a] + +The work is now: +[Given] co : a ~ Int +[Wanted] d' : Foo a + +Now, suppose that we interact the Derived with the Given equality, and +kick him out of the inert, the next time around a superclass C [Int] +will be produced -- but we already *have* C [a] in the inerts which +will anyway get rewritten to C [Int]. + +So we choose (1), and *never* introduce any more superclass work from +Deriveds. This enables yet another optimisation: If we ever meet an +equality that can rewrite a Derived, if that Derived is a superclass +derived (like C [a] above), i.e. not a partially solved one (like B +[a]) above, we may simply completely *discard* that Derived. The +reason is because somewhere in the inert lies the original wanted, or +partially solved constraint that gave rise to that superclass, and +that constraint *will* be kicked out, and *will* result in the +rewritten superclass to be added in the inerts later on, anyway. + + + Note [FunDep and implicit parameter reactions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Currently, our story of interacting two dictionaries (or a dictionary @@ -1935,25 +2234,42 @@ NB: The desugarer needs be more clever to deal with equalities that participate in recursive dictionary bindings. \begin{code} -newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] - -> TcS WorkList -newSCWorkFromFlavored ev flavor cls xis - | Given loc <- flavor -- The NoScSkol says "don't add superclasses" - , NoScSkol <- ctLocOrigin loc -- Very important! + +newGivenSCWork :: EvVar -> GivenLoc -> Class -> [Xi] -> TcS WorkList +newGivenSCWork ev loc cls xis + | NoScSkol <- ctLocOrigin loc -- Very important! = return emptyWorkList - | otherwise + = 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 + ; 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 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta - -- Add *all* its superclasses (equalities or not) as new given work - -- See Note [New Wanted Superclass Work] ; sc_vars <- zipWithM inst_one sc_theta1 [0..] - ; can_cts <- mkCanonicals flavor sc_vars - ; return $ workListFromCCans can_cts - } + ; mkCanonicals flavor sc_vars } where inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n) + data LookupInstResult = NoInstance | GenInst [WantedEvVar] EvTerm