From: simonpj@microsoft.com Date: Tue, 3 Oct 2006 13:40:56 +0000 (+0000) Subject: Fix scoped type variables for expression type signatures X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=9da4639011348fb6c318e3cba4b08622f811d9c4 Fix scoped type variables for expression type signatures I had forgotten to bring scoped type variables into scope at an expression type signature, such as e :: forall s. where 's' should scope over the expression e. Like everything to do with scoped type variables, fixing this took an unreasonable amount of work. I'm sure there must be a better way to achitect this! I updated the user manual too. A test is tc213. It would be good to push this into 6.6.1 --- diff --git a/compiler/hsSyn/HsTypes.lhs b/compiler/hsSyn/HsTypes.lhs index 68d2d90..09cb073 100644 --- a/compiler/hsSyn/HsTypes.lhs +++ b/compiler/hsSyn/HsTypes.lhs @@ -14,7 +14,7 @@ module HsTypes ( LBangType, BangType, HsBang(..), getBangType, getBangStrictness, - mkExplicitHsForAllTy, mkImplicitHsForAllTy, + mkExplicitHsForAllTy, mkImplicitHsForAllTy, hsExplicitTvs, hsTyVarName, hsTyVarNames, replaceTyVarName, hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsLTyVarLocNames, splitHsInstDeclTy, splitHsFunType, @@ -190,6 +190,12 @@ mk_forall_ty exp tvs ty = HsForAllTy exp tvs (L noSrcSpan []) ty Implicit `plus` Implicit = Implicit exp1 `plus` exp2 = Explicit +hsExplicitTvs :: LHsType name -> [name] +-- The explicitly-given forall'd type variables of a HsType +hsExplicitTvs (L _ (HsForAllTy Explicit tvs _ _)) = hsLTyVarNames tvs +hsExplicitTvs other = [] + +--------------------- type LHsTyVarBndr name = Located (HsTyVarBndr name) data HsTyVarBndr name diff --git a/compiler/rename/RnBinds.lhs b/compiler/rename/RnBinds.lhs index f1ac430..ecd3b3d 100644 --- a/compiler/rename/RnBinds.lhs +++ b/compiler/rename/RnBinds.lhs @@ -379,8 +379,8 @@ rnBind sig_fn trim (L loc (PatBind { pat_lhs = pat, pat_rhs = grhss })) ; let bndrs = collectPatBinders pat' - ; (grhss', fvs) <- bindSigTyVarsFV (concatMap sig_fn bndrs) $ - rnGRHSs PatBindRhs grhss + ; (grhss', fvs) <- rnGRHSs PatBindRhs grhss + -- No scoped type variables for pattern bindings ; return (L loc (PatBind { pat_lhs = pat', pat_rhs = grhss', pat_rhs_ty = placeHolderType, bind_fvs = trim fvs }), @@ -392,6 +392,7 @@ rnBind sig_fn trim (L loc (FunBind { fun_id = name, fun_infix = inf, fun_matches ; let plain_name = unLoc new_name ; (matches', fvs) <- bindSigTyVarsFV (sig_fn plain_name) $ + -- bindSigTyVars tests for Opt_ScopedTyVars rnMatchGroup (FunRhs plain_name) matches ; checkPrecMatch inf plain_name matches' diff --git a/compiler/rename/RnExpr.lhs b/compiler/rename/RnExpr.lhs index 049123e..2df8e95 100644 --- a/compiler/rename/RnExpr.lhs +++ b/compiler/rename/RnExpr.lhs @@ -248,9 +248,10 @@ rnExpr (RecordUpd expr rbinds _ _) fvExpr `plusFV` fvRbinds) rnExpr (ExprWithTySig expr pty) - = rnLExpr expr `thenM` \ (expr', fvExpr) -> - rnHsTypeFVs doc pty `thenM` \ (pty', fvTy) -> - returnM (ExprWithTySig expr' pty', fvExpr `plusFV` fvTy) + = do { (pty', fvTy) <- rnHsTypeFVs doc pty + ; (expr', fvExpr) <- bindSigTyVarsFV (hsExplicitTvs pty') $ + rnLExpr expr + ; return (ExprWithTySig expr' pty', fvExpr `plusFV` fvTy) } where doc = text "In an expression type signature" diff --git a/compiler/rename/RnSource.lhs b/compiler/rename/RnSource.lhs index 8f4c1d3..6053098 100644 --- a/compiler/rename/RnSource.lhs +++ b/compiler/rename/RnSource.lhs @@ -15,9 +15,8 @@ module RnSource ( import {-# SOURCE #-} RnExpr( rnLExpr ) import HsSyn -import RdrName ( RdrName, isRdrDataCon, isRdrTyVar, rdrNameOcc, - elemLocalRdrEnv, globalRdrEnvElts, GlobalRdrElt(..), - isLocalGRE ) +import RdrName ( RdrName, isRdrDataCon, elemLocalRdrEnv, + globalRdrEnvElts, GlobalRdrElt(..), isLocalGRE ) import RdrHsSyn ( extractGenericPatTyVars, extractHsRhoRdrTyVars ) import RnHsSyn import RnTypes ( rnLHsType, rnLHsTypes, rnHsSigType, rnHsTypeFVs, rnContext ) diff --git a/compiler/rename/RnTypes.lhs b/compiler/rename/RnTypes.lhs index d04a0d9..0aa0b4e 100644 --- a/compiler/rename/RnTypes.lhs +++ b/compiler/rename/RnTypes.lhs @@ -534,7 +534,6 @@ rnPatsAndThen ctxt pats thing_inside bindLocatedLocalsFV doc_pat bndrs $ \ new_bndrs -> rnLPats pats `thenM` \ (pats', pat_fvs) -> thing_inside pats' `thenM` \ (res, res_fvs) -> - let unused_binders = filter (not . (`elemNameSet` res_fvs)) new_bndrs in diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs index 24f98d8..a3b17a6 100644 --- a/compiler/typecheck/TcBinds.lhs +++ b/compiler/typecheck/TcBinds.lhs @@ -19,10 +19,9 @@ import DynFlags ( dopt, DynFlags, DynFlag(Opt_MonomorphismRestriction, Opt_MonoPatBinds, Opt_GlasgowExts) ) import HsSyn ( HsExpr(..), HsBind(..), LHsBinds, LHsBind, Sig(..), HsLocalBinds(..), HsValBinds(..), HsIPBinds(..), - LSig, Match(..), IPBind(..), Prag(..), - HsType(..), LHsType, HsExplicitForAll(..), hsLTyVarNames, + LSig, Match(..), IPBind(..), Prag(..), LHsType, isVanillaLSig, sigName, placeHolderNames, isPragLSig, - LPat, GRHSs, MatchGroup(..), pprLHsBinds, mkHsWrap, + LPat, GRHSs, MatchGroup(..), pprLHsBinds, mkHsWrap, hsExplicitTvs, collectHsBindBinders, collectPatBinders, pprPatBind, isBangHsBind ) import TcHsSyn ( zonkId ) @@ -973,13 +972,12 @@ mkTcSigFun :: [LSig Name] -> TcSigFun -- Precondition: no duplicates mkTcSigFun sigs = lookupNameEnv env where - env = mkNameEnv [(name, scoped_tyvars hs_ty) - | L span (TypeSig (L _ name) (L _ hs_ty)) <- sigs] - scoped_tyvars (HsForAllTy Explicit tvs _ _) = hsLTyVarNames tvs - scoped_tyvars other = [] + env = mkNameEnv [(name, hsExplicitTvs lhs_ty) + | L span (TypeSig (L _ name) lhs_ty) <- sigs] -- The scoped names are the ones explicitly mentioned -- in the HsForAll. (There may be more in sigma_ty, because -- of nested type synonyms. See Note [Scoped] with TcSigInfo.) + -- See Note [Only scoped tyvars are in the TyVarEnv] --------------- data TcSigInfo @@ -998,6 +996,19 @@ data TcSigInfo sig_loc :: InstLoc -- The location of the signature } + +-- Note [Only scoped tyvars are in the TyVarEnv] +-- We are careful to keep only the *lexically scoped* type variables in +-- the type environment. Why? After all, the renamer has ensured +-- that only legal occurrences occur, so we could put all type variables +-- into the type env. +-- +-- But we want to check that two distinct lexically scoped type variables +-- do not map to the same internal type variable. So we need to know which +-- the lexically-scoped ones are... and at the moment we do that by putting +-- only the lexically scoped ones into the environment. + + -- Note [Scoped] -- There may be more instantiated type variables than scoped -- ones. For example: @@ -1010,7 +1021,7 @@ data TcSigInfo -- 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. +-- It's vital to instantiate a type signature with fresh variables. -- For example: -- type S = forall a. a->a -- f,g :: S @@ -1046,7 +1057,7 @@ tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo -- Instantiate the signature, with either skolems or meta-type variables -- depending on the use_skols boolean. This variable is set True -- when we are typechecking a single function binding; and False for --- pattern bindigs and a group of several function bindings. +-- pattern bindings and a group of several function bindings. -- Reason: in the latter cases, the "skolems" can be unified together, -- so they aren't properly rigid in the type-refinement sense. -- NB: unless we are doing H98, each function with a sig will be done diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index d9e25c3..e2f1d0c 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -21,7 +21,7 @@ import qualified DsMeta #endif import HsSyn ( HsExpr(..), LHsExpr, ArithSeqInfo(..), recBindFields, - HsMatchContext(..), HsRecordBinds, mkHsWrap, + HsMatchContext(..), HsRecordBinds, mkHsWrap, hsExplicitTvs, mkHsApp, mkLHsWrap ) import TcHsSyn ( hsLitType ) import TcRnMonad @@ -32,7 +32,7 @@ import BasicTypes ( Arity, isMarkedStrict ) import Inst ( newMethodFromName, newIPDict, instCall, newMethodWithGivenTy, instStupidTheta ) import TcBinds ( tcLocalBinds ) -import TcEnv ( tcLookup, tcLookupDataCon, tcLookupField ) +import TcEnv ( tcLookup, tcLookupDataCon, tcLookupField, tcExtendTyVarEnv2 ) import TcArrows ( tcProc ) import TcMatches ( tcMatchesCase, tcMatchLambda, tcDoStmts, tcBody, TcMatchCtxt(..) ) @@ -111,7 +111,7 @@ tcPolyExpr expr res_ty tcPolyExprNC expr res_ty | isSigmaTy res_ty - = do { (gen_fn, expr') <- tcGen res_ty emptyVarSet (tcPolyExprNC expr) + = do { (gen_fn, expr') <- tcGen res_ty emptyVarSet (\_ -> tcPolyExprNC expr) -- Note the recursive call to tcPolyExpr, because the -- type may have multiple layers of for-alls ; return (mkLHsWrap gen_fn expr') } @@ -208,9 +208,14 @@ tcExpr (HsLam match) res_ty tcExpr in_expr@(ExprWithTySig expr sig_ty) res_ty = do { sig_tc_ty <- tcHsSigType ExprSigCtxt sig_ty - ; expr' <- tcPolyExpr expr sig_tc_ty + + -- Remember to extend the lexical type-variable environment + ; (gen_fn, expr') <- tcGen sig_tc_ty emptyVarSet (\ skol_tvs res_ty -> + tcExtendTyVarEnv2 (hsExplicitTvs sig_ty `zip` mkTyVarTys skol_tvs) $ + tcPolyExprNC expr res_ty) + ; co_fn <- tcSubExp sig_tc_ty res_ty - ; return (mkHsWrap co_fn (ExprWithTySigOut expr' sig_ty)) } + ; return (mkHsWrap co_fn (ExprWithTySigOut (mkLHsWrap gen_fn expr') sig_ty)) } tcExpr (HsType ty) res_ty = failWithTc (text "Can't handle type argument:" <+> ppr ty) diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 39c3cbd..e9f0301 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -30,10 +30,10 @@ import HsSyn ( HsWrapper(..), idHsWrapper, isIdHsWrapper, (<.>), import TypeRep ( Type(..), PredType(..) ) import TcMType ( lookupTcTyVar, LookupTyVarResult(..), - tcInstSkolType, tcInstBoxyTyVar, newKindVar, newMetaTyVar, + tcInstBoxyTyVar, newKindVar, newMetaTyVar, newBoxyTyVar, newBoxyTyVarTys, readFilledBox, readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy, - tcInstSkolTyVars, tcInstTyVar, + tcInstSkolTyVars, tcInstTyVar, tcInstSkolType, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, readKindVar, writeKindVar ) import TcSimplify ( tcSimplifyCheck ) @@ -53,7 +53,7 @@ import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType, tidyOpenType, tidyOpenTyVar, tidyOpenTyVars, pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar, TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst, - substTy, substTheta, + substTy, substTheta, lookupTyVar, extendTvSubst ) import Type ( Kind, SimpleKind, KindVar, openTypeKind, liftedTypeKind, unliftedTypeKind, @@ -148,7 +148,7 @@ subFunTys error_herald n_pats res_ty thing_inside loop n args_so_far res_ty | isSigmaTy res_ty -- Do this before checking n==0, because we -- guarantee to return a BoxyRhoType, not a BoxySigmaType - = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ res_ty' -> + = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' -> loop n args_so_far res_ty' ; return (gen_fn <.> co_fn, res) } @@ -669,7 +669,7 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty | not exp_ib, -- SKOL does not apply if exp_ty is inside a box isSigmaTy exp_ty - = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty -> + = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty -> tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty ; return (gen_fn <.> co_fn) } where @@ -774,7 +774,7 @@ tcGen :: BoxySigmaType -- expected_ty -> TcTyVarSet -- Extra tyvars that the universally -- quantified tyvars of expected_ty -- must not be unified - -> (BoxyRhoType -> TcM result) -- spec_ty + -> ([TcTyVar] -> BoxyRhoType -> TcM result) -> TcM (HsWrapper, result) -- The expression has type: spec_ty -> expected_ty @@ -784,7 +784,7 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- mention the *instantiated* tyvar names, so that we get a -- good error message "Rigid variable 'a' is bound by (forall a. a->a)" -- Hence the tiresome but innocuous fixM - ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) -> + ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) -> do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty ; span <- getSrcSpanM ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span @@ -793,13 +793,12 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall #ifdef DEBUG ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs, text "expected_ty" <+> ppr expected_ty, - text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty, - text "free_tvs" <+> ppr free_tvs, - text "forall_tvs" <+> ppr forall_tvs]) + text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho', + text "free_tvs" <+> ppr free_tvs]) #endif -- Type-check the arg and unify with poly type - ; (result, lie) <- getLIE (thing_inside rho_ty) + ; (result, lie) <- getLIE (thing_inside tvs' rho') -- Check that the "forall_tvs" havn't been constrained -- The interesting bit here is that we must include the free variables @@ -812,16 +811,16 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- Conclusion: include the free vars of the expected_ty in the -- list of "free vars" for the signature check. - ; dicts <- newDictBndrsO (SigOrigin skol_info) theta - ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie + ; dicts <- newDictBndrsO (SigOrigin skol_info) theta' + ; inst_binds <- tcSimplifyCheck sig_msg tvs' dicts lie - ; checkSigTyVarsWrt free_tvs forall_tvs + ; checkSigTyVarsWrt free_tvs tvs' ; traceTc (text "tcGen:done") ; let -- The WpLet binds any Insts which came out of the simplification. dict_ids = map instToId dicts - co_fn = mkWpTyLams forall_tvs <.> mkWpLams dict_ids <.> WpLet inst_binds + co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds ; returnM (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 09fd3f5..f8ad5c1 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -3301,6 +3301,7 @@ changing the program. A lexically scoped type variable can be bound by: A declaration type signature () +An expression type signature () A pattern type signature () Class and instance declarations () @@ -3352,6 +3353,23 @@ quantification rules. + +Expression type signatures + +An expression type signature that has explicit +quantification (using forall) brings into scope the +explicitly-quantified +type variables, in the annotated expression. For example: + + f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool ) + +Here, the type signature forall a. ST s Bool brings the +type variable s into scope, in the annotated expression +(op >>= \(x :: STRef s Int) -> g x). + + + + Pattern type signatures