[project @ 2001-05-21 09:19:14 by simonpj]

-------------------------------
	Improve pattern type-signatures
	-------------------------------

The main effect of this commit is to implement the idea (originally
Marcin's suggestion) that type variables in pattern type signatures
are simply names for types; they don't have to name a type that is
itself a type variable.

For example

	f :: Int -> Int
	f (x::a) = let  y::a
			y = x
		   in x+y

is fine.  Here 'a' is a name for the type 'Int', and does not have
to be universally quantified.


I also took the opportunity to modularise the implementation of
pattern type-checking, mainly in TcMatches.  As a result pattern type
signatures should work in do-notation (which they didn't before).

ToDo: update documentation

8 files changed, 178 insertions, 157 deletions

diff --git a/ghc/compiler/typecheck/TcEnv.lhs b/ghc/compiler/typecheck/TcEnv.lhs
index 809abce82d..1f83155b6e 100644
--- a/ghc/compiler/typecheck/TcEnv.lhs
+++ b/ghc/compiler/typecheck/TcEnv.lhs
@@ -19,7 +19,7 @@ module TcEnv(
 	tcLookupGlobal_maybe, tcLookupGlobal, tcLookupSyntaxId, tcLookupSyntaxName,
 
 	-- Local environment
-	tcExtendKindEnv,  tcLookupLocalIds,
+	tcExtendKindEnv,  tcLookupLocalIds, tcInLocalScope,
 	tcExtendTyVarEnv, tcExtendTyVarEnvForMeths, 
 	tcExtendLocalValEnv, tcLookup, tcLookup_maybe, tcLookupId,
 
@@ -59,7 +59,7 @@ import Name		( Name, OccName, NamedThing(..),
 			  nameOccName, getSrcLoc, mkLocalName, isLocalName,
 			  nameIsLocalOrFrom
 			)
-import NameEnv		( NameEnv, lookupNameEnv, nameEnvElts, 
+import NameEnv		( NameEnv, lookupNameEnv, nameEnvElts, elemNameEnv,
 			  extendNameEnvList, emptyNameEnv, plusNameEnv )
 import OccName		( mkDFunOcc, occNameString )
 import HscTypes		( DFunId, 
@@ -170,6 +170,9 @@ tcEnvTcIds   env = [id | ATcId  id <- nameEnvElts (tcLEnv env)]
 
 getTcGEnv (TcEnv { tcGEnv = genv }) = genv
 
+tcInLocalScope :: TcEnv -> Name -> Bool
+tcInLocalScope env v = v `elemNameEnv` (tcLEnv env)
+
 -- This data type is used to help tie the knot
 -- when type checking type and class declarations
 data TyThingDetails = SynTyDetails Type
diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs
index 006983ddf4..9be3c54aab 100644
--- a/ghc/compiler/typecheck/TcExpr.lhs
+++ b/ghc/compiler/typecheck/TcExpr.lhs
@@ -595,7 +595,7 @@ tcMonoExpr in_expr@(ArithSeqIn seq@(FromThenTo expr1 expr2 expr3)) res_ty
 
 \begin{code}
 tcMonoExpr in_expr@(ExprWithTySig expr poly_ty) res_ty
- = tcSetErrCtxt (exprSigCtxt in_expr)	$
+ = tcAddErrCtxt (exprSigCtxt in_expr)	$
    tcHsSigType  poly_ty		`thenTc` \ sig_tc_ty ->
 
    if not (isSigmaTy sig_tc_ty) then
diff --git a/ghc/compiler/typecheck/TcInstDcls.lhs b/ghc/compiler/typecheck/TcInstDcls.lhs
index 9b53a04dd2..ad60526c73 100644
--- a/ghc/compiler/typecheck/TcInstDcls.lhs
+++ b/ghc/compiler/typecheck/TcInstDcls.lhs
@@ -12,7 +12,7 @@ module TcInstDcls ( tcInstDecls1, tcInstDecls2, tcAddDeclCtxt ) where
 import CmdLineOpts	( DynFlag(..), dopt )
 
 import HsSyn		( HsDecl(..), InstDecl(..), TyClDecl(..), HsType(..),
-			  MonoBinds(..), HsExpr(..),  HsLit(..), Sig(..), 
+			  MonoBinds(..), HsExpr(..),  HsLit(..), Sig(..), HsTyVarBndr(..),
 			  andMonoBindList, collectMonoBinders, isClassDecl, toHsType
 			)
 import RnHsSyn		( RenamedHsBinds, RenamedInstDecl, RenamedHsDecl, 
@@ -36,7 +36,7 @@ import TcEnv		( TcEnv, tcExtendGlobalValEnv,
 			  isLocalThing,
 			)
 import InstEnv		( InstEnv, extendInstEnv )
-import TcMonoType	( tcTyVars, tcHsSigType, kcHsSigType, checkSigTyVars )
+import TcMonoType	( tcHsTyVars, tcHsSigType, kcHsSigType, checkSigTyVars )
 import TcSimplify	( tcSimplifyCheck )
 import HscTypes		( HomeSymbolTable, DFunId,
 			  ModDetails(..), PackageInstEnv, PersistentRenamerState
@@ -395,9 +395,10 @@ mkGenericInstance clas loc (hs_ty, binds)
   -- For example:	instance (C a, C b) => C (a+b) where { binds }
 
   = 	-- Extract the universally quantified type variables
-    tcTyVars (nameSetToList (extractHsTyVars hs_ty)) 
-	     (kcHsSigType hs_ty)		`thenTc` \ tyvars ->
-    tcExtendTyVarEnv tyvars					$
+    let
+	sig_tvs = map UserTyVar (nameSetToList (extractHsTyVars hs_ty))
+    in
+    tcHsTyVars sig_tvs (kcHsSigType hs_ty)	$ \ tyvars ->
 
 	-- Type-check the instance type, and check its form
     tcHsSigType hs_ty				`thenTc` \ inst_ty ->
diff --git a/ghc/compiler/typecheck/TcMatches.lhs b/ghc/compiler/typecheck/TcMatches.lhs
index 36aed1bb19..a972fb765a 100644
--- a/ghc/compiler/typecheck/TcMatches.lhs
+++ b/ghc/compiler/typecheck/TcMatches.lhs
@@ -17,13 +17,15 @@ import HsSyn		( HsBinds(..), Match(..), GRHSs(..), GRHS(..),
 			  pprMatch, getMatchLoc, pprMatchContext, isDoExpr,
 			  mkMonoBind, nullMonoBinds, collectSigTysFromPats
 			)
-import RnHsSyn		( RenamedMatch, RenamedGRHSs, RenamedStmt )
-import TcHsSyn		( TcMatch, TcGRHSs, TcStmt, TcDictBinds )
+import RnHsSyn		( RenamedMatch, RenamedGRHSs, RenamedStmt, RenamedPat, RenamedHsType,
+			  extractHsTyVars )
+import TcHsSyn		( TcMatch, TcGRHSs, TcStmt, TcDictBinds, TypecheckedPat )
 
 import TcMonad
-import TcMonoType	( kcHsSigType, tcTyVars, checkSigTyVars, tcHsSigType, sigPatCtxt )
+import TcMonoType	( kcHsSigTypes, tcScopedTyVars, checkSigTyVars, tcHsSigType, sigPatCtxt )
 import Inst		( LIE, isEmptyLIE, plusLIE, emptyLIE, plusLIEs, lieToList )
-import TcEnv		( TcId, tcLookupLocalIds, tcExtendTyVarEnv, tcExtendLocalValEnv, tcExtendGlobalTyVars )
+import TcEnv		( TcId, tcLookupLocalIds, tcExtendTyVarEnv, tcExtendLocalValEnv, tcExtendGlobalTyVars,
+			  tcInLocalScope )
 import TcPat		( tcPat, tcMonoPatBndr, polyPatSig )
 import TcType		( TcType, newTyVarTy )
 import TcBinds		( tcBindsAndThen )
@@ -35,6 +37,7 @@ import Id		( idType )
 import BasicTypes	( RecFlag(..) )
 import Type		( tyVarsOfType, isTauTy,  mkFunTy,
 			  liftedTypeKind, openTypeKind, splitSigmaTy )
+import NameSet
 import VarSet
 import Var		( Id )
 import Bag
@@ -130,76 +133,36 @@ tcMatch :: [(Name,Id)]
 	-> TcM (TcMatch, LIE)
 
 tcMatch xve1 match@(Match sig_tvs pats maybe_rhs_sig grhss) expected_ty ctxt
-  = tcAddSrcLoc (getMatchLoc match)		$
-    tcAddErrCtxt (matchCtxt ctxt match)		$
+  = tcMatchPats pats expected_ty tc_grhss	`thenTc` \ ((pats', grhss'), lie, ex_binds) ->
+    returnTc (Match [] pats' Nothing (glue_on Recursive ex_binds grhss'), lie)
 
-    if null sig_tvs then	-- The common case
-	tc_match expected_ty	`thenTc` \ (_, match_and_lie) ->
-	returnTc match_and_lie
-
-    else
-	-- If there are sig tvs we must be careful *not* to use
-	-- expected_ty right away, else we'll unify with tyvars free
-	-- in the envt.  So invent a fresh tyvar and use that instead
-	newTyVarTy openTypeKind					`thenNF_Tc` \ tyvar_ty ->
+  where
+    tc_grhss pats' rhs_ty 
+	=	-- Check that the remaining "expected type" is not a rank-2 type
+		-- If it is it'll mess up the unifier when checking the RHS
+	  checkTc (isTauTy rhs_ty) lurkingRank2SigErr 		`thenTc_`
 
-	-- Extend the tyvar env and check the match itself
-	tcTyVars sig_tvs (mapTc_ kcHsSigType sig_tys)		`thenTc` \ sig_tyvars ->
-	tcExtendTyVarEnv sig_tyvars (tc_match tyvar_ty)		`thenTc` \ (pat_ids, match_and_lie) ->
+		-- Deal with the result signature
+	  tc_result_sig maybe_rhs_sig	( 
 
-	-- Check that the scoped type variables from the patterns
-	-- have not been constrained
-        tcAddErrCtxtM (sigPatCtxt sig_tyvars pat_ids)		(
-		checkSigTyVars sig_tyvars emptyVarSet
-	)							`thenTc_`
+		-- Typecheck the body
+		tcExtendLocalValEnv xve1 	$
+		tcGRHSs grhss rhs_ty ctxt	`thenTc` \ (grhss', lie) ->
+		returnTc ((pats', grhss'), lie)
+	  )
 
-	-- *Now* we're free to unify with expected_ty
-	unifyTauTy expected_ty tyvar_ty	`thenTc_`
+    tc_result_sig Nothing thing_inside
+	= thing_inside
+    tc_result_sig (Just sig) thing_inside
+	= tcAddScopedTyVars [sig]			$
+	  tcHsSigType sig				`thenTc` \ sig_ty ->
 
-	returnTc match_and_lie
+		-- Check that the signature isn't a polymorphic one, which
+		-- we don't permit (at present, anyway)
+	  checkTc (isTauTy sig_ty) (polyPatSig sig_ty)	`thenTc_`
+	  unifyTauTy expected_ty sig_ty			`thenTc_`
+	  thing_inside
 
-  where
-    sig_tys = case maybe_rhs_sig of { Just t -> [t]; Nothing -> [] }
-	      ++ collectSigTysFromPats pats
-	      
-    tc_match expected_ty 	-- Any sig tyvars are in scope by now
-      = -- STEP 1: Typecheck the patterns
-	tcMatchPats pats expected_ty	`thenTc` \ (rhs_ty, pats', lie_req1, ex_tvs, pat_bndrs, lie_avail) ->
-        let
-	  xve2       = bagToList pat_bndrs
-	  pat_ids    = map snd xve2
-        in
-
-	-- STEP 2: Check that the remaining "expected type" is not a rank-2 type
-	-- If it is it'll mess up the unifier when checking the RHS
-	checkTc (isTauTy rhs_ty) lurkingRank2SigErr 		`thenTc_`
-
-	-- STEP 3: Unify with the rhs type signature if any
-	(case maybe_rhs_sig of
-	    Nothing  -> returnTc ()
-	    Just sig -> tcHsSigType sig		`thenTc` \ sig_ty ->
-
-			-- Check that the signature isn't a polymorphic one, which
-			-- we don't permit (at present, anyway)
-		        checkTc (isTauTy sig_ty) (polyPatSig sig_ty)	`thenTc_`
-		        unifyTauTy rhs_ty sig_ty
-	)						`thenTc_`
-
-	-- STEP 4: Typecheck the guarded RHSs and the associated where clause
-	tcExtendLocalValEnv xve1 (tcExtendLocalValEnv xve2 (
-	    tcGRHSs grhss rhs_ty ctxt
-	))					`thenTc` \ (grhss', lie_req2) ->
-
-	-- STEP 5: Check for existentially bound type variables
-	tcCheckExistentialPat pat_ids ex_tvs lie_avail 
-			      (lie_req1 `plusLIE` lie_req2) 
-			      rhs_ty 		`thenTc` \ (lie_req', ex_binds) ->
-
-	-- Phew!  All done.
-	let
-            match' = Match [] pats' Nothing (glue_on Recursive ex_binds grhss')
-	in
-	returnTc (pat_ids, (match', lie_req'))
 
 	-- glue_on just avoids stupid dross
 glue_on _ EmptyMonoBinds grhss = grhss		-- The common case
@@ -221,8 +184,68 @@ tcGRHSs (GRHSs grhss binds _) expected_ty ctxt
 	= tcAddSrcLoc locn					$
 	  tcStmts ctxt (\ty -> ty, expected_ty) guarded		`thenTc` \ (guarded', lie) ->
 	  returnTc (GRHS guarded' locn, lie)
+\end{code}
 
 
+%************************************************************************
+%*									*
+\subsection{tcMatchPats}
+%*									*
+%************************************************************************
+
+\begin{code}	  
+tcMatchPats
+	:: [RenamedPat] -> TcType
+	-> ([TypecheckedPat] -> TcType -> TcM (a, LIE))
+	-> TcM (a, LIE, TcDictBinds)
+-- Typecheck the patterns, extend the environment to bind the variables,
+-- do the thing inside, use any existentially-bound dictionaries to 
+-- discharge parts of the returning LIE, and deal with pattern type
+-- signatures
+
+tcMatchPats pats expected_ty thing_inside
+  = 	-- STEP 1: Bring pattern-signature type variables into scope
+    tcAddScopedTyVars (collectSigTysFromPats pats)			$
+
+	-- STEP 2: Typecheck the patterns themselves, gathering all the stuff
+    tc_match_pats pats expected_ty	`thenTc` \ (rhs_ty, pats', lie_req1, ex_tvs, pat_bndrs, lie_avail) ->
+    
+	-- STEP 3: Extend the environment, and do the thing inside
+    let
+	  xve     = bagToList pat_bndrs
+	  pat_ids = map snd xve
+    in
+    tcExtendLocalValEnv xve (thing_inside pats' rhs_ty)		`thenTc` \ (result, lie_req2) ->
+
+	-- STEP 4: Check for existentially bound type variables
+	-- I'm a bit concerned that lie_req1 from an 'inner' pattern in the list
+	-- might need (via lie_req2) something made available from an 'outer' 
+	-- pattern.  But it's inconvenient to deal with, and I can't find an example
+    tcCheckExistentialPat pat_ids ex_tvs lie_avail lie_req1 rhs_ty	`thenTc` \ (lie_req1', ex_binds) ->
+
+    returnTc (result, lie_req1' `plusLIE` lie_req2, ex_binds)
+
+tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
+-- Find the not-already-in-scope signature type variables,
+-- kind-check them, and bring them into scope
+--
+-- We no longer specify that these type variables must be univerally 
+-- quantified (lots of email on the subject).  If you want to put that 
+-- back in, you need to
+--	a) Do a checkSigTyVars after thing_inside
+--	b) More insidiously, don't pass in expected_ty, else
+--	   we unify with it too early and checkSigTyVars barfs
+--	   Instead you have to pass in a fresh ty var, and unify
+--	   it with expected_ty afterwards
+tcAddScopedTyVars sig_tys thing_inside
+  = tcGetEnv					`thenNF_Tc` \ env ->
+    let
+	all_sig_tvs = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
+	sig_tvs = filter not_in_scope (nameSetToList all_sig_tvs)
+ 	not_in_scope tv = not (tcInLocalScope env tv)
+    in	      
+    tcScopedTyVars sig_tvs (kcHsSigTypes sig_tys) thing_inside
+
 tcCheckExistentialPat :: [TcId]		-- Ids bound by this pattern
 		      -> Bag TcTyVar	-- Existentially quantified tyvars bound by pattern
 		      -> LIE		--   and context
@@ -259,23 +282,14 @@ tcCheckExistentialPat ids ex_tvs lie_avail lie_req result_ty
     tv_list = bagToList ex_tvs
     not_overloaded id = case splitSigmaTy (idType id) of
 			  (_, theta, _) -> null theta
-\end{code}
 
-
-%************************************************************************
-%*									*
-\subsection{tcMatchPats}
-%*									*
-%************************************************************************
-
-\begin{code}
-tcMatchPats [] expected_ty
+tc_match_pats [] expected_ty
   = returnTc (expected_ty, [], emptyLIE, emptyBag, emptyBag, emptyLIE)
 
-tcMatchPats (pat:pats) expected_ty
+tc_match_pats (pat:pats) expected_ty
   = unifyFunTy expected_ty		`thenTc` \ (arg_ty, rest_ty) ->
     tcPat tcMonoPatBndr pat arg_ty	`thenTc` \ (pat', lie_req, pat_tvs, pat_ids, lie_avail) ->
-    tcMatchPats pats rest_ty		`thenTc` \ (rhs_ty, pats', lie_reqs, pats_tvs, pats_ids, lie_avails) ->
+    tc_match_pats pats rest_ty		`thenTc` \ (rhs_ty, pats', lie_reqs, pats_tvs, pats_ids, lie_avails) ->
     returnTc (	rhs_ty, 
 		pat':pats',
 		lie_req `plusLIE` lie_reqs,
@@ -331,52 +345,38 @@ tcStmtsAndThen
 tcStmtsAndThen combine do_or_lc m_ty [] do_next
   = do_next
 
+tcStmtsAndThen combine do_or_lc m_ty (stmt:stmts) do_next
+  = tcStmtAndThen combine do_or_lc m_ty stmt
+	(tcStmtsAndThen combine do_or_lc m_ty stmts do_next)
+
 	-- LetStmt
-tcStmtsAndThen combine do_or_lc m_ty (LetStmt binds : stmts) do_next
+tcStmtAndThen combine do_or_lc m_ty (LetStmt binds) thing_inside
   = tcBindsAndThen		-- No error context, but a binding group is
   	(glue_binds combine)	-- rather a large thing for an error context anyway
   	binds
-  	(tcStmtsAndThen combine do_or_lc m_ty stmts do_next)
-
-	-- BindStmt
-tcStmtsAndThen combine do_or_lc m_ty@(m,elt_ty) (stmt@(BindStmt pat exp src_loc) : stmts) do_next
-  = tcAddSrcLoc src_loc		(
-	tcSetErrCtxt (stmtCtxt do_or_lc stmt)	$
-    	newTyVarTy liftedTypeKind	`thenNF_Tc` \ pat_ty ->
-  	tcPat tcMonoPatBndr pat pat_ty	`thenTc` \ (pat', pat_lie, pat_tvs, pat_ids, avail) ->  
-      	tcExpr exp (m pat_ty)		`thenTc` \ (exp', exp_lie) ->
-  	returnTc (pat', exp',
-		  pat_lie `plusLIE` exp_lie,
-		  pat_tvs, pat_ids, avail)
-    )					`thenTc` \ (pat', exp', lie_req, pat_tvs, pat_bndrs, lie_avail) ->
-    let
-	new_val_env = bagToList pat_bndrs
-	pat_ids     = map snd new_val_env
-    in
-
-	-- Do the rest; we don't need to add the pat_tvs to the envt
-	-- because they all appear in the pat_ids's types
-    tcExtendLocalValEnv new_val_env (
-       tcStmtsAndThen combine do_or_lc m_ty stmts do_next
-    )						`thenTc` \ (thing, stmts_lie) ->
-
-	-- Reinstate context for existential checks
-    tcSetErrCtxt (stmtCtxt do_or_lc stmt) 		$
-    tcCheckExistentialPat pat_ids pat_tvs lie_avail
-			  stmts_lie (m elt_ty) 		`thenTc` \ (final_lie, dict_binds) ->
-
-    returnTc (combine (BindStmt pat' exp' src_loc)
-		      (glue_binds combine Recursive dict_binds thing),
-	      lie_req `plusLIE` final_lie)
+  	thing_inside
+
+tcStmtAndThen combine do_or_lc m_ty@(m,elt_ty) stmt@(BindStmt pat exp src_loc) thing_inside
+  = tcAddSrcLoc src_loc					$
+    tcAddErrCtxt (stmtCtxt do_or_lc stmt)		$
+    newTyVarTy liftedTypeKind				`thenNF_Tc` \ pat_ty ->
+    tcExpr exp (m pat_ty)				`thenTc` \ (exp', exp_lie) ->
+    tcMatchPats [pat] (mkFunTy pat_ty (m elt_ty))	(\ [pat'] _ ->
+	tcPopErrCtxt 				$
+	thing_inside 				`thenTc` \ (thing, lie) ->
+	returnTc ((BindStmt pat' exp' src_loc, thing), lie)
+    )							`thenTc` \ ((stmt', thing), lie, dict_binds) ->
+    returnTc (combine stmt' (glue_binds combine Recursive dict_binds thing),
+	      lie `plusLIE` exp_lie)
 
 
 	-- ParStmt
-tcStmtsAndThen combine do_or_lc m_ty (ParStmtOut bndr_stmts_s : stmts) do_next
+tcStmtAndThen combine do_or_lc m_ty (ParStmtOut bndr_stmts_s) thing_inside
   = loop bndr_stmts_s		`thenTc` \ ((pairs', thing), lie) ->
     returnTc (combine (ParStmtOut pairs') thing, lie)
   where
     loop []
-      = tcStmtsAndThen combine do_or_lc m_ty stmts do_next	`thenTc` \ (thing, stmts_lie) ->
+      = thing_inside				`thenTc` \ (thing, stmts_lie) ->
 	returnTc (([], thing), stmts_lie)
 
     loop ((bndrs,stmts) : pairs)
@@ -393,31 +393,31 @@ tcStmtsAndThen combine do_or_lc m_ty (ParStmtOut bndr_stmts_s : stmts) do_next
     combine_par stmt (stmts, thing) = (stmt:stmts, thing)
 
 	-- ExprStmt
-tcStmtsAndThen combine do_or_lc m_ty@(m, res_elt_ty) (stmt@(ExprStmt exp locn):stmts) do_next
+tcStmtAndThen combine do_or_lc m_ty@(m, res_elt_ty) stmt@(ExprStmt exp locn) thing_inside
   = tcSetErrCtxt (stmtCtxt do_or_lc stmt) (
 	if isDoExpr do_or_lc then
 		newTyVarTy openTypeKind 	`thenNF_Tc` \ any_ty ->
 		tcExpr exp (m any_ty)	
 	else
 		tcExpr exp boolTy
-    )							`thenTc` \ (exp', stmt_lie) ->
+    )						`thenTc` \ (exp', stmt_lie) ->
 
-    tcStmtsAndThen combine do_or_lc m_ty stmts do_next	`thenTc` \ (thing, stmts_lie) ->
+    thing_inside 				`thenTc` \ (thing, stmts_lie) ->
 
     returnTc (combine (ExprStmt exp' locn) thing,
 	      stmt_lie `plusLIE` stmts_lie)
 
 
 	-- Result statements
-tcStmtsAndThen combine do_or_lc m_ty@(m, res_elt_ty) (stmt@(ResultStmt exp locn):stmts) do_next
+tcStmtAndThen combine do_or_lc m_ty@(m, res_elt_ty) stmt@(ResultStmt exp locn) thing_inside
   = tcSetErrCtxt (stmtCtxt do_or_lc stmt) (
 	if isDoExpr do_or_lc then
 		tcExpr exp (m res_elt_ty)
 	else
 		tcExpr exp res_elt_ty
-    )							`thenTc` \ (exp', stmt_lie) ->
+    )						`thenTc` \ (exp', stmt_lie) ->
 
-    tcStmtsAndThen combine do_or_lc m_ty stmts do_next	`thenTc` \ (thing, stmts_lie) ->
+    thing_inside 				`thenTc` \ (thing, stmts_lie) ->
 
     returnTc (combine (ResultStmt exp' locn) thing,
 	      stmt_lie `plusLIE` stmts_lie)
diff --git a/ghc/compiler/typecheck/TcMonad.lhs b/ghc/compiler/typecheck/TcMonad.lhs
index b6f0291cd0..f2d7791de0 100644
--- a/ghc/compiler/typecheck/TcMonad.lhs
+++ b/ghc/compiler/typecheck/TcMonad.lhs
@@ -32,7 +32,7 @@ module TcMonad(
 
 	tcAddSrcLoc, tcGetSrcLoc, tcGetInstLoc,
 	tcAddErrCtxtM, tcSetErrCtxtM,
-	tcAddErrCtxt, tcSetErrCtxt,
+	tcAddErrCtxt, tcSetErrCtxt, tcPopErrCtxt,
 
 	tcNewMutVar, tcNewSigTyVar, tcReadMutVar, tcWriteMutVar, TcRef,
 	tcNewMutTyVar, tcReadMutTyVar, tcWriteMutTyVar,
@@ -524,6 +524,9 @@ tcSetErrCtxt, tcAddErrCtxt :: Message -> Either_TcM r -> Either_TcM r
 -- Usual thing
 tcSetErrCtxt msg m down env = m (setErrCtxt down (\env -> returnNF_Tc (env, msg))) env
 tcAddErrCtxt msg m down env = m (addErrCtxt down (\env -> returnNF_Tc (env, msg))) env
+
+tcPopErrCtxt :: Either_TcM r -> Either_TcM  r
+tcPopErrCtxt m down env = m (popErrCtxt down) env
 \end{code}
 
 
@@ -607,6 +610,10 @@ getErrCtxt (TcDown{tc_ctxt=ctxt}) = ctxt
 setErrCtxt down msg = down{tc_ctxt=[msg]}
 addErrCtxt down msg = down{tc_ctxt = msg : tc_ctxt down}
 
+popErrCtxt down = case tc_ctxt down of
+			[]     -> down
+			m : ms -> down{tc_ctxt = ms}
+
 doptsTc :: DynFlag -> TcM Bool
 doptsTc dflag (TcDown{tc_dflags=dflags}) env_down
    = return (dopt dflag dflags)
diff --git a/ghc/compiler/typecheck/TcMonoType.lhs b/ghc/compiler/typecheck/TcMonoType.lhs
index 086478128c..bc42127e2f 100644
--- a/ghc/compiler/typecheck/TcMonoType.lhs
+++ b/ghc/compiler/typecheck/TcMonoType.lhs
@@ -10,8 +10,9 @@ module TcMonoType ( tcHsType, tcHsRecType, tcIfaceType,
 
 			-- Kind checking
 		    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
-		    kcHsType, kcHsSigType, kcHsLiftedSigType, kcHsContext,
-		    tcTyVars, tcHsTyVars, mkImmutTyVars,
+		    kcHsType, kcHsSigType, kcHsSigTypes, 
+		    kcHsLiftedSigType, kcHsContext,
+		    tcScopedTyVars, tcHsTyVars, mkImmutTyVars,
 
 		    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
 		    checkSigTyVars, sigCtxt, sigPatCtxt
@@ -30,7 +31,7 @@ import TcEnv		( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
 		 	  TyThing(..), TcTyThing(..), tcExtendKindEnv
 			)
 import TcType		( TcKind, TcTyVar, TcThetaType, TcTauType,
-			  newKindVar, tcInstSigVar,
+			  newKindVar, tcInstSigVars,
 			  zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
 			)
 import Inst		( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
@@ -117,6 +118,10 @@ But equally valid would be
 				a::(*->*)-> *, b::*->*
 
 \begin{code}
+-- tcHsTyVars is used for type variables in type signatures
+--	e.g. forall a. a->a
+-- They are immutable, because they scope only over the signature
+-- They may or may not be explicitly-kinded
 tcHsTyVars :: [HsTyVarBndr Name] 
 	   -> TcM a				-- The kind checker
 	   -> ([TyVar] -> TcM b)
@@ -134,16 +139,22 @@ tcHsTyVars tv_names kind_check thing_inside
     in
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 
-tcTyVars :: [Name] 
-	     -> TcM a				-- The kind checker
-	     -> TcM [TyVar]
-tcTyVars [] kind_check = returnTc []
-
-tcTyVars tv_names kind_check
+-- tcScopedTyVars is used for scoped type variables
+--	e.g.  \ (x::a) (y::a) -> x+y
+-- They never have explicit kinds (because this is source-code only)
+-- They are mutable (because they can get bound to a more specific type)
+tcScopedTyVars :: [Name] 
+	       -> TcM a				-- The kind checker
+	       -> TcM b
+	       -> TcM b
+tcScopedTyVars [] kind_check thing_inside = thing_inside
+
+tcScopedTyVars tv_names kind_check thing_inside
   = mapNF_Tc newNamedKindVar tv_names		`thenTc` \ kind_env ->
     tcExtendKindEnv kind_env kind_check		`thenTc_`
     zonkKindEnv kind_env			`thenNF_Tc` \ tvs_w_kinds ->
-    listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- tvs_w_kinds]
+    listTc [tcNewMutTyVar name kind | (name, kind) <- tvs_w_kinds]	`thenNF_Tc` \ tyvars ->
+    tcExtendTyVarEnv tyvars thing_inside
 \end{code}
     
 
@@ -178,7 +189,8 @@ kcTypeType ty
 ---------------------------
 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
 	-- Used for type signatures
-kcHsSigType  	 = kcTypeType
+kcHsSigType  	  = kcTypeType
+kcHsSigTypes tys  = mapTc_ kcHsSigType tys
 kcHsLiftedSigType = kcLiftedType
 
 ---------------------------
@@ -682,7 +694,7 @@ mkTcSig poly_id src_loc
    let
 	(tyvars, rho) = splitForAllTys (idType poly_id)
    in
-   mapNF_Tc tcInstSigVar tyvars		`thenNF_Tc` \ tyvars' ->
+   tcInstSigVars tyvars			`thenNF_Tc` \ tyvars' ->
 	-- Make *signature* type variables
 
    let
diff --git a/ghc/compiler/typecheck/TcRules.lhs b/ghc/compiler/typecheck/TcRules.lhs
index b8f5bb8084..1e37d8cd17 100644
--- a/ghc/compiler/typecheck/TcRules.lhs
+++ b/ghc/compiler/typecheck/TcRules.lhs
@@ -17,7 +17,7 @@ import TcMonad
 import TcSimplify	( tcSimplifyToDicts, tcSimplifyInferCheck )
 import TcType		( zonkTcTyVarToTyVar, newTyVarTy )
 import TcIfaceSig	( tcCoreExpr, tcCoreLamBndrs, tcVar )
-import TcMonoType	( kcHsSigType, tcHsSigType, tcTyVars, checkSigTyVars )
+import TcMonoType	( kcHsSigTypes, tcHsSigType, tcScopedTyVars, checkSigTyVars )
 import TcExpr		( tcExpr )
 import TcEnv		( tcExtendLocalValEnv, tcExtendTyVarEnv, isLocalThing )
 import Rules		( extendRuleBase )
@@ -74,8 +74,7 @@ tcSourceRule (HsRule name sig_tvs vars lhs rhs src_loc)
     newTyVarTy openTypeKind				`thenNF_Tc` \ rule_ty ->
 
 	-- Deal with the tyvars mentioned in signatures
-    tcTyVars sig_tvs (mapTc_ kcHsSigType sig_tys) 	`thenTc` \ sig_tyvars ->
-    tcExtendTyVarEnv sig_tyvars (
+    tcScopedTyVars sig_tvs (kcHsSigTypes sig_tys) 	(
 
 		-- Ditto forall'd variables
 	mapNF_Tc new_id vars					`thenNF_Tc` \ ids ->
@@ -85,12 +84,11 @@ tcSourceRule (HsRule name sig_tvs vars lhs rhs src_loc)
 	tcExpr lhs rule_ty					`thenTc` \ (lhs', lhs_lie) ->
 	tcExpr rhs rule_ty					`thenTc` \ (rhs', rhs_lie) ->
 	
-	returnTc (sig_tyvars, ids, lhs', rhs', lhs_lie, rhs_lie)
-    )						`thenTc` \ (sig_tyvars, ids, lhs', rhs', lhs_lie, rhs_lie) ->
+	returnTc (ids, lhs', rhs', lhs_lie, rhs_lie)
+    )						`thenTc` \ (ids, lhs', rhs', lhs_lie, rhs_lie) ->
 
 		-- Check that LHS has no overloading at all
     tcSimplifyToDicts lhs_lie			`thenTc` \ (lhs_dicts, lhs_binds) ->
-    checkSigTyVars sig_tyvars emptyVarSet	`thenTc_`
 
 	-- Gather the template variables and tyvars
     let
diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 4df862cb16..3f6831bb9a 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -23,7 +23,7 @@ module TcType (
   tcSplitRhoTy,
 
   tcInstTyVar, tcInstTyVars,
-  tcInstSigVar,
+  tcInstSigVars,
   tcInstType,
 
   --------------------------------
@@ -171,14 +171,14 @@ tcInstTyVar tyvar
     in
     tcNewMutTyVar name (tyVarKind tyvar)
 
-tcInstSigVar tyvar	-- Very similar to tcInstTyVar
-  = tcGetUnique 	`thenNF_Tc` \ uniq ->
-    let 
-	name = setNameUnique (tyVarName tyvar) uniq
-	kind = tyVarKind tyvar
-    in
-    ASSERT( not (kind == openTypeKind) )	-- Shouldn't happen
-    tcNewSigTyVar name kind
+tcInstSigVars tyvars	-- Very similar to tcInstTyVar
+  = tcGetUniques 	`thenNF_Tc` \ uniqs ->
+    listTc [ ASSERT( not (kind == openTypeKind) )	-- Shouldn't happen
+	     tcNewSigTyVar name kind 
+	   | (tyvar, uniq) <- tyvars `zip` uniqs,
+	     let name = setNameUnique (tyVarName tyvar) uniq, 
+	     let kind = tyVarKind tyvar
+	   ]
 \end{code}
 
 @tcInstType@ instantiates the outer-level for-alls of a TcType with