From 61bfd5dd3b9d70404d6f93c030a9bb1c402b9d31 Mon Sep 17 00:00:00 2001
From: simonpj <unknown>
Date: Wed, 31 Oct 2001 15:22:55 +0000
Subject: [PATCH] [project @ 2001-10-31 15:22:53 by simonpj]
 ------------------------------------------ 	Improved
 handling of scoped type variables 
 ------------------------------------------

The main effect of this commit is to allow scoped type variables
in pattern bindings, thus

	(x::a, y::b) = e

This was illegal, but now it's ok.  a and b have the same scope
as x and y.


On the way I beefed up the info inside a type variable
(TcType.TyVarDetails; c.f. IdInfo.GlobalIdDetails) which
helps to improve error messages. Hence the wide ranging changes.
Pity about the extra loop from Var to TcType, but can't be helped.
---
 ghc/compiler/basicTypes/Var.lhs            |   43 +++----
 ghc/compiler/deSugar/Desugar.lhs           |    4 +-
 ghc/compiler/deSugar/DsExpr.lhs            |    2 +-
 ghc/compiler/deSugar/Match.lhs             |    2 +-
 ghc/compiler/hsSyn/HsDecls.lhs             |   24 ++--
 ghc/compiler/hsSyn/HsExpr.lhs              |    8 +-
 ghc/compiler/hsSyn/HsSyn.lhs               |   28 +++++
 ghc/compiler/parser/ParseUtil.lhs          |    4 +-
 ghc/compiler/parser/Parser.y               |    8 +-
 ghc/compiler/parser/RdrHsSyn.lhs           |   11 +-
 ghc/compiler/rename/RnBinds.lhs            |    7 +-
 ghc/compiler/rename/RnEnv.lhs              |   20 +---
 ghc/compiler/rename/RnExpr.lhs             |   10 +-
 ghc/compiler/rename/RnHsSyn.lhs            |    8 +-
 ghc/compiler/rename/RnSource.lhs           |   16 ++-
 ghc/compiler/simplCore/OccurAnal.lhs       |   14 +++
 ghc/compiler/simplCore/SimplMonad.lhs      |   45 ++++---
 ghc/compiler/typecheck/Inst.lhs            |    2 +-
 ghc/compiler/typecheck/TcBinds.lhs         |   20 +++-
 ghc/compiler/typecheck/TcClassDcl.lhs      |   10 +-
 ghc/compiler/typecheck/TcEnv.lhs           |   42 ++++---
 ghc/compiler/typecheck/TcExpr.hi-boot      |    2 +-
 ghc/compiler/typecheck/TcExpr.hi-boot-5    |    2 +-
 ghc/compiler/typecheck/TcExpr.lhs          |    5 +-
 ghc/compiler/typecheck/TcGRHSs.hi-boot     |    2 +-
 ghc/compiler/typecheck/TcGenDeriv.lhs      |    2 +-
 ghc/compiler/typecheck/TcHsSyn.lhs         |   11 +-
 ghc/compiler/typecheck/TcInstDcls.lhs      |   10 +-
 ghc/compiler/typecheck/TcMType.lhs         |   32 ++---
 ghc/compiler/typecheck/TcMatches.hi-boot   |    4 +-
 ghc/compiler/typecheck/TcMatches.hi-boot-5 |    4 +-
 ghc/compiler/typecheck/TcMatches.lhs       |   33 +-----
 ghc/compiler/typecheck/TcMonad.lhs         |   40 +------
 ghc/compiler/typecheck/TcMonoType.lhs      |  178 ++++++++++++++++------------
 ghc/compiler/typecheck/TcPat.lhs           |    2 +-
 ghc/compiler/typecheck/TcRules.lhs         |   14 +--
 ghc/compiler/typecheck/TcSimplify.lhs      |    3 +-
 ghc/compiler/typecheck/TcTyClsDecls.lhs    |    2 +-
 ghc/compiler/typecheck/TcType.lhs          |   82 ++++++++++++-
 39 files changed, 425 insertions(+), 331 deletions(-)

