, vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
, vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
, vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
- , vcat (map ppr (Bag.bagToList $ inert_frozen is))
+ , text "Frozen errors =" <+> -- Clearly print frozen errors
+ vcat (map ppr (Bag.bagToList $ inert_frozen is))
]
emptyInert :: InertSet
discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool
discharge_ct ct _rest
- | evVarPred (cc_id ct) `tcEqPred` the_pred
+ | evVarPred (cc_id ct) `eqPred` the_pred
, cc_flavor ct `canSolve` fl
- -- 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 }
- 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}
]
; setWantedTyBind tv xi
- ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi
+ ; let refl_xi = mkReflCo xi
+ ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_xi
- ; when (isWanted wd) (setCoBind cv xi)
+ ; when (isWanted wd) (setCoBind cv refl_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
, 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 })
- | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
- = solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
- | cls1 == cls2 && (not (isGivenOrSolved fl1 && isGivenOrSolved fl2))
- = -- See Note [When improvement happens]
- do { let pty1 = ClassP cls1 tys1
+ | cls1 == cls2
+ = do { let pty1 = ClassP cls1 tys1
pty2 = ClassP cls2 tys2
inert_pred_loc = (pty1, pprFlavorArising fl1)
work_item_pred_loc = (pty2, pprFlavorArising fl2)
- fd_eqns = improveFromAnother
- inert_pred_loc -- the template
- work_item_pred_loc -- the one we aim to rewrite
- -- See Note [Efficient Orientation]
-
- ; m <- rewriteWithFunDeps fd_eqns tys2 fl2
- ; case m of
- Nothing -> noInteraction workItem
- Just (rewritten_tys2, cos2, fd_work)
- | tcEqTypes tys1 rewritten_tys2
- -> -- Solve him on the spot in this case
- 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 }
+
+ ; any_fundeps
+ <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
+ -- NB: We don't create fds for given (and even solved), have not seen a useful
+ -- situation for these and even if we did we'd have to be very careful to only
+ -- create Derived's and not Wanteds.
+
+ else let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
+ wloc = get_workitem_wloc fl2
+ in rewriteWithFunDeps fd_eqns tys2 wloc
+ -- See Note [Efficient Orientation], [When improvement happens]
+
+ ; case any_fundeps of
+ -- No Functional Dependencies
+ Nothing
+ | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
+ | otherwise -> noInteraction workItem
+
+ -- Actual Functional Dependencies
+ Just (rewritten_tys2,cos2,fd_work)
+ | not (eqTypes tys1 rewritten_tys2)
+ -- Standard thing: create derived fds and keep on going. Importantly we don't
+ -- throw workitem back in the worklist because this can cause loops. See #5236.
+ -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
+ ; mkIRContinue "Cls/Cls fundep (not solved)" workItem KeepInert fd_cans }
+
+ -- This WHOLE otherwise branch is an optimization where the fd made the things match
+ | otherwise
+ , let dict_co = mkTyConAppCo (classTyCon cls1) cos2
+ -> case fl2 of
+ Given {}
+ -> pprPanic "Unexpected given!" (ppr inertItem $$ ppr workItem)
+ -- The only way to have created a fundep is if the inert was
+ -- wanted or derived, in which case the workitem can't be given!
+ Derived {}
+ -- The types were made to exactly match so we don't need
+ -- the workitem any longer.
+ -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
+ -- No rewriting really, so let's create deriveds fds
+ ; mkIRStopK "Cls/Cls fundep (solved)" fd_cans }
+ 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)" $
- workListFromNonEq inert_w `unionWorkList` fd_work }
- | otherwise
- -> do { setDictBind d2 (EvCast d1 dict_co)
- ; mkIRStopK "Cls/Cls fundep (solved)" fd_work }
-
- | 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.
- -- 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 }
- ; mkIRStopK "Cls/Cls fundep (partial)" $
- workListFromNonEq workItem' `unionWorkList` fd_work }
-
- where
- dict_co = mkTyConCoercion (classTyCon cls1) cos2
- }
+ -- Maybe rather than starting again, we could keep going
+ -- with the rewritten workitem, having dropped the inert, but its
+ -- safe to restart.
+
+ -- Also: we have rewriting so lets create wanted fds
+ ; fd_cans <- mkCanonicalFDAsWanted fd_work
+ ; mkIRStopD "Cls/Cls fundep (solved)" $
+ workListFromNonEq inert_w `unionWorkList` fd_cans }
+ | otherwise
+ -> do { setDictBind d2 (EvCast d1 dict_co)
+ -- Rewriting is happening, so we have to create wanted fds
+ ; fd_cans <- mkCanonicalFDAsWanted fd_work
+ ; mkIRStopK "Cls/Cls fundep (solved)" fd_cans }
+ }
+ where get_workitem_wloc (Wanted wl) = wl
+ get_workitem_wloc (Derived wl) = wl
+ get_workitem_wloc (Given {}) = panic "Unexpected given!"
+
-- Class constraint and given equality: use the equality to rewrite
-- the class constraint.
-- we must *override* the outer one with the inner one
mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
- | nm1 == nm2 && ty1 `tcEqType` ty2
+ | nm1 == nm2 && ty1 `eqType` ty2
= solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
| nm1 == nm2
Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
Wanted {} ->
do { setIPBind (cc_id workItem) $
- EvCast id1 (mkSymCoercion (mkCoVarCoercion co_var))
+ EvCast id1 (mkSymCo (mkCoVarCo co_var))
; mkIRStopK "IP/IP interaction (solved)" cans }
}
, cc_tyargs = args1, cc_rhs = xi1 })
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
- | tc1 == tc2 && and (zipWith tcEqType args1 args2)
+ | tc1 == tc2 && and (zipWith eqType args1 args2)
, Just GivenSolved <- isGiven_maybe fl1
= mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
- | tc1 == tc2 && and (zipWith tcEqType args1 args2)
+ | tc1 == tc2 && and (zipWith eqType args1 args2)
, 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)
; mkIRStopK "FunEq/FunEq" cans }
| fl2 `canSolve` fl1 && lhss_match
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
where
- lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
+ lhss_match = tc1 == tc2 && eqTypes args1 args2
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)
; mkIRStopK "Eq/Eq lhs" cans }
| fl2 `canSolve` fl1 && tv1 == tv2
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
-- Check for rewriting RHS
-- Equational Rewriting
rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
- = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
+ = do { let cos = map (liftCoSubstWith [tv] [mkCoVarCo cv]) xis -- xis[tv] ~ xis[xi]
args = substTysWith [tv] [xi] xis
con = classTyCon cl
- dict_co = mkTyConCoercion con cos
+ dict_co = mkTyConAppCo con cos
; dv' <- newDictVar cl args
; case gw of
- Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
+ Wanted {} -> setDictBind dv (EvCast dv' (mkSymCo dict_co))
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)
- = 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
; ipid' <- newIPVar nm ty'
; case gw of
- Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
+ Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCo ip_co))
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
- = 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'
xi2' = substTyWith [tv] [xi1] xi2
- xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2'
+ xi2_co = co_subst xi2 -- xi2_co :: xi2 ~ 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`
+ Wanted {} -> setCoBind cv2 (fun_co `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo xi2_co)
+ Given {} -> setCoBind cv2' (mkSymCo fun_co `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
xi2_co)
Derived {} -> return ()
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) (setCoBind cv2 (mkSymCoercion co2'))
+ = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2'))
; return emptyWorkList }
| otherwise
= do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
; case gw of
- 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`
co2'
Derived {} -> return ()
; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
where
xi2' = substTyWith [tv1] [xi1] xi2
- co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
+ co2' = liftCoSubstWith [tv1] [mkCoVarCo cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
-- Used to ineract two equalities of the following form:
= do { cv2' <- newCoVar xi2 xi1
; case gw of
Wanted {} -> setCoBind cv2 $
- co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
+ co1 `mkTransCo` mkSymCo (mkCoVarCo cv2')
Given {} -> setCoBind cv2' $
- mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
+ mkSymCo (mkCoVarCo cv2) `mkTransCo` co1
Derived {} -> return ()
; mkCanonical gw cv2' }
= do { cv2' <- newCoVar xi1 xi2
; case gw of
Wanted {} -> setCoBind cv2 $
- co1 `mkTransCoercion` mkCoVarCoercion cv2'
+ co1 `mkTransCo` mkCoVarCo cv2'
Given {} -> setCoBind cv2' $
- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
+ mkSymCo co1 `mkTransCo` mkCoVarCo cv2
Derived {} -> return ()
; mkCanonical gw cv2' }
rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
= do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
; case fl2 of
- Wanted {} -> setCoBind cv2 $ co2a' `mkTransCoercion`
- mkCoVarCoercion cv2' `mkTransCoercion`
- mkSymCoercion co2b'
+ Wanted {} -> setCoBind cv2 $ co2a' `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo co2b'
- Given {} -> setCoBind cv2' $ mkSymCoercion co2a' `mkTransCoercion`
- mkCoVarCoercion cv2 `mkTransCoercion`
+ Given {} -> setCoBind cv2' $ mkSymCo co2a' `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
co2b'
Derived {} -> return ()
ty2a' = substTyWith [tv1] [xi1] ty2a
ty2b' = substTyWith [tv1] [xi1] ty2b
- 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
+solveOneFromTheOther_ExtraWork :: String -> (EvTerm, CtFlavor)
+ -> CanonicalCt -> WorkList -> TcS InteractResult
-- First argument inert, second argument work-item. They both represent
-- 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 info (ev_term,ifl) workItem
+solveOneFromTheOther_ExtraWork info (ev_term,ifl) workItem extra_work
| isDerived wfl
- = mkIRStopK ("Solved[DW] " ++ info) emptyWorkList
+ = mkIRStopK ("Solved[DW] " ++ info) extra_work
| 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
+ = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert extra_work
| Just GivenSolved <- isGiven_maybe ifl, isGivenOrSolved wfl
-- Same if the inert is a GivenSolved -- just get rid of it
- = mkIRContinue ("Solved[SI] " ++ info) workItem DropInert emptyWorkList
+ = mkIRContinue ("Solved[SI] " ++ info) workItem DropInert extra_work
| otherwise
= ASSERT( ifl `canSolve` wfl )
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 }
+ ; mkIRStopK ("Solved " ++ info) extra_work }
where
wfl = cc_flavor workItem
wid = cc_id workItem
+
+
+solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
+solveOneFromTheOther str evfl ct
+ = solveOneFromTheOther_ExtraWork str evfl ct emptyWorkList -- extra work is empty
+
\end{code}
Note [Superclasses and recursive dictionaries]
= return NoTopInt -- NB: Superclasses already added since it's canonical
-- Derived dictionary: just look for functional dependencies
-doTopReact _inerts workItem@(CDictCan { cc_flavor = fl@(Derived loc)
+doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
, cc_class = cls, cc_tyargs = xis })
= do { instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs
(ClassP cls xis, pprArisingAt loc)
- ; m <- rewriteWithFunDeps fd_eqns xis fl
+ ; m <- rewriteWithFunDeps fd_eqns xis loc
; case m of
Nothing -> return NoTopInt
Just (xis',_,fd_work) ->
let workItem' = workItem { cc_tyargs = xis' }
-- Deriveds are not supposed to have identity (cc_id is unused!)
- in return $ SomeTopInt { tir_new_work = fd_work
- , tir_new_inert = ContinueWith workItem' } }
+ in do { fd_cans <- mkCanonicalFDAsDerived fd_work
+ ; return $ SomeTopInt { tir_new_work = fd_cans
+ , tir_new_inert = ContinueWith workItem' }
+ }
+ }
+
-- Wanted dictionary
-doTopReact inerts workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
+doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
, cc_class = cls, cc_tyargs = xis })
- = do { -- See Note [MATCHING-SYNONYMS]
- ; lkp_inst_res <- matchClassInst inerts cls xis loc
- ; case lkp_inst_res of
- NoInstance ->
- do { traceTcS "doTopReact/ no class instance for" (ppr dv)
-
- ; instEnvs <- getInstEnvs
- ; let fd_eqns = improveFromInstEnv instEnvs
- (ClassP cls xis, pprArisingAt loc)
- ; m <- rewriteWithFunDeps fd_eqns xis fl
- ; case m of
- Nothing -> return NoTopInt
- Just (xis',cos,fd_work) ->
- do { let dict_co = mkTyConCoercion (classTyCon cls) cos
- ; dv'<- newDictVar cls xis'
- ; setDictBind dv (EvCast dv' dict_co)
- ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
- cc_class = cls, cc_tyargs = xis' }
- ; return $
- SomeTopInt { tir_new_work = workListFromNonEq workItem' `unionWorkList` fd_work
- , tir_new_inert = Stop } } }
-
- GenInst wtvs ev_term -- Solved
- -- No need to do fundeps stuff here; the instance
- -- matches already so we won't get any more info
- -- from functional dependencies
- | null wtvs
- -> do { traceTcS "doTopReact/found nullary class instance for" (ppr dv)
- ; setDictBind dv ev_term
- -- Solved in one step and no new wanted work produced.
- -- i.e we directly matched a top-level instance
- -- No point in caching this in 'inert'; hence Stop
- ; return $ SomeTopInt { tir_new_work = emptyWorkList
- , tir_new_inert = Stop } }
-
- | otherwise
- -> do { traceTcS "doTopReact/found non-nullary class instance for" (ppr dv)
- ; setDictBind dv ev_term
+ -- See Note [MATCHING-SYNONYMS]
+ = do { traceTcS "doTopReact" (ppr workItem)
+ ; instEnvs <- getInstEnvs
+ ; let fd_eqns = improveFromInstEnv instEnvs $ (ClassP cls xis, pprArisingAt loc)
+
+ ; any_fundeps <- rewriteWithFunDeps fd_eqns xis loc
+ ; case any_fundeps of
+ -- No Functional Dependencies
+ Nothing ->
+ do { lkup_inst_res <- matchClassInst inerts cls xis loc
+ ; case lkup_inst_res of
+ GenInst wtvs ev_term
+ -> doSolveFromInstance wtvs ev_term workItem emptyWorkList
+ NoInstance
+ -> return NoTopInt
+ }
+ -- Actual Functional Dependencies
+ Just (xis',cos,fd_work) ->
+ do { lkup_inst_res <- matchClassInst inerts cls xis' loc
+ ; case lkup_inst_res of
+ NoInstance
+ -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
+ ; return $
+ SomeTopInt { tir_new_work = fd_cans
+ , tir_new_inert = ContinueWith workItem } }
+ -- This WHOLE branch is an optimization: we can immediately discharge the dictionary
+ GenInst wtvs ev_term
+ -> do { let dict_co = mkTyConAppCo (classTyCon cls) cos
+ ; fd_cans <- mkCanonicalFDAsWanted fd_work
+ ; dv' <- newDictVar cls xis'
+ ; setDictBind dv' ev_term
+ ; doSolveFromInstance wtvs (EvCast dv' dict_co) workItem fd_cans }
+ } }
+
+ where doSolveFromInstance :: [WantedEvVar]
+ -> EvTerm
+ -> CanonicalCt
+ -> WorkList -> TcS TopInteractResult
+ -- Precondition: evidence term matches the predicate of cc_id of workItem
+ doSolveFromInstance wtvs ev_term workItem extra_work
+ | null wtvs
+ = do { traceTcS "doTopReact/found nullary instance for" (ppr (cc_id workItem))
+ ; setDictBind (cc_id workItem) ev_term
+ ; return $ SomeTopInt { tir_new_work = extra_work
+ , tir_new_inert = Stop } }
+ | otherwise
+ = do { traceTcS "doTopReact/found non-nullary instance for" (ppr (cc_id workItem))
+ ; setDictBind (cc_id workItem) ev_term
-- Solved and new wanted work produced, you may cache the
-- (tentatively solved) dictionary as Solved given.
- ; let solved = workItem { cc_flavor = solved_fl }
- solved_fl = mkSolvedFlavor fl UnkSkol
- ; inst_work <- canWanteds wtvs
- ; return $ SomeTopInt { tir_new_work = inst_work
- , tir_new_inert = ContinueWith solved } }
- }
+ ; let solved = workItem { cc_flavor = solved_fl }
+ solved_fl = mkSolvedFlavor fl UnkSkol
+ ; inst_work <- canWanteds wtvs
+ ; return $ SomeTopInt { tir_new_work = inst_work `unionWorkList` extra_work
+ , tir_new_inert = ContinueWith solved } }
+
-- Type functions
doTopReact _inerts (CFunEqCan { cc_flavor = fl })
-- RHS of a type function, so that it never
-- appears in an error message
-- See Note [Type synonym families] in TyCon
- coe = mkTyConApp coe_tc rep_tys
+ coe = mkAxInstCo coe_tc rep_tys
; case fl of
Wanted {} -> do { cv' <- newCoVar rhs_ty xi
- ; setCoBind cv $
- coe `mkTransCoercion` mkCoVarCoercion cv'
+ ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv'
; 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 $
- mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
+ mkSymCo (mkCoVarCo cv) `mkTransCo` coe
; can_cts <- mkCanonical fl cv'
; return $
SomeTopInt { tir_new_work = can_cts
MatchInstSingle (_,_)
| given_overlap untch ->
do { traceTcS "Delaying instance application" $
- vcat [ text "Workitem=" <+> pprPred (ClassP clas tys)
+ vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys)
, 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]
does_not_originate_in_a_silent clas sys
-- UGLY: See Note [Silent parameters overlapping]
- = null $ filter (tcEqPred (ClassP clas sys)) silents_and_their_scs
+ = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs
silents_and_their_scs
= foldlBag (\acc rvnt -> case rvnt of
projects / ghc-hetmet.git / blobdiff