X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=6345efb12a6bfa6bbfd132d9e5c096925a5166f7;hb=97fbb266f9a21eb66cf8ea1336b4324376a14567;hp=4a800a24a0ae947e5a00b2bb13acb5538917f95e;hpb=cdea99491a8dedfc53fc2e8c4c8fbaf209802b27;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index 4a800a2..6345efb 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -12,23 +12,28 @@ module TcMType ( -------------------------------- -- Creating new mutable type variables newFlexiTyVar, - newTyFlexiVarTy, -- Kind -> TcM TcType - newTyFlexiVarTys, -- Int -> Kind -> TcM [TcType] + newFlexiTyVarTy, -- Kind -> TcM TcType + newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newKindVar, newKindVars, - lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..), - newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar, + lookupTcTyVar, LookupTyVarResult(..), + newMetaTyVar, readMetaTyVar, writeMetaTyVar, + + -------------------------------- + -- Boxy type variables + newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, -------------------------------- -- Instantiation - tcInstTyVar, tcInstTyVars, tcInstType, - tcSkolType, tcSkolTyVars, tcInstSigType, + tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar, + tcInstSigTyVars, zonkSigTyVar, + tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt, + Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, - checkValidInstHead, instTypeErr, checkAmbiguity, + checkValidInstHead, checkValidInstance, checkAmbiguity, arityErr, -------------------------------- @@ -46,24 +51,26 @@ module TcMType ( -- friends: -import HsSyn ( LHsType ) import TypeRep ( Type(..), PredType(..), -- Friend; can see representation ThetaType ) import TcType ( TcType, TcThetaType, TcTauType, TcPredType, TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), - MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef, - tcCmpPred, isClassPred, + MetaDetails(..), SkolemInfo(..), BoxInfo(..), + BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType, + UserTypeCtxt(..), + isMetaTyVar, isSigTyVar, metaTvRef, + tcCmpPred, isClassPred, tcGetTyVar, tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, tcValidInstHeadTy, tcSplitForAllTys, tcIsTyVarTy, tcSplitSigmaTy, - isUnLiftedType, isIPPred, isImmutableTyVar, - typeKind, isFlexi, isSkolemTyVar, + isUnLiftedType, isIPPred, + typeKind, isSkolemTyVar, mkAppTy, mkTyVarTy, mkTyVarTys, tyVarsOfPred, getClassPredTys_maybe, tyVarsOfType, tyVarsOfTypes, tcView, pprPred, pprTheta, pprClassPred ) -import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar, isSubKind, +import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar, isLiftedTypeKind, isArgTypeKind, isOpenTypeKind, liftedTypeKind, defaultKind ) @@ -71,57 +78,66 @@ import Type ( TvSubst, zipTopTvSubst, substTy ) import Class ( Class, classArity, className ) import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon, tyConArity, tyConName ) -import Var ( TyVar, tyVarKind, tyVarName, - mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar ) +import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar, + mkTyVar, mkTcTyVar, tcTyVarDetails ) + + -- Assertions +#ifdef DEBUG +import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar ) +import Kind ( isSubKind ) +#endif -- others: import TcRnMonad -- TcType, amongst others -import FunDeps ( grow ) +import FunDeps ( grow, checkInstCoverage ) import Name ( Name, setNameUnique, mkSysTvName ) import VarSet -import VarEnv -import DynFlags ( dopt, DynFlag(..) ) -import UniqSupply ( uniqsFromSupply ) +import DynFlags ( dopt, DynFlag(..), DynFlags ) import Util ( nOfThem, isSingleton, notNull ) import ListSetOps ( removeDups ) -import SrcLoc ( unLoc ) import Outputable + +import Data.List ( (\\) ) \end{code} %************************************************************************ %* * -\subsection{New type variables} + Instantiation in general %* * %************************************************************************ \begin{code} -newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar -newMetaTyVar name kind details - = do { ref <- newMutVar details ; - return (mkTcTyVar name kind (MetaTv ref)) } +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) -readMetaTyVar :: TyVar -> TcM MetaDetails -readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) - readMutVar (metaTvRef tyvar) + (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars -writeMetaTyVar :: TyVar -> MetaDetails -> TcM () -writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) - writeMutVar (metaTvRef tyvar) val + ; 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 -newFlexiTyVar :: Kind -> TcM TcTyVar -newFlexiTyVar kind - = newUnique `thenM` \ uniq -> - newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi + ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) + ; return (tyvars', theta, tau) } +\end{code} -newTyFlexiVarTy :: Kind -> TcM TcType -newTyFlexiVarTy kind - = newFlexiTyVar kind `thenM` \ tc_tyvar -> - returnM (TyVarTy tc_tyvar) -newTyFlexiVarTys :: Int -> Kind -> TcM [TcType] -newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind) +%************************************************************************ +%* * + Kind variables +%* * +%************************************************************************ +\begin{code} newKindVar :: TcM TcKind newKindVar = do { uniq <- newUnique ; ref <- newMutVar Nothing @@ -134,158 +150,196 @@ newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) %************************************************************************ %* * -\subsection{Type instantiation} + SkolemTvs (immutable) %* * %************************************************************************ -Instantiating a bunch of type variables - -Note [TyVarName] -~~~~~~~~~~~~~~~~ -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. - - \begin{code} ------------------------ -tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst) -tcInstTyVars tyvars - = do { tc_tvs <- mappM 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 - -tcInstTyVar tyvar -- Freshen the Name of the tyvar - = do { uniq <- newUnique - ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq) - (tyVarKind tyvar) Flexi } +mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar +mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info) -tcInstType :: TcType -> 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 ty = tc_inst_type (mappM tcInstTyVar) ty - - ---------------------------------------------- -tcInstSigType :: Name -> [Name] -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) --- Instantiate a type with fresh SigSkol variables --- See Note [Signature skolems] in TcType. --- --- Tne new type variables have the sane Name as the original *iff* they are scoped. --- For scoped tyvars, we don't need a fresh unique, because the renamer has made them --- unique, and it's better not to do so because we extend the envt --- with them as scoped type variables, and we'd like to avoid spurious --- 's = s' bindings in error messages --- --- For non-scoped ones, we *must* instantiate fresh ones: --- --- type T = forall a. [a] -> [a] --- f :: T; --- f = g where { g :: T; g = } --- --- We must not use the same 'a' from the defn of T at both places!! - -tcInstSigType id_name scoped_names ty = tc_inst_type (tcInstSigTyVars id_name scoped_names) ty - -tcInstSigTyVars :: Name -> [Name] -> [TyVar] -> TcM [TcTyVar] -tcInstSigTyVars id_name scoped_names tyvars - = mapM new_tv tyvars - where - new_tv tv - = do { let name = tyVarName tv - ; ref <- newMutVar Flexi - ; name' <- if name `elem` scoped_names - then return name - else do { uniq <- newUnique; return (setNameUnique name uniq) } - ; return (mkTcTyVar name' (tyVarKind tv) - (SigSkolTv id_name ref)) } - - ---------------------------------------------- -tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) --- Instantiate a type with fresh skolem constants -tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty - -tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] -tcSkolTyVars info tyvars - = do { us <- newUniqueSupply - ; return (zipWith skol_tv tyvars (uniqsFromSupply us)) } - where - skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq) - (tyVarKind tv) (SkolemTv info) - -- See Note [TyVarName] - - ---------------------------------------------- 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 - = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty +tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] -tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info) +-- Make skolem constants, but do *not* give them new names, as above +tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info | tv <- tyvars ] ------------------------ -tc_inst_type :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables - -> TcType -- Type to instantiate - -> TcM ([TcTyVar], TcThetaType, TcType) -- Result -tc_inst_type 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 +tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) +-- Instantiate a type with fresh skolem constants +tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty - ; 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 +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) } - ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) - ; return (tyvars', theta, tau) } +tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] +tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars \end{code} %************************************************************************ %* * -\subsection{Putting and getting mutable type variables} + MetaTvs (meta type variables; mutable) %* * %************************************************************************ \begin{code} -putMetaTyVar :: TcTyVar -> TcType -> TcM () +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 -putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty) +writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty) #else -putMetaTyVar tyvar ty +writeMetaTyVar tyvar ty | not (isMetaTyVar tyvar) - = pprTrace "putTcTyVar" (ppr tyvar) $ + = pprTrace "writeMetaTyVar" (ppr tyvar) $ returnM () | otherwise = ASSERT( isMetaTyVar tyvar ) ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) ) - do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } ) - ; writeMetaTyVar tyvar (Indirect ty) } + 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} + +%************************************************************************ +%* * + 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} + + +%************************************************************************ +%* * + MetaTvs: SigTvs +%* * +%************************************************************************ + +\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 + = 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} + + +%************************************************************************ +%* * + 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 + +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} + + +%************************************************************************ +%* * +\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 any other type, then there might be bound TyVars embedded inside it. @@ -294,58 +348,19 @@ We return Nothing iff the original box was unbound. \begin{code} data LookupTyVarResult -- The result of a lookupTcTyVar call - = DoneTv TcTyVarDetails -- Unrefined SkolemTv or virgin MetaTv/SigSkolTv - | IndirectTv Bool TcType - -- True => This is a non-wobbly type refinement, - -- gotten from GADT match unification - -- False => This is a wobbly type, - -- gotten from inference unification + = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv + | IndirectTv TcType lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult --- This function is the ONLY PLACE that we consult the --- type refinement carried by the monad lookupTcTyVar tyvar - = let - details = tcTyVarDetails tyvar - in - case details of - MetaTv ref -> lookup_wobbly details ref - - SkolemTv _ -> do { type_reft <- getTypeRefinement - ; case lookupVarEnv type_reft tyvar of - Just ty -> return (IndirectTv True ty) - Nothing -> return (DoneTv details) - } - - -- For SigSkolTvs try the refinement, and, failing that - -- see if it's been unified to anything. It's a combination - -- of SkolemTv and MetaTv - SigSkolTv _ ref -> do { type_reft <- getTypeRefinement - ; case lookupVarEnv type_reft tyvar of - Just ty -> return (IndirectTv True ty) - Nothing -> lookup_wobbly details ref - } - --- Look up a meta type variable, conditionally consulting --- the current type refinement -condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult -condLookupTcTyVar use_refinement tyvar - | use_refinement = lookupTcTyVar tyvar - | otherwise = case details of - MetaTv ref -> lookup_wobbly details ref - SkolemTv _ -> return (DoneTv details) - SigSkolTv _ ref -> lookup_wobbly details ref - where - details = tcTyVarDetails tyvar - -lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult -lookup_wobbly details ref - = do { meta_details <- readMutVar ref - ; case meta_details of - Indirect ty -> return (IndirectTv False ty) - Flexi -> return (DoneTv details) - } + 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 @@ -400,14 +415,15 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> returnM (tyVarsOfTypes tys) zonkTcTyVar :: TcTyVar -> TcM TcType -zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar +zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar ) + zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar \end{code} ----------------- Types \begin{code} zonkTcType :: TcType -> TcM TcType -zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty +zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty zonkTcTypes :: [TcType] -> TcM [TcType] zonkTcTypes tys = mappM zonkTcType tys @@ -461,7 +477,7 @@ zonkQuantifiedTyVar tv -- [Sept 04] I don't think this should happen -- See note [Silly Type Synonym] - other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv)) + Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv) -- Return the new tyvar ; return final_tv } @@ -486,7 +502,7 @@ 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 @@ -518,33 +534,34 @@ a /\a in the final result but all the occurrences of a will be zonked to () zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables -- see zonkTcType, and zonkTcTypeToType - -> Bool -- Should we consult the current type refinement? -> TcType -> TcM Type -zonkType unbound_var_fn rflag ty +zonkType unbound_var_fn ty = go ty where - go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' -> - returnM (TyConApp tycon tys') - - go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations - - 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 (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 rflag tyvar + 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' -> @@ -555,23 +572,17 @@ zonkType unbound_var_fn rflag ty go_pred (IParam n ty) = go ty `thenM` \ ty' -> returnM (IParam n ty') -zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable - -> Bool -- Consult the type refinement? - -> TcTyVar -> TcM TcType -zonkTyVar unbound_var_fn rflag tyvar - | not (isTcTyVar tyvar) -- When zonking (forall a. ...a...), the occurrences of - -- the quantified variable 'a' are TyVars not TcTyVars +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 - = condLookupTcTyVar rflag tyvar `thenM` \ details -> - case details of - -- If b is true, the variable was refined, and therefore it is okay - -- to continue refining inside. Otherwise it was wobbly and we should - -- not refine further inside. - IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid - DoneTv (MetaTv _) -> unbound_var_fn tyvar -- Unbound meta type variable - DoneTv other -> return (TyVarTy tyvar) -- Rigid, no zonking necessary + | 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} @@ -649,54 +660,6 @@ This might not necessarily show up in kind checking. \begin{code} -data UserTypeCtxt - = FunSigCtxt Name -- Function type signature - -- Also used for types in SPECIALISE pragmas - | 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 - | DefaultDeclCtxt -- Types in a default declaration - | SpecInstCtxt -- SPECIALISE instance pragma - --- 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. - - -pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc -pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt - -pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty] -pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)] -pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty] -pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma, - nest 2 (ptext SLIT(", namely") <+> ppr ty)] -pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)] -pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)] -pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)] -pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty] -pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty] -pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)] -pprUserTypeCtxt ty SpecInstCtxt = sep [ptext SLIT("In a SPECIALISE instance pragma:"), nest 2 (ppr ty)] - -pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty) -\end{code} - -\begin{code} checkValidType :: UserTypeCtxt -> Type -> TcM () -- Checks that the type is valid for the given context checkValidType ctxt ty @@ -707,7 +670,8 @@ checkValidType ctxt ty | 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 @@ -777,7 +741,7 @@ check_poly_type rank ubx_tup ty 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 -- @@ -794,7 +758,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 `thenM_` + = check_poly_type Arbitrary UT_NotOk ty `thenM_` checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) ---------------------------------------- @@ -816,7 +780,7 @@ check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags -> 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 `thenM_` - check_tau_type rank UT_Ok res_ty + 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 @@ -826,10 +790,7 @@ check_tau_type rank ubx_tup (NoteTy other_note 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 - do { -- It's OK to have an *over-applied* type synonym + = do { -- It's OK to have an *over-applied* type synonym -- data Tree a b = ... -- type Foo a = Tree [a] -- f :: Foo a b -> ... @@ -907,14 +868,11 @@ data SourceTyCtxt -- f :: N a -> N a | InstThetaCtxt -- Context of an instance decl -- instance => C [a] where ... - | InstHeadCtxt -- Head of an instance decl - -- instance ... => Eq 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} @@ -929,10 +887,6 @@ check_valid_theta ctxt [] check_valid_theta ctxt theta = getDOpts `thenM` \ dflags -> warnTc (notNull dups) (dupPredWarn dups) `thenM_` - -- Actually, in instance decls and type signatures, - -- duplicate constraints are eliminated by TcHsType.hoistForAllTys, - -- so this error can only fire for the context of a class or - -- data type decl. mappM_ (check_source_ty dflags ctxt) theta where (_,dups) = removeDups tcCmpPred theta @@ -952,11 +906,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys) arity = classArity cls n_tys = length tys arity_err = arityErr "Class" class_name arity n_tys - - how_to_allow = case ctxt of - InstHeadCtxt -> empty -- Should not happen - InstThetaCtxt -> parens undecidableMsg - other -> parens (ptext SLIT("Use -fglasgow-exts to permit this")) + how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this")) check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- Implicit parameters only allows in type @@ -975,12 +925,11 @@ 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 tcIsTyVarTy tys - other -> gla_exts || all tyvar_head tys + InstThetaCtxt -> gla_exts || all tcIsTyVarTy tys + -- Further checks on head and theta in + -- checkInstTermination + other -> gla_exts || all tyvar_head tys where - undecidable_ok = dopt Opt_AllowUndecidableInstances dflags gla_exts = dopt Opt_GlasgowExts dflags ------------------------- @@ -1074,7 +1023,8 @@ checkThetaCtxt ctxt theta ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty -predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred +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) arityErr kind name n m @@ -1123,7 +1073,7 @@ checkValidInstHead ty -- Should be a source type check_inst_head dflags clas tys -- If GlasgowExts then check at least one isn't a type variable | dopt Opt_GlasgowExts dflags - = check_tyvars dflags clas tys + = returnM () -- WITH HASKELL 98, MUST HAVE C (T a b c) | isSingleton tys, @@ -1138,18 +1088,6 @@ check_inst_head dflags clas 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") - -check_tyvars dflags clas tys - -- Check that at least one isn't a type variable - -- unless -fallow-undecideable-instances - | dopt Opt_AllowUndecidableInstances dflags = returnM () - | not (all tcIsTyVarTy tys) = returnM () - | 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} @@ -1157,3 +1095,102 @@ instTypeErr pp_ty msg = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, nest 4 msg] \end{code} + + +%************************************************************************ +%* * +\subsection{Checking instance for termination} +%* * +%************************************************************************ + + +\begin{code} +checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () +checkValidInstance tyvars theta clas inst_tys + = do { dflags <- getDOpts + + ; checkValidTheta InstThetaCtxt theta + ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) + + -- Check that instance inference will termainate + -- For Haskell 98, checkValidTheta has already done that + ; checkInstTermination dflags theta inst_tys + + -- The Coverage Condition + ; checkTc (dopt Opt_AllowUndecideableInstances dflags || + checkInstCoverage clas inst_tys) + (instTypeErr (pprClassPred clas inst_tys) msg) + } + where + msg = parens (ptext SLIT("the instance types do not agree with the functional dependencies of the class")) +\end{code} + +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 :: DynFlags -> ThetaType -> [TcType] -> TcM () +checkInstTermination 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") + +-- 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 +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}