From: dimitris@microsoft.com Date: Mon, 18 Oct 2010 15:15:10 +0000 (+0000) Subject: Major pass through type checker:(1) prioritizing equalities, (2) improved Derived... X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=8657bb00544468adc7ad63e962af71674c3b4500 Major pass through type checker:(1) prioritizing equalities, (2) improved Derived mechanism, (3) bugfixes --- diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index d72fae4..88414d9 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -578,9 +578,8 @@ canEqLeafOriented :: CtFlavor -> CoVar canEqLeafOriented fl cv cls1@(FunCls fn tys) s2 | let k1 = kindAppResult (tyConKind fn) tys, let k2 = typeKind s2, - isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CFunEqCan - = do { kindErrorTcS fl (unClassify cls1) s2 - ; return emptyCCan } + isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CFunEqCan + = kindErrorTcS fl (unClassify cls1) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) ) do { (xis1,ccs1) <- flattenMany fl tys -- flatten type function arguments @@ -596,8 +595,7 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys) s2 -- and then do an occurs check. canEqLeafOriented fl cv (VarCls tv) s2 | isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CTyEqCan - = do { kindErrorTcS fl (mkTyVarTy tv) s2 - ; return emptyCCan } + = kindErrorTcS fl (mkTyVarTy tv) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise = do { (xi2,ccs2) <- flatten fl s2 -- flatten RHS diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs index 1254dd6..572f82c 100644 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@ -644,7 +644,7 @@ warnDefaulting wanteds default_ty %************************************************************************ \begin{code} -kindErrorTcS :: CtFlavor -> TcType -> TcType -> TcS () +kindErrorTcS :: CtFlavor -> TcType -> TcType -> TcS a -- If there's a kind error, we don't want to blindly say "kind error" -- We might, say, be unifying a skolem 'a' with a type 'Int', -- in which case that's the error to report. So we set things @@ -654,7 +654,9 @@ kindErrorTcS fl ty1 ty2 do { let ctxt = CEC { cec_encl = [] , cec_extra = extra , cec_tidy = env0 } - ; reportEqErr ctxt ty1 ty2 } + ; reportEqErr ctxt ty1 ty2 + ; failM + } misMatchErrorTcS :: CtFlavor -> TcType -> TcType -> TcS a misMatchErrorTcS fl ty1 ty2 @@ -719,9 +721,9 @@ flattenForAllErrorTcS fl ty _bad_eqs \begin{code} setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a -setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing -setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing -setCtFlavorLoc (Given loc) thing = setCtLoc loc thing +setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing +setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing +setCtFlavorLoc (Given loc) thing = setCtLoc loc thing wrapEqErrTcS :: CtFlavor -> TcType -> TcType -> (TidyEnv -> TcType -> TcType -> SDoc -> TcM a) @@ -740,10 +742,10 @@ wrapEqErrTcS fl ty1 ty2 thing_inside (ctLocOrigin loc) ty1 ty2 ; thing_inside env3 ty1 ty2 extra } ; case fl of - Wanted loc -> do_wanted loc - Derived loc -> do_wanted loc - Given {} -> thing_inside env2 ty1 ty2 empty - -- We could print more info, but it + Wanted loc -> do_wanted loc + Derived loc _ -> do_wanted loc + Given {} -> thing_inside env2 ty1 ty2 empty + -- We could print more info, but it -- seems to be coming out already } } where diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 0659529..b46a502 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -110,7 +110,7 @@ solving. See Note [Loopy Spontaneous Solving] -- See Note [InertSet invariants] data InertSet - = IS { inert_eqs :: Bag.Bag CanonicalCt -- Equalities only (CTyEqCan,CFunEqCan) + = IS { inert_eqs :: Bag.Bag CanonicalCt -- Equalities only **CTyEqCan** , inert_cts :: Bag.Bag CanonicalCt -- Other constraints , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already -- and reside either in the worklist or in the inerts @@ -147,7 +147,7 @@ updInertSet (IS { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks, inert_fds in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks', inert_fds = fdis } updInertSet (IS { inert_eqs = eqs, inert_cts = cts , inert_fsks = fsks, inert_fds = fdis }) item - | isEqCCan item + | isTyEqCCan item = let eqs' = eqs `Bag.snocBag` item in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks, inert_fds = fdis } | otherwise @@ -158,11 +158,15 @@ updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is } updInertSetFDImprs is Nothing = is -foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a --- Prioritize over the equalities see Note [Prioritizing Equalities] -foldlInertSetM k z (IS { inert_eqs = eqs, inert_cts = cts }) - = do { z' <- Bag.foldlBagM k z eqs - ; Bag.foldlBagM k z' cts } +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 + +foldISOtherCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a +-- Fold over other constraints in the inerts +foldISOtherCtsM k z IS { inert_cts = cts } + = Bag.foldlBagM k z cts extractUnsolved :: InertSet -> (InertSet, CanonicalCts) extractUnsolved is@(IS {inert_eqs = eqs, inert_cts = cts, inert_fds = fdis }) @@ -274,6 +278,10 @@ Note [Basic plan] 2. Pairwise interaction (binary) * Take one from work list * Try all pair-wise interactions with each constraint in inert + + As an optimisation, we prioritize the equalities both in the + worklist and in the inerts. + 3. Try to solve spontaneously for equalities involving touchables 4. Top-level interaction (binary wrt top-level) Superclass decomposition belongs in (4), see note [Superclasses] @@ -295,11 +303,13 @@ unionWorkLists wl1 wl2 = WL { wl_eqs = andCCan (wl_eqs wl1) (wl_eqs wl2) , wl_other = andCCan (wl_other wl1) (wl_other wl2) } -foldlWorkListM :: (Monad m) => (a -> WorkItem -> m a) -> a -> WorkList -> m a --- This fold prioritizes equalities -foldlWorkListM f r wl - = do { r' <- Bag.foldlBagM f r (wl_eqs wl) - ; Bag.foldlBagM f r' (wl_other wl) } +foldWorkListEqCtsM :: Monad m => (a -> WorkItem -> m a) -> a -> WorkList -> m a +-- Fold over the equalities of a worklist +foldWorkListEqCtsM f r wl = Bag.foldlBagM f r (wl_eqs wl) + +foldWorkListOtherCtsM :: Monad m => (a -> WorkItem -> m a) -> a -> WorkList -> m a +-- Fold over non-equality constraints of a worklist +foldWorkListOtherCtsM f r wl = Bag.foldlBagM f r (wl_other wl) isEmptyWorkList :: WorkList -> Bool isEmptyWorkList wl = isEmptyCCan (wl_eqs wl) && isEmptyCCan (wl_other wl) @@ -307,24 +317,18 @@ isEmptyWorkList wl = isEmptyCCan (wl_eqs wl) && isEmptyCCan (wl_other wl) emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs = emptyCCan, wl_other = emptyCCan } -mkEqWorkList :: CanonicalCts -> WorkList --- Precondition: *ALL* equalities -mkEqWorkList eqs = WL { wl_eqs = eqs, wl_other = emptyCCan } - -mkNonEqWorkList :: CanonicalCts -> WorkList --- Precondition: *NO* equalities -mkNonEqWorkList cts = WL { wl_eqs = emptyCCan, wl_other = cts } - workListFromCCans :: CanonicalCts -> WorkList -- Generic, no precondition workListFromCCans cts = WL eqs others - where (eqs, others) = Bag.partitionBag isEqCCan cts + where (eqs, others) = Bag.partitionBag isTyEqCCan cts --- Convenience -singleEqWL :: CanonicalCt -> WorkList -singleNonEqWL :: CanonicalCt -> WorkList -singleEqWL = mkEqWorkList . singleCCan -singleNonEqWL = mkNonEqWorkList . singleCCan +workListFromCCan :: CanonicalCt -> WorkList +workListFromCCan ct | isTyEqCCan ct = WL (singleCCan ct) emptyCCan + | otherwise = WL emptyCCan (singleCCan ct) +-- TODO: +-- At the call sites of workListFromCCan(s), sometimes we know whether the new work +-- involves equalities or not. It's probably a good idea to add specialized calls for +-- those, to avoid asking whether 'isTyEqCCan' all the time. data StopOrContinue @@ -449,7 +453,9 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws vcat [ text "Current depth =" <+> ppr n , text "Max depth =" <+> ppr max_depth ] - ; foldlWorkListM (solveOneWithDepth ctxt) inert ws } + ; is_from_eqs <- foldWorkListEqCtsM (solveOneWithDepth ctxt) inert ws + ; foldWorkListOtherCtsM (solveOneWithDepth ctxt) is_from_eqs ws + } ------------------ -- Fully interact the given work item with an inert set, and return a @@ -473,9 +479,10 @@ solveOneWithDepth (max_depth, n, stack) inert work indent = replicate (2*n) ' ' thePipeline :: [(String,SimplifierStage)] -thePipeline = [ ("interact with inerts", interactWithInertsStage) - , ("spontaneous solve", spontaneousSolveStage) - , ("top-level reactions", topReactionsStage) ] +thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage) + , ("interact with inerts", interactWithInertsStage) + , ("spontaneous solve", spontaneousSolveStage) + , ("top-level reactions", topReactionsStage) ] \end{code} ********************************************************************************* @@ -500,41 +507,6 @@ spontaneousSolveStage workItem inerts , sr_stop = Stop } } -{-- This is all old code, but does not quite work now. The problem is that due to - Note [Loopy Spontaneous Solving] we may have unflattened a type, to be able to - perform a sneaky unification. This unflattening means that we may have to recanonicalize - a given (solved) equality, this is why the result of trySpontaneousSolve is now a list - of constraints (instead of an atomic solved constraint). We would have to react all of - them once again with the worklist but that is very tiresome. Instead we throw them back - in the worklist. - - | isWantedCt workItem - -- Original was wanted we have now made him given so - -- we have to ineract him with the inerts again because - -- of the change in his status. This may produce some work. - -> do { traceTcS "recursive interact with inerts {" $ vcat - [ text "work = " <+> ppr workItem' - , text "inerts = " <+> ppr inerts ] - ; itr_again <- interactWithInertsStage workItem' inerts - ; case sr_stop itr_again of - Stop -> pprPanic "BUG: Impossible to happen" $ - vcat [ text "Original workitem:" <+> ppr workItem - , text "Spontaneously solved:" <+> ppr workItem' - , text "Solved was consumed, when reacting with inerts:" - , nest 2 (ppr inerts) ] - ContinueWith workItem'' -- Now *this* guy is inert wrt to inerts - -> do { traceTcS "end recursive interact }" $ ppr workItem'' - ; return $ SR { sr_new_work = sr_new_work itr_again - , sr_inerts = sr_inerts itr_again - `extendInertSet` workItem'' - , sr_stop = Stop } } - } - | otherwise - -> return $ SR { sr_new_work = emptyWorkList - , sr_inerts = inerts `extendInertSet` workItem' - , sr_stop = Stop } } ---} - -- @trySpontaneousSolve wi@ solves equalities where one side is a -- touchable unification variable. Returns: -- * Nothing if we were not able to solve it @@ -568,29 +540,47 @@ trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS (Maybe SWorkList) -- tv is a MetaTyVar, not untouchable trySpontaneousEqOneWay inerts cv gw tv xi - | not (isSigTyVar tv) || isTyVarTy xi, - typeKind xi `isSubKind` tyVarKind tv - = solveWithIdentity inerts cv gw tv xi - | otherwise - = return Nothing + | not (isSigTyVar tv) || isTyVarTy xi + = if typeKind xi `isSubKind` tyVarKind tv then + solveWithIdentity inerts cv gw tv xi + else if tyVarKind tv `isSubKind` typeKind xi then + return Nothing -- 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 kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors] + + | otherwise -- Still can't solve, sig tyvar and non-variable rhs + = return Nothing ---------------- trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS (Maybe SWorkList) --- Both tyvars are *touchable* MetaTyvars --- By the CTyEqCan invariant, k2 `isSubKind` k1 +-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here trySpontaneousEqTwoWay inerts cv gw tv1 tv2 | k1 `isSubKind` k2 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1) | k2 `isSubKind` k1 = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2) - | otherwise = return Nothing + | otherwise -- None is a subkind of the other, but they are both touchable! + = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors] where k1 = tyVarKind tv1 k2 = tyVarKind tv2 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2) \end{code} +Note [Kind errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the wanted problem: + alpha ~ (# Int, Int #) +where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint, +but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay' +simply returns @Nothing@ then that wanted constraint is going to propagate all the way and +get quantified over in inference mode. That's bad because we do know at this point that the +constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails. + +The same applies in canonicalization code in case of kind errors in the givens. Note [Spontaneous solving and kind compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -602,12 +592,14 @@ or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds. 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@. + 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: - Givens from higher-rank, such as: @@ -728,7 +720,7 @@ solveWithIdentity inerts cv gw tv xi Derived {} -> setDerivedCoBind cv co _ -> pprPanic "Can't spontaneously solve *given*" empty -- See Note [Avoid double unifications] - ; return $ Just (mkEqWorkList cts) } + ; return $ Just (workListFromCCans cts) } occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet -> TcTyVar -> TcType -> Maybe (TcType,CoercionI) @@ -861,45 +853,61 @@ noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList data WhichComesFromInert = LeftComesFromInert | RightComesFromInert + --------------------------------------------------- --- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop --- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've --- interacted the WorkItem with the entire InertSet. --- --- Postcondition: the new InertSet in the resulting StageResult is subset --- of the input InertSet. +-- 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 -- We will fold over the equalities + , inert_fsks = Map.empty -- which will generate those two again + , inert_cts = inert_cts inert + , inert_fds = inert_fds inert + } + , sr_new_work = emptyWorkList + , sr_stop = ContinueWith workItem } + +--------------------------------------------------- +-- Interact a single WorkItem with *non-equality* constraints in the inert set. +-- Precondition: equality interactions must have already happened, hence we have +-- to pick up some information from the incoming inert, before folding over the +-- "Other" constraints it contains! interactWithInertsStage :: SimplifierStage interactWithInertsStage workItem inert - = foldlInertSetM interactNext initITR inert + = foldISOtherCtsM interactNext initITR inert where - initITR = SR { sr_inerts = emptyInert { inert_fds = inert_fds inert } -- Pick up the improvements! + initITR = SR { -- Pick up: (1) equations, (2) FD improvements, (3) FlatSkol equiv. classes + sr_inerts = IS { inert_eqs = inert_eqs inert + , inert_cts = emptyCCan + , inert_fds = inert_fds inert + , inert_fsks = inert_fsks inert } , sr_new_work = emptyWorkList , sr_stop = ContinueWith workItem } +interactNext :: StageResult -> AtomicInert -> TcS StageResult +interactNext it inert + | ContinueWith workItem <- sr_stop it + = do { let inerts = sr_inerts it + fdimprs_old = getFDImprovements inerts - 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 + ; 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 = if ir_inert_action ir == KeepInert - then inerts `updInertSet` inert else inerts + -- 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 = if ir_inert_action ir == KeepInert + then inerts `updInertSet` inert else inerts - ; return $ SR { sr_inerts = inerts_new - , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir - , sr_stop = ir_stop ir } } - | otherwise = return $ itrAddInert inert it - - - itrAddInert :: AtomicInert -> StageResult -> StageResult - itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert } + ; return $ SR { sr_inerts = inerts_new + , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir + , sr_stop = ir_stop ir } } + | otherwise = return $ itrAddInert inert it + where itrAddInert :: AtomicInert -> StageResult -> StageResult + itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert } -- Do a single interaction of two constraints. interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult @@ -916,9 +924,9 @@ interactWithInert fdimprs inert workitem -- 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 loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc) - (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc) - _ -> return True + (Wanted loc, Derived {}) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc) + (Derived {}, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc) + _ -> return True ; if is_allowed && rec_ev_ok then doInteractWithInert fdimprs inert workitem @@ -953,16 +961,15 @@ doInteractWithInert fdimprs ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs ; fd_cts <- canWanteds wevvars - ; let fd_work = mkEqWorkList fd_cts + ; let fd_work = workListFromCCans fd_cts -- See Note [Generating extra equalities] ; traceTcS "Checking if improvements existed." (ppr fdimprs) --- ; if isEmptyCCan fd_cts || not (isWanted fl2) || haveBeenImproved fdimprs pty1 pty2 then ; if isEmptyCCan fd_cts || 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` singleNonEqWL workItem) (pty1,pty2) + (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2) } -- See Note [FunDep Reactions] } @@ -974,36 +981,23 @@ doInteractWithInert _fdimprs (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis }) | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes xis - -- substitute for tv in xis. Note that the resulting class - -- constraint is still canonical, since substituting xi-types in - -- xi-types generates xi-types. However, it may no longer be - -- inert with respect to the inert set items we've already seen. - -- For example, consider the inert set - -- - -- D Int (g) - -- a ~g Int - -- - -- and the work item D a (w). D a does not interact with D Int. - -- Next, it does interact with a ~g Int, getting rewritten to D - -- Int (w). But now we must go back through the rest of the inert - -- set again, to find that it can now be discharged by the given D - -- Int instance. - - -- DV: Update to the comment above: - -- This situation can no longer happen, see Note [Prioritizing equalities] - -- so we are good to simply keep going with the rewritten dictionary to rewrite - -- it as much as possible before reaching any other dictionary constraints! - = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis) - ; mkIRContinue rewritten_dict KeepInert emptyWorkList } --- ; mkIRStop KeepInert $ singleNonEqWL rewritten_dict } + = if isDerivedSC wfl then + mkIRStop KeepInert $ emptyWorkList -- See Note [Adding Derived Superclasses] + else 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 } doInteractWithInert _fdimprs (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 (singleNonEqWL rewritten_dict) } + = if isDerivedSC ifl then + mkIRContinue workItem DropInert emptyWorkList -- No need to do any rewriting, + -- see Note [Adding Derived Superclasses] + else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis) + ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. @@ -1014,7 +1008,6 @@ doInteractWithInert _fdimprs , tv `elemVarSet` tyVarsOfType ty = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty) ; mkIRContinue rewritten_ip KeepInert emptyWorkList } --- ; mkIRStop KeepInert (singleNonEqWL rewritten_ip) } doInteractWithInert _fdimprs (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) @@ -1022,7 +1015,7 @@ doInteractWithInert _fdimprs | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfType ty = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty) - ; mkIRContinue workItem DropInert (singleNonEqWL rewritten_ip) } + ; mkIRContinue 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 @@ -1046,7 +1039,7 @@ doInteractWithInert _fdimprs do { co_var <- newWantedCoVar ty1 ty2 ; let flav = Wanted (combineCtLoc ifl wfl) ; cans <- mkCanonical flav co_var - ; mkIRContinue workItem KeepInert (mkEqWorkList cans) } + ; mkIRContinue workItem KeepInert (workListFromCCans cans) } -- Inert: equality, work item: function equality @@ -1065,10 +1058,10 @@ doInteractWithInert _fdimprs | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes args = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) - ; mkIRStop KeepInert (singleEqWL rewritten_funeq) } -- DV: must stop here, because we may no longer be inert after the rewritting. + ; mkIRStop KeepInert (workListFromCCan 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 , cc_tyargs = args, cc_rhs = xi1 }) @@ -1076,7 +1069,7 @@ doInteractWithInert _fdimprs | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfTypes args = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) - ; mkIRContinue workItem DropInert (singleEqWL rewritten_funeq) } + ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) } doInteractWithInert _fdimprs (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 @@ -1085,10 +1078,10 @@ doInteractWithInert _fdimprs , cc_tyargs = args2, cc_rhs = xi2 }) | fl1 `canSolve` fl2 && lhss_match = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert (mkEqWorkList cans) } + ; mkIRStop KeepInert (workListFromCCans cans) } | fl2 `canSolve` fl1 && lhss_match = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert (mkEqWorkList cans) } + ; mkIRContinue workItem DropInert (workListFromCCans cans) } where lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) @@ -1098,19 +1091,19 @@ doInteractWithInert _fdimprs -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) - ; mkIRStop KeepInert (mkEqWorkList cans) } + ; mkIRStop KeepInert (workListFromCCans cans) } | fl2 `canSolve` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert (mkEqWorkList cans) } + ; mkIRContinue workItem DropInert (workListFromCCans 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 (mkEqWorkList rewritten_eq) } + ; mkIRStop KeepInert (workListFromCCans rewritten_eq) } | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) - ; mkIRContinue workItem DropInert (mkEqWorkList rewritten_eq) } + ; mkIRContinue workItem DropInert (workListFromCCans rewritten_eq) } -- Finally, if workitem is a Flatten Equivalence Class constraint and the -- inert is a wanted constraint, even when the workitem cannot rewrite the @@ -1122,7 +1115,7 @@ doInteractWithInert _fdimprs isMetaTyVar tv1, -- and has a unification variable lhs FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2' - = mkIRContinue workItem DropInert (singleEqWL inert) + = mkIRContinue workItem DropInert (workListFromCCan inert) -- Fall-through case for all other situations @@ -1213,7 +1206,7 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts --- Used to ineratct two equalities of the following form: +-- 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 @@ -1695,8 +1688,9 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc -- Solved and new wanted work produced, you may cache the -- (tentatively solved) dictionary as Derived and its superclasses - else do { let solved = makeSolved workItem - ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis + else do { let solved = makeSolvedByInst workItem + ; sc_work <- newDerivedSCWork dv loc cls xis + -- See Note [Adding Derived Superclasses] ; let inst_work = workListFromCCans workList ; return $ SomeTopInt { tir_new_work = inst_work `unionWorkLists` sc_work @@ -1714,17 +1708,18 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc -- NB: fundeps generate some wanted equalities, but -- we don't use their evidence for anything ; fd_cts <- canWanteds wevvars - ; let fd_work = mkEqWorkList fd_cts + ; let fd_work = workListFromCCans fd_cts ; if isEmptyCCan fd_cts then - do { sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis + do { sc_work <- newDerivedSCWork dv loc cls xis + -- See Note [Adding Derived Superclasses] ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work , tir_new_inert = ContinueWith workItem } } else -- More fundep work produced, don't do any superlcass stuff, just -- thow him back in the worklist prioritizing the solution of fd equalities return $ - SomeTopInt { tir_new_work = fd_work `unionWorkLists` singleNonEqWL workItem + SomeTopInt { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem , tir_new_inert = Stop } -- NB: workItem is inert, but it isn't solved @@ -1734,15 +1729,15 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc -- See Note [FunDep Reactions] } --- DV: Derived, we will not add any further derived superclasses --- [no deep recursive dictionaries!] +-- Derived, do not add any further derived superclasses; their full transitive +-- closure has already been added. doTopReact (CDictCan { cc_flavor = fl }) - | isDerived fl - = return NoTopInt + | isDerived fl + = return NoTopInt -doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl - , cc_class = cls, cc_tyargs = xis }) - = do { sc_work <- newSCWorkFromFlavored dv fl cls xis +doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc + , cc_class = cls, cc_tyargs = xis }) + = do { sc_work <- newGivenSCWork dv loc cls xis ; return $ SomeTopInt sc_work (ContinueWith workItem) } -- See Note [Given constraint that matches an instance declaration] @@ -1772,7 +1767,7 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe ; can_cts <- mkCanonical fl cv' - ; let workList = mkEqWorkList can_cts + ; let workList = workListFromCCans can_cts ; return $ SomeTopInt workList Stop } _ -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!" @@ -1783,6 +1778,65 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl doTopReact _workItem = return NoTopInt \end{code} +Note [Adding Derived Superclasses] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Generally speaking, we want to be able to add derived superclasses of +unsolved wanteds, and wanteds that have been partially being solved +via an instance. This is important to be able to simplify the inferred +constraints more (and to allow for recursive dictionaries, less +importantly). Example: + +Inferred wanted constraint is (Eq a, Ord a), but we'd only like to +quantify over Ord a, hence we would like to be able to add the +superclass of Ord a as Derived and use it to solve the wanted Eq a. + +Hence we will add Derived superclasses in the following two cases: + (1) When we meet an unsolved wanted in top-level reactions + (2) When we partially solve a wanted in top-level reactions using an instance decl. + +At that point, we have two options: + (1) Add transitively add *ALL* of the superclasses of the Derived + (2) Add only the immediate ones, but whenever we meet a Derived in + the future, add its own superclasses as Derived. + +Option (2) is terrible, because deriveds may be rewritten or kicked +out of the inert set, which will result in slightly rewritten +superclasses being reintroduced in the worklist and the inert set. Eg: + + class C a => B a + instance Foo a => B [a] + +Original constraints: +[Wanted] d : B [a] +[Given] co : a ~ Int + +We apply the instance to the wanted and put it and its superclasses as +as Deriveds in the inerts: + +[Derived] d : B [a] +[Derived] (sel d) : C [a] + +The work is now: +[Given] co : a ~ Int +[Wanted] d' : Foo a + +Now, suppose that we interact the Derived with the Given equality, and +kick him out of the inert, the next time around a superclass C [Int] +will be produced -- but we already *have* C [a] in the inerts which +will anyway get rewritten to C [Int]. + +So we choose (1), and *never* introduce any more superclass work from +Deriveds. This enables yet another optimisation: If we ever meet an +equality that can rewrite a Derived, if that Derived is a superclass +derived (like C [a] above), i.e. not a partially solved one (like B +[a]) above, we may simply completely *discard* that Derived. The +reason is because somewhere in the inert lies the original wanted, or +partially solved constraint that gave rise to that superclass, and +that constraint *will* be kicked out, and *will* result in the +rewritten superclass to be added in the inerts later on, anyway. + + + Note [FunDep and implicit parameter reactions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Currently, our story of interacting two dictionaries (or a dictionary @@ -1984,25 +2038,42 @@ NB: The desugarer needs be more clever to deal with equalities that participate in recursive dictionary bindings. \begin{code} -newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] - -> TcS WorkList -newSCWorkFromFlavored ev flavor cls xis - | Given loc <- flavor -- The NoScSkol says "don't add superclasses" - , NoScSkol <- ctLocOrigin loc -- Very important! + +newGivenSCWork :: EvVar -> GivenLoc -> Class -> [Xi] -> TcS WorkList +newGivenSCWork ev loc cls xis + | NoScSkol <- ctLocOrigin loc -- Very important! = return emptyWorkList - | otherwise + = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return . workListFromCCans + +newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList +newDerivedSCWork ev loc cls xis + = do { ims <- newImmSCWorkFromFlavored ev flavor cls xis + ; final_cts <- rec_sc_work ims + ; return $ workListFromCCans final_cts } + where rec_sc_work :: CanonicalCts -> TcS CanonicalCts + rec_sc_work cts + = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c + ; recs_ims <- rec_sc_work ims + ; return $ consBag c recs_ims }) cts + ; return $ concatBag bg } + imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis }) + = newImmSCWorkFromFlavored dv fl cls xis + imm_sc_work _ct = return emptyCCan + + flavor = Derived loc DerSC + +newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts +-- Returns immediate superclasses +newImmSCWorkFromFlavored ev flavor cls xis = do { let (tyvars, sc_theta, _, _) = classBigSig cls sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta - -- Add *all* its superclasses (equalities or not) as new given work - -- See Note [New Wanted Superclass Work] ; sc_vars <- zipWithM inst_one sc_theta1 [0..] - ; can_cts <- mkCanonicals flavor sc_vars - ; return $ workListFromCCans can_cts - } + ; mkCanonicals flavor sc_vars } where inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n) + data LookupInstResult = NoInstance | GenInst [WantedEvVar] EvTerm diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 4101a92..5f555c5 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -4,12 +4,14 @@ module TcSMonad ( -- Canonical constraints CanonicalCts, emptyCCan, andCCan, andCCans, - singleCCan, extendCCans, isEmptyCCan, isEqCCan, - CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, + singleCCan, extendCCans, isEmptyCCan, isTyEqCCan, + CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, mkWantedConstraints, deCanonicaliseWanted, - makeGivens, makeSolved, + makeGivens, makeSolvedByInst, - CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, canSolve, + CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst, + DerivedOrig (..), + canRewrite, canSolve, combineCtLoc, mkGivenFlavor, TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality @@ -43,6 +45,7 @@ module TcSMonad ( isGoodRecEv, isTouchableMetaTyVar, + isTouchableMetaTyVar_InRange, getDefaultInfo, getDynFlags, @@ -169,12 +172,12 @@ makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSko -- The UnkSkol doesn't matter because these givens are -- not contradictory (else we'd have rejected them already) -makeSolved :: CanonicalCt -> CanonicalCt +makeSolvedByInst :: CanonicalCt -> CanonicalCt -- Record that a constraint is now solved -- Wanted -> Derived -- Given, Derived -> no-op -makeSolved ct - | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc } +makeSolvedByInst ct + | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst } | otherwise = ct mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints @@ -193,6 +196,13 @@ tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes ( tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty +tyVarsOfCDict :: CanonicalCt -> TcTyVarSet +tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys +tyVarsOfCDict _ct = emptyVarSet + +tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet +tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet + tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet @@ -255,10 +265,10 @@ emptyCCan = emptyBag isEmptyCCan :: CanonicalCts -> Bool isEmptyCCan = isEmptyBag -isEqCCan :: CanonicalCt -> Bool -isEqCCan (CTyEqCan {}) = True -isEqCCan (CFunEqCan {}) = True -isEqCCan _ = False +isTyEqCCan :: CanonicalCt -> Bool +isTyEqCCan (CTyEqCan {}) = True +isTyEqCCan (CFunEqCan {}) = False +isTyEqCCan _ = False \end{code} @@ -272,16 +282,21 @@ isEqCCan _ = False \begin{code} data CtFlavor = Given GivenLoc -- We have evidence for this constraint in TcEvBinds - | Derived WantedLoc -- We have evidence for this constraint in TcEvBinds; + | Derived WantedLoc DerivedOrig + -- We have evidence for this constraint in TcEvBinds; -- *however* this evidence can contain wanteds, so -- it's valid only provisionally to the solution of -- these wanteds | Wanted WantedLoc -- We have no evidence bindings for this constraint. +data DerivedOrig = DerSC | DerInst +-- Deriveds are either superclasses of other wanteds or deriveds, or partially +-- solved wanteds from instances. + instance Outputable CtFlavor where - ppr (Given _) = ptext (sLit "[Given]") - ppr (Wanted _) = ptext (sLit "[Wanted]") - ppr (Derived _) = ptext (sLit "[Derived]") + ppr (Given _) = ptext (sLit "[Given]") + ppr (Wanted _) = ptext (sLit "[Wanted]") + ppr (Derived {}) = ptext (sLit "[Derived]") isWanted :: CtFlavor -> Bool isWanted (Wanted {}) = True @@ -295,6 +310,14 @@ isDerived :: CtFlavor -> Bool isDerived (Derived {}) = True isDerived _ = False +isDerivedSC :: CtFlavor -> Bool +isDerivedSC (Derived _ DerSC) = True +isDerivedSC _ = False + +isDerivedByInst :: CtFlavor -> Bool +isDerivedByInst (Derived _ DerInst) = True +isDerivedByInst _ = False + canSolve :: CtFlavor -> CtFlavor -> Bool -- canSolve ctid1 ctid2 -- The constraint ctid1 can be used to solve ctid2 @@ -317,16 +340,16 @@ canRewrite = canSolve combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc -- Precondition: At least one of them should be wanted -combineCtLoc (Wanted loc) _ = loc -combineCtLoc _ (Wanted loc) = loc -combineCtLoc (Derived loc) _ = loc -combineCtLoc _ (Derived loc) = loc +combineCtLoc (Wanted loc) _ = loc +combineCtLoc _ (Wanted loc) = loc +combineCtLoc (Derived loc _) _ = loc +combineCtLoc _ (Derived loc _) = loc combineCtLoc _ _ = panic "combineCtLoc: both given" mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor -mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) -mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) -mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) \end{code} @@ -585,13 +608,20 @@ pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2) isTouchableMetaTyVar :: TcTyVar -> TcS Bool isTouchableMetaTyVar tv - = case tcTyVarDetails tv of - MetaTv TcsTv _ -> return True -- See Note [Touchable meta type variables] - MetaTv {} -> do { untch <- getUntouchables - ; return (inTouchableRange untch tv) } - _ -> return False + = do { untch <- getUntouchables + ; return $ isTouchableMetaTyVar_InRange untch tv } + +isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool +isTouchableMetaTyVar_InRange untch tv + = case tcTyVarDetails tv of + MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables] + MetaTv {} -> inTouchableRange untch tv + _ -> False + + \end{code} + Note [Touchable meta type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Meta type variables allocated *by the constraint solver itself* are always diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 732f5d5..f0963f7 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -210,8 +210,12 @@ simplifyInfer apply_mr tau_tvs wanted zonked_tau_tvs `minusVarSet` gbl_tvs (perhaps_bound, surely_free) = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted + ; emitConstraints surely_free - ; traceTc "sinf" (ppr proto_qtvs $$ ppr perhaps_bound $$ ppr surely_free) + ; traceTc "sinf" $ vcat + [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound + , ptext (sLit "surely_free =") <+> ppr surely_free + ] -- Now simplify the possibly-bound constraints ; (simplified_perhaps_bound, tc_binds) @@ -808,7 +812,7 @@ applyDefaultingRules inert wanteds | otherwise = do { untch <- getUntouchables ; tv_cts <- mapM (defaultTyVar untch) $ - varSetElems (tyVarsOfCanonicals wanteds) + varSetElems (tyVarsOfCDicts wanteds) ; info@(_, default_tys, _) <- getDefaultInfo ; let groups = findDefaultableGroups info untch wanteds @@ -836,8 +840,7 @@ defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts -- whatever, because the type-class defaulting rules have yet to run. defaultTyVar untch the_tv - | isMetaTyVar the_tv - , inTouchableRange untch the_tv + | isTouchableMetaTyVar_InRange untch the_tv , not (k `eqKind` default_k) = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk @@ -887,7 +890,7 @@ findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) is_defaultable_group ds@((_,tv):_) = isTyConableTyVar tv -- Note [Avoiding spurious errors] && not (tv `elemVarSet` bad_tvs) - && inTouchableRange untch tv + && isTouchableMetaTyVar_InRange untch tv && defaultable_classes [cc_class cc | (cc,_) <- ds] is_defaultable_group [] = panic "defaultable_group"