- -- DV: No special care should be taken for Given/Solveds, we will
- -- never encounter a Given entering the constraint bag after a Given/Solved
- = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct)
+ = do { when (isWanted fl) $ setEvBind ev (evVarTerm (cc_id ct))
-- 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
, cc_flavor = mkSolvedFlavor wd UnkSkol
-- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
; return $ SPSolved (CTyEqCan { cc_id = cv_given
, cc_flavor = mkSolvedFlavor wd UnkSkol
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 (isGivenOrSolved fl1 && isGivenOrSolved fl2))
= solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
| cls1 == cls2 && (not (isGivenOrSolved fl1 && isGivenOrSolved 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
, cc_tyargs = args1, cc_rhs = xi1 })
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
, cc_tyargs = args1, cc_rhs = xi1 })
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
, Just GivenSolved <- isGiven_maybe fl1
= mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
, Just GivenSolved <- isGiven_maybe fl1
= mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
, Just GivenSolved <- isGiven_maybe fl2
= mkIRStopK "Funeq/Funeq" emptyWorkList
| fl1 `canSolve` fl2 && lhss_match
, Just GivenSolved <- isGiven_maybe fl2
= mkIRStopK "Funeq/Funeq" emptyWorkList
| 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
; can_cts <- mkCanonical fl cv'
; let solved = workItem { cc_flavor = solved_fl }
solved_fl = mkSolvedFlavor fl UnkSkol
; can_cts <- mkCanonical fl cv'
; let solved = workItem { cc_flavor = solved_fl }
solved_fl = mkSolvedFlavor fl UnkSkol
, tir_new_inert = ContinueWith solved }
}
Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $
, tir_new_inert = ContinueWith solved }
}
Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $
, text "Silents and their superclasses=" <+> ppr silents_and_their_scs
, text "All given dictionaries=" <+> ppr all_given_dicts ]
; return NoInstance -- see Note [Instance and Given overlap]
, text "Silents and their superclasses=" <+> ppr silents_and_their_scs
, text "All given dictionaries=" <+> ppr all_given_dicts ]
; return NoInstance -- see Note [Instance and Given overlap]