X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=ade2db0d4935692b3334cb8f2a492a2ee553d77a;hp=0fd72644a38d21e0e715a5b8c04b99b764208b71;hb=b10d7d079ec9c3fc22d4700fe484dd297bddb805;hpb=bff88b3a5bf96eea57e99a09774a74bd18cf4e13 diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 0fd7264..ade2db0 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 @@ -303,9 +304,8 @@ tcSubType :: CtOrigin -> SkolemInfo -> TcSigmaType -> TcSigmaType -> TcM HsWrapp -- Returns a wrapper of shape ty_actual ~ ty_expected tcSubType origin skol_info ty_actual ty_expected | isSigmaTy ty_actual - = do { let extra_tvs = tyVarsOfType ty_actual - ; (sk_wrap, inst_wrap) - <- tcGen skol_info extra_tvs ty_expected $ \ _ sk_rho -> do + = do { (sk_wrap, inst_wrap) + <- tcGen skol_info ty_expected $ \ _ sk_rho -> do { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual ; coi <- unifyType in_rho sk_rho ; return (coiToHsWrapper coi <.> in_wrap) } @@ -353,14 +353,14 @@ wrapFunResCoercion arg_tys co_fn_res %************************************************************************ \begin{code} -tcGen :: SkolemInfo -> TcTyVarSet -> TcType +tcGen :: SkolemInfo -> TcType -> ([TcTyVar] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result) -- The expression has type: spec_ty -> expected_ty -tcGen skol_info extra_tvs - expected_ty thing_inside -- We expect expected_ty to be a forall-type - -- If not, the call is a no-op +tcGen skol_info expected_ty thing_inside + -- We expect expected_ty to be a forall-type + -- If not, the call is a no-op = do { traceTc "tcGen" empty ; (wrap, tvs', given, rho') <- deeplySkolemise skol_info expected_ty @@ -369,7 +369,7 @@ tcGen skol_info extra_tvs text "expected_ty" <+> ppr expected_ty, text "inst ty" <+> ppr tvs' <+> ppr rho' ] - -- In 'free_tvs' we must check that the "forall_tvs" havn't been constrained + -- Generally we must check that the "forall_tvs" havn't been constrained -- The interesting bit here is that we must include the free variables -- of the expected_ty. Here's an example: -- runST (newVar True) @@ -377,10 +377,12 @@ tcGen skol_info extra_tvs -- for (newVar True), with s fresh. Then we unify with the runST's arg type -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool. -- So now s' isn't unconstrained because it's linked to a. - -- Conclusion: pass the free vars of the expected_ty to checkConsraints - ; let free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs + -- + -- However [Oct 10] now that the untouchables are a range of + -- TcTyVars, all tihs is handled automatically with no need for + -- extra faffing around - ; (ev_binds, result) <- checkConstraints skol_info free_tvs tvs' given $ + ; (ev_binds, result) <- checkConstraints skol_info tvs' given $ thing_inside tvs' rho' ; return (wrap <.> mkWpLet ev_binds, result) } @@ -388,38 +390,32 @@ tcGen skol_info extra_tvs -- often empty, in which case mkWpLet is a no-op checkConstraints :: SkolemInfo - -> TcTyVarSet -- Free variables (other than the type envt) - -- for the skolem escape check -> [TcTyVar] -- Skolems -> [EvVar] -- Given -> TcM result -> TcM (TcEvBinds, result) -checkConstraints skol_info free_tvs skol_tvs given thing_inside +checkConstraints skol_info skol_tvs given thing_inside | null skol_tvs && null given = do { res <- thing_inside; return (emptyTcEvBinds, res) } -- Just for efficiency. We check every function argument with -- tcPolyExpr, which uses tcGen and hence checkConstraints. | otherwise - = do { (ev_binds, wanted, result) <- newImplication skol_info free_tvs + = do { (ev_binds, wanted, result) <- newImplication skol_info skol_tvs given thing_inside ; emitConstraints wanted ; return (ev_binds, result) } -newImplication :: SkolemInfo -> TcTyVarSet -> [TcTyVar] +newImplication :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM result -> TcM (TcEvBinds, WantedConstraints, result) -newImplication skol_info free_tvs skol_tvs given thing_inside +newImplication skol_info 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 - - ; (result, wanted) <- getConstraints $ - setUntouchables untch $ - thing_inside + do { ((result, untch), wanted) <- captureConstraints $ + captureUntouchables $ + thing_inside ; if isEmptyBag wanted && not (hasEqualities given) -- Optimisation : if there are no wanteds, and the givens @@ -575,7 +571,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 +612,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 +629,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 +893,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 +913,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