Commit 815dcff1 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

A few more constraint solver improvements

* Get rid of the lookupInInerts stage

* Re-introduce the flat-cache for flattening type-family equations
  See Note [Type family equations] in TcSMonad. My previous clever attempt
  with organising the work list proved too fragile.

  There's a (static) flag -fno-flat-cache to switch if off,
  so you can try with and without

* Improve the -ddump-cs-trace output

* The usual round of refactoring
parent 902a8632
......@@ -131,6 +131,7 @@ isStaticFlag f =
"fruntime-types",
"fno-pre-inlining",
"fno-opt-coercion",
"fno-flat-cache",
"fexcess-precision",
"fhardwire-lib-paths",
"fcpr-off",
......
......@@ -48,6 +48,7 @@ module StaticFlags (
opt_SimplExcessPrecision,
opt_NoOptCoercion,
opt_MaxWorkerArgs,
opt_NoFlatCache,
-- Unfolding control
opt_UF_CreationThreshold,
......@@ -243,6 +244,9 @@ opt_SimplExcessPrecision = lookUp (fsLit "-fexcess-precision")
opt_NoOptCoercion :: Bool
opt_NoOptCoercion = lookUp (fsLit "-fno-opt-coercion")
opt_NoFlatCache :: Bool
opt_NoFlatCache = lookUp (fsLit "-fno-flat-cache")
-- Unfolding control
-- See Note [Discounts and thresholds] in CoreUnfold
......
......@@ -532,9 +532,8 @@ flatten loc f ctxt (TyConApp tc tys)
FMFullFlatten ->
do { mb_ct <- lookupFlatEqn fam_ty
; case mb_ct of
Just ct
| let ctev = cc_ev ct
flav = ctEvFlavour ctev
Just (ctev, rhs_ty)
| let flav = ctEvFlavour ctev
, flav `canRewrite` ctxt
-> -- You may think that we can just return (cc_rhs ct) but not so.
-- return (mkTcCoVarCo (ctId ct), cc_rhs ct, [])
......@@ -544,40 +543,21 @@ flatten loc f ctxt (TyConApp tc tys)
-- cache as well when we interact an equality with the inert.
-- The design choice is: do we keep the flat cache rewritten or not?
-- For now I say we don't keep it fully rewritten.
do { traceTcS "flatten/flat-cache hit" $ ppr ct
; let rhs_xi = cc_rhs ct
; (flat_rhs_xi,co) <- flatten (cc_loc ct) f flav rhs_xi
do { traceTcS "flatten/flat-cache hit" $ ppr ctev
; (rhs_xi,co) <- flatten loc f flav rhs_ty
; let final_co = evTermCoercion (ctEvTerm ctev)
`mkTcTransCo` mkTcSymCo co
; return (final_co, flat_rhs_xi) }
; return (final_co, rhs_xi) }
_ | Given <- ctxt -- Given: make new flatten skolem
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_ty <- newFlattenSkolemTy fam_ty
; let co = mkTcReflCo fam_ty
new_ev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
, ctev_evtm = EvCoercion co }
ct = CFunEqCan { cc_ev = new_ev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_ty
, cc_loc = loc }
_ -> do { traceTcS "flatten/flat-cache miss" $ ppr fam_ty
; (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty
; let ct = CFunEqCan { cc_ev = ctev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi
, cc_loc = loc }
; updWorkListTcS $ extendWorkListFunEq ct
; return (co, rhs_ty) }
| otherwise -- Wanted or Derived: make new unification variable
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
; ctev <- newWantedEvVarNC (mkTcEqPred fam_ty rhs_xi_var)
-- NC (no-cache) version because we've already
-- looked in the solved goals an inerts (lookupFlatEqn)
; let ct = CFunEqCan { cc_ev = ctev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi_var
, cc_loc = loc }
; updWorkListTcS $ extendWorkListFunEq ct
; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
; return (evTermCoercion (ctEvTerm ctev), rhs_xi) }
}
-- Emit the flat constraints
; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
......@@ -1140,9 +1120,9 @@ canEqLeafFunEq loc ev fn tys1 ty2 -- ev :: F tys1 ~ ty2
; mb <- rewriteCtFlavor ev (mkTcEqPred fam_head xi2) xco
; case mb of {
Nothing -> return Stop ;
Just new_ev
| isTcReflCo xco -> continueWith new_ct
| otherwise -> do { updWorkListTcS (extendWorkListFunEq new_ct); return Stop }
Just new_ev -> continueWith new_ct
-- | isTcReflCo xco -> continueWith new_ct
-- | otherwise -> do { updWorkListTcS (extendWorkListFunEq new_ct); return Stop }
where
new_ct = CFunEqCan { cc_ev = new_ev, cc_loc = loc
, cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } } }
......
......@@ -171,6 +171,7 @@ runSolverPipeline pipeline workItem
vcat [ ptext (sLit "work item = ") <+> ppr workItem
, ptext (sLit "inerts = ") <+> ppr initial_is]
; bumpStepCountTcS -- One step for each constraint processed
; final_res <- run_pipeline pipeline (ContinueWith workItem)
; final_is <- getTcSInerts
......@@ -178,7 +179,8 @@ runSolverPipeline pipeline workItem
Stop -> do { traceTcS "End solver pipeline (discharged) }"
(ptext (sLit "inerts = ") <+> ppr final_is)
; return () }
ContinueWith ct -> do { traceTcS "End solver pipeline (not discharged) }" $
ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert:") <+> ppr ct)
; traceTcS "End solver pipeline (not discharged) }" $
vcat [ ptext (sLit "final_item = ") <+> ppr ct
, ptext (sLit "inerts = ") <+> ppr final_is]
; insertInertItemTcS ct }
......@@ -220,39 +222,13 @@ React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canoni
\begin{code}
thePipeline :: [(String,SimplifierStage)]
thePipeline = [ ("lookup-in-inerts", lookupInInertsStage)
, ("canonicalization", canonicalizationStage)
thePipeline = [ ("canonicalization", TcCanonical.canonicalize)
, ("spontaneous solve", spontaneousSolveStage)
, ("interact with inerts", interactWithInertsStage)
, ("top-level reactions", topReactionsStage) ]
\end{code}
\begin{code}
-- A quick lookup everywhere to see if we know about this constraint
--------------------------------------------------------------------
lookupInInertsStage :: SimplifierStage
lookupInInertsStage ct
| CtWanted { ctev_evar = ev_id, ctev_pred = pred } <- cc_ev ct
= do { mb_ct <- lookupInInerts pred
; case mb_ct of
Just ctev
| not (isDerived ctev)
-> do { setEvBind ev_id (ctEvTerm ctev)
; return Stop }
_ -> continueWith ct }
| otherwise -- I could do something like that for givens
-- as well I suppose but it is not a big deal
= continueWith ct
-- The canonicalization stage, see TcCanonical for details
----------------------------------------------------------
canonicalizationStage :: SimplifierStage
canonicalizationStage = TcCanonical.canonicalize
\end{code}
*********************************************************************************
* *
The spontaneous-solve Stage
......@@ -287,7 +263,10 @@ spontaneousSolveStage workItem
SPCantSolve
| CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
-- Unsolved equality
-> do { kickOutRewritable (ctEvFlavour fl) tv
-> do { n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
; traceFireTcS workItem $
ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon
<+> ppr workItem
; insertInertItemTcS workItem
; return Stop }
| otherwise
......@@ -296,10 +275,15 @@ spontaneousSolveStage workItem
SPSolved new_tv
-- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
-- see Note [Spontaneously solved in TyBinds]
-> do { traceFireTcS workItem $
ptext (sLit "Spontaneously solved:") <+> ppr workItem
; kickOutRewritable Given new_tv
-> do { n_kicked <- kickOutRewritable Given new_tv
; traceFireTcS workItem $
ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked <> colon
<+> ppr workItem
; return Stop } }
ppr_kicked :: Int -> SDoc
ppr_kicked 0 = empty
ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
\end{code}
Note [Spontaneously solved in TyBinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -320,13 +304,14 @@ these binds /and/ the inerts for potentially unsolved or other given equalities.
kickOutRewritable :: CtFlavour -- Flavour of the equality that is
-- being added to the inert set
-> TcTyVar -- The new equality is tv ~ ty
-> TcS ()
-> TcS Int
kickOutRewritable new_flav new_tv
= do { wl <- modifyInertTcS kick_out
; traceTcS "kickOutRewritable" $
vcat [ text "tv = " <+> ppr new_tv
, ptext (sLit "Kicked out =") <+> ppr wl]
; updWorkListTcS (appendWorkList wl) }
; updWorkListTcS (appendWorkList wl)
; return (workListSize wl) }
where
kick_out :: InertSet -> (WorkList, InertSet)
kick_out (is@(IS { inert_cans = IC { inert_eqs = tv_eqs
......@@ -660,7 +645,7 @@ interactWithInertsStage wi
-> do { traceFireTcS atomic_inert
(mk_msg rule (text "InertItemConsumed"))
; return (ContinueWith wi) }
IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
IRKeepGoing {}
-> do { insertInertItemTcS atomic_inert
; return (ContinueWith wi) }
}
......@@ -1384,23 +1369,31 @@ doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
-> CtLoc -> TcS TopInteractResult
doTopReactDict inerts workItem fl cls xis loc
= do { instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs
(mkClassPred cls xis, arising_sdoc)
; let pred = mkClassPred cls xis
fd_eqns = improveFromInstEnv instEnvs (pred, arising_sdoc)
; fd_work <- rewriteWithFunDeps fd_eqns loc
; if not (null fd_work) then
do { updWorkListTcS (extendWorkListEqs fd_work)
; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
, tir_new_item = ContinueWith workItem } }
else -- No fundeps
if isWanted fl then
do { lkup_inst_res <- matchClassInst inerts cls xis loc
; case lkup_inst_res of
GenInst wtvs ev_term -> do { addSolvedDict fl
; doSolveFromInstance wtvs ev_term }
NoInstance -> return NoTopInt }
else
return NoTopInt }
, tir_new_item = ContinueWith workItem } }
else if not (isWanted fl) then
return NoTopInt
else do
{ solved_dicts <- getTcSInerts >>= (return . inert_solved_dicts)
; case lookupSolvedDict solved_dicts pred of {
Just ev -> do { setEvBind dict_id (ctEvTerm ev);
; return $
SomeTopInt { tir_rule = "Dict/Top (cached)"
, tir_new_item = Stop } } ;
Nothing -> do
{ lkup_inst_res <- matchClassInst inerts cls xis loc
; case lkup_inst_res of
GenInst wtvs ev_term -> do { addSolvedDict fl
; doSolveFromInstance wtvs ev_term }
NoInstance -> return NoTopInt } } } }
where
arising_sdoc = pprArisingAt loc
dict_id = ctEvId fl
......@@ -1430,18 +1423,17 @@ doTopReactDict inerts workItem fl cls xis loc
--------------------
doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
-> CtLoc -> TcS TopInteractResult
doTopReactFunEq ct fl fun_tc args xi loc
doTopReactFunEq _ct fl fun_tc args xi loc
= ASSERT (isSynFamilyTyCon fun_tc) -- No associated data families have
-- reached this far
-- Look in the cache of solved funeqs
do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
; case lookupFamHead fun_eq_cache fam_ty of {
Just (CFunEqCan { cc_ev = ctev, cc_rhs = rhs_ty })
Just (ctev, rhs_ty)
| ctEvFlavour ctev `canRewrite` ctEvFlavour fl
-> ASSERT( not (isDerived ctev) )
succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
Just ct' -> pprPanic "doTopReactFunEq" (ppr ct') ;
Nothing ->
_other ->
-- Look up in top-level instances
do { match_res <- matchFam fun_tc args -- See Note [MATCHING-SYNONYMS]
......@@ -1451,7 +1443,7 @@ doTopReactFunEq ct fl fun_tc args xi loc
-- Found a top-level instance
do { -- Add it to the solved goals
unless (isDerived fl) (addSolvedFunEq ct fam_ty)
unless (isDerived fl) (addSolvedFunEq fam_ty fl xi)
; let coe_ax = famInstAxiom famInst
; succeed_with "Fun/Top" (mkTcAxInstCo coe_ax rep_tys)
......
......@@ -16,7 +16,7 @@ module TcSMonad (
extendWorkListEq, extendWorkListFunEq,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
withWorkList,
withWorkList, workListSize,
updWorkListTcS, updWorkListTcS_return,
......@@ -32,7 +32,7 @@ module TcSMonad (
mkGivenLoc,
TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
traceFireTcS,
traceFireTcS, bumpStepCountTcS,
tryTcS, nestTcS, nestImplicTcS, recoverTcS,
wrapErrTcS, wrapWarnTcS,
......@@ -58,7 +58,7 @@ module TcSMonad (
getTcEvBindsMap, getTcSTyBinds, getTcSTyBindsMap,
newFlattenSkolemTy, -- Flatten skolems
lookupFlatEqn, newFlattenSkolem, -- Flatten skolems
-- Deque
Deque(..), insertDeque, emptyDeque,
......@@ -66,7 +66,7 @@ module TcSMonad (
-- Inerts
InertSet(..), InertCans(..),
getInertEqs,
emptyInert, getTcSInerts, lookupInInerts, lookupFlatEqn,
emptyInert, getTcSInerts, lookupInInerts,
getInertUnsolved, checkAllSolved,
prepareInertsForImplications,
modifyInertTcS,
......@@ -74,7 +74,7 @@ module TcSMonad (
getRelevantCts, extractRelevantInerts,
CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
PredMap, FamHeadMap,
partCtFamHeadMap, lookupFamHead,
partCtFamHeadMap, lookupFamHead, lookupSolvedDict,
filterSolved,
instDFunType, -- Instantiation
......@@ -134,6 +134,7 @@ import TcRnTypes
import Unique
import UniqFM
import Maybes ( orElse, catMaybes, firstJust )
import StaticFlags( opt_NoFlatCache )
import Control.Monad( unless, when, zipWithM )
import Data.IORef
......@@ -208,6 +209,9 @@ emptyDeque = DQ [] []
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)
......@@ -235,6 +239,10 @@ appendWorkList new_wl orig_wl
, wl_rest = wl_rest new_wl ++ wl_rest orig_wl }
workListSize :: WorkList -> Int
workListSize (WorkList { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
= length eqs + dequeSize funeqs + length rest
extendWorkListEq :: Ct -> WorkList -> WorkList
-- Extension by equality
extendWorkListEq ct wl
......@@ -406,6 +414,9 @@ instance Outputable a => Outputable (FamHeadMap a) where
sizePredMap :: PredMap a -> Int
sizePredMap (PredMap m) = foldTypeMap (\_ x -> x+1) 0 m
emptyFamHeadMap :: FamHeadMap a
emptyFamHeadMap = FamHeadMap emptyTM
sizeFamHeadMap :: FamHeadMap a -> Int
sizeFamHeadMap (FamHeadMap m) = foldTypeMap (\_ x -> x+1) 0 m
......@@ -453,31 +464,6 @@ filterSolved p (PredMap mp) = PredMap (foldTM upd mp emptyTM)
%* *
%************************************************************************
\begin{code}
-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
data InertCans
= IC { inert_eqs :: TyVarEnv Ct
-- Must all be CTyEqCans! If an entry exists of the form:
-- a |-> ct,co
-- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi }
-- And co : a ~ xi
, inert_dicts :: CCanMap Class
-- Dictionaries only, index is the class
-- NB: index is /not/ the whole type because FD reactions
-- need to match the class but not necessarily the whole type.
, inert_funeqs :: CtFamHeadMap
-- Family equations, index is the whole family head type.
, inert_irreds :: Cts
-- Irreducible predicates
, inert_insols :: Cts
-- Frozen errors (as non-canonicals)
}
\end{code}
Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:
......@@ -536,24 +522,76 @@ The reason for all this is simply to avoid re-solving goals we have solved alrea
But there are no solved Deriveds in inert_solved_funeqs
Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Type-family equations, of form (ev : F tys ~ ty), live in four places
* The work-list, of course
* The inert_flat_cache. This is used when flattening, to get maximal
sharing. It contains lots of things that are still in the work-list.
E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
work list. Then we flatten w1, dumping (w3: G a ~ f1) in the work
list. Now if we flatten w2 before we get to w3, we still want to
share that (G a).
Because it contains work-list things, DO NOT use the flat cache to solve
a top-level goal. Eg in the above example we don't want to solve w3
using w3 itself!
* The inert_solved_funeqs. These are all "solved" goals (see Note [Solved constraints]),
the result of using a top-level type-family instance.
* THe inert_funeqs are un-solved but fully processed and in the InertCans.
\begin{code}
-- All Given (fully known) or Wanted or Derived
-- See Note [Detailed InertCans Invariants] for more
data InertCans
= IC { inert_eqs :: TyVarEnv Ct
-- Must all be CTyEqCans! If an entry exists of the form:
-- a |-> ct,co
-- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi }
-- And co : a ~ xi
, inert_dicts :: CCanMap Class
-- Dictionaries only, index is the class
-- NB: index is /not/ the whole type because FD reactions
-- need to match the class but not necessarily the whole type.
, inert_funeqs :: CtFamHeadMap
-- Family equations, index is the whole family head type.
, inert_irreds :: Cts
-- Irreducible predicates
, inert_insols :: Cts
-- Frozen errors (as non-canonicals)
}
-- The Inert Set
data InertSet
= IS { inert_cans :: InertCans
-- Canonical Given, Wanted, Derived (no Solved)
-- Sometimes called "the inert set"
, inert_fsks :: [TcTyVar] -- Flatten-skolems allocated in this local scope
-- All ``flattening equations'' are kept here.
-- Always canonical CTyFunEqs (Given or Wanted only!)
-- Key is by family head. We use this field during flattening only
, inert_flat_cache :: FamHeadMap (CtEvidence, TcType)
-- See Note [Type family equations]
-- Just a hash-cons cache for use when flattening only
-- These include entirely un-processed goals, so don't use
-- them to solve a top-level goal, else you may end up solving
-- (w:F ty ~ a) by setting w:=w! We just use the flat-cache
-- when allocating a new flatten-skolem.
-- Not necessarily inert wrt top-level equations (or inert_cans)
, inert_fsks :: [TcTyVar] -- Rigid flatten-skolems (arising from givens)
-- allocated in this local scope
, inert_solved_funeqs :: CtFamHeadMap
, inert_solved_funeqs :: FamHeadMap (CtEvidence, TcType)
-- See Note [Type family equations]
-- Of form co :: F xis ~ xi
-- Always the result of using a top-level family axiom F xis ~ tau
-- No Deriveds
-- Not necessarily fully rewritten (by type substitutions)
, inert_solved_dicts :: PredMap CtEvidence
-- Of form ev :: C t1 .. tn
......@@ -589,12 +627,13 @@ emptyInert :: InertSet
emptyInert
= IS { inert_cans = IC { inert_eqs = emptyVarEnv
, inert_dicts = emptyCCanMap
, inert_funeqs = FamHeadMap emptyTM
, inert_funeqs = emptyFamHeadMap
, inert_irreds = emptyCts
, inert_insols = emptyCts }
, inert_fsks = []
, inert_flat_cache = emptyFamHeadMap
, inert_solved_dicts = PredMap emptyTM
, inert_solved_funeqs = FamHeadMap emptyTM }
, inert_solved_funeqs = emptyFamHeadMap }
insertInertItem :: Ct -> InertSet -> InertSet
-- Add a new inert element to the inert set.
......@@ -661,12 +700,11 @@ addSolvedDict item
pred = ctEvPred item
upd_solved _ = Just item
addSolvedFunEq :: Ct -> TcType -> TcS ()
addSolvedFunEq fun_eq fam_ty
= updInertTcS upd_solved_funeqs
where
upd_solved_funeqs inert
= inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert) fam_ty fun_eq }
addSolvedFunEq :: TcType -> CtEvidence -> TcType -> TcS ()
addSolvedFunEq fam_ty ev rhs_ty
= updInertTcS $ \ inert ->
inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert)
fam_ty (ev, rhs_ty) }
modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a
-- Modify the inert set with the supplied function
......@@ -689,7 +727,8 @@ prepareInertsForImplications :: InertSet -> InertSet
-- See Note [Preparing inert set for implications]
prepareInertsForImplications is
= is { inert_cans = getGivens (inert_cans is)
, inert_fsks = [] }
, inert_fsks = []
, inert_flat_cache = emptyFamHeadMap }
where
getGivens (IC { inert_eqs = eqs
, inert_irreds = irreds
......@@ -831,25 +870,31 @@ extractRelevantInerts wi
extract_ics_relevants _ ics = (emptyCts,ics)
lookupFlatEqn :: TcType -> TcS (Maybe Ct)
lookupFlatEqn :: TcType -> TcS (Maybe (CtEvidence, TcType))
lookupFlatEqn fam_ty
= do { IS { inert_solved_funeqs = solved_funeqs
, inert_flat_cache = flat_cache
, inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
; return (lookupFamHead solved_funeqs fam_ty
`firstJust` lookupFamHead inert_funeqs fam_ty
) }
; return (lookupFamHead solved_funeqs fam_ty `firstJust`
lookupFamHead flat_cache fam_ty `firstJust`
lookup_in_inerts inert_funeqs) }
where
lookup_in_inerts inert_funeqs
= case lookupFamHead inert_funeqs fam_ty of
Nothing -> Nothing
Just ct -> Just (ctEvidence ct, cc_rhs ct)
lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet
lookupInInerts pty
= do { IS { inert_solved_dicts = solved, inert_cans = ics } <- getTcSInerts
; case lookupInSolved solved pty of
; case lookupSolvedDict solved pty of
Just ctev -> return (Just ctev)
Nothing -> return (lookupInInertCans ics pty) }
lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
lookupSolvedDict :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupInSolved tm pty = lookupTM pty $ unPredMap tm
lookupSolvedDict tm pty = lookupTM pty $ unPredMap tm
lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
-- Returns Just if exactly this pred type exists in the inert canonicals
......@@ -960,14 +1005,17 @@ traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
instance HasDynFlags TcS where
getDynFlags = wrapTcS getDynFlags
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
; n <- TcM.readTcRef ref
; TcM.writeTcRef ref (n+1) }
traceFireTcS :: Ct -> SDoc -> TcS ()
-- Dump a rule-firing trace, and bumpt the counter
-- Dump a rule-firing trace
traceFireTcS ct doc
= TcS $ \env ->
TcM.ifDOptM Opt_D_dump_cs_trace $
do { let count_ref = tcs_count env
; n <- TcM.readTcRef count_ref
; TcM.writeTcRef count_ref (n+1)
do { n <- TcM.readTcRef (tcs_count env)
; let msg = int n <> brackets (int (ctLocDepth (cc_loc ct))) <+> doc
; TcM.dumpTcRn msg }
......@@ -1304,19 +1352,42 @@ which will result in two Deriveds to end up in the insoluble set:
\begin{code}
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
newFlattenSkolemTy :: TcType -> TcS TcType
newFlattenSkolemTy fam_ty
newFlattenSkolem :: CtFlavour
-> TcType -- F xis
-> TcS (CtEvidence, TcType) -- co :: F xis ~ ty
-- We have already looked up in the cache; no need to so so again
newFlattenSkolem Given fam_ty
= do { tv <- wrapTcS $
do { uniq <- TcM.newUnique
; let name = TcM.mkTcTyVarName uniq (fsLit "f")
; return $ mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty) }
; traceTcS "New Flatten Skolem Born" $
ppr tv <+> text "[:= " <+> ppr fam_ty <+> text "]"
; updInertTcS (add_fsk tv)
; return (mkTyVarTy tv) }
where
add_fsk :: TcTyVar -> InertSet -> InertSet
add_fsk tv is = is { inert_fsks = tv : inert_fsks is }
; let rhs_ty = mkTyVarTy tv
ctev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
, ctev_evtm = EvCoercion (mkTcReflCo fam_ty) }
; updInertTcS $ \ is@(IS { inert_fsks = fsks }) ->
extendFlatCache fam_ty ctev rhs_ty
is { inert_fsks = tv : fsks }
; return (ctev, rhs_ty) }
newFlattenSkolem _ fam_ty -- Wanted or Derived: make new unification variable
= do { rhs_ty <- newFlexiTcSTy (typeKind fam_ty)
; ctev <- newWantedEvVarNC (mkTcEqPred fam_ty rhs_ty)
-- NC (no-cache) version because we've already
-- looked in the solved goals an inerts (lookupFlatEqn)
; updInertTcS $ extendFlatCache fam_ty ctev rhs_ty
; return (ctev, rhs_ty) }
extendFlatCache :: TcType -> CtEvidence -> TcType -> InertSet -> InertSet
extendFlatCache
| opt_NoFlatCache
= \ _ _ _ is -> is
| otherwise
= \ fam_ty ctev rhs_ty is@(IS { inert_flat_cache = fc }) ->
is { inert_flat_cache = insertFamHead fc fam_ty (ctev,rhs_ty) }
-- Instantiations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment