[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.

39 files changed, 425 insertions, 331 deletions

diff --git a/ghc/compiler/basicTypes/Var.lhs b/ghc/compiler/basicTypes/Var.lhs
index 47d84a3948..9545f4877b 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 1a49ec32c4..d4154b4514 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 44ba746d25..a4a27b1ea0 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 5113913d47..958c333205 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 113a04883f..10e11ea611 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 ad3a25d346..85e08eb4ee 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 c2feb2af26..cb42ba5625 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 6b10b9e7d8..6d45c0d7b1 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 e57973e14e..e273d8f97a 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 de668a882f..ca6b3d9674 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 eb9ea2d81b..f63c93d295 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 f31746246a..6b1fcb879f 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 8f38a09219..cd354890fc 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 f90eb76edd..452754f5d1 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 d02133f9a7..f98124d97d 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 3ac0dcce52..895d7430be 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 16e84998df..adaa6c44a3 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 3d03c32fa4..be2a441e23 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 6c0ec0305b..6578da915e 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 82d5ebbd3c..c3758344d0 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 9b281edf86..a1bf17522e 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 c0df697327..7db92e076c 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 8bfce87ce8..75e2ce9d02 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 2e984fec3b..2c6f3222cc 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 a88316f66d..1431d689dc 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 eafae42cc3..3a8a68e311 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 58480b1ffe..dfe9f9527a 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 b992ce1458..ad07abc90e 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 95069c7b64..d296057bd2 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 1ec6b18042..446a9b2d10 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 d54594a40c..a8190d98f4 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 4bbcc5a5ff..cdd417fdfc 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 588f87168b..389355919f 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 c02e7125d1..0c8e9b3a15 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 e3a7fc322c..9ddc77475b 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 8af0a5379e..e0aa172c92 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 7177347362..71579c4aaf 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 7997de58a0..b2a27f36f5 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 1cb2d7fc5f..dbf52a6cc5 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