X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=d45d774cda04d6ba1818315cabd9ed9e2d7088f1;hp=8a81b488bed500800263e9258cc7163b11c62ff6;hb=a40f2735958055f7ff94e5df73e710044aa63b2c;hpb=d2ce0f52d42edf32bb9f13796e6ba6edba8bd516 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 8a81b48..d45d774 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -28,14 +28,13 @@ module TcMType ( newWantedCoVar, writeWantedCoVar, readWantedCoVar, newIP, newDict, newSelfDict, isSelfDict, - newWantedEvVar, newWantedEvVars, - newKindConstraint, + newWantedEvVar, newWantedEvVars, newTcEvBinds, addTcEvBind, -------------------------------- -- Instantiation tcInstTyVar, tcInstTyVars, tcInstSigTyVars, - tcInstType, tcInstSigType, + tcInstType, tcInstSigType, instMetaTyVar, tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, @@ -51,12 +50,13 @@ module TcMType ( -------------------------------- -- Zonking zonkType, mkZonkTcTyVar, zonkTcPredType, - zonkTcTypeCarefully, + zonkTcTypeCarefully, skolemiseUnboundMetaTyVar, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcThetaType, zonkTcKindToKind, zonkTcKind, zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar, + zonkTcTypeAndSubst, tcGetGlobalTyVars, readKindVar, writeKindVar @@ -134,17 +134,6 @@ newWantedEvVars theta = mapM newWantedEvVar theta newWantedCoVar :: TcType -> TcType -> TcM CoVar newWantedCoVar ty1 ty2 = newCoVar ty1 ty2 --- We used to create a mutable co-var -{- --- A wanted coercion variable is a MetaTyVar --- that can be filled in with its binding - = do { uniq <- newUnique - ; ref <- newMutVar Flexi - ; let name = mkSysTvName uniq (fsLit "c") - kind = mkPredTy (EqPred ty1 ty2) - ; return (mkTcTyVar name kind (MetaTv TauTv ref)) } --} - -------------- newEvVar :: TcPredType -> TcM EvVar -- Creates new *rigid* variables for predicates @@ -174,15 +163,6 @@ newName occ ; return (mkInternalName uniq occ loc) } ----------------- -newKindConstraint :: Type -> Kind -> TcM (CoVar, Type) --- Create a new wanted CoVar that constrains the type --- to have the specified kind -newKindConstraint ty kind - = do { ty_k <- newFlexiTyVarTy kind - ; co_var <- newWantedCoVar ty ty_k - ; return (co_var, ty_k) } - ------------------ newSelfDict :: Class -> [TcType] -> TcM DictId -- Make a dictionary for "self". It behaves just like a normal DictId -- except that it responds True to isSelfDict @@ -299,11 +279,12 @@ tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv) newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar -- Make a new meta tyvar out of thin air newMetaTyVar meta_info kind - = do { uniq <- newUnique + = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi ; let name = mkSysTvName uniq fs fs = case meta_info of TauTv -> fsLit "t" + TcsTv -> fsLit "u" SigTv _ -> fsLit "a" ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } @@ -311,7 +292,7 @@ instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar -- Make a new meta tyvar whose Name and Kind -- come from an existing TyVar instMetaTyVar meta_info tyvar - = do { uniq <- newUnique + = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi ; let name = setNameUnique (tyVarName tyvar) uniq kind = tyVarKind tyvar @@ -468,7 +449,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 +460,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 @@ -517,9 +496,26 @@ zonkTcTyVar tv SkolemTv {} -> return (TyVarTy tv) FlatSkol ty -> zonkTcType ty MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of - Flexi -> return (TyVarTy tv) - Indirect ty -> zonkTcType ty } + ; case cts of + 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 @@ -541,8 +537,6 @@ zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar --- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. --- -- The quantified type variables often include meta type variables -- we want to freeze them into ordinary type variables, and -- default their kind (e.g. from OpenTypeKind to TypeKind) @@ -553,45 +547,49 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- -- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv - | ASSERT2( isTcTyVar tv, ppr tv ) - isSkolemTyVar tv - = do { kind <- zonkTcType (tyVarKind tv) - ; return $ setTyVarKind tv kind - } + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv) + SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv) + ; return $ setTyVarKind tv kind } -- It might be a skolem type variable, -- for example from a user type signature - | otherwise -- It's a meta-type-variable - = do { details <- readMetaTyVar tv - - -- Create the new, frozen, skolem type variable - -- We zonk to a skolem, not to a regular TcVar - -- See Note [Zonking to Skolem] + MetaTv _ _ref -> +#ifdef DEBUG + -- [Sept 04] Check for non-empty. + -- See note [Silly Type Synonym] + (readMutVar _ref >>= \cts -> + case cts of + Flexi -> return () + Indirect ty -> WARN( True, ppr tv $$ ppr ty ) + return ()) >> +#endif + skolemiseUnboundMetaTyVar UnkSkol tv + +skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar +-- We have a Meta tyvar with a ref-cell inside it +-- Skolemise it, including giving it a new Name, so that +-- we are totally out of Meta-tyvar-land +-- We create a skolem TyVar, not a regular TyVar +-- See Note [Zonking to Skolem] +skolemiseUnboundMetaTyVar skol_info tv + = ASSERT2( isMetaTyVar tv, ppr tv ) + do { uniq <- newUnique -- Remove it from TcMetaTyVar unique land ; let final_kind = defaultKind (tyVarKind tv) - final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol - - -- Bind the meta tyvar to the new tyvar - ; case details of - Indirect ty -> WARN( True, ppr tv $$ ppr ty ) - return () - -- [Sept 04] I don't think this should happen - -- See note [Silly Type Synonym] - - Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv) - - -- Return the new tyvar + final_name = setNameUnique (tyVarName tv) uniq + final_tv = mkSkolTyVar final_name final_kind skol_info + ; writeMetaTyVar tv (mkTyVarTy final_tv) ; return final_tv } \end{code} \begin{code} zonkImplication :: Implication -> TcM Implication -zonkImplication implic@(Implic { ic_env_tvs = env_tvs, ic_given = given +zonkImplication implic@(Implic { ic_given = given , ic_wanted = wanted }) - = do { env_tvs' <- zonkTcTyVarsAndFV (varSetElems env_tvs) - ; given' <- mapM zonkEvVar given + = do { given' <- mapM zonkEvVar given ; wanted' <- mapBagM zonkWanted wanted - ; return (implic { ic_env_tvs = env_tvs', ic_given = given' - , ic_wanted = wanted' }) } + ; return (implic { ic_given = given', ic_wanted = wanted' }) } zonkEvVar :: EvVar -> TcM EvVar zonkEvVar var = do { ty' <- zonkTcType (varType var) @@ -686,10 +684,8 @@ simplifier knows how to deal with. -- For tyvars bound at a for-all, zonkType zonks them to an immutable -- type variable and zonks the kind too -zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables - -- see zonkTcType, and zonkTcTypeToType - -> TcType - -> TcM Type +zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars + -> TcType -> TcM Type zonkType zonk_tc_tyvar ty = go ty where @@ -729,17 +725,17 @@ zonkType zonk_tc_tyvar ty ty2' <- go ty2 return (EqPred ty1' ty2') -mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var +mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var -> TcTyVar -> TcM TcType mkZonkTcTyVar unbound_var_fn tyvar = ASSERT( isTcTyVar tyvar ) case tcTyVarDetails tyvar of - SkolemTv {} -> return (TyVarTy tyvar) - FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of - Flexi -> unbound_var_fn tyvar - Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty } + SkolemTv {} -> return (TyVarTy tyvar) + FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> unbound_var_fn tyvar + Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty } -- Zonk the kind of a non-TC tyvar in case it is a coercion variable -- (their kind contains types). @@ -817,10 +813,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 +946,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 +958,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 +1005,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 +1138,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 +1169,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 +1351,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 +1408,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 +1509,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 +1612,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}