Commit 4bc84da3 authored by dimitris's avatar dimitris

Solved goal caching and zonking optimisations.

1) Stopped rewriting and caching solveds in the inerts because
profiling showed that a lot of time was spent on rewriting
already solved goals.

2) Optimisations in zonkEvBinds for common-case
evidence bindings generated from the constraint solver.

3) Now solved goals cache their evidence terms, so that we can more
aggressively optimize Refl coercions during constraint solving.
This patch also includes a rewrite of rewriteInertEqsFromInertEq
which greatly improves its efficiency.
parent f3183d9a
This diff is collapsed.
......@@ -280,7 +280,10 @@ zonkEvBndr :: ZonkEnv -> EvVar -> TcM EvVar
-- Works for dictionaries and coercions
-- Does not extend the ZonkEnv
zonkEvBndr env var
= do { ty <- zonkTcTypeToType env (varType var)
= do { let var_ty = varType var
; ty <-
{-# SCC "zonkEvBndr_zonkTcTypeToType" #-}
zonkTcTypeToType env var_ty
; return (setVarType var ty) }
zonkEvVarOcc :: ZonkEnv -> EvVar -> EvVar
......@@ -1103,7 +1106,8 @@ zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref
zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind)
zonkEvBinds env binds
= fixM (\ ~( _, new_binds) -> do
= {-# SCC "zonkEvBinds" #-}
fixM (\ ~( _, new_binds) -> do
{ let env1 = extendIdZonkEnv env (collect_ev_bndrs new_binds)
; binds' <- mapBagM (zonkEvBind env1) binds
; return (env1, binds') })
......@@ -1113,10 +1117,31 @@ zonkEvBinds env binds
add (EvBind var _) vars = var : vars
zonkEvBind :: ZonkEnv -> EvBind -> TcM EvBind
zonkEvBind env (EvBind var term)
= do { var' <- zonkEvBndr env var
; term' <- zonkEvTerm env term
; return (EvBind var' term') }
= case term of
-- Fast path for reflexivity coercions:
EvCoercionBox co
| Just ty <- isReflCo_maybe co
->
do { zty <- zonkTcTypeToType env ty
; let var' = setVarType var (mkEqPred (zty,zty))
; return (EvBind var' (EvCoercionBox (mkReflCo zty))) }
-- Fast path for variable-variable bindings
-- NB: could be optimized further! (e.g. SymCo cv)
| Just {} <- getCoVar_maybe co
-> do { term'@(EvCoercionBox (CoVarCo cv')) <- zonkEvTerm env term
; let var' = setVarType var (varType cv')
; return (EvBind var' term') }
-- Ugly safe and slow path
_ -> do { var' <- {-# SCC "zonkEvBndr" #-} zonkEvBndr env var
; term' <- zonkEvTerm env term
; return (EvBind var' term')
}
\end{code}
%************************************************************************
......@@ -1186,9 +1211,14 @@ mkZonkTcTyVar unbound_mvar_fn unbound_ivar_fn
FlatSkol ty -> zonkType zonk_tv ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> do { kind <- zonkType zonk_tv (tyVarKind tv)
Flexi -> do { kind <- {-# SCC "zonkKind1" #-}
zonkType zonk_tv (tyVarKind tv)
; unbound_mvar_fn (setTyVarKind tv kind) }
Indirect ty -> zonkType zonk_tv ty }
Indirect ty -> do { zty <- zonkType zonk_tv ty
-- Small optimisation: shortern-out indirect steps
-- so that the old type may be more easily collected.
; writeMutVar ref (Indirect zty)
; return zty } }
zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
zonkTcTypeToType (ZonkEnv zonk_unbound_tyvar tv_env _id_env)
......
This diff is collapsed.
......@@ -71,7 +71,7 @@ module TcRnTypes(
SkolemInfo(..),
CtFlavor(..), pprFlavorArising, isWanted,
isGivenOrSolved, isGiven_maybe,
isGivenOrSolved, isGiven_maybe, isSolved,
isDerived,
-- Pretty printing
......@@ -1210,14 +1210,17 @@ data CtFlavor
data GivenKind
= GivenOrig -- Originates in some given, such as signature or pattern match
| GivenSolved -- Is given as result of being solved, maybe provisionally on
-- some other wanted constraints.
| GivenSolved (Maybe EvTerm)
-- Is given as result of being solved, maybe provisionally on
-- some other wanted constraints. We cache the evidence term
-- sometimes here as well /as well as/ in the EvBinds,
-- see note [Optimizing Spontaneously Solved Coercions]
instance Outputable CtFlavor where
ppr (Given _ GivenOrig) = ptext (sLit "[G]")
ppr (Given _ GivenSolved) = ptext (sLit "[S]") -- Print [S] for Given/Solved's
ppr (Wanted {}) = ptext (sLit "[W]")
ppr (Derived {}) = ptext (sLit "[D]")
ppr (Given _ GivenOrig) = ptext (sLit "[G]")
ppr (Given _ (GivenSolved {})) = ptext (sLit "[S]") -- Print [S] for Given/Solved's
ppr (Wanted {}) = ptext (sLit "[W]")
ppr (Derived {}) = ptext (sLit "[D]")
pprFlavorArising :: CtFlavor -> SDoc
pprFlavorArising (Derived wl) = pprArisingAt wl
......@@ -1232,6 +1235,10 @@ isGivenOrSolved :: CtFlavor -> Bool
isGivenOrSolved (Given {}) = True
isGivenOrSolved _ = False
isSolved :: CtFlavor -> Bool
isSolved (Given _ (GivenSolved {})) = True
isSolved _ = False
isGiven_maybe :: CtFlavor -> Maybe GivenKind
isGiven_maybe (Given _ gk) = Just gk
isGiven_maybe _ = Nothing
......
......@@ -47,8 +47,6 @@ module TcSMonad (
-- Setting evidence variables
setEqBind,
setIPBind,
setDictBind,
setEvBind,
setWantedTyBind,
......@@ -62,7 +60,7 @@ module TcSMonad (
-- Inerts
InertSet(..),
getInertEqs, rewriteFromInertEqs, liftInertEqsTy,
getInertEqs, liftInertEqsTy,
emptyInert, getTcSInerts, updInertSet, extractUnsolved,
extractUnsolvedTcS, modifyInertTcS,
updInertSetTcS, partitionCCanMap, partitionEqMap,
......@@ -125,7 +123,7 @@ import Bag
import MonadUtils
import VarSet
import Pair ( pSnd )
-- import Pair ( pSnd )
import FastString
import Util
......@@ -493,9 +491,17 @@ updInertSet is item
| isCTyEqCan item
= let upd_err a b = pprPanic "updInertSet" $
vcat [text "Multiple inert equalities:", ppr a, ppr b]
-- If evidence is cached, pick it up from the flavor!
coercion
| Just (GivenSolved (Just (EvCoercionBox co))) <- isGiven_maybe (cc_flavor item)
= co
| otherwise
= mkEqVarLCo (cc_id item)
eqs' = extendVarEnv_C upd_err (inert_eqs is)
(cc_tyvar item)
(item, mkEqVarLCo (cc_id item))
(item, coercion)
inscope' = extendInScopeSetSet (inert_eq_tvs is) (tyVarsOfCt item)
in is { inert_eqs = eqs', inert_eq_tvs = inscope' }
......@@ -668,11 +674,11 @@ combineCtLoc (Derived loc ) _ = loc
combineCtLoc _ (Derived loc ) = loc
combineCtLoc _ _ = panic "combineCtLoc: both given"
mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
mkSolvedFlavor :: CtFlavor -> SkolemInfo -> EvTerm -> CtFlavor
-- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
mkSolvedFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
mkSolvedFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenSolved
mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
mkSolvedFlavor (Wanted loc) sk evterm = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm))
mkSolvedFlavor (Derived loc) sk evterm = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm))
mkSolvedFlavor fl@(Given {}) _sk _evterm = pprPanic "Solving a given constraint!" $ ppr fl
mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig
......@@ -1058,8 +1064,8 @@ getTcEvBindsMap
; wrapTcS $ TcM.readTcRef ev_ref }
setEqBind :: EqVar -> LCoercion -> TcS ()
setEqBind eqv co = setEvBind eqv (EvCoercionBox co)
setEqBind :: EqVar -> LCoercion -> CtFlavor -> TcS CtFlavor
setEqBind eqv co fl = setEvBind eqv (EvCoercionBox co) fl
setWantedTyBind :: TcTyVar -> TcType -> TcS ()
-- Add a type binding
......@@ -1075,15 +1081,10 @@ setWantedTyBind tv ty
, text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
setIPBind :: EvVar -> EvTerm -> TcS ()
setIPBind = setEvBind
setDictBind :: EvVar -> EvTerm -> TcS ()
setDictBind = setEvBind
setEvBind :: EvVar -> EvTerm -> TcS ()
-- Internal
setEvBind ev t
setEvBind :: EvVar -> EvTerm -> CtFlavor -> TcS CtFlavor
-- If the flavor is Solved, we cache the new evidence term inside the returned flavor
setEvBind ev t fl
= do { tc_evbinds <- getTcEvBinds
; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
......@@ -1092,6 +1093,11 @@ setEvBind ev t
; let cycle = any (reaches binds) (evterm_evs t)
; when cycle (fail_if_co_loop binds)
#endif
; return $
case fl of
Given gl (GivenSolved _)
-> Given gl (GivenSolved (Just t))
_ -> fl
}
#ifdef DEBUG
......@@ -1275,7 +1281,9 @@ newEvVar :: CtFlavor -> TcPredType -> TcS EvVarCreated
-- the call sites for this invariant to be quickly restored.
newEvVar fl pty
| isGivenOrSolved fl -- Create new variable and update the cache
= do { eref <- getTcSEvVarCache
= do {
{- We lose a lot of time if we enable this check:
eref <- getTcSEvVarCache
; ecache <- wrapTcS (TcM.readTcRef eref)
; case lookupTM pty (evc_cache ecache) of
Just (_,cached_fl)
......@@ -1283,11 +1291,13 @@ newEvVar fl pty
-> pprTrace "Interesting: given newEvVar, missed caching opportunity!" empty $
return ()
_ -> return ()
; new <- forceNewEvVar fl pty
-}
new <- forceNewEvVar fl pty
; return (EvVarCreated True new) }
| otherwise -- Otherwise lookup first
= do { eref <- getTcSEvVarCache
= {-# SCC "newEvVarWanted" #-}
do { eref <- getTcSEvVarCache
; ecache <- wrapTcS (TcM.readTcRef eref)
; case lookupTM pty (evc_cache ecache) of
Just (cached_evvar, cached_flavor)
......@@ -1338,9 +1348,10 @@ updateCache ecache (ev,fl,pty)
ecache' = alterTM pty (\_ -> Just (ev,fl)) $
evc_cache ecache
delCachedEvVar :: EvVar -> TcS ()
delCachedEvVar ev
= do { eref <- getTcSEvVarCache
delCachedEvVar :: EvVar -> CtFlavor -> TcS ()
delCachedEvVar ev _fl
= {-# SCC "delCachedEvVarOther" #-}
do { eref <- getTcSEvVarCache
; ecache <- wrapTcS (TcM.readTcRef eref)
; wrapTcS $ TcM.writeTcRef eref (delFromCache ecache ev) }
......@@ -1377,13 +1388,13 @@ pprEvVarCache tm = ppr (foldTM mk_pair tm [])
where mk_pair (co,_) cos = (co, liftedCoercionKind co) : cos
newGivenEqVar :: CtFlavor -> TcType -> TcType -> Coercion -> TcS EvVar
newGivenEqVar :: CtFlavor -> TcType -> TcType -> Coercion -> TcS (CtFlavor,EvVar)
-- Pre: fl is Given
newGivenEqVar fl ty1 ty2 co
= do { ecv <- newEqVar fl ty1 ty2
; let v = evc_the_evvar ecv -- Will be a new EvVar by post of newEvVar
; setEvBind v (EvCoercionBox co)
; return v }
; fl' <- setEvBind v (EvCoercionBox co) fl
; return (fl',v) }
newEqVar :: CtFlavor -> TcType -> TcType -> TcS EvVarCreated
newEqVar fl ty1 ty2
......@@ -1447,6 +1458,7 @@ getInertEqs :: TcS (TyVarEnv (Ct,Coercion), InScopeSet)
getInertEqs = do { inert <- getTcSInerts
; return (inert_eqs inert, inert_eq_tvs inert) }
{-- UNSAFE in the prsence of Solved flavors! Don't use!
rewriteFromInertEqs :: (TyVarEnv (Ct,Coercion), InScopeSet)
-- Precondition: Ct are CTyEqCans only!
-> CtFlavor
......@@ -1458,7 +1470,7 @@ rewriteFromInertEqs (subst,inscope) fl v
; if isReflCo co then return (v,True)
else do { traceTcS "rewriteFromInertEqs" $
text "Original item =" <+> ppr v <+> dcolon <+> ppr (evVarPred v)
; delCachedEvVar v
; delCachedEvVar v fl
; evc <- newEvVar fl (pSnd (liftedCoercionKind co))
; let v' = evc_the_evvar evc
; if isNewEvVar evc then
......@@ -1476,7 +1488,7 @@ rewriteFromInertEqs (subst,inscope) fl v
_ -> return ()
; return (v',True) } -- As if rewriting never happened?
} }
--}
-- See Note [LiftInertEqs]
liftInertEqsTy :: (TyVarEnv (Ct,Coercion),InScopeSet)
......
......@@ -1046,7 +1046,11 @@ solveCTyFunEqs cts
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
; setEqBind cv (mkReflCo ty) }
; _ <- setEqBind cv (mkReflCo ty) $
(Wanted $ panic "Met an already solved function equality!")
; return () -- Don't care about flavors etc this is
-- the last thing happening
}
------------
type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
......
......@@ -22,6 +22,7 @@ module Coercion (
-- ** Functions over coercions
coVarKind,
coercionType, coercionKind, coercionKinds, isReflCo, liftedCoercionKind,
isReflCo_maybe,
mkCoercionType,
-- ** Constructing coercions
......
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