-- Deriveds need no evidence
-- For Givens, we already have evidence, and we don't need it twice
; return True }
-- Deriveds need no evidence
-- For Givens, we already have evidence, and we don't need it twice
; return True }
-- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
; return $ SPSolved (CTyEqCan { cc_id = cv_given
-- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
; return $ SPSolved (CTyEqCan { cc_id = cv_given
doInteractWithInert
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 })
doInteractWithInert
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 })
= solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
| cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
= solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
| cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
; case m of
Nothing -> noInteraction workItem
Just (rewritten_tys2, cos2, fd_work)
; case m of
Nothing -> noInteraction workItem
Just (rewritten_tys2, cos2, fd_work)
-> -- Solve him on the spot in this case
case fl2 of
Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
-> -- Solve him on the spot in this case
case fl2 of
Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
-- we must *override* the outer one with the inner one
mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
-- we must *override* the outer one with the inner one
mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
= solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
| nm1 == nm2
= -- See Note [When improvement happens]
do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation]
= solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
| nm1 == nm2
= -- See Note [When improvement happens]
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 }
+ ; let flav = Wanted (combineCtLoc ifl wfl)
+ ; cans <- mkCanonical flav co_var
+ ; case wfl of
+ Given {} -> pprPanic "Unexpected given IP" (ppr workItem)
+ Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
+ Wanted {} ->
+ do { setIPBind (cc_id workItem) $
+ EvCast id1 (mkSymCo (mkCoVarCo co_var))
+ ; mkIRStopK "IP/IP interaction (solved)" cans }
+ }
-- Never rewrite a given with a wanted equality, and a type function
-- equality can never rewrite an equality. We rewrite LHS *and* RHS
-- Never rewrite a given with a wanted equality, and a type function
-- equality can never rewrite an equality. We rewrite LHS *and* RHS
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
| fl1 `canSolve` fl2 && lhss_match
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
| fl1 `canSolve` fl2 && lhss_match
- = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
+ = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
doInteractWithInert (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 `canSolve` fl2 && tv1 == tv2
doInteractWithInert (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 `canSolve` fl2 && tv1 == tv2
- = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
+ = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
-- Equational Rewriting
rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
-- Equational Rewriting
rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
Given {} -> setDictBind dv' (EvCast dv dict_co)
Derived {} -> return () -- Derived dicts we don't set any evidence
Given {} -> setDictBind dv' (EvCast dv dict_co)
Derived {} -> return () -- Derived dicts we don't set any evidence
rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
- = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
- ty' = substTyWith [tv] [xi] ty
+ = do { let ip_co = liftCoSubstWith [tv] [mkCoVarCo cv] ty -- ty[tv] ~ t[xi]
+ ty' = substTyWith [tv] [xi] ty
Given {} -> setIPBind ipid' (EvCast ipid ip_co)
Derived {} -> return () -- Derived ips: we don't set any evidence
Given {} -> setIPBind ipid' (EvCast ipid ip_co)
Derived {} -> return () -- Derived ips: we don't set any evidence
rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
- = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
- args' = substTysWith [tv] [xi1] args
- fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args'
+ = do { let co_subst = liftCoSubstWith [tv] [mkCoVarCo cv1]
+ arg_cos = map co_subst args
+ args' = substTysWith [tv] [xi1] args
+ fun_co = mkTyConAppCo tc arg_cos -- fun_co :: F args ~ F args'
- Wanted {} -> setCoBind cv2 (fun_co `mkTransCoercion`
- mkCoVarCoercion cv2' `mkTransCoercion`
- mkSymCoercion xi2_co)
- Given {} -> setCoBind cv2' (mkSymCoercion fun_co `mkTransCoercion`
- mkCoVarCoercion cv2 `mkTransCoercion`
+ Wanted {} -> setCoBind cv2 (fun_co `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo xi2_co)
+ Given {} -> setCoBind cv2' (mkSymCo fun_co `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
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
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
- Wanted {} -> setCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion`
- mkSymCoercion co2'
- Given {} -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion`
+ Wanted {} -> setCoBind cv2 $ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo co2'
+ Given {} -> setCoBind cv2' $ mkCoVarCo cv2 `mkTransCo`
rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
-- Used to ineract two equalities of the following form:
rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
-- Used to ineract two equalities of the following form:
rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
= do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
; case fl2 of
rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
= do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
; case fl2 of
- co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
- co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
+ co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
+ co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
-- First argument inert, second argument work-item. They both represent
solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
-- First argument inert, second argument work-item. They both represent
; case m of
Nothing -> return NoTopInt
Just (xis',cos,fd_work) ->
; case m of
Nothing -> return NoTopInt
Just (xis',cos,fd_work) ->
; dv'<- newDictVar cls xis'
; setDictBind dv (EvCast dv' dict_co)
; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
; dv'<- newDictVar cls xis'
; setDictBind dv (EvCast dv' dict_co)
; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
-- RHS of a type function, so that it never
-- appears in an error message
-- See Note [Type synonym families] in TyCon
-- RHS of a type function, so that it never
-- appears in an error message
-- See Note [Type synonym families] in TyCon
Derived {} -> newDerivedId (EqPred xi rhs_ty)
; can_cts <- mkCanonical fl cv'
; return $ SomeTopInt can_cts Stop }
Derived {} -> newDerivedId (EqPred xi rhs_ty)
; can_cts <- mkCanonical fl cv'
; return $ SomeTopInt can_cts Stop }