X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcInteract.lhs;h=b279c2fc0ae5952014794db754e638d8197cfdae;hp=bc0aae0fa62f4ccbb757acb9259a553ae52570e1;hb=HEAD;hpb=62f76a3cbced691b60f511fb83547a5d62653252 diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index bc0aae0..b279c2f 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -1,7 +1,8 @@ \begin{code} module TcInteract ( - solveInteract, AtomicInert, tyVarsOfInert, - InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, foldISEqCts + solveInteract, solveInteractGiven, solveInteractWanted, + AtomicInert, tyVarsOfInert, + InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, ) where #include "HsVersions.h" @@ -11,6 +12,7 @@ import BasicTypes import TcCanonical import VarSet import Type +import Unify import Id import Var @@ -18,25 +20,25 @@ import Var import TcType import HsBinds -import InstEnv +import Inst( tyVarsOfEvVar ) import Class import TyCon import Name import FunDeps -import Control.Monad ( when ) - import Coercion import Outputable import TcRnTypes +import TcMType ( isSilentEvVar ) import TcErrors import TcSMonad import Bag import qualified Data.Map as Map -import Control.Monad( unless ) +import Control.Monad( when ) + import FastString ( sLit ) import DynFlags \end{code} @@ -68,8 +70,11 @@ An InertSet is a bag of canonical constraints, with the following invariants: will be marked as solved right before being pushed into the inert set. See note [Touchables and givens]. - 8 No Given constraint mentions a touchable unification variable, - except if the + 8 No Given constraint mentions a touchable unification variable, but + Given/Solved may do so. + + 9 Given constraints will also have their superclasses in the inert set, + but Given/Solved will not. Note that 6 and 7 are /not/ enforced by canonicalization but rather by insertion in the inert list, ie by TcInteract. @@ -84,80 +89,90 @@ implication constraint (when in top-level inference mode). \begin{code} -data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts - -- Invariant: all Given or Derived +data CCanMap a = CCanMap { cts_given :: Map.Map a CanonicalCts + -- Invariant: all Given + , cts_derived :: Map.Map a CanonicalCts + -- Invariant: all Derived , cts_wanted :: Map.Map a CanonicalCts } -- Invariant: all Wanted + cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts -cCanMapToBag cmap = Map.fold unionBags rest_cts (cts_givder cmap) - where rest_cts = Map.fold unionBags emptyCCan (cts_wanted cmap) +cCanMapToBag cmap = Map.fold unionBags rest_wder (cts_given cmap) + where rest_wder = Map.fold unionBags rest_der (cts_wanted cmap) + rest_der = Map.fold unionBags emptyCCan (cts_derived cmap) emptyCCanMap :: CCanMap a -emptyCCanMap = CCanMap { cts_givder = Map.empty, cts_wanted = Map.empty } +emptyCCanMap = CCanMap { cts_given = Map.empty + , cts_derived = Map.empty, cts_wanted = Map.empty } updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a updCCanMap (a,ct) cmap = case cc_flavor ct of Wanted {} -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) } - _ - -> cmap { cts_givder = Map.insertWith unionBags a this_ct (cts_givder cmap) } + Given {} + -> cmap { cts_given = Map.insertWith unionBags a this_ct (cts_given cmap) } + Derived {} + -> cmap { cts_derived = Map.insertWith unionBags a this_ct (cts_derived cmap) } where this_ct = singleCCan ct getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a) -- Gets the relevant constraints and returns the rest of the CCanMap getRelevantCts a cmap - = let relevant = unionBags (Map.findWithDefault emptyCCan a (cts_wanted cmap)) - (Map.findWithDefault emptyCCan a (cts_givder cmap)) + = let relevant = unionManyBags [ Map.findWithDefault emptyCCan a (cts_wanted cmap) + , Map.findWithDefault emptyCCan a (cts_given cmap) + , Map.findWithDefault emptyCCan a (cts_derived cmap) ] residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap) - , cts_givder = Map.delete a (cts_givder cmap) } + , cts_given = Map.delete a (cts_given cmap) + , cts_derived = Map.delete a (cts_derived cmap) } in (relevant, residual_map) -extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a) --- Gets the wanted constraints and returns a residual CCanMap -extractUnsolvedCMap cmap = - let unsolved = Map.fold unionBags emptyCCan (cts_wanted cmap) - in (unsolved, cmap { cts_wanted = Map.empty}) +extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a) +-- Gets the wanted or derived constraints and returns a residual +-- CCanMap with only givens. +extractUnsolvedCMap cmap = + let wntd = Map.fold unionBags emptyCCan (cts_wanted cmap) + derd = Map.fold unionBags emptyCCan (cts_derived cmap) + in (wntd `unionBags` derd, + cmap { cts_wanted = Map.empty, cts_derived = Map.empty }) + -- See Note [InertSet invariants] data InertSet = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan) - - , inert_dicts :: CCanMap Class -- Dictionaries only + , inert_dicts :: CCanMap Class -- Dictionaries only , inert_ips :: CCanMap (IPName Name) -- Implicit parameters - , inert_funeqs :: CCanMap TyCon -- Type family equalities only + , inert_frozen :: CanonicalCts + , inert_funeqs :: CCanMap TyCon -- Type family equalities only -- This representation allows us to quickly get to the relevant -- inert constraints when interacting a work item with the inert set. - - - , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already - -- and reside either in the worklist or in the inerts } tyVarsOfInert :: InertSet -> TcTyVarSet tyVarsOfInert (IS { inert_eqs = eqs , inert_dicts = dictmap , inert_ips = ipmap - , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts - where cts = eqs `andCCan` cCanMapToBag dictmap - `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap - -type FDImprovement = (PredType,PredType) -type FDImprovements = [(PredType,PredType)] + , inert_frozen = frozen + , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts + where + cts = eqs `andCCan` frozen `andCCan` cCanMapToBag dictmap + `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap instance Outputable InertSet where ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is)) - , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is))) + , 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))) + , text "Frozen errors =" <+> -- Clearly print frozen errors + vcat (map ppr (Bag.bagToList $ inert_frozen is)) ] emptyInert :: InertSet emptyInert = IS { inert_eqs = Bag.emptyBag + , inert_frozen = Bag.emptyBag , inert_dicts = emptyCCanMap , inert_ips = emptyCCanMap - , inert_funeqs = emptyCCanMap - , inert_fds = [] } + , inert_funeqs = emptyCCanMap } updInertSet :: InertSet -> AtomicInert -> InertSet updInertSet is item @@ -171,101 +186,27 @@ updInertSet is item | Just tc <- isCFunEqCan_Maybe item -- Function equality = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) } | otherwise - = pprPanic "Unknown form of constraint!" (ppr item) - -updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet -updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is } -updInertSetFDImprs is Nothing = is - -foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a --- Fold over the equalities of the inerts -foldISEqCtsM k z IS { inert_eqs = eqs } - = Bag.foldlBagM k z eqs - -foldISEqCts :: (a -> AtomicInert -> a) -> a -> InertSet -> a -foldISEqCts k z IS { inert_eqs = eqs } - = Bag.foldlBag k z eqs + = is { inert_frozen = inert_frozen is `Bag.snocBag` item } extractUnsolved :: InertSet -> (InertSet, CanonicalCts) --- Postcondition: the canonical cts returnd are the very same as the --- WantedEvVars in their canonical form. +-- Postcondition: the returned canonical cts are either Derived, or Wanted. extractUnsolved is@(IS {inert_eqs = eqs}) = let is_solved = is { inert_eqs = solved_eqs , inert_dicts = solved_dicts , inert_ips = solved_ips - , inert_funeqs = solved_funeqs } + , inert_frozen = emptyCCan + , inert_funeqs = solved_funeqs } in (is_solved, unsolved) - where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs + where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenOrSolvedCt) eqs (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is) (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is) (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is) - unsolved = unsolved_eqs `unionBags` + unsolved = unsolved_eqs `unionBags` inert_frozen is `unionBags` unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs - -haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool -haveBeenImproved [] _ _ = False -haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2' - | tcEqPred pty1 pty1' && tcEqPred pty2 pty2' - = True - | tcEqPred pty1 pty2' && tcEqPred pty2 pty1' - = True - | otherwise - = haveBeenImproved fdimprs pty1' pty2' - -getFDImprovements :: InertSet -> FDImprovements --- Return a list of the improvements that have kicked in so far -getFDImprovements = inert_fds - \end{code} -{-- DV: This note will go away! - -Note [Touchables and givens] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Touchable variables will never show up in givens which are inputs to -the solver. However, touchables may show up in givens generated by the flattener. -For example, - - axioms: - G Int ~ Char - F Char ~ Int - - wanted: - F (G alpha) ~w Int - -canonicalises to - - G alpha ~g b - F b ~w Int - -which can be put in the inert set. Suppose we also have a wanted - - alpha ~w Int - -We cannot rewrite the given G alpha ~g b using the wanted alpha ~w -Int. Instead, after reacting alpha ~w Int with the whole inert set, -we observe that we can solve it by unifying alpha with Int, so we mark -it as solved and put it back in the *work list*. [We also immediately unify -alpha := Int, without telling anyone, see trySpontaneousSolve function, to -avoid doing this in the end.] - -Later, because it is solved (given, in effect), we can use it to rewrite -G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually, -we will dispatch the remaining wanted constraints using the top-level axioms. - -Finally, note that after reacting a wanted equality with the entire inert set -we may end up with something like - - b ~w alpha - -which we should flip around to generate the solved constraint alpha ~s b. - --} - - - %********************************************************************* %* * * Main Interaction Solver * @@ -290,22 +231,6 @@ Note [Basic plan] type AtomicInert = CanonicalCt -- constraint pulled from InertSet type WorkItem = CanonicalCt -- constraint pulled from WorkList --- A mixture of Given, Wanted, and Derived constraints. --- We split between equalities and the rest to process equalities first. -type WorkList = CanonicalCts - -unionWorkLists :: WorkList -> WorkList -> WorkList -unionWorkLists = andCCan - -isEmptyWorkList :: WorkList -> Bool -isEmptyWorkList = isEmptyCCan - -emptyWorkList :: WorkList -emptyWorkList = emptyCCan - -workListFromCCan :: CanonicalCt -> WorkList -workListFromCCan = singleCCan - ------------------------ data StopOrContinue = Stop -- Work item is consumed @@ -334,21 +259,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 @@ -365,9 +293,9 @@ 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 } + ; let itr' = itr { sr_new_work = accum_work `unionWorkList` sr_new_work itr } ; run_pipeline stages itr' } \end{code} @@ -399,82 +327,129 @@ React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canoni -- returning an extended inert set. -- -- See Note [Touchables and givens]. -solveInteract :: InertSet -> Bag (CtFlavor,EvVar) -> TcS InertSet +solveInteractGiven :: InertSet -> GivenLoc -> [EvVar] -> TcS InertSet +solveInteractGiven inert gloc evs + = do { (_, inert_ret) <- solveInteract inert $ listToBag $ + map mk_given evs + ; return inert_ret } + where + flav = Given gloc GivenOrig + mk_given ev = mkEvVarX ev flav + +solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet +solveInteractWanted inert wvs + = do { (_,inert_ret) <- solveInteract inert $ listToBag $ + map wantedToFlavored wvs + ; return inert_ret } + +solveInteract :: InertSet -> Bag FlavoredEvVar -> TcS (Bool, InertSet) +-- Post: (True, inert_set) means we managed to discharge all constraints +-- without actually doing any interactions! +-- (False, inert_set) means some interactions occurred solveInteract inert ws = do { dyn_flags <- getDynFlags - ; sctx <- getTcSContext - - ; traceTcS "solveInteract, before clever canonicalization:" $ - ppr (mapBag (\(ct,ev) -> (ct,evVarPred ev)) ws) - - ; can_ws <- foldlBagM (tryPreSolveAndCanon sctx inert) emptyCCan ws - - ; traceTcS "solveInteract, after clever canonicalization:" $ - ppr can_ws - - ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert can_ws } - -tryPreSolveAndCanon :: SimplContext -> InertSet -> CanonicalCts -> (CtFlavor, EvVar) -> TcS CanonicalCts --- Checks if this constraint can be immediately solved from a constraint in the --- inert set or in the previously encountered CanonicalCts and only then --- canonicalise it. See Note [Avoiding the superclass explosion] -tryPreSolveAndCanon sctx is cts_acc (fl,ev_var) - | ClassP clas tys <- evVarPred ev_var - , not $ simplEqsOnly sctx -- And we *can* discharge constraints from other constraints - = do { let (relevant_inert_dicts,_) = getRelevantCts clas (inert_dicts is) - ; b <- dischargeFromCans (cts_acc `unionBags` relevant_inert_dicts) - (fl,ev_var,clas,tys) - ; extra_cts <- if b then return emptyCCan else mkCanonical fl ev_var - ; return (cts_acc `unionBags` extra_cts) } - | otherwise - = do { extra_cts <- mkCanonical fl ev_var - ; return (cts_acc `unionBags` extra_cts) } - -dischargeFromCans :: CanonicalCts -> (CtFlavor,EvVar,Class,[Type]) -> TcS Bool -dischargeFromCans cans (fl,ev,clas,tys) - = Bag.foldlBagM discharge_ct False cans - where discharge_ct :: Bool -> CanonicalCt -> TcS Bool - discharge_ct True _ct = return True - discharge_ct False (CDictCan { cc_id = ev1, cc_flavor = fl1 - , cc_class = clas1, cc_tyargs = tys1 }) - | clas1 == clas - , (and $ zipWith tcEqType tys tys1) - , fl1 `canSolve` fl - = setEvBind ev (EvId ev1) >> return True - discharge_ct False _ct = return False -\end{code} + ; sctx <- getTcSContext -Note [Avoiding the superclass explosion] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + ; traceTcS "solveInteract, before clever canonicalization:" $ + vcat [ text "ws = " <+> ppr (mapBag (\(EvVarX ev ct) + -> (ct,evVarPred ev)) ws) + , text "inert = " <+> ppr inert ] + + ; can_ws <- mkCanonicalFEVs ws + + ; (flag, inert_ret) + <- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws -Consider the example: - f = [(0,1,0,1,0)] -We have 5 wanted (Num alpha) constraints. If we simply try to canonicalize and add them -in our worklist, we will also get all of their superclasses as Derived, hence we will -have an inert set that contains 5*n constraints, where n is the number of superclasses -of of Num. That is bad for the additional reason that we keep *all* the Derived, even -for identical class constraints (for reasons related to recursive dictionaries). + ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $ + vcat [ text "No interaction happened = " <+> ppr flag + , text "inert_ret = " <+> ppr inert_ret ] -Instead, what we do with tryPreSolveAndCanon, is when we encounter a new constraint, -such as the second (Num alpha) above we very quickly see if it can be immediately -discharged by a class constraint in our inert set or the previous canonicals. If so, -we add nothing to the returned canonical constraints. + ; return (flag, inert_ret) } + +tryPreSolveAndInteract :: SimplContext + -> DynFlags + -> CanonicalCt + -> (Bool, InertSet) + -> TcS (Bool, InertSet) +-- Returns: True if it was able to discharge this constraint AND all previous ones +tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert) + = do { let inert_cts = get_inert_cts (evVarPred ev_var) + + ; this_one_discharged <- + if isCFrozenErr ct then + return False + else + dischargeFromCCans inert_cts ev_var fl + + ; if this_one_discharged + then return (all_previous_discharged, inert) + + else do + { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert + ; return (False, inert_ret) } } + + where + ev_var = cc_id ct + fl = cc_flavor ct + + get_inert_cts (ClassP clas _) + | simplEqsOnly sctx = emptyCCan + | otherwise = fst (getRelevantCts clas (inert_dicts inert)) + get_inert_cts (IParam {}) + = emptyCCan -- We must not do the same thing for IParams, because (contrary + -- to dictionaries), work items /must/ override inert items. + -- See Note [Overriding implicit parameters] in TcInteract. + get_inert_cts (EqPred {}) + = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert) + +dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool +-- See if this (pre-canonicalised) work-item is identical to a +-- one already in the inert set. Reasons: +-- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints +-- b) Termination for improve_eqs in TcSimplify.simpl_loop +dischargeFromCCans cans ev fl + = Bag.foldrBag discharge_ct (return False) cans + where + the_pred = evVarPred ev + + discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool + discharge_ct ct _rest + | evVarPred (cc_id ct) `eqPred` the_pred + , cc_flavor ct `canSolve` fl + = 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 } + + discharge_ct _ct rest = rest +\end{code} -For our particular example this will reduce the size of the inert set that we use from -5*n to just n. And hence the number of all possible interactions that we have to look -through is significantly smaller! +Note [Avoiding the superclass explosion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +This note now is not as significant as it used to be because we no +longer add the superclasses of Wanted as Derived, except only if they +have equality superclasses or superclasses with functional +dependencies. The fear was that hundreds of identical wanteds would +give rise each to the same superclass or equality Derived's which +would lead to a blo-up in the number of interactions. + +Instead, what we do with tryPreSolveAndCanon, is when we encounter a +new constraint, we very quickly see if it can be immediately +discharged by a class constraint in our inert set or the previous +canonicals. If so, we add nothing to the returned canonical +constraints. \begin{code} -solveOne :: InertSet -> WorkItem -> TcS InertSet -solveOne inerts workItem +solveOne :: WorkItem -> InertSet -> TcS InertSet +solveOne workItem inerts = do { dyn_flags <- getDynFlags - ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem + ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts } ----------------- solveInteractWithDepth :: (Int, Int, [WorkItem]) - -> InertSet -> WorkList -> TcS InertSet -solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws + -> WorkList -> InertSet -> TcS InertSet +solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert | isEmptyWorkList ws = return inert @@ -484,33 +459,29 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws | otherwise = do { traceTcS "solveInteractWithDepth" $ vcat [ text "Current depth =" <+> ppr n - , text "Max depth =" <+> ppr max_depth ] + , text "Max depth =" <+> ppr max_depth + , text "ws =" <+> ppr ws ] + - -- Solve equalities first - ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws - ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs - ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs } + ; foldrWorkListM (solveOneWithDepth ctxt) inert ws } + -- use foldr to preserve the order ------------------ -- Fully interact the given work item with an inert set, and return a -- 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 + -> WorkItem -> InertSet -> TcS InertSet +solveOneWithDepth (max_depth, depth, stack) work inert + = 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) - new_inert new_work + ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_work new_inert + + ; traceFireTcS depth (text "Done }" <+> ppr work) - ; traceTcS0 (indent ++ "Done }") (ppr work) ; return res_inert } - where - indent = replicate (2*n) ' ' thePipeline :: [(String,SimplifierStage)] thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage) @@ -552,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 @@ -562,13 +533,15 @@ spontaneousSolveStage workItem inerts , sr_stop = ContinueWith workItem } SPSolved workItem' - | not (isGivenCt workItem) + | not (isGivenOrSolvedCt workItem) -- Original was wanted or derived but we have now made him -- given so we have to interact him with the inerts due to -- 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' @@ -579,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 @@ -599,7 +574,7 @@ data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError -- See Note [Touchables and givens] trySpontaneousSolve :: WorkItem -> TcS SPSolveResult trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) - | isGiven gw + | isGivenOrSolved gw = return SPCantSolve | Just tv2 <- tcGetTyVar_maybe xi = do { tch1 <- isTouchableMetaTyVar tv1 @@ -612,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 } } @@ -630,13 +606,16 @@ trySpontaneousEqOneWay cv gw tv xi -- so we have its more specific kind in our hands ; if kxi `isSubKind` tyVarKind tv then solveWithIdentity cv gw tv xi - else if tyVarKind tv `isSubKind` kxi then + else return SPCantSolve +{- + else if tyVarKind tv `isSubKind` kxi then return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way -- This case covers the a_touchable :: * ~ b_untouchable :: ?? -- which has to be deferred or floated out for someone else to solve -- it in a scope where 'b' is no longer untouchable. else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors] ; return SPError } +-} } | otherwise -- Still can't solve, sig tyvar and non-variable rhs = return SPCantSolve @@ -650,8 +629,9 @@ trySpontaneousEqTwoWay cv gw tv1 tv2 | k2 `isSubKind` k1 = solveWithIdentity cv gw tv1 (mkTyVarTy tv2) | otherwise -- None is a subkind of the other, but they are both touchable! - = do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2) - ; return SPError } + = return SPCantSolve + -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2) + -- ; return SPError } where k1 = tyVarKind tv1 k2 = tyVarKind tv2 @@ -681,24 +661,24 @@ so this situation can't happen. Note [Spontaneous solving and kind compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note that our canonical constraints insist that *all* equalities (tv ~ +xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible* +the same kinds. ("compatible" means one is a subKind of the other.) + + - It can't be *equal* kinds, because + b) wanted constraints don't necessarily have identical kinds + eg alpha::? ~ Int + b) a solved wanted constraint becomes a given + + - SPJ thinks that *given* constraints (tv ~ tau) always have that + tau has a sub-kind of tv; and when solving wanted constraints + in trySpontaneousEqTwoWay we re-orient to achieve this. -Note that our canonical constraints insist that only *given* equalities (tv ~ xi) -or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds. - - - We have to require this because: - Given equalities can be freely used to rewrite inside - other types or constraints. - - We do not have to do the same for wanteds because: - First, wanted equations (tv ~ xi) where tv is a touchable - unification variable may have kinds that do not agree (the - kind of xi must be a sub kind of the kind of tv). Second, any - potential kind mismatch will result in the constraint not - being soluble, which will be reported anyway. This is the - reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@ - will perform a kind compatibility check, and only then will - they proceed to @solveWithIdentity@. - -Caveat: + - Note that the kind invariant is maintained by rewriting. + Eg wanted1 rewrites wanted2; if both were compatible kinds before, + wanted2 will be afterwards. Similarly givens. + +Caveat: - Givens from higher-rank, such as: type family T b :: * -> * -> * type instance T Bool = (->) @@ -746,29 +726,49 @@ solveWithIdentity cv wd tv xi text "Right Kind is : " <+> ppr (typeKind xi) ] - ; setWantedTyBind tv xi -- Set tv := xi_unflat - ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi - - ; case wd of Wanted {} -> setWantedCoBind cv xi - Derived {} -> setDerivedCoBind cv xi - _ -> pprPanic "Can't spontaneously solve given!" empty + ; setWantedTyBind tv xi + ; let refl_xi = mkReflCo xi + ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_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 = mkGivenFlavor wd UnkSkol - , cc_tyvar = tv, cc_rhs = xi }) - } - + , cc_flavor = mkSolvedFlavor wd UnkSkol + , cc_tyvar = tv, cc_rhs = xi }) } \end{code} - - ********************************************************************************* * * The interact-with-inert Stage * * ********************************************************************************* +Note [The Solver Invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We always add Givens first. So you might think that the solver has +the invariant + + If the work-item is Given, + then the inert item must Given + +But this isn't quite true. Suppose we have, + c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int +After processing the first two, we get + c1: [G] beta ~ [alpha], c2 : [W] blah +Now, c3 does not interact with the the given c1, so when we spontaneously +solve c3, we must re-react it with the inert set. So we can attempt a +reaction between inert c2 [W] and work-item c3 [G]. + +It *is* true that [Solver Invariant] + If the work-item is Given, + AND there is a reaction + then the inert item must Given +or, equivalently, + If the work-item is Given, + and the inert item is Wanted/Derived + then there is no reaction + \begin{code} -- Interaction result of WorkItem <~> AtomicInert data InteractResult @@ -786,50 +786,50 @@ data InteractResult , ir_new_work :: WorkList -- new work items to add to the WorkList - , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in + , 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 +data InertAction = KeepInert | DropInert -mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult -mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing +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 } -mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult -mkIRStop keep newWork = return $ IR Stop keep newWork Nothing +mkIRStopK :: String -> WorkList -> TcS InteractResult +mkIRStopK rule newWork + = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert + , ir_new_work = newWork, ir_fire = Just rule } -mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult -mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr) - -dischargeWorkItem :: Monad m => m InteractResult -dischargeWorkItem = mkIRStop KeepInert emptyWorkList +mkIRStopD :: String -> WorkList -> TcS InteractResult +mkIRStopD rule newWork + = return $ IR { ir_stop = Stop, ir_inert_action = DropInert + , 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] --------------------------------------------------- --- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we --- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've +-- Interact a single WorkItem with the equalities of an inert set as +-- far as possible, i.e. until we get a Stop result from an individual +-- reaction (i.e. when the WorkItem is consumed), or until we've -- interact the WorkItem with the entire equalities of the InertSet interactWithInertEqsStage :: SimplifierStage -interactWithInertEqsStage workItem inert - = foldISEqCtsM interactNext initITR inert - where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- Will fold over equalities - , inert_dicts = inert_dicts inert - , inert_ips = inert_ips inert - , inert_funeqs = inert_funeqs inert - , inert_fds = inert_fds inert - } - , sr_new_work = emptyWorkList - , sr_stop = ContinueWith workItem } - +interactWithInertEqsStage depth workItem inert + = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert) + -- use foldr to preserve the order + where + initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan } + , sr_new_work = emptyWorkList + , sr_stop = ContinueWith workItem } --------------------------------------------------- -- Interact a single WorkItem with *non-equality* constraints in the inert set. @@ -838,16 +838,21 @@ 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.foldrBagM (interactNext depth) initITR relevant + -- use foldr to preserve the order where getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) - getISRelevant (CDictCan { cc_class = cls } ) is - = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is) + getISRelevant (CFrozenErr {}) is = (emptyCCan, is) + -- Nothing s relevant; we have alread interacted + -- it with the equalities in the inert set + + getISRelevant (CDictCan { cc_class = cls } ) is + = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is) in (relevant, is { inert_dicts = residual_map }) getISRelevant (CFunEqCan { cc_fun = tc } ) is = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is) @@ -866,52 +871,51 @@ 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 - fdimprs_old = getFDImprovements inerts - - ; ir <- interactWithInert fdimprs_old 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 = updInertSetFDImprs upd_inert (ir_improvement ir) - upd_inert = case ir_inert_action ir of - KeepInert -> inerts `updInertSet` inert - DropInert -> inerts - KeepTransformedInert inert' -> inerts `updInertSet` inert' +interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult +interactNext depth inert it + | 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 (isEmptyWorkList 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 `unionWorkList` new_work + , sr_stop = stop } } | otherwise = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert } -- Do a single interaction of two constraints. -interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult -interactWithInert fdimprs inert workitem - = do { ctxt <- getTcSContext - ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem - inert_ev = cc_id inert - work_ev = cc_id workitem - - -- Never interact a wanted and a derived where the derived's evidence - -- mentions the wanted evidence in an unguarded way. - -- See Note [Superclasses and recursive dictionaries] - -- and Note [New Wanted Superclass Work] - -- We don't have to do this for givens, as we fully know the evidence for them. - ; rec_ev_ok <- - case (cc_flavor inert, cc_flavor workitem) of - (Wanted {}, Derived {}) -> isGoodRecEv work_ev inert_ev - (Derived {}, Wanted {}) -> isGoodRecEv inert_ev work_ev - _ -> return True - - ; if is_allowed && rec_ev_ok then - doInteractWithInert fdimprs inert workitem +interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult +interactWithInert inert workItem + = do { ctxt <- getTcSContext + ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workItem + + ; if is_allowed then + doInteractWithInert inert workItem else - noInteraction workitem - } + noInteraction workItem + } allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool -- Allowed interactions @@ -920,102 +924,149 @@ allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only allowedInteraction _ _ _ = True -------------------------------------------- -doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult +doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult -- Identical class constraints. -doInteractWithInert fdimprs - (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) - workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) - | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2) - = solveOneFromTheOther (d1,fl1) workItem +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 && (not (isGiven fl1 && isGiven fl2)) - = -- See Note [When improvement happens] - do { let pty1 = ClassP cls1 tys1 + | cls1 == cls2 + = 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] - - ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs - ; fd_work <- canWanteds wevvars - -- See Note [Generating extra equalities] - ; traceTcS "Checking if improvements existed." (ppr fdimprs) - ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then - -- Must keep going - mkIRContinue workItem KeepInert fd_work - else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2)) - ; mkIRStop_RecordImprovement KeepInert - (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2) - } - -- See Note [FunDep Reactions] + work_item_pred_loc = (pty2, pprFlavorArising 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 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. -doInteractWithInert _fdimprs - (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) +doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis }) | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes xis = 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 _fdimprs - (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) +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 (workListFromNonEq rewritten_dict) } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. -doInteractWithInert _fdimprs - (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) +doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty }) | 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 _fdimprs - (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) +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 (workListFromNonEq rewritten_ip) } -- Two implicit parameter constraints. If the names are the same, -- but their types are not, we generate a wanted type equality -- that equates the type (this is "improvement"). -- However, we don't actually need the coercion evidence, -- so we just generate a fresh coercion variable that isn't used anywhere. -doInteractWithInert _fdimprs - (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) +doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 }) - | nm1 == nm2 && isGiven wfl && isGiven ifl + | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl = -- 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 + | nm1 == nm2 && ty1 `eqType` ty2 + = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem | nm1 == nm2 = -- See Note [When improvement happens] - 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 } - - + do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation] + ; let flav = Wanted (combineCtLoc ifl wfl) + ; cans <- mkCanonical flav co_var + ; case wfl of + Given {} -> pprPanic "Unexpected given IP" (ppr workItem) + Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem) + Wanted {} -> + do { setIPBind (cc_id workItem) $ + EvCast id1 (mkSymCo (mkCoVarCo co_var)) + ; mkIRStopK "IP/IP interaction (solved)" cans } + } -- Never rewrite a given with a wanted equality, and a type function -- equality can never rewrite an equality. We rewrite LHS *and* RHS @@ -1023,25 +1074,23 @@ doInteractWithInert _fdimprs -- we know about equalities. -- Inert: equality, work item: function equality -doInteractWithInert _fdimprs - (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 }) +doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 }) (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc , cc_tyargs = args, cc_rhs = xi2 }) | 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) } + ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) } -- Must Stop here, because we may no longer be inert after the rewritting. -- Inert: function equality, work item: equality -doInteractWithInert _fdimprs - (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc +doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc , cc_tyargs = args, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 }) | 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 (workListFromEq 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: @@ -1051,54 +1100,75 @@ doInteractWithInert _fdimprs -- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] } -- At the end, which is *not* inert. So we should unfortunately DropInert here. -doInteractWithInert _fdimprs - (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 +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 eqType args1 args2) + , Just GivenSolved <- isGiven_maybe fl1 + = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList + | 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) - ; mkIRStop KeepInert cans } + = 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) - ; mkIRContinue workItem DropInert cans } + = 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 _fdimprs - (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) +doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 }) -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 - = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert cans } + = 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) - ; mkIRContinue workItem DropInert cans } + = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1) + ; 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 } + ; mkIRStopK "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) + ; mkIRStopK "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 "Frozen/Eq" workItem DropInert rewritten_frozen } -- Fall-through case for all other situations -doInteractWithInert _fdimprs _ workItem = noInteraction workItem +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)) - _given_or_derived -> setDictBind dv' (EvCast dv 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 + ; return (CDictCan { cc_id = dv' , cc_flavor = gw , cc_class = cl @@ -1106,12 +1176,14 @@ 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)) - _given_or_derived -> setIPBind ipid' (EvCast ipid 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 + ; return (CIPCan { cc_id = ipid' , cc_flavor = gw , cc_ip_nm = nm @@ -1119,21 +1191,24 @@ 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' - ; cv2' <- case gw of - Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2' - ; setWantedCoBind cv2 $ - fun_co `mkTransCoercion` - mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co - ; return cv2' } - _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2' $ - mkSymCoercion fun_co `mkTransCoercion` - mkCoVarCoercion cv2 `mkTransCoercion` xi2_co + xi2_co = co_subst xi2 -- xi2_co :: xi2 ~ xi2' + + ; cv2' <- newCoVar (mkTyConApp tc args') xi2' + ; case gw of + 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 () + ; return (CFunEqCan { cc_id = cv2' , cc_flavor = gw , cc_tyargs = args' @@ -1151,83 +1226,108 @@ 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) (setWantedCoBind cv2 (mkSymCoercion co2')) - ; return emptyCCan } + = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2')) + ; return emptyWorkList } | otherwise - = do { cv2' <- - case gw of - Wanted {} - -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2' - ; setWantedCoBind cv2 $ - mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2' - ; return cv2' } - _giv_or_der - -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $ - mkCoVarCoercion cv2 `mkTransCoercion` co2' - - ; canEq gw cv2' (mkTyVarTy tv2) xi2' - } + = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2' + ; case gw of + 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: -- First Equality: co1: (XXX ~ xi1) -- Second Equality: cv2: (XXX ~ xi2) --- Where the cv1 `canSolve` cv2 equality +-- Where the cv1 `canRewrite` cv2 equality -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1), -- See Note [Efficient Orientation] for that -rewriteEqLHS which (co1,xi1) (cv2,gw,xi2) - = do { cv2' <- case (isWanted gw, which) of - (True,LeftComesFromInert) -> - do { cv2' <- newWantedCoVar xi2 xi1 - ; setWantedCoBind cv2 $ - co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2') - ; return cv2' } - (True,RightComesFromInert) -> - do { cv2' <- newWantedCoVar xi1 xi2 - ; setWantedCoBind cv2 $ - co1 `mkTransCoercion` mkCoVarCoercion cv2' - ; return cv2' } - (False,LeftComesFromInert) -> - newGivOrDerCoVar xi2 xi1 $ - mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 - (False,RightComesFromInert) -> - newGivOrDerCoVar xi1 xi2 $ - mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 - ; mkCanonical gw cv2' - } - -solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult --- First argument inert, second argument workitem. They both represent --- wanted/given/derived evidence for the *same* predicate so we try here to --- discharge one directly from the other. +rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2) + = do { cv2' <- newCoVar xi2 xi1 + ; case gw of + Wanted {} -> setCoBind cv2 $ + co1 `mkTransCo` mkSymCo (mkCoVarCo cv2') + Given {} -> setCoBind cv2' $ + mkSymCo (mkCoVarCo cv2) `mkTransCo` co1 + Derived {} -> return () + ; mkCanonical gw cv2' } + +rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2) + = do { cv2' <- newCoVar xi1 xi2 + ; case gw of + Wanted {} -> setCoBind cv2 $ + co1 `mkTransCo` mkCoVarCo cv2' + Given {} -> setCoBind cv2' $ + mkSymCo co1 `mkTransCo` mkCoVarCo cv2 + Derived {} -> return () + ; mkCanonical gw cv2' } + +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' `mkTransCo` + mkCoVarCo cv2' `mkTransCo` + mkSymCo co2b' + + Given {} -> setCoBind cv2' $ mkSymCo co2a' `mkTransCo` + mkCoVarCo cv2 `mkTransCo` + co2b' + + Derived {} -> return () + + ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) } + where + (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b + ty2a' = substTyWith [tv1] [xi1] ty2a + ty2b' = substTyWith [tv1] [xi1] ty2b + + co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a -- ty2a ~ ty2a[xi1/tv1] + co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b -- ty2b ~ ty2b[xi1/tv1] + +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 (iid,ifl) workItem - -- Both derived needs a special case. You might think that we do not need - -- two evidence terms for the same claim. But, since the evidence is partial, - -- either evidence may do in some cases; see TcSMonad.isGoodRecEv. - -- See also Example 3 in Note [Superclasses and recursive dictionaries] - | isDerived ifl && isDerived wfl - = noInteraction workItem - - | ifl `canSolve` wfl - = do { unless (isGiven wfl) $ setEvBind wid (EvId iid) - -- Overwrite the binding, if one exists - -- For Givens, which are lambda-bound, nothing to overwrite, - ; dischargeWorkItem } - - | otherwise -- wfl `canSolve` ifl - = do { unless (isGiven ifl) $ setEvBind iid (EvId wid) - ; mkIRContinue workItem DropInert emptyWorkList } +solveOneFromTheOther_ExtraWork info (ev_term,ifl) workItem extra_work + | isDerived wfl + = 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 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 extra_work + | otherwise + = ASSERT( ifl `canSolve` wfl ) + -- Because of Note [The Solver Invariant], plus Derived dealt with + 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) 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] @@ -1245,8 +1345,9 @@ our worklist. When we simplify a wanted constraint, if we first see a matching instance, we may produce new wanted work. To (1) avoid doing this work twice in the future and (2) to handle recursive dictionaries we may ``cache'' -this item as solved (in effect, given) into our inert set and with that add -its superclass constraints (as given) in our worklist. +this item as given into our inert set WITHOUT adding its superclass constraints, +otherwise we'd be in danger of creating a loop [In fact this was the exact reason +for doing the isGoodRecEv check in an older version of the type checker]. But now we have added partially solved constraints to the worklist which may interact with other wanteds. Consider the example: @@ -1257,17 +1358,12 @@ Example 1: instance Eq a => Foo [a] a --- fooDFun and wanted (Foo [t] t). We are first going to see that the instance matches -and create an inert set that includes the solved (Foo [t] t) and its -superclasses. +and create an inert set that includes the solved (Foo [t] t) but not its superclasses: d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3 - d2 :_g Eq t d2 := EvSuperClass d1 0 Our work list is going to contain a new *wanted* goal d3 :_w Eq t -It is wrong to react the wanted (Eq t) with the given (Eq t) because that would -construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert. -OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries, -at all? Consider +Ok, so how do we get recursive dictionaries, at all: Example 2: @@ -1584,7 +1680,8 @@ we keep the synonym-using RHS without expansion. \begin{code} -- If a work item has any form of interaction with top-level we get this data TopInteractResult - = NoTopInt -- No top-level interaction + = NoTopInt -- No top-level interaction + -- Equivalent to (SomeTopInt emptyWorkList (ContinueWith work_item)) | SomeTopInt { tir_new_work :: WorkList -- Sub-goals or new work (could be given, -- for superclasses) @@ -1595,38 +1692,42 @@ data TopInteractResult -- only reacted with functional dependencies -- arising from top-level instances. -topReactionsStage :: SimplifierStage -topReactionsStage workItem inerts - = do { tir <- tryTopReact workItem - ; case tir of - NoTopInt -> - return $ SR { sr_inerts = 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 - } +topReactionsStage :: SimplifierStage +topReactionsStage depth workItem inerts + = do { tir <- tryTopReact inerts workItem + -- NB: we pass the inerts as well. See Note [Instance and Given overlap] + ; case tir of + NoTopInt -> + return $ SR { sr_inerts = inerts + , sr_new_work = emptyWorkList + , sr_stop = ContinueWith workItem } + SomeTopInt tir_new_work 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 -tryTopReact workitem +tryTopReact :: InertSet -> WorkItem -> TcS TopInteractResult +tryTopReact inerts workitem = do { -- A flag controls the amount of interaction allowed -- See Note [Simplifying RULE lhs constraints] ctxt <- getTcSContext ; if allowedTopReaction (simplEqsOnly ctxt) workitem then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem) - ; doTopReact workitem } + ; doTopReact inerts workitem } else return NoTopInt } -allowedTopReaction :: Bool -> WorkItem -> Bool +allowedTopReaction :: Bool -> WorkItem -> Bool allowedTopReaction eqs_only (CDictCan {}) = not eqs_only -allowedTopReaction _ _ = True +allowedTopReaction _ _ = True - -doTopReact :: WorkItem -> TcS TopInteractResult +doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult -- The work item does not react with the inert set, so try interaction with top-level instances -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are -- added in the worklist as part of the canonicalisation process. @@ -1634,66 +1735,100 @@ doTopReact :: WorkItem -> TcS TopInteractResult -- Given dictionary -- See Note [Given constraint that matches an instance declaration] -doTopReact (CDictCan { cc_flavor = Given {} }) +doTopReact _inerts (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 _ - , 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 } } +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 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 do { fd_cans <- mkCanonicalFDAsDerived fd_work + ; return $ SomeTopInt { tir_new_work = fd_cans + , tir_new_inert = ContinueWith workItem' } + } + } + + -- Wanted dictionary -doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = 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 - ; if isEmptyWorkList fd_work then - return $ SomeTopInt - { tir_new_work = emptyWorkList - , tir_new_inert = ContinueWith workItem } - else -- More fundep work produced, just thow him back in the - -- worklist to prioritize the solution of fd equalities - return $ SomeTopInt - { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem - , 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 - -- 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' - 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 Derived - else do { let solved = makeSolvedByInst workItem - ; return $ SomeTopInt - { tir_new_work = inst_work - , tir_new_inert = ContinueWith solved } } - } } +doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc) + , cc_class = cls, cc_tyargs = xis }) + -- 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 `unionWorkList` extra_work + , tir_new_inert = ContinueWith solved } } + -- Type functions -doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl - , cc_fun = tc, cc_tyargs = args, cc_rhs = xi }) +doTopReact _inerts (CFunEqCan { cc_flavor = fl }) + | Just GivenSolved <- isGiven_maybe fl + = return NoTopInt -- If Solved, no more interactions should happen + +-- Otherwise, it's a Given, Derived, or Wanted +doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, cc_flavor = fl + , cc_fun = tc, cc_tyargs = args, cc_rhs = xi }) = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS] ; case match_res of - MatchInstNo - -> return NoTopInt + MatchInstNo -> return NoTopInt MatchInstSingle (rep_tc, rep_tys) -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys) @@ -1701,38 +1836,40 @@ doTopReact (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 - ; cv' <- case fl of - Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi - ; setWantedCoBind cv $ - coe `mkTransCoercion` - mkCoVarCoercion cv' - ; return cv' } - _ -> newGivOrDerCoVar xi rhs_ty $ - mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe - - ; can_cts <- mkCanonical fl cv' - ; return $ SomeTopInt can_cts Stop } + coe = mkAxInstCo coe_tc rep_tys + ; case fl of + Wanted {} -> do { cv' <- newCoVar rhs_ty xi + ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv' + ; can_cts <- mkCanonical fl cv' + ; let solved = workItem { cc_flavor = solved_fl } + solved_fl = mkSolvedFlavor fl UnkSkol + ; if isEmptyWorkList can_cts then + return (SomeTopInt can_cts Stop) -- No point in caching + else return $ + SomeTopInt { tir_new_work = can_cts + , tir_new_inert = ContinueWith solved } + } + Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $ + mkSymCo (mkCoVarCo cv) `mkTransCo` coe + ; can_cts <- mkCanonical fl cv' + ; return $ + SomeTopInt { tir_new_work = can_cts + , tir_new_inert = Stop } + } + Derived {} -> do { cv' <- newDerivedId (EqPred xi rhs_ty) + ; can_cts <- mkCanonical fl cv' + ; return $ + SomeTopInt { tir_new_work = can_cts + , tir_new_inert = Stop } + } + } _ -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!" } -- 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) - ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs - -- NB: fundeps generate some wanted equalities, but - -- we don't use their evidence for anything - ; canWanteds wevvars } +doTopReact _inerts _workItem = return NoTopInt \end{code} @@ -1861,19 +1998,10 @@ We are choosing option 2 below but we might consider having a flag as well. Note [New Wanted Superclass Work] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Even in the case of wanted constraints, we add all of its superclasses as -new given work. There are several reasons for this: - a) to minimise error messages; - eg suppose we have wanted (Eq a, Ord a) - then we report only (Ord a) unsoluble - - b) to make the smallest number of constraints when *inferring* a type - (same Eq/Ord example) - - c) for recursive dictionaries we *must* add the superclasses - so that we can use them when solving a sub-problem +Even in the case of wanted constraints, we may add some superclasses +as new given work. The reason is: - d) To allow FD-like improvement for type families. Assume that + To allow FD-like improvement for type families. Assume that we have a class class C a b | a -> b and we have to solve the implication constraint: @@ -1899,7 +2027,11 @@ new given work. There are several reasons for this: equalities that have a touchable in their RHS, *in addition* to solving wanted equalities. -Here is another example where this is useful. +We also need to somehow use the superclasses to quantify over a minimal, +constraint see note [Minimize by Superclasses] in TcSimplify. + + +Finally, here is another example where this is useful. Example 1: ---------- @@ -1937,21 +2069,29 @@ NB: The desugarer needs be more clever to deal with equalities that participate in recursive dictionary bindings. \begin{code} - - data LookupInstResult = NoInstance | GenInst [WantedEvVar] EvTerm -matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult -matchClassInst clas tys loc +matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult +matchClassInst inerts clas tys loc = do { let pred = mkClassPred clas tys ; mb_result <- matchClass clas tys + ; untch <- getUntouchables ; case mb_result of MatchInstNo -> return NoInstance - MatchInstMany -> return NoInstance -- defer any reactions of a multitude until + MatchInstMany -> return NoInstance -- defer any reactions of a multitude until -- we learn more about the reagent - MatchInstSingle (dfun_id, mb_inst_tys) -> + MatchInstSingle (_,_) + | given_overlap untch -> + do { traceTcS "Delaying instance application" $ + 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] + } + + MatchInstSingle (dfun_id, mb_inst_tys) -> do { checkWellStagedDFun pred dfun_id loc -- It's possible that not all the tyvars are in @@ -1960,15 +2100,104 @@ matchClassInst clas tys loc -- (presumably there's a functional dependency in class C) -- Hence mb_inst_tys :: Either TyVar TcType - ; tys <- instDFunTypes mb_inst_tys + ; tys <- instDFunTypes mb_inst_tys ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys) ; if null theta then - return (GenInst [] (EvDFunApp dfun_id tys [] [])) + return (GenInst [] (EvDFunApp dfun_id tys [])) else do { ev_vars <- instDFunConstraints theta - ; let wevs = [WantedEvVar w loc | w <- ev_vars] - ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars ev_vars) } - -- NB: All the dependencies are ev_vars + ; let wevs = [EvVarX w loc | w <- ev_vars] + ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) } } } + where given_overlap :: TcsUntouchables -> Bool + given_overlap untch + = foldlBag (\r d -> r || matchable untch d) False all_given_dicts + + matchable untch (CDictCan { cc_class = clas', cc_tyargs = sys, cc_flavor = fl }) + | Just GivenOrig <- isGiven_maybe fl + , clas' == clas + , does_not_originate_in_a_silent clas' sys + = case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv && + tv `elemVarSet` tyVarsOfTypes tys + then BindMe else Skolem) tys sys of + -- We can't learn anything more about any variable at this point, so the only + -- cause of overlap can be by an instantiation of a touchable unification + -- variable. Hence we only bind touchable unification variables. In addition, + -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions. + Nothing -> False + Just _ -> True + | otherwise = False -- No overlap with a solved, already been taken care of + -- by the overlap check with the instance environment. + matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct) + + does_not_originate_in_a_silent clas sys + -- UGLY: See Note [Silent parameters overlapping] + = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs + + silents_and_their_scs + = foldlBag (\acc rvnt -> case rvnt of + CDictCan { cc_id = d, cc_class = c, cc_tyargs = s } + | isSilentEvVar d -> (ClassP c s) : (transSuperClasses c s) ++ acc + _ -> acc) [] all_given_dicts + + -- TODO: + -- When silent parameters will go away we should simply select from + -- the given map of the inert set. + all_given_dicts = Map.fold unionBags emptyCCan (cts_given $ inert_dicts inerts) + \end{code} + +Note [Silent parameters overlapping] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +DV 12/05/2011: +The long-term goal is to completely remove silent superclass +parameters when checking instance declarations. But until then we must +make sure that we never prevent the application of an instance +declaration because of a potential match from a silent parameter -- +after all we are supposed to have solved that silent parameter from +some instance, anyway! In effect silent parameters behave more like +Solved than like Given. + +A concrete example appears in typecheck/SilentParametersOverlapping.hs + +Note [Instance and Given overlap] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Assume that we have an inert set that looks as follows: + [Given] D [Int] +And an instance declaration: + instance C a => D [a] +A new wanted comes along of the form: + [Wanted] D [alpha] + +One possibility is to apply the instance declaration which will leave us +with an unsolvable goal (C alpha). However, later on a new constraint may +arise (for instance due to a functional dependency between two later dictionaries), +that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha]) +will be transformed to [Wanted] D [Int], which could have been discharged by the given. + +The solution is that in matchClassInst and eventually in topReact, we get back with +a matching instance, only when there is no Given in the inerts which is unifiable to +this particular dictionary. + +The end effect is that, much as we do for overlapping instances, we delay choosing a +class instance if there is a possibility of another instance OR a given to match our +constraint later on. This fixes bugs #4981 and #5002. + +This is arguably not easy to appear in practice due to our aggressive prioritization +of equality solving over other constraints, but it is possible. I've added a test case +in typecheck/should-compile/GivenOverlapping.hs + +Moreover notice that our goals here are different than the goals of the top-level +overlapping checks. There we are interested in validating the following principle: + + If we inline a function f at a site where the same global instance environment + is available as the instance environment at the definition site of f then we + should get the same behaviour. + +But for the Given Overlap check our goal is just related to completeness of +constraint solving. + + + +