From: simonpj@microsoft.com Date: Mon, 21 Feb 2011 15:32:39 +0000 (+0000) Subject: Fix another fundep error (fixes Trac #4969) X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=d1796b5266121ff6930d6cabba6201e48708703b Fix another fundep error (fixes Trac #4969) If I had a pound for every hour Dimitrios and I have spent making functional dependencies work right, we'd be rich! We had stupidly caused a 'wanted' to be rewritten by a 'derived', with resulting abject failure. As well as fixing the bug, this patch refactors some more, adds useful assert and comments. --- diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 1974143..59d221e 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -162,7 +162,7 @@ flatten fl (TyConApp tc tys) ; return $ (mkCoVarCoercion cv, rhs_var, ct) } else -- Derived or Wanted: make a new *unification* flatten variable do { rhs_var <- newFlexiTcSTy (typeKind fam_ty) - ; cv <- newWantedCoVar fam_ty rhs_var + ; cv <- newCoVar fam_ty rhs_var ; let ct = CFunEqCan { cc_id = cv , cc_flavor = mkWantedFlavor fl -- Always Wanted, not Derived @@ -380,7 +380,7 @@ canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts canEq fl cv ty1 ty2 | tcEqType ty1 ty2 -- Dealing with equality here avoids -- later spurious occurs checks for a~a - = do { when (isWanted fl) (setWantedCoBind cv ty1) + = do { when (isWanted fl) (setCoBind cv ty1) ; return emptyCCan } -- If one side is a variable, orient and flatten, @@ -408,12 +408,12 @@ canEq fl cv s1 s2 Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2 = do { (v1,v2,v3) <- if isWanted fl then -- Wanted - do { v1 <- newWantedCoVar t1a t2a - ; v2 <- newWantedCoVar t1b t2b - ; v3 <- newWantedCoVar t1c t2c + do { v1 <- newCoVar t1a t2a + ; v2 <- newCoVar t1b t2b + ; v3 <- newCoVar t1c t2c ; let res_co = mkCoPredCo (mkCoVarCoercion v1) (mkCoVarCoercion v2) (mkCoVarCoercion v3) - ; setWantedCoBind cv res_co + ; setCoBind cv res_co ; return (v1,v2,v3) } else if isGiven fl then -- Given let co_orig = mkCoVarCoercion cv @@ -439,9 +439,9 @@ canEq fl cv s1 s2 canEq fl cv (FunTy s1 t1) (FunTy s2 t2) = do { (argv, resv) <- if isWanted fl then - do { argv <- newWantedCoVar s1 s2 - ; resv <- newWantedCoVar t1 t2 - ; setWantedCoBind cv $ + do { argv <- newCoVar s1 s2 + ; resv <- newCoVar t1 t2 + ; setCoBind cv $ mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv) ; return (argv,resv) } @@ -463,16 +463,16 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2) canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) | n1 == n2 = if isWanted fl then - do { v <- newWantedCoVar t1 t2 - ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv) + do { v <- newCoVar t1 t2 + ; setCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv) ; canEq fl v t1 t2 } else return emptyCCan -- DV: How to decompose given IP coercions? canEq fl cv (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) | c1 == c2 = if isWanted fl then - do { vs <- zipWithM newWantedCoVar tys1 tys2 - ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) + do { vs <- zipWithM newCoVar tys1 tys2 + ; setCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2 } else return emptyCCan @@ -492,8 +492,8 @@ canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) = -- Generate equalities for each of the corresponding arguments do { argsv <- if isWanted fl then - do { argsv <- zipWithM newWantedCoVar tys1 tys2 - ; setWantedCoBind cv $ + do { argsv <- zipWithM newCoVar tys1 tys2 + ; setCoBind cv $ mkTyConCoercion tc1 (map mkCoVarCoercion argsv) ; return argsv } @@ -513,9 +513,9 @@ canEq fl cv ty1 ty2 , Just (s2,t2) <- tcSplitAppTy_maybe ty2 = do { (cv1,cv2) <- if isWanted fl - then do { cv1 <- newWantedCoVar s1 s2 - ; cv2 <- newWantedCoVar t1 t2 - ; setWantedCoBind cv $ + then do { cv1 <- newCoVar s1 s2 + ; cv2 <- newCoVar t1 t2 + ; setCoBind cv $ mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2) ; return (cv1,cv2) } @@ -735,8 +735,8 @@ canEqLeaf :: TcsUntouchables 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') + then do { cv' <- newCoVar s2 s1 + ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv') ; return cv' } else if isGiven fl then newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv)) @@ -774,7 +774,7 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 ; cv_new <- if no_flattening_happened then return cv else if isGiven fl then return cv else if isWanted fl then - do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2 + do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2 -- cv' : F xis ~ xi2 ; let -- fun_co :: F xis1 ~ F tys1 fun_co = mkTyConCoercion fn cos1 @@ -782,7 +782,7 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 want_co = mkSymCoercion fun_co `mkTransCoercion` mkCoVarCoercion cv' `mkTransCoercion` co2 - ; setWantedCoBind cv want_co + ; setCoBind cv want_co ; return cv' } else -- Derived newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2) @@ -820,8 +820,8 @@ canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2 ; cv_new <- if no_flattening_happened then return cv else if isGiven fl then return cv else if isWanted fl then - do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2 - ; setWantedCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co) + do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2 + ; setCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co) ; return cv' } else -- Derived newDerivedId (EqPred (mkTyVarTy tv) xi2') diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 4889e38..c8b0114 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -406,20 +406,29 @@ tryPreSolveAndInteract sctx dyn_flags flavev@(EvVarX ev_var fl) (all_previous_di = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert) dischargeFromCCans :: CanonicalCts -> FlavoredEvVar -> TcS Bool +-- See if this (pre-canonicalised) work-item is identical to a +-- one already in the inert set. Reasons: +-- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints +-- b) Termination for improve_eqs in TcSimplify.simpl_loop dischargeFromCCans cans (EvVarX ev fl) - = Bag.foldlBagM discharge_ct False cans - where discharge_ct :: Bool -> CanonicalCt -> TcS Bool - discharge_ct True _ct = return True - discharge_ct False ct - | evVarPred (cc_id ct) `tcEqPred` evVarPred ev - , cc_flavor ct `canSolve` fl - = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) - ; return True } - where set_ev_bind x y - | EqPred {} <- evVarPred y - = setEvBind x (EvCoercion (mkCoVarCoercion y)) - | otherwise = setEvBind x (EvId y) - discharge_ct False _ct = return False + = Bag.foldrBag discharge_ct (return False) cans + where + the_pred = evVarPred ev + + discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool + discharge_ct ct _rest + | evVarPred (cc_id ct) `tcEqPred` the_pred + , cc_flavor ct `canSolve` fl + = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) + -- Deriveds need no evidence + -- For Givens, we already have evidence, and we don't need it twice + ; return True } + where + set_ev_bind x y + | EqPred {} <- evVarPred y = setEvBind x (EvCoercion (mkCoVarCoercion y)) + | otherwise = setEvBind x (EvId y) + + discharge_ct _ct rest = rest \end{code} Note [Avoiding the superclass explosion] @@ -729,7 +738,7 @@ solveWithIdentity cv wd tv xi ; setWantedTyBind tv xi ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi - ; when (isWanted wd) (setWantedCoBind cv xi) + ; when (isWanted wd) (setCoBind cv xi) -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)' ; return $ SPSolved (CTyEqCan { cc_id = cv_given @@ -738,14 +747,37 @@ solveWithIdentity cv wd tv xi \end{code} - - ********************************************************************************* * * The interact-with-inert Stage * * ********************************************************************************* +Note [The Solver Invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We always add Givens first. So you might think that the solver has +the invariant + + If the work-item is Given, + then the inert item must Given + +But this isn't quite true. Suppose we have, + c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int +After processing the first two, we get + c1: [G] beta ~ [alpha], c2 : [W] blah +Now, c3 does not interact with the the given c1, so when we spontaneously +solve c3, we must re-react it with the inert set. So we can attempt a +reaction between inert c2 [W] and work-item c3 [G]. + +It *is* true that [Solver Invariant] + If the work-item is Given, + AND there is a reaction + then the inert item must Given +or, equivalently, + If the work-item is Given, + and the inert item is Wanted/Derived + then there is no reaction + \begin{code} -- Interaction result of WorkItem <~> AtomicInert data InteractResult @@ -774,11 +806,16 @@ mkIRContinue rule wi keep newWork = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep , ir_new_work = newWork, ir_fire = Just rule } -mkIRStop :: String -> WorkList -> TcS InteractResult -mkIRStop rule newWork +mkIRStopK :: String -> WorkList -> TcS InteractResult +mkIRStopK rule newWork = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert , ir_new_work = newWork, ir_fire = Just rule } +mkIRStopD :: String -> WorkList -> TcS InteractResult +mkIRStopD rule newWork + = return $ IR { ir_stop = Stop, ir_inert_action = DropInert + , ir_new_work = newWork, ir_fire = Just rule } + noInteraction :: Monad m => WorkItem -> m InteractResult noInteraction wi = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert @@ -879,15 +916,15 @@ interactNext depth inert it -- Do a single interaction of two constraints. interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult -interactWithInert inert workitem - = do { ctxt <- getTcSContext - ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem +interactWithInert inert workItem + = do { ctxt <- getTcSContext + ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workItem - ; if is_allowed then - doInteractWithInert inert workitem + ; if is_allowed then + doInteractWithInert inert workItem else - noInteraction workitem - } + noInteraction workItem + } allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool -- Allowed interactions @@ -900,10 +937,10 @@ doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult -- Identical class constraints. doInteractWithInert - (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 }) + inertItem@(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) - = solveOneFromTheOther (d1,fl1) workItem + = solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2)) = -- See Note [When improvement happens] @@ -920,34 +957,51 @@ doInteractWithInert ; case m of Nothing -> noInteraction workItem Just (rewritten_tys2, cos2, fd_work) - | tcEqTypes tys1 rewritten_tys2 -> -- Solve him on the spot in this case - do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2 - ; when (isWanted fl2) $ setDictBind d2 (EvCast d1 dict_co) - ; mkIRStop "Cls/Cls fundep (solved)" fd_work } + case fl2 of + Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem) + Derived {} -> mkIRStopK "Cls/Cls fundep (solved)" fd_work + Wanted {} + | isDerived fl1 + -> do { setDictBind d2 (EvCast d1 dict_co) + ; let inert_w = inertItem { cc_flavor = fl2 } + -- A bit naughty: we take the inert Derived, + -- turn it into a Wanted, use it to solve the work-item + -- and put it back into the work-list + -- Maybe rather than starting again, we could *replace* the + -- inert item, but its safe and simple to restart + ; mkIRStopD "Cls/Cls fundep (solved)" (inert_w `consBag` fd_work) } + + | otherwise + -> do { setDictBind d2 (EvCast d1 dict_co) + ; mkIRStopK "Cls/Cls fundep (solved)" fd_work } - | isWanted fl2 - -> -- We could not quite solve him, but we stil rewrite him + | otherwise + -> -- We could not quite solve him, but we still rewrite him -- Example: class C a b c | a -> b -- Given: C Int Bool x, Wanted: C Int beta y -- Then rewrite the wanted to C Int Bool y -- but note that is still not identical to the given -- The important thing is that the rewritten constraint is -- inert wrt the given. - -- In fact, it is inert wrt all the previous inerts too, so - -- we can keep on going rather than sending it back to the work list - do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2 - ; d2' <- newDictVar cls1 rewritten_tys2 - ; setDictBind d2 (EvCast d2' dict_co) + -- However it is not necessarily inert wrt previous inert-set items. + -- class C a b c d | a -> b, b c -> d + -- Inert: c1: C b Q R S, c2: C P Q a b + -- Work: C P alpha R beta + -- Does not react with c1; reacts with c2, with alpha:=Q + -- NOW it reacts with c1! + -- So we must stop, and put the rewritten constraint back in the work list + do { d2' <- newDictVar cls1 rewritten_tys2 + ; case fl2 of + Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem) + Wanted {} -> setDictBind d2 (EvCast d2' dict_co) + Derived {} -> return () ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 } - ; mkIRContinue "Cls/Cls fundep (partial)" workItem' KeepInert fd_work } + ; mkIRStopK "Cls/Cls fundep (partial)" (workItem' `consBag` fd_work) } - | otherwise - -> ASSERT (isDerived fl2) -- Derived constraints have no evidence, - -- so just produce the rewritten constraint - let workItem' = workItem { cc_tyargs = rewritten_tys2 } - in mkIRContinue "Cls/Cls fundep" workItem' KeepInert fd_work + where + dict_co = mkTyConCoercion (classTyCon cls1) cos2 } -- Class constraint and given equality: use the equality to rewrite @@ -1000,11 +1054,11 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i mkIRContinue "IP/IP override" workItem DropInert emptyWorkList | nm1 == nm2 && ty1 `tcEqType` ty2 - = solveOneFromTheOther (id1,ifl) workItem + = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem | nm1 == nm2 = -- See Note [When improvement happens] - do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation] + do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation] ; let flav = Wanted (combineCtLoc ifl wfl) ; cans <- mkCanonical flav co_var ; mkIRContinue "IP/IP fundep" workItem KeepInert cans } @@ -1021,7 +1075,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_ | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) - ; mkIRStop "Eq/FunEq" (workListFromCCan rewritten_funeq) } + ; mkIRStopK "Eq/FunEq" (workListFromCCan rewritten_funeq) } -- Must Stop here, because we may no longer be inert after the rewritting. -- Inert: function equality, work item: equality @@ -1047,7 +1101,7 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 , cc_tyargs = args2, cc_rhs = xi2 }) | fl1 `canSolve` fl2 && lhss_match = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop "FunEq/FunEq" cans } + ; mkIRStopK "FunEq/FunEq" cans } | fl2 `canSolve` fl1 && lhss_match = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) ; mkIRContinue "FunEq/FunEq" workItem DropInert cans } @@ -1059,7 +1113,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop "Eq/Eq lhs" cans } + ; mkIRStopK "Eq/Eq lhs" cans } | fl2 `canSolve` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) @@ -1068,7 +1122,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc -- Check for rewriting RHS | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2) - ; mkIRStop "Eq/Eq rhs" rewritten_eq } + ; mkIRStopK "Eq/Eq rhs" rewritten_eq } | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) @@ -1078,7 +1132,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, (CFrozenErr { cc_id = cv2, cc_flavor = fl2 }) | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) - ; mkIRStop "Frozen/Eq" rewritten_frozen } + ; mkIRStopK "Frozen/Eq" rewritten_frozen } doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 }) workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) @@ -1131,16 +1185,16 @@ rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F ar xi2' = substTyWith [tv] [xi1] xi2 xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2' - ; cv2' <- case gw of - Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2' - ; setWantedCoBind cv2 $ - fun_co `mkTransCoercion` - mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co - ; return cv2' } - Given {} -> newGivenCoVar (mkTyConApp tc args') xi2' $ - mkSymCoercion fun_co `mkTransCoercion` - mkCoVarCoercion cv2 `mkTransCoercion` xi2_co - Derived {} -> newDerivedId (EqPred (mkTyConApp tc args') xi2') + + ; cv2' <- newCoVar (mkTyConApp tc args') xi2' + ; case gw of + Wanted {} -> setCoBind cv2 (fun_co `mkTransCoercion` + mkCoVarCoercion cv2' `mkTransCoercion` + mkSymCoercion xi2_co) + Given {} -> setCoBind cv2' (mkSymCoercion fun_co `mkTransCoercion` + mkCoVarCoercion cv2 `mkTransCoercion` + xi2_co) + Derived {} -> return () ; return (CFunEqCan { cc_id = cv2' , cc_flavor = gw @@ -1159,78 +1213,62 @@ rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkLis rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) | Just tv2' <- tcGetTyVar_maybe xi2' , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2 - = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2')) + = do { when (isWanted gw) (setCoBind cv2 (mkSymCoercion co2')) ; return emptyCCan } | otherwise - = do { cv2' <- - case gw of - Wanted {} - -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2' - ; setWantedCoBind cv2 $ - mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2' - ; return cv2' } - Given {} - -> newGivenCoVar (mkTyVarTy tv2) xi2' $ - mkCoVarCoercion cv2 `mkTransCoercion` co2' - Derived {} - -> newDerivedId (EqPred (mkTyVarTy tv2) xi2') - - ; canEq gw cv2' (mkTyVarTy tv2) xi2' - } + = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2' + ; case gw of + Wanted {} -> setCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion` + mkSymCoercion co2' + Given {} -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion` + co2' + Derived {} -> return () + ; 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 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 +-- Where the cv1 `canRewrite` cv2 equality -- 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) -> - do { cv2' <- newWantedCoVar xi2 xi1 - ; setWantedCoBind cv2 $ - co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2') - ; return cv2' } - (True,RightComesFromInert) -> - do { cv2' <- newWantedCoVar xi1 xi2 - ; setWantedCoBind cv2 $ - co1 `mkTransCoercion` mkCoVarCoercion cv2' - ; return cv2' } - (False,LeftComesFromInert) -> - if isGiven gw then - newGivenCoVar xi2 xi1 $ - mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 - else newDerivedId (EqPred xi2 xi1) - (False,RightComesFromInert) -> - if isGiven gw then - newGivenCoVar xi1 xi2 $ - mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 - else newDerivedId (EqPred xi1 xi2) +rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2) + = do { cv2' <- newCoVar xi2 xi1 + ; case gw of + Wanted {} -> setCoBind cv2 $ + co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2') + Given {} -> setCoBind cv2' $ + mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 + Derived {} -> return () ; mkCanonical gw cv2' } - + +rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2) + = do { cv2' <- newCoVar xi1 xi2 + ; case gw of + Wanted {} -> setCoBind cv2 $ + co1 `mkTransCoercion` mkCoVarCoercion cv2' + Given {} -> setCoBind cv2' $ + mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 + Derived {} -> return () + ; mkCanonical gw cv2' } + rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) - = do { cv2' <- - case fl2 of - Wanted {} -> do { cv2' <- newWantedCoVar ty2a' ty2b' - -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1] - ; setWantedCoBind cv2 $ - co2a' `mkTransCoercion` - mkCoVarCoercion cv2' `mkTransCoercion` - mkSymCoercion co2b' - ; return cv2' } - - Given {} -> newGivenCoVar ty2a' ty2b' $ - mkSymCoercion co2a' `mkTransCoercion` - mkCoVarCoercion cv2 `mkTransCoercion` - co2b' - - Derived {} -> newDerivedId (EqPred ty2a' ty2b') + = do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1] + ; case fl2 of + Wanted {} -> setCoBind cv2 $ co2a' `mkTransCoercion` + mkCoVarCoercion cv2' `mkTransCoercion` + mkSymCoercion co2b' + + Given {} -> setCoBind cv2' $ mkSymCoercion co2a' `mkTransCoercion` + mkCoVarCoercion cv2 `mkTransCoercion` + co2b' + + Derived {} -> return () + ; return (singleCCan $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) } where (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b @@ -1240,30 +1278,29 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a -- ty2a ~ ty2a[xi1/tv1] co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1] -solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult +solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult -- First argument inert, second argument work-item. They both represent --- wanted/given/derived evidence for the *same* predicate so we try here to --- discharge one directly from the other. +-- wanted/given/derived evidence for the *same* predicate so +-- we can discharge one directly from the other. -- -- Precondition: value evidence only (implicit parameters, classes) -- not coercion -solveOneFromTheOther (iid,ifl) workItem +solveOneFromTheOther info (ev_term,ifl) workItem | isDerived wfl - = mkIRStop "Solved (derived)" emptyWorkList - - | ifl `canSolve` wfl - = do { when (isWanted wfl) $ setEvBind wid (EvId iid) - -- Overwrite the binding, if one exists - -- For Givens, which are lambda-bound, nothing to overwrite, - ; mkIRStop "Solved" emptyWorkList } + = mkIRStopK ("Solved[DW] " ++ info) emptyWorkList - | wfl `canSolve` ifl - = do { when (isWanted ifl) $ setEvBind iid (EvId wid) - ; mkIRContinue "Solved inert" workItem DropInert emptyWorkList } - - | otherwise -- The inert item is Derived, we can just throw it away, - = mkIRContinue "Discard derived inert" workItem DropInert emptyWorkList + | isDerived ifl -- The inert item is Derived, we can just throw it away, + -- The workItem is inert wrt earlier inert-set items, + -- so it's safe to continue on from this point + = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert emptyWorkList + | otherwise + = ASSERT( ifl `canSolve` wfl ) + -- Because of Note [The Solver Invariant], plus Derived dealt with + do { when (isWanted wfl) $ setEvBind wid ev_term + -- Overwrite the binding, if one exists + -- If both are Given, we already have evidence; no need to duplicate + ; mkIRStopK ("Solved " ++ info) emptyWorkList } where wfl = cc_flavor workItem wid = cc_id workItem @@ -1758,8 +1795,8 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl -- See Note [Type synonym families] in TyCon coe = mkTyConApp coe_tc rep_tys ; cv' <- case fl of - Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi - ; setWantedCoBind cv $ + Wanted {} -> do { cv' <- newCoVar rhs_ty xi + ; setCoBind cv $ coe `mkTransCoercion` mkCoVarCoercion cv' ; return cv' } diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index b68fee5..9d74ff8 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -26,7 +26,7 @@ module TcMType ( -------------------------------- -- Creating new evidence variables newEvVar, newCoVar, newEvVars, - newWantedCoVar, writeWantedCoVar, readWantedCoVar, + writeWantedCoVar, readWantedCoVar, newIP, newDict, newSilentGiven, isSilentEvVar, newWantedEvVar, newWantedEvVars, @@ -129,16 +129,13 @@ newEvVars :: TcThetaType -> TcM [EvVar] newEvVars theta = mapM newEvVar theta newWantedEvVar :: TcPredType -> TcM EvVar -newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2 +newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2 newWantedEvVar (ClassP cls tys) = newDict cls tys newWantedEvVar (IParam ip ty) = newIP ip ty newWantedEvVars :: TcThetaType -> TcM [EvVar] newWantedEvVars theta = mapM newWantedEvVar theta -newWantedCoVar :: TcType -> TcType -> TcM CoVar -newWantedCoVar ty1 ty2 = newCoVar ty1 ty2 - -------------- newEvVar :: TcPredType -> TcM EvVar -- Creates new *rigid* variables for predicates diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index ad24eb7..bf3ab32 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -26,13 +26,12 @@ module TcSMonad ( SimplContext(..), isInteractive, simplEqsOnly, performDefaulting, -- Creation of evidence variables - newEvVar, newCoVar, newWantedCoVar, newGivenCoVar, + newEvVar, newCoVar, newGivenCoVar, newDerivedId, newIPVar, newDictVar, newKindConstraint, -- Setting evidence variables - setWantedCoBind, - setIPBind, setDictBind, setEvBind, + setCoBind, setIPBind, setDictBind, setEvBind, setWantedTyBind, @@ -290,12 +289,14 @@ canSolve :: CtFlavor -> CtFlavor -> Bool -- active(tv ~ xi) = tv -- active(D xis) = D xis -- active(IP nm ty) = nm +-- +-- NB: either (a `canSolve` b) or (b `canSolve` a) must hold ----------------------------------------- canSolve (Given {}) _ = True -canSolve (Derived {}) (Wanted {}) = False -- DV: changing the semantics -canSolve (Derived {}) (Derived {}) = True -- DV: changing the semantics of derived +canSolve (Wanted {}) (Derived {}) = True canSolve (Wanted {}) (Wanted {}) = True -canSolve _ _ = False +canSolve (Derived {}) (Derived {}) = True -- Important: derived can't solve wanted/given +canSolve _ _ = False -- (There is no *evidence* for a derived.) canRewrite :: CtFlavor -> CtFlavor -> Bool -- canRewrite ctid1 ctid2 @@ -548,10 +549,8 @@ getTcEvBindsBag = do { EvBindsVar ev_ref _ <- getTcEvBinds ; wrapTcS $ TcM.readTcRef ev_ref } -setWantedCoBind :: CoVar -> Coercion -> TcS () -setWantedCoBind cv co - = setEvBind cv (EvCoercion co) - -- Was: wrapTcS $ TcM.writeWantedCoVar cv co +setCoBind :: CoVar -> Coercion -> TcS () +setCoBind cv co = setEvBind cv (EvCoercion co) setWantedTyBind :: TcTyVar -> TcType -> TcS () -- Add a type binding @@ -706,7 +705,7 @@ newKindConstraint :: TcTyVar -> Kind -> TcS CoVar newKindConstraint tv knd = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd ; let ty_k = mkTyVarTy tv_k - ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k + ; co_var <- newCoVar (mkTyVarTy tv) ty_k ; return co_var } instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar @@ -737,9 +736,6 @@ newGivenCoVar ty1 ty2 co ; setEvBind cv (EvCoercion co) ; return cv } -newWantedCoVar :: TcType -> TcType -> TcS EvVar -newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2 - newCoVar :: TcType -> TcType -> TcS EvVar newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 55520fb..eecfb27 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -982,7 +982,7 @@ solveCTyFunEqs cts ; return (niFixTvSubst ni_subst, unsolved_can_cts) } where - solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setWantedCoBind cv ty + solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty ------------ type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)]) diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 8045327..4fc50b3 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -520,7 +520,7 @@ uType, uType_np, uType_defer -- See Note [Deferred unification] uType_defer (item : origin) ty1 ty2 = wrapEqCtxt origin $ - do { co_var <- newWantedCoVar ty1 ty2 + do { co_var <- newCoVar ty1 ty2 ; loc <- getCtLoc (TypeEqOrigin item) ; emitFlat (mkEvVarX co_var loc)