X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=df1f06972f9ca9eb3d4b515c37467979d4f85b80;hp=c13993a808e39a2a91ba17536bff10d0453f1464;hb=1cdafe99abae1628f34ca8c064e3a8c0fcdbd079;hpb=5bca72372c6596012685063cb14cc4c6848fbc74 diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index c13993a..df1f069 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -11,30 +11,40 @@ module TcMType ( -------------------------------- -- Creating new mutable type variables - newTyVar, - newTyVarTy, -- Kind -> NF_TcM TcType - newTyVarTys, -- Int -> Kind -> NF_TcM [TcType] - newKindVar, newKindVars, newBoxityVar, - putTcTyVar, getTcTyVar, + newFlexiTyVar, + newFlexiTyVarTy, -- Kind -> TcM TcType + newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] + newKindVar, newKindVars, + lookupTcTyVar, LookupTyVarResult(..), + newMetaTyVar, readMetaTyVar, writeMetaTyVar, - newHoleTyVarTy, readHoleResult, zapToType, + -------------------------------- + -- Boxy type variables + newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, -------------------------------- -- Instantiation - tcInstTyVar, tcInstTyVars, tcInstType, + tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar, + tcInstSigTyVars, zonkSigTyVar, + tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, + tcSkolSigType, tcSkolSigTyVars, -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt, - SourceTyCtxt(..), checkValidTheta, - checkValidTyCon, checkValidClass, + Rank, UserTypeCtxt(..), checkValidType, + SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, instTypeErr, checkAmbiguity, + checkInstTermination, + arityErr, -------------------------------- -- Zonking - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, + zonkType, zonkTcPredType, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, - zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv, + zonkTcKindToKind, zonkTcKind, + + readKindVar, writeKindVar ) where @@ -42,220 +52,294 @@ module TcMType ( -- friends: -import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation - Kind, ThetaType +import TypeRep ( Type(..), PredType(..), -- Friend; can see representation + ThetaType ) import TcType ( TcType, TcThetaType, TcTauType, TcPredType, - TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..), - tcEqType, tcCmpPred, + TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), + MetaDetails(..), SkolemInfo(..), BoxInfo(..), + BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType, + UserTypeCtxt(..), + isMetaTyVar, isSigTyVar, metaTvRef, + tcCmpPred, isClassPred, tcGetTyVar, tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, - tcSplitTyConApp_maybe, tcSplitForAllTys, + tcValidInstHeadTy, tcSplitForAllTys, tcIsTyVarTy, tcSplitSigmaTy, - isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy, - + isUnLiftedType, isIPPred, + typeKind, isSkolemTyVar, mkAppTy, mkTyVarTy, mkTyVarTys, tyVarsOfPred, getClassPredTys_maybe, - - liftedTypeKind, openTypeKind, defaultKind, superKind, - superBoxity, liftedBoxity, typeKind, - tyVarsOfType, tyVarsOfTypes, - eqKind, isTypeKind, isAnyTypeKind, - - isFFIArgumentTy, isFFIImportResultTy + tyVarsOfType, tyVarsOfTypes, tcView, + pprPred, pprTheta, pprClassPred ) +import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar, + isLiftedTypeKind, isArgTypeKind, isOpenTypeKind, + liftedTypeKind, defaultKind ) -import qualified Type ( splitFunTys ) -import Subst ( Subst, mkTopTyVarSubst, substTy ) -import Class ( Class, DefMeth(..), classArity, className, classBigSig ) -import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon, - tyConArity, tyConName, tyConKind, tyConTheta, - getSynTyConDefn, tyConDataCons ) -import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels ) -import FieldLabel ( fieldLabelName, fieldLabelType ) -import PrimRep ( PrimRep(VoidRep) ) -import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar ) +import Type ( TvSubst, zipTopTvSubst, substTy ) +import Class ( Class, classArity, className ) +import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon, + tyConArity, tyConName ) +import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar, + mkTyVar, mkTcTyVar, tcTyVarDetails ) + + -- Assertions +#ifdef DEBUG +import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar ) +import Kind ( isSubKind ) +#endif -- others: -import Generics ( validGenericMethodType ) -import TcMonad -- TcType, amongst others -import TysWiredIn ( voidTy, listTyCon, tupleTyCon ) -import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey ) -import ForeignCall ( Safety(..) ) +import TcRnMonad -- TcType, amongst others import FunDeps ( grow ) -import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred ) -import Name ( Name, NamedThing(..), setNameUnique, - mkInternalName, mkDerivedTyConOcc, - mkSystemTvNameEncoded, - ) +import Name ( Name, setNameUnique, mkSysTvName ) import VarSet -import BasicTypes ( Boxity(Boxed) ) -import CmdLineOpts ( dopt, DynFlag(..) ) -import Unique ( Uniquable(..) ) -import SrcLoc ( noSrcLoc ) -import Util ( nOfThem, isSingleton, equalLength, notNull ) -import ListSetOps ( equivClasses, removeDups ) +import DynFlags ( dopt, DynFlag(..) ) +import Util ( nOfThem, isSingleton, notNull ) +import ListSetOps ( removeDups ) import Outputable + +import Data.List ( (\\) ) \end{code} %************************************************************************ %* * -\subsection{New type variables} + Instantiation in general %* * %************************************************************************ \begin{code} -newTyVar :: Kind -> NF_TcM TcTyVar -newTyVar kind - = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv - -newTyVarTy :: Kind -> NF_TcM TcType -newTyVarTy kind - = newTyVar kind `thenNF_Tc` \ tc_tyvar -> - returnNF_Tc (TyVarTy tc_tyvar) - -newTyVarTys :: Int -> Kind -> NF_TcM [TcType] -newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind) - -newKindVar :: NF_TcM TcKind -newKindVar - = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv -> - returnNF_Tc (TyVarTy kv) - -newKindVars :: Int -> NF_TcM [TcKind] -newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ()) - -newBoxityVar :: NF_TcM TcKind -newBoxityVar - = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv -> - returnNF_Tc (TyVarTy kv) +tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables + -> TcType -- Type to instantiate + -> TcM ([TcTyVar], TcThetaType, TcType) -- Result +tcInstType inst_tyvars ty + = case tcSplitForAllTys ty of + ([], rho) -> let -- There may be overloading despite no type variables; + -- (?x :: Int) => Int -> Int + (theta, tau) = tcSplitPhiTy rho + in + return ([], theta, tau) + + (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars + + ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars') + -- Either the tyvars are freshly made, by inst_tyvars, + -- or (in the call from tcSkolSigType) any nested foralls + -- have different binders. Either way, zipTopTvSubst is ok + + ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) + ; return (tyvars', theta, tau) } \end{code} %************************************************************************ %* * -\subsection{'hole' type variables} + Kind variables %* * %************************************************************************ \begin{code} -newHoleTyVarTy :: NF_TcM TcType - = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv -> - returnNF_Tc (TyVarTy tv) - -readHoleResult :: TcType -> NF_TcM TcType --- Read the answer out of a hole, constructed by newHoleTyVarTy -readHoleResult (TyVarTy tv) - = ASSERT( isHoleTyVar tv ) - getTcTyVar tv `thenNF_Tc` \ maybe_res -> - case maybe_res of - Just ty -> returnNF_Tc ty - Nothing -> pprPanic "readHoleResult: empty" (ppr tv) -readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty) - -zapToType :: TcType -> NF_TcM TcType -zapToType (TyVarTy tv) - | isHoleTyVar tv - = getTcTyVar tv `thenNF_Tc` \ maybe_res -> - case maybe_res of - Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty -> - putTcTyVar tv ty `thenNF_Tc_` - returnNF_Tc ty - Just ty -> returnNF_Tc ty -- No need to loop; we never - -- have chains of holes - -zapToType other_ty = returnNF_Tc other_ty -\end{code} +newKindVar :: TcM TcKind +newKindVar = do { uniq <- newUnique + ; ref <- newMutVar Nothing + ; return (KindVar (mkKindVar uniq ref)) } + +newKindVars :: Int -> TcM [TcKind] +newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) +\end{code} + %************************************************************************ %* * -\subsection{Type instantiation} + SkolemTvs (immutable) %* * %************************************************************************ -Instantiating a bunch of type variables +\begin{code} +mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar +mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info) + +tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType) +-- Instantiate a type signature with skolem constants, but +-- do *not* give them fresh names, because we want the name to +-- be in the type environment -- it is lexically scoped. +tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty + +tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] +-- Make skolem constants, but do *not* give them new names, as above +tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info + | tv <- tyvars ] + +tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) +-- Instantiate a type with fresh skolem constants +tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty + +tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar +tcInstSkolTyVar info tyvar + = do { uniq <- newUnique + ; let name = setNameUnique (tyVarName tyvar) uniq + kind = tyVarKind tyvar + ; return (mkSkolTyVar name kind info) } + +tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] +tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars +\end{code} + + +%************************************************************************ +%* * + MetaTvs (meta type variables; mutable) +%* * +%************************************************************************ \begin{code} -tcInstTyVars :: TyVarDetails -> [TyVar] - -> NF_TcM ([TcTyVar], [TcType], Subst) +newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar +-- Make a new meta tyvar out of thin air +newMetaTyVar box_info kind + = do { uniq <- newUnique + ; ref <- newMutVar Flexi ; + ; let name = mkSysTvName uniq fs + fs = case box_info of + BoxTv -> FSLIT("bx") + TauTv -> FSLIT("t") + SigTv _ -> FSLIT("a") + ; return (mkTcTyVar name kind (MetaTv box_info ref)) } + +instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar +-- Make a new meta tyvar whose Name and Kind +-- come from an existing TyVar +instMetaTyVar box_info tyvar + = do { uniq <- newUnique + ; ref <- newMutVar Flexi ; + ; let name = setNameUnique (tyVarName tyvar) uniq + kind = tyVarKind tyvar + ; return (mkTcTyVar name kind (MetaTv box_info ref)) } + +readMetaTyVar :: TyVar -> TcM MetaDetails +readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) + readMutVar (metaTvRef tyvar) + +writeMetaTyVar :: TcTyVar -> TcType -> TcM () +#ifndef DEBUG +writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty) +#else +writeMetaTyVar tyvar ty + | not (isMetaTyVar tyvar) + = pprTrace "writeMetaTyVar" (ppr tyvar) $ + returnM () -tcInstTyVars tv_details tyvars - = mapNF_Tc (tcInstTyVar tv_details) tyvars `thenNF_Tc` \ tc_tyvars -> - let - tys = mkTyVarTys tc_tyvars - in - returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys) - -- Since the tyvars are freshly made, - -- they cannot possibly be captured by - -- any existing for-alls. Hence mkTopTyVarSubst - -tcInstTyVar tv_details tyvar - = tcGetUnique `thenNF_Tc` \ uniq -> - let - name = setNameUnique (tyVarName tyvar) uniq - -- Note that we don't change the print-name - -- This won't confuse the type checker but there's a chance - -- that two different tyvars will print the same way - -- in an error message. -dppr-debug will show up the difference - -- Better watch out for this. If worst comes to worst, just - -- use mkSystemName. - in - tcNewMutTyVar name (tyVarKind tyvar) tv_details + | otherwise + = ASSERT( isMetaTyVar tyvar ) + ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) ) + do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar ) + ; writeMutVar (metaTvRef tyvar) (Indirect ty) } + where + k1 = tyVarKind tyvar + k2 = typeKind ty +#endif +\end{code} -tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType) --- tcInstType instantiates the outer-level for-alls of a TcType with --- fresh (mutable) type variables, splits off the dictionary part, --- and returns the pieces. -tcInstType tv_details ty - = case tcSplitForAllTys ty of - ([], rho) -> -- There may be overloading despite no type variables; - -- (?x :: Int) => Int -> Int - let - (theta, tau) = tcSplitPhiTy rho - in - returnNF_Tc ([], theta, tau) - (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenNF_Tc` \ (tyvars', _, tenv) -> - let - (theta, tau) = tcSplitPhiTy (substTy tenv rho) - in - returnNF_Tc (tyvars', theta, tau) +%************************************************************************ +%* * + MetaTvs: TauTvs +%* * +%************************************************************************ + +\begin{code} +newFlexiTyVar :: Kind -> TcM TcTyVar +newFlexiTyVar kind = newMetaTyVar TauTv kind + +newFlexiTyVarTy :: Kind -> TcM TcType +newFlexiTyVarTy kind + = newFlexiTyVar kind `thenM` \ tc_tyvar -> + returnM (TyVarTy tc_tyvar) + +newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] +newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind) + +tcInstTyVar :: TyVar -> TcM TcTyVar +-- Instantiate with a META type variable +tcInstTyVar tyvar = instMetaTyVar TauTv tyvar + +tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst) +-- Instantiate with META type variables +tcInstTyVars tyvars + = do { tc_tvs <- mapM tcInstTyVar tyvars + ; let tys = mkTyVarTys tc_tvs + ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) } + -- Since the tyvars are freshly made, + -- they cannot possibly be captured by + -- any existing for-alls. Hence zipTopTvSubst \end{code} %************************************************************************ %* * -\subsection{Putting and getting mutable type variables} + MetaTvs: SigTvs %* * %************************************************************************ \begin{code} -putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType -getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType) +tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] +-- Instantiate with meta SigTvs +tcInstSigTyVars skol_info tyvars + = mapM (instMetaTyVar (SigTv skol_info)) tyvars + +zonkSigTyVar :: TcTyVar -> TcM TcTyVar +zonkSigTyVar sig_tv + | isSkolemTyVar sig_tv + = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars + | otherwise + = ASSERT( isSigTyVar sig_tv ) + do { ty <- zonkTcTyVar sig_tv + ; return (tcGetTyVar "zonkSigTyVar" ty) } + -- 'ty' is bound to be a type variable, because SigTvs + -- can only be unified with type variables \end{code} -Putting is easy: + +%************************************************************************ +%* * + MetaTvs: BoxTvs +%* * +%************************************************************************ \begin{code} -putTcTyVar tyvar ty - | not (isMutTyVar tyvar) - = pprTrace "putTcTyVar" (ppr tyvar) $ - returnNF_Tc ty +newBoxyTyVar :: Kind -> TcM BoxyTyVar +newBoxyTyVar kind = newMetaTyVar BoxTv kind - | otherwise - = ASSERT( isMutTyVar tyvar ) - tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_` - returnNF_Tc ty +newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar] +newBoxyTyVars kinds = mapM newBoxyTyVar kinds + +newBoxyTyVarTys :: [Kind] -> TcM [BoxyType] +newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) } + +readFilledBox :: BoxyTyVar -> TcM TcType +-- Read the contents of the box, which should be filled in by now +readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv ) + do { cts <- readMetaTyVar box_tv + ; case cts of + Flexi -> pprPanic "readFilledBox" (ppr box_tv) + Indirect ty -> return ty } + +tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar +-- Instantiate with a BOXY type variable +tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar + +tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType) +-- tcInstType instantiates the outer-level for-alls of a TcType with +-- fresh BOXY type variables, splits off the dictionary part, +-- and returns the pieces. +tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty \end{code} -Getting is more interesting. The easy thing to do is just to read, thus: -\begin{verbatim} -getTcTyVar tyvar = tcReadMutTyVar tyvar -\end{verbatim} +%************************************************************************ +%* * +\subsection{Putting and getting mutable type variables} +%* * +%************************************************************************ But it's more fun to short out indirections on the way: If this version returns a TyVar, then that TyVar is unbound. If it returns @@ -264,36 +348,54 @@ any other type, then there might be bound TyVars embedded inside it. We return Nothing iff the original box was unbound. \begin{code} +data LookupTyVarResult -- The result of a lookupTcTyVar call + = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv + | IndirectTv TcType + +lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult +lookupTcTyVar tyvar + = case details of + SkolemTv _ -> return (DoneTv details) + MetaTv _ ref -> do { meta_details <- readMutVar ref + ; case meta_details of + Indirect ty -> return (IndirectTv ty) + Flexi -> return (DoneTv details) } + where + details = tcTyVarDetails tyvar + +{- +-- gaw 2004 We aren't shorting anything out anymore, at least for now getTcTyVar tyvar - | not (isMutTyVar tyvar) + | not (isTcTyVar tyvar) = pprTrace "getTcTyVar" (ppr tyvar) $ - returnNF_Tc (Just (mkTyVarTy tyvar)) + returnM (Just (mkTyVarTy tyvar)) | otherwise - = ASSERT2( isMutTyVar tyvar, ppr tyvar ) - tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty -> + = ASSERT2( isTcTyVar tyvar, ppr tyvar ) + readMetaTyVar tyvar `thenM` \ maybe_ty -> case maybe_ty of - Just ty -> short_out ty `thenNF_Tc` \ ty' -> - tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_` - returnNF_Tc (Just ty') + Just ty -> short_out ty `thenM` \ ty' -> + writeMetaTyVar tyvar (Just ty') `thenM_` + returnM (Just ty') - Nothing -> returnNF_Tc Nothing + Nothing -> returnM Nothing -short_out :: TcType -> NF_TcM TcType +short_out :: TcType -> TcM TcType short_out ty@(TyVarTy tyvar) - | not (isMutTyVar tyvar) - = returnNF_Tc ty + | not (isTcTyVar tyvar) + = returnM ty | otherwise - = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty -> + = readMetaTyVar tyvar `thenM` \ maybe_ty -> case maybe_ty of - Just ty' -> short_out ty' `thenNF_Tc` \ ty' -> - tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_` - returnNF_Tc ty' + Just ty' -> short_out ty' `thenM` \ ty' -> + writeMetaTyVar tyvar (Just ty') `thenM_` + returnM ty' - other -> returnNF_Tc ty + other -> returnM ty -short_out other_ty = returnNF_Tc other_ty +short_out other_ty = returnM other_ty +-} \end{code} @@ -306,153 +408,80 @@ short_out other_ty = returnNF_Tc other_ty ----------------- Type variables \begin{code} -zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType] -zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars +zonkTcTyVars :: [TcTyVar] -> TcM [TcType] +zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars -zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet -zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys -> - returnNF_Tc (tyVarsOfTypes tys) +zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet +zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> + returnM (tyVarsOfTypes tys) -zonkTcTyVar :: TcTyVar -> NF_TcM TcType -zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar +zonkTcTyVar :: TcTyVar -> TcM TcType +zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar ) + zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar \end{code} ----------------- Types \begin{code} -zonkTcType :: TcType -> NF_TcM TcType -zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty +zonkTcType :: TcType -> TcM TcType +zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty -zonkTcTypes :: [TcType] -> NF_TcM [TcType] -zonkTcTypes tys = mapNF_Tc zonkTcType tys +zonkTcTypes :: [TcType] -> TcM [TcType] +zonkTcTypes tys = mappM zonkTcType tys -zonkTcClassConstraints cts = mapNF_Tc zonk cts +zonkTcClassConstraints cts = mappM zonk cts where zonk (clas, tys) - = zonkTcTypes tys `thenNF_Tc` \ new_tys -> - returnNF_Tc (clas, new_tys) + = zonkTcTypes tys `thenM` \ new_tys -> + returnM (clas, new_tys) -zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType -zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta +zonkTcThetaType :: TcThetaType -> TcM TcThetaType +zonkTcThetaType theta = mappM zonkTcPredType theta -zonkTcPredType :: TcPredType -> NF_TcM TcPredType +zonkTcPredType :: TcPredType -> TcM TcPredType zonkTcPredType (ClassP c ts) - = zonkTcTypes ts `thenNF_Tc` \ new_ts -> - returnNF_Tc (ClassP c new_ts) + = zonkTcTypes ts `thenM` \ new_ts -> + returnM (ClassP c new_ts) zonkTcPredType (IParam n t) - = zonkTcType t `thenNF_Tc` \ new_t -> - returnNF_Tc (IParam n new_t) + = zonkTcType t `thenM` \ new_t -> + returnM (IParam n new_t) \end{code} ------------------- These ...ToType, ...ToKind versions are used at the end of type checking \begin{code} -zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)] -zonkKindEnv pairs - = mapNF_Tc zonk_it pairs - where - zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind -> - returnNF_Tc (name, kind) - - -- When zonking a kind, we want to - -- zonk a *kind* variable to (Type *) - -- zonk a *boxity* variable to * - zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind - | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity - | otherwise = pprPanic "zonkKindEnv" (ppr kv) - -zonkTcTypeToType :: TcType -> NF_TcM Type -zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty - where - -- Zonk a mutable but unbound type variable to an arbitrary type - -- We know it's unbound even though we don't carry an environment, - -- because at the binding site for a type variable we bind the - -- mutable tyvar to a fresh immutable one. So the mutable store - -- plays the role of an environment. If we come across a mutable - -- type variable that isn't so bound, it must be completely free. - zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv) - - --- When the type checker finds a type variable with no binding, --- which means it can be instantiated with an arbitrary type, it --- usually instantiates it to Void. Eg. --- --- length [] --- ===> --- length Void (Nil Void) --- --- But in really obscure programs, the type variable might have --- a kind other than *, so we need to invent a suitably-kinded type. --- --- This commit uses --- Void for kind * --- List for kind *->* --- Tuple for kind *->...*->* --- --- which deals with most cases. (Previously, it only dealt with --- kind *.) --- --- In the other cases, it just makes up a TyCon with a suitable --- kind. If this gets into an interface file, anyone reading that --- file won't understand it. This is fixable (by making the client --- of the interface file make up a TyCon too) but it is tiresome and --- never happens, so I am leaving it - -mkArbitraryType :: TcTyVar -> Type --- Make up an arbitrary type whose kind is the same as the tyvar. --- We'll use this to instantiate the (unbound) tyvar. -mkArbitraryType tv - | isAnyTypeKind kind = voidTy -- The vastly common case - | otherwise = TyConApp tycon [] - where - kind = tyVarKind tv - (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys - - tycon | kind `eqKind` tyConKind listTyCon -- *->* - = listTyCon -- No tuples this size - - | all isTypeKind args && isTypeKind res - = tupleTyCon Boxed (length args) -- *-> ... ->*->* - - | otherwise - = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $ - mkPrimTyCon tc_name kind 0 [] VoidRep - -- Same name as the tyvar, apart from making it start with a colon (sigh) - -- I dread to think what will happen if this gets out into an - -- interface file. Catastrophe likely. Major sigh. - - tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc - --- zonkTcTyVarToTyVar is applied to the *binding* occurrence --- of a type variable, at the *end* of type checking. It changes --- the *mutable* type variable into an *immutable* one. --- --- It does this by making an immutable version of tv and binds tv to it. --- Now any bound occurences of the original type variable will get --- zonked to the immutable version. - -zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar -zonkTcTyVarToTyVar tv - = let - -- Make an immutable version, defaulting - -- the kind to lifted if necessary - immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv)) - immut_tv_ty = mkTyVarTy immut_tv - - zap tv = putTcTyVar tv immut_tv_ty - -- Bind the mutable version to the immutable one - in - -- If the type variable is mutable, then bind it to immut_tv_ty - -- so that all other occurrences of the tyvar will get zapped too - zonkTyVar zap tv `thenNF_Tc` \ ty2 -> - - -- This warning shows up if the allegedly-unbound tyvar is - -- already bound to something. It can actually happen, and - -- in a harmless way (see [Silly Type Synonyms] below) so - -- it's only a warning - WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 ) - - returnNF_Tc immut_tv +zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar +-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. +-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar. +-- When we do this, we also default the kind -- see notes with Kind.defaultKind +-- The meta tyvar is updated to point to the new regular TyVar. Now any +-- bound occurences of the original type variable will get zonked to +-- the immutable version. +-- +-- We leave skolem TyVars alone; they are immutable. +zonkQuantifiedTyVar tv + | isSkolemTyVar tv = return tv + -- 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, regular type variable + ; let final_kind = defaultKind (tyVarKind tv) + final_tv = mkTyVar (tyVarName tv) final_kind + + -- 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 + ; return final_tv } \end{code} [Silly Type Synonyms] @@ -474,16 +503,21 @@ Consider this: where a is fresh. * Now abstract over the 'a', but float out the Num (C d a) constraint - because it does not 'really' mention a. (see Type.tyVarsOfType) + because it does not 'really' mention a. (see exactTyVarsOfType) The arg to foo becomes /\a -> \t -> t+t * So we get a dict binding for Num (C d a), which is zonked to give a = () + [Note Sept 04: now that we are zonking quantified type variables + on construction, the 'a' will be frozen as a regular tyvar on + quantification, so the floated dict will still have type (C d a). + Which renders this whole note moot; happily!] * Then the /\a abstraction has a zonked 'a' in it. -All very silly. I think its harmless to ignore the problem. +All very silly. I think its harmless to ignore the problem. We'll end up with +a /\a in the final result but all the occurrences of a will be zonked to () %************************************************************************ @@ -495,76 +529,105 @@ All very silly. I think its harmless to ignore the problem. %************************************************************************ \begin{code} --- zonkType is used for Kinds as well - -- For unbound, mutable tyvars, zonkType uses the function given to it -- For tyvars bound at a for-all, zonkType zonks them to an immutable -- type variable and zonks the kind too -zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables +zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables -- see zonkTcType, and zonkTcTypeToType - -> TcType - -> NF_TcM Type + -> TcType + -> TcM Type zonkType unbound_var_fn ty = go ty where - go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' -> - returnNF_Tc (TyConApp tycon tys') - - go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' -> - go ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (NoteTy (SynNote ty1') ty2') - - go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations - - go (SourceTy p) = go_pred p `thenNF_Tc` \ p' -> - returnNF_Tc (SourceTy p') - - go (FunTy arg res) = go arg `thenNF_Tc` \ arg' -> - go res `thenNF_Tc` \ res' -> - returnNF_Tc (FunTy arg' res') - - go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' -> - go arg `thenNF_Tc` \ arg' -> - returnNF_Tc (mkAppTy fun' arg') + go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations + + go (TyConApp tc tys) = mappM go tys `thenM` \ tys' -> + returnM (TyConApp tc tys') + + go (PredTy p) = go_pred p `thenM` \ p' -> + returnM (PredTy p') + + go (FunTy arg res) = go arg `thenM` \ arg' -> + go res `thenM` \ res' -> + returnM (FunTy arg' res') + + go (AppTy fun arg) = go fun `thenM` \ fun' -> + go arg `thenM` \ arg' -> + returnM (mkAppTy fun' arg') -- NB the mkAppTy; we might have instantiated a -- type variable to a type constructor, so we need -- to pull the TyConApp to the top. -- The two interesting cases! - go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar - - go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' -> - go ty `thenNF_Tc` \ ty' -> - returnNF_Tc (ForAllTy tyvar' ty') - - go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' -> - returnNF_Tc (ClassP c tys') - go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' -> - returnNF_Tc (NType tc tys') - go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' -> - returnNF_Tc (IParam n ty') - -zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable - -> TcTyVar -> NF_TcM TcType -zonkTyVar unbound_var_fn tyvar - | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when - -- zonking a forall type, when the bound type variable - -- needn't be mutable - = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars - returnNF_Tc (TyVarTy tyvar) - - | otherwise - = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - Nothing -> unbound_var_fn tyvar -- Mutable and unbound - Just other_ty -> zonkType unbound_var_fn other_ty -- Bound + go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar + | otherwise = return (TyVarTy tyvar) + -- Ordinary (non Tc) tyvars occur inside quantified types + + go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) + go ty `thenM` \ ty' -> + returnM (ForAllTy tyvar ty') + + go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' -> + returnM (ClassP c tys') + go_pred (IParam n ty) = go ty `thenM` \ ty' -> + returnM (IParam n ty') + +zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable + -> TcTyVar -> TcM TcType +zonk_tc_tyvar unbound_var_fn tyvar + | not (isMetaTyVar tyvar) -- Skolems + = returnM (TyVarTy tyvar) + + | otherwise -- Mutables + = do { cts <- readMetaTyVar tyvar + ; case cts of + Flexi -> unbound_var_fn tyvar -- Unbound meta type variable + Indirect ty -> zonkType unbound_var_fn ty } \end{code} %************************************************************************ %* * + Zonking kinds +%* * +%************************************************************************ + +\begin{code} +readKindVar :: KindVar -> TcM (Maybe TcKind) +writeKindVar :: KindVar -> TcKind -> TcM () +readKindVar kv = readMutVar (kindVarRef kv) +writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val) + +------------- +zonkTcKind :: TcKind -> TcM TcKind +zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1 + ; k2' <- zonkTcKind k2 + ; returnM (FunKind k1' k2') } +zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv + ; case mb_kind of + Nothing -> returnM k + Just k -> zonkTcKind k } +zonkTcKind other_kind = returnM other_kind + +------------- +zonkTcKindToKind :: TcKind -> TcM Kind +zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1 + ; k2' <- zonkTcKindToKind k2 + ; returnM (FunKind k1' k2') } + +zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv + ; case mb_kind of + Nothing -> return liftedTypeKind + Just k -> zonkTcKindToKind k } + +zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to * +zonkTcKindToKind other_kind = returnM other_kind +\end{code} + +%************************************************************************ +%* * \subsection{Checking a user type} %* * %************************************************************************ @@ -598,53 +661,19 @@ This might not necessarily show up in kind checking. \begin{code} -data UserTypeCtxt - = FunSigCtxt Name -- Function type signature - | ExprSigCtxt -- Expression type signature - | ConArgCtxt Name -- Data constructor argument - | TySynCtxt Name -- RHS of a type synonym decl - | GenPatCtxt -- Pattern in generic decl - -- f{| a+b |} (Inl x) = ... - | PatSigCtxt -- Type sig in pattern - -- f (x::t) = ... - | ResSigCtxt -- Result type sig - -- f x :: t = .... - | ForSigCtxt Name -- Foreign inport or export signature - | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE - --- Notes re TySynCtxt --- We allow type synonyms that aren't types; e.g. type List = [] --- --- If the RHS mentions tyvars that aren't in scope, we'll --- quantify over them: --- e.g. type T = a->a --- will become type T = forall a. a->a --- --- With gla-exts that's right, but for H98 we should complain. - - -pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n) -pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature") -pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c) -pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c) -pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition") -pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature") -pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature") -pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n) -pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n) -\end{code} - -\begin{code} checkValidType :: UserTypeCtxt -> Type -> TcM () -- Checks that the type is valid for the given context checkValidType ctxt ty - = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts -> + = traceTc (text "checkValidType" <+> ppr ty) `thenM_` + doptM Opt_GlasgowExts `thenM` \ gla_exts -> let rank | gla_exts = Arbitrary | otherwise = case ctxt of -- Haskell 98 GenPatCtxt -> Rank 0 - PatSigCtxt -> Rank 0 + LamPatSigCtxt -> Rank 0 + BindPatSigCtxt -> Rank 0 + DefaultDeclCtxt-> Rank 0 ResSigCtxt -> Rank 0 TySynCtxt _ -> Rank 0 ExprSigCtxt -> Rank 1 @@ -653,50 +682,34 @@ checkValidType ctxt ty -- constructor, hence rank 1 ForSigCtxt _ -> Rank 1 RuleSigCtxt _ -> Rank 1 + SpecInstCtxt -> Rank 1 actual_kind = typeKind ty - actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind - kind_ok = case ctxt of TySynCtxt _ -> True -- Any kind will do - GenPatCtxt -> actual_kind_is_lifted - ForSigCtxt _ -> actual_kind_is_lifted - other -> isTypeKind actual_kind + ResSigCtxt -> isOpenTypeKind actual_kind + ExprSigCtxt -> isOpenTypeKind actual_kind + GenPatCtxt -> isLiftedTypeKind actual_kind + ForSigCtxt _ -> isLiftedTypeKind actual_kind + other -> isArgTypeKind actual_kind ubx_tup | not gla_exts = UT_NotOk | otherwise = case ctxt of TySynCtxt _ -> UT_Ok + ExprSigCtxt -> UT_Ok other -> UT_NotOk -- Unboxed tuples ok in function results, -- but for type synonyms we allow them even at -- top level in - tcAddErrCtxt (checkTypeCtxt ctxt ty) $ - -- Check that the thing has kind Type, and is lifted if necessary - checkTc kind_ok (kindErr actual_kind) `thenTc_` + checkTc kind_ok (kindErr actual_kind) `thenM_` -- Check the internal validity of the type itself - check_poly_type rank ubx_tup ty - - -checkTypeCtxt ctxt ty - = vcat [ptext SLIT("In the type:") <+> ppr_ty ty, - ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ] - - -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print - -- something strange like {Eq k} -> k -> k, because there is no - -- ForAll at the top of the type. Since this is going to the user - -- we want it to look like a proper Haskell type even then; hence the hack - -- - -- This shows up in the complaint about - -- case C a where - -- op :: Eq a => a -> a -ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau - | otherwise = ppr ty - where - (forall_tvs, theta, tau) = tcSplitSigmaTy ty + check_poly_type rank ubx_tup ty `thenM_` + + traceTc (text "checkValidType done" <+> ppr ty) \end{code} @@ -720,16 +733,16 @@ check_poly_type rank ubx_tup ty = let (tvs, theta, tau) = tcSplitSigmaTy ty in - check_valid_theta SigmaCtxt theta `thenTc_` - check_tau_type (decRank rank) ubx_tup tau `thenTc_` - checkFreeness tvs theta `thenTc_` + check_valid_theta SigmaCtxt theta `thenM_` + check_tau_type (decRank rank) ubx_tup tau `thenM_` + checkFreeness tvs theta `thenM_` checkAmbiguity tvs theta (tyVarsOfType tau) ---------------------------------------- check_arg_type :: Type -> TcM () -- The sort of type that can instantiate a type variable, -- or be the argument of a type constructor. --- Not an unboxed tuple, not a forall. +-- Not an unboxed tuple, but now *can* be a forall (since impredicativity) -- Other unboxed types are very occasionally allowed as type -- arguments depending on the kind of the type constructor -- @@ -746,7 +759,7 @@ check_arg_type :: Type -> TcM () -- Anyway, they are dealt with by a special case in check_tau_type check_arg_type ty - = check_tau_type (Rank 0) UT_NotOk ty `thenTc_` + = check_poly_type Arbitrary UT_NotOk ty `thenM_` checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) ---------------------------------------- @@ -754,24 +767,42 @@ check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM () -- Rank is allowed rank for function args -- No foralls otherwise -check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty) -check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags -> - check_source_ty dflags TypeCtxt sty -check_tau_type rank ubx_tup (TyVarTy _) = returnTc () +check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty) +check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty) + -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message + +-- Naked PredTys don't usually show up, but they can as a result of +-- {-# SPECIALISE instance Ord Char #-} +-- The Right Thing would be to fix the way that SPECIALISE instance pragmas +-- are handled, but the quick thing is just to permit PredTys here. +check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags -> + check_source_ty dflags TypeCtxt sty + +check_tau_type rank ubx_tup (TyVarTy _) = returnM () check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty) - = check_poly_type rank UT_NotOk arg_ty `thenTc_` - check_tau_type rank UT_Ok res_ty + = check_poly_type rank UT_NotOk arg_ty `thenM_` + check_poly_type rank UT_Ok res_ty check_tau_type rank ubx_tup (AppTy ty1 ty2) - = check_arg_type ty1 `thenTc_` check_arg_type ty2 - -check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty) - -- Synonym notes are built only when the synonym is - -- saturated (see Type.mkSynTy) - = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts -> - (if gla_exts then - -- If -fglasgow-exts then don't check the 'note' part. - -- This allows us to instantiate a synonym defn with a + = check_arg_type ty1 `thenM_` check_arg_type ty2 + +check_tau_type rank ubx_tup (NoteTy other_note ty) + = check_tau_type rank ubx_tup ty + +check_tau_type rank ubx_tup ty@(TyConApp tc tys) + | isSynTyCon tc + = do { -- It's OK to have an *over-applied* type synonym + -- data Tree a b = ... + -- type Foo a = Tree [a] + -- f :: Foo a b -> ... + ; case tcView ty of + Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion + Nothing -> failWithTc arity_msg + + ; gla_exts <- doptM Opt_GlasgowExts + ; if gla_exts then + -- If -fglasgow-exts then don't check the type arguments + -- This allows us to instantiate a synonym defn with a -- for-all type, or with a partially-applied type synonym. -- e.g. type T a b = a -- type S m = m () @@ -780,43 +811,25 @@ check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty) -- But if you expand S first, then T we get just -- f :: Int -- which is fine. - returnTc () - else - -- For H98, do check the un-expanded part - check_tau_type rank ubx_tup syn - ) `thenTc_` - - check_tau_type rank ubx_tup ty - -check_tau_type rank ubx_tup (NoteTy other_note ty) - = check_tau_type rank ubx_tup ty - -check_tau_type rank ubx_tup ty@(TyConApp tc tys) - | isSynTyCon tc - = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated - -- synonym application, leaving it to checkValidType (i.e. right here) - -- to find the error - checkTc syn_arity_ok arity_msg `thenTc_` - mapTc_ check_arg_type tys + returnM () + else + -- For H98, do check the type args + mappM_ check_arg_type tys + } | isUnboxedTupleTyCon tc - = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts -> - checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_` - mapTc_ (check_tau_type (Rank 0) UT_Ok) tys - -- Args are allowed to be unlifted, or - -- more unboxed tuples, so can't use check_arg_ty + = doptM Opt_GlasgowExts `thenM` \ gla_exts -> + checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_` + mappM_ (check_tau_type (Rank 0) UT_Ok) tys + -- Args are allowed to be unlifted, or + -- more unboxed tuples, so can't use check_arg_ty | otherwise - = mapTc_ check_arg_type tys + = mappM_ check_arg_type tys where ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False } - syn_arity_ok = tc_arity <= n_args - -- It's OK to have an *over-applied* type synonym - -- data Tree a b = ... - -- type Foo a = Tree [a] - -- f :: Foo a b -> ... n_args = length tys tc_arity = tyConArity tc @@ -824,82 +837,12 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) ubx_tup_msg = ubxArgTyErr ty ---------------------------------------- -forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty -unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty -ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty +forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty +unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty +ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind \end{code} -Check for ambiguity -~~~~~~~~~~~~~~~~~~~ - forall V. P => tau -is ambiguous if P contains generic variables -(i.e. one of the Vs) that are not mentioned in tau - -However, we need to take account of functional dependencies -when we speak of 'mentioned in tau'. Example: - class C a b | a -> b where ... -Then the type - forall x y. (C x y) => x -is not ambiguous because x is mentioned and x determines y - -NB; the ambiguity check is only used for *user* types, not for types -coming from inteface files. The latter can legitimately have -ambiguous types. Example - - class S a where s :: a -> (Int,Int) - instance S Char where s _ = (1,1) - f:: S a => [a] -> Int -> (Int,Int) - f (_::[a]) x = (a*x,b) - where (a,b) = s (undefined::a) - -Here the worker for f gets the type - fw :: forall a. S a => Int -> (# Int, Int #) - -If the list of tv_names is empty, we have a monotype, and then we -don't need to check for ambiguity either, because the test can't fail -(see is_ambig). - -\begin{code} -checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM () -checkAmbiguity forall_tyvars theta tau_tyvars - = mapTc_ complain (filter is_ambig theta) - where - complain pred = addErrTc (ambigErr pred) - extended_tau_vars = grow theta tau_tyvars - is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred)) - - ambig_var ct_var = (ct_var `elem` forall_tyvars) && - not (ct_var `elemVarSet` extended_tau_vars) - - is_free ct_var = not (ct_var `elem` forall_tyvars) - -ambigErr pred - = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred), - nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$ - ptext SLIT("must be reachable from the type after the '=>'"))] -\end{code} - -In addition, GHC insists that at least one type variable -in each constraint is in V. So we disallow a type like - forall a. Eq b => b -> b -even in a scope where b is in scope. - -\begin{code} -checkFreeness forall_tyvars theta - = mapTc_ complain (filter is_free theta) - where - is_free pred = not (isIPPred pred) - && not (any bound_var (varSetElems (tyVarsOfPred pred))) - bound_var ct_var = ct_var `elem` forall_tyvars - complain pred = addErrTc (freeErr pred) - -freeErr pred - = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+> - ptext SLIT("are already in scope"), - nest 4 (ptext SLIT("(at least one must be universally quantified here)")) - ] -\end{code} %************************************************************************ @@ -909,42 +852,53 @@ freeErr pred %************************************************************************ \begin{code} +-- Enumerate the contexts in which a "source type", , can occur +-- Eq a +-- or ?x::Int +-- or r <: {x::Int} +-- or (N a) where N is a newtype + data SourceTyCtxt = ClassSCCtxt Name -- Superclasses of clas - | SigmaCtxt -- Context of a normal for-all type - | DataTyCtxt Name -- Context of a data decl + -- class => C a where ... + | SigmaCtxt -- Theta part of a normal for-all type + -- f :: => a -> a + | DataTyCtxt Name -- Theta part of a data decl + -- data => T a = MkT a | TypeCtxt -- Source type in an ordinary type + -- f :: N a -> N a | InstThetaCtxt -- Context of an instance decl - | InstHeadCtxt -- Head of an instance decl + -- instance => C [a] where ... pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c) pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type") pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc) pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration") -pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration") pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type") \end{code} \begin{code} checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM () checkValidTheta ctxt theta - = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta) + = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta) ------------------------- check_valid_theta ctxt [] - = returnTc () + = returnM () check_valid_theta ctxt theta - = getDOptsTc `thenNF_Tc` \ dflags -> - warnTc (notNull dups) (dupPredWarn dups) `thenNF_Tc_` - mapTc_ (check_source_ty dflags ctxt) theta + = getDOpts `thenM` \ dflags -> + warnTc (notNull dups) (dupPredWarn dups) `thenM_` + mappM_ (check_source_ty dflags ctxt) theta where (_,dups) = removeDups tcCmpPred theta ------------------------- check_source_ty dflags ctxt pred@(ClassP cls tys) = -- Class predicates are valid in all contexts - mapTc_ check_arg_type tys `thenTc_` - checkTc (arity == n_tys) arity_err `thenTc_` + checkTc (arity == n_tys) arity_err `thenM_` + + -- Check the form of the argument types + mappM_ check_arg_type tys `thenM_` checkTc (check_class_pred_tys dflags ctxt tys) (predTyVarErr pred $$ how_to_allow) @@ -969,20 +923,18 @@ check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- constraint Foo [Int] might come out of e,and applying the -- instance decl would show up two uses of ?x. -check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys - -- Catch-all check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty) ------------------------- check_class_pred_tys dflags ctxt tys = case ctxt of + TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine InstHeadCtxt -> True -- We check for instance-head -- formation in checkValidInstHead - InstThetaCtxt -> undecidable_ok || all isTyVarTy tys + InstThetaCtxt -> undecidable_ok || distinct_tyvars tys other -> gla_exts || all tyvar_head tys where - undecidable_ok = dopt Opt_AllowUndecidableInstances dflags gla_exts = dopt Opt_GlasgowExts dflags ------------------------- @@ -994,141 +946,99 @@ tyvar_head ty -- Haskell 98 allows predicates of form Nothing -> False \end{code} -\begin{code} -badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty -predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred -dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) - -checkThetaCtxt ctxt theta - = vcat [ptext SLIT("In the context:") <+> pprTheta theta, - ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] -\end{code} +Check for ambiguity +~~~~~~~~~~~~~~~~~~~ + forall V. P => tau +is ambiguous if P contains generic variables +(i.e. one of the Vs) that are not mentioned in tau +However, we need to take account of functional dependencies +when we speak of 'mentioned in tau'. Example: + class C a b | a -> b where ... +Then the type + forall x y. (C x y) => x +is not ambiguous because x is mentioned and x determines y -%************************************************************************ -%* * -\subsection{Validity check for TyCons} -%* * -%************************************************************************ +NB; the ambiguity check is only used for *user* types, not for types +coming from inteface files. The latter can legitimately have +ambiguous types. Example -checkValidTyCon is called once the mutually-recursive knot has been -tied, so we can look at things freely. + class S a where s :: a -> (Int,Int) + instance S Char where s _ = (1,1) + f:: S a => [a] -> Int -> (Int,Int) + f (_::[a]) x = (a*x,b) + where (a,b) = s (undefined::a) -\begin{code} -checkValidTyCon :: TyCon -> TcM () -checkValidTyCon tc - | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs - | otherwise - = -- Check the context on the data decl - checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenTc_` - - -- Check arg types of data constructors - mapTc_ checkValidDataCon data_cons `thenTc_` +Here the worker for f gets the type + fw :: forall a. S a => Int -> (# Int, Int #) - -- Check that fields with the same name share a type - mapTc_ check_fields groups +If the list of tv_names is empty, we have a monotype, and then we +don't need to check for ambiguity either, because the test can't fail +(see is_ambig). +\begin{code} +checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM () +checkAmbiguity forall_tyvars theta tau_tyvars + = mappM_ complain (filter is_ambig theta) where - name = tyConName tc - (_, syn_rhs) = getSynTyConDefn tc - data_cons = tyConDataCons tc - - fields = [field | con <- data_cons, field <- dataConFieldLabels con] - groups = equivClasses cmp_name fields - cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2 - - check_fields fields@(first_field_label : other_fields) - -- These fields all have the same name, but are from - -- different constructors in the data type - = -- Check that all the fields in the group have the same type - -- NB: this check assumes that all the constructors of a given - -- data type use the same type variables - checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name) - where - field_ty = fieldLabelType first_field_label - field_name = fieldLabelName first_field_label - other_tys = map fieldLabelType other_fields - -checkValidDataCon :: DataCon -> TcM () -checkValidDataCon con - = checkValidType ctxt (idType (dataConWrapId con)) `thenTc_` - -- This checks the argument types and - -- ambiguity of the existential context (if any) - tcAddErrCtxt (existentialCtxt con) - (checkFreeness ex_tvs ex_theta) - where - ctxt = ConArgCtxt (dataConName con) - (_, _, ex_tvs, ex_theta, _, _) = dataConSig con + complain pred = addErrTc (ambigErr pred) + extended_tau_vars = grow theta tau_tyvars + -- Only a *class* predicate can give rise to ambiguity + -- An *implicit parameter* cannot. For example: + -- foo :: (?x :: [a]) => Int + -- foo = length ?x + -- is fine. The call site will suppply a particular 'x' + is_ambig pred = isClassPred pred && + any ambig_var (varSetElems (tyVarsOfPred pred)) -fieldTypeMisMatch field_name - = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)] + ambig_var ct_var = (ct_var `elem` forall_tyvars) && + not (ct_var `elemVarSet` extended_tau_vars) -existentialCtxt con = ptext SLIT("When checking the existential context of constructor") - <+> quotes (ppr con) +ambigErr pred + = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred), + nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$ + ptext SLIT("must be reachable from the type after the '=>'"))] \end{code} - - -checkValidClass is called once the mutually-recursive knot has been -tied, so we can look at things freely. + +In addition, GHC insists that at least one type variable +in each constraint is in V. So we disallow a type like + forall a. Eq b => b -> b +even in a scope where b is in scope. \begin{code} -checkValidClass :: Class -> TcM () -checkValidClass cls - = -- CHECK ARITY 1 FOR HASKELL 1.4 - doptsTc Opt_GlasgowExts `thenTc` \ gla_exts -> - - -- Check that the class is unary, unless GlaExs - checkTc (notNull tyvars) (nullaryClassErr cls) `thenTc_` - checkTc (gla_exts || unary) (classArityErr cls) `thenTc_` +checkFreeness forall_tyvars theta + = mappM_ complain (filter is_free theta) + where + is_free pred = not (isIPPred pred) + && not (any bound_var (varSetElems (tyVarsOfPred pred))) + bound_var ct_var = ct_var `elem` forall_tyvars + complain pred = addErrTc (freeErr pred) - -- Check the super-classes - checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_` +freeErr pred + = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+> + ptext SLIT("are already in scope"), + nest 4 (ptext SLIT("(at least one must be universally quantified here)")) + ] +\end{code} - -- Check the class operations - mapTc_ check_op op_stuff `thenTc_` +\begin{code} +checkThetaCtxt ctxt theta + = vcat [ptext SLIT("In the context:") <+> pprTheta theta, + ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] - -- Check that if the class has generic methods, then the - -- class has only one parameter. We can't do generic - -- multi-parameter type classes! - checkTc (unary || no_generics) (genericMultiParamErr cls) +badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty +predTyVarErr pred = sep [ptext SLIT("Non-type variable argument"), + nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)] +dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) - where - (tyvars, theta, _, op_stuff) = classBigSig cls - unary = isSingleton tyvars - no_generics = null [() | (_, GenDefMeth) <- op_stuff] - - check_op (sel_id, dm) - = checkValidTheta SigmaCtxt (tail theta) `thenTc_` - -- The 'tail' removes the initial (C a) from the - -- class itself, leaving just the method type - - checkValidType (FunSigCtxt op_name) tau `thenTc_` - - -- Check that for a generic method, the type of - -- the method is sufficiently simple - checkTc (dm /= GenDefMeth || validGenericMethodType op_ty) - (badGenericMethodType op_name op_ty) - where - op_name = idName sel_id - op_ty = idType sel_id - (_,theta,tau) = tcSplitSigmaTy op_ty - -nullaryClassErr cls - = ptext SLIT("No parameters for class") <+> quotes (ppr cls) - -classArityErr cls - = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls), - parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))] - -genericMultiParamErr clas - = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+> - ptext SLIT("cannot have generic methods") - -badGenericMethodType op op_ty - = hang (ptext SLIT("Generic method type is too complex")) - 4 (vcat [ppr op <+> dcolon <+> ppr op_ty, - ptext SLIT("You can only use type variables, arrows, and tuples")]) +arityErr kind name n m + = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"), + n_arguments <> comma, text "but has been given", int m] + where + n_arguments | n == 0 = ptext SLIT("no arguments") + | n == 1 = ptext SLIT("1 argument") + | True = hsep [int n, ptext SLIT("arguments")] \end{code} @@ -1159,66 +1069,116 @@ checkValidInstHead ty -- Should be a source type Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ; Just (clas,tys) -> - getDOptsTc `thenNF_Tc` \ dflags -> - mapTc_ check_arg_type tys `thenTc_` - check_inst_head dflags clas tys `thenTc_` - returnTc (clas, tys) + getDOpts `thenM` \ dflags -> + mappM_ check_arg_type tys `thenM_` + check_inst_head dflags clas tys `thenM_` + returnM (clas, tys) }} check_inst_head dflags clas tys - | -- CCALL CHECK - -- A user declaration of a CCallable/CReturnable instance - -- must be for a "boxed primitive" type. - (clas `hasKey` cCallableClassKey - && not (ccallable_type first_ty)) - || (clas `hasKey` cReturnableClassKey - && not (creturnable_type first_ty)) - = failWithTc (nonBoxedPrimCCallErr clas first_ty) - -- If GlasgowExts then check at least one isn't a type variable | dopt Opt_GlasgowExts dflags - = check_tyvars dflags clas tys + = returnM () - -- WITH HASKELL 1.4, MUST HAVE C (T a b c) + -- WITH HASKELL 98, MUST HAVE C (T a b c) | isSingleton tys, - Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty, - not (isSynTyCon tycon), -- ...but not a synonym - all tcIsTyVarTy arg_tys, -- Applied to type variables - equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys - -- This last condition checks that all the type variables are distinct - = returnTc () + tcValidInstHeadTy first_ty + = returnM () | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg) where - (first_ty : _) = tys + (first_ty : _) = tys - ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty - creturnable_type ty = isFFIImportResultTy dflags ty - head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$ text "where T is not a synonym, and a,b,c are distinct type variables") - -check_tyvars dflags clas tys - -- Check that at least one isn't a type variable - -- unless -fallow-undecideable-instances - | dopt Opt_AllowUndecidableInstances dflags = returnTc () - | not (all tcIsTyVarTy tys) = returnTc () - | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg) - where - msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head") - $$ undecidableMsg) - -undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this") \end{code} \begin{code} instTypeErr pp_ty msg = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, nest 4 msg] +\end{code} + + +%************************************************************************ +%* * +\subsection{Checking instance for termination} +%* * +%************************************************************************ + +Termination test: each assertion in the context satisfies + (1) no variable has more occurrences in the assertion than in the head, and + (2) the assertion has fewer constructors and variables (taken together + and counting repetitions) than the head. +This is only needed with -fglasgow-exts, as Haskell 98 restrictions +(which have already been checked) guarantee termination. + +\begin{code} +checkInstTermination :: ThetaType -> [TcType] -> TcM () +checkInstTermination theta tys + = do + dflags <- getDOpts + check_inst_termination dflags theta tys + +check_inst_termination dflags theta tys + | not (dopt Opt_GlasgowExts dflags) = returnM () + | dopt Opt_AllowUndecidableInstances dflags = returnM () + | otherwise = do + mappM_ (check_nomore (fvTypes tys)) theta + mappM_ (check_smaller (sizeTypes tys)) theta + +check_nomore :: [TyVar] -> PredType -> TcM () +check_nomore fvs pred + = checkTc (null (fvPred pred \\ fvs)) + (predUndecErr pred nomoreMsg $$ parens undecidableMsg) + +check_smaller :: Int -> PredType -> TcM () +check_smaller n pred + = checkTc (sizePred pred < n) + (predUndecErr pred smallerMsg $$ parens undecidableMsg) + +predUndecErr pred msg = sep [msg, + nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)] + +nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head") +smallerMsg = ptext SLIT("Constraint is no smaller than the instance head") +undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this") -nonBoxedPrimCCallErr clas inst_ty - = hang (ptext SLIT("Unacceptable instance type for ccall-ish class")) - 4 (pprClassPred clas [inst_ty]) +-- free variables of a type, retaining repetitions +fvType :: Type -> [TyVar] +fvType ty | Just exp_ty <- tcView ty = fvType exp_ty +fvType (TyVarTy tv) = [tv] +fvType (TyConApp _ tys) = fvTypes tys +fvType (NoteTy _ ty) = fvType ty +fvType (PredTy pred) = fvPred pred +fvType (FunTy arg res) = fvType arg ++ fvType res +fvType (AppTy fun arg) = fvType fun ++ fvType arg +fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty) + +fvTypes :: [Type] -> [TyVar] +fvTypes tys = concat (map fvType tys) + +fvPred :: PredType -> [TyVar] +fvPred (ClassP _ tys') = fvTypes tys' +fvPred (IParam _ ty) = fvType ty + +-- size of a type: the number of variables and constructors +sizeType :: Type -> Int +sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty +sizeType (TyVarTy _) = 1 +sizeType (TyConApp _ tys) = sizeTypes tys + 1 +sizeType (NoteTy _ ty) = sizeType ty +sizeType (PredTy pred) = sizePred pred +sizeType (FunTy arg res) = sizeType arg + sizeType res + 1 +sizeType (AppTy fun arg) = sizeType fun + sizeType arg +sizeType (ForAllTy _ ty) = sizeType ty + +sizeTypes :: [Type] -> Int +sizeTypes xs = sum (map sizeType xs) + +sizePred :: PredType -> Int +sizePred (ClassP _ tys') = sizeTypes tys' +sizePred (IParam _ ty) = sizeType ty \end{code}