X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=d45d774cda04d6ba1818315cabd9ed9e2d7088f1;hp=a3484a96336e827906cfd6f90059217f50b23e32;hb=a40f2735958055f7ff94e5df73e710044aa63b2c;hpb=a6f2d598e1e7760d334d1b5ea0b7745e66835e11 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index a3484a9..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). @@ -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}