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
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
, 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
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
| 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
* *
*********************************************************************************
+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
, 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
-- * 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
| 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 ...) = ...
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
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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,
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
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
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
----------------
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)
noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
+ -- See Note [Efficient Orientation, Case 2]
---------------------------------------------------
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))
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
, 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)
-- 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
, 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
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) ->
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
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
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!"
}
-- 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]
| 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
projects / ghc-hetmet.git / blobdiff