solving. See Note [Loopy Spontaneous Solving]
\begin{code}
+data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts
+ -- Invariant: all Given or Derived
+ , cts_wanted :: Map.Map a CanonicalCts }
+ -- Invariant: all Wanted
+cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
+cCanMapToBag cmap = Map.fold unionBags rest_cts (cts_givder cmap)
+ where rest_cts = Map.fold unionBags emptyCCan (cts_wanted cmap)
+
+emptyCCanMap :: CCanMap a
+emptyCCanMap = CCanMap { cts_givder = Map.empty, cts_wanted = Map.empty }
+
+updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
+updCCanMap (a,ct) cmap
+ = case cc_flavor ct of
+ Wanted {}
+ -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
+ _
+ -> cmap { cts_givder = Map.insertWith unionBags a this_ct (cts_givder cmap) }
+ where this_ct = singleCCan ct
+
+getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
+-- Gets the relevant constraints and returns the rest of the CCanMap
+getRelevantCts a cmap
+ = let relevant = unionBags (Map.findWithDefault emptyCCan a (cts_wanted cmap))
+ (Map.findWithDefault emptyCCan a (cts_givder cmap))
+ residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
+ , cts_givder = Map.delete a (cts_givder cmap) }
+ in (relevant, residual_map)
+
+extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
+-- Gets the wanted constraints and returns a residual CCanMap
+extractUnsolvedCMap cmap =
+ let unsolved = Map.fold unionBags emptyCCan (cts_wanted cmap)
+ in (unsolved, cmap { cts_wanted = Map.empty})
+
-- See Note [InertSet invariants]
data InertSet
- = IS { inert_eqs :: Bag.Bag CanonicalCt -- Equalities only **CTyEqCan**
- , inert_cts :: Bag.Bag CanonicalCt -- Other constraints
+ = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan)
+
+ , inert_dicts :: CCanMap Class -- Dictionaries only
+ , inert_ips :: CCanMap (IPName Name) -- Implicit parameters
+ , inert_funeqs :: CCanMap TyCon -- Type family equalities only
+ -- This representation allows us to quickly get to the relevant
+ -- inert constraints when interacting a work item with the inert set.
+
+
, inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already
-- and reside either in the worklist or in the inerts
, inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
instance Outputable InertSet where
ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
- , vcat (map ppr (Bag.bagToList $ inert_cts is))
+ , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
+ , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
+ , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
, vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest))
(Map.toList $ inert_fsks is)
)
]
emptyInert :: InertSet
-emptyInert = IS { inert_eqs = Bag.emptyBag
- , inert_cts = Bag.emptyBag, inert_fsks = Map.empty, inert_fds = [] }
+emptyInert = IS { inert_eqs = Bag.emptyBag
+ , inert_dicts = emptyCCanMap
+ , inert_ips = emptyCCanMap
+ , inert_funeqs = emptyCCanMap
+ , inert_fsks = Map.empty, inert_fds = [] }
updInertSet :: InertSet -> AtomicInert -> InertSet
-- Introduces an element in the inert set for the first time
-updInertSet (IS { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks, inert_fds = fdis })
+updInertSet is@(IS { inert_eqs = eqs, inert_fsks = fsks })
item@(CTyEqCan { cc_id = cv
, cc_tyvar = tv1
, cc_rhs = xi })
= let eqs' = eqs `Bag.snocBag` item
fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
-- See Note [InertSet FlattenSkolemEqClass]
- in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks', inert_fds = fdis }
-updInertSet (IS { inert_eqs = eqs, inert_cts = cts
- , inert_fsks = fsks, inert_fds = fdis }) item
- | isTyEqCCan item
- = let eqs' = eqs `Bag.snocBag` item
- in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks, inert_fds = fdis }
+ in is { inert_eqs = eqs', inert_fsks = fsks' }
+updInertSet is item
+ | isCTyEqCan item -- Other equality
+ = let eqs' = inert_eqs is `Bag.snocBag` item
+ in is { inert_eqs = eqs' }
+ | Just cls <- isCDictCan_Maybe item -- Dictionary
+ = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
+ | Just x <- isCIPCan_Maybe item -- IP
+ = is { inert_ips = updCCanMap (x,item) (inert_ips is) }
+ | Just tc <- isCFunEqCan_Maybe item -- Function equality
+ = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
| otherwise
- = let cts' = cts `Bag.snocBag` item
- in IS { inert_eqs = eqs, inert_cts = cts', inert_fsks = fsks, inert_fds = fdis }
+ = pprPanic "Unknown form of constraint!" (ppr item)
updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet
updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is }
foldISEqCtsM k z IS { inert_eqs = eqs }
= Bag.foldlBagM k z eqs
-foldISOtherCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
--- Fold over other constraints in the inerts
-foldISOtherCtsM k z IS { inert_cts = cts }
- = Bag.foldlBagM k z cts
-
extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
-extractUnsolved is@(IS {inert_eqs = eqs, inert_cts = cts, inert_fds = fdis })
- = let is_init = is { inert_eqs = emptyCCan
- , inert_cts = solved_cts, inert_fsks = Map.empty, inert_fds = fdis }
+extractUnsolved is@(IS {inert_eqs = eqs})
+ = let is_init = is { inert_eqs = emptyCCan
+ , inert_dicts = solved_dicts
+ , inert_ips = solved_ips
+ , inert_funeqs = solved_funeqs }
is_final = Bag.foldlBag updInertSet is_init solved_eqs -- Add equalities carefully
- in (is_final, unsolved)
- where (unsolved_cts, solved_cts) = Bag.partitionBag isWantedCt cts
- (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
- unsolved = unsolved_cts `unionBags` unsolved_eqs
+ in (is_final, unsolved)
+
+ where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
+ (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
+ (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
+ (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
+ unsolved = unsolved_eqs `unionBags`
+ unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)]
-- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass]
-getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv
+getFskEqClass (IS { inert_eqs = cts, inert_fsks = fsks }) tv
= case lkpTyEqCanByLhs of
Nothing -> fromMaybe [] (Map.lookup tv fsks)
Just ceq ->
haveBeenImproved [] _ _ = False
haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2'
| tcEqPred pty1 pty1' && tcEqPred pty2 pty2'
- = True
+ = True
| tcEqPred pty1 pty2' && tcEqPred pty2 pty1'
- = True
- | otherwise
- = haveBeenImproved fdimprs pty1' pty2'
+ = True
+ | otherwise
+ = haveBeenImproved fdimprs pty1' pty2'
-getFDImprovements :: InertSet -> FDImprovements
+getFDImprovements :: InertSet -> FDImprovements
-- Return a list of the improvements that have kicked in so far
-getFDImprovements = inert_fds
-
-
-isWantedCt :: CanonicalCt -> Bool
-isWantedCt ct = isWanted (cc_flavor ct)
-
-{- TODO: Later ...
-data Inert = IS { class_inerts :: FiniteMap Class Atomics
- ip_inerts :: FiniteMap Class Atomics
- tyfun_inerts :: FiniteMap TyCon Atomics
- tyvar_inerts :: FiniteMap TyVar Atomics
- }
-
-Later should we also separate out givens and wanteds?
--}
+getFDImprovements = inert_fds
\end{code}
, text "Max depth =" <+> ppr max_depth ]
-- Solve equalities first
- ; let (eqs, non_eqs) = Bag.partitionBag isTyEqCCan ws
+ ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
There are two cases where we have to be careful about
orienting equalities to get better efficiency.
-Case 1: In Spontaneous Solving
+Case 2: In Rewriting Equalities (function rewriteEqLHS)
- The OrientFlag is used to preserve the original orientation of a
- spontaneously solved equality (insofar the canonical constraints
- invariants allow it). This way we hope to be more efficient since
- when reaching the spontaneous solve stage, a particular
- constraint has already been inert-ified wrt to the preexisting
- inerts.
+ 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.
- Example:
+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)
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, we instead solve (alpha := beta), but we preserve the
- original orientation, so that we get a given (beta ~ alpha),
- which will result in no more inerts getting kicked out of the
- inert set in the next iteration.
-
-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.
+
+ 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.
, 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 }
}
-
-data OrientFlag = OrientThisWay
- | OrientOtherWay -- See Note [Efficient Orientation]
-
-- @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 :: 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
; tch2 <- isTouchableMetaTyVar tv2
; case (tch1, tch2) of
(True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
- (True, False) -> trySpontaneousEqOneWay OrientThisWay inerts cv gw tv1 xi
- (False, True) -> trySpontaneousEqOneWay OrientOtherWay inerts cv gw tv2 (mkTyVarTy tv1)
+ (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
+ (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
_ -> return Nothing }
| otherwise
= do { tch1 <- isTouchableMetaTyVar tv1
- ; if tch1 then trySpontaneousEqOneWay OrientThisWay inerts cv gw tv1 xi
+ ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
; return Nothing }
}
trySpontaneousSolve _ _ = return Nothing
----------------
-trySpontaneousEqOneWay :: OrientFlag
- -> InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
- -> TcS (Maybe SWorkList)
--- NB: The OrientFlag is there to help us recover the orientation of the original
--- constraint which is important for enforcing the canonical constraints invariants.
--- Also, tv is a MetaTyVar, not untouchable
-trySpontaneousEqOneWay or_flag inerts cv gw tv xi
+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
= 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 or_flag inerts cv gw tv xi
+ 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 :: ??
----------------
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
- , nicer_to_update_tv2 = solveWithIdentity OrientOtherWay inerts cv gw tv2 (mkTyVarTy tv1)
+ , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
| k2 `isSubKind` k1
- = solveWithIdentity OrientThisWay inerts cv gw tv1 (mkTyVarTy tv2)
+ = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
| otherwise -- None is a subkind of the other, but they are both touchable!
= kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors]
where
Note [Loopy Spontaneous Solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Example 1: (The problem of 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)
-****************************************************************************
+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)
-*******************************************************************************************
+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)
-************************************************
+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:
as much as possible from the RHS of other wanted equalities, and hence it suffices to look
in their flatten skolem equivalence classes.
-This situation appears in the IndTypesPerf test case, inside indexed-types/.
+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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{code}
----------------
-solveWithIdentity :: OrientFlag
- -> InertSet
+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
-solveWithIdentity or_flag inerts cv gw tv xi
+-- 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
+
+ ; 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 { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
- ; setWantedTyBind tv xi_unflat
- ; can_eqs <- case or_flag of
- OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi_unflat
- OrientOtherWay -> canEq flav cv_given xi_unflat (mkTyVarTy tv)
- ; return (can_eqs, co) }
- IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
- ; setWantedTyBind tv xi
- ; can_eqs <- case or_flag of
- OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi
- OrientOtherWay -> canEq flav cv_given xi (mkTyVarTy tv)
- ; return (can_eqs, co) }
+ ; (ct,cts, co) <- case coi of
+ ACo co -> do { (cc,ccs) <- canEqLeafTyVarLeft flav cv_given tv xi_unflat
+ ; return (cc, ccs, co) }
+ IdCo co -> return $ (CTyEqCan { cc_id = cv_given
+ , cc_flavor = mkGivenFlavor gw UnkSkol
+ , cc_tyvar = tv, cc_rhs = xi }
+ -- xi, *not* xi_unflat because
+ -- xi_unflat may require flattening!
+ , emptyWorkList, co)
; case gw of
Wanted {} -> setWantedCoBind cv co
Derived {} -> setDerivedCoBind cv co
_ -> pprPanic "Can't spontaneously solve *given*" empty
- -- See Note [Avoid double unifications]
- ; return $ Just cts }
+ -- See Note [Avoid double unifications]
+ ; return $ Just (ct,cts)
+ }
+
+-- ; let flav = mkGivenFlavor gw UnkSkol
+-- ; (cts, co) <- case coi of
+-- -- TODO: Optimise this, along the way it used to be
+-- ACo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
+-- ; setWantedTyBind tv xi_unflat
+-- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
+-- ; return (can_eqs, co) }
+-- IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
+-- ; setWantedTyBind tv xi
+-- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi
+-- ; return (can_eqs, co) }
+-- ; case gw of
+-- Wanted {} -> setWantedCoBind cv co
+-- Derived {} -> setDerivedCoBind cv co
+-- _ -> pprPanic "Can't spontaneously solve *given*" empty
+-- -- See Note [Avoid double unifications]
+-- ; return $ Just cts }
occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
-> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
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
= foldISEqCtsM interactNext initITR inert
where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- We will fold over the equalities
, inert_fsks = Map.empty -- which will generate those two again
- , inert_cts = inert_cts inert
- , inert_fds = inert_fds inert
+ , inert_dicts = inert_dicts inert
+ , inert_ips = inert_ips inert
+ , inert_funeqs = inert_funeqs inert
+ , inert_fds = inert_fds inert
}
, sr_new_work = emptyWorkList
, sr_stop = ContinueWith workItem }
-- Interact a single WorkItem with *non-equality* constraints in the inert set.
-- Precondition: equality interactions must have already happened, hence we have
-- to pick up some information from the incoming inert, before folding over the
--- "Other" constraints it contains!
+-- "Other" constraints it contains!
+
interactWithInertsStage :: SimplifierStage
interactWithInertsStage workItem inert
- = foldISOtherCtsM interactNext initITR inert
+ = let (relevant, inert_residual) = getISRelevant workItem inert
+ initITR = SR { sr_inerts = inert_residual
+ , sr_new_work = emptyWorkList
+ , sr_stop = ContinueWith workItem }
+ in Bag.foldlBagM interactNext initITR relevant
where
- initITR = SR { -- Pick up: (1) equations, (2) FD improvements, (3) FlatSkol equiv. classes
- sr_inerts = IS { inert_eqs = inert_eqs inert
- , inert_cts = emptyCCan
- , inert_fds = inert_fds inert
- , inert_fsks = inert_fsks inert }
- , sr_new_work = emptyWorkList
- , sr_stop = ContinueWith workItem }
+ getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
+ getISRelevant (CDictCan { cc_class = cls } ) is
+ = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
+ in (relevant, is { inert_dicts = residual_map })
+ getISRelevant (CFunEqCan { cc_fun = tc } ) is
+ = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
+ in (relevant, is { inert_funeqs = residual_map })
+ getISRelevant (CIPCan { cc_ip_nm = nm }) is
+ = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
+ in (relevant, is { inert_ips = residual_map })
+ -- An equality, finally, may kick everything except equalities out
+ -- because we have already interacted the equalities in interactWithInertEqsStage
+ getISRelevant _eq_ct is -- Equality, everything is relevant for this one
+ -- TODO: if we were caching variables, we'd know that only
+ -- some are relevant. Experiment with this for now.
+ = let cts = cCanMapToBag (inert_ips is) `unionBags`
+ cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
+ in (cts, is { inert_dicts = emptyCCanMap
+ , inert_ips = emptyCCanMap
+ , inert_funeqs = emptyCCanMap })
interactNext :: StageResult -> AtomicInert -> TcS StageResult
interactNext it inert
; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
; fd_work <- canWanteds wevvars
-- See Note [Generating extra equalities]
- ; traceTcS "Checking if improvements existed." (ppr fdimprs)
+ ; traceTcS "Checking if improvements existed." (ppr fdimprs)
; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
-- Must keep going
mkIRContinue workItem KeepInert fd_work
; mkIRStop_RecordImprovement KeepInert
(fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
}
- -- See Note [FunDep Reactions]
+ -- See Note [FunDep Reactions]
}
-- Class constraint and given equality: use the equality to rewrite
projects / ghc-hetmet.git / blobdiff