LBangType, BangType, HsBang(..),
getBangType, getBangStrictness,
- mkExplicitHsForAllTy, mkImplicitHsForAllTy,
+ mkExplicitHsForAllTy, mkImplicitHsForAllTy, hsExplicitTvs,
hsTyVarName, hsTyVarNames, replaceTyVarName,
hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsLTyVarLocNames,
splitHsInstDeclTy, splitHsFunType,
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
; 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 }),
; 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'
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"
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 )
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
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 )
-- 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
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:
-- 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
-- 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
#endif
import HsSyn ( HsExpr(..), LHsExpr, ArithSeqInfo(..), recBindFields,
- HsMatchContext(..), HsRecordBinds, mkHsWrap,
+ HsMatchContext(..), HsRecordBinds, mkHsWrap, hsExplicitTvs,
mkHsApp, mkLHsWrap )
import TcHsSyn ( hsLitType )
import TcRnMonad
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(..) )
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') }
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)
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 )
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,
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) }
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
-> 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
-- 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
#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
-- 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
A <emphasis>lexically scoped type variable</emphasis> can be bound by:
<itemizedlist>
<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
+<listitem><para>An expression type signature (<xref linkend="exp-type-sigs"/>)</para></listitem>
<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
<listitem><para>Class and instance declarations (<xref linkend="cls-inst-scoped-tyvars"/>)</para></listitem>
</itemizedlist>
</para>
</sect3>
+<sect3 id="exp-type-sigs">
+<title>Expression type signatures</title>
+
+<para>An expression type signature that has <emphasis>explicit</emphasis>
+quantification (using <literal>forall</literal>) brings into scope the
+explicitly-quantified
+type variables, in the annotated expression. For example:
+<programlisting>
+ f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
+</programlisting>
+Here, the type signature <literal>forall a. ST s Bool</literal> brings the
+type variable <literal>s</literal> into scope, in the annotated expression
+<literal>(op >>= \(x :: STRef s Int) -> g x)</literal>.
+</para>
+
+</sect3>
+
<sect3 id="pattern-type-sigs">
<title>Pattern type signatures</title>
<para>
projects / ghc-hetmet.git / commitdiff