X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=0fd72644a38d21e0e715a5b8c04b99b764208b71;hb=bff88b3a5bf96eea57e99a09774a74bd18cf4e13;hp=340be9afb52717c3da4253961f447f5139ecdb14;hpb=af2e0d24abe49e06fdee4a95530af8a5c33da4a3;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 340be9a..0fd7264 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -413,12 +413,12 @@ newImplication :: SkolemInfo -> TcTyVarSet -> [TcTyVar]
 newImplication skol_info free_tvs skol_tvs given thing_inside
   = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
     ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
-    do { gbl_tvs <- tcGetGlobalTyVars
-       ; lcl_env <- getLclTypeEnv
-       ; let all_free_tvs = gbl_tvs `unionVarSet` free_tvs
+    do { gbl_tvs  <- tcGetGlobalTyVars
+       ; free_tvs <- zonkTcTyVarsAndFV free_tvs
+       ; let untch = gbl_tvs `unionVarSet` free_tvs
 
        ; (result, wanted) <- getConstraints               $ 
-                             setUntouchables all_free_tvs $
+                             setUntouchables untch $
                              thing_inside
 
        ; if isEmptyBag wanted && not (hasEqualities given) 
@@ -431,8 +431,9 @@ newImplication skol_info free_tvs skol_tvs given thing_inside
             return (emptyTcEvBinds, emptyWanteds, result)
          else do
        { ev_binds_var <- newTcEvBinds
+       ; lcl_env <- getLclTypeEnv
        ; loc <- getCtLoc skol_info
-       ; let implic = Implic { ic_env_tvs = all_free_tvs
+       ; let implic = Implic { ic_untch = untch
              		     , ic_env = lcl_env
              		     , ic_skols = mkVarSet skol_tvs
              		     , ic_scoped = panic "emitImplication"
@@ -444,7 +445,6 @@ newImplication skol_info free_tvs skol_tvs given thing_inside
        ; return (TcEvBinds ev_binds_var, unitBag (WcImplic implic), result) } }
 \end{code}
 
-
 %************************************************************************
 %*                                                                      *
                 Boxy unification
@@ -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
@@ -1194,7 +1235,7 @@ checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
 -- The extra_tvs can include boxy type variables;
 --      e.g. TcMatches.tcCheckExistentialPat
 checkSigTyVarsWrt extra_tvs sig_tvs
-  = do  { extra_tvs' <- zonkTcTyVarsAndFV (varSetElems extra_tvs)
+  = do  { extra_tvs' <- zonkTcTyVarsAndFV extra_tvs
         ; check_sig_tyvars extra_tvs' sig_tvs }
 
 check_sig_tyvars