X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=f0edcc97f49106a1ddec382dba3271db02173e88;hb=debb7b80e707c343a3a7d8993ffab19b83e5c52b;hp=b079368816a1dcd98883f96d31f83b82ab1f6e88;hpb=bff88b3a5bf96eea57e99a09774a74bd18cf4e13;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index b079368..f0edcc9 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -1,18 +1,21 @@ \begin{code} module TcInteract ( solveInteract, AtomicInert, - InertSet, emptyInert, extendInertSet, extractUnsolved, solveOne, + InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, listToWorkList ) where #include "HsVersions.h" + import BasicTypes import TcCanonical import VarSet import Type +import TypeRep import Id +import VarEnv import Var import TcType @@ -33,13 +36,16 @@ import Outputable import TcRnTypes import TcErrors import TcSMonad -import qualified Bag as Bag +import Bag +import qualified Data.Map as Map +import Maybes + import Control.Monad( zipWithM, unless ) import FastString ( sLit ) import DynFlags \end{code} -Note [InsertSet invariants] +Note [InertSet invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ An InertSet is a bag of canonical constraints, with the following invariants: @@ -76,13 +82,97 @@ now we do not distinguish between given and solved constraints. Note that we must switch wanted inert items to given when going under an implication constraint (when in top-level inference mode). +Note [InertSet FlattenSkolemEqClass] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The inert_fsks field of the inert set contains an "inverse map" of all the +flatten skolem equalities in the inert set. For instance, if inert_cts looks +like this: + + fsk1 ~ fsk2 + fsk3 ~ fsk2 + fsk4 ~ fsk5 + +Then, the inert_fsks fields holds the following map: + fsk2 |-> { fsk1, fsk3 } + fsk5 |-> { fsk4 } +Along with the necessary coercions to convert fsk1 and fsk3 back to fsk2 +and fsk4 back to fsk5. Hence, the invariants of the inert_fsks field are: + + (a) All TcTyVars in the domain and range of inert_fsks are flatten skolems + (b) All TcTyVars in the domain of inert_fsk occur naked as rhs in some + equalities of inert_cts + (c) For every mapping fsk1 |-> { (fsk2,co), ... } it must be: + co : fsk2 ~ fsk1 + +The role of the inert_fsks is to make it easy to maintain the equivalence +class of each flatten skolem, which is much needed to correctly do spontaneous +solving. See Note [Loopy Spontaneous Solving] \begin{code} -- See Note [InertSet invariants] +data InertSet + = IS { inert_cts :: Bag.Bag CanonicalCt + , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] } + -- See Note [InertSet FlattenSkolemEqClass] -newtype InertSet = IS (Bag.Bag CanonicalCt) instance Outputable InertSet where - ppr (IS cts) = vcat (map ppr (Bag.bagToList cts)) + ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_cts is)) + , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest)) + (Map.toList $ inert_fsks is) + ) + ] + +emptyInert :: InertSet +emptyInert = IS { inert_cts = Bag.emptyBag, inert_fsks = Map.empty } + +updInertSet :: InertSet -> AtomicInert -> InertSet +-- Introduces an element in the inert set for the first time +updInertSet (IS { inert_cts = cts, inert_fsks = fsks }) + item@(CTyEqCan { cc_id = cv + , cc_tyvar = tv1 + , cc_rhs = xi }) + | Just tv2 <- tcGetTyVar_maybe xi, + FlatSkol {} <- tcTyVarDetails tv1, + FlatSkol {} <- tcTyVarDetails tv2 + = let cts' = cts `Bag.snocBag` item + fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks + -- See Note [InertSet FlattenSkolemEqClass] + in IS { inert_cts = cts', inert_fsks = fsks' } +updInertSet (IS { inert_cts = cts + , inert_fsks = fsks }) item + = let cts' = cts `Bag.snocBag` item + in IS { inert_cts = cts', inert_fsks = fsks } + +foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a +foldlInertSetM k z (IS { inert_cts = cts }) + = Bag.foldlBagM k z cts + +extractUnsolved :: InertSet -> (InertSet, CanonicalCts) +extractUnsolved is@(IS {inert_cts = cts}) + = (is { inert_cts = cts'}, unsolved) + where (unsolved, cts') = Bag.partitionBag isWantedCt cts + + +getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)] +-- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass] +getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv + = case lkpTyEqCanByLhs of + Nothing -> fromMaybe [] (Map.lookup tv fsks) + Just ceq -> + case tcGetTyVar_maybe (cc_rhs ceq) of + Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs + -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq) + mk_co (v,c) = (v, mkTransCoercion c ceq_co) + in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks) + _ -> [] + where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts + lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt + lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct + lkp other _ct = other + + +isWantedCt :: CanonicalCt -> Bool +isWantedCt ct = isWanted (cc_flavor ct) {- TODO: Later ... data Inert = IS { class_inerts :: FiniteMap Class Atomics @@ -94,22 +184,6 @@ data Inert = IS { class_inerts :: FiniteMap Class Atomics Later should we also separate out givens and wanteds? -} -emptyInert :: InertSet -emptyInert = IS Bag.emptyBag - -extendInertSet :: InertSet -> AtomicInert -> InertSet -extendInertSet (IS cts) item = IS (cts `Bag.snocBag` item) - -foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a -foldlInertSetM k z (IS cts) = Bag.foldlBagM k z cts - -extractUnsolved :: InertSet -> (InertSet, CanonicalCts) -extractUnsolved (IS cts) - = (IS cts', unsolved) - where (unsolved, cts') = Bag.partitionBag isWantedCt cts - -isWantedCt :: CanonicalCt -> Bool -isWantedCt ct = isWanted (cc_flavor ct) \end{code} Note [Touchables and givens] @@ -172,9 +246,9 @@ Note [Basic plan] type AtomicInert = CanonicalCt -- constraint pulled from InertSet type WorkItem = CanonicalCt -- constraint pulled from WorkList -type SWorkItem = WorkItem -- a work item we know is solved type WorkList = CanonicalCts -- A mixture of Given, Wanted, and Solved +type SWorkList = WorkList -- A worklist of solved listToWorkList :: [WorkItem] -> WorkList @@ -192,6 +266,9 @@ isEmptyWorkList = Bag.isEmptyBag emptyWorkList :: WorkList emptyWorkList = Bag.emptyBag +singletonWorkList :: CanonicalCt -> WorkList +singletonWorkList ct = singleCCan ct + data StopOrContinue = Stop -- Work item is consumed | ContinueWith WorkItem -- Not consumed @@ -238,7 +315,7 @@ runSolverPipeline pipeline inerts workItem ; let new_inert = case sr_stop itr_out of Stop -> sr_inerts itr_out - ContinueWith item -> sr_inerts itr_out `extendInertSet` item + ContinueWith item -> sr_inerts itr_out `updInertSet` item ; return (new_inert, sr_new_work itr_out) } where run_pipeline :: [(String, SimplifierStage)] @@ -349,14 +426,27 @@ thePipeline = [ ("interact with inerts", interactWithInertsStage) \begin{code} spontaneousSolveStage :: SimplifierStage spontaneousSolveStage workItem inerts - = do { mSolve <- trySpontaneousSolve workItem + = do { mSolve <- trySpontaneousSolve workItem inerts ; case mSolve of Nothing -> -- no spontaneous solution for him, keep going return $ SR { sr_new_work = emptyWorkList , sr_inerts = inerts , sr_stop = ContinueWith workItem } - Just workItem' -- He has been solved; workItem' is a Given + Just workList' -> -- He has been solved; workList' are all givens + return $ SR { sr_new_work = workList' + , sr_inerts = inerts + , 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 @@ -382,54 +472,58 @@ spontaneousSolveStage workItem inerts -> 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] -trySpontaneousSolve :: WorkItem -> TcS (Maybe SWorkItem) -trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) +-- Note, 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 + | isGiven gw + = return Nothing | Just tv2 <- tcGetTyVar_maybe xi = do { tch1 <- isTouchableMetaTyVar tv1 ; tch2 <- isTouchableMetaTyVar tv2 ; case (tch1, tch2) of - (True, True) -> trySpontaneousEqTwoWay cv gw tv1 tv2 - (True, False) -> trySpontaneousEqOneWay cv gw tv1 xi + (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2 + (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi (False, True) | tyVarKind tv1 `isSubKind` tyVarKind tv2 - -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1) + -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1) _ -> return Nothing } | otherwise = do { tch1 <- isTouchableMetaTyVar tv1 - ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi + ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi else return Nothing } -- No need for -- trySpontaneousSolve (CFunEqCan ...) = ... -- See Note [No touchables as FunEq RHS] in TcSMonad -trySpontaneousSolve _ = return Nothing +trySpontaneousSolve _ _ = return Nothing ---------------- -trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi - -> TcS (Maybe SWorkItem) +trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi + -> TcS (Maybe SWorkList) -- tv is a MetaTyVar, not untouchable -- Precondition: kind(xi) is a sub-kind of kind(tv) -trySpontaneousEqOneWay cv gw tv xi +trySpontaneousEqOneWay inerts cv gw tv xi | not (isSigTyVar tv) || isTyVarTy xi - = solveWithIdentity cv gw tv xi + = solveWithIdentity inerts cv gw tv xi | otherwise = return Nothing ---------------- -trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar - -> TcS (Maybe SWorkItem) +trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar + -> TcS (Maybe SWorkList) -- Both tyvars are *touchable* MetaTyvars -- By the CTyEqCan invariant, k2 `isSubKind` k1 -trySpontaneousEqTwoWay cv gw tv1 tv2 +trySpontaneousEqTwoWay inerts cv gw tv1 tv2 | k1 `eqKind` k2 - , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1) + , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1) | otherwise = ASSERT( k2 `isSubKind` k1 ) - solveWithIdentity cv gw tv1 (mkTyVarTy tv2) + solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2) where k1 = tyVarKind tv1 k2 = tyVarKind tv2 @@ -449,8 +543,42 @@ where (fsk := E alpha, on the side). Now, if we spontaneously *solve* it and keep it as wanted. In inference mode we'll end up quantifying over (alpha ~ Maybe (E alpha)) Hence, 'solveWithIdentity' performs a small occurs check before -actually solving. But this occurs check *must look through* flatten -skolems. +actually solving. But this occurs check *must look through* flatten skolems. + +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: + +Original wanteds: + g: F alpha ~ F beta + w: alpha ~ F alpha +After canonicalization: + g: F beta ~ f1 + g: F alpha ~ f1 + w: alpha ~ f2 + g: F alpha ~ f2 +After some reactions: + g: f1 ~ f2 + g: F beta ~ f1 + w: alpha ~ f2 + g: F alpha ~ f2 +At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved. +We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However +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! + +A similar problem happens because of other spontaneous solving. Suppose we have the +following wanteds, arriving in this exact order: + (first) w: beta ~ alpha + (second) w: alpha ~ fsk + (third) g: F beta ~ fsk +Then, we first spontaneously solve the first constraint, making (beta := alpha), and having +(beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not +obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But +that is wrong since fsk mentions beta, which has already secretly been unified to alpha! + +To avoid this problem, the same occurs check must unveil rewritings that can happen because +of spontaneously having solved other constraints. + Note [Avoid double unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -458,73 +586,141 @@ The spontaneous solver has to return a given which mentions the unified unificat variable *on the left* of the equality. Here is what happens if not: Original wanted: (a ~ alpha), (alpha ~ Int) We spontaneously solve the first wanted, without changing the order! - given : a ~ alpha [having unifice alpha := a] + given : a ~ alpha [having unified alpha := a] Now the second wanted comes along, but he cannot rewrite the given, so we simply continue. At the end we spontaneously solve that guy, *reunifying* [alpha := Int] -We avoid this problem by orienting the given so that the unification variable is on the left. -[Note that alternatively we could attempt to enforce this at canonicalization] +We avoid this problem by orienting the given so that the unification +variable is on the left. [Note that alternatively we could attempt to +enforce this at canonicalization] -Avoiding double unifications is yet another reason to disallow touchable unification variables -as RHS of type family equations: F xis ~ alpha. Consider having already spontaneously solved -a wanted (alpha ~ [b]) by setting alpha := [b]. So the inert set looks like: - given : alpha ~ [b] -And now a new wanted (F tau ~ alpha) comes along. Since it does not react with anything -we will be left with a constraint (F tau ~ alpha) that must cause a unification of -(alpha := F tau) at some point (either in spontaneous solving, or at the end). But alpha -is *already* unified so we must not do anything to it. By disallowing naked touchables in -the RHS of constraints (in favor of introduced flatten skolems) we do not have to worry at -all about unifying or spontaneously solving (F xis ~ alpha) by unification. +See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding +double unifications is the main reason we disallow touchable +unification variables as RHS of type family equations: F xis ~ alpha. \begin{code} ---------------- -solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS (Maybe SWorkItem) +solveWithIdentity :: InertSet + -> CoVar -> CtFlavor -> TcTyVar -> Xi + -> TcS (Maybe SWorkList) -- Solve with the identity coercion -- Precondition: kind(xi) is a sub-kind of kind(tv) --- See [New Wanted Superclass Work] to see why we do this for *given* as well -solveWithIdentity cv gw tv xi - | tv `elemVarSet` tyVarsOfUnflattenedType xi - -- Beware of Note [Loopy spontaneous solving] - -- Can't spontaneously solve loopy equalities - -- though they are not a type error - = return Nothing - | not (isGiven gw) -- Wanted or Derived - = 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 -- Set tv := xi - ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi - -- Create new given with identity evidence - - ; case gw of - Wanted {} -> setWantedCoBind cv xi - Derived {} -> setDerivedCoBind cv xi - _ -> pprPanic "Can't spontaneously solve *given*" empty - - ; let solved = CTyEqCan { cc_id = cv_given - , cc_flavor = mkGivenFlavor gw UnkSkol - , cc_tyvar = tv, cc_rhs = xi } - -- See Note [Avoid double unifications] - - -- The reason that we create a new given variable (cv_given) instead of reusing cv - -- is because we do not want to end up with coercion unification variables in the givens. - ; return (Just solved) } - | otherwise -- Given - = return Nothing - -tyVarsOfUnflattenedType :: TcType -> TcTyVarSet --- A version of tyVarsOfType which looks through flatSkols -tyVarsOfUnflattenedType ty - = foldVarSet (unionVarSet . do_tv) emptyVarSet (tyVarsOfType ty) +-- Precondition: CtFlavor is Wanted or Derived +-- See [New Wanted Superclass Work] to see why solveWithIdentity +-- must work for Derived as well as Wanted +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 - do_tv :: TyVar -> TcTyVarSet - do_tv tv = ASSERT( isTcTyVar tv) - case tcTyVarDetails tv of - FlatSkol ty -> tyVarsOfUnflattenedType ty - _ -> unitVarSet tv + 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) + ; 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) +-- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem. +-- If it appears under some flatten skolem look in that flatten skolem equivalence class +-- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you +-- can find a different flatten skolem to use, that is, one that does not mention @tv@. +-- +-- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty +-- coi :: ty' ~ ty +-- NB: The returned type ty' may not be flat! + +occurCheck ty_binds inerts the_tv the_ty + = ok emptyVarSet the_ty + where + -- If (fsk `elem` bad) then tv occurs in any rendering + -- of the type under the expansion of fsk + ok bad this_ty@(TyConApp tc tys) + | Just tys_cois <- allMaybes (map (ok bad) tys) + , (tys',cois') <- unzip tys_cois + = Just (TyConApp tc tys', mkTyConAppCoI tc cois') + | isSynTyCon tc, Just ty_expanded <- tcView this_ty + = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify + ok bad (PredTy sty) + | Just (sty',coi) <- ok_pred bad sty + = Just (PredTy sty', coi) + ok bad (FunTy arg res) + | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res + = Just (FunTy arg' res', mkFunTyCoI coiarg coires) + ok bad (AppTy fun arg) + | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg + = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg) + ok bad (ForAllTy tv1 ty1) + -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment. + | Just (ty1', coi) <- ok bad ty1 + = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi) + + -- Variable cases + ok bad this_ty@(TyVarTy tv) + | tv == the_tv = Nothing -- Occurs check error + | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var + | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty + | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty + | otherwise = Just (this_ty, IdCo this_ty) + + -- Check if there exists a ty bind already, as a result of sneaky unification. + -- Fall through + ok _bad _ty = Nothing + + ----------- + ok_pred bad (ClassP cn tys) + | Just tys_cois <- allMaybes $ map (ok bad) tys + = let (tys', cois') = unzip tys_cois + in Just (ClassP cn tys', mkClassPPredCoI cn cois') + ok_pred bad (IParam nm ty) + | Just (ty',co') <- ok bad ty + = Just (IParam nm ty', mkIParamPredCoI nm co') + ok_pred bad (EqPred ty1 ty2) + | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2 + = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2) + ok_pred _ _ = Nothing + + ----------- + ok_fsk bad fsk zty + | fsk `elemVarSet` bad + -- We are already trying to find a rendering of fsk, + -- and to do that it seems we need a rendering, so fail + = Nothing + | otherwise + = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs) + where + fsk_equivs = getFskEqClass inerts fsk + new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs) + + ----------- + go_under_fsk bad_tvs (fsk,co) + | FlatSkol zty <- tcTyVarDetails fsk + = case ok bad_tvs zty of + Nothing -> Nothing + Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co)) + | otherwise = pprPanic "go_down_equiv" (ppr fsk) \end{code} @@ -586,13 +782,14 @@ interactWithInertsStage workItem inert , sr_new_work = emptyCCan , sr_stop = ContinueWith workItem } + 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 `extendInertSet` inert + then inerts `updInertSet` inert else inerts , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir , sr_stop = ir_stop ir } } @@ -600,7 +797,7 @@ interactWithInertsStage workItem inert itrAddInert :: AtomicInert -> StageResult -> StageResult - itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `extendInertSet` inert } + itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert } -- Do a single interaction of two constraints. interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult @@ -766,21 +963,14 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 where lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) -doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) +doInteractWithInert + 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 `canRewrite` fl2 && tv1 == tv2 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) ; mkIRStop KeepInert cans } -{- - | fl1 `canRewrite` fl2 -- If at all possible, keep the inert, - , Just tv1_rhs <- tcGetTyVar_maybe xi1 -- special case of inert a~b - , tv1_rhs == tv2 - = do { cans <- rewriteEqLHS (mkSymCoercion (mkCoVarCoercion cv1), mkTyVarTy tv1) - (cv2,fl2,xi2) - ; mkIRStop KeepInert cans } --} | fl2 `canRewrite` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) ; mkIRContinue workItem DropInert cans } @@ -793,8 +983,20 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) ; 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 +-- inert, drop the inert out because you may have to reconsider solving the +-- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving] +-- and [InertSet FlattenSkolemEqClass] + + | not $ isGiven fl1, -- The inert is wanted or derived + 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 (singletonWorkList inert) + --- Fall-through case for all other cases +-- Fall-through case for all other situations doInteractWithInert _ workItem = noInteraction workItem -------------------------------------------- @@ -918,15 +1120,6 @@ rewriteEqLHS which (co1,xi1) (cv2,gw,xi2) mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 ; mkCanonical gw cv2' } --- -> --- if isWanted gw then --- do { cv2' <- newWantedCoVar xi1 xi2 --- ; setWantedCoBind cv2 $ --- co1 `mkTransCoercion` mkCoVarCoercion cv2' --- ; return cv2' } --- else newGivOrDerCoVar xi1 xi2 $ --- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 --- ; mkCanonical gw cv2' } solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult @@ -1592,19 +1785,18 @@ new given work. There are several reasons for this: Now suppose that we have: given: C a b wanted: C a beta - By interacting the given we will get that (F a ~ b) which is not + By interacting the given we will get given (F a ~ b) which is not enough by itself to make us discharge (C a beta). However, we - may create a new given equality from the super-class that we promise - to solve: (F a ~ beta). Now we may interact this with the rest of - constraint to finally get: - given : beta ~ b - + may create a new derived equality from the super-class of the + wanted constraint (C a beta), namely derived (F a ~ beta). + Now we may interact this with given (F a ~ b) to get: + derived : beta ~ b But 'beta' is a touchable unification variable, and hence OK to - unify it with 'b', replacing the given evidence with the identity. + unify it with 'b', replacing the derived evidence with the identity. - This requires trySpontaneousSolve to solve given equalities that - have a touchable in their RHS, *in addition* to solving wanted - equalities. + This requires trySpontaneousSolve to solve *derived* + equalities that have a touchable in their RHS, *in addition* + to solving wanted equalities. Here is another example where this is useful. @@ -1693,5 +1885,3 @@ matchClassInst clas tys loc } } \end{code} - -