noInteraction :: Monad m => WorkItem -> m InteractResult
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
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
| 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 }
| 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 }
where
lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
-- Check for matching LHS
| 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 }
-}
| 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 }
-- Check for rewriting RHS
xi2' = substTyWith [tv1] [xi1] xi2
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:
-- First Equality: co1: (XXX ~ xi1)
-- Second Equality: cv2: (XXX ~ xi2)
-- Where the cv1 `canRewrite` cv2 equality
-rewriteEqLHS (co1,xi1) (cv2,gw,xi2)
- = do { 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
+-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
+-- 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
+ ; setWantedCoBind cv2 $
+ co1 `mkTransCoercion` mkCoVarCoercion cv2'
+ ; return cv2' }
+ (False,LeftComesFromInert) ->
+ newGivOrDerCoVar xi2 xi1 $
+ mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
+ (False,RightComesFromInert) ->
+ newGivOrDerCoVar xi1 xi2 $
+ mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion 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
-- First argument inert, second argument workitem. They both represent
-- Check (a) that tv doesn't occur in ty (occurs check)
-- (b) that ty is a monotype
-- (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:
-- (1) Return the type to update the type variable with,
checkTauTvUpdate tv ty
= do { ty' <- zonkTcType ty
- ; if not (tv `elemVarSet` tyVarsOfType ty')
- && typeKind ty' `isSubKind` tyVarKind tv
+ ; if ok ty' && (typeKind ty' `isSubKind` tyVarKind tv)
then return (Just ty')
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}
+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}
data LookupTyVarResult -- The result of a lookupTcTyVar call
projects / ghc-hetmet.git / commitdiff