\begin{code}
module TcCanonical(
mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck,
- canEq
+ canEq, canEqLeafTyVarLeft
) where
#include "HsVersions.h"
-- If one side is a variable, orient and flatten,
-- WITHOUT expanding type synonyms, so that we tend to
--- substitute a~Age rather than a~Int when type Age=Ing
-canEq fl cv ty1@(TyVarTy {}) ty2 = canEqLeaf fl cv (classify ty1) (classify ty2)
-canEq fl cv ty1 ty2@(TyVarTy {}) = canEqLeaf fl cv (classify ty1) (classify ty2)
- -- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
+-- substitute a ~ Age rather than a ~ Int when @type Age = Int@
+canEq fl cv ty1@(TyVarTy {}) ty2
+ = do { untch <- getUntouchables
+ ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
+canEq fl cv ty1 ty2@(TyVarTy {})
+ = do { untch <- getUntouchables
+ ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
+ -- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
canEq fl cv (TyConApp fn tys) ty2
| isSynFamilyTyCon fn, length tys == tyConArity fn
- = canEqLeaf fl cv (FunCls fn tys) (classify ty2)
+ = do { untch <- getUntouchables
+ ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
canEq fl cv ty1 (TyConApp fn tys)
| isSynFamilyTyCon fn, length tys == tyConArity fn
- = canEqLeaf fl cv (classify ty1) (FunCls fn tys)
+ = do { untch <- getUntouchables
+ ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
canEq fl cv s1 s2
| Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1,
= OtherCls ty
-- See note [Canonical ordering for equality constraints].
-reOrient :: TypeClassifier -> TypeClassifier -> Bool
+reOrient :: Untouchables -> TypeClassifier -> TypeClassifier -> Bool
-- (t1 `reOrient` t2) responds True
-- iff we should flip to (t2~t1)
-- We try to say False if possible, to minimise evidence generation
--
-- Postcondition: After re-orienting, first arg is not OTherCls
-reOrient (OtherCls {}) (FunCls {}) = True
-reOrient (OtherCls {}) (FskCls {}) = True
-reOrient (OtherCls {}) (VarCls {}) = True
-reOrient (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
+reOrient _untch (OtherCls {}) (FunCls {}) = True
+reOrient _untch (OtherCls {}) (FskCls {}) = True
+reOrient _untch (OtherCls {}) (VarCls {}) = True
+reOrient _untch (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
-reOrient (FunCls {}) (VarCls tv2) = isMetaTyVar tv2
+reOrient _untch (FunCls {}) (VarCls tv2) = isMetaTyVar tv2
-- See Note [No touchables as FunEq RHS] in TcSMonad
- -- For convenience we enforce the stronger invariant that no
- -- meta type variable is the RHS of a function equality
-reOrient (FunCls {}) _ = False -- Fun/Other on rhs
+reOrient _untch (FunCls {}) _ = False -- Fun/Other on rhs
-reOrient (VarCls tv1) (FunCls {}) = not (isMetaTyVar tv1)
+reOrient _untch (VarCls tv1) (FunCls {}) = not $ isMetaTyVar tv1
-reOrient (VarCls {}) (FskCls {}) = True
+reOrient _untch (VarCls tv1) (FskCls {}) = not $ isMetaTyVar tv1
-- See Note [Loopy Spontaneous Solving, Example 4]
-reOrient (VarCls {}) (OtherCls {}) = False
-reOrient (VarCls {}) (VarCls {}) = False
+reOrient _untch (VarCls {}) (OtherCls {}) = False
+reOrient _untch (VarCls {}) (VarCls {}) = False
-reOrient (FskCls {}) (VarCls {}) = False
+reOrient _untch (FskCls {}) (VarCls tv2) = isMetaTyVar tv2
-- See Note [Loopy Spontaneous Solving, Example 4]
-reOrient (FskCls {}) (FskCls {}) = False
-reOrient (FskCls {}) (FunCls {}) = True
-reOrient (FskCls {}) (OtherCls {}) = False
+reOrient _untch (FskCls {}) (FskCls {}) = False
+reOrient _untch (FskCls {}) (FunCls {}) = True
+reOrient _untch (FskCls {}) (OtherCls {}) = False
------------------
-canEqLeaf :: CtFlavor -> CoVar
+canEqLeaf :: Untouchables
+ -> CtFlavor -> CoVar
-> TypeClassifier -> TypeClassifier -> TcS CanonicalCts
-- Canonicalizing "leaf" equality constraints which cannot be
-- decomposed further (ie one of the types is a variable or
-- Preconditions:
-- * one of the two arguments is not OtherCls
-- * the two types are not equal (looking through synonyms)
-canEqLeaf fl cv cls1 cls2
- | cls1 `reOrient` cls2
+canEqLeaf untch fl cv cls1 cls2
+ | cls1 `re_orient` cls2
= do { cv' <- if isWanted fl
then do { cv' <- newWantedCoVar s2 s1
; setWantedCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
| otherwise
= canEqLeafOriented fl cv cls1 s2
where
+ re_orient = reOrient untch
s1 = unClassify cls1
s2 = unClassify cls2
-- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft
canEqLeafOriented fl cv (FskCls tv) s2
- = canEqLeafTyVarLeft fl cv tv s2
+ = do { (cc,ccs) <- canEqLeafTyVarLeft fl cv tv s2
+ ; return $ ccs `extendCCans` cc }
canEqLeafOriented fl cv (VarCls tv) s2
- = canEqLeafTyVarLeft fl cv tv s2
+ = do { (cc,ccs) <- canEqLeafTyVarLeft fl cv tv s2
+ ; return $ ccs `extendCCans` cc }
canEqLeafOriented _ cv (OtherCls ty1) ty2
= pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
-canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts
+canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS (CanonicalCt, CanonicalCts)
-- Establish invariants of CTyEqCans
canEqLeafTyVarLeft fl cv tv s2
| isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan
, cc_tyvar = tv
, cc_rhs = xi2'
}
- ; return $ ccs2 `extendCCans` final_cc }
+ ; return $ (final_cc, ccs2) }
where
k1 = tyVarKind tv
k2 = typeKind s2
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
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.
+ -> 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)
projects / ghc-hetmet.git / commitdiff