Commit 9da46390 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

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. <type>
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
parent 1bf36305
......@@ -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
......
......@@ -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'
......
......@@ -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"
......
......@@ -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 )
......
......@@ -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
......
......@@ -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
......
......@@ -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)
......
......@@ -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 )
......@@ -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
......
......@@ -3301,6 +3301,7 @@ changing the program.</para></listitem>
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>
......@@ -3352,6 +3353,23 @@ quantification rules.
</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>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment