X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=84fb1b81ede9cce659a7bf3faa03f3218449bbc4;hp=8a81b488bed500800263e9258cc7163b11c62ff6;hb=5de363ca9ebdb7d85e3c353c1cffdf0a1c11128e;hpb=d2ce0f52d42edf32bb9f13796e6ba6edba8bd516 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 8a81b48..84fb1b8 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -57,6 +57,7 @@ module TcMType ( zonkTcType, zonkTcTypes, zonkTcThetaType, zonkTcKindToKind, zonkTcKind, zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar, + zonkTcTypeAndSubst, tcGetGlobalTyVars, readKindVar, writeKindVar @@ -468,7 +469,7 @@ tcGetGlobalTyVars :: TcM TcTyVarSet tcGetGlobalTyVars = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv ; gbl_tvs <- readMutVar gtv_var - ; gbl_tvs' <- zonkTcTyVarsAndFV (varSetElems gbl_tvs) + ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs ; writeMutVar gtv_var gbl_tvs' ; return gbl_tvs' } \end{code} @@ -479,31 +480,29 @@ tcGetGlobalTyVars zonkTcTyVars :: [TcTyVar] -> TcM [TcType] zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars -zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet -zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars +zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet +zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars) ----------------- Types zonkTcTypeCarefully :: TcType -> TcM TcType +-- Do not zonk type variables free in the environment zonkTcTypeCarefully ty = do { env_tvs <- tcGetGlobalTyVars - ; zonkType (zonkTcTyVarCarefully env_tvs) ty } - - -zonkTcTyVarCarefully :: TcTyVarSet -> TcTyVar -> TcM TcType --- Do not zonk type variables free in the environment -zonkTcTyVarCarefully env_tvs tv - | tv `elemVarSet` env_tvs - = return (TyVarTy tv) - | otherwise - = ASSERT( isTcTyVar tv ) - case tcTyVarDetails tv of - SkolemTv {} -> return (TyVarTy tv) - FlatSkol ty -> zonkType (zonkTcTyVarCarefully env_tvs) ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of - Flexi -> return (TyVarTy tv) - Indirect ty -> zonkType (zonkTcTyVarCarefully env_tvs) ty } + ; zonkType (zonk_tv env_tvs) ty } + where + zonk_tv env_tvs tv + | tv `elemVarSet` env_tvs + = return (TyVarTy tv) + | otherwise + = ASSERT( isTcTyVar tv ) + case tcTyVarDetails tv of + SkolemTv {} -> return (TyVarTy tv) + FlatSkol ty -> zonkType (zonk_tv env_tvs) ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> return (TyVarTy tv) + Indirect ty -> zonkType (zonk_tv env_tvs) ty } zonkTcType :: TcType -> TcM TcType -- Simply look through all Flexis @@ -521,6 +520,23 @@ zonkTcTyVar tv Flexi -> return (TyVarTy tv) Indirect ty -> zonkTcType ty } +zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType +-- Zonk, and simultaneously apply a non-necessarily-idempotent substitution +zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty + where + zonk_tv tv + = case tcTyVarDetails tv of + SkolemTv {} -> return (TyVarTy tv) + FlatSkol ty -> zonkType zonk_tv ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> zonk_flexi tv + Indirect ty -> zonkType zonk_tv ty } + zonk_flexi tv + = case lookupTyVar subst tv of + Just ty -> zonkType zonk_tv ty + Nothing -> return (TyVarTy tv) + zonkTcTypes :: [TcType] -> TcM [TcType] zonkTcTypes tys = mapM zonkTcType tys @@ -585,12 +601,12 @@ zonkQuantifiedTyVar tv \begin{code} zonkImplication :: Implication -> TcM Implication -zonkImplication implic@(Implic { ic_env_tvs = env_tvs, ic_given = given +zonkImplication implic@(Implic { ic_untch = env_tvs, ic_given = given , ic_wanted = wanted }) - = do { env_tvs' <- zonkTcTyVarsAndFV (varSetElems env_tvs) + = do { env_tvs' <- zonkTcTyVarsAndFV env_tvs ; given' <- mapM zonkEvVar given ; wanted' <- mapBagM zonkWanted wanted - ; return (implic { ic_env_tvs = env_tvs', ic_given = given' + ; return (implic { ic_untch = env_tvs', ic_given = given' , ic_wanted = wanted' }) } zonkEvVar :: EvVar -> TcM EvVar @@ -817,10 +833,10 @@ checkValidType :: UserTypeCtxt -> Type -> TcM () -- Checks that the type is valid for the given context checkValidType ctxt ty = do traceTc "checkValidType" (ppr ty) - unboxed <- doptM Opt_UnboxedTuples - rank2 <- doptM Opt_Rank2Types - rankn <- doptM Opt_RankNTypes - polycomp <- doptM Opt_PolymorphicComponents + unboxed <- xoptM Opt_UnboxedTuples + rank2 <- xoptM Opt_Rank2Types + rankn <- xoptM Opt_RankNTypes + polycomp <- xoptM Opt_PolymorphicComponents let gen_rank n | rankn = ArbitraryRank | rank2 = Rank 2 @@ -950,7 +966,7 @@ check_type rank ubx_tup ty@(TyConApp tc tys) checkTc (tyConArity tc <= length tys) arity_msg -- See Note [Liberal type synonyms] - ; liberal <- doptM Opt_LiberalTypeSynonyms + ; liberal <- xoptM Opt_LiberalTypeSynonyms ; if not liberal || isSynFamilyTyCon tc then -- For H98 and synonym families, do check the type args mapM_ (check_mono_type SynArgMonoType) tys @@ -962,10 +978,10 @@ check_type rank ubx_tup ty@(TyConApp tc tys) } | isUnboxedTupleTyCon tc - = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples + = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg - ; impred <- doptM Opt_ImpredicativeTypes + ; impred <- xoptM Opt_ImpredicativeTypes ; let rank' = if impred then ArbitraryRank else TyConArgMonoType -- c.f. check_arg_type -- However, args are allowed to be unlifted, or @@ -1009,7 +1025,7 @@ check_arg_type :: Rank -> Type -> TcM () -- Anyway, they are dealt with by a special case in check_tau_type check_arg_type rank ty - = do { impred <- doptM Opt_ImpredicativeTypes + = do { impred <- xoptM Opt_ImpredicativeTypes ; let rank' = case rank of -- Predictive => must be monotype MustBeMonoType -> MustBeMonoType -- Monotype, regardless _other | impred -> ArbitraryRank @@ -1142,7 +1158,7 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) check_pred_ty dflags _ pred@(EqPred ty1 ty2) = do { -- Equational constraints are valid in all contexts if type -- families are permitted - ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred) + ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred) -- Check the form of the argument types ; checkValidMonoType ty1 @@ -1173,8 +1189,8 @@ check_class_pred_tys dflags ctxt tys -- checkInstTermination _ -> flexible_contexts || all tyvar_head tys where - flexible_contexts = dopt Opt_FlexibleContexts dflags - undecidable_ok = dopt Opt_UndecidableInstances dflags + flexible_contexts = xopt Opt_FlexibleContexts dflags + undecidable_ok = xopt Opt_UndecidableInstances dflags ------------------------- tyvar_head :: Type -> Bool @@ -1355,13 +1371,13 @@ checkValidInstHead ty -- Should be a source type check_inst_head :: DynFlags -> Class -> [Type] -> TcM () check_inst_head dflags clas tys = do { -- If GlasgowExts then check at least one isn't a type variable - ; checkTc (dopt Opt_TypeSynonymInstances dflags || + ; checkTc (xopt Opt_TypeSynonymInstances dflags || all tcInstHeadTyNotSynonym tys) (instTypeErr (pprClassPred clas tys) head_type_synonym_msg) - ; checkTc (dopt Opt_FlexibleInstances dflags || + ; checkTc (xopt Opt_FlexibleInstances dflags || all tcInstHeadTyAppAllTyVars tys) (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg) - ; checkTc (dopt Opt_MultiParamTypeClasses dflags || + ; checkTc (xopt Opt_MultiParamTypeClasses dflags || isSingleton tys) (instTypeErr (pprClassPred clas tys) head_one_type_msg) -- May not contain type family applications @@ -1412,7 +1428,7 @@ checkValidInstance hs_type tyvars theta tau do { (clas, inst_tys) <- setSrcSpan head_loc $ checkValidInstHead tau - ; undecidable_ok <- doptM Opt_UndecidableInstances + ; undecidable_ok <- xoptM Opt_UndecidableInstances ; checkValidTheta InstThetaCtxt theta ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) @@ -1513,7 +1529,7 @@ checkValidTypeInst typats rhs ; checkValidMonoType rhs -- we have a decidable instance unless otherwise permitted - ; undecidable_ok <- doptM Opt_UndecidableInstances + ; undecidable_ok <- xoptM Opt_UndecidableInstances ; unless undecidable_ok $ mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs)) } @@ -1616,14 +1632,12 @@ sizeTypes xs = sum (map sizeType xs) -- Size of a predicate -- --- Equalities are a special case. The equality itself doesn't contribute to the --- size and as we do not count class predicates, we have to start with one less. --- This is easy to see considering that, given --- class C a b | a -> b --- type family F a --- constraints (C a b) and (F a ~ b) are equivalent in size. +-- We are considering whether *class* constraints terminate +-- Once we get into an implicit parameter or equality we +-- can't get back to a class constraint, so it's safe +-- to say "size 0". See Trac #4200. sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' -sizePred (IParam _ ty) = sizeType ty -sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 - 1 +sizePred (IParam {}) = 0 +sizePred (EqPred {}) = 0 \end{code}