X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=ade2db0d4935692b3334cb8f2a492a2ee553d77a;hp=3360f5dd176d52577f96b092ce2bbb7950e388d2;hb=b10d7d079ec9c3fc22d4700fe484dd297bddb805;hpb=d2ce0f52d42edf32bb9f13796e6ba6edba8bd516 diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 3360f5d..ade2db0 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -14,9 +14,6 @@ module TcUnify ( -- Various unifications unifyType, unifyTypeList, unifyTheta, unifyKind, - -- Occurs check error - typeExtraInfoMsg, emitMisMatchErr, - -------------------------------- -- Holes tcInfer, @@ -31,9 +28,8 @@ module TcUnify ( import HsSyn import TypeRep -import TcErrors ( typeExtraInfoMsg ) +import TcErrors ( typeExtraInfoMsg, unifyCtxt ) import TcMType -import TcEnv import TcIface import TcRnMonad import TcType @@ -49,6 +45,8 @@ import Name import ErrUtils import BasicTypes import Bag + +import Maybes ( allMaybes ) import Util import Outputable import FastString @@ -306,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) } @@ -356,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 @@ -372,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) @@ -380,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) } @@ -391,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 - ; lcl_env <- getLclTypeEnv - ; let all_free_tvs = gbl_tvs `unionVarSet` free_tvs - - ; (result, wanted) <- getConstraints $ - setUntouchables all_free_tvs $ - 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 @@ -434,8 +427,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" @@ -447,7 +441,6 @@ newImplication skol_info free_tvs skol_tvs given thing_inside ; return (TcEvBinds ev_binds_var, unitBag (WcImplic implic), result) } } \end{code} - %************************************************************************ %* * Boxy unification @@ -526,13 +519,15 @@ uType, uType_np, uType_defer -------------- -- It is always safe to defer unification to the main constraint solver -- See Note [Deferred unification] -uType_defer origin ty1 ty2 +uType_defer (item : origin) ty1 ty2 = do { co_var <- newWantedCoVar ty1 ty2 ; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin]) - ; loc <- getCtLoc TypeEqOrigin + ; loc <- getCtLoc (TypeEqOrigin item) ; wrapEqCtxt origin $ emitConstraint (WcEvVar (WantedEvVar co_var loc)) ; return $ ACo $ mkTyVarTy co_var } +uType_defer [] _ _ + = panic "uType_defer" -------------- -- Push a new item on the origin stack (the most common case) @@ -576,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 @@ -608,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 @@ -625,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 @@ -890,8 +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) +-- (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,12 +913,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 @@ -970,33 +1053,25 @@ wrapEqCtxt :: [EqOrigin] -> TcM a -> TcM a -- and, if there is more than one item, the "Expected/inferred" part -- comes from the outermost item wrapEqCtxt [] thing_inside = thing_inside -wrapEqCtxt [_] thing_inside = thing_inside wrapEqCtxt items thing_inside = addErrCtxtM (unifyCtxt (last items)) thing_inside --------------- failWithMisMatch :: [EqOrigin] -> TcM a -- Generate the message when two types fail to match, -- going to some trouble to make it helpful. --- The argument order is: actual type, expected type -failWithMisMatch [] - = panic "failWithMisMatch" -failWithMisMatch origin@(item:_) +-- We take the failing types from the top of the origin stack +-- rather than reporting the particular ones we are looking +-- at right now +failWithMisMatch (item:origin) = wrapEqCtxt origin $ - emitMisMatchErr (uo_actual item) (uo_expected item) - -mkExpectedActualMsg :: Type -> Type -> SDoc -mkExpectedActualMsg act_ty exp_ty - = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty, - text " Actual type" <> colon <+> ppr act_ty ]) - -emitMisMatchErr :: TcType -> TcType -> TcM a -emitMisMatchErr ty_act ty_exp - = do { ty_act <- zonkTcType ty_act - ; ty_exp <- zonkTcType ty_exp + do { ty_act <- zonkTcType (uo_actual item) + ; ty_exp <- zonkTcType (uo_expected item) ; env0 <- tcInitTidyEnv ; let (env1, pp_exp) = tidyOpenType env0 ty_exp (env2, pp_act) = tidyOpenType env1 ty_act ; failWithTcM (misMatchMsg env2 pp_act pp_exp) } +failWithMisMatch [] + = panic "failWithMisMatch" misMatchMsg :: TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc) misMatchMsg env ty_act ty_exp @@ -1006,15 +1081,6 @@ misMatchMsg env ty_act ty_exp where (env1, extra1) = typeExtraInfoMsg env ty_exp (env2, extra2) = typeExtraInfoMsg env1 ty_act - --------------------- -unifyCtxt :: EqOrigin -> TidyEnv -> TcM (TidyEnv, SDoc) -unifyCtxt (UnifyOrigin { uo_actual = act_ty, uo_expected = exp_ty }) tidy_env - = do { act_ty' <- zonkTcType act_ty - ; exp_ty' <- zonkTcType exp_ty - ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty' - (env2, act_ty'') = tidyOpenType env1 act_ty' - ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') } \end{code} @@ -1212,7 +1278,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