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

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

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'

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"
 

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 )

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

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

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)

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

docs/users_guide/glasgow_exts.xml

@@ -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>