Commit 13b0b460 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Reorganise the work list, so that flattening goals are treated in the right order

Trac #9872 showed the importance of processing goals in depth-first, so that
we do not build up a huge pool of suspended function calls, waiting for their
children to fire.  There is a detailed explanation in
     Note [The flattening work list]
in TcFlatten

The effect for Trac #9872 (slow1.hs) is dramatic.  We go from too long
to wait down to 28Gbyte allocation.  GHC 7.8.3 did 116Gbyte allocation!
parent b006a1af
......@@ -197,8 +197,7 @@ canClassNC ev cls tys
`andWhenContinue` emitSuperclasses
canClass ev cls tys
= do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
; (xis, cos) <- flattenMany fmode tys
= do { (xis, cos) <- flattenMany FM_FlattenAll ev tys
; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
xi = mkClassPred cls xis
mk_ct new_ev = CDictCan { cc_ev = new_ev
......@@ -332,10 +331,9 @@ canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
-- Precondition: ty not a tuple and no other evidence form
canIrred old_ev
= do { let old_ty = ctEvPred old_ev
fmode = FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }
-- Flatten (F [a]), say, so that it can reduce to Eq a
; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
; (xi,co) <- flatten fmode old_ty -- co :: xi ~ old_ty
; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty
-- Flatten (F [a]), say, so that it can reduce to Eq a
; mb <- rewriteEvidence old_ev xi co
; case mb of {
Stop ev s -> return (Stop ev s) ;
......@@ -351,9 +349,8 @@ canIrred old_ev
canHole :: CtEvidence -> OccName -> HoleSort -> TcS (StopOrContinue Ct)
canHole ev occ hole_sort
= do { let ty = ctEvPred ev
fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly }
; (xi,co) <- flatten fmode ty -- co :: xi ~ ty
= do { let ty = ctEvPred ev
; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
; mb <- rewriteEvidence ev xi co
; case mb of
ContinueWith new_ev -> do { emitInsoluble (CHoleCan { cc_ev = new_ev
......@@ -472,8 +469,7 @@ can_eq_fam_nc :: CtEvidence -> SwapFlag
-- or the swapped version thereof
-- Flatten both sides and go round again
can_eq_fam_nc ev swapped fn tys rhs ps_rhs
= do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
; (xi_lhs, co_lhs) <- flattenFamApp fmode fn tys
= do { (xi_lhs, co_lhs) <- flattenFamApp FM_FlattenAll ev fn tys
; mb_ct <- rewriteEqEvidence ev swapped xi_lhs rhs co_lhs (mkTcNomReflCo rhs)
; case mb_ct of
Stop ev s -> return (Stop ev s)
......@@ -488,9 +484,8 @@ can_eq_wanted_app :: CtEvidence -> TcType -> TcType
-- One or the other is an App; neither is a type variable
-- See Note [Canonicalising type applications]
can_eq_wanted_app ev ty1 ty2
= do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
; (xi1, co1) <- flatten fmode ty1
; (xi2, co2) <- flatten fmode ty2
= do { (xi1, co1) <- flatten FM_FlattenAll ev ty1
; (xi2, co2) <- flatten FM_FlattenAll ev ty2
; mb_ct <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
; case mb_ct of {
Stop ev s -> return (Stop ev s) ;
......@@ -568,9 +563,8 @@ canDecomposableTyConAppOK ev tc1 tys1 tys2
canEqFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct)
-- See Note [Make sure that insolubles are fully rewritten]
canEqFailure ev ty1 ty2
= do { let fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly }
; (s1, co1) <- flatten fmode ty1
; (s2, co2) <- flatten fmode ty2
= do { (s1, co1) <- flatten FM_SubstOnly ev ty1
; (s2, co2) <- flatten FM_SubstOnly ev ty2
; mb_ct <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
; case mb_ct of
ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev)
......@@ -643,8 +637,7 @@ canCFunEqCan :: CtEvidence
-- and the RHS is a fsk, which we must *not* substitute.
-- So just substitute in the LHS
canCFunEqCan ev fn tys fsk
= do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
; (tys', cos) <- flattenMany fmode tys
= do { (tys', cos) <- flattenMany FM_FlattenAll ev tys
-- cos :: tys' ~ tys
; let lhs_co = mkTcTyConAppCo Nominal fn cos
-- :: F tys' ~ F tys
......@@ -683,8 +676,7 @@ canEqTyVar ev swapped tv1 ty2 ps_ty2 -- ev :: tv ~ s2
-- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
-- Flatten the RHS less vigorously, to avoid gratuitous flattening
-- True <=> xi2 should not itself be a type-function application
let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
; (xi2, co2) <- flatten fmode ps_ty2 -- co2 :: xi2 ~ ps_ty2
; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2 -- co2 :: xi2 ~ ps_ty2
-- Use ps_ty2 to preserve type synonyms if poss
; dflags <- getDynFlags
; canEqTyVar2 dflags ev swapped tv1' xi2 co2 } }
......
......@@ -2,7 +2,8 @@
module TcFlatten(
FlattenEnv(..), FlattenMode(..),
flatten, flattenMany, flattenFamApp, flattenTyVarOuter,
flatten, flattenMany, flatten_many,
flattenFamApp, flattenTyVarOuter,
unflatten,
eqCanRewrite, canRewriteOrSame
) where
......@@ -565,7 +566,8 @@ unexpanded synonym.
data FlattenEnv
= FE { fe_mode :: FlattenMode
, fe_ev :: CtEvidence }
, fe_ev :: CtEvidence
}
data FlattenMode -- Postcondition for all three: inert wrt the type substitution
= FM_FlattenAll -- Postcondition: function-free
......@@ -607,45 +609,66 @@ Note: T5321Fun got faster when I disabled FM_Avoid
T5837 did too, but it's pathalogical anyway
-}
------------------
flatten :: FlattenMode -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
flatten mode ev ty
= runFlatten (flatten_one fmode ty)
where
fmode = FE { fe_mode = mode, fe_ev = ev }
flattenMany :: FlattenMode -> CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
-- Flatten a bunch of types all at once.
flattenMany :: FlattenEnv -> [Type] -> TcS ([Xi], [TcCoercion])
flattenMany mode ev tys
= runFlatten (flatten_many fmode tys)
where
fmode = FE { fe_mode = mode, fe_ev = ev }
flattenFamApp :: FlattenMode -> CtEvidence -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
flattenFamApp mode ev tc tys
= runFlatten (flatten_fam_app fmode tc tys)
where
fmode = FE { fe_mode = mode, fe_ev = ev }
------------------
flatten_many :: FlattenEnv -> [Type] -> TcS ([Xi], [TcCoercion])
-- Coercions :: Xi ~ Type
-- Returns True iff (no flattening happened)
-- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused,
-- we merely want (a) Given/Solved/Derived/Wanted info
-- (b) the GivenLoc/WantedLoc for when we create new evidence
flattenMany fmode tys
flatten_many fmode tys
= -- pprTrace "flattenMany" empty $
go tys
where go [] = return ([],[])
go (ty:tys) = do { (xi,co) <- flatten fmode ty
go (ty:tys) = do { (xi,co) <- flatten_one fmode ty
; (xis,cos) <- go tys
; return (xi:xis,co:cos) }
flatten :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion)
------------------
flatten_one :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion)
-- Flatten a type to get rid of type function applications, returning
-- the new type-function-free type, and a collection of new equality
-- constraints. See Note [Flattening] for more detail.
--
-- Postcondition: Coercion :: Xi ~ TcType
flatten _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
flatten_one _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
flatten fmode (TyVarTy tv)
flatten_one fmode (TyVarTy tv)
= flattenTyVar fmode tv
flatten fmode (AppTy ty1 ty2)
= do { (xi1,co1) <- flatten fmode ty1
; (xi2,co2) <- flatten fmode ty2
flatten_one fmode (AppTy ty1 ty2)
= do { (xi1,co1) <- flatten_one fmode ty1
; (xi2,co2) <- flatten_one fmode ty2
; traceTcS "flatten/appty" (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$ ppr co1 $$ ppr xi2 $$ ppr co2)
; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
flatten fmode (FunTy ty1 ty2)
= do { (xi1,co1) <- flatten fmode ty1
; (xi2,co2) <- flatten fmode ty2
flatten_one fmode (FunTy ty1 ty2)
= do { (xi1,co1) <- flatten_one fmode ty1
; (xi2,co2) <- flatten_one fmode ty2
; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
flatten fmode (TyConApp tc tys)
flatten_one fmode (TyConApp tc tys)
-- Expand type synonyms that mention type families
-- on the RHS; see Note [Flattening synonyms]
......@@ -653,7 +676,7 @@ flatten fmode (TyConApp tc tys)
, let expanded_ty = mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys'
= case fe_mode fmode of
FM_FlattenAll | anyNameEnv isTypeFamilyTyCon (tyConsOfType rhs)
-> flatten fmode expanded_ty
-> flatten_one fmode expanded_ty
| otherwise
-> flattenTyConApp fmode tc tys
_ -> flattenTyConApp fmode tc tys
......@@ -662,7 +685,7 @@ flatten fmode (TyConApp tc tys)
-- flatten it away as well, and generate a new given equality constraint
-- between the application and a newly generated flattening skolem variable.
| isTypeFamilyTyCon tc
= flattenFamApp fmode tc tys
= flatten_fam_app fmode tc tys
-- For * a normal data type application
-- * data family application
......@@ -675,18 +698,18 @@ flatten fmode (TyConApp tc tys)
-- _ -> fmode
= flattenTyConApp fmode tc tys
flatten fmode ty@(ForAllTy {})
flatten_one fmode ty@(ForAllTy {})
-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
= do { let (tvs, rho) = splitForAllTys ty
; (rho', co) <- flatten (fmode { fe_mode = FM_SubstOnly }) rho
; (rho', co) <- flatten_one (fmode { fe_mode = FM_SubstOnly }) rho
-- Substitute only under a forall
-- See Note [Flattening under a forall]
; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
flattenTyConApp :: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
flattenTyConApp fmode tc tys
= do { (xis, cos) <- flattenMany fmode tys
= do { (xis, cos) <- flatten_many fmode tys
; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
{-
......@@ -732,43 +755,43 @@ and we have not begun to think about how to make that work!
************************************************************************
-}
flattenFamApp, flattenExactFamApp, flattenExactFamApp_fully
flatten_fam_app, flatten_exact_fam_app, flatten_exact_fam_app_fully
:: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
-- flattenFamApp can be over-saturated
-- flattenExactFamApp is exactly saturated
-- flattenExactFamApp_fully lifts out the application to top level
-- flatten_fam_app can be over-saturated
-- flatten_exact_fam_app is exactly saturated
-- flatten_exact_fam_app_fully lifts out the application to top level
-- Postcondition: Coercion :: Xi ~ F tys
flattenFamApp fmode tc tys -- Can be over-saturated
flatten_fam_app fmode tc tys -- Can be over-saturated
= ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
-- The type function might be *over* saturated
-- in which case the remaining arguments should
-- be dealt with by AppTys
do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
; (xi1, co1) <- flattenExactFamApp fmode tc tys1
; (xi1, co1) <- flatten_exact_fam_app fmode tc tys1
-- co1 :: xi1 ~ F tys1
; (xis_rest, cos_rest) <- flattenMany fmode tys_rest
; (xis_rest, cos_rest) <- flatten_many fmode tys_rest
-- cos_res :: xis_rest ~ tys_rest
; return ( mkAppTys xi1 xis_rest -- NB mkAppTys: rhs_xi might not be a type variable
-- cf Trac #5655
, mkTcAppCos co1 cos_rest -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
) }
flattenExactFamApp fmode tc tys
flatten_exact_fam_app fmode tc tys
= case fe_mode fmode of
FM_FlattenAll -> flattenExactFamApp_fully fmode tc tys
FM_FlattenAll -> flatten_exact_fam_app_fully fmode tc tys
FM_SubstOnly -> do { (xis, cos) <- flattenMany fmode tys
FM_SubstOnly -> do { (xis, cos) <- flatten_many fmode tys
; return ( mkTyConApp tc xis
, mkTcTyConAppCo Nominal tc cos ) }
FM_Avoid tv flat_top -> do { (xis, cos) <- flattenMany fmode tys
FM_Avoid tv flat_top -> do { (xis, cos) <- flatten_many fmode tys
; if flat_top || tv `elemVarSet` tyVarsOfTypes xis
then flattenExactFamApp_fully fmode tc tys
then flatten_exact_fam_app_fully fmode tc tys
else return ( mkTyConApp tc xis
, mkTcTyConAppCo Nominal tc cos ) }
flattenExactFamApp_fully fmode tc tys
= do { (xis, cos) <- flattenMany (fmode { fe_mode = FM_FlattenAll })tys
flatten_exact_fam_app_fully fmode tc tys
= do { (xis, cos) <- flatten_many (fmode { fe_mode = FM_FlattenAll })tys
; let ret_co = mkTcTyConAppCo Nominal tc cos
-- ret_co :: F xis ~ F tys
ctxt_ev = fe_ev fmode
......@@ -796,7 +819,7 @@ flattenExactFamApp_fully fmode tc tys
, cc_fun = tc
, cc_tyargs = xis
, cc_fsk = fsk }
; updWorkListTcS (extendWorkListFunEq ct)
; emitFlatWork ct
; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev)
; return (mkTyVarTy fsk, mkTcSymCo (ctEvCoercion ev) `mkTcTransCo` ret_co) } }
......@@ -827,7 +850,7 @@ flattenTyVar fmode tv
ty' = mkTyVarTy tv'
Right (ty1, co1) -- Recurse
-> do { (ty2, co2) <- flatten fmode ty1
-> do { (ty2, co2) <- flatten_one fmode ty1
; traceTcS "flattenTyVar3" (ppr tv $$ ppr ty2)
; return (ty2, co2 `mkTcTransCo` co1) }
}
......@@ -873,7 +896,7 @@ flattenTyVarFinal ctxt_ev tv
= -- Done, but make sure the kind is zonked
do { let kind = tyVarKind tv
kind_fmode = FE { fe_ev = ctxt_ev, fe_mode = FM_SubstOnly }
; (new_knd, _kind_co) <- flatten kind_fmode kind
; (new_knd, _kind_co) <- flatten_one kind_fmode kind
; return (Left (setVarType tv new_knd)) }
{-
......
......@@ -29,6 +29,7 @@ import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as,
is_decl, Provenance(Imported), gre_prov )
import FunDeps
import FamInst
import Inst( tyVarsOfCt )
import TcEvidence
import Outputable
......@@ -976,7 +977,7 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
, inert_insols = insols_in }
kicked_out = WL { wl_eqs = tv_eqs_out
, wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
, wl_funeqs = feqs_out
, wl_rest = bagToList (dicts_out `andCts` irs_out
`andCts` insols_out)
, wl_implics = emptyBag }
......@@ -1660,7 +1661,9 @@ shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
-> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
shortCutReduction old_ev fsk ax_co fam_tc tc_args
| isGiven old_ev
= do { (xis, cos) <- flattenMany (FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }) tc_args
= runFlatten $
do { let fmode = FE { fe_mode = FM_FlattenAll, fe_ev = old_ev }
; (xis, cos) <- flatten_many fmode tc_args
-- ax_co :: F args ~ G tc_args
-- cos :: xis ~ tc_args
-- old_ev :: F args ~ fsk
......@@ -1673,12 +1676,14 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
`mkTcTransCo` ctEvCoercion old_ev) )
; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
; updWorkListTcS (extendWorkListFunEq new_ct)
; emitFlatWork new_ct
; stopWith old_ev "Fun/Top (given, shortcut)" }
| otherwise
= ASSERT( not (isDerived old_ev) ) -- Caller ensures this
do { (xis, cos) <- flattenMany (FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }) tc_args
runFlatten $
do { let fmode = FE { fe_mode = FM_FlattenAll, fe_ev = old_ev }
; (xis, cos) <- flatten_many fmode tc_args
-- ax_co :: F args ~ G tc_args
-- cos :: xis ~ tc_args
-- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
......@@ -1691,7 +1696,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
`mkTcTransCo` ctEvCoercion new_ev))
; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
; updWorkListTcS (extendWorkListFunEq new_ct)
; emitFlatWork new_ct
; stopWith old_ev "Fun/Top (wanted, shortcut)" }
where
loc = ctEvLoc old_ev
......
......@@ -455,7 +455,15 @@ writeTcRef :: TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef = writeMutVar
updTcRef :: TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
updTcRef = updMutVar
-- Returns ()
updTcRef ref fn = liftIO $ do { old <- readIORef ref
; writeIORef ref (fn old) }
updTcRefX :: TcRef a -> (a -> a) -> TcRnIf gbl lcl a
-- Returns previous value
updTcRefX ref fn = liftIO $ do { old <- readIORef ref
; writeIORef ref (fn old)
; return old }
{-
************************************************************************
......
......@@ -3,41 +3,26 @@
-- Type definitions for the constraint solver
module TcSMonad (
-- Canonical constraints, definition is now in TcRnTypes
-- The work list
WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListFunEq,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, appendWorkList, selectWorkItem,
workListSize,
updWorkListTcS, updWorkListTcS_return,
runFlatten, emitFlatWork,
updInertTcS, updInertCans, updInertDicts, updInertIrreds, updInertFunEqs,
Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
emitInsoluble, emitWorkNC,
isWanted, isDerived,
isGivenCt, isWantedCt, isDerivedCt,
-- The TcS monad
TcS, runTcS, runTcSWithEvBinds,
failTcS, tryTcS, nestTcS, nestImplicTcS, recoverTcS,
mkGivenLoc,
runTcPluginTcS, addUsedRdrNamesTcS, deferTcSForAllEq,
TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
-- Tracing etc
panicTcS, traceTcS,
traceFireTcS, bumpStepCountTcS, csTraceTcS,
tryTcS, nestTcS, nestImplicTcS, recoverTcS,
wrapErrTcS, wrapWarnTcS,
runTcPluginTcS,
-- Getting and setting the flattening cache
addSolvedDict,
-- Marking stuff as used
addUsedRdrNamesTcS,
deferTcSForAllEq,
setEvBind,
-- Evidence creation and transformation
XEvTerm(..),
Freshness(..), freshGoals, isFresh,
......@@ -49,40 +34,47 @@ module TcSMonad (
maybeSym,
newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
setWantedTyBind, reportUnifications,
setEvBind,
newEvVar, newGivenEvVar,
emitNewDerived, emitNewDerivedEq,
instDFunConstraints,
-- Creation of evidence variables
setWantedTyBind, reportUnifications,
getInstEnvs, getFamInstEnvs, -- Getting the environments
getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
getTcEvBindsMap,
lookupFlatCache, newFlattenSkolem, -- Flatten skolems
-- Deque
Deque(..), insertDeque, emptyDeque,
-- Inerts
InertSet(..), InertCans(..),
updInertTcS, updInertCans, updInertDicts, updInertIrreds,
getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
emptyInert, getTcSInerts, setTcSInerts,
getUnsolvedInerts, checkAllSolved,
splitInertCans, removeInertCts,
prepareInertsForImplications,
addInertCan, insertInertItemTcS, insertFunEq,
emitInsoluble, emitWorkNC,
EqualCtList,
lookupSolvedDict, extendFlatCache,
-- Inert CDictCans
lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
findFunEq, findTyEqs,
-- Inert CTyEqCans
findTyEqs,
-- Inert solved dictionaries
addSolvedDict, lookupSolvedDict,
-- The flattening cache
lookupFlatCache, extendFlatCache, newFlattenSkolem, -- Flatten skolems
-- Inert CFunEqCans
updInertFunEqs, findFunEq, sizeFunEqMap,
findFunEqsByTyCon, findFunEqs, partitionFunEqs,
sizeFunEqMap,
instDFunType, -- Instantiation
-- MetaTyVars
newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
cloneMetaTyVar, demoteUnfilledFmv,
......@@ -90,8 +82,11 @@ module TcSMonad (
isFilledMetaTyVar_maybe, isFilledMetaTyVar,
zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkFlats,
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
-- References
newTcRef, readTcRef, updTcRef,
-- Misc
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam,
checkWellStagedDFun,
pprEq -- Smaller utils, re-exported from TcM
......@@ -176,43 +171,62 @@ 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.
-}
data Deque a = DQ [a] [a] -- Insert in RH field, remove from LH field
-- First to remove is at head of LH field
instance Outputable a => Outputable (Deque a) where
ppr q = ppr (dequeList q)
dequeList :: Deque a -> [a]
dequeList (DQ as bs) = as ++ reverse bs -- First one to come out at the start
emptyDeque :: Deque a
emptyDeque = DQ [] []
Note [The flattening work list]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "flattening work list", held in the tcs_flat_work field of TcSEnv,
is a list of CFunEqCans generated during flattening. The key idea
is this. Consider flattening (Eq (F (G Int) (H Bool)):
* The flattener recursively calls itself on sub-terms before building
the main term, so it will encounter the terms in order
G Int
H Bool
F (G Int) (H Bool)
flattening to sub-goals
w1: G Int ~ fuv0
w2: H Bool ~ fuv1
w3: F fuv0 fuv1 ~ fuv2
* Processing w3 first is BAD, because we can't reduce i t,so it'll
get put into the inert set, and later kicked out when w1, w2 are
solved. In Trac #9872 this led to inert sets containing hundreds
of suspended calls.
* So we want to process w1, w2 first.
* So you might think that we should just use a FIFO deque for the work-list,
so that putting adding goals in order w1,w2,w3 would mean we processed
w1 first.
* BUT suppose we have 'type instance G Int = H Char'. Then processing
w1 leads to a new goal
w4: H Char ~ fuv0
We do NOT want to put that on the far end of a deque! Instead we want
to put it at the *front* of the work-list so that we continue to work
on it.
So the work-list structure is this:
* The wl_funeqs is a LIFO stack; we push new goals (such as w4) on
top (extendWorkListFunEq), and take new work from the top
(selectWorkItem).
* When flattening, emitFlatWork pushes new flattening goals (like
w1,w2,w3) onto the flattening work list, tcs_flat_work, another
push-down stack.
* When we finish flattening, we *reverse* the tcs_flat_work stack
onto the wl_funeqs stack (which brings w1 to the top).
The function runFlatten initialised the tcs_flat_work stack, and reverses
it onto wl_fun_eqs at the end.
isEmptyDeque :: Deque a -> Bool
isEmptyDeque (DQ as bs) = null as && null bs
dequeSize :: Deque a -> Int
dequeSize (DQ as bs) = length as + length bs
insertDeque :: a -> Deque a -> Deque a
insertDeque b (DQ as bs) = DQ as (b:bs)
appendDeque :: Deque a -> Deque a -> Deque a
appendDeque (DQ as1 bs1) (DQ as2 bs2) = DQ (as1 ++ reverse bs1 ++ as2) bs2
extractDeque :: Deque a -> Maybe (Deque a, a)
extractDeque (DQ [] []) = Nothing
extractDeque (DQ (a:as) bs) = Just (DQ as bs, a)
extractDeque (DQ [] bs) = case reverse bs of
(a:as) -> Just (DQ as [], a)
[] -> panic "extractDeque"
-}
-- See Note [WorkList priorities]
data WorkList
= WL { wl_eqs :: [Ct]
, wl_funeqs :: Deque Ct
, wl_funeqs :: [Ct] -- LIFO stack of goals
, wl_rest :: [Ct]
, wl_implics :: Bag Implication -- See Note [Residual implications]
}
......@@ -221,15 +235,15 @@ appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
(WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1, wl_implics = implics1 })
(WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 })
= WL { wl_eqs = eqs1 ++ eqs2
, wl_funeqs = funeqs1 `appendDeque` funeqs2
, wl_rest = rest1 ++ rest2
= WL { wl_eqs = eqs1 ++ eqs2
, wl_funeqs = funeqs1 ++ funeqs2
, wl_rest = rest1 ++ rest2
, wl_implics = implics1 `unionBags` implics2 }
workListSize :: WorkList -> Int
workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
= length eqs + dequeSize funeqs + length rest
= length eqs + length funeqs + length rest
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq ct wl
......@@ -237,7 +251,7 @@ extendWorkListEq ct wl
extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq ct wl
= wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
= wl { wl_funeqs = ct : wl_funeqs wl }
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
......@@ -268,20 +282,19 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
, wl_rest = rest, wl_implics = implics })
= null eqs && null rest && isEmptyDeque funeqs && isEmptyBag implics
= null eqs && null rest && null funeqs && isEmptyBag implics