X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=09bbc26fbd3aeb721bbc7c946843b492072d6740;hb=8459e1aa09423e15bddccb97820bc1481c40a520;hp=df9bd1134468c93d4e39a4b68df45b2e3d86d34c;hpb=98688c6e8fd33f31c51218cf93cbf03fe3a5e73d;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index df9bd11..09bbc26 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -11,31 +11,33 @@ module TcMType ( -------------------------------- -- Creating new mutable type variables - newTyVar, newSigTyVar, - newTyVarTy, -- Kind -> TcM TcType - newTyVarTys, -- Int -> Kind -> TcM [TcType] - newKindVar, newKindVars, newBoxityVar, - putTcTyVar, getTcTyVar, - newMutTyVar, readMutTyVar, writeMutTyVar, + newFlexiTyVar, + newTyFlexiVarTy, -- Kind -> TcM TcType + newTyFlexiVarTys, -- Int -> Kind -> TcM [TcType] + newKindVar, newKindVars, + lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..), + newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar, -------------------------------- -- Instantiation tcInstTyVar, tcInstTyVars, tcInstType, + tcSkolTyVar, tcSkolTyVars, tcSkolType, -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt, + Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, instTypeErr, checkAmbiguity, - arityErr, + arityErr, isRigidType, -------------------------------- -- Zonking - zonkType, - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, + zonkType, zonkTcPredType, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, - zonkTcPredType, zonkTcTyVarToTyVar, - zonkTcKindToKind + zonkTcKindToKind, zonkTcKind, + + readKindVar, writeKindVar ) where @@ -43,41 +45,44 @@ module TcMType ( -- friends: +import HsSyn ( LHsType ) import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation Kind, ThetaType ) import TcType ( TcType, TcThetaType, TcTauType, TcPredType, - TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..), - tcEqType, tcCmpPred, isClassPred, + TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), + MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef, + tcCmpPred, isClassPred, tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcSplitForAllTys, - tcIsTyVarTy, tcSplitSigmaTy, - isUnLiftedType, isIPPred, isTyVarTy, - + tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy, + isUnLiftedType, isIPPred, isImmutableTyVar, + typeKind, isFlexi, isSkolemTyVar, mkAppTy, mkTyVarTy, mkTyVarTys, tyVarsOfPred, getClassPredTys_maybe, - - liftedTypeKind, defaultKind, superKind, - superBoxity, liftedBoxity, typeKind, tyVarsOfType, tyVarsOfTypes, - eqKind, isTypeKind, + pprPred, pprTheta, pprClassPred ) +import Kind ( Kind(..), KindVar(..), mkKindVar, isSubKind, + isLiftedTypeKind, isArgTypeKind, isOpenTypeKind, + liftedTypeKind, defaultKind ) -import Subst ( Subst, mkTopTyVarSubst, substTy ) +import Type ( TvSubst, zipTopTvSubst, substTy ) import Class ( Class, classArity, className ) import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon, tyConArity, tyConName ) -import Var ( TyVar, tyVarKind, tyVarName, isTyVar, - mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef ) +import Var ( TyVar, tyVarKind, tyVarName, + mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar ) -- others: import TcRnMonad -- TcType, amongst others import FunDeps ( grow ) -import PprType ( pprPred, pprTheta, pprClassPred ) -import Name ( Name, setNameUnique, mkSystemTvNameEncoded ) +import Name ( Name, setNameUnique, mkSysTvName ) import VarSet +import VarEnv import CmdLineOpts ( dopt, DynFlag(..) ) import Util ( nOfThem, isSingleton, equalLength, notNull ) import ListSetOps ( removeDups ) +import SrcLoc ( unLoc ) import Outputable \end{code} @@ -89,49 +94,55 @@ import Outputable %************************************************************************ \begin{code} -newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar -newMutTyVar name kind details - = do { ref <- newMutVar Nothing ; - return (mkMutTyVar name kind details ref) } - -readMutTyVar :: TyVar -> TcM (Maybe Type) -readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar) +newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar +newMetaTyVar name kind details + = do { ref <- newMutVar details ; + return (mkTcTyVar name kind (MetaTv ref)) } -writeMutTyVar :: TyVar -> Maybe Type -> TcM () -writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val +readMetaTyVar :: TyVar -> TcM MetaDetails +readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) + readMutVar (metaTvRef tyvar) -newTyVar :: Kind -> TcM TcTyVar -newTyVar kind - = newUnique `thenM` \ uniq -> - newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv +writeMetaTyVar :: TyVar -> MetaDetails -> TcM () +writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) + writeMutVar (metaTvRef tyvar) val -newSigTyVar :: Kind -> TcM TcTyVar -newSigTyVar kind +newFlexiTyVar :: Kind -> TcM TcTyVar +newFlexiTyVar kind = newUnique `thenM` \ uniq -> - newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("s")) kind SigTv + newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi -newTyVarTy :: Kind -> TcM TcType -newTyVarTy kind - = newTyVar kind `thenM` \ tc_tyvar -> +newTyFlexiVarTy :: Kind -> TcM TcType +newTyFlexiVarTy kind + = newFlexiTyVar kind `thenM` \ tc_tyvar -> returnM (TyVarTy tc_tyvar) -newTyVarTys :: Int -> Kind -> TcM [TcType] -newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind) +newTyFlexiVarTys :: Int -> Kind -> TcM [TcType] +newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind) + +isRigidType :: TcType -> TcM Bool +-- Check that the type is rigid, *taking the type refinement into account* +-- In other words if a rigid type variable tv is refined to a wobbly type, +-- the answer should be False +-- ToDo: can this happen? +isRigidType ty + = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty)) + ; return (and rigids) } + where + is_rigid tv = do { details <- lookupTcTyVar tv + ; case details of + RigidTv -> return True + IndirectTv True ty -> isRigidType ty + other -> return False + } newKindVar :: TcM TcKind -newKindVar - = newUnique `thenM` \ uniq -> - newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenM` \ kv -> - returnM (TyVarTy kv) +newKindVar = do { uniq <- newUnique + ; ref <- newMutVar Nothing + ; return (KindVar (mkKindVar uniq ref)) } newKindVars :: Int -> TcM [TcKind] newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) - -newBoxityVar :: TcM TcKind -- Really TcBoxity - = newUnique `thenM` \ uniq -> - newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) - superBoxity VanillaTv `thenM` \ kv -> - returnM (TyVarTy kv) \end{code} @@ -143,38 +154,38 @@ newBoxityVar :: TcM TcKind -- Really TcBoxity Instantiating a bunch of type variables -\begin{code} -tcInstTyVars :: TyVarDetails -> [TyVar] - -> TcM ([TcTyVar], [TcType], Subst) +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. -tcInstTyVars tv_details tyvars - = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars -> - let - tys = mkTyVarTys tc_tyvars - in - returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys) + +\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 mkTopTyVarSubst - -tcInstTyVar tv_details tyvar - = newUnique `thenM` \ uniq -> - let - name = setNameUnique (tyVarName tyvar) uniq - -- Note that we don't change the print-name - -- This won't confuse the type checker but there's a chance - -- that two different tyvars will print the same way - -- in an error message. -dppr-debug will show up the difference - -- Better watch out for this. If worst comes to worst, just - -- use mkSystemName. - in - newMutTyVar name (tyVarKind tyvar) tv_details + -- any existing for-alls. Hence zipTopTvSubst -tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) +tcInstTyVar tyvar + = do { uniq <- newUnique + ; let name = setNameUnique (tyVarName tyvar) uniq + -- See Note [TyVarName] + ; newMetaTyVar name (tyVarKind tyvar) Flexi } + +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 tv_details ty +tcInstType ty = case tcSplitForAllTys ty of ([], rho) -> -- There may be overloading despite no type variables; -- (?x :: Int) => Int -> Int @@ -183,8 +194,37 @@ tcInstType tv_details ty in returnM ([], theta, tau) - (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) -> + (tyvars, rho) -> tcInstTyVars tyvars `thenM` \ (tyvars', _, tenv) -> + let + (theta, tau) = tcSplitPhiTy (substTy tenv rho) + in + returnM (tyvars', theta, tau) + +--------------------------------------------- +-- Similar functions but for skolem constants + +tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] +tcSkolTyVars info tyvars = mappM (tcSkolTyVar info) tyvars + +tcSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar +tcSkolTyVar info tyvar + = do { uniq <- newUnique + ; let name = setNameUnique (tyVarName tyvar) uniq + -- See Note [TyVarName] + ; return (mkTcTyVar name (tyVarKind tyvar) + (SkolemTv info)) } + +tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) +tcSkolType info ty + = case tcSplitForAllTys ty of + ([], rho) -> let + (theta, tau) = tcSplitPhiTy rho + in + returnM ([], theta, tau) + + (tyvars, rho) -> tcSkolTyVars info tyvars `thenM` \ tyvars' -> let + tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars') (theta, tau) = tcSplitPhiTy (substTy tenv rho) in returnM (tyvars', theta, tau) @@ -198,30 +238,26 @@ tcInstType tv_details ty %************************************************************************ \begin{code} -putTcTyVar :: TcTyVar -> TcType -> TcM TcType -getTcTyVar :: TcTyVar -> TcM (Maybe TcType) -\end{code} - -Putting is easy: - -\begin{code} -putTcTyVar tyvar ty - | not (isMutTyVar tyvar) +putMetaTyVar :: TcTyVar -> TcType -> TcM () +#ifndef DEBUG +putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty) +#else +putMetaTyVar tyvar ty + | not (isMetaTyVar tyvar) = pprTrace "putTcTyVar" (ppr tyvar) $ - returnM ty + returnM () | otherwise - = ASSERT( isMutTyVar tyvar ) - writeMutTyVar tyvar (Just ty) `thenM_` - returnM ty + = 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) } + where + k1 = tyVarKind tyvar + k2 = typeKind ty +#endif \end{code} -Getting is more interesting. The easy thing to do is just to read, thus: - -\begin{verbatim} -getTcTyVar tyvar = readMutTyVar tyvar -\end{verbatim} - 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. @@ -229,36 +265,80 @@ any other type, then there might be bound TyVars embedded inside it. We return Nothing iff the original box was unbound. \begin{code} +data LookupTyVarResult -- The result of a lookupTcTyVar call + = FlexiTv + | RigidTv + | 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 + +lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult +-- This function is the ONLY PLACE that we consult the +-- type refinement carried by the monad +-- +-- The boolean returned with Indirect +lookupTcTyVar tyvar + = case tcTyVarDetails tyvar of + SkolemTv _ -> do { type_reft <- getTypeRefinement + ; case lookupVarEnv type_reft tyvar of + Just ty -> return (IndirectTv True ty) + Nothing -> return RigidTv + } + MetaTv ref -> do { details <- readMutVar ref + ; case details of + Indirect ty -> return (IndirectTv False ty) + Flexi -> return FlexiTv + } + +-- 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 tcTyVarDetails tyvar of + SkolemTv _ -> return RigidTv + MetaTv ref -> do { details <- readMutVar ref + ; case details of + Indirect ty -> return (IndirectTv False ty) + Flexi -> return FlexiTv + } + +{- +-- gaw 2004 We aren't shorting anything out anymore, at least for now getTcTyVar tyvar - | not (isMutTyVar tyvar) + | not (isTcTyVar tyvar) = pprTrace "getTcTyVar" (ppr tyvar) $ returnM (Just (mkTyVarTy tyvar)) | otherwise - = ASSERT2( isMutTyVar tyvar, ppr tyvar ) - readMutTyVar tyvar `thenM` \ maybe_ty -> + = ASSERT2( isTcTyVar tyvar, ppr tyvar ) + readMetaTyVar tyvar `thenM` \ maybe_ty -> case maybe_ty of Just ty -> short_out ty `thenM` \ ty' -> - writeMutTyVar tyvar (Just ty') `thenM_` + writeMetaTyVar tyvar (Just ty') `thenM_` returnM (Just ty') Nothing -> returnM Nothing short_out :: TcType -> TcM TcType short_out ty@(TyVarTy tyvar) - | not (isMutTyVar tyvar) + | not (isTcTyVar tyvar) = returnM ty | otherwise - = readMutTyVar tyvar `thenM` \ maybe_ty -> + = readMetaTyVar tyvar `thenM` \ maybe_ty -> case maybe_ty of Just ty' -> short_out ty' `thenM` \ ty' -> - writeMutTyVar tyvar (Just ty') `thenM_` + writeMetaTyVar tyvar (Just ty') `thenM_` returnM ty' other -> returnM ty short_out other_ty = returnM other_ty +-} \end{code} @@ -279,14 +359,14 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> returnM (tyVarsOfTypes tys) zonkTcTyVar :: TcTyVar -> TcM TcType -zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar +zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar \end{code} ----------------- Types \begin{code} zonkTcType :: TcType -> TcM TcType -zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty +zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty zonkTcTypes :: [TcType] -> TcM [TcType] zonkTcTypes tys = mappM zonkTcType tys @@ -312,48 +392,38 @@ zonkTcPredType (IParam n t) are used at the end of type checking \begin{code} -zonkTcKindToKind :: TcKind -> TcM Kind -zonkTcKindToKind tc_kind - = zonkType zonk_unbound_kind_var tc_kind - where - -- When zonking a kind, we want to - -- zonk a *kind* variable to (Type *) - -- zonk a *boxity* variable to * - zonk_unbound_kind_var kv - | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind - | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity - | otherwise = pprPanic "zonkKindEnv" (ppr kv) - --- zonkTcTyVarToTyVar is applied to the *binding* occurrence --- of a type variable, at the *end* of type checking. It changes --- the *mutable* type variable into an *immutable* one. --- --- It does this by making an immutable version of tv and binds tv to it. --- Now any bound occurences of the original type variable will get --- zonked to the immutable version. - -zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar -zonkTcTyVarToTyVar tv - = let - -- Make an immutable version, defaulting - -- the kind to lifted if necessary - immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv)) - immut_tv_ty = mkTyVarTy immut_tv - - zap tv = putTcTyVar tv immut_tv_ty - -- Bind the mutable version to the immutable one - in - -- If the type variable is mutable, then bind it to immut_tv_ty - -- so that all other occurrences of the tyvar will get zapped too - zonkTyVar zap tv `thenM` \ ty2 -> - - -- This warning shows up if the allegedly-unbound tyvar is - -- already bound to something. It can actually happen, and - -- in a harmless way (see [Silly Type Synonyms] below) so - -- it's only a warning - WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 ) - - returnM immut_tv +zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar +-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. +-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar. +-- When we do this, we also default the kind -- see notes with Kind.defaultKind +-- The meta tyvar is updated to point to the new regular TyVar. Now any +-- bound occurences of the original type variable will get zonked to +-- the immutable version. +-- +-- We leave skolem TyVars alone; they are imutable. +zonkQuantifiedTyVar tv + | isSkolemTyVar tv = return tv + -- It might be a skolem type variable, + -- for example from a user type signature + + | otherwise -- It's a meta-type-variable + = do { details <- readMetaTyVar tv + + -- Create the new, frozen, regular type variable + ; let final_kind = defaultKind (tyVarKind tv) + final_tv = mkTyVar (tyVarName tv) final_kind + + -- Bind the meta tyvar to the new tyvar + ; case details of + Indirect ty -> WARN( True, ppr tv $$ ppr ty ) + return () + -- [Sept 04] I don't think this should happen + -- See note [Silly Type Synonym] + + other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv)) + + -- Return the new tyvar + ; return final_tv } \end{code} [Silly Type Synonyms] @@ -381,10 +451,15 @@ Consider this: * So we get a dict binding for Num (C d a), which is zonked to give a = () + [Note Sept 04: now that we are zonking quantified type variables + on construction, the 'a' will be frozen as a regular tyvar on + quantification, so the floated dict will still have type (C d a). + Which renders this whole note moot; happily!] * Then the /\a abstraction has a zonked 'a' in it. -All very silly. I think its harmless to ignore the problem. +All very silly. I think its harmless to ignore the problem. We'll end up with +a /\a in the final result but all the occurrences of a will be zonked to () %************************************************************************ @@ -396,25 +471,21 @@ All very silly. I think its harmless to ignore the problem. %************************************************************************ \begin{code} --- zonkType is used for Kinds as well - -- For unbound, mutable tyvars, zonkType uses the function given to it -- For tyvars bound at a for-all, zonkType zonks them to an immutable -- type variable and zonks the kind too zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables -- see zonkTcType, and zonkTcTypeToType - -> TcType + -> Bool -- Should we consult the current type refinement? + -> TcType -> TcM Type -zonkType unbound_var_fn ty +zonkType unbound_var_fn rflag ty = go ty where go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' -> returnM (TyConApp tycon tys') - go (NewTcApp tycon tys) = mappM go tys `thenM` \ tys' -> - returnM (NewTcApp tycon tys') - go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' -> go ty2 `thenM` \ ty2' -> returnM (NoteTy (SynNote ty1') ty2') @@ -436,11 +507,11 @@ zonkType unbound_var_fn ty -- to pull the TyConApp to the top. -- The two interesting cases! - go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar + go (TyVarTy tyvar) = zonkTyVar unbound_var_fn rflag tyvar - go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' -> - go ty `thenM` \ ty' -> - returnM (ForAllTy tyvar' ty') + go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) + go ty `thenM` \ ty' -> + returnM (ForAllTy tyvar ty') go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' -> returnM (ClassP c tys') @@ -448,25 +519,66 @@ zonkType unbound_var_fn ty returnM (IParam n ty') zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable - -> TcTyVar -> TcM TcType -zonkTyVar unbound_var_fn tyvar - | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when - -- zonking a forall type, when the bound type variable - -- needn't be mutable - = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars - returnM (TyVarTy tyvar) + -> 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 + = returnM (TyVarTy tyvar) | otherwise - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Nothing -> unbound_var_fn tyvar -- Mutable and unbound - Just other_ty -> zonkType unbound_var_fn other_ty -- Bound + = 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 + FlexiTv -> unbound_var_fn tyvar -- Unbound flexi + RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary \end{code} %************************************************************************ %* * + Zonking kinds +%* * +%************************************************************************ + +\begin{code} +readKindVar :: KindVar -> TcM (Maybe TcKind) +writeKindVar :: KindVar -> TcKind -> TcM () +readKindVar (KVar _ ref) = readMutVar ref +writeKindVar (KVar _ ref) val = writeMutVar ref (Just val) + +------------- +zonkTcKind :: TcKind -> TcM TcKind +zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1 + ; k2' <- zonkTcKind k2 + ; returnM (FunKind k1' k2') } +zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv + ; case mb_kind of + Nothing -> returnM k + Just k -> zonkTcKind k } +zonkTcKind other_kind = returnM other_kind + +------------- +zonkTcKindToKind :: TcKind -> TcM Kind +zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1 + ; k2' <- zonkTcKindToKind k2 + ; returnM (FunKind k1' k2') } + +zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv + ; case mb_kind of + Nothing -> return liftedTypeKind + Just k -> zonkTcKindToKind k } + +zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to * +zonkTcKindToKind other_kind = returnM other_kind +\end{code} + +%************************************************************************ +%* * \subsection{Checking a user type} %* * %************************************************************************ @@ -526,16 +638,22 @@ data UserTypeCtxt -- With gla-exts that's right, but for H98 we should complain. -pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n) -pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature") -pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c) -pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c) -pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition") -pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature") -pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature") -pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n) -pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n) -pprUserTypeCtxt DefaultDeclCtxt = ptext SLIT("a `default' declaration") +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)] + +pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty) \end{code} \begin{code} @@ -562,17 +680,18 @@ checkValidType ctxt ty actual_kind = typeKind ty - actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind - kind_ok = case ctxt of TySynCtxt _ -> True -- Any kind will do - GenPatCtxt -> actual_kind_is_lifted - ForSigCtxt _ -> actual_kind_is_lifted - other -> isTypeKind actual_kind + ResSigCtxt -> isOpenTypeKind actual_kind + ExprSigCtxt -> isOpenTypeKind actual_kind + GenPatCtxt -> isLiftedTypeKind actual_kind + ForSigCtxt _ -> isLiftedTypeKind actual_kind + other -> isArgTypeKind actual_kind ubx_tup | not gla_exts = UT_NotOk | otherwise = case ctxt of TySynCtxt _ -> UT_Ok + ExprSigCtxt -> UT_Ok other -> UT_NotOk -- Unboxed tuples ok in function results, -- but for type synonyms we allow them even at @@ -642,9 +761,17 @@ 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 (PredTy sty) = getDOpts `thenM` \ dflags -> - check_source_ty dflags TypeCtxt sty +check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty) +check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty) + -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message + +-- Naked PredTys don't usually show up, but they can as a result of +-- {-# SPECIALISE instance Ord Char #-} +-- The Right Thing would be to fix the way that SPECIALISE instance pragmas +-- are handled, but the quick thing is just to permit PredTys here. +check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags -> + check_source_ty dflags TypeCtxt sty + check_tau_type rank ubx_tup (TyVarTy _) = returnM () check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty) = check_poly_type rank UT_NotOk arg_ty `thenM_` @@ -679,9 +806,6 @@ check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty) check_tau_type rank ubx_tup (NoteTy other_note ty) = check_tau_type rank ubx_tup ty -check_tau_type rank ubx_tup (NewTcApp tc tys) - = mappM_ check_arg_type tys - check_tau_type rank ubx_tup ty@(TyConApp tc tys) | isSynTyCon tc = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated @@ -694,8 +818,8 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) = 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 + -- Args are allowed to be unlifted, or + -- more unboxed tuples, so can't use check_arg_ty | otherwise = mappM_ check_arg_type tys @@ -715,7 +839,7 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) ubx_tup_msg = ubxArgTyErr ty ---------------------------------------- -forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty +forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind @@ -816,7 +940,7 @@ check_class_pred_tys dflags ctxt tys = case ctxt of InstHeadCtxt -> True -- We check for instance-head -- formation in checkValidInstHead - InstThetaCtxt -> undecidable_ok || all isTyVarTy tys + InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys other -> gla_exts || all tyvar_head tys where undecidable_ok = dopt Opt_AllowUndecidableInstances dflags