X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=529d62488ac50d348ddad62ec47119e69f4db678;hb=25bff7fe1a22edbafa188af8d844c67057fa5eb8;hp=0fd72644a38d21e0e715a5b8c04b99b764208b71;hpb=bff88b3a5bf96eea57e99a09774a74bd18cf4e13;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 0fd7264..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 - ; free_tvs <- zonkTcTyVarsAndFV free_tvs - ; let untch = 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 untch $ - thing_inside + ; ((result, untch), wanted) <- captureConstraints $ + captureUntouchables $ + thing_inside ; if isEmptyBag wanted && not (hasEqualities given) -- Optimisation : if there are no wanteds, and the givens @@ -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,9 +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) --- (d) that ty does not contain any type families, see Note [SHARING] +-- (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, @@ -910,26 +918,66 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) checkTauTvUpdate tv ty = do { ty' <- zonkTcType ty - ; if ok 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 -> 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 + + 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 [SHARING] +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