X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=b279c2fc0ae5952014794db754e638d8197cfdae;hp=46eece84e8903a1cc5952a00a5ccddedf6d45dbf;hb=HEAD;hpb=9591547fbbdf12728884e125f8ba08b0e6e69f82 diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 46eece8..b279c2f 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -163,7 +163,8 @@ instance Outputable InertSet where , 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 @@ -413,18 +414,12 @@ dischargeFromCCans cans ev fl 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} @@ -732,9 +727,10 @@ solveWithIdentity cv wd tv xi ] ; 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 @@ -934,71 +930,77 @@ doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult 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. @@ -1049,7 +1051,7 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i -- 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 @@ -1062,7 +1064,7 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i 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 } } @@ -1102,31 +1104,31 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 , 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 @@ -1157,13 +1159,13 @@ doInteractWithInert _ workItem = noInteraction workItem -- 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 @@ -1174,11 +1176,11 @@ rewriteDict (cv,tv,xi) (dv,gw,cl,xis) 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 @@ -1189,20 +1191,21 @@ rewriteIP (cv,tv,xi) (ipid,gw,nm,ty) 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 () @@ -1223,20 +1226,20 @@ 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) (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: @@ -1249,9 +1252,9 @@ rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2) = 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' } @@ -1259,9 +1262,9 @@ rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2) = 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' } @@ -1269,12 +1272,12 @@ rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList 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 () @@ -1285,28 +1288,29 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) 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 ) @@ -1314,10 +1318,16 @@ solveOneFromTheOther info (ev_term,ifl) workItem 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] @@ -1729,69 +1739,83 @@ doTopReact _inerts (CDictCan { cc_flavor = Given {} }) = 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 }) @@ -1812,11 +1836,10 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, 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 @@ -1827,7 +1850,7 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, cc_flavor = fl , 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 @@ -2062,7 +2085,7 @@ matchClassInst inerts clas tys loc 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] @@ -2110,7 +2133,7 @@ matchClassInst inerts clas tys loc 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