; 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
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,
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
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) }
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
= -- 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 }
, 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) }
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))
; 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
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)
; 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')
= 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]
; 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
\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
= 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
-- 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
-- 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]
; 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
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 }
| 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
, 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 }
-- 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)
-- 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)
(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 })
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
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
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
-- 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' }
projects / ghc-hetmet.git / commitdiff