-- 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 :: Bag.Bag CanonicalCt -- Equalities only **CTyEqCan**
+ , inert_cts :: Bag.Bag CanonicalCt -- Other constraints
+ , 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))
emptyInert :: InertSet
emptyInert = IS { inert_eqs = Bag.emptyBag
- , inert_cts = Bag.emptyBag, inert_fsks = Map.empty }
+ , inert_cts = Bag.emptyBag, 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 { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks, inert_fds = fdis })
item@(CTyEqCan { cc_id = cv
, cc_tyvar = tv1
, cc_rhs = xi })
= 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' }
+ 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 }) item
- | isEqCCan item
+ , 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 }
+ in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks, inert_fds = fdis }
| otherwise
= let cts' = cts `Bag.snocBag` item
- in IS { inert_eqs = eqs, inert_cts = cts', inert_fsks = fsks }
+ in IS { inert_eqs = eqs, inert_cts = cts', inert_fsks = fsks, inert_fds = fdis }
+
+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
+
+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})
+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_cts = solved_cts, inert_fsks = Map.empty, inert_fds = fdis }
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
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'
+
+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
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
, 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
, 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}
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
- ]
- ; 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 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
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}
*********************************************************************************
* *
*********************************************************************************
+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 }
}
-{-- 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
| 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,
- 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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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:
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 (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)
, 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.
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
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_cts = inert_cts 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
+ = foldISOtherCtsM interactNext initITR inert
where
- initITR = SR { sr_inerts = emptyInert
+ 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 }
+interactNext :: StageResult -> AtomicInert -> TcS StageResult
+interactNext it inert
+ | ContinueWith workItem <- sr_stop it
+ = do { let inerts = sr_inerts it
+ fdimprs_old = getFDImprovements inerts
- 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 }
+ ; 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
-- 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
}
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)
| 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
-
+ 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]
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
-- 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
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
, 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
--- 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) ->
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
-- 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
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!"
}
-- 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
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
projects / ghc-hetmet.git / blobdiff