Performance bug fixes

parent e6e40cc1
...@@ -568,6 +568,7 @@ dischargeWorkItem = mkIRStop KeepInert emptyCCan ...@@ -568,6 +568,7 @@ dischargeWorkItem = mkIRStop KeepInert emptyCCan
noInteraction :: Monad m => WorkItem -> m InteractResult noInteraction :: Monad m => WorkItem -> m InteractResult
noInteraction workItem = mkIRContinue workItem KeepInert emptyCCan noInteraction workItem = mkIRContinue workItem KeepInert emptyCCan
data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
--------------------------------------------------- ---------------------------------------------------
-- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop -- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop
...@@ -757,10 +758,10 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 ...@@ -757,10 +758,10 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 }) , cc_tyargs = args2, cc_rhs = xi2 })
| fl1 `canRewrite` fl2 && lhss_match | fl1 `canRewrite` fl2 && lhss_match
= do { cans <- rewriteEqLHS (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
; mkIRStop KeepInert cans } ; mkIRStop KeepInert cans }
| fl2 `canRewrite` fl1 && lhss_match | fl2 `canRewrite` fl1 && lhss_match
= do { cans <- rewriteEqLHS (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue workItem DropInert cans } ; mkIRContinue workItem DropInert cans }
where where
lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
...@@ -769,7 +770,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc ...@@ -769,7 +770,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc
workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
-- Check for matching LHS -- Check for matching LHS
| fl1 `canRewrite` fl2 && tv1 == tv2 | fl1 `canRewrite` fl2 && tv1 == tv2
= do { cans <- rewriteEqLHS (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
; mkIRStop KeepInert cans } ; mkIRStop KeepInert cans }
{- {-
...@@ -781,7 +782,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc ...@@ -781,7 +782,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc
; mkIRStop KeepInert cans } ; mkIRStop KeepInert cans }
-} -}
| fl2 `canRewrite` fl1 && tv1 == tv2 | fl2 `canRewrite` fl1 && tv1 == tv2
= do { cans <- rewriteEqLHS (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue workItem DropInert cans } ; mkIRContinue workItem DropInert cans }
-- Check for rewriting RHS -- Check for rewriting RHS
...@@ -886,21 +887,47 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) ...@@ -886,21 +887,47 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
xi2' = substTyWith [tv1] [xi1] xi2 xi2' = substTyWith [tv1] [xi1] xi2
co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1] co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
rewriteEqLHS :: (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
-- Used to ineratct two equalities of the following form: -- Used to ineratct two equalities of the following form:
-- First Equality: co1: (XXX ~ xi1) -- First Equality: co1: (XXX ~ xi1)
-- Second Equality: cv2: (XXX ~ xi2) -- Second Equality: cv2: (XXX ~ xi2)
-- Where the cv1 `canRewrite` cv2 equality -- Where the cv1 `canRewrite` cv2 equality
rewriteEqLHS (co1,xi1) (cv2,gw,xi2) -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
= do { cv2' <- if isWanted gw then -- depends on whether the left or the right equality comes from the inert set.
-- We must:
-- prefer to create (xi2 ~ xi1) if the first comes from the inert
-- prefer to create (xi1 ~ xi2) if the second comes from the inert
rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
= do { cv2' <- case (isWanted gw, which) of
(True,LeftComesFromInert) ->
do { cv2' <- newWantedCoVar xi2 xi1
; setWantedCoBind cv2 $
co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
; return cv2' }
(True,RightComesFromInert) ->
do { cv2' <- newWantedCoVar xi1 xi2 do { cv2' <- newWantedCoVar xi1 xi2
; setWantedCoBind cv2 $ ; setWantedCoBind cv2 $
co1 `mkTransCoercion` mkCoVarCoercion cv2' co1 `mkTransCoercion` mkCoVarCoercion cv2'
; return cv2' } ; return cv2' }
else newGivOrDerCoVar xi1 xi2 $ (False,LeftComesFromInert) ->
newGivOrDerCoVar xi2 xi1 $
mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
(False,RightComesFromInert) ->
newGivOrDerCoVar xi1 xi2 $
mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
; mkCanonical gw cv2' } ; mkCanonical gw cv2' }
-- ->
-- if isWanted gw then
-- do { cv2' <- newWantedCoVar xi1 xi2
-- ; setWantedCoBind cv2 $
-- co1 `mkTransCoercion` mkCoVarCoercion cv2'
-- ; return cv2' }
-- else newGivOrDerCoVar xi1 xi2 $
-- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
-- ; mkCanonical gw cv2' }
solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
-- First argument inert, second argument workitem. They both represent -- First argument inert, second argument workitem. They both represent
......
...@@ -891,6 +891,7 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) ...@@ -891,6 +891,7 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
-- Check (a) that tv doesn't occur in ty (occurs check) -- Check (a) that tv doesn't occur in ty (occurs check)
-- (b) that ty is a monotype -- (b) that ty is a monotype
-- (c) that kind(ty) is a sub-kind of kind(tv) -- (c) that kind(ty) is a sub-kind of kind(tv)
-- (d) that ty does not contain any type families, see Note [SHARING]
-- --
-- We have two possible outcomes: -- We have two possible outcomes:
-- (1) Return the type to update the type variable with, -- (1) Return the type to update the type variable with,
...@@ -909,12 +910,52 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) ...@@ -909,12 +910,52 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
checkTauTvUpdate tv ty checkTauTvUpdate tv ty
= do { ty' <- zonkTcType ty = do { ty' <- zonkTcType ty
; if not (tv `elemVarSet` tyVarsOfType ty') ; if ok ty' && (typeKind ty' `isSubKind` tyVarKind tv)
&& typeKind ty' `isSubKind` tyVarKind tv
then return (Just ty') then return (Just ty')
else return Nothing } else return Nothing }
where ok :: TcType -> Bool
-- Check that tv is not among the free variables of
-- the type and that the type is type-family-free.
ok (TyVarTy tv') = not (tv == tv')
ok (TyConApp tc tys) = all ok tys && not (isSynFamilyTyCon tc)
ok (PredTy sty) = ok_pred sty
ok (FunTy arg res) = ok arg && ok res
ok (AppTy fun arg) = ok fun && ok arg
ok (ForAllTy _tv1 ty1) = ok ty1
ok_pred (IParam _ ty) = ok ty
ok_pred (ClassP _ tys) = all ok tys
ok_pred (EqPred ty1 ty2) = ok ty1 && ok ty2
\end{code} \end{code}
Note [SHARING]
~~~~~~~~~~~~~~
We must avoid eagerly unifying type variables to types that contain function symbols,
because this may lead to loss of sharing, and in turn, in very poor performance of the
constraint simplifier. Assume that we have a wanted constraint:
{
m1 ~ [F m2],
m2 ~ [F m3],
m3 ~ [F m4],
D m1,
D m2,
D m3
}
where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m2],
then, after zonking, our constraint simplifier will be faced with the following wanted
constraint:
{
D [F [F [F m4]]],
D [F [F m4]],
D [F m4]
}
which has to be flattened by the constraint solver. However, because the sharing is lost,
an polynomially larger number of flatten skolems will be created and the constraint sets
we are working with will be polynomially larger.
Instead, if we defer the unifications m1 := [F m2], etc. we will only be generating three
flatten skolems, which is the maximum possible sharing arising from the original constraint.
\begin{code} \begin{code}
data LookupTyVarResult -- The result of a lookupTcTyVar call data LookupTyVarResult -- The result of a lookupTcTyVar call
......
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