From 50d0293555691012f96259de7f8682b94db58517 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Thu, 17 Feb 2011 14:09:21 +0000 Subject: [PATCH] Use "on the spot" solving for fundeps When we spot an equality arising from a functional dependency, we now use that equality (a "wanted") to rewrite the work-item constraint right away. This avoids two dangers Danger 1: If we send the original constraint on down the pipeline it may react with an instance declaration, and in delicate situations (when a Given overlaps with an instance) that may produce new insoluble goals: see Trac #4952 Danger 2: If we don't rewrite the constraint, it may re-react with the same thing later, and produce the same equality again --> termination worries. To achieve this required some refactoring of FunDeps.lhs (nicer now!). This patch also contains a couple of unrelated improvements * A bad bug in TcSMonad.nestImplicTcS whereby the Tcs tyvars of an outer implication were not untouchable inside * Improved logging machinery for the type constraint solver; use -ddump-cs-trace (probably with a wider default line width -dppr-cols=200 or something) --- compiler/main/DynFlags.hs | 2 + compiler/typecheck/TcCanonical.lhs | 79 ++++++++- compiler/typecheck/TcInteract.lhs | 345 +++++++++++++++++++++--------------- compiler/typecheck/TcRnTypes.lhs | 7 +- compiler/typecheck/TcSMonad.lhs | 114 +++++------- compiler/types/FunDeps.lhs | 299 ++++++++++++++++++------------- 6 files changed, 509 insertions(+), 337 deletions(-) diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 9147a92..7bd4d84 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -153,6 +153,7 @@ data DynFlag | Opt_D_dump_rn_stats | Opt_D_dump_opt_cmm | Opt_D_dump_simpl_stats + | Opt_D_dump_cs_trace -- Constraint solver in type checker | Opt_D_dump_tc_trace | Opt_D_dump_if_trace | Opt_D_dump_splices @@ -1259,6 +1260,7 @@ dynamic_flags = [ , Flag "ddump-worker-wrapper" (setDumpFlag Opt_D_dump_worker_wrapper) , Flag "ddump-rn-trace" (setDumpFlag Opt_D_dump_rn_trace) , Flag "ddump-if-trace" (setDumpFlag Opt_D_dump_if_trace) + , Flag "ddump-cs-trace" (setDumpFlag Opt_D_dump_cs_trace) , Flag "ddump-tc-trace" (setDumpFlag Opt_D_dump_tc_trace) , Flag "ddump-splices" (setDumpFlag Opt_D_dump_splices) , Flag "ddump-rn-stats" (setDumpFlag Opt_D_dump_rn_stats) diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 861b262..8668d90 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -1,7 +1,8 @@ \begin{code} module TcCanonical( mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens, - canOccursCheck, canEq + canOccursCheck, canEq, + rewriteWithFunDeps ) where #include "HsVersions.h" @@ -9,7 +10,8 @@ module TcCanonical( import BasicTypes import Type import TcRnTypes - +import FunDeps +import qualified TcMType as TcM import TcType import TcErrors import Coercion @@ -18,6 +20,7 @@ import TyCon import TypeRep import Name import Var +import VarEnv ( TidyEnv ) import Outputable import Control.Monad ( unless, when, zipWithM, zipWithM_ ) import MonadUtils @@ -28,6 +31,7 @@ import Bag import HsBinds import TcSMonad +import FastString \end{code} Note [Canonicalisation] @@ -991,4 +995,75 @@ a. If this turns out to be impossible, we next try expanding F itself, and so on. +%************************************************************************ +%* * +%* Functional dependencies, instantiation of equations +%* * +%************************************************************************ +\begin{code} +rewriteWithFunDeps :: [Equation] + -> [Xi] -> CtFlavor + -> TcS (Maybe ([Xi], [Coercion], CanonicalCts)) +rewriteWithFunDeps eqn_pred_locs xis fl + = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs + ; let fd_ev_pos :: [(Int,FlavoredEvVar)] + 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 = unionManyBags fds + ; if isEmptyBag fd_work + then return Nothing + else return (Just (rewritten_xis, cos, fd_work)) } + +instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived + -> Equation + -> TcS [(Int, FlavoredEvVar)] +-- Post: Returns the position index as well as the corresponding FunDep equality +instFunDepEqn fl (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 } + where + fl' = case fl of + Given _ -> panic "mkFunDepEqns" + Wanted loc -> Wanted (push_ctx loc) + Derived loc -> Derived (push_ctx loc) + + 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 = substTy subst ty1 + sty2 = 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, mkCoVarCoercion (evVarOf wev)) + Nothing -> (ty,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 (pred1,from1) (pred2,from2) tidy_env + = do { zpred1 <- TcM.zonkTcPredType pred1 + ; zpred2 <- TcM.zonkTcPredType pred2 + ; let { tpred1 = tidyPred tidy_env zpred1 + ; tpred2 = tidyPred tidy_env zpred2 } + ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"), + nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), + nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])] + ; return (tidy_env, msg) } +\end{code} \ No newline at end of file diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index f9d3d97..3f166cf 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -20,7 +20,6 @@ import TcType import HsBinds import Inst( tyVarsOfEvVar ) -import InstEnv import Class import TyCon import Name @@ -270,21 +269,24 @@ instance Outputable StageResult where , ptext (sLit "new work =") <+> ppr work <> comma , ptext (sLit "stop =") <+> ppr stop]) -type SimplifierStage = WorkItem -> InertSet -> TcS StageResult +type SubGoalDepth = Int -- Starts at zero; used to limit infinite + -- recursion of sub-goals +type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult -- Combine a sequence of simplifier 'stages' to create a pipeline -runSolverPipeline :: [(String, SimplifierStage)] - -> InertSet -> WorkItem +runSolverPipeline :: SubGoalDepth + -> [(String, SimplifierStage)] + -> InertSet -> WorkItem -> TcS (InertSet, WorkList) -- Precondition: non-empty list of stages -runSolverPipeline pipeline inerts workItem +runSolverPipeline depth pipeline inerts workItem = do { traceTcS "Start solver pipeline" $ vcat [ ptext (sLit "work item =") <+> ppr workItem , ptext (sLit "inerts =") <+> ppr inerts] ; let itr_in = SR { sr_inerts = inerts - , sr_new_work = emptyWorkList - , sr_stop = ContinueWith workItem } + , sr_new_work = emptyWorkList + , sr_stop = ContinueWith workItem } ; itr_out <- run_pipeline pipeline itr_in ; let new_inert = case sr_stop itr_out of @@ -301,7 +303,7 @@ runSolverPipeline pipeline inerts workItem (SR { sr_new_work = accum_work , sr_inerts = inerts , sr_stop = ContinueWith work_item }) - = do { itr <- stage work_item inerts + = do { itr <- stage depth work_item inerts ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr) ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr } ; run_pipeline stages itr' } @@ -468,21 +470,18 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws -- new inert set which has assimilated the new information. solveOneWithDepth :: (Int, Int, [WorkItem]) -> InertSet -> WorkItem -> TcS InertSet -solveOneWithDepth (max_depth, n, stack) inert work - = do { traceTcS0 (indent ++ "Solving {") (ppr work) - ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work +solveOneWithDepth (max_depth, depth, stack) inert work + = do { traceFireTcS depth (text "Solving {" <+> ppr work) + ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work - ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work) - -- Recursively solve the new work generated -- from workItem, with a greater depth - ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack) + ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_inert new_work - ; traceTcS0 (indent ++ "Done }") (ppr work) + ; traceFireTcS depth (text "Done }" <+> ppr work) + ; return res_inert } - where - indent = replicate (2*n) ' ' thePipeline :: [(String,SimplifierStage)] thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage) @@ -524,7 +523,7 @@ Case 3: IP improvement work \begin{code} spontaneousSolveStage :: SimplifierStage -spontaneousSolveStage workItem inerts +spontaneousSolveStage depth workItem inerts = do { mSolve <- trySpontaneousSolve workItem ; case mSolve of @@ -540,7 +539,9 @@ spontaneousSolveStage workItem inerts -- its status change. This in turn may produce more work. -- We do this *right now* (rather than just putting workItem' -- back into the work-list) because we've solved - -> do { (new_inert, new_work) <- runSolverPipeline + -> do { bumpStepCountTcS + ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem) + ; (new_inert, new_work) <- runSolverPipeline depth [ ("recursive interact with inert eqs", interactWithInertEqsStage) , ("recursive interact with inerts", interactWithInertsStage) ] inerts workItem' @@ -551,9 +552,11 @@ spontaneousSolveStage workItem inerts | otherwise -> -- Original was given; he must then be inert all right, and -- workList' are all givens from flattening - return $ SR { sr_new_work = emptyWorkList - , sr_inerts = inerts `updInertSet` workItem' - , sr_stop = Stop } + do { bumpStepCountTcS + ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem) + ; return $ SR { sr_new_work = emptyWorkList + , sr_inerts = inerts `updInertSet` workItem' + , sr_stop = Stop } } SPError -> -- Return with no new work return $ SR { sr_new_work = emptyWorkList , sr_inerts = inerts @@ -584,7 +587,8 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = | otherwise = do { tch1 <- isTouchableMetaTyVar tv1 ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi - else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem) + else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" + (ppr workItem) ; return SPCantSolve } } @@ -758,24 +762,27 @@ data InteractResult , ir_new_work :: WorkList -- new work items to add to the WorkList + + , ir_fire :: Maybe String -- Tells whether a rule fired, and if so what } -- What to do with the inert reactant. -data InertAction = KeepInert - | DropInert - | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert - -mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult -mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork +data InertAction = KeepInert | DropInert -mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult -mkIRStop keep newWork = return $ IR Stop keep newWork +mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult +mkIRContinue rule wi keep newWork + = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep + , ir_new_work = newWork, ir_fire = Just rule } -dischargeWorkItem :: Monad m => m InteractResult -dischargeWorkItem = mkIRStop KeepInert emptyWorkList +mkIRStop :: String -> WorkList -> TcS InteractResult +mkIRStop rule newWork + = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert + , ir_new_work = newWork, ir_fire = Just rule } noInteraction :: Monad m => WorkItem -> m InteractResult -noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList +noInteraction wi + = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert + , ir_new_work = emptyWorkList, ir_fire = Nothing } data WhichComesFromInert = LeftComesFromInert | RightComesFromInert -- See Note [Efficient Orientation] @@ -788,8 +795,8 @@ data WhichComesFromInert = LeftComesFromInert | RightComesFromInert -- interact the WorkItem with the entire equalities of the InertSet interactWithInertEqsStage :: SimplifierStage -interactWithInertEqsStage workItem inert - = Bag.foldlBagM interactNext initITR (inert_eqs inert) +interactWithInertEqsStage depth workItem inert + = Bag.foldlBagM (interactNext depth) initITR (inert_eqs inert) where initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan } , sr_new_work = emptyWorkList @@ -802,12 +809,12 @@ interactWithInertEqsStage workItem inert -- "Other" constraints it contains! interactWithInertsStage :: SimplifierStage -interactWithInertsStage workItem inert +interactWithInertsStage depth workItem inert = let (relevant, inert_residual) = getISRelevant workItem inert initITR = SR { sr_inerts = inert_residual , sr_new_work = emptyWorkList , sr_stop = ContinueWith workItem } - in Bag.foldlBagM interactNext initITR relevant + in Bag.foldlBagM (interactNext depth) initITR relevant where getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) getISRelevant (CFrozenErr {}) is = (emptyCCan, is) @@ -834,23 +841,37 @@ interactWithInertsStage workItem inert , inert_ips = emptyCCanMap , inert_funeqs = emptyCCanMap }) -interactNext :: StageResult -> AtomicInert -> TcS StageResult -interactNext it inert - | ContinueWith workItem <- sr_stop it - = do { let inerts = sr_inerts it - - ; ir <- interactWithInert inert workItem - - -- New inerts depend on whether we KeepInert or not and must - -- be updated with FD improvement information from the interaction result (ir) - ; let inerts_new = case ir_inert_action ir of - KeepInert -> inerts `updInertSet` inert - DropInert -> inerts - KeepTransformedInert inert' -> inerts `updInertSet` inert' +interactNext :: SubGoalDepth -> StageResult -> AtomicInert -> TcS StageResult +interactNext depth it inert + | ContinueWith work_item <- sr_stop it + = do { let inerts = sr_inerts it + + ; IR { ir_new_work = new_work, ir_inert_action = inert_action + , ir_fire = fire_info, ir_stop = stop } + <- interactWithInert inert work_item + + ; let mk_msg rule + = text rule <+> keep_doc + <+> vcat [ ptext (sLit "Inert =") <+> ppr inert + , ptext (sLit "Work =") <+> ppr work_item + , ppUnless (isEmptyBag new_work) $ + ptext (sLit "New =") <+> ppr new_work ] + keep_doc = case inert_action of + KeepInert -> ptext (sLit "[keep]") + DropInert -> ptext (sLit "[drop]") + ; case fire_info of + Just rule -> do { bumpStepCountTcS + ; traceFireTcS depth (mk_msg rule) } + Nothing -> return () + + -- New inerts depend on whether we KeepInert or not + ; let inerts_new = case inert_action of + KeepInert -> inerts `updInertSet` inert + DropInert -> inerts ; return $ SR { sr_inerts = inerts_new - , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir - , sr_stop = ir_stop ir } } + , sr_new_work = sr_new_work it `unionWorkLists` new_work + , sr_stop = stop } } | otherwise = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert } @@ -878,7 +899,7 @@ doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult doInteractWithInert (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) - workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) + workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2) = solveOneFromTheOther (d1,fl1) workItem @@ -886,18 +907,46 @@ doInteractWithInert = -- See Note [When improvement happens] do { let pty1 = ClassP cls1 tys1 pty2 = ClassP cls2 tys2 - work_item_pred_loc = (pty2, pprFlavorArising fl2) inert_pred_loc = (pty1, pprFlavorArising fl1) - loc = combineCtLoc fl1 fl2 - eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc - -- See Note [Efficient Orientation] - - ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs - ; fd_work <- mapM mkCanonicalFEV derived_evs - -- See Note [Generating extra equalities] - - ; mkIRContinue workItem KeepInert (unionManyBags fd_work) - } + 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 + do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2 + ; when (isWanted fl2) $ setDictBind d2 (EvCast d1 dict_co) + ; mkIRStop "Cls/Cls fundep (solved)" fd_work } + + | isWanted fl2 + -> -- We could not quite solve him, but we stil 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. + -- In fact, it is inert wrt all the previous inerts too, so + -- we can keep on going rather than sending it back to the work list + do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2 + ; d2' <- newDictVar cls1 rewritten_tys2 + ; setDictBind d2 (EvCast d2' dict_co) + ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 } + ; mkIRContinue "Cls/Cls fundep (partial)" workItem' KeepInert fd_work } + + | otherwise + -> ASSERT (isDerived fl2) -- Derived constraints have no evidence, + -- so just produce the rewritten constraint + let workItem' = workItem { cc_tyargs = rewritten_tys2 } + in mkIRContinue "Cls/Cls fundep" workItem' KeepInert fd_work + } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. @@ -908,14 +957,14 @@ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_r = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis) -- Continue with rewritten Dictionary because we can only be in the -- interactWithEqsStage, so the dictionary is inert. - ; mkIRContinue rewritten_dict KeepInert emptyWorkList } + ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList } doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi }) | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfTypes xis = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis) - ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) } + ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromCCan rewritten_dict) } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. @@ -924,14 +973,14 @@ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_r | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfType ty = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty) - ; mkIRContinue rewritten_ip KeepInert emptyWorkList } + ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList } doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi }) | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfType ty = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty) - ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) } + ; mkIRContinue "IP/Eq" workItem DropInert (workListFromCCan rewritten_ip) } -- Two implicit parameter constraints. If the names are the same, -- but their types are not, we generate a wanted type equality @@ -944,7 +993,9 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i = -- See Note [Overriding implicit parameters] -- Dump the inert item, override totally with the new one -- Do not require type equality - mkIRContinue workItem DropInert emptyWorkList + -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ... + -- we must *override* the outer one with the inner one + mkIRContinue "IP/IP override" workItem DropInert emptyWorkList | nm1 == nm2 && ty1 `tcEqType` ty2 = solveOneFromTheOther (id1,ifl) workItem @@ -954,9 +1005,7 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation] ; let flav = Wanted (combineCtLoc ifl wfl) ; cans <- mkCanonical flav co_var - ; mkIRContinue workItem KeepInert cans } - - + ; mkIRContinue "IP/IP fundep" workItem KeepInert cans } -- Never rewrite a given with a wanted equality, and a type function -- equality can never rewrite an equality. We rewrite LHS *and* RHS @@ -970,7 +1019,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_ | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) - ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) } + ; mkIRStop "Eq/FunEq" (workListFromCCan rewritten_funeq) } -- Must Stop here, because we may no longer be inert after the rewritting. -- Inert: function equality, work item: equality @@ -980,7 +1029,7 @@ doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) - ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) } + ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromCCan rewritten_funeq) } -- One may think that we could (KeepTransformedInert rewritten_funeq) -- but that is wrong, because it may end up not being inert with respect -- to future inerts. Example: @@ -996,10 +1045,10 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 , cc_tyargs = args2, cc_rhs = xi2 }) | fl1 `canSolve` fl2 && lhss_match = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert cans } + ; mkIRStop "FunEq/FunEq" cans } | fl2 `canSolve` fl1 && lhss_match = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert cans } + ; mkIRContinue "FunEq/FunEq" workItem DropInert cans } where lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) @@ -1008,30 +1057,32 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert cans } + ; mkIRStop "Eq/Eq lhs" cans } | fl2 `canSolve` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert cans } + ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans } + -- Check for rewriting RHS | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2) - ; mkIRStop KeepInert rewritten_eq } + ; mkIRStop "Eq/Eq rhs" rewritten_eq } + | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) - ; mkIRContinue workItem DropInert rewritten_eq } + ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq } doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) (CFrozenErr { cc_id = cv2, cc_flavor = fl2 }) | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) - ; mkIRStop KeepInert rewritten_frozen } + ; mkIRStop "Frozen/Eq" rewritten_frozen } doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 }) workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) - ; mkIRContinue workItem DropInert rewritten_frozen } + ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen } -- Fall-through case for all other situations doInteractWithInert _ workItem = noInteraction workItem @@ -1188,26 +1239,28 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1] solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult --- First argument inert, second argument workitem. They both represent +-- First argument inert, second argument work-item. They both represent -- wanted/given/derived evidence for the *same* predicate so we try here to -- discharge one directly from the other. -- -- Precondition: value evidence only (implicit parameters, classes) -- not coercion solveOneFromTheOther (iid,ifl) workItem + | isDerived wfl + = mkIRStop "Solved (derived)" emptyWorkList + | ifl `canSolve` wfl = do { when (isWanted wfl) $ setEvBind wid (EvId iid) -- Overwrite the binding, if one exists -- For Givens, which are lambda-bound, nothing to overwrite, - ; dischargeWorkItem } + ; mkIRStop "Solved" emptyWorkList } + | wfl `canSolve` ifl = do { when (isWanted ifl) $ setEvBind iid (EvId wid) - ; mkIRContinue workItem DropInert emptyWorkList } + ; mkIRContinue "Solved inert" workItem DropInert emptyWorkList } - | otherwise -- One of the two is Derived, we can just throw it away, - -- preferrably the work item. - = if isDerived wfl then dischargeWorkItem - else mkIRContinue workItem DropInert emptyWorkList + | otherwise -- The inert item is Derived, we can just throw it away, + = mkIRContinue "Discard derived inert" workItem DropInert emptyWorkList where wfl = cc_flavor workItem @@ -1577,7 +1630,7 @@ data TopInteractResult -- arising from top-level instances. topReactionsStage :: SimplifierStage -topReactionsStage workItem inerts +topReactionsStage depth workItem inerts = do { tir <- tryTopReact workItem ; case tir of NoTopInt -> @@ -1585,10 +1638,14 @@ topReactionsStage workItem inerts , sr_new_work = emptyWorkList , sr_stop = ContinueWith workItem } SomeTopInt tir_new_work tir_new_inert -> - return $ SR { sr_inerts = inerts - , sr_new_work = tir_new_work - , sr_stop = tir_new_inert - } + do { bumpStepCountTcS + ; traceFireTcS depth (ptext (sLit "Top react") + <+> vcat [ ptext (sLit "Work =") <+> ppr workItem + , ptext (sLit "New =") <+> ppr tir_new_work ]) + ; return $ SR { sr_inerts = inerts + , sr_new_work = tir_new_work + , sr_stop = tir_new_inert + } } } tryTopReact :: WorkItem -> TcS TopInteractResult @@ -1618,47 +1675,69 @@ doTopReact (CDictCan { cc_flavor = Given {} }) = return NoTopInt -- NB: Superclasses already added since it's canonical -- Derived dictionary: just look for functional dependencies -doTopReact workItem@(CDictCan { cc_flavor = Derived loc +doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc) , cc_class = cls, cc_tyargs = xis }) - = do { fd_work <- findClassFunDeps cls xis loc - ; if isEmptyWorkList fd_work then - return NoTopInt - else return $ SomeTopInt { tir_new_work = fd_work - , tir_new_inert = ContinueWith workItem } } + = do { 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',_,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' } } + -- Wanted dictionary -doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc - , cc_class = cls, cc_tyargs = xis }) +doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc) + , cc_class = cls, cc_tyargs = xis }) = do { -- See Note [MATCHING-SYNONYMS] ; lkp_inst_res <- matchClassInst cls xis loc - ; case lkp_inst_res of - NoInstance -> - do { traceTcS "doTopReact/ no class instance for" (ppr dv) - ; fd_work <- findClassFunDeps cls xis loc - ; return $ SomeTopInt - { tir_new_work = fd_work - , tir_new_inert = ContinueWith workItem } } - - GenInst wtvs ev_term -> -- Solved + ; 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 = singleCCan workItem' `andCCan` 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 - do { traceTcS "doTopReact/ found class instance for" (ppr dv) - ; setDictBind dv ev_term - ; inst_work <- canWanteds wtvs - ; if null wtvs + | 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 - then return $ SomeTopInt { tir_new_work = emptyWorkList - , tir_new_inert = Stop } - - -- Solved and new wanted work produced, you may cache the - -- (tentatively solved) dictionary as Given! (used to be: Derived) - else do { let solved = makeSolvedByInst workItem - ; return $ SomeTopInt - { tir_new_work = inst_work - , tir_new_inert = ContinueWith solved } } - } } + ; return $ SomeTopInt { tir_new_work = emptyWorkList + , tir_new_inert = Stop } } + + | otherwise + -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) + ; setDictBind dv ev_term + -- Solved and new wanted work produced, you may cache the + -- (tentatively solved) dictionary as Given! (used to be: Derived) + ; let solved = workItem { cc_flavor = given_fl } + given_fl = Given (setCtLocOrigin loc UnkSkol) + ; inst_work <- canWanteds wtvs + ; return $ SomeTopInt { tir_new_work = inst_work + , tir_new_inert = ContinueWith solved } } + } -- Type functions doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl @@ -1694,20 +1773,6 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl -- Any other work item does not react with any top-level equations doTopReact _workItem = return NoTopInt - ----------------------- -findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList --- Look for a fundep reaction beween the wanted item --- and a top-level instance declaration -findClassFunDeps cls xis loc - = do { instEnvs <- getInstEnvs - ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs) - (ClassP cls xis, pprArisingAt loc) - ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs - -- NB: fundeps generate some wanted equalities, but - -- we don't use their evidence for anything - ; cts <- mapM mkCanonicalFEV derived_evs - ; return $ unionManyBags cts } \end{code} diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 96ca3b3..f9422a8 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -935,10 +935,9 @@ data CtFlavor -- superclasses. instance Outputable CtFlavor where - ppr (Given _) = ptext (sLit "[Given]") - ppr (Wanted _) = ptext (sLit "[Wanted]") - ppr (Derived {}) = ptext (sLit "[Derived]") - + ppr (Given {}) = ptext (sLit "[G]") + ppr (Wanted {}) = ptext (sLit "[W]") + ppr (Derived {}) = ptext (sLit "[D]") pprFlavorArising :: CtFlavor -> SDoc pprFlavorArising (Derived wl ) = pprArisingAt wl pprFlavorArising (Wanted wl) = pprArisingAt wl diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 8d5093d..ad24eb7 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -10,7 +10,6 @@ module TcSMonad ( CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, deCanonicalise, mkFrozenError, - makeSolvedByInst, isWanted, isGiven, isDerived, isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising, @@ -21,7 +20,8 @@ module TcSMonad ( combineCtLoc, mkGivenFlavor, mkWantedFlavor, getWantedLoc, - TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality + TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality + traceFireTcS, bumpStepCountTcS, tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS, SimplContext(..), isInteractive, simplEqsOnly, performDefaulting, @@ -45,7 +45,7 @@ module TcSMonad ( instDFunTypes, -- Instantiation instDFunConstraints, - newFlexiTcSTy, + newFlexiTcSTy, instFlexiTcS, compatKind, @@ -58,15 +58,11 @@ module TcSMonad ( matchClass, matchFam, MatchInstResult (..), checkWellStagedDFun, warnTcS, - pprEq, -- Smaller utils, re-exported from TcM + pprEq -- Smaller utils, re-exported from TcM -- TODO (DV): these are only really used in the -- instance matcher in TcSimplify. I am wondering -- if the whole instance matcher simply belongs -- here - - - mkDerivedFunDepEqns -- Instantiation of 'Equations' from FunDeps - ) where #include "HsVersions.h" @@ -102,7 +98,6 @@ import FastString import HsBinds -- for TcEvBinds stuff import Id -import FunDeps import TcRnTypes @@ -180,16 +175,6 @@ mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl } compatKind :: Kind -> Kind -> Bool compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 -makeSolvedByInst :: CanonicalCt -> CanonicalCt --- Record that a constraint is now solved --- Wanted -> Given --- Given, Derived -> no-op -makeSolvedByInst ct - | Wanted loc <- cc_flavor ct - = ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) } - | otherwise -- Only called on wanteds - = pprPanic "makeSolvedByInst" (ppr ct) - deCanonicalise :: CanonicalCt -> FlavoredEvVar deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct) @@ -367,7 +352,10 @@ data TcSEnv tcs_context :: SimplContext, - tcs_untch :: TcsUntouchables + tcs_untch :: TcsUntouchables, + + tcs_ic_depth :: Int, -- Implication nesting depth + tcs_count :: IORef Int -- Global step count } type TcsUntouchables = (Untouchables,TcTyVarSet) @@ -443,8 +431,21 @@ panicTcS doc = pprPanic "TcCanonical" doc traceTcS :: String -> SDoc -> TcS () traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc -traceTcS0 :: String -> SDoc -> TcS () -traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc +bumpStepCountTcS :: TcS () +bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env + ; n <- TcM.readTcRef ref + ; TcM.writeTcRef ref (n+1) } + +traceFireTcS :: Int -> SDoc -> TcS () +-- Dump a rule-firing trace +traceFireTcS depth doc + = TcS $ \env -> + TcM.ifDOptM Opt_D_dump_cs_trace $ + do { n <- TcM.readTcRef (tcs_count env) + ; let msg = int n + <> text (replicate (tcs_ic_depth env) '>') + <> brackets (int depth) <+> doc + ; TcM.dumpTcRn msg } runTcS :: SimplContext -> Untouchables -- Untouchables @@ -453,10 +454,13 @@ runTcS :: SimplContext runTcS context untouch tcs = do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds + ; step_count <- TcM.newTcRef 0 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var , tcs_context = context , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet + , tcs_count = step_count + , tcs_ic_depth = 0 } -- Run the computation @@ -465,6 +469,10 @@ runTcS context untouch tcs ; ty_binds <- TcM.readTcRef ty_binds_var ; mapM_ do_unification (varEnvElts ty_binds) +#ifdef DEBUG + ; count <- TcM.readTcRef step_count + ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count) +#endif -- And return ; ev_binds <- TcM.readTcRef evb_ref ; return (res, evBindMapBinds ev_binds) } @@ -472,13 +480,23 @@ runTcS context untouch tcs do_unification (tv,ty) = TcM.writeMetaTyVar tv ty nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a -nestImplicTcS ref untch (TcS thing_inside) - = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, - tcs_context = ctxt } -> +nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside) + = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds + , tcs_untch = (_outer_range, outer_tcs) + , tcs_count = count + , tcs_ic_depth = idepth + , tcs_context = ctxt } -> let + inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs) + -- The inner_range should be narrower than the outer one + -- (thus increasing the set of untouchables) but + -- the inner Tcs-untouchables must be unioned with the + -- outer ones! nest_env = TcSEnv { tcs_ev_binds = ref , tcs_ty_binds = ty_binds - , tcs_untch = untch + , tcs_untch = inner_untch + , tcs_count = count + , tcs_ic_depth = idepth+1 , tcs_context = ctxtUnderImplic ctxt } in thing_inside nest_env @@ -785,48 +803,4 @@ matchFam tycon args -- DV: We never return MatchInstMany, since tcLookupFamInst never returns -- multiple matches. Check. } - - --- Functional dependencies, instantiation of equations -------------------------------------------------------- - -mkDerivedFunDepEqns :: WantedLoc - -> [(Equation, (PredType, SDoc), (PredType, SDoc))] - -> TcS [FlavoredEvVar] -- All Derived -mkDerivedFunDepEqns _ [] = return [] -mkDerivedFunDepEqns loc eqns - = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns)) - ; evvars <- mapM to_work_item eqns - ; return $ concat evvars } - where - to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar] - to_work_item ((qtvs, pairs), d1, d2) - = do { let tvs = varSetElems qtvs - ; tvs' <- mapM instFlexiTcS tvs - ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs') - loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc - flav = Derived loc' - ; mapM (do_one subst flav) pairs } - - do_one subst flav (ty1, ty2) - = do { let sty1 = substTy subst ty1 - sty2 = substTy subst ty2 - ; ev <- newCoVar sty1 sty2 - ; return (mkEvVarX ev flav) } - -pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc -pprEquationDoc (eqn, (p1, _), (p2, _)) - = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] - -mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv - -> TcM (TidyEnv, SDoc) -mkEqnMsg (pred1,from1) (pred2,from2) tidy_env - = do { pred1' <- TcM.zonkTcPredType pred1 - ; pred2' <- TcM.zonkTcPredType pred2 - ; let { pred1'' = tidyPred tidy_env pred1' - ; pred2'' = tidyPred tidy_env pred2' } - ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"), - nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), - nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])] - ; return (tidy_env, msg) } \end{code} diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs index 511472c..6ce932b 100644 --- a/compiler/types/FunDeps.lhs +++ b/compiler/types/FunDeps.lhs @@ -9,7 +9,8 @@ It's better to read it as: "if we know these, then we're going to know these" \begin{code} module FunDeps ( - Equation, pprEquation, + FDEq (..), + Equation(..), pprEquation, oclose, improveFromInstEnv, improveFromAnother, checkInstCoverage, checkFunDeps, pprFundeps @@ -140,32 +141,67 @@ oclose preds fixed_tvs %************************************************************************ +Each functional dependency with one variable in the RHS is responsible +for generating a single equality. For instance: + class C a b | a -> b +The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha + FDEq { fd_pos = 1 + , fd_ty_left = Bool + , fd_ty_right = alpha } +However notice that a functional dependency may have more than one variable +in the RHS which will create more than one FDEq. Example: + class C a b c | a -> b c + [Wanted] C Int alpha alpha + [Wanted] C Int Bool beta +Will generate: + fd1 = FDEq { fd_pos = 1, fd_ty_left = alpha, fd_ty_right = Bool } and + fd2 = FDEq { fd_pos = 2, fd_ty_left = alpha, fd_ty_right = beta } + +We record the paremeter position so that can immediately rewrite a constraint +using the produced FDEqs and remove it from our worklist. + + +INVARIANT: Corresponding types aren't already equal +That is, there exists at least one non-identity equality in FDEqs. + +Assume: + class C a b c | a -> b c + instance C Int x x +And: [Wanted] C Int Bool alpha +We will /match/ the LHS of fundep equations, producing a matching substitution +and create equations for the RHS sides. In our last example we'd have generated: + ({x}, [fd1,fd2]) +where + fd1 = FDEq 1 Bool x + fd2 = FDEq 2 alpha x +To ``execute'' the equation, make fresh type variable for each tyvar in the set, +instantiate the two types with these fresh variables, and then unify or generate +a new constraint. In the above example we would generate a new unification +variable 'beta' for x and produce the following constraints: + [Wanted] (Bool ~ beta) + [Wanted] (alpha ~ beta) + +Notice the subtle difference between the above class declaration and: + class C a b c | a -> b, a -> c +where we would generate: + ({x},[fd1]),({x},[fd2]) +This means that the template variable would be instantiated to different +unification variables when producing the FD constraints. + +Finally, the position parameters will help us rewrite the wanted constraint ``on the spot'' + \begin{code} -type Equation = (TyVarSet, [(Type, Type)]) --- These pairs of types should be equal, for some --- substitution of the tyvars in the tyvar set --- INVARIANT: corresponding types aren't already equal - --- It's important that we have a *list* of pairs of types. Consider --- class C a b c | a -> b c where ... --- instance C Int x x where ... --- Then, given the constraint (C Int Bool v) we should improve v to Bool, --- via the equation ({x}, [(Bool,x), (v,x)]) --- This would not happen if the class had looked like --- class C a b c | a -> b, a -> c - --- To "execute" the equation, make fresh type variable for each tyvar in the set, --- instantiate the two types with these fresh variables, and then unify. --- --- For example, ({a,b}, (a,Int,b), (Int,z,Bool)) --- We unify z with Int, but since a and b are quantified we do nothing to them --- We usually act on an equation by instantiating the quantified type varaibles --- to fresh type variables, and then calling the standard unifier. +type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from -pprEquation :: Equation -> SDoc -pprEquation (qtvs, pairs) - = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)), - nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (t1,t2) <- pairs])] +data Equation + = FDEqn { fd_qtvs :: TyVarSet -- Instantiate these to fresh unification vars + , fd_eqs :: [FDEq] -- and then make these equal + , fd_pred1, fd_pred2 :: Pred_Loc } -- The Equation arose from + -- combining these two constraints + +data FDEq = FDEq { fd_pos :: Int -- We use '0' for the first position + , fd_ty_left :: Type + , fd_ty_right :: Type } \end{code} Given a bunch of predicates that must hold, such as @@ -198,93 +234,97 @@ NOTA BENE: \begin{code} -type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from +instFD_WithPos :: FunDep TyVar -> [TyVar] -> [Type] -> ([Type], [(Int,Type)]) +-- Returns a FunDep between the types accompanied along with their +-- position (<=0) in the types argument list. +instFD_WithPos (ls,rs) tvs tys + = (map (snd . lookup) ls, map lookup rs) + where + ind_tys = zip [0..] tys + env = zipVarEnv tvs ind_tys + lookup tv = lookupVarEnv_NF env tv -improveFromInstEnv :: (Class -> [Instance]) - -> Pred_Loc - -> [(Equation,Pred_Loc,Pred_Loc)] --- Improvement from top-level instances -improveFromInstEnv _inst_env pred - = improveOne _inst_env pred [] -- TODO: Refactor to directly use instance_eqnd? +zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true + -> [Type] + -> [(Int,Type)] + -> [FDEq] +-- Create a list of FDEqs from two lists of types, making sure +-- that the types are not equal. +zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2) + | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2 + | otherwise = FDEq { fd_pos = i2 + , fd_ty_left = ty1 + , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2 +zipAndComputeFDEqs _ _ _ = [] + +-- Improve a class constraint from another class constraint +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +improveFromAnother :: Pred_Loc -- Template item (usually given, or inert) + -> Pred_Loc -- Workitem [that can be improved] + -> [Equation] +-- Post: FDEqs always oriented from the other to the workitem +-- Equations have empty quantified variables +improveFromAnother pred1@(ClassP cls1 tys1, _) pred2@(ClassP cls2 tys2, _) + | tys1 `lengthAtLeast` 2 && cls1 == cls2 + = [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 } + | let (cls_tvs, cls_fds) = classTvsFds cls1 + , fd <- cls_fds + , let (ltys1, rs1) = instFD fd cls_tvs tys1 + (ltys2, irs2) = instFD_WithPos fd cls_tvs tys2 + , tcEqTypes ltys1 ltys2 -- The LHSs match + , let eqs = zipAndComputeFDEqs tcEqType rs1 irs2 + , not (null eqs) ] + +improveFromAnother _ _ = [] + + +-- Improve a class constraint from instance declarations +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +pprEquation :: Equation -> SDoc +pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs }) + = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)), + nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])] -improveFromAnother :: Pred_Loc +improveFromInstEnv :: (InstEnv,InstEnv) -> Pred_Loc - -> [(Equation, Pred_Loc, Pred_Loc)] --- Improvement from another local (given or wanted) constraint -improveFromAnother pred1 pred2 - = improveOne (\_ -> []) pred1 [pred2] -- TODO: Refactor to directly use pairwise_eqns? - - -improveOne :: (Class -> [Instance]) -- Gives instances for given class - -> Pred_Loc -- Do improvement triggered by this - -> [Pred_Loc] -- Current constraints - -> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold - -- (NB the above INVARIANT for type Equation) - -- The Pred_Locs explain which two predicates were - -- combined (for error messages) --- Just do improvement triggered by a single, distinguised predicate - -improveOne _inst_env pred@(IParam ip ty, _) preds - = [ ((emptyVarSet, [(ty,ty2)]), pred, p2) - | p2@(IParam ip2 ty2, _) <- preds - , ip==ip2 - , not (ty `tcEqType` ty2)] - -improveOne inst_env pred@(ClassP cls tys, _) preds + -> [Equation] -- Needs to be an Equation because + -- of quantified variables +-- Post: Equations oriented from the template (matching instance) to the workitem! +improveFromInstEnv _inst_env (pred,_loc) + | not (isClassPred pred) + = panic "improveFromInstEnv: not a class predicate" +improveFromInstEnv inst_env pred@(ClassP cls tys, _) | tys `lengthAtLeast` 2 - = instance_eqns ++ pairwise_eqns - -- NB: we put the instance equations first. This biases the - -- order so that we first improve individual constraints against the - -- instances (which are perhaps in a library and less likely to be - -- wrong; and THEN perform the pairwise checks. - -- The other way round, it's possible for the pairwise check to succeed - -- and cause a subsequent, misleading failure of one of the pair with an - -- instance declaration. See tcfail143.hs for an example - where - (cls_tvs, cls_fds) = classTvsFds cls - instances = inst_env cls - rough_tcs = roughMatchTcs tys - - -- NOTE that we iterate over the fds first; they are typically - -- empty, which aborts the rest of the loop. - pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)] - pairwise_eqns -- This group comes from pairwise comparison - = [ (eqn, pred, p2) - | fd <- cls_fds - , p2@(ClassP cls2 tys2, _) <- preds - , cls == cls2 - , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2 - ] - - instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)] - instance_eqns -- This group comes from comparing with instance decls - = [ (eqn, p_inst, pred) - | fd <- cls_fds -- Iterate through the fundeps first, + = [ FDEqn { fd_qtvs = qtvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred } + | fd <- cls_fds -- Iterate through the fundeps first, -- because there often are none! - , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs + , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs -- Trim the rough_tcs based on the head of the fundep. -- Remember that instanceCantMatch treats both argumnents -- symmetrically, so it's ok to trim the rough_tcs, -- rather than trimming each inst_tcs in turn - , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst, - is_tcs = inst_tcs }) <- instances - , not (instanceCantMatch inst_tcs trimmed_tcs) - , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys - , let p_inst = (mkClassPred cls tys_inst, - sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd) - , ptext (sLit "in the instance declaration at") - <+> ppr (getSrcLoc ispec)]) - ] - -improveOne _ _ _ - = [] + , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst, + is_tcs = inst_tcs }) <- instances + , not (instanceCantMatch inst_tcs trimmed_tcs) + , let p_inst = (mkClassPred cls tys_inst, + sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd) + , ptext (sLit "in the instance declaration at") + <+> ppr (getSrcLoc ispec)]) + , (qtvs, eqs) <- checkClsFD qtvs fd cls_tvs tys_inst tys -- NB: orientation + , not (null eqs) + ] + where + (cls_tvs, cls_fds) = classTvsFds cls + instances = classInstances inst_env cls + rough_tcs = roughMatchTcs tys +improveFromInstEnv _ _ = [] checkClsFD :: TyVarSet -- Quantified type variables; see note below -> FunDep TyVar -> [TyVar] -- One functional dependency from the class -> [Type] -> [Type] - -> [Equation] + -> [(TyVarSet, [FDEq])] checkClsFD qtvs fd clas_tvs tys1 tys2 -- 'qtvs' are the quantified type variables, the ones which an be instantiated @@ -313,52 +353,69 @@ checkClsFD qtvs fd clas_tvs tys1 tys2 length tys1 == length clas_tvs , ppr tys1 <+> ppr tys2 ) - case tcUnifyTys bind_fn ls1 ls2 of + case tcUnifyTys bind_fn ltys1 ltys2 of Nothing -> [] - Just subst | isJust (tcUnifyTys bind_fn rs1' rs2') - -- Don't include any equations that already hold. + Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2') + -- Don't include any equations that already hold. -- Reason: then we know if any actual improvement has happened, -- in which case we need to iterate the solver - -- In making this check we must taking account of the fact that any - -- qtvs that aren't already instantiated can be instantiated to anything + -- In making this check we must taking account of the fact that any + -- qtvs that aren't already instantiated can be instantiated to anything -- at all - -> [] - - | otherwise -- Aha! A useful equation - -> [ (qtvs', zip rs1' rs2')] + -- NB: We can't do this 'is-useful-equation' check element-wise + -- because of: + -- class C a b c | a -> b c + -- instance C Int x x + -- [Wanted] C Int alpha Int + -- We would get that x -> alpha (isJust) and x -> Int (isJust) + -- so we would produce no FDs, which is clearly wrong. + -> [] + + | otherwise + -> [(qtvs', fdeqs)] -- We could avoid this substTy stuff by producing the eqn -- (qtvs, ls1++rs1, ls2++rs2) -- which will re-do the ls1/ls2 unification when the equation is -- executed. What we're doing instead is recording the partial -- work of the ls1/ls2 unification leaving a smaller unification problem - where - rs1' = substTys subst rs1 - rs2' = substTys subst rs2 + where + rtys1' = map (substTy subst) rtys1 + irs2' = map (\(i,x) -> (i,substTy subst x)) irs2 + rtys2' = map snd irs2' + + fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2' + -- Don't discard anything! + -- We could discard equal types but it's an overkill to call + -- tcEqType again, since we know for sure that /at least one/ + -- equation in there is useful) + qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs - -- qtvs' are the quantified type variables - -- that have not been substituted out - -- - -- Eg. class C a b | a -> b - -- instance C Int [y] - -- Given constraint C Int z - -- we generate the equation - -- ({y}, [y], z) + -- qtvs' are the quantified type variables + -- that have not been substituted out + -- + -- Eg. class C a b | a -> b + -- instance C Int [y] + -- Given constraint C Int z + -- we generate the equation + -- ({y}, [y], z) where bind_fn tv | tv `elemVarSet` qtvs = BindMe | otherwise = Skolem - (ls1, rs1) = instFD fd clas_tvs tys1 - (ls2, rs2) = instFD fd clas_tvs tys2 + (ltys1, rtys1) = instFD fd clas_tvs tys1 + (ltys2, irs2) = instFD_WithPos fd clas_tvs tys2 +\end{code} + +\begin{code} instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type +-- A simpler version of instFD_WithPos to be used in checking instance coverage etc. instFD (ls,rs) tvs tys = (map lookup ls, map lookup rs) where env = zipVarEnv tvs tys lookup tv = lookupVarEnv_NF env tv -\end{code} -\begin{code} checkInstCoverage :: Class -> [Type] -> Bool -- Check that the Coverage Condition is obeyed in an instance decl -- For example, if we have -- 1.7.10.4