Commit 107715b3 authored by dimitris's avatar dimitris

Reorganized functional dependency reactions once more:

 1) generating Derived FDs as happens for equality superclasses
 2) Kept the optimization of immediately discharging items
    if fundeps cause a match
 3) Restructured top-reactions and interactions with inerts to
    behave similarly to each other.

In particular, (1) fixes ticket #5236.
parent f31e9349
......@@ -2,7 +2,7 @@
module TcCanonical(
mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
canOccursCheck, canEqToWorkList,
rewriteWithFunDeps
rewriteWithFunDeps, mkCanonicalFDAsDerived, mkCanonicalFDAsWanted
) where
#include "HsVersions.h"
......@@ -23,7 +23,7 @@ import Name
import Var
import VarEnv ( TidyEnv )
import Outputable
import Control.Monad ( unless, when, zipWithM, zipWithM_ )
import Control.Monad ( unless, when, zipWithM, zipWithM_, foldM )
import MonadUtils
import Control.Applicative ( (<|>) )
......@@ -981,60 +981,44 @@ now!).
\begin{code}
rewriteWithFunDeps :: [Equation]
-> [Xi] -> CtFlavor
-> TcS (Maybe ([Xi], [Coercion], WorkList))
rewriteWithFunDeps eqn_pred_locs xis fl
= do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
; let fd_ev_pos :: [(Int,FlavoredEvVar)]
-> [Xi]
-> WantedLoc
-> TcS (Maybe ([Xi], [Coercion], [(EvVar,WantedLoc)]))
-- Not quite a WantedEvVar unfortunately
-- Because our intention could be to make
-- it derived at the end of the day
-- NB: The flavor of the returned EvVars will be decided by the caller
-- Post: returns no trivial equalities (identities)
rewriteWithFunDeps eqn_pred_locs xis wloc
= do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
; let fd_ev_pos :: [(Int,(EvVar,WantedLoc))]
fd_ev_pos = concat fd_ev_poss
(rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
; let fd_work = unionWorkLists fds
; if isEmptyWorkList fd_work
then return Nothing
else return (Just (rewritten_xis, cos, fd_work)) }
instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
-> Equation
-> TcS [(Int, FlavoredEvVar)]
; if null fd_ev_pos then return Nothing
else return (Just (rewritten_xis, cos, map snd fd_ev_pos)) }
instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
-- Post: Returns the position index as well as the corresponding FunDep equality
instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
, fd_pred1 = d1, fd_pred2 = d2 })
= do { let tvs = varSetElems qtvs
; tvs' <- mapM instFlexiTcS tvs
; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
; mapM (do_one subst) eqs }
; foldM (do_one subst) [] eqs }
where
fl' = case fl of
Given {} -> panic "mkFunDepEqns"
Wanted loc -> Wanted (push_ctx loc)
Derived loc -> Derived (push_ctx loc)
do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
= let sty1 = Type.substTy subst ty1
sty2 = Type.substTy subst ty2
in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
else do { ev <- newCoVar sty1 sty2
; let wl' = push_ctx wl
; return $ (i,(ev,wl')):ievs }
push_ctx :: WantedLoc -> WantedLoc
push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
= do { let sty1 = Type.substTy subst ty1
sty2 = Type.substTy subst ty2
; ev <- newCoVar sty1 sty2
; return (i, mkEvVarX ev fl') }
rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
-> [Type] -- A sequence of types: tys
-> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)]
rewriteDictParams param_eqs tys
= zipWith do_one tys [0..]
where
do_one :: Type -> Int -> (Type,Coercion)
do_one ty n = case lookup n param_eqs of
Just wev -> (get_fst_ty wev, mkCoVarCo (evVarOf wev))
Nothing -> (ty, mkReflCo ty) -- Identity
get_fst_ty wev = case evVarOfPred wev of
EqPred ty1 _ -> ty1
_ -> panic "rewriteDictParams: non equality fundep"
mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
-> TcM (TidyEnv, SDoc)
mkEqnMsg :: (TcPredType, SDoc)
-> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
= do { zpred1 <- TcM.zonkTcPredType pred1
; zpred2 <- TcM.zonkTcPredType pred2
......@@ -1044,4 +1028,36 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
; return (tidy_env, msg) }
rewriteDictParams :: [(Int,(EvVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty)
-> [Type] -- A sequence of types: tys
-> [(Type,Coercion)] -- Returns: [(ty', co : ty' ~ ty)]
rewriteDictParams param_eqs tys
= zipWith do_one tys [0..]
where
do_one :: Type -> Int -> (Type,Coercion)
do_one ty n = case lookup n param_eqs of
Just wev -> (get_fst_ty wev, mkCoVarCo (fst wev))
Nothing -> (ty, mkReflCo ty) -- Identity
get_fst_ty (wev,_wloc)
| EqPred ty1 _ <- evVarPred wev
= ty1
| otherwise
= panic "rewriteDictParams: non equality fundep!?"
mkCanonicalFDAsWanted :: [(EvVar,WantedLoc)] -> TcS WorkList
mkCanonicalFDAsWanted evlocs
= do { ws <- mapM can_as_wanted evlocs
; return (unionWorkLists ws) }
where can_as_wanted (ev,loc) = mkCanonicalFEV (EvVarX ev (Wanted loc))
mkCanonicalFDAsDerived :: [(EvVar,WantedLoc)] -> TcS WorkList
mkCanonicalFDAsDerived evlocs
= do { ws <- mapM can_as_derived evlocs
; return (unionWorkLists ws) }
where can_as_derived (ev,loc) = mkCanonicalFEV (EvVarX ev (Derived loc))
\end{code}
\ No newline at end of file
......@@ -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
......@@ -929,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 && eqTypes 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)
| eqTypes 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 = mkTyConAppCo (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.
......@@ -1284,25 +1291,26 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
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 )
......@@ -1310,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]
......@@ -1725,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 = mkTyConAppCo (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 })
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment