X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcHsType.lhs;h=968ccfb960b1fe48531e1a560b2c43c8acf8c6d9;hb=ac10f8408520a30e8437496d320b8b86afda2e8f;hp=ebb97b308195fb3920079c9eb3a8f875d44b5eba;hpb=dd313897eb9a14bcc7b81f97e4f2292c30039efd;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcHsType.lhs b/ghc/compiler/typecheck/TcHsType.lhs index ebb97b3..968ccfb 100644 --- a/ghc/compiler/typecheck/TcHsType.lhs +++ b/ghc/compiler/typecheck/TcHsType.lhs @@ -14,38 +14,40 @@ module TcHsType ( -- Typechecking kinded types tcHsKindedContext, tcHsKindedType, tcHsBangType, - tcTyVarBndrs, dsHsType, tcLHsConSig, tcDataKindSig, + tcTyVarBndrs, dsHsType, tcLHsConResTy, + tcDataKindSig, - tcHsPatSigType, tcAddLetBoundTyVars, - - TcSigInfo(..), TcSigFun, lookupSig + -- Pattern type signatures + tcHsPatSigType, tcPatSig ) where #include "HsVersions.h" -import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, HsBang, - LHsContext, HsPred(..), LHsPred, LHsBinds, - getBangStrictness, collectSigTysFromHsBinds ) +import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, + LHsContext, HsPred(..), LHsPred, HsExplicitForAll(..) ) import RnHsSyn ( extractHsTyVars ) import TcRnMonad -import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnv, +import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnvTvs, tcLookup, tcLookupClass, tcLookupTyCon, - TyThing(..), getInLocalScope, wrongThingErr + TyThing(..), getInLocalScope, getScopedTyVarBinds, + wrongThingErr ) -import TcMType ( newKindVar, newMetaTyVar, zonkTcKindToKind, - checkValidType, UserTypeCtxt(..), pprHsSigCtxt +import TcMType ( newKindVar, + zonkTcKindToKind, + tcInstBoxyTyVar, readFilledBox, + checkValidType ) -import TcUnify ( unifyFunKind, checkExpectedKind ) +import TcUnify ( boxyUnify, unifyFunKind, checkExpectedKind ) import TcIface ( checkWiredInTyCon ) -import TcType ( Type, PredType(..), ThetaType, - MetaDetails(Flexi), hoistForAllTys, - TcType, TcTyVar, TcKind, TcThetaType, TcTauType, - mkFunTy, mkSigmaTy, mkPredTy, mkGenTyConApp, +import TcType ( Type, PredType(..), ThetaType, BoxySigmaType, + TcType, TcKind, isRigidTy, + UserTypeCtxt(..), pprUserTypeCtxt, + substTyWith, mkTyVarTys, tcEqType, + tcIsTyVarTy, mkFunTy, mkSigmaTy, mkPredTy, mkTyConApp, mkAppTys, typeKind ) import Kind ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, openTypeKind, argTypeKind, splitKindFunTys ) -import Id ( idName ) -import Var ( TyVar, mkTyVar ) +import Var ( TyVar, mkTyVar, tyVarName ) import TyCon ( TyCon, tyConKind ) import Class ( Class, classTyCon ) import Name ( Name, mkInternalName ) @@ -53,9 +55,8 @@ import OccName ( mkOccName, tvName ) import NameSet import PrelNames ( genUnitTyConName ) import TysWiredIn ( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon ) -import Bag ( bagToList ) import BasicTypes ( Boxity(..) ) -import SrcLoc ( Located(..), unLoc, noLoc, srcSpanStart ) +import SrcLoc ( Located(..), unLoc, noLoc, getLoc, srcSpanStart ) import UniqSupply ( uniqsFromSupply ) import Outputable \end{code} @@ -195,9 +196,7 @@ tcHsKindedType :: LHsType Name -> TcM Type -- This is used in type and class decls, where kinding is -- done in advance, and validity checking is done later -- [Validity checking done later because of knot-tying issues.] -tcHsKindedType hs_ty - = do { ty <- dsHsType hs_ty - ; return (hoistForAllTys ty) } +tcHsKindedType hs_ty = dsHsType hs_ty tcHsBangType :: LHsType Name -> TcM Type -- Permit a bang, but discard it @@ -238,13 +237,20 @@ kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name) -- with OpenTypeKind, because it gives better error messages kcCheckHsType (L span ty) exp_kind = setSrcSpan span $ - do { (ty', act_kind) <- addErrCtxt (typeCtxt ty) $ - kc_hs_type ty + do { (ty', act_kind) <- add_ctxt ty (kc_hs_type ty) -- Add the context round the inner check only -- because checkExpectedKind already mentions -- 'ty' by name in any error message + ; checkExpectedKind ty act_kind exp_kind ; return (L span ty') } + where + -- Wrap a context around only if we want to + -- show that contexts. Omit invisble ones + -- and ones user's won't grok (HsPred p). + add_ctxt (HsPredTy p) thing = thing + add_ctxt (HsForAllTy Implicit tvs (L _ []) ty) thing = thing + add_ctxt other_ty thing = addErrCtxt (typeCtxt ty) thing \end{code} Here comes the main function @@ -511,7 +517,7 @@ ds_var_app name arg_tys = tcLookup name `thenM` \ thing -> case thing of ATyVar _ ty -> returnM (mkAppTys ty arg_tys) - AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys) + AGlobal (ATyCon tc) -> returnM (mkTyConApp tc arg_tys) other -> wrongThingErr "type" thing name \end{code} @@ -536,36 +542,12 @@ dsHsPred (HsIParam name ty) GADT constructor signatures \begin{code} -tcLHsConSig :: LHsType Name - -> TcM ([TcTyVar], TcThetaType, - [HsBang], [TcType], - TyCon, [TcType]) --- Take apart the type signature for a data constructor --- The difference is that there can be bangs at the top of --- the argument types, and kind-checking is the right place to check -tcLHsConSig sig@(L span (HsForAllTy exp tv_names ctxt ty)) - = setSrcSpan span $ - addErrCtxt (gadtSigCtxt sig) $ - tcTyVarBndrs tv_names $ \ tyvars -> - do { theta <- mappM dsHsLPred (unLoc ctxt) - ; (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty - ; return (tyvars, theta, bangs, arg_tys, tc, res_tys) } -tcLHsConSig ty - = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty - ; return ([], [], bangs, arg_tys, tc, res_tys) } - --------- -tc_con_sig_tau (L _ (HsFunTy arg ty)) - = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty - ; arg_ty <- tcHsBangType arg - ; return (getBangStrictness arg : bangs, - arg_ty : arg_tys, tc, res_tys) } - -tc_con_sig_tau ty - = do { (tc, res_tys) <- tc_con_res ty [] - ; return ([], [], tc, res_tys) } - --------- +tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType]) +tcLHsConResTy ty@(L span _) + = setSrcSpan span $ + addErrCtxt (gadtResCtxt ty) $ + tc_con_res ty [] + tc_con_res (L _ (HsAppTy fun res_ty)) res_tys = do { res_ty' <- dsHsType res_ty ; tc_con_res fun (res_ty' : res_tys) } @@ -579,11 +561,11 @@ tc_con_res ty@(L _ (HsTyVar name)) res_tys tc_con_res ty _ = failWithTc (badGadtDecl ty) -gadtSigCtxt ty - = hang (ptext SLIT("In the signature of a data constructor:")) +gadtResCtxt ty + = hang (ptext SLIT("In the result type of a data constructor:")) 2 (ppr ty) badGadtDecl ty - = hang (ptext SLIT("Malformed constructor signature:")) + = hang (ptext SLIT("Malformed constructor result type:")) 2 (ppr ty) typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty) @@ -603,8 +585,7 @@ kcHsTyVars :: [LHsTyVarBndr Name] -> TcM r kcHsTyVars tvs thing_inside = mappM (wrapLocM kcHsTyVar) tvs `thenM` \ bndrs -> - tcExtendKindEnv [(n,k) | L _ (KindedTyVar n k) <- bndrs] - (thing_inside bndrs) + tcExtendKindEnvTvs bndrs (thing_inside bndrs) kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name) -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it @@ -622,10 +603,10 @@ tcTyVarBndrs bndrs thing_inside = mapM (zonk . unLoc) bndrs `thenM` \ tyvars -> tcExtendTyVarEnv tyvars (thing_inside tyvars) where - zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' -> - returnM (mkTyVar name kind') + zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind + ; return (mkTyVar name kind') } zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $ - returnM (mkTyVar name liftedTypeKind) + return (mkTyVar name liftedTypeKind) ----------------------------------- tcDataKindSig :: Maybe Kind -> TcM [TyVar] @@ -699,139 +680,137 @@ Historical note: it with expected_ty afterwards \begin{code} -tcPatSigBndrs :: LHsType Name - -> TcM ([TcTyVar], -- Brought into scope - LHsType Name) -- Kinded, but not yet desugared +tcHsPatSigType :: UserTypeCtxt + -> LHsType Name -- The type signature + -> TcM ([TyVar], -- Newly in-scope type variables + Type) -- The signature +-- Used for type-checking type signatures in +-- (a) patterns e.g f (x::Int) = e +-- (b) result signatures e.g. g x :: Int = e +-- (c) RULE forall bndrs e.g. forall (x::Int). f x = x -tcPatSigBndrs hs_ty - = do { in_scope <- getInLocalScope - ; span <- getSrcSpanM - ; let sig_tvs = [ L span (UserTyVar n) +tcHsPatSigType ctxt hs_ty + = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $ + do { -- Find the type variables that are mentioned in the type + -- but not already in scope. These are the ones that + -- should be bound by the pattern signature + in_scope <- getInLocalScope + ; let span = getLoc hs_ty + sig_tvs = [ L span (UserTyVar n) | n <- nameSetToList (extractHsTyVars hs_ty), not (in_scope n) ] - -- The tyvars we want are the free type variables of - -- the type that are not already in scope - -- Behave like kcHsType on a ForAll type - -- i.e. make kinded tyvars with mutable kinds, - -- and kind-check the enclosed types + -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty), + -- except that we want to keep the tvs separate ; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do { kinded_ty <- kcTypeType hs_ty ; return (kinded_tvs, kinded_ty) } - - -- Zonk the mutable kinds and bring the tyvars into scope - -- Just like the call to tcTyVarBndrs in ds_type (HsForAllTy case), - -- except that it brings *meta* tyvars into scope, not regular ones - -- - -- [Out of date, but perhaps should be resurrected] - -- Furthermore, the tyvars are PatSigTvs, which means that we get better - -- error messages when type variables escape: - -- Inferred type is less polymorphic than expected - -- Quantified type variable `t' escapes - -- It is mentioned in the environment: - -- t is bound by the pattern type signature at tcfail103.hs:6 - ; tyvars <- mapM (zonk . unLoc) kinded_tvs - ; return (tyvars, kinded_ty) } + ; tcTyVarBndrs kinded_tvs $ \ tyvars -> do + { sig_ty <- dsHsType kinded_ty + ; checkValidType ctxt sig_ty + ; return (tyvars, sig_ty) + } } + +tcPatSig :: UserTypeCtxt + -> LHsType Name + -> BoxySigmaType + -> TcM (TcType, -- The type to use for "inside" the signature + [(Name,TcType)]) -- The new bit of type environment, binding + -- the scoped type variables +tcPatSig ctxt sig res_ty + = do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig + + ; if null sig_tvs then do { + -- The type signature binds no type variables, + -- and hence is rigid, so use it to zap the res_ty + boxyUnify sig_ty res_ty + ; return (sig_ty, []) + + } else do { + -- Type signature binds at least one scoped type variable + + -- A pattern binding cannot bind scoped type variables + -- The renamer fails with a name-out-of-scope error + -- if a pattern binding tries to bind a type variable, + -- So we just have an ASSERT here + ; let in_pat_bind = case ctxt of + BindPatSigCtxt -> True + other -> False + ; ASSERT( not in_pat_bind || null sig_tvs ) return () + + -- Check that pat_ty is rigid + ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs) + + -- Now match the pattern signature against res_ty + -- For convenience, and uniform-looking error messages + -- we do the matching by allocating meta type variables, + -- unifying, and reading out the results. + -- This is a strictly local operation. + ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs + ; boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) res_ty + ; sig_tv_tys <- mapM readFilledBox box_tvs + + -- Check that each is bound to a distinct type variable, + -- and one that is not already in scope + ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys + ; binds_in_scope <- getScopedTyVarBinds + ; check binds_in_scope tv_binds + + -- Phew! + ; return (res_ty, tv_binds) + } } where - zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' -> - newMetaTyVar name kind' Flexi - -- Scoped type variables are bound to a *type*, hence Flexi - zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $ - returnM (mkTyVar name liftedTypeKind) + check in_scope [] = return () + check in_scope ((n,ty):rest) = do { check_one in_scope n ty + ; check ((n,ty):in_scope) rest } -tcHsPatSigType :: UserTypeCtxt - -> LHsType Name -- The type signature - -> TcM ([TcTyVar], -- Newly in-scope type variables - TcType) -- The signature - -tcHsPatSigType ctxt hs_ty - = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $ - do { (tyvars, kinded_ty) <- tcPatSigBndrs hs_ty - - -- Complete processing of the type, and check its validity - ; tcExtendTyVarEnv tyvars $ do - { sig_ty <- tcHsKindedType kinded_ty - ; checkValidType ctxt sig_ty - ; return (tyvars, sig_ty) } - } + check_one in_scope n ty + = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty) + -- Must bind to a type variable -tcAddLetBoundTyVars :: LHsBinds Name -> TcM a -> TcM a --- Turgid funciton, used for type variables bound by the patterns of a let binding + ; checkTc (null dups) (dupInScope n (head dups) ty) + -- Must not bind to the same type variable + -- as some other in-scope type variable -tcAddLetBoundTyVars binds thing_inside - = go (collectSigTysFromHsBinds (bagToList binds)) thing_inside - where - go [] thing_inside = thing_inside - go (hs_ty:hs_tys) thing_inside - = do { (tyvars, _kinded_ty) <- tcPatSigBndrs hs_ty - ; tcExtendTyVarEnv tyvars (go hs_tys thing_inside) } + ; return () } + where + dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty] \end{code} %************************************************************************ %* * -\subsection{Signatures} + Scoped type variables %* * %************************************************************************ -@tcSigs@ checks the signatures for validity, and returns a list of -{\em freshly-instantiated} signatures. That is, the types are already -split up, and have fresh type variables installed. All non-type-signature -"RenamedSigs" are ignored. - -The @TcSigInfo@ contains @TcTypes@ because they are unified with -the variable's type, and after that checked to see whether they've -been instantiated. - \begin{code} -data TcSigInfo - = TcSigInfo { - sig_id :: TcId, -- *Polymorphic* binder for this value... - - sig_scoped :: [Name], -- Names for any scoped type variables - -- Invariant: correspond 1-1 with an initial - -- segment of sig_tvs (see Note [Scoped]) - - sig_tvs :: [TcTyVar], -- Instantiated type variables - -- See Note [Instantiate sig] - - sig_theta :: TcThetaType, -- Instantiated theta - sig_tau :: TcTauType, -- Instantiated tau - sig_loc :: InstLoc -- The location of the signature - } - --- Note [Scoped] --- There may be more instantiated type variables than scoped --- ones. For example: --- type T a = forall b. b -> (a,b) --- f :: forall c. T c --- Here, the signature for f will have one scoped type variable, c, --- but two instantiated type variables, c' and b'. --- --- We assume that the scoped ones are at the *front* of sig_tvs, --- and remember the names from the original HsForAllTy in sig_scoped - --- Note [Instantiate sig] --- It's vital to instantiate a type signature with fresh variable. --- For example: --- type S = forall a. a->a --- f,g :: S --- f = ... --- g = ... --- Here, we must use distinct type variables when checking f,g's right hand sides. --- (Instantiation is only necessary because of type synonyms. Otherwise, --- it's all cool; each signature has distinct type variables from the renamer.) - -type TcSigFun = Name -> Maybe TcSigInfo - -instance Outputable TcSigInfo where - ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau}) - = ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau - -lookupSig :: [TcSigInfo] -> TcSigFun -- Search for a particular signature -lookupSig [] name = Nothing -lookupSig (sig : sigs) name - | name == idName (sig_id sig) = Just sig - | otherwise = lookupSig sigs name +pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc +pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon, + nest 2 (pp_sig ctxt) ] + where + pp_sig (FunSigCtxt n) = pp_n_colon n + pp_sig (ConArgCtxt n) = pp_n_colon n + pp_sig (ForSigCtxt n) = pp_n_colon n + pp_sig (RuleSigCtxt n) = pp_n_colon n + pp_sig other = ppr (unLoc hs_ty) + + pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty) + + +wobblyPatSig sig_tvs + = hang (ptext SLIT("A pattern type signature cannot bind scoped type variables") + <+> pprQuotedList sig_tvs) + 2 (ptext SLIT("unless the pattern has a rigid type context")) + +scopedNonVar n ty + = vcat [sep [ptext SLIT("The scoped type variable") <+> quotes (ppr n), + nest 2 (ptext SLIT("is bound to the type") <+> quotes (ppr ty))], + nest 2 (ptext SLIT("You can only bind scoped type variables to type variables"))] + +dupInScope n n' ty + = hang (ptext SLIT("The scoped type variables") <+> quotes (ppr n) <+> ptext SLIT("and") <+> quotes (ppr n')) + 2 (vcat [ptext SLIT("are bound to the same type (variable)"), + ptext SLIT("Distinct scoped type variables must be distinct")]) \end{code}