X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=529d62488ac50d348ddad62ec47119e69f4db678;hb=25bff7fe1a22edbafa188af8d844c67057fa5eb8;hp=340be9afb52717c3da4253961f447f5139ecdb14;hpb=af2e0d24abe49e06fdee4a95530af8a5c33da4a3;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 340be9a..529d624 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -30,7 +30,6 @@ import TypeRep import TcErrors ( typeExtraInfoMsg, unifyCtxt ) import TcMType -import TcEnv import TcIface import TcRnMonad import TcType @@ -46,6 +45,8 @@ import Name import ErrUtils import BasicTypes import Bag + +import Maybes ( allMaybes ) import Util import Outputable import FastString @@ -410,16 +411,16 @@ checkConstraints skol_info free_tvs skol_tvs given thing_inside newImplication :: SkolemInfo -> TcTyVarSet -> [TcTyVar] -> [EvVar] -> TcM result -> TcM (TcEvBinds, WantedConstraints, result) -newImplication skol_info free_tvs skol_tvs given thing_inside +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 $ - thing_inside + ; ((result, untch), wanted) <- captureConstraints $ + captureUntouchables $ + thing_inside ; if isEmptyBag wanted && not (hasEqualities given) -- Optimisation : if there are no wanteds, and the givens @@ -431,8 +432,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 +446,6 @@ newImplication skol_info free_tvs skol_tvs given thing_inside ; return (TcEvBinds ev_binds_var, unitBag (WcImplic implic), result) } } \end{code} - %************************************************************************ %* * Boxy unification @@ -575,7 +576,16 @@ uType_np origin orig_ty1 orig_ty2 -- Predicates go origin (PredTy p1) (PredTy p2) = uPred origin p1 p2 - -- Functions; just check the two parts + -- Coercion functions: (t1a ~ t1b) => t1c ~ (t2a ~ t2b) => t2c + go origin ty1 ty2 + | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1, + Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2 + = do { co1 <- uType origin t1a t2a + ; co2 <- uType origin t1b t2b + ; co3 <- uType origin t1c t2c + ; return $ mkCoPredCoI co1 co2 co3 } + + -- Functions (or predicate functions) just check the two parts go origin (FunTy fun1 arg1) (FunTy fun2 arg2) = do { coi_l <- uType origin fun1 fun2 ; coi_r <- uType origin arg1 arg2 @@ -607,7 +617,7 @@ uType_np origin orig_ty1 orig_ty2 ; return $ mkAppTyCoI coi_s coi_t } go _ ty1 ty2 - | isSigmaTy ty1 || isSigmaTy ty2 + | tcIsForAllTy ty1 || tcIsForAllTy ty2 = unifySigmaTy origin ty1 ty2 -- Anything else fails @@ -624,12 +634,11 @@ unifySigmaTy origin ty1 ty2 in_scope = mkInScopeSet (mkVarSet skol_tvs) phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1 phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2 - untch = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 - - ; (coi, lie) <- getConstraints $ - setUntouchables untch $ - uType origin phi1 phi2 +-- untch = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 + ; ((coi, _untch), lie) <- captureConstraints $ + captureUntouchables $ + uType origin phi1 phi2 -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a) ; let bad_lie = filterBag is_bad lie is_bad w = any (`elemVarSet` tyVarsOfWanted w) skol_tvs @@ -889,8 +898,8 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) -- (checkTauTvUpdate tv ty) -- We are about to update the TauTv tv with ty. -- 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) +-- (b) that kind(ty) is a sub-kind of kind(tv) +-- (c) that ty does not contain any type families, see Note [Type family sharing] -- -- We have two possible outcomes: -- (1) Return the type to update the type variable with, @@ -909,12 +918,92 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) checkTauTvUpdate tv ty = do { ty' <- zonkTcType ty - ; if not (tv `elemVarSet` tyVarsOfType ty') - && typeKind ty' `isSubKind` tyVarKind tv - then return (Just ty') + ; if typeKind ty' `isSubKind` tyVarKind tv then + case ok ty' of + Nothing -> return Nothing + Just ty'' -> return (Just ty'') else return Nothing } + + where ok :: TcType -> Maybe TcType + ok (TyVarTy tv') | not (tv == tv') = Just (TyVarTy tv') + ok this_ty@(TyConApp tc tys) + | not (isSynFamilyTyCon tc), Just tys' <- allMaybes (map ok tys) + = Just (TyConApp tc tys') + | isSynTyCon tc, Just ty_expanded <- tcView this_ty + = ok ty_expanded -- See Note [Type synonyms and the occur check] + ok (PredTy sty) | Just sty' <- ok_pred sty = Just (PredTy sty') + ok (FunTy arg res) | Just arg' <- ok arg, Just res' <- ok res + = Just (FunTy arg' res') + ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg + = Just (AppTy fun' arg') + ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1') + -- Fall-through + ok _ty = Nothing + + ok_pred (IParam nm ty) | Just ty' <- ok ty = Just (IParam nm ty') + ok_pred (ClassP cl tys) + | Just tys' <- allMaybes (map ok tys) + = Just (ClassP cl tys') + ok_pred (EqPred ty1 ty2) + | Just ty1' <- ok ty1, Just ty2' <- ok ty2 + = Just (EqPred ty1' ty2') + -- Fall-through + ok_pred _pty = Nothing + \end{code} +Note [Type synonyms and the occur check] +~~~~~~~~~~~~~~~~~~~~ +Generally speaking we need to update a variable with type synonyms not expanded, which +improves later error messages, except for when looking inside a type synonym may help resolve +a spurious occurs check error. Consider: + type A a = () + + f :: (A a -> a -> ()) -> () + f = \ _ -> () + + x :: () + x = f (\ x p -> p x) + +We will eventually get a constraint of the form t ~ A t. The ok function above will +properly expand the type (A t) to just (), which is ok to be unified with t. If we had +unified with the original type A t, we would lead the type checker into an infinite loop. + +Hence, if the occurs check fails for a type synonym application, then (and *only* then), +the ok function expands the synonym to detect opportunities for occurs check success using +the underlying definition of the type synonym. + +The same applies later on in the constraint interaction code; see TcInteract, +function @occ_check_ok@. + + +Note [Type family 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 +1283,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