X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=1d163aaed49c63445049ef0d9206efc6e2bc5f09;hp=dd7b6272ecc277021e5170fc0d012de4190c9528;hb=35a1ec430a5e44a9bc79d385b997422c20cb427b;hpb=cc6f35b14bd2bb06ff73bf76249bcf9df50dd225 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index dd7b627..1d163aa 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -18,41 +18,52 @@ module TcMType ( newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newKindVar, newKindVars, - lookupTcTyVar, LookupTyVarResult(..), - newMetaTyVar, readMetaTyVar, writeMetaTyVar, + mkTcTyVarName, - -------------------------------- - -- Boxy type variables - newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, + newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, + isFilledMetaTyVar, isFlexiMetaTyVar, -------------------------------- - -- Creating new coercion variables - newCoVars, + -- Creating new evidence variables + newEvVar, newCoVar, newEvVars, + writeWantedCoVar, readWantedCoVar, + newIP, newDict, newSilentGiven, isSilentEvVar, + + newWantedEvVar, newWantedEvVars, + newTcEvBinds, addTcEvBind, -------------------------------- -- Instantiation - tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, - tcInstSigTyVars, zonkSigTyVar, - tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, + tcInstTyVars, tcInstSigTyVars, + tcInstType, + tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType, + tcSkolDFunType, tcSuperSkolTyVars, -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, - SourceTyCtxt(..), checkValidTheta, checkFreeness, - checkValidInstHead, checkValidInstance, checkAmbiguity, - checkInstTermination, + Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, + SourceTyCtxt(..), checkValidTheta, + checkValidInstance, + checkValidTypeInst, checkTyFamFreeness, arityErr, + growPredTyVars, growThetaTyVars, validDerivPred, -------------------------------- -- Zonking - zonkType, zonkTcPredType, - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar, - zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, - zonkTcKindToKind, zonkTcKind, + zonkType, mkZonkTcTyVar, zonkTcPredType, + zonkTcTypeCarefully, + skolemiseUnboundMetaTyVar, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, + zonkQuantifiedTyVar, zonkQuantifiedTyVars, + zonkTcType, zonkTcTypes, zonkTcThetaType, + zonkTcKindToKind, zonkTcKind, + zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar, + zonkWC, zonkWantedEvVars, + zonkTcTypeAndSubst, + tcGetGlobalTyVars, - readKindVar, writeKindVar + readKindVar, writeKindVar ) where #include "HsVersions.h" @@ -61,14 +72,15 @@ module TcMType ( import TypeRep import TcType import Type -import Type import Coercion import Class import TyCon import Var -- others: -import TcRnMonad -- TcType, amongst others +import HsSyn -- HsType +import TcRnMonad -- TcType, amongst others +import Id import FunDeps import Name import VarSet @@ -77,65 +89,100 @@ import DynFlags import Util import Maybes import ListSetOps -import UniqSupply +import BasicTypes +import SrcLoc import Outputable +import FastString +import Unique( Unique ) +import Bag -import Control.Monad ( when ) -import Data.List ( (\\) ) +import Control.Monad +import Data.List ( (\\) ) \end{code} %************************************************************************ %* * - Instantiation in general + Kind variables %* * %************************************************************************ \begin{code} -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 +newKindVar :: TcM TcKind +newKindVar = do { uniq <- newUnique + ; ref <- newMutVar Flexi + ; return (mkTyVarTy (mkKindVar uniq ref)) } - ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) - ; return (tyvars', theta, tau) } +newKindVars :: Int -> TcM [TcKind] +newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ()) \end{code} %************************************************************************ %* * - Kind variables + Evidence variables; range over constraints we can abstract over %* * %************************************************************************ \begin{code} -newCoVars :: [(TcType,TcType)] -> TcM [CoVar] -newCoVars spec - = do { us <- newUniqueSupply - ; return [ mkCoVar (mkSysTvName uniq FSLIT("co")) - (mkCoKind ty1 ty2) - | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] } - -newKindVar :: TcM TcKind -newKindVar = do { uniq <- newUnique - ; ref <- newMutVar Flexi - ; return (mkTyVarTy (mkKindVar uniq ref)) } - -newKindVars :: Int -> TcM [TcKind] -newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) +newEvVars :: TcThetaType -> TcM [EvVar] +newEvVars theta = mapM newEvVar theta + +newWantedEvVar :: TcPredType -> TcM EvVar +newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2 +newWantedEvVar (ClassP cls tys) = newDict cls tys +newWantedEvVar (IParam ip ty) = newIP ip ty + +newWantedEvVars :: TcThetaType -> TcM [EvVar] +newWantedEvVars theta = mapM newWantedEvVar theta + +-------------- +newEvVar :: TcPredType -> TcM EvVar +-- Creates new *rigid* variables for predicates +newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2 +newEvVar (ClassP cls tys) = newDict cls tys +newEvVar (IParam ip ty) = newIP ip ty + +newCoVar :: TcType -> TcType -> TcM CoVar +newCoVar ty1 ty2 + = do { name <- newName (mkTyVarOccFS (fsLit "co")) + ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) } + +newIP :: IPName Name -> TcType -> TcM IpId +newIP ip ty + = do { name <- newName (getOccName (ipNameName ip)) + ; return (mkLocalId name (mkPredTy (IParam ip ty))) } + +newDict :: Class -> [TcType] -> TcM DictId +newDict cls tys + = do { name <- newName (mkDictOcc (getOccName cls)) + ; return (mkLocalId name (mkPredTy (ClassP cls tys))) } + +newName :: OccName -> TcM Name +newName occ + = do { uniq <- newUnique + ; loc <- getSrcSpanM + ; return (mkInternalName uniq occ loc) } + +----------------- +newSilentGiven :: PredType -> TcM EvVar +-- Make a dictionary for a "silent" given dictionary +-- Behaves just like any EvVar except that it responds True to isSilentDict +-- This is used only to suppress confusing error reports +newSilentGiven (ClassP cls tys) + = do { uniq <- newUnique + ; let name = mkSystemName uniq (mkDictOcc (getOccName cls)) + ; return (mkLocalId name (mkPredTy (ClassP cls tys))) } +newSilentGiven (EqPred ty1 ty2) + = do { uniq <- newUnique + ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co")) + ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) } +newSilentGiven pred@(IParam {}) + = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier + +isSilentEvVar :: EvVar -> Bool +isSilentEvVar v = isSystemName (Var.varName v) + -- Notice that all *other* evidence variables get Internal Names \end{code} @@ -146,33 +193,82 @@ newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) %************************************************************************ \begin{code} -mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar -mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info) +tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables + -> TcType -- Type to instantiate + -> TcM ([TcTyVar], TcThetaType, TcType) -- Result + -- (type vars (excl coercion vars), preds (incl equalities), rho) +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 any nested foralls have different binders. + -- Either way, zipTopTvSubst is ok -tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType) + ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) + ; return (tyvars', theta, tau) } + +tcSkolDFunType :: 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 +-- be in the type environment: it is lexically scoped. +tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty -tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] +tcSuperSkolTyVars :: [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 ] +-- Moreover, make them "super skolems"; see comments with superSkolemTv +tcSuperSkolTyVars tyvars + = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv + | tv <- tyvars ] + +tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar +-- Instantiate the tyvar, using +-- * the occ-name and kind of the supplied tyvar, +-- * the unique from the monad, +-- * the location either from the tyvar (skol_info = SigSkol) +-- or from the monad (otherwise) +tcInstSkolTyVar overlappable tyvar + = do { uniq <- newUnique + ; loc <- getSrcSpanM + ; let new_name = mkInternalName uniq occ loc + ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) } + where + old_name = tyVarName tyvar + occ = nameOccName old_name + kind = tyVarKind tyvar -tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) --- Instantiate a type with fresh skolem constants -tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty +tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar] +tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars -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) } +tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar] +tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars -tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] -tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars +tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType) +-- Instantiate a type with fresh skolem constants +-- Binding location comes from the monad +tcInstSkolType ty = tcInstType tcInstSkolTyVars ty + +tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar] +-- Make meta SigTv type variables for patten-bound scoped type varaibles +-- We use SigTvs for them, so that they can't unify with arbitrary types +tcInstSigTyVars = mapM tcInstSigTyVar + +tcInstSigTyVar :: TyVar -> TcM TcTyVar +tcInstSigTyVar tyvar + = do { uniq <- newMetaUnique + ; ref <- newMutVar Flexi + ; let name = setNameUnique (tyVarName tyvar) uniq + -- Use the same OccName so that the tidy-er + -- doesn't rename 'a' to 'a0' etc + kind = tyVarKind tyvar + ; return (mkTcTyVar name kind (MetaTv SigTv ref)) } \end{code} @@ -183,54 +279,99 @@ tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars %************************************************************************ \begin{code} -newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar +newMetaTyVar :: MetaInfo -> 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("t") - TauTv -> FSLIT("t") - SigTv _ -> FSLIT("a") - -- We give BoxTv and TauTv the same string, because - -- otherwise we get user-visible differences in error - -- messages, which are confusing. If you want to see - -- the box_info of each tyvar, use -dppr-debug - ; 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)) } +newMetaTyVar meta_info kind + = do { uniq <- newMetaUnique + ; ref <- newMutVar Flexi + ; let name = mkTcTyVarName uniq s + s = case meta_info of + TauTv -> fsLit "t" + TcsTv -> fsLit "u" + SigTv -> fsLit "a" + ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } + +mkTcTyVarName :: Unique -> FastString -> Name +-- Make sure that fresh TcTyVar names finish with a digit +-- leaving the un-cluttered names free for user names +mkTcTyVarName uniq str = mkSysTvName uniq str readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) readMutVar (metaTvRef tyvar) +readWantedCoVar :: CoVar -> TcM MetaDetails +readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar ) + readMutVar (metaTvRef covar) + +isFilledMetaTyVar :: TyVar -> TcM Bool +-- True of a filled-in (Indirect) meta type variable +isFilledMetaTyVar tv + | not (isTcTyVar tv) = return False + | MetaTv _ ref <- tcTyVarDetails tv + = do { details <- readMutVar ref + ; return (isIndirect details) } + | otherwise = return False + +isFlexiMetaTyVar :: TyVar -> TcM Bool +-- True of a un-filled-in (Flexi) meta type variable +isFlexiMetaTyVar tv + | not (isTcTyVar tv) = return False + | MetaTv _ ref <- tcTyVarDetails tv + = do { details <- readMutVar ref + ; return (isFlexi details) } + | otherwise = return False + +-------------------- writeMetaTyVar :: TcTyVar -> TcType -> TcM () -#ifndef DEBUG -writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty) -#else +-- Write into a currently-empty MetaTyVar + writeMetaTyVar tyvar ty - | not (isMetaTyVar tyvar) - = pprTrace "writeMetaTyVar" (ppr tyvar) $ - returnM () + | not debugIsOn + = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty + +-- Everything from here on only happens if DEBUG is on + | not (isTcTyVar tyvar) + = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar ) + return () + + | MetaTv _ ref <- tcTyVarDetails tyvar + = writeMetaTyVarRef tyvar ref ty | 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) } + = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar ) + return () + +writeWantedCoVar :: CoVar -> Coercion -> TcM () +writeWantedCoVar cv co = writeMetaTyVar cv co + +-------------------- +writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM () +-- Here the tyvar is for error checking only; +-- the ref cell must be for the same tyvar +writeMetaTyVarRef tyvar ref ty + | not debugIsOn + = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) + ; writeMutVar ref (Indirect ty) } + +-- Everything from here on only happens if DEBUG is on + | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables + , not (ty_kind `isSubKind` tv_kind) + = WARN( True, hang (text "Ill-kinded update to meta tyvar") + 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) ) + return () + + | otherwise + = do { meta_details <- readMutVar ref; + ; ASSERT2( isFlexi meta_details, + hang (text "Double update of meta tyvar") + 2 (ppr tyvar $$ ppr meta_details) ) + + traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) + ; writeMutVar ref (Indirect ty) } where - k1 = tyVarKind tyvar - k2 = typeKind ty -#endif + tv_kind = tyVarKind tyvar + ty_kind = typeKind ty \end{code} @@ -245,26 +386,32 @@ newFlexiTyVar :: Kind -> TcM TcTyVar newFlexiTyVar kind = newMetaTyVar TauTv kind newFlexiTyVarTy :: Kind -> TcM TcType -newFlexiTyVarTy kind - = newFlexiTyVar kind `thenM` \ tc_tyvar -> - returnM (TyVarTy tc_tyvar) +newFlexiTyVarTy kind = do + tc_tyvar <- newFlexiTyVar kind + return (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 +newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind) 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) } + ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) } -- Since the tyvars are freshly made, -- they cannot possibly be captured by -- any existing for-alls. Hence zipTopTvSubst + +tcInstTyVar :: TyVar -> TcM TcTyVar +-- Make a new unification variable tyvar whose Name and Kind +-- come from an existing TyVar +tcInstTyVar tyvar + = do { uniq <- newMetaUnique + ; ref <- newMutVar Flexi + ; let name = mkSystemName uniq (getOccName tyvar) + kind = tyVarKind tyvar + ; return (mkTcTyVar name kind (MetaTv TauTv ref)) } \end{code} @@ -275,11 +422,6 @@ tcInstTyVars tyvars %************************************************************************ \begin{code} -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 @@ -293,192 +435,219 @@ zonkSigTyVar sig_tv \end{code} -%************************************************************************ -%* * - MetaTvs: BoxTvs -%* * -%************************************************************************ - -\begin{code} -newBoxyTyVar :: Kind -> TcM BoxyTyVar -newBoxyTyVar kind = newMetaTyVar BoxTv kind - -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 -\end{code} - %************************************************************************ %* * -\subsection{Putting and getting mutable type variables} +\subsection{Zonking -- the exernal interfaces} %* * %************************************************************************ -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 -any other type, then there might be bound TyVars embedded inside it. - -We return Nothing iff the original box was unbound. +@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment. +To improve subsequent calls to the same function it writes the zonked set back into +the environment. \begin{code} -data LookupTyVarResult -- The result of a lookupTcTyVar call - = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv - | IndirectTv TcType - -lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult -lookupTcTyVar tyvar - = ASSERT( isTcTyVar 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 (isTcTyVar tyvar) - = pprTrace "getTcTyVar" (ppr tyvar) $ - returnM (Just (mkTyVarTy tyvar)) - - | otherwise - = ASSERT2( isTcTyVar tyvar, ppr tyvar ) - readMetaTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty -> short_out ty `thenM` \ ty' -> - writeMetaTyVar tyvar (Just ty') `thenM_` - returnM (Just ty') - - Nothing -> returnM Nothing - -short_out :: TcType -> TcM TcType -short_out ty@(TyVarTy tyvar) - | not (isTcTyVar tyvar) - = returnM ty - - | otherwise - = readMetaTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> short_out ty' `thenM` \ ty' -> - writeMetaTyVar tyvar (Just ty') `thenM_` - returnM ty' - - other -> returnM ty - -short_out other_ty = returnM other_ty --} +tcGetGlobalTyVars :: TcM TcTyVarSet +tcGetGlobalTyVars + = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv + ; gbl_tvs <- readMutVar gtv_var + ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs + ; writeMutVar gtv_var gbl_tvs' + ; return gbl_tvs' } \end{code} - -%************************************************************************ -%* * -\subsection{Zonking -- the exernal interfaces} -%* * -%************************************************************************ - ----------------- Type variables \begin{code} zonkTcTyVars :: [TcTyVar] -> TcM [TcType] -zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars - -zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet -zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> - returnM (tyVarsOfTypes tys) +zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars -zonkTcTyVar :: TcTyVar -> TcM TcType -zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar ) - zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar -\end{code} +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 (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) + RuntimeUnk {} -> 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 } -\begin{code} zonkTcType :: TcType -> TcM TcType -zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty +-- Simply look through all Flexis +zonkTcType ty = zonkType zonkTcTyVar ty -zonkTcTypes :: [TcType] -> TcM [TcType] -zonkTcTypes tys = mappM zonkTcType tys +zonkTcTyVar :: TcTyVar -> TcM TcType +-- Simply look through all Flexis +zonkTcTyVar tv + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + SkolemTv {} -> return (TyVarTy tv) + RuntimeUnk {} -> return (TyVarTy tv) + FlatSkol ty -> zonkTcType ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; 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) + RuntimeUnk {} -> 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) -zonkTcClassConstraints cts = mappM zonk cts - where zonk (clas, tys) - = zonkTcTypes tys `thenM` \ new_tys -> - returnM (clas, new_tys) +zonkTcTypes :: [TcType] -> TcM [TcType] +zonkTcTypes tys = mapM zonkTcType tys zonkTcThetaType :: TcThetaType -> TcM TcThetaType -zonkTcThetaType theta = mappM zonkTcPredType theta +zonkTcThetaType theta = mapM zonkTcPredType theta zonkTcPredType :: TcPredType -> TcM TcPredType -zonkTcPredType (ClassP c ts) - = zonkTcTypes ts `thenM` \ new_ts -> - returnM (ClassP c new_ts) -zonkTcPredType (IParam n t) - = zonkTcType t `thenM` \ new_t -> - returnM (IParam n new_t) -zonkTcPredType (EqPred t1 t2) - = zonkTcType t1 `thenM` \ new_t1 -> - zonkTcType t2 `thenM` \ new_t2 -> - returnM (EqPred new_t1 new_t2) +zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts +zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t +zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2 \end{code} ------------------- These ...ToType, ...ToKind versions are used at the end of type checking \begin{code} -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 +zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] +zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar + +zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar +-- 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) +-- -- see notes with Kind.defaultKind +-- The meta tyvar is updated to point to the new skolem 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 + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen? + 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, regular type variable + 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 tv vanillaSkolemTv + _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk + +skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> 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 tv details + = ASSERT2( isMetaTyVar tv, ppr tv ) + do { span <- getSrcSpanM -- Get the location from "here" + -- ie where we are generalising + ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land ; 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 + final_name = mkInternalName uniq (getOccName tv) span + final_tv = mkTcTyVar final_name final_kind details + ; writeMetaTyVar tv (mkTyVarTy final_tv) ; return final_tv } \end{code} -[Silly Type Synonyms] +\begin{code} +zonkImplication :: Implication -> TcM Implication +zonkImplication implic@(Implic { ic_given = given + , ic_wanted = wanted + , ic_loc = loc }) + = do { -- No need to zonk the skolems + ; given' <- mapM zonkEvVar given + ; loc' <- zonkGivenLoc loc + ; wanted' <- zonkWC wanted + ; return (implic { ic_given = given' + , ic_wanted = wanted' + , ic_loc = loc' }) } + +zonkEvVar :: EvVar -> TcM EvVar +zonkEvVar var = do { ty' <- zonkTcType (varType var) + ; return (setVarType var ty') } + +zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar +zonkFlavoredEvVar (EvVarX ev fl) + = do { ev' <- zonkEvVar ev + ; fl' <- zonkFlavor fl + ; return (EvVarX ev' fl') } + +zonkWC :: WantedConstraints -> TcM WantedConstraints +zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol }) + = do { flat' <- zonkWantedEvVars flat + ; implic' <- mapBagM zonkImplication implic + ; insol' <- mapBagM zonkFlavoredEvVar insol + ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) } + +zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar) +zonkWantedEvVars = mapBagM zonkWantedEvVar + +zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar +zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) } + +zonkFlavor :: CtFlavor -> TcM CtFlavor +zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') } +zonkFlavor fl = return fl + +zonkGivenLoc :: GivenLoc -> TcM GivenLoc +-- GivenLocs may have unification variables inside them! +zonkGivenLoc (CtLoc skol_info span ctxt) + = do { skol_info' <- zonkSkolemInfo skol_info + ; return (CtLoc skol_info' span ctxt) } + +zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo +zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty + ; return (SigSkol cx ty') } +zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys + ; return (InferSkol ntys') } + where + do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') } +zonkSkolemInfo skol_info = return skol_info +\end{code} +Note [Silly Type Synonyms] +~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: type C u a = u -- Note 'a' unused @@ -498,7 +667,7 @@ Consider this: * Now abstract over the 'a', but float out the Num (C d a) constraint because it does not 'really' mention a. (see exactTyVarsOfType) The arg to foo becomes - /\a -> \t -> t+t + \/\a -> \t -> t+t * So we get a dict binding for Num (C d a), which is zonked to give a = () @@ -507,10 +676,41 @@ Consider this: 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. +* Then the \/\a abstraction has a zonked 'a' in it. 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 () +a \/\a in the final result but all the occurrences of a will be zonked to () + +Note [Zonking to Skolem] +~~~~~~~~~~~~~~~~~~~~~~~~ +We used to zonk quantified type variables to regular TyVars. However, this +leads to problems. Consider this program from the regression test suite: + + eval :: Int -> String -> String -> String + eval 0 root actual = evalRHS 0 root actual + + evalRHS :: Int -> a + evalRHS 0 root actual = eval 0 root actual + +It leads to the deferral of an equality (wrapped in an implication constraint) + + forall a. (String -> String -> String) ~ a + +which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck). +In the meantime `a' is zonked and quantified to form `evalRHS's signature. +This has the *side effect* of also zonking the `a' in the deferred equality +(which at this point is being handed around wrapped in an implication +constraint). + +Finally, the equality (with the zonked `a') will be handed back to the +simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop. +If we zonk `a' with a regular type variable, we will have this regular type +variable now floating around in the simplifier, which in many places assumes to +only see proper TcTyVars. + +We can avoid this problem by zonking with a skolem. The skolem is rigid +(which we require for a quantified variable), but is still a TcTyVar that the +simplifier knows how to deal with. %************************************************************************ @@ -526,60 +726,69 @@ a /\a in the final result but all the occurrences of a will be zonked to () -- 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 unbound_var_fn ty +zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars + -> TcType -> TcM Type +zonkType zonk_tc_tyvar ty = go ty where - 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') + go (TyConApp tc tys) = do tys' <- mapM go tys + return (TyConApp tc tys') + + go (PredTy p) = do p' <- go_pred p + return (PredTy p') + + go (FunTy arg res) = do arg' <- go arg + res' <- go res + return (FunTy arg' res') + + go (AppTy fun arg) = do fun' <- go fun + arg' <- go arg + return (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) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar - | otherwise = return (TyVarTy tyvar) + go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar + | otherwise = liftM TyVarTy $ + zonkTyVar zonk_tc_tyvar 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 (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do + ty' <- go ty + tyvar' <- zonkTyVar zonk_tc_tyvar tyvar + return (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') - go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' -> - go ty2 `thenM` \ ty2' -> - returnM (EqPred ty1' ty2') + go_pred (ClassP c tys) = do tys' <- mapM go tys + return (ClassP c tys') + go_pred (IParam n ty) = do ty' <- go ty + return (IParam n ty') + go_pred (EqPred ty1 ty2) = do ty1' <- go ty1 + ty2' <- go ty2 + return (EqPred ty1' ty2') -zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable +mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var -> 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 } +mkZonkTcTyVar unbound_var_fn tyvar + = ASSERT( isTcTyVar tyvar ) + case tcTyVarDetails tyvar of + SkolemTv {} -> return (TyVarTy tyvar) + RuntimeUnk {} -> 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). +zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar + -> TyVar -> TcM TyVar +zonkTyVar zonk_tc_tyvar tv + | isCoVar tv + = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv) + ; return $ setTyVarKind tv kind } + | otherwise = return tv \end{code} @@ -604,7 +813,8 @@ zonkTcKind k = zonkTcType k zonkTcKindToKind :: TcKind -> TcM Kind -- When zonking a TcKind to a kind, we need to instantiate kind variables, -- Haskell specifies that * is to be used, so we follow that. -zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k +zonkTcKindToKind k + = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k \end{code} %************************************************************************ @@ -644,85 +854,183 @@ This might not necessarily show up in kind checking. \begin{code} checkValidType :: UserTypeCtxt -> Type -> TcM () -- Checks that the type is valid for the given context -checkValidType ctxt ty - = traceTc (text "checkValidType" <+> ppr ty) `thenM_` - doptM Opt_GlasgowExts `thenM` \ gla_exts -> +checkValidType ctxt ty = do + traceTc "checkValidType" (ppr ty) + unboxed <- xoptM Opt_UnboxedTuples + rank2 <- xoptM Opt_Rank2Types + rankn <- xoptM Opt_RankNTypes + polycomp <- xoptM Opt_PolymorphicComponents let - rank | gla_exts = Arbitrary - | otherwise - = case ctxt of -- Haskell 98 - GenPatCtxt -> Rank 0 - LamPatSigCtxt -> Rank 0 - BindPatSigCtxt -> Rank 0 - DefaultDeclCtxt-> Rank 0 - ResSigCtxt -> Rank 0 - TySynCtxt _ -> Rank 0 - ExprSigCtxt -> Rank 1 - FunSigCtxt _ -> Rank 1 - ConArgCtxt _ -> Rank 1 -- We are given the type of the entire - -- constructor, hence rank 1 - ForSigCtxt _ -> Rank 1 - RuleSigCtxt _ -> Rank 1 - SpecInstCtxt -> Rank 1 + gen_rank n | rankn = ArbitraryRank + | rank2 = Rank 2 + | otherwise = Rank n + rank + = case ctxt of + DefaultDeclCtxt-> MustBeMonoType + ResSigCtxt -> MustBeMonoType + LamPatSigCtxt -> gen_rank 0 + BindPatSigCtxt -> gen_rank 0 + TySynCtxt _ -> gen_rank 0 + GenPatCtxt -> gen_rank 1 + -- This one is a bit of a hack + -- See the forall-wrapping in TcClassDcl.mkGenericInstance + + ExprSigCtxt -> gen_rank 1 + FunSigCtxt _ -> gen_rank 1 + ConArgCtxt _ | polycomp -> gen_rank 2 + -- We are given the type of the entire + -- constructor, hence rank 1 + | otherwise -> gen_rank 1 + + ForSigCtxt _ -> gen_rank 1 + SpecInstCtxt -> gen_rank 1 + ThBrackCtxt -> gen_rank 1 + GenSigCtxt -> panic "checkValidType" + -- Can't happen; GenSigCtxt not used for *user* sigs actual_kind = typeKind ty kind_ok = case ctxt of - TySynCtxt _ -> True -- Any kind will do - ResSigCtxt -> isSubOpenTypeKind actual_kind - ExprSigCtxt -> isSubOpenTypeKind actual_kind + TySynCtxt _ -> True -- Any kind will do + ThBrackCtxt -> True -- Any kind will do + ResSigCtxt -> isSubOpenTypeKind actual_kind + ExprSigCtxt -> isSubOpenTypeKind actual_kind GenPatCtxt -> isLiftedTypeKind actual_kind ForSigCtxt _ -> isLiftedTypeKind actual_kind - other -> isSubArgTypeKind actual_kind + _ -> isSubArgTypeKind 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 - -- Check that the thing has kind Type, and is lifted if necessary - checkTc kind_ok (kindErr actual_kind) `thenM_` + ubx_tup = case ctxt of + TySynCtxt _ | unboxed -> UT_Ok + ExprSigCtxt | unboxed -> UT_Ok + ThBrackCtxt | unboxed -> UT_Ok + _ -> UT_NotOk -- Check the internal validity of the type itself - check_poly_type rank ubx_tup ty `thenM_` + check_type rank ubx_tup ty - traceTc (text "checkValidType done" <+> ppr ty) + -- Check that the thing has kind Type, and is lifted if necessary + -- Do this second, becuase we can't usefully take the kind of an + -- ill-formed type such as (a~Int) + checkTc kind_ok (kindErr actual_kind) + + traceTc "checkValidType done" (ppr ty) + +checkValidMonoType :: Type -> TcM () +checkValidMonoType ty = check_mono_type MustBeMonoType ty \end{code} \begin{code} -data Rank = Rank Int | Arbitrary - -decRank :: Rank -> Rank -decRank Arbitrary = Arbitrary -decRank (Rank n) = Rank (n-1) +data Rank = ArbitraryRank -- Any rank ok + | MustBeMonoType -- Monotype regardless of flags + | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes + | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms + | Rank Int -- Rank n, but could be more with -XRankNTypes + +decRank :: Rank -> Rank -- Function arguments +decRank (Rank 0) = Rank 0 +decRank (Rank n) = Rank (n-1) +decRank other_rank = other_rank + +nonZeroRank :: Rank -> Bool +nonZeroRank ArbitraryRank = True +nonZeroRank (Rank n) = n>0 +nonZeroRank _ = False ---------------------------------------- data UbxTupFlag = UT_Ok | UT_NotOk - -- The "Ok" version means "ok if -fglasgow-exts is on" + -- The "Ok" version means "ok if UnboxedTuples is on" ---------------------------------------- -check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM () -check_poly_type (Rank 0) ubx_tup ty - = check_tau_type (Rank 0) ubx_tup ty - -check_poly_type rank ubx_tup ty - | null tvs && null theta - = check_tau_type rank ubx_tup ty - | otherwise - = do { check_valid_theta SigmaCtxt theta - ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow - ; checkFreeness tvs theta +check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere + -- No unlifted types of any kind +check_mono_type rank ty + = do { check_type rank UT_NotOk ty + ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } + +check_type :: Rank -> UbxTupFlag -> Type -> TcM () +-- The args say what the *type context* requires, independent +-- of *flag* settings. You test the flag settings at usage sites. +-- +-- Rank is allowed rank for function args +-- Rank 0 means no for-alls anywhere + +check_type rank ubx_tup ty + | not (null tvs && null theta) + = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty) + -- Reject e.g. (Maybe (?x::Int => Int)), + -- with a decent error message + ; check_valid_theta SigmaCtxt theta + ; check_type rank ubx_tup tau -- Allow foralls to right of arrow ; checkAmbiguity tvs theta (tyVarsOfType tau) } where (tvs, theta, tau) = tcSplitSigmaTy ty +-- Naked PredTys should, I think, have been rejected before now +check_type _ _ ty@(PredTy {}) + = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type") + +check_type _ _ (TyVarTy _) = return () + +check_type rank _ (FunTy arg_ty res_ty) + = do { check_type (decRank rank) UT_NotOk arg_ty + ; check_type rank UT_Ok res_ty } + +check_type rank _ (AppTy ty1 ty2) + = do { check_arg_type rank ty1 + ; check_arg_type rank ty2 } + +check_type rank ubx_tup ty@(TyConApp tc tys) + | isSynTyCon tc + = do { -- Check that the synonym has enough args + -- This applies equally to open and closed synonyms + -- It's OK to have an *over-applied* type synonym + -- data Tree a b = ... + -- type Foo a = Tree [a] + -- f :: Foo a b -> ... + checkTc (tyConArity tc <= length tys) arity_msg + + -- See Note [Liberal type synonyms] + ; 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 + + else -- In the liberal case (only for closed syns), expand then check + case tcView ty of + Just ty' -> check_type rank ubx_tup ty' + Nothing -> pprPanic "check_tau_type" (ppr ty) + } + + | isUnboxedTupleTyCon tc + = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples + ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg + + ; 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 + -- more unboxed tuples, so can't use check_arg_ty + ; mapM_ (check_type rank' UT_Ok) tys } + + | otherwise + = mapM_ (check_arg_type rank) tys + + where + ubx_tup_ok ub_tuples_allowed = case ubx_tup of + UT_Ok -> ub_tuples_allowed + _ -> False + + n_args = length tys + tc_arity = tyConArity tc + + arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args + ubx_tup_msg = ubxArgTyErr ty + +check_type _ _ ty = pprPanic "check_type" (ppr ty) + ---------------------------------------- -check_arg_type :: Type -> TcM () +check_arg_type :: Rank -> Type -> TcM () -- The sort of type that can instantiate a type variable, -- or be the argument of a type constructor. -- Not an unboxed tuple, but now *can* be a forall (since impredicativity) @@ -741,91 +1049,67 @@ check_arg_type :: Type -> TcM () -- But not in user code. -- Anyway, they are dealt with by a special case in check_tau_type -check_arg_type ty - = check_poly_type Arbitrary UT_NotOk ty `thenM_` - checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) - ----------------------------------------- -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 ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty) - -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message +check_arg_type rank ty + = do { impred <- xoptM Opt_ImpredicativeTypes + ; let rank' = case rank of -- Predictive => must be monotype + MustBeMonoType -> MustBeMonoType -- Monotype, regardless + _other | impred -> ArbitraryRank + | otherwise -> TyConArgMonoType + -- Make sure that MustBeMonoType is propagated, + -- so that we don't suggest -XImpredicativeTypes in + -- (Ord (forall a.a)) => a -> a + -- and so that if it Must be a monotype, we check that it is! --- 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_pred_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 (decRank 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 `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 () - -- f :: S (T Int) - -- Here, T is partially applied, so it's illegal in H98. - -- But if you expand S first, then T we get just - -- f :: Int - -- which is fine. - returnM () - else - -- For H98, do check the type args - mappM_ check_arg_type tys - } - - | isUnboxedTupleTyCon tc - = 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 - = mappM_ check_arg_type tys + ; check_type rank' UT_NotOk ty + ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } +---------------------------------------- +forAllTyErr :: Rank -> Type -> SDoc +forAllTyErr rank ty + = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty) + , suggestion ] where - ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False } + suggestion = case rank of + Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types") + TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes") + SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms") + _ -> empty -- Polytype is always illegal + +unliftedArgErr, ubxArgTyErr :: Type -> SDoc +unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty] +ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty] + +kindErr :: Kind -> SDoc +kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind] +\end{code} - n_args = length tys - tc_arity = tyConArity tc +Note [Liberal type synonyms] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If -XLiberalTypeSynonyms is on, expand closed type synonyms *before* +doing validity checking. 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 () + f :: S (T Int) +Here, T is partially applied, so it's illegal in H98. But if you +expand S first, then T we get just + f :: Int +which is fine. - arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args - ubx_tup_msg = ubxArgTyErr ty +IMPORTANT: suppose T is a type synonym. Then we must do validity +checking on an appliation (T ty1 ty2) ----------------------------------------- -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} + *either* before expansion (i.e. check ty1, ty2) + *or* after expansion (i.e. expand T ty1 ty2, and then check) + BUT NOT BOTH +If we do both, we get exponential behaviour!! + + data TIACons1 i r c = c i ::: r c + type TIACons2 t x = TIACons1 t (TIACons1 t x) + type TIACons3 t x = TIACons2 t (TIACons1 t x) + type TIACons4 t x = TIACons2 t (TIACons2 t x) + type TIACons7 t x = TIACons4 t (TIACons3 t x) %************************************************************************ @@ -853,11 +1137,12 @@ data SourceTyCtxt | InstThetaCtxt -- Context 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 TypeCtxt = ptext SLIT("the context of a type") +pprSourceTyCtxt :: SourceTyCtxt -> SDoc +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 TypeCtxt = ptext (sLit "the context of a type") \end{code} \begin{code} @@ -866,36 +1151,52 @@ checkValidTheta ctxt theta = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta) ------------------------- -check_valid_theta ctxt [] - = returnM () -check_valid_theta ctxt theta - = getDOpts `thenM` \ dflags -> - warnTc (notNull dups) (dupPredWarn dups) `thenM_` - mappM_ (check_pred_ty dflags ctxt) theta +check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM () +check_valid_theta _ [] + = return () +check_valid_theta ctxt theta = do + dflags <- getDOpts + warnTc (notNull dups) (dupPredWarn dups) + mapM_ (check_pred_ty dflags ctxt) theta where (_,dups) = removeDups tcCmpPred theta ------------------------- +check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM () check_pred_ty dflags ctxt pred@(ClassP cls tys) - = -- Class predicates are valid in all contexts - 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) - + = do { -- Class predicates are valid in all contexts + ; checkTc (arity == n_tys) arity_err + + -- Check the form of the argument types + ; mapM_ checkValidMonoType tys + ; checkTc (check_class_pred_tys dflags ctxt tys) + (predTyVarErr pred $$ how_to_allow) + } where class_name = className cls arity = classArity cls n_tys = length tys arity_err = arityErr "Class" class_name arity n_tys - how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this")) + how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this")) + -check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty - -- Implicit parameters only allows in type +check_pred_ty dflags ctxt pred@(EqPred ty1 ty2) + = do { -- Equational constraints are valid in all contexts if type + -- families are permitted + ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred) + ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True) + (eqSuperClassErr pred) + + -- Check the form of the argument types + ; checkValidMonoType ty1 + ; checkValidMonoType ty2 + } + +check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty + -- Implicit parameters only allowed in type -- signatures; not in instance decls, superclasses etc - -- The reason for not allowing implicit params in instances is a bit subtle + -- The reason for not allowing implicit params in instances is a bit + -- subtle. -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ... -- then when we saw (e :: (?x::Int) => t) it would be unclear how to -- discharge all the potential usas of the ?x in e. For example, a @@ -903,21 +1204,23 @@ check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- instance decl would show up two uses of ?x. -- Catch-all -check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty) +check_pred_ty _ _ sty = failWithTc (badPredTyErr sty) ------------------------- +check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool check_class_pred_tys dflags ctxt tys = case ctxt of TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine - InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys + InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys -- Further checks on head and theta in -- checkInstTermination - other -> gla_exts || all tyvar_head tys + _ -> flexible_contexts || all tyvar_head tys where - gla_exts = dopt Opt_GlasgowExts dflags - undecidable_ok = dopt Opt_AllowUndecidableInstances dflags + flexible_contexts = xopt Opt_FlexibleContexts dflags + undecidable_ok = xopt Opt_UndecidableInstances dflags ------------------------- +tyvar_head :: Type -> Bool tyvar_head ty -- Haskell 98 allows predicates of form | tcIsTyVarTy ty = True -- C (a ty1 .. tyn) | otherwise -- where a is a type variable @@ -956,72 +1259,115 @@ 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). +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} checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM () checkAmbiguity forall_tyvars theta tau_tyvars - = mappM_ complain (filter is_ambig theta) + = mapM_ complain (filter is_ambig theta) where complain pred = addErrTc (ambigErr pred) - extended_tau_vars = grow theta tau_tyvars + extended_tau_vars = growThetaTyVars 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' + -- See Note [Implicit parameters and ambiguity] in TcSimplify is_ambig pred = isClassPred pred && any ambig_var (varSetElems (tyVarsOfPred pred)) ambig_var ct_var = (ct_var `elem` forall_tyvars) && not (ct_var `elemVarSet` extended_tau_vars) +ambigErr :: PredType -> SDoc 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 '=>'"))] + = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred), + nest 2 (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. + +Note [Growing the tau-tvs using constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +(growInstsTyVars insts tvs) is the result of extending the set + of tyvars tvs using all conceivable links from pred + +E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e} +Then grow precs tvs = {a,b,c} \begin{code} -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) - -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)")) - ] +growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet +-- See Note [Growing the tau-tvs using constraints] +growThetaTyVars theta tvs + | null theta = tvs + | otherwise = fixVarSet mk_next tvs + where + mk_next tvs = foldr grow_one tvs theta + grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs + +growPredTyVars :: TcPredType + -> TyVarSet -- The set to extend + -> TyVarSet -- TyVars of the predicate if it intersects + -- the set, or is implicit parameter +growPredTyVars pred tvs + | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity] + | pred_tvs `intersectsVarSet` tvs = pred_tvs + | otherwise = emptyVarSet + where + pred_tvs = tyVarsOfPred pred \end{code} + +Note [Implicit parameters and ambiguity] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +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' + +Furthermore, the type variables fixed by an implicit parameter +propagate to the others. E.g. + foo :: (Show a, ?x::[a]) => Int + foo = show (?x++?x) +The type of foo looks ambiguous. But it isn't, because at a call site +we might have + let ?x = 5::Int in foo +and all is well. In effect, implicit parameters are, well, parameters, +so we can take their type variables into account as part of the +"tau-tvs" stuff. This is done in the function 'FunDeps.grow'. + \begin{code} +checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc checkThetaCtxt ctxt theta - = vcat [ptext SLIT("In the context:") <+> pprTheta theta, - ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] - -badPredTyErr 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) - + = vcat [ptext (sLit "In the context:") <+> pprTheta theta, + ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ] + +eqSuperClassErr :: PredType -> SDoc +eqSuperClassErr pred + = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:")) + 2 (ppr pred) + +badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc +badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred +eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred + $$ + parens (ptext (sLit "Use -XTypeFamilies to permit this")) +predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"), + nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)] +dupPredWarn :: [[PredType]] -> SDoc +dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) + +arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc 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] + = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"), + n_arguments <> comma, text "but has been given", + if m==0 then text "none" else int m] where - n_arguments | n == 0 = ptext SLIT("no arguments") - | n == 1 = ptext SLIT("1 argument") - | True = hsep [int n, ptext SLIT("arguments")] + n_arguments | n == 0 = ptext (sLit "no arguments") + | n == 1 = ptext (sLit "1 argument") + | True = hsep [int n, ptext (sLit "arguments")] \end{code} - %************************************************************************ %* * \subsection{Checking for a decent instance head type} @@ -1038,50 +1384,52 @@ compiled elsewhere). In these cases, we let them go through anyway. We can also have instances for functions: @instance Foo (a -> b) ...@. \begin{code} -checkValidInstHead :: Type -> TcM (Class, [TcType]) - -checkValidInstHead ty -- Should be a source type - = case tcSplitPredTy_maybe ty of { - Nothing -> failWithTc (instTypeErr (ppr ty) empty) ; - Just pred -> - - case getClassPredTys_maybe pred of { - Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ; - Just (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 - -- If GlasgowExts then check at least one isn't a type variable - | dopt Opt_GlasgowExts dflags - = mapM_ check_one tys - - -- WITH HASKELL 98, MUST HAVE C (T a b c) - | otherwise - = checkTc (isSingleton tys && tcValidInstHeadTy first_ty) - (instTypeErr (pprClassPred clas tys) head_shape_msg) - - where - (first_ty : _) = tys - - 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") - +checkValidInstHead :: Class -> [Type] -> TcM () +checkValidInstHead clas tys + = do { dflags <- getDOpts + + -- If GlasgowExts then check at least one isn't a type variable + ; checkTc (xopt Opt_TypeSynonymInstances dflags || + all tcInstHeadTyNotSynonym tys) + (instTypeErr pp_pred head_type_synonym_msg) + ; checkTc (xopt Opt_FlexibleInstances dflags || + all tcInstHeadTyAppAllTyVars tys) + (instTypeErr pp_pred head_type_args_tyvars_msg) + ; checkTc (xopt Opt_MultiParamTypeClasses dflags || + isSingleton tys) + (instTypeErr pp_pred head_one_type_msg) + -- May not contain type family applications + ; mapM_ checkTyFamFreeness tys + + ; mapM_ checkValidMonoType tys -- For now, I only allow tau-types (not polytypes) in -- the head of an instance decl. -- E.g. instance C (forall a. a->a) is rejected -- One could imagine generalising that, but I'm not sure -- what all the consequences might be - check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty - ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } + } + where + pp_pred = pprClassPred clas tys + head_type_synonym_msg = parens ( + text "All instance types must be of the form (T t1 ... tn)" $$ + text "where T is not a synonym." $$ + text "Use -XTypeSynonymInstances if you want to disable this.") + + head_type_args_tyvars_msg = parens (vcat [ + text "All instance types must be of the form (T a1 ... an)", + text "where a1 ... an are *distinct type variables*,", + text "and each type variable appears at most once in the instance head.", + text "Use -XFlexibleInstances if you want to disable this."]) + + head_one_type_msg = parens ( + text "Only one type can be given in an instance head." $$ + text "Use -XMultiParamTypeClasses if you want to allow more.") + +instTypeErr :: SDoc -> SDoc -> SDoc instTypeErr pp_ty msg - = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, - nest 4 msg] + = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, + nest 2 msg] \end{code} @@ -1091,31 +1439,41 @@ instTypeErr pp_ty msg %* * %************************************************************************ - \begin{code} -checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () -checkValidInstance tyvars theta clas inst_tys - = do { gla_exts <- doptM Opt_GlasgowExts - ; undecidable_ok <- doptM Opt_AllowUndecidableInstances - - ; checkValidTheta InstThetaCtxt theta +checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType + -> Class -> [TcType] -> TcM () +checkValidInstance hs_type tyvars theta clas inst_tys + = setSrcSpan (getLoc hs_type) $ + do { setSrcSpan head_loc (checkValidInstHead clas inst_tys) + ; checkValidTheta InstThetaCtxt theta ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) -- Check that instance inference will terminate (if we care) - -- For Haskell 98, checkValidTheta has already done that - ; when (gla_exts && not undecidable_ok) $ - mapM_ failWithTc (checkInstTermination inst_tys theta) + -- For Haskell 98 this will already have been done by checkValidTheta, + -- but as we may be using other extensions we need to check. + ; undecidable_ok <- xoptM Opt_UndecidableInstances + ; unless undecidable_ok $ + mapM_ addErrTc (checkInstTermination inst_tys theta) -- The Coverage Condition ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) (instTypeErr (pprClassPred clas inst_tys) msg) - } + } where - msg = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"), + msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"), undecidableMsg]) + + -- The location of the "head" of the instance + head_loc = case hs_type of + L _ (HsForAllTy _ _ _ (L loc _)) -> loc + L loc _ -> loc \end{code} -Termination test: each assertion in the context satisfies +Termination test: the so-called "Paterson conditions" (see Section 5 of +"Understanding functionsl dependencies via Constraint Handling Rules, +JFP Jan 2007). + +We check that 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. @@ -1143,19 +1501,123 @@ checkInstTermination tys theta | otherwise = Nothing +predUndecErr :: PredType -> SDoc -> SDoc predUndecErr pred msg = sep [msg, - nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)] + 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") +nomoreMsg, smallerMsg, undecidableMsg :: SDoc +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 -XUndecidableInstances to permit this") +\end{code} +validDeivPred checks for OK 'deriving' context. See Note [Exotic +derived instance contexts] in TcSimplify. However the predicate is +here because it uses sizeTypes, fvTypes. + +\begin{code} +validDerivPred :: PredType -> Bool +validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs + where fvs = fvTypes tys +validDerivPred _ = False +\end{code} + + +%************************************************************************ +%* * + Checking type instance well-formedness and termination +%* * +%************************************************************************ + +\begin{code} +-- Check that a "type instance" is well-formed (which includes decidability +-- unless -XUndecidableInstances is given). +-- +checkValidTypeInst :: [Type] -> Type -> TcM () +checkValidTypeInst typats rhs + = do { -- left-hand side contains no type family applications + -- (vanilla synonyms are fine, though) + ; mapM_ checkTyFamFreeness typats + + -- the right-hand side is a tau type + ; checkValidMonoType rhs + + -- we have a decidable instance unless otherwise permitted + ; undecidable_ok <- xoptM Opt_UndecidableInstances + ; unless undecidable_ok $ + mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs)) + } + +-- Make sure that each type family instance is +-- (1) strictly smaller than the lhs, +-- (2) mentions no type variable more often than the lhs, and +-- (3) does not contain any further type family instances. +-- +checkFamInst :: [Type] -- lhs + -> [(TyCon, [Type])] -- type family instances + -> [Message] +checkFamInst lhsTys famInsts + = mapCatMaybes check famInsts + where + size = sizeTypes lhsTys + fvs = fvTypes lhsTys + check (tc, tys) + | not (all isTyFamFree tys) + = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg) + | not (null (fvTypes tys \\ fvs)) + = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg) + | size <= sizeTypes tys + = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg) + | otherwise + = Nothing + where + famInst = TyConApp tc tys + +-- Ensure that no type family instances occur in a type. +-- +checkTyFamFreeness :: Type -> TcM () +checkTyFamFreeness ty + = checkTc (isTyFamFree ty) $ + tyFamInstIllegalErr ty + +-- Check that a type does not contain any type family applications. +-- +isTyFamFree :: Type -> Bool +isTyFamFree = null . tyFamInsts + +-- Error messages + +tyFamInstIllegalErr :: Type -> SDoc +tyFamInstIllegalErr ty + = hang (ptext (sLit "Illegal type synonym family application in instance") <> + colon) 2 $ + ppr ty + +famInstUndecErr :: Type -> SDoc -> SDoc +famInstUndecErr ty msg + = sep [msg, + nest 2 (ptext (sLit "in the type family application:") <+> + pprType ty)] + +nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc +nestedMsg = ptext (sLit "Nested type family application") +nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head") +smallerAppMsg = ptext (sLit "Application is no smaller than the instance head") +\end{code} + + +%************************************************************************ +%* * +\subsection{Auxiliary functions} +%* * +%************************************************************************ + +\begin{code} -- Free variables of a type, retaining repetitions, and expanding synonyms 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 @@ -1174,7 +1636,6 @@ 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 @@ -1183,8 +1644,14 @@ sizeType (ForAllTy _ ty) = sizeType ty sizeTypes :: [Type] -> Int sizeTypes xs = sum (map sizeType xs) +-- Size of a predicate +-- +-- 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 +sizePred (IParam {}) = 0 +sizePred (EqPred {}) = 0 \end{code}