Performance bug fixes

2 files changed, 83 insertions, 15 deletions

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index ccf1ee102e..b079368816 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -568,6 +568,7 @@ dischargeWorkItem = mkIRStop KeepInert emptyCCan
 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 
@@ -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
                                , 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) 
@@ -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 })
 -- 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 } 
 
 {-
@@ -781,7 +782,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc
        ; 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 
@@ -886,21 +887,47 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
     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 
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 348c70e4d4..0fd72644a3 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -891,6 +891,7 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 -- 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, 
@@ -909,12 +910,52 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 
 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