X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=49da076fbad4d60e27fb6d44b2a3b3d2ba0d5474;hb=ead9311db6e098b3affdc552269ea52bad8c12b5;hp=570f2f566fd13fb23652dec75cf49e55505c8c85;hpb=32836fa7556e79a6f1f98c4019f7daf0400ad4fd;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index 570f2f5..49da076 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -21,14 +21,15 @@ module TcMType ( -------------------------------- -- Instantiation tcInstTyVar, tcInstTyVars, tcInstType, - tcSkolTyVar, tcSkolTyVars, tcSkolType, + tcSkolType, tcSkolTyVars, tcInstSigType, + tcSkolSigType, tcSkolSigTyVars, -------------------------------- -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, instTypeErr, checkAmbiguity, - arityErr, isRigidType, + arityErr, -------------------------------- -- Zonking @@ -47,7 +48,7 @@ module TcMType ( -- friends: import HsSyn ( LHsType ) import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation - Kind, ThetaType + ThetaType ) import TcType ( TcType, TcThetaType, TcTauType, TcPredType, TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), @@ -55,7 +56,7 @@ import TcType ( TcType, TcThetaType, TcTauType, TcPredType, tcCmpPred, isClassPred, tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcSplitForAllTys, - tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy, + tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred, isImmutableTyVar, typeKind, isFlexi, isSkolemTyVar, mkAppTy, mkTyVarTy, mkTyVarTys, @@ -79,7 +80,8 @@ import FunDeps ( grow ) import Name ( Name, setNameUnique, mkSysTvName ) import VarSet import VarEnv -import CmdLineOpts ( dopt, DynFlag(..) ) +import DynFlags ( dopt, DynFlag(..) ) +import UniqSupply ( uniqsFromSupply ) import Util ( nOfThem, isSingleton, equalLength, notNull ) import ListSetOps ( removeDups ) import SrcLoc ( unLoc ) @@ -120,22 +122,6 @@ newTyFlexiVarTy 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 = do { uniq <- newUnique ; ref <- newMutVar Nothing @@ -175,59 +161,101 @@ tcInstTyVars tyvars -- they cannot possibly be captured by -- any existing for-alls. Hence zipTopTvSubst -tcInstTyVar tyvar +tcInstTyVar tyvar -- Freshen the Name of the tyvar = do { uniq <- newUnique - ; let name = setNameUnique (tyVarName tyvar) uniq - -- See Note [TyVarName] - ; newMetaTyVar name (tyVarKind tyvar) Flexi } + ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq) + (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 ty - = case tcSplitForAllTys ty of - ([], rho) -> -- There may be overloading despite no type variables; - -- (?x :: Int) => Int -> Int - let - (theta, tau) = tcSplitPhiTy rho - in - returnM ([], theta, tau) +tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty - (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 +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!! -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)) } +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) -tcSkolType info ty +-- 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 + +tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] +tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv 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 + ([], rho) -> let -- There may be overloading despite no type variables; + -- (?x :: Int) => Int -> Int (theta, tau) = tcSplitPhiTy rho in - returnM ([], theta, tau) + return ([], 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) + (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars + + ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars') + -- Either the tyvars are freshly made, by inst_tyvars, + -- or (in the call from tcSkolSigType) any nested foralls + -- have different binders. Either way, zipTopTvSubst is ok + + ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) + ; return (tyvars', theta, tau) } \end{code} @@ -266,8 +294,7 @@ We return Nothing iff the original box was unbound. \begin{code} data LookupTyVarResult -- The result of a lookupTcTyVar call - = FlexiTv - | RigidTv + = DoneTv TcTyVarDetails | IndirectTv Bool TcType -- True => This is a non-wobbly type refinement, -- gotten from GADT match unification @@ -277,34 +304,48 @@ data LookupTyVarResult -- The result of a lookupTcTyVar call 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 + = 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 RigidTv - } - MetaTv ref -> do { details <- readMutVar ref - ; case details of - Indirect ty -> return (IndirectTv False ty) - Flexi -> return FlexiTv + 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 tcTyVarDetails tyvar of - SkolemTv _ -> return RigidTv - MetaTv ref -> do { details <- readMutVar ref - ; case details of - Indirect ty -> return (IndirectTv False ty) - Flexi -> return FlexiTv - } + = 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) + } {- -- gaw 2004 We aren't shorting anything out anymore, at least for now @@ -394,13 +435,13 @@ zonkTcPredType (IParam n t) \begin{code} zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. --- It might be a meta TyVar, in which case we freeze it inot ano ordinary TyVar. +-- 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. +-- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv | isSkolemTyVar tv = return tv -- It might be a skolem type variable, @@ -523,7 +564,7 @@ zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variabl -> 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 + -- the quantified variable 'a' are TyVars not TcTyVars = returnM (TyVarTy tyvar) | otherwise @@ -532,9 +573,9 @@ zonkTyVar unbound_var_fn rflag tyvar -- 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 + 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 \end{code} @@ -761,9 +802,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_` @@ -831,7 +880,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