diff options
Diffstat (limited to 'compiler/typecheck/TcSMonad.hs')
| -rw-r--r-- | compiler/typecheck/TcSMonad.hs | 1233 |
1 files changed, 777 insertions, 456 deletions
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index b5f6554766..db29f67f86 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -5,7 +5,7 @@ module TcSMonad ( -- The work list WorkList(..), isEmptyWorkList, emptyWorkList, - extendWorkListNonEq, extendWorkListCt, extendWorkListDerived, + extendWorkListNonEq, extendWorkListCt, extendWorkListCts, extendWorkListEq, extendWorkListFunEq, appendWorkList, extendWorkListImplic, selectNextWorkItem, @@ -16,9 +16,13 @@ module TcSMonad ( TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, failTcS, warnTcS, addErrTcS, runTcSEqualities, - nestTcS, nestImplicTcS, setEvBindsTcS, buildImplication, + nestTcS, nestImplicTcS, setEvBindsTcS, + checkConstraintsTcS, checkTvConstraintsTcS, runTcPluginTcS, addUsedGRE, addUsedGREs, + matchGlobalInst, TcM.ClsInstResult(..), + + QCInst(..), -- Tracing etc panicTcS, traceTcS, @@ -26,25 +30,25 @@ module TcSMonad ( wrapErrTcS, wrapWarnTcS, -- Evidence creation and transformation - MaybeNew(..), freshGoals, isFresh, getEvTerm, + MaybeNew(..), freshGoals, isFresh, getEvExpr, - newTcEvBinds, + newTcEvBinds, newNoTcEvBinds, newWantedEq, emitNewWantedEq, newWanted, newWantedEvVar, newWantedNC, newWantedEvVarNC, newDerivedNC, newBoundEvVarId, unifyTyVar, unflattenFmv, reportUnifications, - setEvBind, setWantedEq, setEqIfWanted, - setWantedEvTerm, setWantedEvBind, setEvBindIfWanted, + setEvBind, setWantedEq, + setWantedEvTerm, setEvBindIfWanted, newEvVar, newGivenEvVar, newGivenEvVars, - emitNewDerived, emitNewDeriveds, emitNewDerivedEq, + emitNewDeriveds, emitNewDerivedEq, checkReductionDepth, + getSolvedDicts, setSolvedDicts, getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getLclEnv, getTcEvBindsVar, getTcLevel, - getTcEvBindsAndTCVs, getTcEvBindsMap, - tcLookupClass, - tcLookupId, + getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap, + tcLookupClass, tcLookupId, -- Inerts InertSet(..), InertCans(..), @@ -53,11 +57,11 @@ module TcSMonad ( getInertEqs, getInertCans, getInertGivens, getInertInsols, getTcSInerts, setTcSInerts, - matchableGivens, prohibitedSuperClassSolve, + matchableGivens, prohibitedSuperClassSolve, mightMatchLater, getUnsolvedInerts, - removeInertCts, getPendingScDicts, - addInertCan, addInertEq, insertFunEq, - emitInsoluble, emitWorkNC, emitWork, + removeInertCts, getPendingGivenScs, + addInertCan, insertFunEq, addInertForAll, + emitWorkNC, emitWork, isImprovable, -- The Model @@ -83,6 +87,7 @@ module TcSMonad ( -- The flattening cache lookupFlatCache, extendFlatCache, newFlattenSkolem, -- Flatten skolems + dischargeFunEq, pprKicked, -- Inert CFunEqCans updInertFunEqs, findFunEq, @@ -93,16 +98,17 @@ module TcSMonad ( -- MetaTyVars newFlexiTcSTy, instFlexi, instFlexiX, cloneMetaTyVar, demoteUnfilledFmv, - tcInstType, tcInstSkolTyVarsX, + tcInstSkolTyVarsX, - TcLevel, isTouchableMetaTyVarTcS, + TcLevel, isFilledMetaTyVar_maybe, isFilledMetaTyVar, zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo, zonkTyCoVarsAndFVList, zonkSimples, zonkWC, + zonkTcTyCoVarBndr, -- References - newTcRef, readTcRef, updTcRef, + newTcRef, readTcRef, writeTcRef, updTcRef, -- Misc getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS, @@ -117,6 +123,8 @@ module TcSMonad ( #include "HsVersions.h" +import GhcPrelude + import HscTypes import qualified Inst as TcM @@ -126,13 +134,16 @@ import FamInstEnv import qualified TcRnMonad as TcM import qualified TcMType as TcM +import qualified ClsInst as TcM( matchGlobalInst, ClsInstResult(..) ) import qualified TcEnv as TcM - ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass, tcLookupId ) + ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl ) import PrelNames( heqTyConKey, eqTyConKey ) +import ClsInst( InstanceWhat(..) ) import Kind import TcType import DynFlags import Type +import TyCoRep( coHoleCoVar ) import Coercion import Unify @@ -142,6 +153,7 @@ import TyCon import TcErrors ( solverDepthErrorTcS ) import Name +import Module ( HasModule, getModule ) import RdrName ( GlobalRdrEnv, GlobalRdrElt ) import qualified RnEnv as TcM import Var @@ -158,14 +170,12 @@ import UniqFM import UniqDFM import Maybes -import TrieMap +import CoreMap import Control.Monad -#if __GLASGOW_HASKELL__ > 710 import qualified Control.Monad.Fail as MonadFail -#endif import MonadUtils import Data.IORef -import Data.List ( foldl', partition ) +import Data.List ( foldl', partition, mapAccumL ) #if defined(DEBUG) import Digraph @@ -189,16 +199,44 @@ Notice that each Ct now has a simplification depth. We may consider using this depth for prioritization as well in the future. As a simple form of priority queue, our worklist separates out -equalities (wl_eqs) from the rest of the canonical constraints, -so that it's easier to deal with them first, but the separation -is not strictly necessary. Notice that non-canonical constraints -are also parts of the worklist. -Note [Process derived items last] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We can often solve all goals without processing *any* derived constraints. -The derived constraints are just there to help us if we get stuck. So -we keep them in a separate list. +* equalities (wl_eqs); see Note [Prioritise equalities] +* type-function equalities (wl_funeqs) +* all the rest (wl_rest) + +Note [Prioritise equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +It's very important to process equalities /first/: + +* (Efficiency) The general reason to do so is that if we process a + class constraint first, we may end up putting it into the inert set + and then kicking it out later. That's extra work compared to just + doing the equality first. + +* (Avoiding fundep iteration) As Trac #14723 showed, it's possible to + get non-termination if we + - Emit the Derived fundep equalities for a class constraint, + generating some fresh unification variables. + - That leads to some unification + - Which kicks out the class constraint + - Which isn't solved (because there are still some more Derived + equalities in the work-list), but generates yet more fundeps + Solution: prioritise derived equalities over class constraints + +* (Class equalities) We need to prioritise equalities even if they + are hidden inside a class constraint; + see Note [Prioritise class equalities] + +* (Kick-out) We want to apply this priority scheme to kicked-out + constraints too (see the call to extendWorkListCt in kick_out_rewritable + E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become + homo-kinded when kicked out, and hence we want to priotitise it. + +* (Derived equalities) Originally we tried to postpone processing + Derived equalities, in the hope that we might never need to deal + with them at all; but in fact we must process Derived equalities + eagerly, partly for the (Efficiency) reason, and more importantly + for (Avoiding fundep iteration). Note [Prioritise class equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -220,46 +258,50 @@ So we arrange to put these particular class constraints in the wl_eqs. -- See Note [WorkList priorities] data WorkList - = WL { wl_eqs :: [Ct] -- Both equality constraints and their - -- class-level variants (a~b) and (a~~b); - -- See Note [Prioritise class equalities] + = WL { wl_eqs :: [Ct] -- CTyEqCan, CDictCan, CIrredCan + -- Given, Wanted, and Derived + -- Contains both equality constraints and their + -- class-level variants (a~b) and (a~~b); + -- See Note [Prioritise equalities] + -- See Note [Prioritise class equalities] - , wl_funeqs :: [Ct] -- LIFO stack of goals + , wl_funeqs :: [Ct] , wl_rest :: [Ct] - , wl_deriv :: [CtEvidence] -- Implicitly non-canonical - -- See Note [Process derived items last] - , wl_implics :: Bag Implication -- See Note [Residual implications] } appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1 - , wl_deriv = ders1, wl_implics = implics1 }) + , wl_implics = implics1 }) (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2 - , wl_deriv = ders2, wl_implics = implics2 }) + , wl_implics = implics2 }) = WL { wl_eqs = eqs1 ++ eqs2 , wl_funeqs = funeqs1 ++ funeqs2 , wl_rest = rest1 ++ rest2 - , wl_deriv = ders1 ++ ders2 , wl_implics = implics1 `unionBags` implics2 } workListSize :: WorkList -> Int -workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest = rest }) - = length eqs + length funeqs + length rest + length ders +workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest }) + = length eqs + length funeqs + length rest workListWantedCount :: WorkList -> Int +-- Count the things we need to solve +-- excluding the insolubles (c.f. inert_count) workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest }) - = count isWantedCt eqs + count isWantedCt rest + = count isWantedCt eqs + count is_wanted rest + where + is_wanted ct + | CIrredCan { cc_ev = ev, cc_insol = insol } <- ct + = not insol && isWanted ev + | otherwise + = isWantedCt ct extendWorkListEq :: Ct -> WorkList -> WorkList extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl } -extendWorkListEqs :: [Ct] -> WorkList -> WorkList -extendWorkListEqs cts wl = wl { wl_eqs = cts ++ wl_eqs wl } - extendWorkListFunEq :: Ct -> WorkList -> WorkList extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl } @@ -267,15 +309,9 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } -extendWorkListDerived :: CtLoc -> CtEvidence -> WorkList -> WorkList -extendWorkListDerived loc ev wl - | isDroppableDerivedLoc loc = wl { wl_deriv = ev : wl_deriv wl } - | otherwise = extendWorkListEq (mkNonCanonical ev) wl - -extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList -extendWorkListDeriveds loc evs wl - | isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl } - | otherwise = extendWorkListEqs (map mkNonCanonical evs) wl +extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList +extendWorkListDeriveds evs wl + = extendWorkListCts (map mkNonCanonical evs) wl extendWorkListImplic :: Bag Implication -> WorkList -> WorkList extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl } @@ -305,14 +341,15 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts isEmptyWorkList :: WorkList -> Bool isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs - , wl_rest = rest, wl_deriv = ders, wl_implics = implics }) - = null eqs && null rest && null funeqs && isEmptyBag implics && null ders + , wl_rest = rest, wl_implics = implics }) + = null eqs && null rest && null funeqs && isEmptyBag implics emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs = [], wl_rest = [] - , wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag } + , wl_funeqs = [], wl_implics = emptyBag } selectWorkItem :: WorkList -> Maybe (Ct, WorkList) +-- See Note [Prioritise equalities] selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs , wl_rest = rest }) | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts }) @@ -324,36 +361,24 @@ getWorkList :: TcS WorkList getWorkList = do { wl_var <- getTcSWorkListRef ; wrapTcS (TcM.readTcRef wl_var) } -selectDerivedWorkItem :: WorkList -> Maybe (Ct, WorkList) -selectDerivedWorkItem wl@(WL { wl_deriv = ders }) - | ev:evs <- ders = Just (mkNonCanonical ev, wl { wl_deriv = evs }) - | otherwise = Nothing - selectNextWorkItem :: TcS (Maybe Ct) +-- Pick which work item to do next +-- See Note [Prioritise equalities] selectNextWorkItem = do { wl_var <- getTcSWorkListRef - ; wl <- wrapTcS (TcM.readTcRef wl_var) - - ; let try :: Maybe (Ct,WorkList) -> TcS (Maybe Ct) -> TcS (Maybe Ct) - try mb_work do_this_if_fail - | Just (ct, new_wl) <- mb_work - = do { checkReductionDepth (ctLoc ct) (ctPred ct) - ; wrapTcS (TcM.writeTcRef wl_var new_wl) - ; return (Just ct) } - | otherwise - = do_this_if_fail - - ; try (selectWorkItem wl) $ - - do { ics <- getInertCans - ; if inert_count ics == 0 - then return Nothing - else try (selectDerivedWorkItem wl) (return Nothing) } } + ; wl <- readTcRef wl_var + ; case selectWorkItem wl of { + Nothing -> return Nothing ; + Just (ct, new_wl) -> + do { -- checkReductionDepth (ctLoc ct) (ctPred ct) + -- This is done by TcInteract.chooseInstance + ; writeTcRef wl_var new_wl + ; return (Just ct) } } } -- Pretty printing instance Outputable WorkList where ppr (WL { wl_eqs = eqs, wl_funeqs = feqs - , wl_rest = rest, wl_implics = implics, wl_deriv = ders }) + , wl_rest = rest, wl_implics = implics }) = text "WL" <+> (braces $ vcat [ ppUnless (null eqs) $ text "Eqs =" <+> vcat (map ppr eqs) @@ -361,13 +386,9 @@ instance Outputable WorkList where text "Funeqs =" <+> vcat (map ppr feqs) , ppUnless (null rest) $ text "Non-eqs =" <+> vcat (map ppr rest) - , ppUnless (null ders) $ - text "Derived =" <+> vcat (map ppr ders) , ppUnless (isEmptyBag implics) $ - sdocWithPprDebug $ \dbg -> - if dbg -- Typically we only want the work list for this level - then text "Implics =" <+> vcat (map ppr (bagToList implics)) - else text "(Implics omitted)" + ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics))) + (text "(Implics omitted)") ]) @@ -409,30 +430,38 @@ data InertSet -- NB: An ExactFunEqMap -- this doesn't match via loose types! , inert_solved_dicts :: DictMap CtEvidence - -- Of form ev :: C t1 .. tn + -- All Wanteds, of form ev :: C t1 .. tn -- See Note [Solved dictionaries] -- and Note [Do not add superclasses of solved dictionaries] } instance Outputable InertSet where - ppr is = vcat [ ppr $ inert_cans is - , ppUnless (null dicts) $ - text "Solved dicts" <+> vcat (map ppr dicts) ] + ppr (IS { inert_cans = ics + , inert_fsks = ifsks + , inert_solved_dicts = solved_dicts }) + = vcat [ ppr ics + , text "Inert fsks =" <+> ppr ifsks + , ppUnless (null dicts) $ + text "Solved dicts =" <+> vcat (map ppr dicts) ] where - dicts = bagToList (dictsToBag (inert_solved_dicts is)) + dicts = bagToList (dictsToBag solved_dicts) + +emptyInertCans :: InertCans +emptyInertCans + = IC { inert_count = 0 + , inert_eqs = emptyDVarEnv + , inert_dicts = emptyDicts + , inert_safehask = emptyDicts + , inert_funeqs = emptyFunEqs + , inert_insts = [] + , inert_irreds = emptyCts } emptyInert :: InertSet emptyInert - = IS { inert_cans = IC { inert_count = 0 - , inert_eqs = emptyDVarEnv - , inert_dicts = emptyDicts - , inert_safehask = emptyDicts - , inert_funeqs = emptyFunEqs - , inert_irreds = emptyCts - , inert_insols = emptyCts } - , inert_flat_cache = emptyExactFunEqs - , inert_fsks = [] - , inert_solved_dicts = emptyDictMap } + = IS { inert_cans = emptyInertCans + , inert_fsks = [] + , inert_flat_cache = emptyExactFunEqs + , inert_solved_dicts = emptyDictMap } {- Note [Solved dictionaries] @@ -459,8 +488,16 @@ Other notes about solved dictionaries * See also Note [Do not add superclasses of solved dictionaries] -* The inert_solved_dicts field is not rewritten by equalities, so it may - get out of date. +* The inert_solved_dicts field is not rewritten by equalities, + so it may get out of date. + +* THe inert_solved_dicts are all Wanteds, never givens + +* We only cache dictionaries from top-level instances, not from + local quantified constraints. Reason: if we cached the latter + we'd need to purge the cache when bringing new quantified + constraints into scope, because quantified constraints "shadow" + top-level instances. Note [Do not add superclasses of solved dictionaries] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -621,6 +658,8 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more -- All fully rewritten (modulo flavour constraints) -- wrt inert_eqs + , inert_insts :: [QCInst] + , inert_safehask :: DictMap Ct -- Failed dictionary resolution due to Safe Haskell overlapping -- instances restriction. We keep this separate from inert_dicts @@ -631,16 +670,15 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more -- in TcSimplify , inert_irreds :: Cts - -- Irreducible predicates - - , inert_insols :: Cts - -- Frozen errors (as non-canonicals) + -- Irreducible predicates that cannot be made canonical, + -- and which don't interact with others (e.g. (c a)) + -- and insoluble predicates (e.g. Int ~ Bool, or a ~ [a]) , inert_count :: Int -- Number of Wanted goals in -- inert_eqs, inert_dicts, inert_safehask, inert_irreds -- Does not include insolubles - -- When non-zero, keep trying to solved + -- When non-zero, keep trying to solve } type InertEqs = DTyVarEnv EqualCtList @@ -779,36 +817,38 @@ guarantee that this recursive use will terminate. Note [Extending the inert equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Theorem [Stability under extension] - This is the main theorem! +Main Theorem [Stability under extension] Suppose we have a "work item" a -fw-> t and an inert generalised substitution S, - such that + THEN the extended substitution T = S+(a -fw-> t) + is an inert generalised substitution + PROVIDED (T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_) (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_) (T3) a not in t -- No occurs check in the work item - (K1) for every (a -fs-> s) in S, then not (fw >= fs) - Reason: the work item is fully rewritten by S, hence not (fs >= fw) - but if (fw >= fs) then the work item could rewrite - the inert item + AND, for every (b -fs-> s) in S: + (K0) not (fw >= fs) + Reason: suppose we kick out (a -fs-> s), + and add (a -fw-> t) to the inert set. + The latter can't rewrite the former, + so the kick-out achieved nothing - (K2) for every (b -fs-> s) in S, where b /= a, then - (K2a) not (fs >= fs) - or (K2b) fs >= fw - or (K2c) not (fw >= fs) - or (K2d) a not in s + OR { (K1) not (a = b) + Reason: if fw >= fs, WF1 says we can't have both + a -fw-> t and a -fs-> s - (K3) See Note [K3: completeness of solving] - If (b -fs-> s) is in S with (fw >= fs), then - (K3a) If the role of fs is nominal: s /= a - (K3b) If the role of fs is representational: EITHER - a not in s, OR - the path from the top of s to a includes at least one non-newtype + AND (K2): guarantees inertness of the new substitution + { (K2a) not (fs >= fs) + OR (K2b) fs >= fw + OR (K2d) a not in s } + + AND (K3) See Note [K3: completeness of solving] + { (K3a) If the role of fs is nominal: s /= a + (K3b) If the role of fs is representational: + s is not of form (a t1 .. tn) } } - then the extended substitution T = S+(a -fw-> t) - is an inert generalised substitution. Conditions (T1-T3) are established by the canonicaliser Conditions (K1-K3) are established by TcSMonad.kickOutRewritable @@ -836,11 +876,12 @@ The idea is that us to kick out an inert wanted that mentions a, because of (K2a). This is a common case, hence good not to kick out. -* Lemma (L2): if not (fw >= fw), then K1-K3 all hold. +* Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing Proof: using Definition [Can-rewrite relation], fw can't rewrite anything - and so K1-K3 hold. Intuitively, since fw can't rewrite anything, + and so K0 holds. Intuitively, since fw can't rewrite anything, adding it cannot cause any loops This is a common case, because Wanteds cannot rewrite Wanteds. + It's used to avoid even looking for constraint to kick out. * Lemma (L1): The conditions of the Main Theorem imply that there is no (a -fs-> t) in S, s.t. (fs >= fw). @@ -853,9 +894,9 @@ The idea is that - (T3) guarantees (WF2). * (K2) is about inertness. Intuitively, any infinite chain T^0(f,t), - T^1(f,t), T^2(f,T).... must pass through the new work item infnitely + T^1(f,t), T^2(f,T).... must pass through the new work item infinitely often, since the substitution without the work item is inert; and must - pass through at least one of the triples in S infnitely often. + pass through at least one of the triples in S infinitely often. - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f), and hence this triple never plays a role in application S(f,a). @@ -864,7 +905,7 @@ The idea is that (NB: we could strengten K1) in this way too, but see K3. - (K2b): If this holds then, by (T2), b is not in t. So applying the - work item does not genenerate any new opportunities for applying S + work item does not generate any new opportunities for applying S - (K2c): If this holds, we can't pass through this triple infinitely often, because if we did then fs>=f, fw>=f, hence by (R2) @@ -917,26 +958,35 @@ is somewhat accidental. When considering roles, we also need the second clause (K3b). Consider - inert-item a -W/R-> b c work-item c -G/N-> a + inert-item a -W/R-> b c The work-item doesn't get rewritten by the inert, because (>=) doesn't hold. -We've satisfied conditions (T1)-(T3) and (K1) and (K2). If all we had were -condition (K3a), then we would keep the inert around and add the work item. -But then, consider if we hit the following: - - work-item2 b -G/N-> Id +But we don't kick out the inert item because not (W/R >= W/R). So we just +add the work item. But then, consider if we hit the following: + work-item b -G/N-> Id + inert-items a -W/R-> b c + c -G/N-> a where - newtype Id x = Id x For similar reasons, if we only had (K3a), we wouldn't kick the representational inert out. And then, we'd miss solving the inert, which -now reduced to reflexivity. The solution here is to kick out representational -inerts whenever the tyvar of a work item is "exposed", where exposed means -not under some proper data-type constructor, like [] or Maybe. See -isTyVarExposed in TcType. This is encoded in (K3b). +now reduced to reflexivity. + +The solution here is to kick out representational inerts whenever the +tyvar of a work item is "exposed", where exposed means being at the +head of the top-level application chain (a t1 .. tn). See +TcType.isTyVarHead. This is encoded in (K3b). + +Beware: if we make this test succeed too often, we kick out too much, +and the solver might loop. Consider (Trac #14363) + work item: [G] a ~R f b + inert item: [G] b ~R f a +In GHC 8.2 the completeness tests more aggressive, and kicked out +the inert item; but no rewriting happened and there was an infinite +loop. All we need is to have the tyvar at the head. Note [Flavours with roles] ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -966,7 +1016,8 @@ instance Outputable InertCans where ppr (IC { inert_eqs = eqs , inert_funeqs = funeqs, inert_dicts = dicts , inert_safehask = safehask, inert_irreds = irreds - , inert_insols = insols, inert_count = count }) + , inert_insts = insts + , inert_count = count }) = braces $ vcat [ ppUnless (isEmptyDVarEnv eqs) $ text "Equalities:" @@ -979,8 +1030,8 @@ instance Outputable InertCans where text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask) , ppUnless (isEmptyCts irreds) $ text "Irreds =" <+> pprCts irreds - , ppUnless (isEmptyCts insols) $ - text "Insolubles =" <+> pprCts insols + , ppUnless (null insts) $ + text "Given instances =" <+> vcat (map ppr insts) , text "Unsolved goals =" <+> int count ] @@ -1031,7 +1082,7 @@ The same idea is sometimes also called "saturation"; find all the equalities that must hold in any solution. Or, equivalently, you can think of the derived shadows as implementing -the "model": an non-idempotent but no-occurs-check substitution, +the "model": a non-idempotent but no-occurs-check substitution, reflecting *all* *Nominal* equalities (a ~N ty) that are not immediately soluble by unification. @@ -1112,8 +1163,78 @@ work? because even tyvars in the casts and coercions could give an infinite loop if we don't expose it +* CIrredCan: Yes if the inert set can rewrite the constraint. + We used to think splitting irreds was unnecessary, but + see Note [Splitting Irred WD constraints] + * Others: nothing is gained by splitting. +Note [Splitting Irred WD constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Splitting Irred constraints can make a difference. Here is the +scenario: + + a[sk] :: F v -- F is a type family + beta :: alpha + + work item: [WD] a ~ beta + +This is heterogeneous, so we try flattening the kinds. + + co :: F v ~ fmv + [WD] (a |> co) ~ beta + +This is still hetero, so we emit a kind equality and make the work item an +inert Irred. + + work item: [D] fmv ~ alpha + inert: [WD] (a |> co) ~ beta (CIrredCan) + +Can't make progress on the work item. Add to inert set. This kicks out the +old inert, because a [D] can rewrite a [WD]. + + work item: [WD] (a |> co) ~ beta + inert: [D] fmv ~ alpha (CTyEqCan) + +Can't make progress on this work item either (although GHC tries by +decomposing the cast and reflattening... but that doesn't make a difference), +which is still hetero. Emit a new kind equality and add to inert set. But, +critically, we split the Irred. + + work list: + [D] fmv ~ alpha (CTyEqCan) + [D] (a |> co) ~ beta (CIrred) -- this one was split off + inert: + [W] (a |> co) ~ beta + [D] fmv ~ alpha + +We quickly solve the first work item, as it's the same as an inert. + + work item: [D] (a |> co) ~ beta + inert: + [W] (a |> co) ~ beta + [D] fmv ~ alpha + +We decompose the cast, yielding + + [D] a ~ beta + +We then flatten the kinds. The lhs kind is F v, which flattens to fmv which +then rewrites to alpha. + + co' :: F v ~ alpha + [D] (a |> co') ~ beta + +Now this equality is homo-kinded. So we swizzle it around to + + [D] beta ~ (a |> co') + +and set beta := a |> co', and go home happy. + +If we don't split the Irreds, we loop. This is all dangerously subtle. + +This is triggered by test case typecheck/should_compile/SplitWD. + Note [Examples of how Derived shadows helps completeness] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Trac #10009, a very nasty example: @@ -1270,22 +1391,34 @@ shouldSplitWD inert_eqs (CDictCan { cc_tyargs = tys }) -- NB True: ignore coercions -- See Note [Splitting WD constraints] -shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty }) +shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty + , cc_eq_rel = eq_rel }) = tv `elemDVarEnv` inert_eqs - || anyRewritableTyVar False (`elemDVarEnv` inert_eqs) ty + || anyRewritableTyVar False eq_rel (canRewriteTv inert_eqs) ty -- NB False: do not ignore casts and coercions -- See Note [Splitting WD constraints] +shouldSplitWD inert_eqs (CIrredCan { cc_ev = ev }) + = anyRewritableTyVar False (ctEvEqRel ev) (canRewriteTv inert_eqs) (ctEvPred ev) + shouldSplitWD _ _ = False -- No point in splitting otherwise should_split_match_args :: InertEqs -> [TcType] -> Bool -- True if the inert_eqs can rewrite anything in the argument -- types, ignoring casts and coercions should_split_match_args inert_eqs tys - = any (anyRewritableTyVar True (`elemDVarEnv` inert_eqs)) tys + = any (anyRewritableTyVar True NomEq (canRewriteTv inert_eqs)) tys -- NB True: ignore casts coercions -- See Note [Splitting WD constraints] +canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool +canRewriteTv inert_eqs eq_rel tv + | Just (ct : _) <- lookupDVarEnv inert_eqs tv + , CTyEqCan { cc_eq_rel = eq_rel1 } <- ct + = eq_rel1 `eqCanRewrite` eq_rel + | otherwise + = False + isImprovable :: CtEvidence -> Bool -- See Note [Do not do improvement for WOnly] isImprovable (CtWanted { ctev_nosh = WOnly }) = False @@ -1348,6 +1481,45 @@ equalities arising from injectivity. {- ********************************************************************* * * + Inert instances: inert_insts +* * +********************************************************************* -} + +addInertForAll :: QCInst -> TcS () +-- Add a local Given instance, typically arising from a type signature +addInertForAll new_qci + = updInertCans $ \ics -> + ics { inert_insts = add_qci (inert_insts ics) } + where + add_qci :: [QCInst] -> [QCInst] + -- See Note [Do not add duplicate quantified instances] + add_qci qcis | any same_qci qcis = qcis + | otherwise = new_qci : qcis + + same_qci old_qci = tcEqType (ctEvPred (qci_ev old_qci)) + (ctEvPred (qci_ev new_qci)) + +{- Note [Do not add duplicate quantified instances] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this (Trac #15244): + + f :: (C g, D g) => .... + class S g => C g where ... + class S g => D g where ... + class (forall a. Eq a => Eq (g a)) => S g where ... + +Then in f's RHS there are two identical quantified constraints +available, one via the superclasses of C and one via the superclasses +of D. The two are identical, and it seems wrong to reject the program +because of that. But without doing duplicate-elimination we will have +two matching QCInsts when we try to solve constraints arising from f's +RHS. + +The simplest thing is simply to eliminate duplicattes, which we do here. +-} + +{- ********************************************************************* +* * Adding an inert * * ************************************************************************ @@ -1386,50 +1558,43 @@ So in kickOutRewritable we look at all the tyvars of the CFunEqCan, including the fsk. -} -addInertEq :: Ct -> TcS () --- This is a key function, because of the kick-out stuff +addInertCan :: Ct -> TcS () -- Constraints *other than* equalities -- Precondition: item /is/ canonical -- See Note [Adding an equality to the InertCans] -addInertEq ct - = do { traceTcS "addInertEq {" $ - text "Adding new inert equality:" <+> ppr ct - - ; ics <- getInertCans - - ; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev }) <- maybeEmitShadow ics ct - - ; (_, ics1) <- kickOutRewritable (ctEvFlavourRole ev) tv ics - - ; let ics2 = ics1 { inert_eqs = addTyEq (inert_eqs ics1) tv ct - , inert_count = bumpUnsolvedCount ev (inert_count ics1) } - ; setInertCans ics2 - - ; traceTcS "addInertEq }" $ empty } - --------------- -addInertCan :: Ct -> TcS () -- Constraints *other than* equalities addInertCan ct = do { traceTcS "insertInertCan {" $ - text "Trying to insert new non-eq inert item:" <+> ppr ct + text "Trying to insert new inert item:" <+> ppr ct ; ics <- getInertCans - ; ct <- maybeEmitShadow ics ct + ; ct <- maybeEmitShadow ics ct + ; ics <- maybeKickOut ics ct ; setInertCans (add_item ics ct) ; traceTcS "addInertCan }" $ empty } +maybeKickOut :: InertCans -> Ct -> TcS InertCans +-- For a CTyEqCan, kick out any inert that can be rewritten by the CTyEqCan +maybeKickOut ics ct + | CTyEqCan { cc_tyvar = tv, cc_ev = ev, cc_eq_rel = eq_rel } <- ct + = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics + ; return ics' } + | otherwise + = return ics + add_item :: InertCans -> Ct -> InertCans add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys }) = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item } -add_item ics item@(CIrredEvCan { cc_ev = ev }) - = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item +add_item ics item@(CTyEqCan { cc_tyvar = tv, cc_ev = ev }) + = ics { inert_eqs = addTyEq (inert_eqs ics) tv item , inert_count = bumpUnsolvedCount ev (inert_count ics) } - -- The 'False' is because the irreducible constraint might later instantiate - -- to an equality. - -- But since we try to simplify first, if there's a constraint function FC with - -- type instance FC Int = Show - -- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible + +add_item ics@(IC { inert_irreds = irreds, inert_count = count }) + item@(CIrredCan { cc_ev = ev, cc_insol = insoluble }) + = ics { inert_irreds = irreds `Bag.snocBag` item + , inert_count = if insoluble + then count -- inert_count does not include insolubles + else bumpUnsolvedCount ev count } add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys }) = ics { inert_dicts = addDict (inert_dicts ics) cls tys item @@ -1437,9 +1602,8 @@ add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys }) add_item _ item = pprPanic "upd_inert set: can't happen! Inserting " $ - ppr item -- CTyEqCan is dealt with by addInertEq - -- Can't be CNonCanonical, CHoleCan, - -- because they only land in inert_insols + ppr item -- Can't be CNonCanonical, CHoleCan, + -- because they only land in inert_irreds bumpUnsolvedCount :: CtEvidence -> Int -> Int bumpUnsolvedCount ev n | isWanted ev = n+1 @@ -1472,13 +1636,14 @@ kick_out_rewritable :: CtFlavourRole -- Flavour/role of the equality that -> InertCans -> (WorkList, InertCans) -- See Note [kickOutRewritable] -kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs - , inert_dicts = dictmap - , inert_safehask = safehask - , inert_funeqs = funeqmap - , inert_irreds = irreds - , inert_insols = insols - , inert_count = n }) +kick_out_rewritable new_fr new_tv + ics@(IC { inert_eqs = tv_eqs + , inert_dicts = dictmap + , inert_safehask = safehask + , inert_funeqs = funeqmap + , inert_irreds = irreds + , inert_insts = old_insts + , inert_count = n }) | not (new_fr `eqMayRewriteFR` new_fr) = (emptyWorkList, ics) -- If new_fr can't rewrite itself, it can't rewrite @@ -1494,23 +1659,55 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs , inert_safehask = safehask -- ?? , inert_funeqs = feqs_in , inert_irreds = irs_in - , inert_insols = insols_in + , inert_insts = insts_in , inert_count = n - workListWantedCount kicked_out } - kicked_out = WL { wl_eqs = tv_eqs_out - , wl_funeqs = feqs_out - , wl_deriv = [] - , wl_rest = bagToList (dicts_out `andCts` irs_out - `andCts` insols_out) - , wl_implics = emptyBag } + kicked_out :: WorkList + -- NB: use extendWorkList to ensure that kicked-out equalities get priority + -- See Note [Prioritise equality constraints] (Kick-out). + -- The irreds may include non-canonical (hetero-kinded) equality + -- constraints, which perhaps may have become soluble after new_tv + -- is substituted; ditto the dictionaries, which may include (a~b) + -- or (a~~b) constraints. + kicked_out = foldrBag extendWorkListCt + (emptyWorkList { wl_eqs = tv_eqs_out + , wl_funeqs = feqs_out }) + ((dicts_out `andCts` irs_out) + `extendCtsList` insts_out) (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap -- See Note [Kicking out CFunEqCan for fundeps] (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap (irs_out, irs_in) = partitionBag kick_out_ct irreds - (insols_out, insols_in) = partitionBag kick_out_ct insols -- Kick out even insolubles: See Note [Rewrite insolubles] + -- Of course we must kick out irreducibles like (c a), in case + -- we can rewrite 'c' to something more useful + + -- Kick-out for inert instances + -- See Note [Quantified constraints] in TcCanonical + insts_out :: [Ct] + insts_in :: [QCInst] + (insts_out, insts_in) + | fr_may_rewrite (Given, NomEq) -- All the insts are Givens + = partitionWith kick_out_qci old_insts + | otherwise + = ([], old_insts) + kick_out_qci qci + | let ev = qci_ev qci + , fr_can_rewrite_ty NomEq (ctEvPred (qci_ev qci)) + = Left (mkNonCanonical ev) + | otherwise + = Right qci + + (_, new_role) = new_fr + + fr_can_rewrite_ty :: EqRel -> Type -> Bool + fr_can_rewrite_ty role ty = anyRewritableTyVar False role + fr_can_rewrite_tv ty + fr_can_rewrite_tv :: EqRel -> TyVar -> Bool + fr_can_rewrite_tv role tv = new_role `eqCanRewrite` role + && tv == new_tv fr_may_rewrite :: CtFlavourRole -> Bool fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs @@ -1519,9 +1716,9 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs kick_out_ct :: Ct -> Bool -- Kick it out if the new CTyEqCan can rewrite the inert one -- See Note [kickOutRewritable] - kick_out_ct ct | let ev = ctEvidence ct - = fr_may_rewrite (ctEvFlavourRole ev) - && anyRewritableTyVar False (== new_tv) (ctEvPred ev) + kick_out_ct ct | let fs@(_,role) = ctFlavourRole ct + = fr_may_rewrite fs + && fr_can_rewrite_ty role (ctPred ct) -- False: ignore casts and coercions -- NB: this includes the fsk of a CFunEqCan. It can't -- actually be rewritten, but we need to kick it out @@ -1535,33 +1732,34 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs [] -> acc_in (eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in) where - (eqs_in, eqs_out) = partition keep_eq eqs + (eqs_out, eqs_in) = partition kick_out_eq eqs -- Implements criteria K1-K3 in Note [Extending the inert equalities] - keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev - , cc_eq_rel = eq_rel }) - | tv == new_tv - = not (fr_may_rewrite fs) -- (K1) + kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty + , cc_ev = ev, cc_eq_rel = eq_rel }) + | not (fr_may_rewrite fs) + = False -- Keep it in the inert set if the new thing can't rewrite it + + -- Below here (fr_may_rewrite fs) is True + | tv == new_tv = True -- (K1) + | kick_out_for_inertness = True + | kick_out_for_completeness = True + | otherwise = False - | otherwise - = check_k2 && check_k3 where - fs = ctEvFlavourRole ev - check_k2 = not (fs `eqMayRewriteFR` fs) -- (K2a) - || (fs `eqMayRewriteFR` new_fr) -- (K2b) - || not (fr_may_rewrite fs) -- (K2c) - || not (new_tv `elemVarSet` tyCoVarsOfType rhs_ty) -- (K2d) - - check_k3 - | fr_may_rewrite fs + fs = (ctEvFlavour ev, eq_rel) + kick_out_for_inertness + = (fs `eqMayRewriteFR` fs) -- (K2a) + && not (fs `eqMayRewriteFR` new_fr) -- (K2b) + && fr_can_rewrite_ty eq_rel rhs_ty -- (K2d) + -- (K2c) is guaranteed by the first guard of keep_eq + + kick_out_for_completeness = case eq_rel of - NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv) - ReprEq -> not (isTyVarExposed new_tv rhs_ty) + NomEq -> rhs_ty `eqType` mkTyVarTy new_tv + ReprEq -> isTyVarHead new_tv rhs_ty - | otherwise - = True - - keep_eq ct = pprPanic "keep_eq" (ppr ct) + kick_out_eq ct = pprPanic "keep_eq" (ppr ct) kickOutAfterUnification :: TcTyVar -> TcS Int kickOutAfterUnification new_tv @@ -1660,6 +1858,15 @@ addSolvedDict item cls tys ; updInertTcS $ \ ics -> ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } } +getSolvedDicts :: TcS (DictMap CtEvidence) +getSolvedDicts = do { ics <- getTcSInerts; return (inert_solved_dicts ics) } + +setSolvedDicts :: DictMap CtEvidence -> TcS () +setSolvedDicts solved_dicts + = updInertTcS $ \ ics -> + ics { inert_solved_dicts = solved_dicts } + + {- ********************************************************************* * * Other inert-set operations @@ -1717,7 +1924,10 @@ getInertEqs :: TcS (DTyVarEnv EqualCtList) getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) } getInertInsols :: TcS Cts -getInertInsols = do { inert <- getInertCans; return (inert_insols inert) } +-- Returns insoluble equality constraints +-- specifically including Givens +getInertInsols = do { inert <- getInertCans + ; return (filterBag insolubleEqCt (inert_irreds inert)) } getInertGivens :: TcS [Ct] -- Returns the Given constraints in the inert set, @@ -1729,34 +1939,57 @@ getInertGivens $ concat (dVarEnvElts (inert_eqs inerts)) ; return (filter isGivenCt all_cts) } -getPendingScDicts :: TcS [Ct] --- Find all inert Given dictionaries whose cc_pend_sc flag is True --- Set the flag to False in the inert set, and return that Ct -getPendingScDicts = updRetInertCans get_sc_dicts +getPendingGivenScs :: TcS [Ct] +-- Find all inert Given dictionaries, or quantified constraints, +-- whose cc_pend_sc flag is True +-- and that belong to the current level +-- Set their cc_pend_sc flag to False in the inert set, and return that Ct +getPendingGivenScs = do { lvl <- getTcLevel + ; updRetInertCans (get_sc_pending lvl) } + +get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans) +get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) + = ASSERT2( all isGivenCt sc_pending, ppr sc_pending ) + -- When getPendingScDics is called, + -- there are never any Wanteds in the inert set + (sc_pending, ic { inert_dicts = dicts', inert_insts = insts' }) where - get_sc_dicts ic@(IC { inert_dicts = dicts }) - = (sc_pend_dicts, ic') - where - ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts } + sc_pending = sc_pend_insts ++ sc_pend_dicts - sc_pend_dicts :: [Ct] - sc_pend_dicts = foldDicts get_pending dicts [] + sc_pend_dicts = foldDicts get_pending dicts [] + dicts' = foldr add dicts sc_pend_dicts + + (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True -- but flipping the flag get_pending dict dicts - | Just dict' <- isPendingScDict dict = dict' : dicts - | otherwise = dicts + | Just dict' <- isPendingScDict dict + , belongs_to_this_level (ctEvidence dict) + = dict' : dicts + | otherwise + = dicts add :: Ct -> DictMap Ct -> DictMap Ct add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts = addDict dicts cls tys ct add ct _ = pprPanic "getPendingScDicts" (ppr ct) + get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst) + get_pending_inst cts qci@(QCI { qci_ev = ev }) + | Just qci' <- isPendingScInst qci + , belongs_to_this_level ev + = (CQuantCan qci' : cts, qci') + | otherwise + = (cts, qci) + + belongs_to_this_level ev = ctLocLevel (ctEvLoc ev) == this_lvl + -- We only want Givens from this level; see (3a) in + -- Note [The superclass story] in TcCanonical + getUnsolvedInerts :: TcS ( Bag Implication , Cts -- Tyvar eqs: a ~ ty , Cts -- Fun eqs: F a ~ ty - , Cts -- Insoluble , Cts ) -- All others -- Return all the unsolved [Wanted] or [Derived] constraints -- @@ -1768,7 +2001,6 @@ getUnsolvedInerts , inert_funeqs = fun_eqs , inert_irreds = irreds , inert_dicts = idicts - , inert_insols = insols } <- getInertCans ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts @@ -1776,19 +2008,16 @@ getUnsolvedInerts unsolved_irreds = Bag.filterBag is_unsolved irreds unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts unsolved_others = unsolved_irreds `unionBags` unsolved_dicts - unsolved_insols = filterBag is_unsolved insols ; implics <- getWorkListImplics ; traceTcS "getUnsolvedInerts" $ vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs , text "fun eqs =" <+> ppr unsolved_fun_eqs - , text "insols =" <+> ppr unsolved_insols , text "others =" <+> ppr unsolved_others , text "implics =" <+> ppr implics ] - ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs - , unsolved_insols, unsolved_others) } + ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, unsolved_others) } where add_if_unsolved :: Ct -> Cts -> Cts add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts @@ -1799,7 +2028,7 @@ getUnsolvedInerts -- For CFunEqCans we ignore the Derived ones, and keep -- only the Wanteds for flattening. The Derived ones -- share a unification variable with the corresponding - -- Wanted, so we definitely don't want to to participate + -- Wanted, so we definitely don't want to participate -- in unflattening -- See Note [Type family equations] add_if_wanted ct cts | isWantedCt ct = ct `consCts` cts @@ -1821,32 +2050,39 @@ isInInertEqs eqs tv rhs getNoGivenEqs :: TcLevel -- TcLevel of this implication -> [TcTyVar] -- Skolems of this implication -> TcS ( Bool -- True <=> definitely no residual given equalities - , Cts ) -- Insoluble constraints arising from givens + , Cts ) -- Insoluble equalities arising from givens -- See Note [When does an implication have given equalities?] getNoGivenEqs tclvl skol_tvs - = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds - , inert_insols = insols }) + = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = irreds }) <- getInertCans - ; let has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False - (iirreds `unionBags` insols) + ; let has_given_eqs = foldrBag ((||) . ct_given_here) False irreds || anyDVarEnv eqs_given_here ieqs - - ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts - , ppr insols]) + insols = filterBag insolubleEqCt irreds + -- Specifically includes ones that originated in some + -- outer context but were refined to an insoluble by + -- a local equality; so do /not/ add ct_given_here. + + ; traceTcS "getNoGivenEqs" $ + vcat [ if has_given_eqs then text "May have given equalities" + else text "No given equalities" + , text "Skols:" <+> ppr skol_tvs + , text "Inerts:" <+> ppr inerts + , text "Insols:" <+> ppr insols] ; return (not has_given_eqs, insols) } where eqs_given_here :: EqualCtList -> Bool - eqs_given_here [CTyEqCan { cc_tyvar = tv, cc_ev = ev }] + eqs_given_here [ct@(CTyEqCan { cc_tyvar = tv })] -- Givens are always a sigleton - = not (skolem_bound_here tv) && ev_given_here ev + = not (skolem_bound_here tv) && ct_given_here ct eqs_given_here _ = False - ev_given_here :: CtEvidence -> Bool + ct_given_here :: Ct -> Bool -- True for a Given bound by the current implication, -- i.e. the current level - ev_given_here ev - = isGiven ev - && tclvl == ctLocLevel (ctEvLoc ev) + ct_given_here ct = isGiven ev + && tclvl == ctLocLevel (ctEvLoc ev) + where + ev = ctEvidence ct skol_tv_set = mkVarSet skol_tvs skolem_bound_here tv -- See Note [Let-bound skolems] @@ -1859,7 +2095,7 @@ getNoGivenEqs tclvl skol_tvs -- Given might overlap with an instance. See Note [Instance and Given overlap] -- in TcInteract. matchableGivens :: CtLoc -> PredType -> InertSet -> Cts -matchableGivens loc_w pred (IS { inert_cans = inert_cans }) +matchableGivens loc_w pred_w (IS { inert_cans = inert_cans }) = filterBag matchable_given all_relevant_givens where -- just look in class constraints and irreds. matchableGivens does get called @@ -1868,7 +2104,7 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans }) -- non-canonical -- that is, irreducible -- equalities. all_relevant_givens :: Cts all_relevant_givens - | Just (clas, _) <- getClassPredTys_maybe pred + | Just (clas, _) <- getClassPredTys_maybe pred_w = findDictsByClass (inert_dicts inert_cans) clas `unionBags` inert_irreds inert_cans | otherwise @@ -1876,16 +2112,17 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans }) matchable_given :: Ct -> Bool matchable_given ct - | CtGiven { ctev_loc = loc_g } <- ctev - , Just _ <- tcUnifyTys bind_meta_tv [ctEvPred ctev] [pred] - , not (prohibitedSuperClassSolve loc_g loc_w) - = True + | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct + = mightMatchLater pred_g loc_g pred_w loc_w | otherwise = False - where - ctev = cc_ev ct +mightMatchLater :: TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool +mightMatchLater given_pred given_loc wanted_pred wanted_loc + = not (prohibitedSuperClassSolve given_loc wanted_loc) + && isJust (tcUnifyTys bind_meta_tv [given_pred] [wanted_pred]) + where bind_meta_tv :: TcTyVar -> BindFlag -- Any meta tyvar may be unified later, so we treat it as -- bindable when unifying with givens. That ensures that we @@ -1959,7 +2196,7 @@ are some wrinkles: Note [Let-bound skolems] ~~~~~~~~~~~~~~~~~~~~~~~~ If * the inert set contains a canonical Given CTyEqCan (a ~ ty) -and * 'a' is a skolem bound in this very implication, b +and * 'a' is a skolem bound in this very implication, then: a) The Given is pretty much a let-binding, like @@ -1974,6 +2211,10 @@ b) 'a' will have been completely substituted out in the inert set, returned as part of 'fsks' For an example, see Trac #9211. + +See also TcUnify Note [Deeper level on the left] for how we ensure +that the right variable is on the left of the equality when both are +tyvars. -} removeInertCts :: [Ct] -> InertCans -> InertCans @@ -1994,7 +2235,8 @@ removeInertCt is ct = CTyEqCan { cc_tyvar = x, cc_rhs = ty } -> is { inert_eqs = delTyEq (inert_eqs is) x ty } - CIrredEvCan {} -> panic "removeInertCt: CIrredEvCan" + CQuantCan {} -> panic "removeInertCt: CQuantCan" + CIrredCan {} -> panic "removeInertCt: CIrredEvCan" CNonCanonical {} -> panic "removeInertCt: CNonCanonical" CHoleCan {} -> panic "removeInertCt: CHoleCan" @@ -2017,30 +2259,30 @@ lookupFlatCache fam_tc tys lookup_flats flat_cache = findExactFunEq flat_cache fam_tc tys -lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence) +lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence) -- Is this exact predicate type cached in the solved or canonicals of the InertSet? -lookupInInerts pty +lookupInInerts loc pty | ClassPred cls tys <- classifyPredType pty = do { inerts <- getTcSInerts - ; return (lookupSolvedDict inerts cls tys `mplus` - lookupInertDict (inert_cans inerts) cls tys) } + ; return (lookupSolvedDict inerts loc cls tys `mplus` + lookupInertDict (inert_cans inerts) loc cls tys) } | otherwise -- NB: No caching for equalities, IPs, holes, or errors = return Nothing -- | Look up a dictionary inert. NB: the returned 'CtEvidence' might not -- match the input exactly. Note [Use loose types in inert set]. -lookupInertDict :: InertCans -> Class -> [Type] -> Maybe CtEvidence -lookupInertDict (IC { inert_dicts = dicts }) cls tys - = case findDict dicts cls tys of +lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence +lookupInertDict (IC { inert_dicts = dicts }) loc cls tys + = case findDict dicts loc cls tys of Just ct -> Just (ctEvidence ct) _ -> Nothing -- | Look up a solved inert. NB: the returned 'CtEvidence' might not -- match the input exactly. See Note [Use loose types in inert set]. -lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence +lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence -- Returns just if exactly this predicate type exists in the solved. -lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys - = case findDict solved cls tys of +lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys + = case findDict solved loc cls tys of Just ev -> Just ev _ -> Nothing @@ -2067,7 +2309,7 @@ solvable from the other. So, we do lookup in the inert set using loose types, which omit the kind-check. We must be careful when using the result of a lookup because it may -not match the requsted info exactly! +not match the requested info exactly! -} @@ -2127,16 +2369,66 @@ foldTcAppMap k m z = foldUDFM (foldTM k) z m * * ********************************************************************* -} + +{- Note [Tuples hiding implicit parameters] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + f,g :: (?x::Int, C a) => a -> a + f v = let ?x = 4 in g v + +The call to 'g' gives rise to a Wanted constraint (?x::Int, C a). +We must /not/ solve this from the Given (?x::Int, C a), because of +the intervening binding for (?x::Int). Trac #14218. + +We deal with this by arranging that we always fail when looking up a +tuple constraint that hides an implicit parameter. Not that this applies + * both to the inert_dicts (lookupInertDict) + * and to the solved_dicts (looukpSolvedDict) +An alternative would be not to extend these sets with such tuple +constraints, but it seemed more direct to deal with the lookup. + +Note [Solving CallStack constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose f :: HasCallStack => blah. Then + +* Each call to 'f' gives rise to + [W] s1 :: IP "callStack" CallStack -- CtOrigin = OccurrenceOf f + with a CtOrigin that says "OccurrenceOf f". + Remember that HasCallStack is just shorthand for + IP "callStack CallStack + See Note [Overview of implicit CallStacks] in TcEvidence + +* We cannonicalise such constraints, in TcCanonical.canClassNC, by + pushing the call-site info on the stack, and changing the CtOrigin + to record that has been done. + Bind: s1 = pushCallStack <site-info> s2 + [W] s2 :: IP "callStack" CallStack -- CtOrigin = IPOccOrigin + +* Then, and only then, we can solve the constraint from an enclosing + Given. + +So we must be careful /not/ to solve 's1' from the Givens. Again, +we ensure this by arranging that findDict always misses when looking +up souch constraints. +-} + type DictMap a = TcAppMap a emptyDictMap :: DictMap a emptyDictMap = emptyTcAppMap --- sizeDictMap :: DictMap a -> Int --- sizeDictMap m = foldDicts (\ _ x -> x+1) m 0 +findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a +findDict m loc cls tys + | isCTupleClass cls + , any hasIPPred tys -- See Note [Tuples hiding implicit parameters] + = Nothing -findDict :: DictMap a -> Class -> [Type] -> Maybe a -findDict m cls tys = findTcApp m (getUnique cls) tys + | Just {} <- isCallStackPred cls tys + , OccurrenceOf {} <- ctLocOrigin loc + = Nothing -- See Note [Solving CallStack constraints] + + | otherwise + = findTcApp m (getUnique cls) tys findDictsByClass :: DictMap a -> Class -> Bag a findDictsByClass m cls @@ -2295,17 +2587,21 @@ instance Applicative TcS where (<*>) = ap instance Monad TcS where - fail err = TcS (\_ -> fail err) + fail = MonadFail.fail m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs) -#if __GLASGOW_HASKELL__ > 710 instance MonadFail.MonadFail TcS where fail err = TcS (\_ -> fail err) -#endif instance MonadUnique TcS where getUniqueSupplyM = wrapTcS getUniqueSupplyM +instance HasModule TcS where + getModule = wrapTcS getModule + +instance MonadThings TcS where + lookupThing n = wrapTcS (lookupThing n) + -- Basic functionality -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ wrapTcS :: TcM a -> TcS a @@ -2393,7 +2689,7 @@ runTcSDeriveds tcs -- | This can deal only with equality constraints. runTcSEqualities :: TcS a -> TcM a runTcSEqualities thing_inside - = do { ev_binds_var <- TcM.newTcEvBinds + = do { ev_binds_var <- TcM.newNoTcEvBinds ; runTcSWithEvBinds ev_binds_var thing_inside } runTcSWithEvBinds :: EvBindsVar @@ -2468,9 +2764,10 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) , tcs_count = count } -> do { inerts <- TcM.readTcRef old_inert_var - ; let nest_inert = emptyInert { inert_cans = inert_cans inerts - , inert_solved_dicts = inert_solved_dicts inerts } - -- See Note [Do not inherit the flat cache] + ; let nest_inert = emptyInert + { inert_cans = inert_cans inerts + , inert_solved_dicts = inert_solved_dicts inerts } + -- See Note [Do not inherit the flat cache] ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList ; let nest_env = TcSEnv { tcs_ev_binds = ref @@ -2530,44 +2827,81 @@ nestTcS (TcS thing_inside) ; return res } -buildImplication :: SkolemInfo - -> [TcTyVar] -- Skolems - -> [EvVar] -- Givens - -> TcS result - -> TcS (Bag Implication, TcEvBinds, result) --- Just like TcUnify.buildImplication, but in the TcS monnad, --- using the work-list to gather the constraints -buildImplication skol_info skol_tvs givens (TcS thing_inside) - = TcS $ \ env -> - do { new_wl_var <- TcM.newTcRef emptyWorkList - ; tc_lvl <- TcM.getTcLevel - ; let new_tclvl = pushTcLevel tc_lvl - - ; res <- TcM.setTcLevel new_tclvl $ - thing_inside (env { tcs_worklist = new_wl_var }) - - ; wl@WL { wl_eqs = eqs } <- TcM.readTcRef new_wl_var - ; if null eqs - then return (emptyBag, emptyTcEvBinds, res) - else - do { env <- TcM.getLclEnv +checkTvConstraintsTcS :: SkolemInfo + -> [TcTyVar] -- Skolems + -> TcS (result, Cts) + -> TcS result +-- Just like TcUnify.checkTvConstraints, but +-- - In the TcS monnad +-- - The thing-inside should not put things in the work-list +-- Instead, it returns the Wanted constraints it needs +-- - No 'givens', and no TcEvBinds; this is type-level constraints only +checkTvConstraintsTcS skol_info skol_tvs (TcS thing_inside) + = TcS $ \ tcs_env -> + do { let wl_panic = pprPanic "TcSMonad.buildImplication" $ + ppr skol_info $$ ppr skol_tvs + -- This panic checks that the thing-inside + -- does not emit any work-list constraints + new_tcs_env = tcs_env { tcs_worklist = wl_panic } + + ; ((res, wanteds), new_tclvl) <- TcM.pushTcLevelM $ + thing_inside new_tcs_env + + ; unless (null wanteds) $ + do { ev_binds_var <- TcM.newNoTcEvBinds + ; imp <- newImplication + ; let wc = emptyWC { wc_simple = wanteds } + imp' = imp { ic_tclvl = new_tclvl + , ic_skols = skol_tvs + , ic_wanted = wc + , ic_binds = ev_binds_var + , ic_info = skol_info } + + -- Add the implication to the work-list + ; TcM.updTcRef (tcs_worklist tcs_env) + (extendWorkListImplic (unitBag imp')) } + + ; return res } + +checkConstraintsTcS :: SkolemInfo + -> [TcTyVar] -- Skolems + -> [EvVar] -- Givens + -> TcS (result, Cts) + -> TcS (result, TcEvBinds) +-- Just like checkConstraintsTcS, but +-- - In the TcS monnad +-- - The thing-inside should not put things in the work-list +-- Instead, it returns the Wanted constraints it needs +-- - I did not bother to put in the fast-path for +-- empty-skols/empty-givens, or for empty-wanteds, because +-- this function is used only for "quantified constraints" in +-- with both tests are pretty much guaranteed to fail +checkConstraintsTcS skol_info skol_tvs given (TcS thing_inside) + = TcS $ \ tcs_env -> + do { let wl_panic = pprPanic "TcSMonad.buildImplication" $ + ppr skol_info $$ ppr skol_tvs + -- This panic checks that the thing-inside + -- does not emit any work-list constraints + new_tcs_env = tcs_env { tcs_worklist = wl_panic } + + ; ((res, wanteds), new_tclvl) <- TcM.pushTcLevelM $ + thing_inside new_tcs_env + ; ev_binds_var <- TcM.newTcEvBinds - ; let wc = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) && - null (wl_deriv wl) && null (wl_implics wl), ppr wl ) - WC { wc_simple = listToCts eqs - , wc_impl = emptyBag - , wc_insol = emptyCts } - imp = Implic { ic_tclvl = new_tclvl - , ic_skols = skol_tvs - , ic_no_eqs = True - , ic_given = givens - , ic_wanted = wc - , ic_status = IC_Unsolved - , ic_binds = ev_binds_var - , ic_env = env - , ic_needed = emptyVarSet - , ic_info = skol_info } - ; return (unitBag imp, TcEvBinds ev_binds_var, res) } } + ; imp <- newImplication + ; let wc = emptyWC { wc_simple = wanteds } + imp' = imp { ic_tclvl = new_tclvl + , ic_skols = skol_tvs + , ic_given = given + , ic_wanted = wc + , ic_binds = ev_binds_var + , ic_info = skol_info } + + -- Add the implication to the work-list + ; TcM.updTcRef (tcs_worklist tcs_env) + (extendWorkListImplic (unitBag imp')) + + ; return (res, TcEvBinds ev_binds_var) } {- Note [Propagate the solved dictionaries] @@ -2594,23 +2928,21 @@ getTcSWorkListRef :: TcS (IORef WorkList) getTcSWorkListRef = TcS (return . tcs_worklist) getTcSInerts :: TcS InertSet -getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef) +getTcSInerts = getTcSInertsRef >>= readTcRef setTcSInerts :: InertSet -> TcS () -setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) } +setTcSInerts ics = do { r <- getTcSInertsRef; writeTcRef r ics } getWorkListImplics :: TcS (Bag Implication) getWorkListImplics = do { wl_var <- getTcSWorkListRef - ; wl_curr <- wrapTcS (TcM.readTcRef wl_var) + ; wl_curr <- readTcRef wl_var ; return (wl_implics wl_curr) } updWorkListTcS :: (WorkList -> WorkList) -> TcS () updWorkListTcS f = do { wl_var <- getTcSWorkListRef - ; wl_curr <- wrapTcS (TcM.readTcRef wl_var) - ; let new_work = f wl_curr - ; wrapTcS (TcM.writeTcRef wl_var new_work) } + ; updTcRef wl_var f } emitWorkNC :: [CtEvidence] -> TcS () emitWorkNC evs @@ -2624,27 +2956,15 @@ emitWork cts = do { traceTcS "Emitting fresh work" (vcat (map ppr cts)) ; updWorkListTcS (extendWorkListCts cts) } -emitInsoluble :: Ct -> TcS () --- Emits a non-canonical constraint that will stand for a frozen error in the inerts. -emitInsoluble ct - = do { traceTcS "Emit insoluble" (ppr ct $$ pprCtLoc (ctLoc ct)) - ; updInertTcS add_insol } - where - this_pred = ctPred ct - add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) }) - | drop_it = is - | otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } } - where - drop_it = isDroppableDerivedCt ct && - anyBag (tcEqType this_pred . ctPred) old_insols - -- See Note [Do not add duplicate derived insolubles] - newTcRef :: a -> TcS (TcRef a) newTcRef x = wrapTcS (TcM.newTcRef x) readTcRef :: TcRef a -> TcS a readTcRef ref = wrapTcS (TcM.readTcRef ref) +writeTcRef :: TcRef a -> a -> TcS () +writeTcRef ref val = wrapTcS (TcM.writeTcRef ref val) + updTcRef :: TcRef a -> (a->a) -> TcS () updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn) @@ -2654,16 +2974,17 @@ getTcEvBindsVar = TcS (return . tcs_ev_binds) getTcLevel :: TcS TcLevel getTcLevel = wrapTcS TcM.getTcLevel -getTcEvBindsAndTCVs :: EvBindsVar -> TcS (EvBindMap, TyCoVarSet) -getTcEvBindsAndTCVs ev_binds_var - = wrapTcS $ do { bnds <- TcM.getTcEvBindsMap ev_binds_var - ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var - ; return (bnds, tcvs) } +getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet +getTcEvTyCoVars ev_binds_var + = wrapTcS $ TcM.getTcEvTyCoVars ev_binds_var -getTcEvBindsMap :: TcS EvBindMap -getTcEvBindsMap - = do { ev_binds_var <- getTcEvBindsVar - ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var } +getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap +getTcEvBindsMap ev_binds_var + = wrapTcS $ TcM.getTcEvBindsMap ev_binds_var + +setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS () +setTcEvBindsMap ev_binds_var binds + = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds unifyTyVar :: TcTyVar -> TcType -> TcS () -- Unify a meta-tyvar with a type @@ -2726,28 +3047,33 @@ addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS () -checkWellStagedDFun pred dfun_id loc +checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS () +-- Check that we do not try to use an instance before it is available. E.g. +-- instance Eq T where ... +-- f x = $( ... (\(p::T) -> p == p)... ) +-- Here we can't use the equality function from the instance in the splice + +checkWellStagedDFun loc what pred + | TopLevInstance { iw_dfun_id = dfun_id } <- what + , let bind_lvl = TcM.topIdLvl dfun_id + , bind_lvl > impLevel = wrapTcS $ TcM.setCtLocM loc $ do { use_stage <- TcM.getStage ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) } + + | otherwise + = return () -- Fast path for common case where pp_thing = text "instance for" <+> quotes (ppr pred) - bind_lvl = TcM.topIdLvl dfun_id pprEq :: TcType -> TcType -> SDoc pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2 -isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool -isTouchableMetaTyVarTcS tv - = do { tclvl <- getTcLevel - ; return $ isTouchableMetaTyVar tclvl tv } - isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type) isFilledMetaTyVar_maybe tv = case tcTyVarDetails tv of MetaTv { mtv_ref = ref } - -> do { cts <- wrapTcS (TcM.readTcRef ref) + -> do { cts <- readTcRef ref ; case cts of Indirect ty -> return (Just ty) Flexi -> return Nothing } @@ -2780,56 +3106,8 @@ zonkSimples cts = wrapTcS (TcM.zonkSimples cts) zonkWC :: WantedConstraints -> TcS WantedConstraints zonkWC wc = wrapTcS (TcM.zonkWC wc) -{- -Note [Do not add duplicate derived insolubles] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In general we *must* add an insoluble (Int ~ Bool) even if there is -one such there already, because they may come from distinct call -sites. Not only do we want an error message for each, but with --fdefer-type-errors we must generate evidence for each. But for -*derived* insolubles, we only want to report each one once. Why? - -(a) A constraint (C r s t) where r -> s, say, may generate the same fundep - equality many times, as the original constraint is successively rewritten. - -(b) Ditto the successive iterations of the main solver itself, as it traverses - the constraint tree. See example below. - -Also for *given* insolubles we may get repeated errors, as we -repeatedly traverse the constraint tree. These are relatively rare -anyway, so removing duplicates seems ok. (Alternatively we could take -the SrcLoc into account.) - -Note that the test does not need to be particularly efficient because -it is only used if the program has a type error anyway. - -Example of (b): assume a top-level class and instance declaration: - - class D a b | a -> b - instance D [a] [a] - -Assume we have started with an implication: - - forall c. Eq c => { wc_simple = D [c] c [W] } - -which we have simplified to: - - forall c. Eq c => { wc_simple = D [c] c [W] - , wc_insols = (c ~ [c]) [D] } - -For some reason, e.g. because we floated an equality somewhere else, -we might try to re-solve this implication. If we do not do a -dropDerivedWC, then we will end up trying to solve the following -constraints the second time: - - (D [c] c) [W] - (c ~ [c]) [D] - -which will result in two Deriveds to end up in the insoluble set: - - wc_simple = D [c] c [W] - wc_insols = (c ~ [c]) [D], (c ~ [c]) [D] --} +zonkTcTyCoVarBndr :: TcTyCoVar -> TcS TcTyCoVar +zonkTcTyCoVarBndr tv = wrapTcS (TcM.zonkTcTyCoVarBndr tv) {- ********************************************************************* * * @@ -2858,7 +3136,7 @@ newFlattenSkolem flav loc tc xis -- Construct the Refl evidence ; let pred = mkPrimEqPred fam_ty (mkTyVarTy fsk) co = mkNomReflCo fam_ty - ; ev <- newGivenEvVar loc (pred, EvCoercion co) + ; ev <- newGivenEvVar loc (pred, evCoercion co) ; return (ev, co, fsk) } | otherwise -- Generate a [WD] for both Wanted and Derived @@ -2870,7 +3148,7 @@ newFlattenSkolem flav loc tc xis ---------------------------- unflattenGivens :: IORef InertSet -> TcM () -- Unflatten all the fsks created by flattening types in Given --- constraints We must be sure to do this, else we end up with +-- constraints. We must be sure to do this, else we end up with -- flatten-skolems buried in any residual Wanteds -- -- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv) @@ -2881,6 +3159,7 @@ unflattenGivens :: IORef InertSet -> TcM () -- is nicely paired with the creation an empty inert_fsks list. unflattenGivens inert_var = do { inerts <- TcM.readTcRef inert_var + ; TcM.traceTc "unflattenGivens" (ppr (inert_fsks inerts)) ; mapM_ flatten_one (inert_fsks inerts) } where flatten_one (fsk, ty) = TcM.writeMetaTyVar fsk ty @@ -2921,6 +3200,51 @@ demoteUnfilledFmv fmv do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv) ; TcM.writeMetaTyVar fmv tv_ty } } +----------------------------- +dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS () +-- (dischargeFunEq tv co ty) +-- Preconditions +-- - ev :: F tys ~ tv is a CFunEqCan +-- - tv is a FlatMetaTv of FlatSkolTv +-- - co :: F tys ~ xi +-- - fmv/fsk `notElem` xi +-- - fmv not filled (for Wanteds) +-- +-- Then for [W] or [WD], we actually fill in the fmv: +-- set fmv := xi, +-- set ev := co +-- kick out any inert things that are now rewritable +-- +-- For [D], we instead emit an equality that must ultimately hold +-- [D] xi ~ fmv +-- Does not evaluate 'co' if 'ev' is Derived +-- +-- For [G], emit this equality +-- [G] (sym ev; co) :: fsk ~ xi + +-- See TcFlatten Note [The flattening story], +-- especially "Ownership of fsk/fmv" +dischargeFunEq (CtGiven { ctev_evar = old_evar, ctev_loc = loc }) fsk co xi + = do { new_ev <- newGivenEvVar loc ( new_pred, evCoercion new_co ) + ; emitWorkNC [new_ev] } + where + new_pred = mkPrimEqPred (mkTyVarTy fsk) xi + new_co = mkTcSymCo (mkTcCoVarCo old_evar) `mkTcTransCo` co + +dischargeFunEq ev@(CtWanted { ctev_dest = dest }) fmv co xi + = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi ) + do { setWantedEvTerm dest (evCoercion co) + ; unflattenFmv fmv xi + ; n_kicked <- kickOutAfterUnification fmv + ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) } + +dischargeFunEq (CtDerived { ctev_loc = loc }) fmv _co xi + = emitNewDerivedEq loc Nominal xi (mkTyVarTy fmv) + -- FunEqs are always at Nominal role + +pprKicked :: Int -> SDoc +pprKicked 0 = empty +pprKicked n = parens (int n <+> text "kicked out") {- ********************************************************************* * * @@ -2955,14 +3279,15 @@ instFlexiHelper subst tv ; let name = setNameUnique (tyVarName tv) uniq kind = substTyUnchecked subst (tyVarKind tv) ty' = mkTyVarTy (mkTcTyVar name kind details) + ; TcM.traceTc "instFlexi" (ppr ty') ; return (extendTvSubst subst tv ty') } -tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar])) - -- ^ How to instantiate the type variables - -> Id -- ^ Type to instantiate - -> TcS ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result - -- (type vars, preds (incl equalities), rho) -tcInstType inst_tyvars id = wrapTcS (TcM.tcInstType inst_tyvars id) +matchGlobalInst :: DynFlags + -> Bool -- True <=> caller is the short-cut solver + -- See Note [Shortcut solving: overlap] + -> Class -> [Type] -> TcS TcM.ClsInstResult +matchGlobalInst dflags short_cut cls tys + = wrapTcS (TcM.matchGlobalInst dflags short_cut cls tys) tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar]) tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs @@ -2970,7 +3295,7 @@ tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs -- Creating and setting evidence variables and CtFlavors -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -data MaybeNew = Fresh CtEvidence | Cached EvTerm +data MaybeNew = Fresh CtEvidence | Cached EvExpr isFresh :: MaybeNew -> Bool isFresh (Fresh {}) = True @@ -2979,9 +3304,9 @@ isFresh (Cached {}) = False freshGoals :: [MaybeNew] -> [CtEvidence] freshGoals mns = [ ctev | Fresh ctev <- mns ] -getEvTerm :: MaybeNew -> EvTerm -getEvTerm (Fresh ctev) = ctEvTerm ctev -getEvTerm (Cached evt) = evt +getEvExpr :: MaybeNew -> EvExpr +getEvExpr (Fresh ctev) = ctEvExpr ctev +getEvExpr (Cached evt) = evt setEvBind :: EvBind -> TcS () setEvBind ev_bind @@ -2991,7 +3316,8 @@ setEvBind ev_bind -- | Mark variables as used filling a coercion hole useVars :: CoVarSet -> TcS () useVars vars - = do { EvBindsVar { ebv_tcvs = ref } <- getTcEvBindsVar + = do { ev_binds_var <- getTcEvBindsVar + ; let ref = ebv_tcvs ev_binds_var ; wrapTcS $ do { tcvs <- TcM.readTcRef ref ; let tcvs' = tcvs `unionVarSet` vars @@ -3004,32 +3330,32 @@ setWantedEq (HoleDest hole) co ; wrapTcS $ TcM.fillCoercionHole hole co } setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev) --- | Equalities only -setEqIfWanted :: CtEvidence -> Coercion -> TcS () -setEqIfWanted (CtWanted { ctev_dest = dest }) co = setWantedEq dest co -setEqIfWanted _ _ = return () - --- | Good for equalities and non-equalities +-- | Good for both equalities and non-equalities setWantedEvTerm :: TcEvDest -> EvTerm -> TcS () setWantedEvTerm (HoleDest hole) tm - = do { let co = evTermCoercion tm - ; useVars (coVarsOfCo co) + | Just co <- evTermCoercion_maybe tm + = do { useVars (coVarsOfCo co) ; wrapTcS $ TcM.fillCoercionHole hole co } -setWantedEvTerm (EvVarDest ev) tm = setWantedEvBind ev tm + | otherwise + = do { let co_var = coHoleCoVar hole + ; setEvBind (mkWantedEvBind co_var tm) + ; wrapTcS $ TcM.fillCoercionHole hole (mkTcCoVarCo co_var) } -setWantedEvBind :: EvVar -> EvTerm -> TcS () -setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm) +setWantedEvTerm (EvVarDest ev_id) tm + = setEvBind (mkWantedEvBind ev_id tm) setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS () setEvBindIfWanted ev tm = case ev of - CtWanted { ctev_dest = dest } - -> setWantedEvTerm dest tm - _ -> return () + CtWanted { ctev_dest = dest } -> setWantedEvTerm dest tm + _ -> return () newTcEvBinds :: TcS EvBindsVar newTcEvBinds = wrapTcS TcM.newTcEvBinds +newNoTcEvBinds :: TcS EvBindsVar +newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds + newEvVar :: TcPredType -> TcS EvVar newEvVar pred = wrapTcS (TcM.newEvVar pred) @@ -3065,12 +3391,12 @@ emitNewWantedEq loc role ty1 ty2 -- | Make a new equality CtEvidence newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) newWantedEq loc role ty1 ty2 - = do { hole <- wrapTcS $ TcM.newCoercionHole + = do { hole <- wrapTcS $ TcM.newCoercionHole pty ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty) ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole , ctev_nosh = WDeriv , ctev_loc = loc} - , mkHoleCo hole role ty1 ty2 ) } + , mkHoleCo hole ) } where pty = mkPrimEqPredRole role ty1 ty2 @@ -3088,12 +3414,12 @@ newWantedEvVarNC loc pty newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew -- For anything except ClassPred, this is the same as newWantedEvVarNC newWantedEvVar loc pty - = do { mb_ct <- lookupInInerts pty + = do { mb_ct <- lookupInInerts loc pty ; case mb_ct of Just ctev | not (isDerived ctev) -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev - ; return $ Cached (ctEvTerm ctev) } + ; return $ Cached (ctEvExpr ctev) } _ -> do { ctev <- newWantedEvVarNC loc pty ; return (Fresh ctev) } } @@ -3114,12 +3440,6 @@ newWantedNC loc pty | otherwise = newWantedEvVarNC loc pty -emitNewDerived :: CtLoc -> TcPredType -> TcS () -emitNewDerived loc pred - = do { ev <- newDerivedNC loc pred - ; traceTcS "Emitting new derived" (ppr ev) - ; updWorkListTcS (extendWorkListDerived loc ev) } - emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS () emitNewDeriveds loc preds | null preds @@ -3127,7 +3447,7 @@ emitNewDeriveds loc preds | otherwise = do { evs <- mapM (newDerivedNC loc) preds ; traceTcS "Emitting new deriveds" (ppr evs) - ; updWorkListTcS (extendWorkListDeriveds loc evs) } + ; updWorkListTcS (extendWorkListDeriveds evs) } emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS () -- Create new equality Derived and put it in the work list @@ -3135,7 +3455,9 @@ emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS () emitNewDerivedEq loc role ty1 ty2 = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2) ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc) - ; updWorkListTcS (extendWorkListDerived loc ev) } + ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) } + -- Very important: put in the wl_eqs + -- See Note [Prioritise equalities] (Avoiding fundep iteration) newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence newDerivedNC loc pred @@ -3183,4 +3505,3 @@ from which we get the implication (forall a. t1 ~ t2) See TcSMonad.deferTcSForAllEq -} - |