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
* *
*********************************************************************************
+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 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]
---------------------------------------------------
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
-- 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) ->
projects / ghc-hetmet.git / blobdiff