X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=6423a830a91e792f94e653f88d00be880c319641;hp=f3485a26cfe1b619761f2034feebb2634e3f73c9;hb=HEAD;hpb=98bbd9b2bf02496f9fc21f1f443f315292a6ce5f diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index f3485a2..6423a83 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -18,6 +18,7 @@ module TcMType ( newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newKindVar, newKindVars, + mkTcTyVarName, newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, isFilledMetaTyVar, isFlexiMetaTyVar, @@ -25,18 +26,17 @@ module TcMType ( -------------------------------- -- Creating new evidence variables newEvVar, newCoVar, newEvVars, - newWantedCoVar, writeWantedCoVar, readWantedCoVar, - newIP, newDict, newSelfDict, isSelfDict, + newIP, newDict, newSilentGiven, isSilentEvVar, newWantedEvVar, newWantedEvVars, newTcEvBinds, addTcEvBind, -------------------------------- -- Instantiation - tcInstTyVar, tcInstTyVars, tcInstSigTyVars, - tcInstType, tcInstSigType, instMetaTyVar, - tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, + tcInstTyVars, tcInstSigTyVars, + tcInstType, + tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType, + tcSkolDFunType, tcSuperSkolTyVars, -------------------------------- -- Checking type validity @@ -50,15 +50,17 @@ module TcMType ( -------------------------------- -- Zonking zonkType, mkZonkTcTyVar, zonkTcPredType, - zonkTcTypeCarefully, + zonkTcTypeCarefully, skolemiseUnboundMetaTyVar, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcThetaType, zonkTcKindToKind, zonkTcKind, - zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar, + zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar, + zonkWC, zonkWantedEvVars, zonkTcTypeAndSubst, tcGetGlobalTyVars, + readKindVar, writeKindVar ) where @@ -68,7 +70,6 @@ module TcMType ( import TypeRep import TcType import Type -import Coercion import Class import TyCon import Var @@ -89,10 +90,11 @@ import BasicTypes import SrcLoc import Outputable import FastString +import Unique( Unique ) import Bag import Control.Monad -import Data.List ( (\\) ) +import Data.List ( (\\) ) \end{code} @@ -124,27 +126,13 @@ newEvVars :: TcThetaType -> TcM [EvVar] newEvVars theta = mapM newEvVar theta newWantedEvVar :: TcPredType -> TcM EvVar -newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2 +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 -newWantedCoVar :: TcType -> TcType -> TcM CoVar -newWantedCoVar ty1 ty2 = newCoVar ty1 ty2 - --- We used to create a mutable co-var -{- --- A wanted coercion variable is a MetaTyVar --- that can be filled in with its binding - = do { uniq <- newUnique - ; ref <- newMutVar Flexi - ; let name = mkSysTvName uniq (fsLit "c") - kind = mkPredTy (EqPred ty1 ty2) - ; return (mkTcTyVar name kind (MetaTv TauTv ref)) } --} - -------------- newEvVar :: TcPredType -> TcM EvVar -- Creates new *rigid* variables for predicates @@ -154,7 +142,7 @@ newEvVar (IParam ip ty) = newIP ip ty newCoVar :: TcType -> TcType -> TcM CoVar newCoVar ty1 ty2 - = do { name <- newName (mkTyVarOccFS (fsLit "co")) + = do { name <- newName (mkVarOccFS (fsLit "co")) ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) } newIP :: IPName Name -> TcType -> TcM IpId @@ -174,20 +162,23 @@ newName occ ; return (mkInternalName uniq occ loc) } ----------------- -newSelfDict :: Class -> [TcType] -> TcM DictId --- Make a dictionary for "self". It behaves just like a normal DictId --- except that it responds True to isSelfDict +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 -newSelfDict cls tys +newSilentGiven (ClassP cls tys) = do { uniq <- newUnique - ; let name = mkSystemName uniq selfDictOcc + ; 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 -selfDictOcc :: OccName -selfDictOcc = mkVarOcc "self" - -isSelfDict :: EvVar -> Bool -isSelfDict v = isSystemName (Var.varName v) +isSilentEvVar :: EvVar -> Bool +isSilentEvVar v = isSystemName (Var.varName v) -- Notice that all *other* evidence variables get Internal Names \end{code} @@ -215,68 +206,66 @@ tcInstType inst_tyvars 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 + -- or any nested foralls have different binders. + -- Either way, zipTopTvSubst is ok ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) ; return (tyvars', theta, tau) } -mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar -mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info) - -tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType) +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 +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 :: SkolemInfo -> TyVar -> TcM TcTyVar +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 (otehrwise) -tcInstSkolTyVar skol_info tyvar +-- or from the monad (otherwise) +tcInstSkolTyVar overlappable tyvar = do { uniq <- newUnique - ; loc <- case skol_info of - SigSkol {} -> return (getSrcSpan old_name) - _ -> getSrcSpanM + ; loc <- getSrcSpanM ; let new_name = mkInternalName uniq occ loc - ; return (mkSkolTyVar new_name kind skol_info) } + ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) } where old_name = tyVarName tyvar occ = nameOccName old_name kind = tyVarKind tyvar -tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] --- Get the location from the monad -tcInstSkolTyVars info tyvars - = mapM (tcInstSkolTyVar info) tyvars +tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar] +tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars -tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) +tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar] +tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars + +tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type with fresh skolem constants -- Binding location comes from the monad -tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty - -tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType) --- Instantiate with skolems or meta SigTvs; depending on use_skols --- Always take location info from the supplied tyvars -tcInstSigType use_skols name ty - | use_skols - = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty - | otherwise - = tcInstType tcInstSigTyVars ty +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 (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv) - -- ToDo: the "function binding site is bogus +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} @@ -292,33 +281,22 @@ newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar newMetaTyVar meta_info kind = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi - ; let name = mkSysTvName uniq fs - fs = case meta_info of - TauTv -> fsLit "t" - TcsTv -> fsLit "u" - SigTv _ -> fsLit "a" + ; 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)) } -instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar --- Make a new meta tyvar whose Name and Kind --- come from an existing TyVar -instMetaTyVar meta_info tyvar - = do { uniq <- newMetaUnique - ; ref <- newMutVar Flexi - ; let name = setNameUnique (tyVarName tyvar) uniq - kind = tyVarKind tyvar - ; 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 @@ -357,9 +335,6 @@ writeMetaTyVar tyvar 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; @@ -378,8 +353,8 @@ writeMetaTyVarRef tyvar ref ty | otherwise = do { meta_details <- readMutVar ref; - ; WARN( not (isFlexi meta_details), - hang (text "Double update of meta tyvar") + ; ASSERT2( isFlexi meta_details, + hang (text "Double update of meta tyvar") 2 (ppr tyvar $$ ppr meta_details) ) traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) @@ -408,10 +383,6 @@ newFlexiTyVarTy kind = do newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] newFlexiTyVarTys n kind = mapM 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 @@ -421,6 +392,16 @@ tcInstTyVars tyvars -- 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} @@ -475,7 +456,6 @@ 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 @@ -488,10 +468,11 @@ zonkTcTypeCarefully ty | otherwise = ASSERT( isTcTyVar tv ) case tcTyVarDetails tv of - SkolemTv {} -> return (TyVarTy tv) - FlatSkol ty -> zonkType (zonk_tv env_tvs) ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of + 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 } @@ -504,11 +485,12 @@ zonkTcTyVar :: TcTyVar -> TcM TcType zonkTcTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) case tcTyVarDetails tv of - SkolemTv {} -> return (TyVarTy tv) - FlatSkol ty -> zonkTcType ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of - Flexi -> return (TyVarTy tv) + 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 @@ -517,10 +499,11 @@ zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty where zonk_tv tv = case tcTyVarDetails tv of - SkolemTv {} -> return (TyVarTy tv) - FlatSkol ty -> zonkType zonk_tv ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of + 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 @@ -548,8 +531,6 @@ zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar --- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. --- -- The quantified type variables often include meta type variables -- we want to freeze them into ordinary type variables, and -- default their kind (e.g. from OpenTypeKind to TypeKind) @@ -560,59 +541,101 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- -- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv - | ASSERT2( isTcTyVar tv, ppr tv ) - isSkolemTyVar tv - = do { kind <- zonkTcType (tyVarKind tv) - ; return $ setTyVarKind tv kind - } + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + 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, skolem type variable - -- We zonk to a skolem, not to a regular TcVar - -- See Note [Zonking to Skolem] - ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land + 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_name = setNameUnique (tyVarName tv) uniq - final_tv = mkSkolTyVar final_name final_kind UnkSkol - - -- Bind the meta tyvar to the new tyvar - ; case details of - Indirect ty -> WARN( True, ppr tv $$ ppr ty ) - return () - -- [Sept 04] I don't think this should happen - -- See note [Silly Type Synonym] - - Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv) - - -- Return the new tyvar + final_name = mkInternalName uniq (getOccName tv) span + final_tv = mkTcTyVar final_name final_kind details + ; writeMetaTyVar tv (mkTyVarTy final_tv) ; return final_tv } \end{code} \begin{code} zonkImplication :: Implication -> TcM Implication zonkImplication implic@(Implic { ic_given = given - , ic_wanted = wanted }) - = do { given' <- mapM zonkEvVar given - ; wanted' <- mapBagM zonkWanted wanted - ; return (implic { ic_given = given', ic_wanted = wanted' }) } + , 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') } -zonkWanted :: WantedConstraint -> TcM WantedConstraint -zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') } -zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') } +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 (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) } +zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) } + +zonkFlavor :: CtFlavor -> TcM CtFlavor +zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) } +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: @@ -693,10 +716,8 @@ simplifier knows how to deal with. -- For tyvars bound at a for-all, zonkType zonks them to an immutable -- type variable and zonks the kind too -zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables - -- see zonkTcType, and zonkTcTypeToType - -> TcType - -> TcM Type +zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars + -> TcType -> TcM Type zonkType zonk_tc_tyvar ty = go ty where @@ -719,13 +740,12 @@ zonkType zonk_tc_tyvar ty -- The two interesting cases! go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar - | otherwise = liftM TyVarTy $ - zonkTyVar zonk_tc_tyvar tyvar + | otherwise = return (TyVarTy tyvar) -- Ordinary (non Tc) tyvars occur inside quantified types go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do ty' <- go ty - tyvar' <- zonkTyVar zonk_tc_tyvar tyvar + tyvar' <- return tyvar return (ForAllTy tyvar' ty') go_pred (ClassP c tys) = do tys' <- mapM go tys @@ -736,27 +756,18 @@ zonkType zonk_tc_tyvar ty ty2' <- go ty2 return (EqPred ty1' ty2') -mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var +mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var -> TcTyVar -> TcM TcType mkZonkTcTyVar unbound_var_fn tyvar = ASSERT( isTcTyVar tyvar ) case tcTyVarDetails tyvar of SkolemTv {} -> return (TyVarTy tyvar) + 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} @@ -852,7 +863,9 @@ checkValidType ctxt ty = do ForSigCtxt _ -> gen_rank 1 SpecInstCtxt -> gen_rank 1 - ThBrackCtxt -> gen_rank 1 + ThBrackCtxt -> gen_rank 1 + GenSigCtxt -> panic "checkValidType" + -- Can't happen; GenSigCtxt not used for *user* sigs actual_kind = typeKind ty @@ -1125,7 +1138,7 @@ check_valid_theta ctxt theta = do warnTc (notNull dups) (dupPredWarn dups) mapM_ (check_pred_ty dflags ctxt) theta where - (_,dups) = removeDups tcCmpPred theta + (_,dups) = removeDups cmpPred theta ------------------------- check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM () @@ -1146,10 +1159,13 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this")) -check_pred_ty dflags _ pred@(EqPred ty1 ty2) +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 (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags) + (eqPredTyErr pred) + ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True) + (eqSuperClassErr pred) -- Check the form of the argument types ; checkValidMonoType ty1 @@ -1245,7 +1261,7 @@ checkAmbiguity forall_tyvars theta tau_tyvars ambigErr :: PredType -> SDoc ambigErr pred - = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred), + = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy 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} @@ -1306,15 +1322,20 @@ checkThetaCtxt ctxt theta = 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 sty = ptext (sLit "Illegal constraint") <+> pprPred sty -eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty - $$ - parens (ptext (sLit "Use -XTypeFamilies to permit this")) +badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred +eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred + $$ + parens (ptext (sLit "Use -XGADTs or -XTypeFamilies to permit this")) predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"), - nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)] + nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)] dupPredWarn :: [[PredType]] -> SDoc -dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) +dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups) arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc arityErr kind name n m @@ -1343,34 +1364,20 @@ 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 -> +checkValidInstHead :: Class -> [Type] -> TcM () +checkValidInstHead clas tys + = do { dflags <- getDOpts - case getClassPredTys_maybe pred of { - Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ; - Just (clas,tys) -> do - - dflags <- getDOpts - check_inst_head dflags clas tys - return (clas, tys) - }} - -check_inst_head :: DynFlags -> Class -> [Type] -> TcM () -check_inst_head dflags clas tys - = do { -- If GlasgowExts then check at least one isn't a type variable + -- If GlasgowExts then check at least one isn't a type variable ; checkTc (xopt Opt_TypeSynonymInstances dflags || all tcInstHeadTyNotSynonym tys) - (instTypeErr (pprClassPred clas tys) head_type_synonym_msg) + (instTypeErr pp_pred head_type_synonym_msg) ; checkTc (xopt Opt_FlexibleInstances dflags || all tcInstHeadTyAppAllTyVars tys) - (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg) + (instTypeErr pp_pred head_type_args_tyvars_msg) ; checkTc (xopt Opt_MultiParamTypeClasses dflags || isSingleton tys) - (instTypeErr (pprClassPred clas tys) head_one_type_msg) + (instTypeErr pp_pred head_one_type_msg) -- May not contain type family applications ; mapM_ checkTyFamFreeness tys @@ -1383,6 +1390,7 @@ check_inst_head dflags clas tys } 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." $$ @@ -1390,7 +1398,7 @@ check_inst_head dflags clas tys head_type_args_tyvars_msg = parens (vcat [ text "All instance types must be of the form (T a1 ... an)", - text "where a1 ... an are type *variables*,", + 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."]) @@ -1412,35 +1420,30 @@ instTypeErr pp_ty msg %************************************************************************ \begin{code} -checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type - -> TcM (Class, [TcType]) -checkValidInstance hs_type tyvars theta tau +checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType + -> Class -> [TcType] -> TcM () +checkValidInstance hs_type tyvars theta clas inst_tys = setSrcSpan (getLoc hs_type) $ - do { (clas, inst_tys) <- setSrcSpan head_loc $ - checkValidInstHead tau - - ; undecidable_ok <- xoptM Opt_UndecidableInstances - - ; checkValidTheta InstThetaCtxt theta + 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 this will already have been done by checkValidTheta, -- but as we may be using other extensions we need to check. - ; unless undecidable_ok $ + ; 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) - - ; return (clas, inst_tys) - } + } where msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"), undecidableMsg]) - -- The location of the "head" of the instance + -- The location of the "head" of the instance head_loc = case hs_type of L _ (HsForAllTy _ _ _ (L loc _)) -> loc L loc _ -> loc @@ -1480,7 +1483,7 @@ checkInstTermination tys theta 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:") <+> pprPredTy pred)] nomoreMsg, smallerMsg, undecidableMsg :: SDoc nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")