diff --git a/ghc/compiler/basicTypes/Var.lhs b/ghc/compiler/basicTypes/Var.lhs
index 47d84a3..9545f48 100644
--- a/ghc/compiler/basicTypes/Var.lhs
+++ b/ghc/compiler/basicTypes/Var.lhs
@@ -14,8 +14,7 @@ module Var (
 	tyVarName, tyVarKind,
 	setTyVarName, setTyVarUnique,
 	mkTyVar, mkSysTyVar, 
-	newMutTyVar, newSigTyVar,
-	readMutTyVar, writeMutTyVar, makeTyVarImmutable,
+	newMutTyVar, readMutTyVar, writeMutTyVar, makeTyVarImmutable,
 
 	-- Ids
 	Id, DictId,
@@ -27,7 +26,7 @@ module Var (
 
 	mkLocalId, mkGlobalId, mkSpecPragmaId,
 
-	isTyVar, isMutTyVar, isSigTyVar,
+	isTyVar, isMutTyVar, mutTyVarDetails,
 	isId, isLocalVar, isLocalId,
 	isGlobalId, isExportedId, isSpecPragmaId,
 	mustHaveLocalBinding
@@ -36,6 +35,7 @@ module Var (
 #include "HsVersions.h"
 
 import {-# SOURCE #-}	TypeRep( Type, Kind )
+import {-# SOURCE #-}	TcType( TyVarDetails )
 import {-# SOURCE #-}	IdInfo( GlobalIdDetails, notGlobalId,
 				IdInfo, seqIdInfo )
 
@@ -84,8 +84,7 @@ data VarDetails
 
   | TyVar
   | MutTyVar (IORef (Maybe Type)) 	-- Used during unification;
-	     Bool			-- True <=> this is a type signature variable, which
-					--	    should not be unified with a non-tyvar type
+	     TyVarDetails
 
 	-- For a long time I tried to keep mutable Vars statically type-distinct
 	-- from immutable Vars, but I've finally given up.   It's just too painful.
@@ -198,24 +197,15 @@ mkSysTyVar uniq kind = Var { varName    = name
 		     where
 		       name = mkSysLocalName uniq SLIT("t")
 
-newMutTyVar :: Name -> Kind -> IO TyVar
-newMutTyVar name kind = newTyVar name kind False
-
-newSigTyVar :: Name -> Kind -> IO TyVar
--- Type variables from type signatures are still mutable, because
--- they may get unified with type variables from other signatures
--- But they do contain a flag to distinguish them, so we can tell if
--- we unify them with a non-type-variable.
-newSigTyVar name kind = newTyVar name kind True
-
-newTyVar name kind is_sig
- = do loc <- newIORef Nothing
-      return (Var { varName    = name
-		  , realUnique = getKey (nameUnique name)
-		  , varType    = kind
-		  , varDetails = MutTyVar loc is_sig
-		  , varInfo    = pprPanic "newMutTyVar" (ppr name)
-		  })
+newMutTyVar :: Name -> Kind -> TyVarDetails -> IO TyVar
+newMutTyVar name kind details 
+  = do loc <- newIORef Nothing
+       return (Var { varName    = name
+		   , realUnique = getKey (nameUnique name)
+		   , varType    = kind
+		   , varDetails = MutTyVar loc details
+		   , varInfo    = pprPanic "newMutTyVar" (ppr name)
+		   })
 
 readMutTyVar :: TyVar -> IO (Maybe Type)
 readMutTyVar (Var {varDetails = MutTyVar loc _}) = readIORef loc
@@ -225,6 +215,9 @@ writeMutTyVar (Var {varDetails = MutTyVar loc _}) val = writeIORef loc val
 
 makeTyVarImmutable :: TyVar -> TyVar
 makeTyVarImmutable tyvar = tyvar { varDetails = TyVar}
+
+mutTyVarDetails :: TyVar -> TyVarDetails
+mutTyVarDetails (Var {varDetails = MutTyVar _ details}) = details
 \end{code}
 
 
@@ -308,7 +301,7 @@ mkGlobalId details name ty info = mkId name ty (GlobalId details) info
 \end{code}
 
 \begin{code}
-isTyVar, isMutTyVar, isSigTyVar		 :: Var -> Bool
+isTyVar, isMutTyVar			 :: Var -> Bool
 isId, isLocalVar, isLocalId    		 :: Var -> Bool
 isGlobalId, isExportedId, isSpecPragmaId :: Var -> Bool
 mustHaveLocalBinding			 :: Var -> Bool
@@ -321,8 +314,6 @@ isTyVar var = case varDetails var of
 isMutTyVar (Var {varDetails = MutTyVar _ _}) = True
 isMutTyVar other			     = False
 
-isSigTyVar (Var {varDetails = MutTyVar _ is_sig}) = is_sig
-isSigTyVar other			          = False
 
 isId var = case varDetails var of
 		LocalId _  -> True
diff --git a/ghc/compiler/deSugar/Desugar.lhs b/ghc/compiler/deSugar/Desugar.lhs
index 1a49ec3..d4154b4 100644
--- a/ghc/compiler/deSugar/Desugar.lhs
+++ b/ghc/compiler/deSugar/Desugar.lhs
@@ -165,13 +165,13 @@ dsRule :: IdSet -> TypecheckedRuleDecl -> DsM (Id, CoreRule)
 dsRule in_scope (IfaceRuleOut fun rule)	-- Built-in rules come this way
   = returnDs (fun, rule)
 
-dsRule in_scope (HsRule name act sig_tvs vars lhs rhs loc)
+dsRule in_scope (HsRule name act vars lhs rhs loc)
   = putSrcLocDs loc		$
     ds_lhs all_vars lhs		`thenDs` \ (fn, args) ->
     dsExpr rhs			`thenDs` \ core_rhs ->
     returnDs (fn, Rule name act tpl_vars args core_rhs)
   where
-    tpl_vars = sig_tvs ++ [var | RuleBndr var <- vars]
+    tpl_vars = [var | RuleBndr var <- vars]
     all_vars = mkInScopeSet (in_scope `unionVarSet` mkVarSet tpl_vars)
 
 ds_lhs all_vars lhs
diff --git a/ghc/compiler/deSugar/DsExpr.lhs b/ghc/compiler/deSugar/DsExpr.lhs
index 44ba746..a4a27b1 100644
--- a/ghc/compiler/deSugar/DsExpr.lhs
+++ b/ghc/compiler/deSugar/DsExpr.lhs
@@ -239,7 +239,7 @@ dsExpr (HsCase discrim matches src_loc)
 		returnDs (Case core_discrim bndr alts)
 	_ -> panic ("dsExpr: tuple pattern:\n" ++ showSDoc (ppr matching_code))
   where
-    ubx_tuple_match (Match _ [TuplePat ps Unboxed] _ _) = True
+    ubx_tuple_match (Match [TuplePat ps Unboxed] _ _) = True
     ubx_tuple_match _ = False
 
 dsExpr (HsCase discrim matches src_loc)
diff --git a/ghc/compiler/deSugar/Match.lhs b/ghc/compiler/deSugar/Match.lhs
index 5113913..958c333 100644
--- a/ghc/compiler/deSugar/Match.lhs
+++ b/ghc/compiler/deSugar/Match.lhs
@@ -738,7 +738,7 @@ flattenMatches kind matches
     ASSERT( all (tcEqType result_ty) result_tys )
     returnDs (result_ty, eqn_infos)
   where
-    flatten_match (Match _ pats _ grhss, n)
+    flatten_match (Match pats _ grhss, n)
       = dsGRHSs kind pats grhss 		`thenDs` \ (ty, match_result) ->
         getSrcLocDs				`thenDs` \ locn ->
 	returnDs (ty, EqnInfo n (DsMatchContext kind pats locn) pats match_result)
diff --git a/ghc/compiler/hsSyn/HsDecls.lhs b/ghc/compiler/hsSyn/HsDecls.lhs
index 113a048..10e11ea 100644
--- a/ghc/compiler/hsSyn/HsDecls.lhs
+++ b/ghc/compiler/hsSyn/HsDecls.lhs
@@ -18,7 +18,8 @@ module HsDecls (
 	tyClDeclName, tyClDeclNames, tyClDeclSysNames, tyClDeclTyVars,
 	isClassDecl, isSynDecl, isDataDecl, isIfaceSigDecl, countTyClDecls,
 	mkClassDeclSysNames, isIfaceRuleDecl, ifaceRuleDeclName,
-	getClassDeclSysNames, conDetailsTys
+	getClassDeclSysNames, conDetailsTys,
+	collectRuleBndrSigTys
     ) where
 
 #include "HsVersions.h"
@@ -768,9 +769,7 @@ data RuleDecl name pat
   = HsRule			-- Source rule
 	RuleName		-- Rule name
 	Activation
-	[name]			-- Forall'd tyvars, filled in by the renamer with
-				-- tyvars mentioned in sigs; then filled out by typechecker
-	[RuleBndr name]		-- Forall'd term vars
+	[RuleBndr name]		-- Forall'd vars; after typechecking this includes tyvars
 	(HsExpr name pat)	-- LHS
 	(HsExpr name pat)	-- RHS
 	SrcLoc		
@@ -789,18 +788,21 @@ data RuleDecl name pat
 	CoreRule
 
 isIfaceRuleDecl :: RuleDecl name pat -> Bool
-isIfaceRuleDecl (HsRule _ _ _ _ _ _ _) = False
-isIfaceRuleDecl other		       = True
+isIfaceRuleDecl (HsRule _ _ _ _ _ _) = False
+isIfaceRuleDecl other		     = True
 
 ifaceRuleDeclName :: RuleDecl name pat -> name
 ifaceRuleDeclName (IfaceRule _ _ _ n _ _ _) = n
 ifaceRuleDeclName (IfaceRuleOut n r)	    = n
-ifaceRuleDeclName (HsRule fs _ _ _ _ _ _)   = pprPanic "ifaceRuleDeclName" (ppr fs)
+ifaceRuleDeclName (HsRule fs _ _ _ _ _)     = pprPanic "ifaceRuleDeclName" (ppr fs)
 
 data RuleBndr name
   = RuleBndr name
   | RuleBndrSig name (HsType name)
 
+collectRuleBndrSigTys :: [RuleBndr name] -> [HsType name]
+collectRuleBndrSigTys bndrs = [ty | RuleBndrSig _ ty <- bndrs]
+
 instance (NamedThing name, Ord name) => Eq (RuleDecl name pat) where
   -- Works for IfaceRules only; used when comparing interface file versions
   (IfaceRule n1 a1 bs1 f1 es1 rhs1 _) == (IfaceRule n2 a2 bs2 f2 es2 rhs2 _)
@@ -810,15 +812,13 @@ instance (NamedThing name, Ord name) => Eq (RuleDecl name pat) where
 
 instance (NamedThing name, Outputable name, Outputable pat)
 	      => Outputable (RuleDecl name pat) where
-  ppr (HsRule name act tvs ns lhs rhs loc)
+  ppr (HsRule name act ns lhs rhs loc)
 	= sep [text "{-# RULES" <+> doubleQuotes (ptext name) <+> ppr act,
 	       pp_forall, ppr lhs, equals <+> ppr rhs,
                text "#-}" ]
 	where
-	  pp_forall | null tvs && null ns = empty
-		    | otherwise		  = text "forall" <+> 
-					    fsep (map ppr tvs ++ map ppr ns)
-					    <> dot
+	  pp_forall | null ns   = empty
+		    | otherwise	= text "forall" <+> fsep (map ppr ns) <> dot
 
   ppr (IfaceRule name act tpl_vars fn tpl_args rhs loc) 
     = hsep [ doubleQuotes (ptext name), ppr act,
diff --git a/ghc/compiler/hsSyn/HsExpr.lhs b/ghc/compiler/hsSyn/HsExpr.lhs
index ad3a25d..85e08eb 100644
--- a/ghc/compiler/hsSyn/HsExpr.lhs
+++ b/ghc/compiler/hsSyn/HsExpr.lhs
@@ -443,8 +443,6 @@ patterns in each equation.
 \begin{code}
 data Match id pat
   = Match
-	[id] 			-- Tyvars wrt which this match is universally quantified
-				-- empty after typechecking
 	[pat]			-- The patterns
 	(Maybe (HsType id))	-- A type signature for the result of the match
 				--	Nothing after typechecking
@@ -465,7 +463,7 @@ data GRHS id pat
 
 mkSimpleMatch :: [pat] -> HsExpr id pat -> Type -> SrcLoc -> Match id pat
 mkSimpleMatch pats rhs rhs_ty locn
-  = Match [] pats Nothing (GRHSs (unguardedRHS rhs locn) EmptyBinds rhs_ty)
+  = Match pats Nothing (GRHSs (unguardedRHS rhs locn) EmptyBinds rhs_ty)
 
 unguardedRHS :: HsExpr id pat -> SrcLoc -> [GRHS id pat]
 unguardedRHS rhs loc = [GRHS [ResultStmt rhs loc] loc]
@@ -477,7 +475,7 @@ THis is something of a nuisance, but no more.
 
 \begin{code}
 getMatchLoc :: Match id pat -> SrcLoc
-getMatchLoc (Match _ _ _ (GRHSs (GRHS _ loc : _) _ _)) = loc
+getMatchLoc (Match _ _ (GRHSs (GRHS _ loc : _) _ _)) = loc
 \end{code}
 
 We know the list must have at least one @Match@ in it.
@@ -500,7 +498,7 @@ pprPatBind pat grhss = sep [ppr pat, nest 4 (pprGRHSs PatBindRhs grhss)]
 
 pprMatch :: (Outputable id, Outputable pat)
 	   => HsMatchContext id -> Match id pat -> SDoc
-pprMatch ctxt (Match _ pats maybe_ty grhss)
+pprMatch ctxt (Match pats maybe_ty grhss)
   = pp_name ctxt <+> sep [sep (map ppr pats), 
 		     ppr_maybe_ty,
 		     nest 2 (pprGRHSs ctxt grhss)]
diff --git a/ghc/compiler/hsSyn/HsSyn.lhs b/ghc/compiler/hsSyn/HsSyn.lhs
index c2feb2a..cb42ba5 100644
--- a/ghc/compiler/hsSyn/HsSyn.lhs
+++ b/ghc/compiler/hsSyn/HsSyn.lhs
@@ -25,6 +25,7 @@ module HsSyn (
 
 	collectHsBinders, collectLocatedHsBinders, 
 	collectMonoBinders, collectLocatedMonoBinders,
+	collectSigTysFromMonoBinds,
 	hsModuleName, hsModuleImports
      ) where
 
@@ -149,3 +150,30 @@ collectMonoBinders binds
     go (FunMonoBind f _ _ loc) acc = f : acc
     go (AndMonoBinds bs1 bs2)  acc = go bs1 (go bs2 acc)
 \end{code}
+
+%************************************************************************
+%*									*
+\subsection{Getting patterns out of bindings}
+%*									*
+%************************************************************************
+
+Get all the pattern type signatures out of a bunch of bindings
+
+\begin{code}
+collectSigTysFromMonoBinds :: MonoBinds name (InPat name) -> [HsType name]
+collectSigTysFromMonoBinds bind
+  = go bind []
+  where
+    go EmptyMonoBinds           acc = acc
+    go (PatMonoBind pat _ loc)  acc = collectSigTysFromPat pat ++ acc
+    go (FunMonoBind f _ ms loc) acc = go_matches ms acc
+    go (AndMonoBinds bs1 bs2)   acc = go bs1 (go bs2 acc)
+
+	-- A binding like    x :: a = f y
+	-- is parsed as FunMonoBind, but for this purpose we 	
+	-- want to treat it as a pattern binding
+    go_matches []				 acc = acc
+    go_matches (Match [] (Just sig) _ : matches) acc = sig : go_matches matches acc
+    go_matches (match		      : matches) acc = go_matches matches acc
+\end{code}
+
diff --git a/ghc/compiler/parser/ParseUtil.lhs b/ghc/compiler/parser/ParseUtil.lhs
index 6b10b9e..6d45c0d 100644
--- a/ghc/compiler/parser/ParseUtil.lhs
+++ b/ghc/compiler/parser/ParseUtil.lhs
@@ -245,7 +245,7 @@ checkValDef lhs opt_sig grhss loc
  = case isFunLhs lhs [] of
 	   Just (f,inf,es) -> 
 		checkPatterns loc es `thenP` \ps ->
-		returnP (RdrValBinding (FunMonoBind f inf [Match [] ps opt_sig grhss] loc))
+		returnP (RdrValBinding (FunMonoBind f inf [Match ps opt_sig grhss] loc))
 
            Nothing ->
 		checkPattern loc lhs `thenP` \lhs ->
@@ -324,7 +324,7 @@ groupBindings binds = group Nothing binds
 		-- than pattern bindings (tests/rename/should_fail/rnfail002).
 	group (Just (FunMonoBind f inf1 mtchs ignore_srcloc))
 		    (RdrValBinding (FunMonoBind f' _ 
-					[mtch@(Match _ (_:_) _ _)] loc)
+					[mtch@(Match (_:_) _ _)] loc)
 			: binds)
 	    | f == f' = group (Just (FunMonoBind f inf1 (mtch:mtchs) loc)) binds
 
diff --git a/ghc/compiler/parser/Parser.y b/ghc/compiler/parser/Parser.y
index e57973e..e273d8f 100644
--- a/ghc/compiler/parser/Parser.y
+++ b/ghc/compiler/parser/Parser.y
@@ -1,6 +1,6 @@
 {-
 -----------------------------------------------------------------------------
-$Id: Parser.y,v 1.75 2001/10/22 09:37:24 simonpj Exp $
+$Id: Parser.y,v 1.76 2001/10/31 15:22:54 simonpj Exp $
 
 Haskell grammar.
 
@@ -454,7 +454,7 @@ rules	:: { RdrBinding }
 
 rule  	:: { RdrBinding }
 	: STRING activation rule_forall infixexp '=' srcloc exp
-	     { RdrHsDecl (RuleD (HsRule $1 $2 [] $3 $4 $7 $6)) }
+	     { RdrHsDecl (RuleD (HsRule $1 $2 $3 $4 $7 $6)) }
 
 activation :: { Activation }           -- Omitted means AlwaysActive
         : {- empty -}                           { AlwaysActive }
@@ -725,7 +725,7 @@ infixexp :: { RdrNameHsExpr }
 exp10 :: { RdrNameHsExpr }
 	: '\\' srcloc aexp aexps opt_asig '->' srcloc exp	
 			{% checkPatterns $2 ($3 : reverse $4) `thenP` \ ps -> 
-			   returnP (HsLam (Match [] ps $5 
+			   returnP (HsLam (Match ps $5 
 					    (GRHSs (unguardedRHS $8 $7) 
 						   EmptyBinds placeHolderType))) }
   	| 'let' declbinds 'in' exp		{ HsLet $2 $4 }
@@ -852,7 +852,7 @@ alts1 	:: { [RdrNameMatch] }
 alt 	:: { RdrNameMatch }
 	: srcloc infixexp opt_sig ralt wherebinds
 					{% (checkPattern $1 $2 `thenP` \p ->
-				   	   returnP (Match [] [p] $3
+				   	   returnP (Match [p] $3
 					             (GRHSs $4 $5 placeHolderType))  )}
 
 ralt :: { [RdrNameGRHS] }
diff --git a/ghc/compiler/parser/RdrHsSyn.lhs b/ghc/compiler/parser/RdrHsSyn.lhs
index de668a8..ca6b3d9 100644
--- a/ghc/compiler/parser/RdrHsSyn.lhs
+++ b/ghc/compiler/parser/RdrHsSyn.lhs
@@ -44,7 +44,6 @@ module RdrHsSyn (
 	SigConverter,
 
 	extractHsTyRdrNames,  extractHsTyRdrTyVars, 
-	extractRuleBndrsTyVars,
 	extractHsCtxtRdrTyVars, extractGenericPatTyVars,
  
 	mkHsOpApp, mkClassDecl, mkClassOpSigDM, mkConDecl,
@@ -130,12 +129,6 @@ extractHsTyRdrNames ty = nub (extract_ty ty [])
 extractHsTyRdrTyVars :: RdrNameHsType -> [RdrName]
 extractHsTyRdrTyVars ty = nub (filter isRdrTyVar (extract_ty ty []))
 
-extractRuleBndrsTyVars :: [RuleBndr RdrName] -> [RdrName]
-extractRuleBndrsTyVars bndrs = filter isRdrTyVar (nub (foldr go [] bndrs))
-                           where
-                             go (RuleBndr _)       acc = acc
-                             go (RuleBndrSig _ ty) acc = extract_ty ty acc
-
 extractHsCtxtRdrNames :: HsContext RdrName -> [RdrName]
 extractHsCtxtRdrNames ty = nub (extract_ctxt ty [])
 extractHsCtxtRdrTyVars :: HsContext RdrName -> [RdrName]
@@ -176,8 +169,8 @@ extractGenericPatTyVars binds
     get (FunMonoBind _ _ ms _) acc = foldr get_m acc ms
     get other		       acc = acc
 
-    get_m (Match _ (TypePatIn ty : _) _ _) acc = extract_ty ty acc
-    get_m other				   acc = acc
+    get_m (Match (TypePatIn ty : _) _ _) acc = extract_ty ty acc
+    get_m other				 acc = acc
 \end{code}
 
 
diff --git a/ghc/compiler/rename/RnBinds.lhs b/ghc/compiler/rename/RnBinds.lhs
index eb9ea2d..f63c93d 100644
--- a/ghc/compiler/rename/RnBinds.lhs
+++ b/ghc/compiler/rename/RnBinds.lhs
@@ -27,7 +27,7 @@ import RnMonad
 import RnTypes		( rnHsSigType, rnHsType )
 import RnExpr		( rnMatch, rnGRHSs, rnPat, checkPrecMatch )
 import RnEnv		( bindLocatedLocalsRn, lookupBndrRn, 
-			  lookupGlobalOccRn, lookupSigOccRn,
+			  lookupGlobalOccRn, lookupSigOccRn, bindPatSigTyVars,
 			  warnUnusedLocalBinds, mapFvRn, extendTyVarEnvFVRn,
 			)
 import CmdLineOpts	( DynFlag(..) )
@@ -217,7 +217,8 @@ rnMonoBinds mbinds sigs	thing_inside -- Non-empty monobinds
   =	-- Extract all the binders in this group,
 	-- and extend current scope, inventing new names for the new binders
 	-- This also checks that the names form a set
-    bindLocatedLocalsRn doc mbinders_w_srclocs	$ \ new_mbinders ->
+    bindLocatedLocalsRn doc mbinders_w_srclocs			$ \ new_mbinders ->
+    bindPatSigTyVars (collectSigTysFromMonoBinds mbinds)	$ 
     let
 	binder_set = mkNameSet new_mbinders
     in
@@ -388,7 +389,7 @@ rnMethodBinds gen_tyvars (FunMonoBind name inf matches locn)
   where
 	-- Gruesome; bring into scope the correct members of the generic type variables
 	-- See comments in RnSource.rnSourceDecl(ClassDecl)
-    rn_match match@(Match _ (TypePatIn ty : _) _ _)
+    rn_match match@(Match (TypePatIn ty : _) _ _)
 	= extendTyVarEnvFVRn gen_tvs (rnMatch (FunRhs name) match)
 	where
 	  tvs     = map rdrNameOcc (extractHsTyRdrNames ty)
diff --git a/ghc/compiler/rename/RnEnv.lhs b/ghc/compiler/rename/RnEnv.lhs
index f317462..6b1fcb8 100644
--- a/ghc/compiler/rename/RnEnv.lhs
+++ b/ghc/compiler/rename/RnEnv.lhs
@@ -596,24 +596,8 @@ bindTyVars2Rn doc_str tyvar_names enclosed_scope
     bindLocatedLocalsRn doc_str located_tyvars	$ \ names ->
     enclosed_scope names (zipWith replaceTyVarName tyvar_names names)
 
-bindTyVarsFVRn :: SDoc -> [HsTyVarBndr RdrName]
-	      -> ([HsTyVarBndr Name] -> RnMS (a, FreeVars))
-	      -> RnMS (a, FreeVars)
-bindTyVarsFVRn doc_str rdr_names enclosed_scope
-  = bindTyVars2Rn doc_str rdr_names	$ \ names tyvars ->
-    enclosed_scope tyvars		`thenRn` \ (thing, fvs) ->
-    returnRn (thing, delListFromNameSet fvs names)
-
-bindTyVarsFV2Rn :: SDoc -> [HsTyVarBndr RdrName]
-	      -> ([Name] -> [HsTyVarBndr Name] -> RnMS (a, FreeVars))
-	      -> RnMS (a, FreeVars)
-bindTyVarsFV2Rn doc_str rdr_names enclosed_scope
-  = bindTyVars2Rn doc_str rdr_names	$ \ names tyvars ->
-    enclosed_scope names tyvars		`thenRn` \ (thing, fvs) ->
-    returnRn (thing, delListFromNameSet fvs names)
-
 bindPatSigTyVars :: [RdrNameHsType]
-		 -> ([Name] -> RnMS (a, FreeVars))
+		 -> RnMS (a, FreeVars)
 	  	 -> RnMS (a, FreeVars)
   -- Find the type variables in the pattern type 
   -- signatures that must be brought into scope
@@ -634,7 +618,7 @@ bindPatSigTyVars tys enclosed_scope
 	doc_sig        = text "In a pattern type-signature"
     in
     bindLocatedLocalsRn doc_sig located_tyvars	$ \ names ->
-    enclosed_scope names			`thenRn` \ (thing, fvs) ->
+    enclosed_scope 				`thenRn` \ (thing, fvs) ->
     returnRn (thing, delListFromNameSet fvs names)
 
 
diff --git a/ghc/compiler/rename/RnExpr.lhs b/ghc/compiler/rename/RnExpr.lhs
index 8f38a09..cd35489 100644
--- a/ghc/compiler/rename/RnExpr.lhs
+++ b/ghc/compiler/rename/RnExpr.lhs
@@ -159,7 +159,7 @@ rnPat (TypePatIn name) =
 \begin{code}
 rnMatch :: HsMatchContext RdrName -> RdrNameMatch -> RnMS (RenamedMatch, FreeVars)
 
-rnMatch ctxt match@(Match _ pats maybe_rhs_sig grhss)
+rnMatch ctxt match@(Match pats maybe_rhs_sig grhss)
   = pushSrcLocRn (getMatchLoc match)	$
 
 	-- Bind pattern-bound type variables
@@ -171,7 +171,7 @@ rnMatch ctxt match@(Match _ pats maybe_rhs_sig grhss)
 	doc_sig     = text "In a result type-signature"
  	doc_pat     = pprMatchContext ctxt
     in
-    bindPatSigTyVars (rhs_sig_tys ++ pat_sig_tys)	$ \ sig_tyvars ->
+    bindPatSigTyVars (rhs_sig_tys ++ pat_sig_tys)	$ 
 
 	-- Note that we do a single bindLocalsRn for all the
 	-- matches together, so that we spot the repeated variable in
@@ -196,7 +196,7 @@ rnMatch ctxt match@(Match _ pats maybe_rhs_sig grhss)
     in
     warnUnusedMatches unused_binders		`thenRn_`
     
-    returnRn (Match sig_tyvars pats' maybe_rhs_sig' grhss', all_fvs)
+    returnRn (Match pats' maybe_rhs_sig' grhss', all_fvs)
 	-- The bindLocals and bindTyVars will remove the bound FVs
 \end{code}
 
@@ -571,7 +571,7 @@ rnStmt (ParStmt stmtss) thing_inside
 rnStmt (BindStmt pat expr src_loc) thing_inside
   = pushSrcLocRn src_loc $
     rnExpr expr					`thenRn` \ (expr', fv_expr) ->
-    bindPatSigTyVars (collectSigTysFromPat pat)	$ \ sig_tyvars ->
+    bindPatSigTyVars (collectSigTysFromPat pat)	$ 
     bindLocalsFVRn doc (collectPatBinders pat)	$ \ new_binders ->
     rnPat pat					`thenRn` \ (pat', fv_pat) ->
     thing_inside (BindStmt pat' expr' src_loc)	`thenRn` \ ((rest_binders, result), fvs) ->
@@ -719,7 +719,7 @@ checkPrecMatch :: Bool -> Name -> RenamedMatch -> RnMS ()
 checkPrecMatch False fn match
   = returnRn ()
 
-checkPrecMatch True op (Match _ (p1:p2:_) _ _)
+checkPrecMatch True op (Match (p1:p2:_) _ _)
 	-- True indicates an infix lhs
   = getModeRn 		`thenRn` \ mode ->
 	-- See comments with rnExpr (OpApp ...)
diff --git a/ghc/compiler/rename/RnHsSyn.lhs b/ghc/compiler/rename/RnHsSyn.lhs
index f90eb76..452754f 100644
--- a/ghc/compiler/rename/RnHsSyn.lhs
+++ b/ghc/compiler/rename/RnHsSyn.lhs
@@ -167,8 +167,8 @@ instDeclFVs (InstDecl inst_ty _ _ maybe_dfun _)
     (case maybe_dfun of { Just n -> unitFV n; Nothing -> emptyFVs })
 
 ----------------
-ruleDeclFVs (HsRule _ _ _ _ _ _ _) = emptyFVs
-ruleDeclFVs (IfaceRuleOut _ _)	   = emptyFVs
+ruleDeclFVs (HsRule _ _ _ _ _ _) = emptyFVs
+ruleDeclFVs (IfaceRuleOut _ _)	 = emptyFVs
 ruleDeclFVs (IfaceRule _ _ vars _ args rhs _)
   = delFVs (map ufBinderName vars) $
     ufExprFVs rhs `plusFV` plusFVs (map ufExprFVs args)
@@ -236,8 +236,8 @@ maybeGenericMatch :: RenamedMatch -> Maybe (RenamedHsType, RenamedMatch)
   -- Tells whether a Match is for a generic definition
   -- and extract the type from a generic match and put it at the front
 
-maybeGenericMatch (Match tvs (TypePatIn ty : pats) sig_ty grhss)
-  = Just (ty, Match tvs pats sig_ty grhss)
+maybeGenericMatch (Match (TypePatIn ty : pats) sig_ty grhss)
+  = Just (ty, Match pats sig_ty grhss)
 
 maybeGenericMatch other_match = Nothing
 \end{code}
diff --git a/ghc/compiler/rename/RnSource.lhs b/ghc/compiler/rename/RnSource.lhs
index d02133f..f98124d 100644
--- a/ghc/compiler/rename/RnSource.lhs
+++ b/ghc/compiler/rename/RnSource.lhs
@@ -14,7 +14,7 @@ import HsSyn
 import HscTypes		( GlobalRdrEnv )
 import RdrName		( RdrName, isRdrDataCon, elemRdrEnv )
 import RdrHsSyn		( RdrNameConDecl, RdrNameTyClDecl,
-			  extractRuleBndrsTyVars, extractGenericPatTyVars
+			  extractGenericPatTyVars
 			)
 import RnHsSyn
 import HsCore
@@ -24,9 +24,9 @@ import RnTypes		( rnHsType, rnHsSigType, rnHsTypeFVs, rnContext )
 import RnBinds		( rnTopBinds, rnMethodBinds, renameSigs, renameSigsFVs )
 import RnEnv		( lookupTopBndrRn, lookupOccRn, lookupIfaceName,
 			  lookupOrigNames, lookupSysBinder, newLocalsRn,
-			  bindLocalsFVRn, 
+			  bindLocalsFVRn, bindPatSigTyVars,
 			  bindTyVarsRn, bindTyVars2Rn,
-			  bindTyVarsFV2Rn, extendTyVarEnvFVRn,
+			  extendTyVarEnvFVRn,
 			  bindCoreLocalRn, bindCoreLocalsRn, bindLocalNames,
 			  checkDupOrQualNames, checkDupNames, mapFvRn
 			)
@@ -229,11 +229,10 @@ rnIfaceRuleDecl (IfaceRuleOut fn rule)		-- Builtin rules come this way
   = lookupOccRn fn		`thenRn` \ fn' ->
     returnRn (IfaceRuleOut fn' rule)
 
-rnHsRuleDecl (HsRule rule_name act tvs vars lhs rhs src_loc)
-  = ASSERT( null tvs )
-    pushSrcLocRn src_loc			$
+rnHsRuleDecl (HsRule rule_name act vars lhs rhs src_loc)
+  = pushSrcLocRn src_loc				$
+    bindPatSigTyVars (collectRuleBndrSigTys vars)	$
 
-    bindTyVarsFV2Rn doc (map UserTyVar sig_tvs)	$ \ sig_tvs' _ ->
     bindLocalsFVRn doc (map get_var vars)	$ \ ids ->
     mapFvRn rn_var (vars `zip` ids)		`thenRn` \ (vars', fv_vars) ->
 
@@ -245,11 +244,10 @@ rnHsRuleDecl (HsRule rule_name act tvs vars lhs rhs src_loc)
 	bad_vars = [var | var <- ids, not (var `elemNameSet` fv_lhs)]
     in
     mapRn (addErrRn . badRuleVar rule_name) bad_vars	`thenRn_`
-    returnRn (HsRule rule_name act sig_tvs' vars' lhs' rhs' src_loc,
+    returnRn (HsRule rule_name act vars' lhs' rhs' src_loc,
 	      fv_vars `plusFV` fv_lhs `plusFV` fv_rhs)
   where
     doc = text "In the transformation rule" <+> ptext rule_name
-    sig_tvs = extractRuleBndrsTyVars vars
   
     get_var (RuleBndr v)      = v
     get_var (RuleBndrSig v _) = v
diff --git a/ghc/compiler/simplCore/OccurAnal.lhs b/ghc/compiler/simplCore/OccurAnal.lhs
index 3ac0dcc..895d743 100644
--- a/ghc/compiler/simplCore/OccurAnal.lhs
+++ b/ghc/compiler/simplCore/OccurAnal.lhs
@@ -507,6 +507,20 @@ occAnalRhs env id rhs
   = (final_usage, rhs')
   where
     (rhs_usage, rhs') = occAnal (rhsCtxt env) rhs
+	-- Note that we use an rhsCtxt.  This tells the occ anal that it's
+	-- looking at an RHS, which has an effect in occAnalApp
+	--
+	-- But there's a problem.  Consider
+	--	x1 = a0 : []
+	--	x2 = a1 : x1
+	--	x3 = a2 : x2
+	--	g  = f x2
+	-- First time round, it looks as if x1 and x2 occur as an arg of a 
+	-- let-bound constructor ==> give them a many-occurrence.
+	-- But then x3 is inlined (unconditionally as it happens) and
+	-- next time round, x2 will be, and the next time round x1 will be
+	-- Result: multiple simplifier iterations.  Sigh.  
+	-- Possible solution: use rhsCtxt for things that occur just once...
 
 	-- [March 98] A new wrinkle is that if the binder has specialisations inside
 	-- it then we count the specialised Ids as "extra rhs's".  That way
diff --git a/ghc/compiler/simplCore/SimplMonad.lhs b/ghc/compiler/simplCore/SimplMonad.lhs
index 16e8499..adaa6c4 100644
--- a/ghc/compiler/simplCore/SimplMonad.lhs
+++ b/ghc/compiler/simplCore/SimplMonad.lhs
@@ -790,8 +790,19 @@ seems a bit fragile.
 \begin{code}
 preInlineUnconditionally :: SimplEnv -> TopLevelFlag -> InId -> Bool
 preInlineUnconditionally env top_lvl bndr
---  | isTopLevel top_lvl     = False
--- 	Top-level fusion lost if we do this for (e.g. string constants)
+  | isTopLevel top_lvl     = False
+-- If we don't have this test, consider
+--	x = length [1,2,3]
+-- The full laziness pass carefully floats all the cons cells to
+-- top level, and preInlineUnconditionally floats them all back in.
+-- Result is (a) static allocation replaced by dynamic allocation
+--	     (b) many simplifier iterations because this tickles
+--		 a related problem
+-- 
+-- On the other hand, I have seen cases where top-level fusion is
+-- lost if we don't inline top level thing (e.g. string constants)
+-- We'll have to see
+
   | not active 		   = False
   | opt_SimplNoPreInlining = False
   | otherwise = case idOccInfo bndr of
@@ -859,19 +870,23 @@ gentle we are being.
 activeInline :: SimplEnv -> OutId -> OccInfo -> Bool
 activeInline env id occ
   = case getMode env of
-	SimplGently -> isDataConWrapId id || isOneOcc occ
-		-- No inlining at all when doing gentle stuff,
-		-- except (a) things that occur once
-		-- and (b) (hack alert) data con wrappers
-		-- 	   We want to inline data con wrappers even 
-		--	   in gentle mode because rule LHSs match better then
--- The reason for (a) is that too little clean-up happens if you 
--- don't inline use-once things.   Also a bit of inlining is *good* for
--- full laziness; it can expose constant sub-expressions.
--- Example in spectral/mandel/Mandel.hs, where the mandelset 
--- function gets a useful let-float if you inline windowToViewport
-
-	SimplPhase n -> isActive n (idInlinePragma id)
+      SimplGently -> isOneOcc occ
+	-- No inlining at all when doing gentle stuff,
+	-- except for things that occur once
+	-- The reason is that too little clean-up happens if you 
+	-- don't inline use-once things.   Also a bit of inlining is *good* for
+	-- full laziness; it can expose constant sub-expressions.
+	-- Example in spectral/mandel/Mandel.hs, where the mandelset 
+	-- function gets a useful let-float if you inline windowToViewport
+
+	-- NB: we used to have a second exception, for data con wrappers.
+	-- On the grounds that we use gentle mode for rule LHSs, and 
+	-- they match better when data con wrappers are inlined.
+	-- But that only really applies to the trivial wrappers (like (:)),
+	-- and they are now constructed as Compulsory unfoldings (in MkId)
+	-- so they'll happen anyway.
+
+      SimplPhase n -> isActive n (idInlinePragma id)
 
 -- Belongs in BasicTypes; this frag occurs in OccurAnal too
 isOneOcc (OneOcc _ _) = True
diff --git a/ghc/compiler/typecheck/Inst.lhs b/ghc/compiler/typecheck/Inst.lhs
index 3d03c32..be2a441 100644
--- a/ghc/compiler/typecheck/Inst.lhs
+++ b/ghc/compiler/typecheck/Inst.lhs
@@ -44,7 +44,7 @@ import InstEnv	( InstLookupResult(..), lookupInstEnv )
 import TcMType	( zonkTcType, zonkTcTypes, zonkTcPredType,
 		  zonkTcThetaType, tcInstTyVar, tcInstType,
 		)
-import TcType	( Type, 
+import TcType	( Type, TcType, TcThetaType, TcPredType, TcTauType, TcTyVarSet,
 		  SourceType(..), PredType, ThetaType,
 		  tcSplitForAllTys, tcSplitForAllTys, 
 		  tcSplitMethodTy, tcSplitRhoTy, tcFunArgTy,
diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs
index 6c0ec03..6578da9 100644
--- a/ghc/compiler/typecheck/TcBinds.lhs
+++ b/ghc/compiler/typecheck/TcBinds.lhs
@@ -15,7 +15,8 @@ import {-# SOURCE #-} TcExpr  ( tcExpr )
 import CmdLineOpts	( opt_NoMonomorphismRestriction )
 import HsSyn		( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..), 
 			  Match(..), HsMatchContext(..), 
-			  collectMonoBinders, andMonoBinds
+			  collectMonoBinders, andMonoBinds,
+			  collectSigTysFromMonoBinds
 			)
 import RnHsSyn		( RenamedHsBinds, RenamedSig, RenamedMonoBinds )
 import TcHsSyn		( TcMonoBinds, TcId, zonkId, mkHsLet )
@@ -29,7 +30,7 @@ import TcEnv		( tcExtendLocalValEnv,
 			)
 import TcSimplify	( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, tcSimplifyToDicts )
 import TcMonoType	( tcHsSigType, UserTypeCtxt(..), checkSigTyVars,
-			  TcSigInfo(..), tcTySig, maybeSig, sigCtxt
+			  TcSigInfo(..), tcTySig, maybeSig, sigCtxt, tcAddScopedTyVars
 			)
 import TcPat		( tcPat )
 import TcSimplify	( bindInstsOfLocalFuns )
@@ -118,7 +119,14 @@ tc_binds_and_then top_lvl combiner (ThenBinds b1 b2) do_next
     do_next
 
 tc_binds_and_then top_lvl combiner (MonoBind bind sigs is_rec) do_next
-  =   	-- TYPECHECK THE SIGNATURES
+  =   	-- BRING ANY SCOPED TYPE VARIABLES INTO SCOPE
+	-- Notice that they scope over 
+	--	a) the type signatures in the binding group
+	--	b) the bindings in the group
+	--	c) the scope of the binding group (the "in" part)
+      tcAddScopedTyVars (collectSigTysFromMonoBinds bind)	$
+
+	-- TYPECHECK THE SIGNATURES
       mapTc tcTySig [sig | sig@(Sig name _ _) <- sigs]	`thenTc` \ tc_ty_sigs ->
   
       tcBindWithSigs top_lvl bind tc_ty_sigs
@@ -536,14 +544,14 @@ is_elem v vs = isIn "isUnResMono" v vs
 
 isUnRestrictedGroup sigs (PatMonoBind other        _ _) = False
 isUnRestrictedGroup sigs (VarMonoBind v _)	        = v `is_elem` sigs
-isUnRestrictedGroup sigs (FunMonoBind v _ matches _)	= any isUnRestrictedMatch matches || 
+isUnRestrictedGroup sigs (FunMonoBind v _ matches _)	= isUnRestrictedMatch matches || 
 							  v `is_elem` sigs
 isUnRestrictedGroup sigs (AndMonoBinds mb1 mb2)		= isUnRestrictedGroup sigs mb1 &&
 							  isUnRestrictedGroup sigs mb2
 isUnRestrictedGroup sigs EmptyMonoBinds			= True
 
-isUnRestrictedMatch (Match _ [] Nothing _) = False	-- No args, no signature
-isUnRestrictedMatch other		   = True	-- Some args or a signature
+isUnRestrictedMatch (Match [] _ _ : _) = False	-- No args => like a pattern binding
+isUnRestrictedMatch other	       = True	-- Some args => a function binding
 \end{code}
 
 
diff --git a/ghc/compiler/typecheck/TcClassDcl.lhs b/ghc/compiler/typecheck/TcClassDcl.lhs
index 82d5ebb..c375834 100644
--- a/ghc/compiler/typecheck/TcClassDcl.lhs
+++ b/ghc/compiler/typecheck/TcClassDcl.lhs
@@ -32,8 +32,9 @@ import TcEnv		( RecTcEnv, TyThingDetails(..), tcAddImportedIdInfo,
 import TcBinds		( tcBindWithSigs, tcSpecSigs )
 import TcMonoType	( tcHsType, tcHsTheta, checkSigTyVars, sigCtxt, mkTcSig )
 import TcSimplify	( tcSimplifyCheck, bindInstsOfLocalFuns )
-import TcMType		( tcInstTyVars, checkValidTheta, checkValidType, SourceTyCtxt(..), UserTypeCtxt(..) )
-import TcType		( Type, mkSigmaTy, mkTyVarTys, mkPredTys, mkClassPred, 
+import TcMType		( tcInstSigTyVars, checkValidTheta, checkValidType, SourceTyCtxt(..), UserTypeCtxt(..) )
+import TcType		( Type, TyVarDetails(..), TcType, TcThetaType, TcTyVar, 
+			  mkSigmaTy, mkTyVarTys, mkPredTys, mkClassPred, 
 			  tcIsTyVarTy, tcSplitTyConApp_maybe, tcSplitSigmaTy
 			)
 import TcMonad
@@ -420,9 +421,10 @@ tcDefMeth clas tyvars binds_in prags (_, GenDefMeth) = returnTc (EmptyMonoBinds,
 	-- (If necessary we can fix that, but we don't have a convenient Id to hand.)
 
 tcDefMeth clas tyvars binds_in prags op_item@(_, DefMeth dm_id)
-  = tcInstTyVars tyvars			`thenNF_Tc` \ (clas_tyvars, inst_tys, _) ->
+  = tcInstSigTyVars ClsTv tyvars			`thenNF_Tc` \ clas_tyvars ->
     let
-        theta = [(mkClassPred clas inst_tys)]
+	inst_tys    = mkTyVarTys clas_tyvars
+        theta       = [mkClassPred clas inst_tys]
 	local_dm_id = setIdLocalExported dm_id
 		-- Reason for setIdLocalExported: see notes with MkId.mkDictFunId
     in
diff --git a/ghc/compiler/typecheck/TcEnv.lhs b/ghc/compiler/typecheck/TcEnv.lhs
index 9b281ed..a1bf175 100644
--- a/ghc/compiler/typecheck/TcEnv.lhs
+++ b/ghc/compiler/typecheck/TcEnv.lhs
@@ -5,7 +5,7 @@ module TcEnv(
 
 	-- Getting stuff from the environment
 	TcEnv, initTcEnv, 
-	tcEnvTyCons, tcEnvClasses, tcEnvIds, tcEnvTcIds, tcEnvTyVars,
+	tcEnvTyCons, tcEnvClasses, tcEnvIds, tcLEnvElts,
 	getTcGEnv,
 	
 	-- Instance environment, and InstInfo type
@@ -42,7 +42,7 @@ module TcEnv(
 import RnHsSyn		( RenamedMonoBinds, RenamedSig )
 import TcMonad
 import TcMType		( zonkTcTyVarsAndFV )
-import TcType		( Type, ThetaType, 
+import TcType		( Type, ThetaType, TcType, TcKind, TcTyVar, TcTyVarSet, 
 			  tyVarsOfTypes, tcSplitDFunTy,
 			  getDFunTyKey, tcTyConAppTyCon
 			)
@@ -130,18 +130,6 @@ used thus:
 
 
 \begin{code}
-data TcTyThing
-  = AGlobal TyThing	-- Used only in the return type of a lookup
-  | ATcId  TcId		-- Ids defined in this module
-  | ATyVar TyVar	-- Type variables
-  | AThing TcKind	-- Used temporarily, during kind checking
--- Here's an example of how the AThing guy is used
--- Suppose we are checking (forall a. T a Int):
---	1. We first bind (a -> AThink kv), where kv is a kind variable. 
---	2. Then we kind-check the (T a Int) part.
---	3. Then we zonk the kind variable.
---	4. Now we know the kind for 'a', and we add (a -> ATyVar a::K) to the environment
-
 initTcEnv :: HomeSymbolTable -> PackageTypeEnv -> IO TcEnv
 initTcEnv hst pte 
   = do { gtv_var <- newIORef emptyVarSet ;
@@ -159,23 +147,39 @@ initTcEnv hst pte
 tcEnvClasses env = typeEnvClasses (tcGEnv env)
 tcEnvTyCons  env = typeEnvTyCons  (tcGEnv env) 
 tcEnvIds     env = typeEnvIds     (tcGEnv env) 
-tcEnvTyVars  env = [tv | ATyVar tv <- nameEnvElts (tcLEnv env)]
-tcEnvTcIds   env = [id | ATcId  id <- nameEnvElts (tcLEnv env)]
+tcLEnvElts   env = nameEnvElts (tcLEnv env)
 
 getTcGEnv (TcEnv { tcGEnv = genv }) = genv
 
 tcInLocalScope :: TcEnv -> Name -> Bool
 tcInLocalScope env v = v `elemNameEnv` (tcLEnv env)
+\end{code}
 
--- This data type is used to help tie the knot
--- when type checking type and class declarations
+\begin{code}
+data TcTyThing
+  = AGlobal TyThing		-- Used only in the return type of a lookup
+  | ATcId   TcId		-- Ids defined in this module
+  | ATyVar  TyVar 		-- Type variables
+  | AThing  TcKind		-- Used temporarily, during kind checking
+-- Here's an example of how the AThing guy is used
+-- Suppose we are checking (forall a. T a Int):
+--	1. We first bind (a -> AThink kv), where kv is a kind variable. 
+--	2. Then we kind-check the (T a Int) part.
+--	3. Then we zonk the kind variable.
+--	4. Now we know the kind for 'a', and we add (a -> ATyVar a::K) to the environment
+
+\end{code}
+
+This data type is used to help tie the knot
+ when type checking type and class declarations
+
+\begin{code}
 data TyThingDetails = SynTyDetails Type
 		    | DataTyDetails ThetaType [DataCon] [Id]
 		    | ClassDetails ThetaType [Id] [ClassOpItem] DataCon
 		    | ForeignTyDetails	-- Nothing yet
 \end{code}
 
-
 %************************************************************************
 %*									*
 \subsection{Basic lookups}
diff --git a/ghc/compiler/typecheck/TcExpr.hi-boot b/ghc/compiler/typecheck/TcExpr.hi-boot
index c0df697..7db92e0 100644
--- a/ghc/compiler/typecheck/TcExpr.hi-boot
+++ b/ghc/compiler/typecheck/TcExpr.hi-boot
@@ -4,7 +4,7 @@ TcExpr tcExpr ;
 _declarations_
 1 tcExpr _:_ _forall_ [s] => 
 	  RnHsSyn.RenamedHsExpr
-       -> TcMonad.TcType
+       -> TcType.TcType
        -> TcMonad.TcM s (TcHsSyn.TcExpr, Inst.LIE) ;;
 
 
diff --git a/ghc/compiler/typecheck/TcExpr.hi-boot-5 b/ghc/compiler/typecheck/TcExpr.hi-boot-5
index 8bfce87..75e2ce9 100644
--- a/ghc/compiler/typecheck/TcExpr.hi-boot-5
+++ b/ghc/compiler/typecheck/TcExpr.hi-boot-5
@@ -2,5 +2,5 @@ __interface TcExpr 1 0 where
 __export TcExpr tcExpr ;
 1 tcExpr :: 
 	  RnHsSyn.RenamedHsExpr
-       -> TcMonad.TcType
+       -> TcType.TcType
        -> TcMonad.TcM (TcHsSyn.TcExpr, Inst.LIE) ;
diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs
index 2e984fe..2c6f322 100644
--- a/ghc/compiler/typecheck/TcExpr.lhs
+++ b/ghc/compiler/typecheck/TcExpr.lhs
@@ -35,9 +35,8 @@ import TcMType		( tcInstTyVars, tcInstType,
 			  newTyVarTy, newTyVarTys, zonkTcType,
 			  unifyTauTy, unifyFunTy, unifyListTy, unifyTupleTy
 			)
-import TcType		( tcSplitFunTys, tcSplitTyConApp,
-			  isQualifiedTy, 
-			  mkFunTy, mkAppTy, mkTyConTy,
+import TcType		( TcType, TcTauType, tcSplitFunTys, tcSplitTyConApp,
+			  isQualifiedTy, mkFunTy, mkAppTy, mkTyConTy,
 			  mkTyConApp, mkClassPred, tcFunArgTy,
 			  isTauTy, tyVarsOfType, tyVarsOfTypes, 
 			  liftedTypeKind, openTypeKind, mkArrowKind,
diff --git a/ghc/compiler/typecheck/TcGRHSs.hi-boot b/ghc/compiler/typecheck/TcGRHSs.hi-boot
index a88316f..1431d68 100644
--- a/ghc/compiler/typecheck/TcGRHSs.hi-boot
+++ b/ghc/compiler/typecheck/TcGRHSs.hi-boot
@@ -4,7 +4,7 @@ TcGRHSs tcGRHSsAndBinds;
 _declarations_
 2 tcGRHSsAndBinds _:_ _forall_ [s] => 
 		RnHsSyn.RenamedGRHSsAndBinds
-		-> TcMonad.TcType s
+		-> TcType.TcType s
 		-> HsExpr.StmtCtxt
 		-> TcMonad.TcM s (TcHsSyn.TcGRHSsAndBinds s, Inst.LIE s) ;;
 
diff --git a/ghc/compiler/typecheck/TcGenDeriv.lhs b/ghc/compiler/typecheck/TcGenDeriv.lhs
index eafae42..3a8a68e 100644
--- a/ghc/compiler/typecheck/TcGenDeriv.lhs
+++ b/ghc/compiler/typecheck/TcGenDeriv.lhs
@@ -1155,7 +1155,7 @@ mk_FunMonoBind loc fun pats_and_exprs
 		loc
 
 mk_match loc pats expr binds
-  = Match [] (map paren pats) Nothing 
+  = Match (map paren pats) Nothing 
 	  (GRHSs (unguardedRHS expr loc) binds placeHolderType)
   where
     paren p@(VarPatIn _) = p
diff --git a/ghc/compiler/typecheck/TcHsSyn.lhs b/ghc/compiler/typecheck/TcHsSyn.lhs
index 58480b1..dfe9f95 100644
--- a/ghc/compiler/typecheck/TcHsSyn.lhs
+++ b/ghc/compiler/typecheck/TcHsSyn.lhs
@@ -343,11 +343,11 @@ zonkMonoBinds (AbsBinds tyvars dicts exports inlines val_bind)
 \begin{code}
 zonkMatch :: TcMatch -> NF_TcM TypecheckedMatch
 
-zonkMatch (Match _ pats _ grhss)
+zonkMatch (Match pats _ grhss)
   = zonkPats pats				`thenNF_Tc` \ (new_pats, new_ids) ->
     tcExtendGlobalValEnv (bagToList new_ids)	$
     zonkGRHSs grhss 				`thenNF_Tc` \ new_grhss ->
-    returnNF_Tc (Match [] new_pats Nothing new_grhss)
+    returnNF_Tc (Match new_pats Nothing new_grhss)
 
 -------------------------------------------------------------------------
 zonkGRHSs :: TcGRHSs
@@ -716,13 +716,12 @@ zonkForeignExport (ForeignExport i hs_ty spec src_loc) =
 zonkRules :: [TcRuleDecl] -> NF_TcM [TypecheckedRuleDecl]
 zonkRules rs = mapNF_Tc zonkRule rs
 
-zonkRule (HsRule name act tyvars vars lhs rhs loc)
-  = mapNF_Tc zonkTcTyVarToTyVar tyvars			`thenNF_Tc` \ new_tyvars ->
-    mapNF_Tc zonkIdBndr [v | RuleBndr v <- vars]	`thenNF_Tc` \ new_bndrs ->
+zonkRule (HsRule name act vars lhs rhs loc)
+  = mapNF_Tc zonkIdBndr [v | RuleBndr v <- vars]	`thenNF_Tc` \ new_bndrs ->
     tcExtendGlobalValEnv new_bndrs			$
     zonkExpr lhs					`thenNF_Tc` \ new_lhs ->
     zonkExpr rhs					`thenNF_Tc` \ new_rhs ->
-    returnNF_Tc (HsRule name act new_tyvars (map RuleBndr new_bndrs) new_lhs new_rhs loc)
+    returnNF_Tc (HsRule name act (map RuleBndr new_bndrs) new_lhs new_rhs loc)
 	-- I hate this map RuleBndr stuff
 
 zonkRule (IfaceRuleOut fun rule)
diff --git a/ghc/compiler/typecheck/TcInstDcls.lhs b/ghc/compiler/typecheck/TcInstDcls.lhs
index b992ce1..ad07abc 100644
--- a/ghc/compiler/typecheck/TcInstDcls.lhs
+++ b/ghc/compiler/typecheck/TcInstDcls.lhs
@@ -23,10 +23,11 @@ import TcHsSyn		( TcMonoBinds, mkHsConApp )
 import TcBinds		( tcSpecSigs )
 import TcClassDcl	( tcMethodBind, badMethodErr )
 import TcMonad       
-import TcMType		( tcInstTyVars, checkValidTheta, checkValidInstHead, instTypeErr,
+import TcMType		( tcInstSigTyVars, checkValidTheta, checkValidInstHead, instTypeErr, 
 			  UserTypeCtxt(..), SourceTyCtxt(..) )
-import TcType		( tcSplitDFunTy, mkClassPred, mkTyVarTy,
-			  tcSplitSigmaTy, tcSplitPredTy_maybe, getClassPredTys
+import TcType		( tcSplitDFunTy, mkClassPred, mkTyVarTy, mkTyVarTys,
+			  tcSplitSigmaTy, tcSplitPredTy_maybe, getClassPredTys,
+			  TyVarDetails(..)
 			)
 import Inst		( InstOrigin(..),
 			  newDicts, instToId,
@@ -524,8 +525,9 @@ tcInstDecl2 (InstInfo { iDFunId = dfun_id,
     let
 	(inst_tyvars, dfun_theta, clas, inst_tys) = tcSplitDFunTy (idType dfun_id)
     in
-    tcInstTyVars inst_tyvars		`thenNF_Tc` \ (inst_tyvars', _, tenv) ->
+    tcInstSigTyVars InstTv inst_tyvars		`thenNF_Tc` \ inst_tyvars' ->
     let
+	tenv	    = mkTopTyVarSubst inst_tyvars (mkTyVarTys inst_tyvars')
 	inst_tys'   = map (substTy tenv) inst_tys
 	dfun_theta' = substTheta tenv dfun_theta
 	origin	    = InstanceDeclOrigin
diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index 95069c7..d296057 100644
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -19,7 +19,7 @@ module TcMType (
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars,
-  tcInstSigVars, tcInstType,
+  tcInstSigTyVars, tcInstType,
   tcSplitRhoTyM,
 
   --------------------------------
@@ -50,10 +50,13 @@ import TypeRep		( Type(..), SourceType(..), TyNote(..),	 -- Friend; can see repr
 			  Kind, TauType, ThetaType, 
 			  openKindCon, typeCon
 			) 
-import TcType		( tcEqType, tcCmpPred,
+import TcType		( TcType, TcRhoType, TcThetaType, TcTauType, TcPredType,
+			  TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
+			  tcEqType, tcCmpPred,
 			  tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
 			  tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
-			  tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred,
+			  tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, 
+			  isUnLiftedType, isIPPred, isUserTyVar, isSkolemTyVar,
 
 			  mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
 			  tyVarsOfPred, getClassPredTys_maybe,
@@ -71,7 +74,7 @@ import TyCon		( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
 			  isTupleTyCon, tyConArity, tupleTyConBoxity, tyConName )
 import PrimRep		( PrimRep(VoidRep) )
 import Var		( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
-			  isMutTyVar, isSigTyVar )
+			  isMutTyVar, mutTyVarDetails )
 
 -- others:
 import TcMonad          -- TcType, amongst others
@@ -104,7 +107,7 @@ import Outputable
 newTyVar :: Kind -> NF_TcM TcTyVar
 newTyVar kind
   = tcGetUnique 	`thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
+    tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
 
 newTyVarTy  :: Kind -> NF_TcM TcType
 newTyVarTy kind
@@ -116,8 +119,8 @@ newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 
 newKindVar :: NF_TcM TcKind
 newKindVar
-  = tcGetUnique 						`thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind	`thenNF_Tc` \ kv ->
+  = tcGetUnique 							`thenNF_Tc` \ uniq ->
+    tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv	`thenNF_Tc` \ kv ->
     returnNF_Tc (TyVarTy kv)
 
 newKindVars :: Int -> NF_TcM [TcKind]
@@ -125,8 +128,8 @@ newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 
 newBoxityVar :: NF_TcM TcKind
 newBoxityVar
-  = tcGetUnique 						`thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity	`thenNF_Tc` \ kv ->
+  = tcGetUnique 							  `thenNF_Tc` \ uniq ->
+    tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
     returnNF_Tc (TyVarTy kv)
 \end{code}
 
@@ -195,12 +198,13 @@ tcInstTyVar tyvar
 	-- Better watch out for this.  If worst comes to worst, just
 	-- use mkSysLocalName.
     in
-    tcNewMutTyVar name (tyVarKind tyvar)
+    tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
 
-tcInstSigVars tyvars	-- Very similar to tcInstTyVar
+tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
+tcInstSigTyVars details tyvars	-- Very similar to tcInstTyVar
   = tcGetUniques 	`thenNF_Tc` \ uniqs ->
     listTc [ ASSERT( not (kind `eqKind` openTypeKind) )	-- Shouldn't happen
-	     tcNewSigTyVar name kind 
+	     tcNewMutTyVar name kind details
 	   | (tyvar, uniq) <- tyvars `zip` uniqs,
 	     let name = setNameUnique (tyVarName tyvar) uniq, 
 	     let kind = tyVarKind tyvar
@@ -1269,7 +1273,7 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
     update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
 			-- Try to get rid of open type variables as soon as poss
 
-    nicer_to_update_tv2 =  isSigTyVar tv1 
+    nicer_to_update_tv2 =  isUserTyVar (mutTyVarDetails tv1)
 				-- Don't unify a signature type variable if poss
 			|| isSystemName (varName tv2)
 				-- Try to update sys-y type variables in preference to sig-y ones
@@ -1280,7 +1284,7 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
     checkKinds swapped tv1 non_var_ty2			`thenTc_`
 
 	-- Check that tv1 isn't a type-signature type variable
-    checkTcM (not (isSigTyVar tv1))
+    checkTcM (not (isSkolemTyVar (mutTyVarDetails tv1)))
 	     (failWithTcM (unifyWithSigErr tv1 ps_ty2))	`thenTc_`
 
 	-- Check that we aren't losing boxity info (shouldn't happen)
diff --git a/ghc/compiler/typecheck/TcMatches.hi-boot b/ghc/compiler/typecheck/TcMatches.hi-boot
index 1ec6b18..446a9b2 100644
--- a/ghc/compiler/typecheck/TcMatches.hi-boot
+++ b/ghc/compiler/typecheck/TcMatches.hi-boot
@@ -5,12 +5,12 @@ _declarations_
 2 tcGRHSs _:_ _forall_ [s] => 
 	      HsExpr.HsMatchContext Name.Name
 	      -> RnHsSyn.RenamedGRHSs
-	      -> TcMonad.TcType
+	      -> TcType.TcType
 	      -> TcMonad.TcM s (TcHsSyn.TcGRHSs, Inst.LIE) ;;
 3 tcMatchesFun _:_ _forall_ [s] => 
 		[(Name.Name,Var.Id)]
 	     ->	Name.Name
-	     -> TcMonad.TcType
+	     -> TcType.TcType
 	     -> [RnHsSyn.RenamedMatch]
 	     -> TcMonad.TcM s ([TcHsSyn.TcMatch], Inst.LIE) ;;
 
diff --git a/ghc/compiler/typecheck/TcMatches.hi-boot-5 b/ghc/compiler/typecheck/TcMatches.hi-boot-5
index d54594a..a8190d9 100644
--- a/ghc/compiler/typecheck/TcMatches.hi-boot-5
+++ b/ghc/compiler/typecheck/TcMatches.hi-boot-5
@@ -2,12 +2,12 @@ __interface TcMatches 1 0 where
 __export TcMatches tcGRHSs tcMatchesFun;
 1 tcGRHSs ::  HsExpr.HsMatchContext Name.Name
 	      -> RnHsSyn.RenamedGRHSs
-	      -> TcMonad.TcType
+	      -> TcType.TcType
 	      -> TcMonad.TcM (TcHsSyn.TcGRHSs, Inst.LIE) ;
 1 tcMatchesFun :: 
 		[(Name.Name,Var.Id)]
 	     ->	Name.Name
-	     -> TcMonad.TcType
+	     -> TcType.TcType
 	     -> [RnHsSyn.RenamedMatch]
 	     -> TcMonad.TcM ([TcHsSyn.TcMatch], Inst.LIE) ;
 
diff --git a/ghc/compiler/typecheck/TcMatches.lhs b/ghc/compiler/typecheck/TcMatches.lhs
index 4bbcc5a..cdd417f 100644
--- a/ghc/compiler/typecheck/TcMatches.lhs
+++ b/ghc/compiler/typecheck/TcMatches.lhs
@@ -22,14 +22,14 @@ import RnHsSyn		( RenamedMatch, RenamedGRHSs, RenamedStmt, RenamedPat, RenamedHs
 import TcHsSyn		( TcMatch, TcGRHSs, TcStmt, TcDictBinds, TypecheckedPat )
 
 import TcMonad
-import TcMonoType	( kcHsSigTypes, tcScopedTyVars, checkSigTyVars, tcHsSigType, UserTypeCtxt(..), sigPatCtxt )
+import TcMonoType	( kcHsSigTypes, tcAddScopedTyVars, checkSigTyVars, tcHsSigType, UserTypeCtxt(..), sigPatCtxt )
 import Inst		( LIE, isEmptyLIE, plusLIE, emptyLIE, plusLIEs, lieToList )
 import TcEnv		( TcId, tcLookupLocalIds, tcExtendLocalValEnv, tcExtendGlobalTyVars,
 			  tcInLocalScope )
 import TcPat		( tcPat, tcMonoPatBndr, polyPatSig )
 import TcMType		( newTyVarTy, unifyFunTy, unifyTauTy )
-import TcType		( tyVarsOfType, isTauTy,  mkFunTy, isOverloadedTy,
-			  liftedTypeKind, openTypeKind  )
+import TcType		( TcType, TcTyVar, tyVarsOfType, isTauTy,  
+			  mkFunTy, isOverloadedTy, liftedTypeKind, openTypeKind  )
 import TcBinds		( tcBindsAndThen )
 import TcSimplify	( tcSimplifyCheck, bindInstsOfLocalFuns )
 import Name		( Name )
@@ -136,12 +136,12 @@ tcMatch :: [(Name,Id)]
 			-- where there are n patterns.
 	-> TcM (TcMatch, LIE)
 
-tcMatch xve1 ctxt match@(Match sig_tvs pats maybe_rhs_sig grhss) expected_ty
+tcMatch xve1 ctxt match@(Match pats maybe_rhs_sig grhss) expected_ty
   = tcAddSrcLoc (getMatchLoc match)		$	-- At one stage I removed this;
     tcAddErrCtxt (matchCtxt ctxt match)		$	-- I'm not sure why, so I put it back
     
     tcMatchPats pats expected_ty tc_grhss	`thenTc` \ ((pats', grhss'), lie, ex_binds) ->
-    returnTc (Match [] pats' Nothing (glue_on Recursive ex_binds grhss'), lie)
+    returnTc (Match pats' Nothing (glue_on Recursive ex_binds grhss'), lie)
 
   where
     tc_grhss pats' rhs_ty 
@@ -244,27 +244,6 @@ tcMatchPats pats expected_ty thing_inside
 
     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
@@ -462,7 +441,7 @@ sameNoOfArgs :: [RenamedMatch] -> Bool
 sameNoOfArgs matches = isSingleton (nub (map args_in_match matches))
   where
     args_in_match :: RenamedMatch -> Int
-    args_in_match (Match _ pats _ _) = length pats
+    args_in_match (Match pats _ _) = length pats
 \end{code}
 
 \begin{code}
diff --git a/ghc/compiler/typecheck/TcMonad.lhs b/ghc/compiler/typecheck/TcMonad.lhs
index 588f871..3893559 100644
--- a/ghc/compiler/typecheck/TcMonad.lhs
+++ b/ghc/compiler/typecheck/TcMonad.lhs
@@ -1,8 +1,5 @@
 \begin{code}
 module TcMonad(
-	TcType, TcTauType, TcPredType, TcThetaType, TcRhoType,
-	TcTyVar, TcTyVarSet, TcKind,
-
 	TcM, NF_TcM, TcDown, TcEnv, 
 
 	initTc,
@@ -32,7 +29,7 @@ module TcMonad(
 	tcAddErrCtxtM, tcSetErrCtxtM,
 	tcAddErrCtxt, tcSetErrCtxt, tcPopErrCtxt,
 
-	tcNewMutVar, tcNewSigTyVar, tcReadMutVar, tcWriteMutVar, TcRef,
+	tcNewMutVar, tcReadMutVar, tcWriteMutVar, TcRef,
 	tcNewMutTyVar, tcReadMutTyVar, tcWriteMutTyVar,
 
 	InstOrigin(..), InstLoc, pprInstLoc, 
@@ -47,14 +44,14 @@ import {-# SOURCE #-} TcEnv  ( TcEnv )
 
 import HsLit		( HsOverLit )
 import RnHsSyn		( RenamedPat, RenamedArithSeqInfo, RenamedHsExpr )
-import TcType		( Type, Kind, PredType, ThetaType, TauType, RhoType )
+import TcType		( Type, Kind, PredType, ThetaType, TyVarDetails )
 import ErrUtils		( addShortErrLocLine, addShortWarnLocLine, ErrMsg, Message, WarnMsg )
 
 import Bag		( Bag, emptyBag, isEmptyBag,
 			  foldBag, unitBag, unionBags, snocBag )
 import Class		( Class )
 import Name		( Name )
-import Var		( Id, TyVar, newMutTyVar, newSigTyVar, readMutTyVar, writeMutTyVar )
+import Var		( Id, TyVar, newMutTyVar, readMutTyVar, writeMutTyVar )
 import VarEnv		( TidyEnv, emptyTidyEnv )
 import VarSet		( TyVarSet )
 import UniqSupply	( UniqSupply, uniqFromSupply, uniqsFromSupply, 
@@ -77,30 +74,6 @@ infixr 9 `thenTc`, `thenTc_`, `thenNF_Tc`, `thenNF_Tc_`
 
 %************************************************************************
 %*									*
-\subsection{Types}
-%*									*
-%************************************************************************
-
-\begin{code}
-type TcTyVar    = TyVar		-- Might be a mutable tyvar
-type TcTyVarSet = TyVarSet
-
-type TcType = Type 		-- A TcType can have mutable type variables
-	-- Invariant on ForAllTy in TcTypes:
-	-- 	forall a. T
-	-- a cannot occur inside a MutTyVar in T; that is,
-	-- T is "flattened" before quantifying over a
-
-type TcPredType     = PredType
-type TcThetaType    = ThetaType
-type TcRhoType      = RhoType
-type TcTauType      = TauType
-type TcKind         = TcType
-\end{code}
-
-
-%************************************************************************
-%*									*
 \subsection{The main monads: TcM, NF_TcM}
 %*									*
 %************************************************************************
@@ -469,11 +442,8 @@ tcWriteMutVar var val down env = writeIORef var val
 tcReadMutVar :: TcRef a -> NF_TcM a
 tcReadMutVar var down env = readIORef var
 
-tcNewMutTyVar :: Name -> Kind -> NF_TcM TyVar
-tcNewMutTyVar name kind down env = newMutTyVar name kind
-
-tcNewSigTyVar :: Name -> Kind -> NF_TcM TyVar
-tcNewSigTyVar name kind down env = newSigTyVar name kind
+tcNewMutTyVar :: Name -> Kind -> TyVarDetails -> NF_TcM TyVar
+tcNewMutTyVar name kind details down env = newMutTyVar name kind details
 
 tcReadMutTyVar :: TyVar -> NF_TcM (Maybe Type)
 tcReadMutTyVar tyvar down env = readMutTyVar tyvar
diff --git a/ghc/compiler/typecheck/TcMonoType.lhs b/ghc/compiler/typecheck/TcMonoType.lhs
index c02e712..0c8e9b3 100644
--- a/ghc/compiler/typecheck/TcMonoType.lhs
+++ b/ghc/compiler/typecheck/TcMonoType.lhs
@@ -11,7 +11,7 @@ module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta,
 		    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
 		    kcHsType, kcHsSigType, kcHsSigTypes, 
 		    kcHsLiftedSigType, kcHsContext,
-		    tcScopedTyVars, tcHsTyVars, mkImmutTyVars,
+		    tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
 
 		    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
 		    checkSigTyVars, sigCtxt, sigPatCtxt
@@ -21,43 +21,45 @@ module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta,
 
 import HsSyn		( HsType(..), HsTyVarBndr(..),
                           Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
-import RnHsSyn		( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
+import RnHsSyn		( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
 import TcHsSyn		( TcId )
 
 import TcMonad
 import TcEnv		( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
-			  tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars,
+			  tcGetGlobalTyVars, tcLEnvElts, tcInLocalScope,
 		 	  TyThing(..), TcTyThing(..), tcExtendKindEnv
 			)
-import TcMType		( newKindVar, tcInstSigVars, 
+import TcMType		( newKindVar, tcInstSigTyVars, 
 			  zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
 			  unifyKind, unifyOpenTypeKind,
 			  checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
 			)
-import TcType		( Type, Kind, SourceType(..), ThetaType,
+import TcType		( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
+			  TcTyVar, TcTyVarSet, TcType, TcKind, TcThetaType, TcTauType,
 			  mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
-			  tcSplitForAllTys, tcSplitRhoTy,
-		 	  hoistForAllTys, allDistinctTyVars,
-                          zipFunTys, 
-			  mkSigmaTy, mkPredTy, mkTyConApp,
-			  mkAppTys, mkRhoTy,
+			  tcSplitForAllTys, tcSplitRhoTy, 
+		 	  hoistForAllTys, allDistinctTyVars, zipFunTys, 
+			  mkSigmaTy, mkPredTy, mkTyConApp, mkAppTys, mkRhoTy,
 			  liftedTypeKind, unliftedTypeKind, mkArrowKind,
 			  mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
 		  	  tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
 			  tyVarsOfType, mkForAllTys
 			)
+import qualified Type	( getTyVar_maybe )
+
 import Inst		( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
 import PprType		( pprType )
 import Subst		( mkTopTyVarSubst, substTy )
 import CoreFVs		( idFreeTyVars )
 import Id		( mkLocalId, idName, idType )
-import Var		( Id, Var, TyVar, mkTyVar, tyVarKind )
+import Var		( Id, Var, TyVar, mkTyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
 import VarEnv
 import VarSet
 import ErrUtils		( Message )
 import TyCon		( TyCon, isSynTyCon, tyConArity, tyConKind )
 import Class		( classTyCon )
-import Name		( Name )
+import Name		( Name, getSrcLoc )
+import NameSet
 import TysWiredIn	( mkListTy, mkTupleTy, genUnitTyCon )
 import BasicTypes	( Boxity(..) )
 import SrcLoc		( SrcLoc )
@@ -194,21 +196,41 @@ tcHsTyVars tv_names kind_check thing_inside
     in
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 
--- tcScopedTyVars is used for scoped type variables
+
+
+tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
+-- tcAddScopedTyVars is used for scoped type variables
+-- added by pattern type signatures
 --	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 ->
-    listTc [tcNewMutTyVar name kind | (name, kind) <- tvs_w_kinds]	`thenNF_Tc` \ tyvars ->
+
+-- 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 [] thing_inside
+  = thing_inside	-- Quick get-out for the empty case
+
+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	      
+    mapNF_Tc newNamedKindVar sig_tvs			`thenTc` \ kind_env ->
+    tcExtendKindEnv kind_env (kcHsSigTypes sig_tys)	`thenTc_`
+    zonkKindEnv kind_env				`thenNF_Tc` \ tvs_w_kinds ->
+    listTc [ tcNewMutTyVar name kind PatSigTv
+	   | (name, kind) <- tvs_w_kinds]		`thenNF_Tc` \ tyvars ->
     tcExtendTyVarEnv tyvars thing_inside
 \end{code}
     
@@ -561,7 +583,7 @@ mkTcSig poly_id src_loc
    let
 	(tyvars, rho) = tcSplitForAllTys (idType poly_id)
    in
-   tcInstSigVars tyvars			`thenNF_Tc` \ tyvars' ->
+   tcInstSigTyVars SigTv tyvars			`thenNF_Tc` \ tyvars' ->
 	-- Make *signature* type variables
 
    let
@@ -668,29 +690,12 @@ checkSigTyVars sig_tyvars free_tyvars
 
   where
     complain sig_tys globals
-      = -- For the in-scope ones, zonk them and construct a map
-	-- from the zonked tyvar to the in-scope one
-	-- If any of the in-scope tyvars zonk to a type, then ignore them;
-	-- that'll be caught later when we back up to their type sig
- 	tcGetEnv				`thenNF_Tc` \ env ->
- 	let
- 	   in_scope_tvs = tcEnvTyVars env
- 	in
-	zonkTcTyVars in_scope_tvs		`thenNF_Tc` \ in_scope_tys ->
-	let
-	    in_scope_assoc = [ (zonked_tv, in_scope_tv) 
-			     | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
-			       Just zonked_tv <- [tcGetTyVar_maybe z_ty]
-    			     ]
-	    in_scope_env = mkVarEnv in_scope_assoc
-	in
-
-	-- "check" checks each sig tyvar in turn
+      = -- "check" checks each sig tyvar in turn
         foldlNF_Tc check
-		   (env2, in_scope_env, [])
+		   (env2, emptyVarEnv, [])
 		   (tidy_tvs `zip` tidy_tys)	`thenNF_Tc` \ (env3, _, msgs) ->
 
-        failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
+        failWithTcM (env3, main_msg $$ vcat msgs)
       where
 	(env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
 	(env2, tidy_tys) = tidyOpenTypes  env1	       sig_tys
@@ -709,21 +714,21 @@ checkSigTyVars sig_tyvars free_tyvars
 	      Just tv ->
 
 	    case lookupVarEnv acc tv of {
-		Just sig_tyvar' -> 	-- Error (b) or (d)!
+		Just sig_tyvar' -> 	-- Error (b)!
 			returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
 		    where
 			thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
 
 	      ; Nothing ->
 
-	    if tv `elemVarSet` globals	-- Error (c)! Type variable escapes
+	    if tv `elemVarSet` globals	-- Error (c) or (d)! Type variable escapes
 					-- The least comprehensible, so put it last
 			-- Game plan: 
-			--    a) get the local TcIds from the environment,
+			--    a) get the local TcIds and TyVars from the environment,
 			-- 	 and pass them to find_globals (they might have tv free)
 			--    b) similarly, find any free_tyvars that mention tv
 	    then   tcGetEnv 							`thenNF_Tc` \ ve ->
-        	   find_globals tv tidy_env  [] (tcEnvTcIds ve)			`thenNF_Tc` \ (tidy_env1, globs) ->
+        	   find_globals tv tidy_env  (tcLEnvElts ve)			`thenNF_Tc` \ (tidy_env1, globs) ->
         	   find_frees   tv tidy_env1 [] (varSetElems free_tyvars)	`thenNF_Tc` \ (tidy_env2, frees) ->
 		   returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
 
@@ -731,6 +736,7 @@ checkSigTyVars sig_tyvars free_tyvars
 	    returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
 	    }}
 
+-----------------------
 -- find_globals looks at the value environment and finds values
 -- whose types mention the offending type variable.  It has to be 
 -- careful to zonk the Id's type first, so it has to be in the monad.
@@ -738,28 +744,56 @@ checkSigTyVars sig_tyvars free_tyvars
 
 find_globals :: Var 
              -> TidyEnv 
-             -> [(Name,Type)] 
-             -> [Id] 
-             -> NF_TcM (TidyEnv,[(Name,Type)])
-
-find_globals tv tidy_env acc []
-  = returnNF_Tc (tidy_env, acc)
+             -> [TcTyThing] 
+             -> NF_TcM (TidyEnv, [SDoc])
 
-find_globals tv tidy_env acc (id:ids) 
-  | isEmptyVarSet (idFreeTyVars id)
-  = find_globals tv tidy_env acc ids
-
-  | otherwise
-  = zonkTcType (idType id)	`thenNF_Tc` \ id_ty ->
-    if tv `elemVarSet` tyVarsOfType id_ty then
-    	let 
-    	   (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
-	   acc'		       = (idName id, id_ty') : acc
-    	in
-    	find_globals tv tidy_env' acc' ids
-    else
-    	find_globals tv tidy_env  acc  ids
+find_globals tv tidy_env things
+  = go tidy_env [] things
+  where
+    go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
+    go tidy_env acc (thing : things)
+      = find_thing ignore_it tidy_env thing 	`thenNF_Tc` \ (tidy_env1, maybe_doc) ->
+	case maybe_doc of
+	  Just d  -> go tidy_env1 (d:acc) things
+	  Nothing -> go tidy_env1 acc     things
+
+    ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
+
+-----------------------
+find_thing ignore_it tidy_env (ATcId id)
+  = zonkTcType  (idType id)	`thenNF_Tc` \ id_ty ->
+    if ignore_it id_ty then
+	returnNF_Tc (tidy_env, Nothing)
+    else let
+	(tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
+	msg = sep [ppr id <+> dcolon <+> ppr tidy_ty, 
+		   nest 2 (sep [quotes (ppr id) <+> ptext SLIT("is bound at"),
+				ptext SLIT("at") <+> ppr (getSrcLoc id)])]
+    in
+    returnNF_Tc (tidy_env', Just msg)
+
+find_thing ignore_it tidy_env (ATyVar tv)
+  = zonkTcTyVar tv		`thenNF_Tc` \ tv_ty ->
+    if ignore_it tv_ty then
+	returnNF_Tc (tidy_env, Nothing)
+    else let
+	(tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
+	(tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
+	msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
+
+	eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
+		 | otherwise	  				    = equals <+> ppr tv_ty
+		-- It's ok to use Type.getTyVar_maybe because ty is zonked by now
+	
+	bound_at | isMutTyVar tv = mut_info	-- The expected case
+		 | otherwise     = empty
+	
+	mut_info = sep [ptext SLIT("is bound by") <+> ppr (mutTyVarDetails tv),
+	     	        ptext SLIT("at") <+> ppr (getSrcLoc tv)]
+    in
+    returnNF_Tc (tidy_env2, Just msg)
 
+-----------------------
 find_frees tv tidy_env acc []
   = returnNF_Tc (tidy_env, acc)
 find_frees tv tidy_env acc (ftv:ftvs)
@@ -776,10 +810,7 @@ find_frees tv tidy_env acc (ftv:ftvs)
 escape_msg sig_tv tv globs frees
   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
     if not (null globs) then
-	vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
-	      ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
-	      nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
-	]
+	vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"), vcat globs]
      else if not (null frees) then
 	vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
 	      nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
@@ -798,6 +829,7 @@ escape_msg sig_tv tv globs frees
     vcat_first 0 (x:xs) = text "...others omitted..."
     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 
+
 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 \end{code}
diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs
index e3a7fc3..9ddc774 100644
--- a/ghc/compiler/typecheck/TcPat.lhs
+++ b/ghc/compiler/typecheck/TcPat.lhs
@@ -22,7 +22,7 @@ import Name		( Name )
 import FieldLabel	( fieldLabelName )
 import TcEnv		( tcLookupClass, tcLookupDataCon, tcLookupGlobalId, tcLookupId )
 import TcMType 		( tcInstTyVars, newTyVarTy, unifyTauTy, unifyListTy, unifyTupleTy )
-import TcType		( isTauTy, mkTyConApp, mkClassPred, liftedTypeKind )
+import TcType		( TcType, TcTyVar, isTauTy, mkTyConApp, mkClassPred, liftedTypeKind )
 import TcMonoType	( tcHsSigType, UserTypeCtxt(..) )
 
 import CmdLineOpts	( opt_IrrefutableTuples )
diff --git a/ghc/compiler/typecheck/TcRules.lhs b/ghc/compiler/typecheck/TcRules.lhs
index 8af0a53..e0aa172 100644
--- a/ghc/compiler/typecheck/TcRules.lhs
+++ b/ghc/compiler/typecheck/TcRules.lhs
@@ -8,7 +8,7 @@ module TcRules ( tcIfaceRules, tcSourceRules ) where
 
 #include "HsVersions.h"
 
-import HsSyn		( RuleDecl(..), RuleBndr(..) )
+import HsSyn		( RuleDecl(..), RuleBndr(..), collectRuleBndrSigTys )
 import CoreSyn		( CoreRule(..) )
 import RnHsSyn		( RenamedRuleDecl )
 import HscTypes		( PackageRuleBase )
@@ -18,7 +18,7 @@ import TcSimplify	( tcSimplifyToDicts, tcSimplifyInferCheck )
 import TcMType		( newTyVarTy )
 import TcType		( tyVarsOfTypes, openTypeKind )
 import TcIfaceSig	( tcCoreExpr, tcCoreLamBndrs, tcVar, tcDelay )
-import TcMonoType	( kcHsSigTypes, tcHsSigType, UserTypeCtxt(..), tcScopedTyVars )
+import TcMonoType	( kcHsSigTypes, tcHsSigType, UserTypeCtxt(..), tcAddScopedTyVars )
 import TcExpr		( tcExpr )
 import TcEnv		( RecTcEnv, tcExtendLocalValEnv, isLocalThing )
 import Rules		( extendRuleBase )
@@ -72,13 +72,13 @@ tcSourceRules decls
   = mapAndUnzipTc tcSourceRule decls	`thenTc` \ (lies, decls') ->
     returnTc (plusLIEs lies, decls')
 
-tcSourceRule (HsRule name act sig_tvs vars lhs rhs src_loc)
+tcSourceRule (HsRule name act vars lhs rhs src_loc)
   = tcAddSrcLoc src_loc 				$
     tcAddErrCtxt (ruleCtxt name)			$
     newTyVarTy openTypeKind				`thenNF_Tc` \ rule_ty ->
 
 	-- Deal with the tyvars mentioned in signatures
-    tcScopedTyVars sig_tvs (kcHsSigTypes sig_tys) 	(
+    tcAddScopedTyVars (collectRuleBndrSigTys vars) (
 
 		-- Ditto forall'd variables
 	mapNF_Tc new_id vars					`thenNF_Tc` \ ids ->
@@ -130,14 +130,12 @@ tcSourceRule (HsRule name act sig_tvs vars lhs rhs src_loc)
 			 forall_tvs
 			 lhs_dicts rhs_lie	`thenTc` \ (forall_tvs1, lie', rhs_binds) ->
 
-    returnTc (lie', HsRule	name act forall_tvs1
-				(map RuleBndr tpl_ids)	-- yuk
+    returnTc (lie', HsRule	name act
+				(map RuleBndr (forall_tvs1 ++ tpl_ids))	-- yuk
 				(mkHsLet lhs_binds lhs')
 				(mkHsLet rhs_binds rhs')
 				src_loc)
   where
-    sig_tys = [t | RuleBndrSig _ t <- vars]
-
     new_id (RuleBndr var) 	   = newTyVarTy openTypeKind			`thenNF_Tc` \ ty ->
 		          	     returnNF_Tc (mkLocalId var ty)
     new_id (RuleBndrSig var rn_ty) = tcHsSigType (RuleSigCtxt var) rn_ty	`thenTc` \ ty ->
diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs
index 7177347..71579c4 100644
--- a/ghc/compiler/typecheck/TcSimplify.lhs
+++ b/ghc/compiler/typecheck/TcSimplify.lhs
@@ -40,7 +40,8 @@ import TcEnv		( tcGetGlobalTyVars, tcGetInstEnv )
 import InstEnv		( lookupInstEnv, classInstEnv, InstLookupResult(..) )
 
 import TcMType		( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
-import TcType		( ThetaType, PredType, mkClassPred, isOverloadedTy,
+import TcType		( TcTyVar, TcTyVarSet, ThetaType, PredType, 
+			  mkClassPred, isOverloadedTy,
 			  mkTyVarTy, tcGetTyVar, isTyVarClassPred,
 			  tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
 			  inheritablePred, predHasFDs )
diff --git a/ghc/compiler/typecheck/TcTyClsDecls.lhs b/ghc/compiler/typecheck/TcTyClsDecls.lhs
index 7997de5..b2a27f3 100644
--- a/ghc/compiler/typecheck/TcTyClsDecls.lhs
+++ b/ghc/compiler/typecheck/TcTyClsDecls.lhs
@@ -30,7 +30,7 @@ import TcClassDcl	( tcClassDecl1, checkValidClass )
 import TcInstDcls	( tcAddDeclCtxt )
 import TcMonoType	( kcHsTyVars, kcHsType, kcHsLiftedSigType, kcHsContext, mkTyClTyVars )
 import TcMType		( unifyKind, newKindVar, zonkKindEnv )
-import TcType		( Type, Kind, mkArrowKind, liftedTypeKind, zipFunTys )
+import TcType		( Type, Kind, TcKind, mkArrowKind, liftedTypeKind, zipFunTys )
 import Type		( splitTyConApp_maybe )
 import Variance         ( calcTyConArgVrcs )
 import Class		( Class, mkClass, classTyCon )
diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 1cb2d7f..dbf52a6 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -17,7 +17,12 @@ is the principal client.
 module TcType (
   --------------------------------
   -- Types 
-  TauType, RhoType, SigmaType, 
+  TcType, TcTauType, TcPredType, TcThetaType, TcRhoType,
+  TcTyVar, TcTyVarSet, TcKind,
+
+  --------------------------------
+  -- TyVarDetails
+  TyVarDetails(..), isUserTyVar, isSkolemTyVar,
 
   --------------------------------
   -- Builders
@@ -142,14 +147,83 @@ import Outputable
 
 %************************************************************************
 %*									*
-\subsection{Tau, sigma and rho}
+\subsection{Types}
+%*									*
+%************************************************************************
+
+\begin{code}
+type TcTyVar    = TyVar		-- Might be a mutable tyvar
+type TcTyVarSet = TyVarSet
+
+type TcType = Type 		-- A TcType can have mutable type variables
+	-- Invariant on ForAllTy in TcTypes:
+	-- 	forall a. T
+	-- a cannot occur inside a MutTyVar in T; that is,
+	-- T is "flattened" before quantifying over a
+
+type TcPredType     = PredType
+type TcThetaType    = ThetaType
+type TcRhoType      = Type
+type TcTauType      = TauType
+type TcKind         = TcType
+\end{code}
+
+
+%************************************************************************
+%*									*
+\subsection{TyVarDetails}
 %*									*
 %************************************************************************
 
+TyVarDetails gives extra info about type variables, used during type
+checking.  It's attached to mutable type variables only.
+
 \begin{code}
-type SigmaType    = Type
-type RhoType   	  = Type
+data TyVarDetails
+  = SigTv	-- Introduced when instantiating a type signature,
+		-- prior to checking that the defn of a fn does 
+		-- have the expected type.  Should not be instantiated.
+		--
+		-- 	f :: forall a. a -> a
+		-- 	f = e
+		-- When checking e, with expected type (a->a), we 
+		-- should not instantiate a
+
+   | ClsTv	-- Scoped type variable introduced by a class decl
+		--	class C a where ...
+
+   | InstTv	-- Ditto, but instance decl
+
+   | PatSigTv	-- Scoped type variable, introduced by a pattern
+		-- type signature
+		--	\ x::a -> e
+
+   | VanillaTv	-- Everything else
+
+isUserTyVar :: TyVarDetails -> Bool	-- Avoid unifying these if possible
+isUserTyVar VanillaTv = False
+isUserTyVar other     = True
+
+isSkolemTyVar :: TyVarDetails -> Bool
+isSkolemTyVar SigTv = True
+isSkolemTyVar other = False
+
+instance Outputable TyVarDetails where
+  ppr SigTv	= ptext SLIT("type signature")
+  ppr ClsTv     = ptext SLIT("class declaration")
+  ppr InstTv    = ptext SLIT("instance declaration")
+  ppr PatSigTv  = ptext SLIT("pattern type signature")
+  ppr VanillaTv = ptext SLIT("???")
+\end{code}
 
+
+%************************************************************************
+%*									*
+\subsection{Tau, sigma and rho}
+%*									*
+%************************************************************************
+
+\begin{code}
 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
 
 mkRhoTy :: [SourceType] -> Type -> Type
-- 
1.7.10.4