diff --git a/ghc/compiler/iface/TcIface.lhs b/ghc/compiler/iface/TcIface.lhs
index 63be22cd549f37b044de70a62ba1881ac811f652..0f3cca2f500d0bf09777a7452ad891abe9c684b2 100644
--- a/ghc/compiler/iface/TcIface.lhs
+++ b/ghc/compiler/iface/TcIface.lhs
@@ -29,7 +29,7 @@ import HscTypes		( ExternalPackageState(..), EpsStats(..), PackageInstEnv,
 			  ModIface(..), ModDetails(..), ModGuts,
 			  mkTypeEnv, extendTypeEnv, 
 			  lookupTypeEnv, lookupType, typeEnvIds )
-import InstEnv		( extendInstEnv )
+import InstEnv		( extendInstEnvList )
 import CoreSyn
 import PprCore		( pprIdRules )
 import Rules		( extendRuleBaseList )
@@ -436,7 +436,7 @@ loadImportedInsts cls tys
 	-- And put them in the package instance environment
 	; updateEps ( \ eps ->
 	    let 
-		inst_env' = foldl extendInstEnv (eps_inst_env eps) dfuns
+		inst_env' = extendInstEnvList (eps_inst_env eps) dfuns
 	    in
 	    (eps { eps_inst_env = inst_env' }, inst_env')
 	)}}
diff --git a/ghc/compiler/main/CmdLineOpts.lhs b/ghc/compiler/main/CmdLineOpts.lhs
index 0e9f29b758145a92300d5e7f036d520a4acc533c..24e6d1569d9b6036fd23ae4ad2c9b996e68c81a6 100644
--- a/ghc/compiler/main/CmdLineOpts.lhs
+++ b/ghc/compiler/main/CmdLineOpts.lhs
@@ -275,6 +275,7 @@ data DynFlag
    | Opt_ImplicitParams
    | Opt_Generics
    | Opt_ImplicitPrelude 
+   | Opt_ScopedTypeVariables
 
    -- optimisation opts
    | Opt_Strictness
diff --git a/ghc/compiler/main/DriverFlags.hs b/ghc/compiler/main/DriverFlags.hs
index 0f53bd41001ae1359e82f7eac2eb0657b5cbbb61..2787040d9b4e26e8741012c538be8f2f4f765b0f 100644
--- a/ghc/compiler/main/DriverFlags.hs
+++ b/ghc/compiler/main/DriverFlags.hs
@@ -467,6 +467,7 @@ fFlags = [
   ( "parr",				Opt_PArr ),
   ( "th",				Opt_TH ),
   ( "implicit-prelude",  		Opt_ImplicitPrelude ),
+  ( "scoped-type-variables",  		Opt_ScopedTypeVariables ),
   ( "monomorphism-restriction",		Opt_MonomorphismRestriction ),
   ( "implicit-params",			Opt_ImplicitParams ),
   ( "allow-overlapping-instances", 	Opt_AllowOverlappingInstances ),
@@ -485,7 +486,7 @@ fFlags = [
   ( "unbox-strict-fields",		Opt_UnboxStrictFields )
   ]
 
-glasgowExtsFlags = [ Opt_GlasgowExts, Opt_FFI, Opt_TH, Opt_ImplicitParams ]
+glasgowExtsFlags = [ Opt_GlasgowExts, Opt_FFI, Opt_TH, Opt_ImplicitParams, Opt_ScopedTypeVariables ]
 
 isFFlag f = f `elem` (map fst fFlags)
 getFFlag f = fromJust (lookup f fFlags)
diff --git a/ghc/compiler/main/HscTypes.lhs b/ghc/compiler/main/HscTypes.lhs
index 3ce9eb9c940f95afbccb2b79266620613253d977..124397fe3c00ec158a4230fac3653cb2b68ad939 100644
--- a/ghc/compiler/main/HscTypes.lhs
+++ b/ghc/compiler/main/HscTypes.lhs
@@ -92,7 +92,6 @@ import Maybes		( orElse )
 import Outputable
 import SrcLoc		( SrcSpan )
 import UniqSupply	( UniqSupply )
-import Maybe		( fromJust )
 import FastString	( FastString )
 
 import DATA_IOREF	( IORef, readIORef )
diff --git a/ghc/compiler/rename/RnBinds.lhs b/ghc/compiler/rename/RnBinds.lhs
index 3d88d3231eb92ec03d131c639d2d900ceaba9fa6..0e01812347b1e49657add7e7a697e3482714f468 100644
--- a/ghc/compiler/rename/RnBinds.lhs
+++ b/ghc/compiler/rename/RnBinds.lhs
@@ -27,7 +27,7 @@ import RnExpr		( rnMatchGroup, rnMatch, rnGRHSs, checkPrecMatch )
 import RnEnv		( bindLocatedLocalsRn, lookupLocatedBndrRn, 
 			  lookupLocatedInstDeclBndr,
 			  lookupLocatedSigOccRn, bindPatSigTyVars, bindPatSigTyVarsFV,
-			  bindLocalFixities,
+			  bindLocalFixities, bindSigTyVarsFV, 
 			  warnUnusedLocalBinds, mapFvRn, extendTyVarEnvFVRn,
 			)
 import CmdLineOpts	( DynFlag(..) )
@@ -298,7 +298,9 @@ mkBindVertex sigs (L loc (PatBind pat grhss ty))
 	names_bound_here = mkNameSet (collectPatBinders pat')
     in
     sigsForMe names_bound_here sigs	`thenM` \ sigs_for_me ->
-    rnGRHSs PatBindRhs grhss		`thenM` \ (grhss', fvs) ->
+    bindSigTyVarsFV sigs_for_me (
+        rnGRHSs PatBindRhs grhss
+    )					`thenM` \ (grhss', fvs) ->
     returnM 
 	(names_bound_here, fvs `plusFV` pat_fvs,
 	  L loc (PatBind pat' grhss' ty), sigs_for_me
@@ -312,7 +314,9 @@ mkBindVertex sigs (L loc (FunBind name inf matches))
 	names_bound_here = unitNameSet plain_name
     in
     sigsForMe names_bound_here sigs			`thenM` \ sigs_for_me ->
-    rnMatchGroup (FunRhs plain_name) matches		`thenM` \ (new_matches, fvs) ->
+    bindSigTyVarsFV sigs_for_me (
+    	rnMatchGroup (FunRhs plain_name) matches
+    )							`thenM` \ (new_matches, fvs) ->
     checkPrecMatch inf plain_name new_matches		`thenM_`
     returnM
       (unitNameSet plain_name, fvs,
diff --git a/ghc/compiler/rename/RnEnv.lhs b/ghc/compiler/rename/RnEnv.lhs
index 9b0374daafff5b5eb8430189459aac4dfe40cd9b..d43a4e3eb54c84582c9d9da061c3db48f7c60fa5 100644
--- a/ghc/compiler/rename/RnEnv.lhs
+++ b/ghc/compiler/rename/RnEnv.lhs
@@ -18,7 +18,7 @@ module RnEnv (
 	newLocalsRn, newIPNameRn,
 	bindLocalNames, bindLocalNamesFV,
 	bindLocatedLocalsFV, bindLocatedLocalsRn,
-	bindPatSigTyVars, bindPatSigTyVarsFV,
+	bindSigTyVarsFV, bindPatSigTyVars, bindPatSigTyVarsFV,
 	bindTyVarsRn, extendTyVarEnvFVRn,
 	bindLocalFixities,
 
@@ -45,7 +45,7 @@ import RdrName		( RdrName, rdrNameModule, rdrNameOcc, isQual, isUnqual, isOrig,
 import HsTypes		( replaceTyVarName )
 import HscTypes		( availNames, ModIface(..), FixItem(..), lookupFixity )
 import TcRnMonad
-import Name		( Name, nameIsLocalOrFrom, mkInternalName, isInternalName,
+import Name		( Name, nameIsLocalOrFrom, mkInternalName, 
 			  nameSrcLoc, nameOccName, nameModule, nameParent, isExternalName )
 import NameSet
 import OccName		( tcName, isDataOcc, occNameFlavour, reportIfUnused )
@@ -557,15 +557,16 @@ bindLocatedLocalsRn doc_str rdr_names_w_loc enclosed_scope
 		   (enclosed_scope names)
 
 
+bindLocalNames :: [Name] -> RnM a -> RnM a
 bindLocalNames names enclosed_scope
   = getLocalRdrEnv 		`thenM` \ name_env ->
     setLocalRdrEnv (extendLocalRdrEnv name_env names)
 		    enclosed_scope
 
+bindLocalNamesFV :: [Name] -> RnM (a, FreeVars) -> RnM (a, FreeVars)
 bindLocalNamesFV names enclosed_scope
-  = bindLocalNames names $
-    enclosed_scope `thenM` \ (thing, fvs) ->
-    returnM (thing, delListFromNameSet fvs names)
+  = do	{ (result, fvs) <- bindLocalNames names enclosed_scope
+	; returnM (result, delListFromNameSet fvs names) }
 
 
 -------------------------------------
@@ -579,15 +580,10 @@ bindLocatedLocalsFV doc rdr_names enclosed_scope
     returnM (thing, delListFromNameSet fvs names)
 
 -------------------------------------
-extendTyVarEnvFVRn :: [Name] -> RnM (a, FreeVars) -> RnM (a, FreeVars)
-	-- This tiresome function is used only in rnSourceDecl on InstDecl
-extendTyVarEnvFVRn tyvars enclosed_scope
-  = bindLocalNames tyvars enclosed_scope 	`thenM` \ (thing, fvs) -> 
-    returnM (thing, delListFromNameSet fvs tyvars)
-
 bindTyVarsRn :: SDoc -> [LHsTyVarBndr RdrName]
 	      -> ([LHsTyVarBndr Name] -> RnM a)
 	      -> RnM a
+-- Haskell-98 binding of type variables; e.g. within a data type decl
 bindTyVarsRn doc_str tyvar_names enclosed_scope
   = let
 	located_tyvars = hsLTyVarLocNames tyvar_names
@@ -601,19 +597,22 @@ bindPatSigTyVars :: [LHsType RdrName] -> ([Name] -> RnM a) -> RnM a
   -- Find the type variables in the pattern type 
   -- signatures that must be brought into scope
 bindPatSigTyVars tys thing_inside
-  = getLocalRdrEnv		`thenM` \ name_env ->
-    let
-	located_tyvars  = nubBy eqLocated [ tv | ty <- tys,
-				    tv <- extractHsTyRdrTyVars ty,
-				    not (unLoc tv `elemLocalRdrEnv` name_env)
-			 ]
+  = do 	{ scoped_tyvars <- doptM Opt_ScopedTypeVariables
+	; if not scoped_tyvars then 
+		thing_inside []
+	  else 
+    do 	{ name_env <- getLocalRdrEnv
+	; let locd_tvs  = [ tv | ty <- tys
+			       , tv <- extractHsTyRdrTyVars ty
+			       , not (unLoc tv `elemLocalRdrEnv` name_env) ]
+	      nubbed_tvs = nubBy eqLocated locd_tvs
 		-- The 'nub' is important.  For example:
 		--	f (x :: t) (y :: t) = ....
 		-- We don't want to complain about binding t twice!
 
-	doc_sig        = text "In a pattern type-signature"
-    in
-    bindLocatedLocalsRn doc_sig located_tyvars thing_inside
+	; bindLocatedLocalsRn doc_sig nubbed_tvs thing_inside }}
+  where
+    doc_sig = text "In a pattern type-signature"
 
 bindPatSigTyVarsFV :: [LHsType RdrName]
 		   -> RnM (a, FreeVars)
@@ -623,6 +622,35 @@ bindPatSigTyVarsFV tys thing_inside
     thing_inside		`thenM` \ (result,fvs) ->
     returnM (result, fvs `delListFromNameSet` tvs)
 
+bindSigTyVarsFV :: [LSig Name]
+		-> RnM (a, FreeVars)
+	  	-> RnM (a, FreeVars)
+-- Bind the top-level forall'd type variables in the sigs.
+-- E.g 	f :: a -> a
+--	f = rhs
+--	The 'a' scopes over the rhs
+--
+-- NB: there'll usually be just one (for a function binding)
+--     but if there are many, one may shadow the rest; too bad!
+--	e.g  x :: [a] -> [a]
+--	     y :: [(a,a)] -> a
+--	     (x,y) = e
+--      In e, 'a' will be in scope, and it'll be the one from 'y'!
+bindSigTyVarsFV sigs thing_inside
+  = do	{ scoped_tyvars <- doptM Opt_ScopedTypeVariables
+	; if not scoped_tyvars then 
+		thing_inside 
+	  else
+		bindLocalNamesFV tvs thing_inside }
+  where
+    tvs = [ hsLTyVarName ltv 
+	  | L _ (Sig _ (L _ (HsForAllTy _ ltvs _ _))) <- sigs, ltv <- ltvs ]
+				
+
+extendTyVarEnvFVRn :: [Name] -> RnM (a, FreeVars) -> RnM (a, FreeVars)
+	-- This function is used only in rnSourceDecl on InstDecl
+extendTyVarEnvFVRn tyvars thing_inside = bindLocalNamesFV tyvars thing_inside
+
 -------------------------------------
 checkDupNames :: SDoc
 	      -> [Located RdrName]
diff --git a/ghc/compiler/typecheck/Inst.lhs b/ghc/compiler/typecheck/Inst.lhs
index 2f09895562c5912fd46bd0787b919b2819156af7..862145fac806731b795cd414a3c62245147d205e 100644
--- a/ghc/compiler/typecheck/Inst.lhs
+++ b/ghc/compiler/typecheck/Inst.lhs
@@ -54,9 +54,9 @@ import TcMType	( zonkTcType, zonkTcTypes, zonkTcPredType,
 		  zonkTcThetaType, tcInstTyVar, tcInstType, tcInstTyVars
 		)
 import TcType	( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar,
-		  PredType(..), typeKind,
+		  PredType(..), typeKind, mkSigmaTy,
 		  tcSplitForAllTys, tcSplitForAllTys, 
-		  tcSplitPhiTy, tcIsTyVarTy, tcSplitDFunTy,
+		  tcSplitPhiTy, tcIsTyVarTy, tcSplitDFunTy, tcSplitDFunHead,
 		  isIntTy,isFloatTy, isIntegerTy, isDoubleTy,
 		  tcIsTyVarTy, mkPredTy, mkTyVarTy, mkTyVarTys,
 		  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tidyPred,
@@ -79,7 +79,7 @@ import Name	( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
 		  isInternalName, setNameUnique, mkSystemNameEncoded )
 import NameSet	( addOneToNameSet )
 import Literal	( inIntRange )
-import Var	( TyVar, tyVarKind )
+import Var	( TyVar, tyVarKind, setIdType )
 import VarEnv	( TidyEnv, emptyTidyEnv, lookupVarEnv )
 import VarSet	( elemVarSet, emptyVarSet, unionVarSet, mkVarSet )
 import TysWiredIn ( floatDataCon, doubleDataCon )
@@ -566,10 +566,15 @@ addInst :: DynFlags -> InstEnv -> DFunId -> TcM InstEnv
 -- Check that the proposed new instance is OK, 
 -- and then add it to the home inst env
 addInst dflags home_ie dfun
-  = do	{ 	-- Load imported instances, so that we report
+  = do	{ 	-- Instantiate the dfun type so that we extend the instance
+		-- envt with completely fresh template variables
+	  (tvs', theta', tau') <- tcInstType (idType dfun)
+	; let	(cls, tys') = tcSplitDFunHead tau'
+		dfun' 	    = setIdType dfun (mkSigmaTy tvs' theta' tau')	    
+
+		-- Load imported instances, so that we report
 		-- duplicates correctly
-	  let (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
-	; pkg_ie  <- loadImportedInsts cls tys
+	; pkg_ie  <- loadImportedInsts cls tys'
 
 		-- Check functional dependencies
 	; case checkFunDeps (pkg_ie, home_ie) dfun of
@@ -577,13 +582,9 @@ addInst dflags home_ie dfun
 		Nothing    -> return ()
 
 		-- Check for duplicate instance decls
-		-- We instantiate the dfun type because the instance lookup
-		-- requires nice fresh types in the thing to be looked up
-	; (tvs', _, tenv) <- tcInstTyVars tvs
-	; let { tys' = substTys tenv tys
-	      ; (matches, _) = lookupInstEnv dflags (pkg_ie, home_ie) cls tys'
+	; let { (matches, _) = lookupInstEnv dflags (pkg_ie, home_ie) cls tys'
 	      ;	dup_dfuns = [dup_dfun | (_, (_, dup_tys, dup_dfun)) <- matches,
-			  		isJust (tcMatchTys (mkVarSet tvs) tys' dup_tys)] }
+			  		isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
 		-- Find memebers of the match list which 
 		-- dfun itself matches. If the match is 2-way, it's a duplicate
 	; case dup_dfuns of
@@ -591,7 +592,7 @@ addInst dflags home_ie dfun
 	    []           -> return ()
 
 		-- OK, now extend the envt
-	; return (extendInstEnv home_ie dfun) }
+	; return (extendInstEnv home_ie dfun') }
 
 
 traceDFuns dfuns
diff --git a/ghc/compiler/typecheck/TcArrows.lhs b/ghc/compiler/typecheck/TcArrows.lhs
index 2ddab4eeb9e2c5d7fe2e994ea3740191d706ee19..d45c7f3a2b15ae03f301e08458923daae341b0f7 100644
--- a/ghc/compiler/typecheck/TcArrows.lhs
+++ b/ghc/compiler/typecheck/TcArrows.lhs
@@ -19,7 +19,7 @@ import TcMatches ( TcStmtCtxt(..), tcMatchPats, matchCtxt, tcStmts,
 import TcType	( TcType, TcTauType, TcRhoType, mkFunTys, mkTyConApp,
 		  mkTyVarTy, mkAppTys, tcSplitTyConApp_maybe, tcEqType, 
 		  SkolemInfo(..) )
-import TcMType	( newTyFlexiVarTy, newTyFlexiVarTys, tcSkolTyVar, zonkTcType )
+import TcMType	( newTyFlexiVarTy, newTyFlexiVarTys, tcSkolTyVars, zonkTcType )
 import TcBinds	( tcBindsAndThen )
 import TcSimplify ( tcSimplifyCheck )
 import TcUnify	( Expected(..), checkSigTyVarsWrt, zapExpectedTo )
@@ -244,7 +244,7 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)
   = addErrCtxt (cmdCtxt cmd)	$
     do	{ cmds_w_tys <- zipWithM new_cmd_ty cmd_args [1..]
 	; span       <- getSrcSpanM
-	; w_tv       <- tcSkolTyVar (ArrowSkol span) alphaTyVar
+	; [w_tv]     <- tcSkolTyVars (ArrowSkol span) [alphaTyVar]
 	; let w_ty = mkTyVarTy w_tv 	-- Just a convenient starting point
 
 		--  a ((w,t1) .. tn) t
diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs
index ad5060b4c1a47ecc8dc0a7a003f41a35c3f85d6e..bd0e95c568d6ec070d8b55ab3a7d7758a4545b1a 100644
--- a/ghc/compiler/typecheck/TcBinds.lhs
+++ b/ghc/compiler/typecheck/TcBinds.lhs
@@ -21,16 +21,16 @@ import TcHsSyn		( TcId, TcDictBinds, zonkId, mkHsLet )
 
 import TcRnMonad
 import Inst		( InstOrigin(..), newDictsAtLoc, newIPDict, instToId )
-import TcEnv		( tcExtendIdEnv, tcExtendIdEnv2, newLocalName, tcLookupLocalIds )
+import TcEnv		( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv, newLocalName, tcLookupLocalIds )
 import TcUnify		( Expected(..), tcInfer, checkSigTyVars, sigCtxt )
 import TcSimplify	( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, 
 			  tcSimplifyToDicts, tcSimplifyIPs )
 import TcHsType		( tcHsSigType, UserTypeCtxt(..), tcAddLetBoundTyVars,
-			  TcSigInfo(..), TcSigFun, mkTcSig, lookupSig
+			  TcSigInfo(..), TcSigFun, lookupSig
 			)
 import TcPat		( tcPat, PatCtxt(..) )
 import TcSimplify	( bindInstsOfLocalFuns )
-import TcMType		( newTyFlexiVarTy, tcSkolType, zonkQuantifiedTyVar, zonkTcTypes )
+import TcMType		( newTyFlexiVarTy, tcSkolSigType, zonkQuantifiedTyVar, zonkTcTypes )
 import TcType		( TcTyVar, SkolemInfo(SigSkol), 
 			  TcTauType, TcSigmaType, 
 			  TvSubstEnv, mkTvSubst, substTheta, substTy, 
@@ -38,14 +38,13 @@ import TcType		( TcTyVar, SkolemInfo(SigSkol),
 			  mkForAllTy, isUnLiftedType, tcGetTyVar_maybe, 
 			  mkTyVarTys )
 import Unify		( tcMatchPreds )
-import Kind		( argTypeKind, isUnliftedTypeKind )
+import Kind		( argTypeKind )
 import VarEnv		( lookupVarEnv ) 
 import TysPrim		( alphaTyVar )
 import Id		( mkLocalId, mkSpecPragmaId, setInlinePragma )
 import Var		( idType, idName )
 import Name		( Name )
 import NameSet
-import Var		( tyVarKind )
 import VarSet
 import SrcLoc		( Located(..), unLoc, noLoc, getLoc )
 import Bag
@@ -435,22 +434,24 @@ tcMonoBinds :: LHsBinds Name
 	    -> TcSigFun -> RecFlag
 	    -> TcM (LHsBinds TcId, [MonoBindInfo])
 
-type MonoBindInfo = (Name, Maybe TcSigInfo, TcId)
-	-- Type signature (if any), and
-	-- the monomorphic bound things
-
-bndrNames :: [MonoBindInfo] -> [Name]
-bndrNames mbi = [n | (n,_,_) <- mbi]
-
-getMonoType :: MonoBindInfo -> TcTauType
-getMonoType (_,_,mono_id) = idType mono_id
-
 tcMonoBinds binds lookup_sig is_rec
   = do	{ tc_binds <- mapBagM (wrapLocM (tcLhs lookup_sig)) binds
-	; let mono_info = getMonoBindInfo tc_binds
-	; binds' <- tcExtendIdEnv2 (rhsEnvExtension mono_info) $
+
+	-- Bring (a) the scoped type variables, and (b) the Ids, into scope for the RHSs
+	-- For (a) it's ok to bring them all into scope at once, even
+	-- though each type sig should scope only over its own RHS,
+	-- because the renamer has sorted all that out.
+	; let mono_info  = getMonoBindInfo tc_binds
+	      rhs_tvs    = [ tv | (_, Just sig, _) <- mono_info, tv <- sig_tvs sig ]
+	      rhs_id_env = map mk mono_info 	-- A binding for each term variable
+
+	; binds' <- tcExtendTyVarEnv rhs_tvs    $
+		    tcExtendIdEnv2   rhs_id_env $
 		    mapBagM (wrapLocM tcRhs) tc_binds
 	; return (binds', mono_info) }
+   where
+    mk (name, Just sig, _)       = (name, sig_id sig)	-- Use the type sig if there is one
+    mk (name, Nothing,  mono_id) = (name, mono_id)	-- otherwise use a monomorphic version
 
 ------------------------
 -- tcLhs typechecks the LHS of the bindings, to construct the environment in which
@@ -472,6 +473,16 @@ data TcMonoBind		-- Half completed; LHS done, RHS not done
   = TcFunBind  MonoBindInfo  (Located TcId) Bool (MatchGroup Name) 
   | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name) TcSigmaType
 
+type MonoBindInfo = (Name, Maybe TcSigInfo, TcId)
+	-- Type signature (if any), and
+	-- the monomorphic bound things
+
+bndrNames :: [MonoBindInfo] -> [Name]
+bndrNames mbi = [n | (n,_,_) <- mbi]
+
+getMonoType :: MonoBindInfo -> TcTauType
+getMonoType (_,_,mono_id) = idType mono_id
+
 tcLhs :: TcSigFun -> HsBind Name -> TcM TcMonoBind
 tcLhs lookup_sig (FunBind (L nm_loc name) inf matches)
   = do	{ let mb_sig = lookup_sig name
@@ -505,7 +516,7 @@ tcLhs lookup_sig bind@(PatBind pat grhss _)
 
 -------------------
 tcRhs :: TcMonoBind -> TcM (HsBind TcId)
-tcRhs (TcFunBind _ fun'@(L _ mono_id) inf matches)
+tcRhs (TcFunBind info fun'@(L _ mono_id) inf matches)
   = do	{ matches' <- tcMatchesFun (idName mono_id) matches 
 				   (Check (idType mono_id))
 	; return (FunBind fun' inf matches') }
@@ -523,15 +534,6 @@ getMonoBindInfo tc_binds
   where
     get_info (TcFunBind info _ _ _)  rest = info : rest
     get_info (TcPatBind infos _ _ _) rest = infos ++ rest
-
----------------------
-rhsEnvExtension :: [MonoBindInfo] -> [(Name, TcId)]
--- Environment for RHS of definitions: use type sig if there is one
-rhsEnvExtension mono_info
-  = map mk mono_info
-  where
-    mk (name, Just sig, _)       = (name, sig_id sig)
-    mk (name, Nothing,  mono_id) = (name, mono_id)
 \end{code}
 
 
@@ -548,42 +550,47 @@ tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
 -- all the right hand sides agree a common vocabulary for their type
 -- constraints
 tcTySigs [] = return []
-tcTySigs (L span (Sig (L _ name) ty) : sigs)
-  = do  { 	-- Typecheck the first signature
-	; sigma1 <- setSrcSpan span $
-		    tcHsSigType (FunSigCtxt name) ty
-	; let id1 = mkLocalId name sigma1
-	; tc_sig1 <- mkTcSig id1
 
-	; tc_sigs <- mapM (tcTySig tc_sig1) sigs
-	; return (tc_sig1 : tc_sigs) }
+tcTySigs sigs
+  = do	{ (tc_sig1 : tc_sigs) <- mappM tcTySig sigs
+	; tc_sigs' 	      <- mapM (checkSigCtxt tc_sig1) tc_sigs
+        ; return (tc_sig1 : tc_sigs') }
 
-tcTySig sig1 (L span (Sig (L _ name) ty))
+tcTySig :: LSig Name -> TcM TcSigInfo
+tcTySig (L span (Sig (L _ name) ty))
   = setSrcSpan span		$
     do	{ sigma_ty <- tcHsSigType (FunSigCtxt name) ty
-	; (tvs, theta, tau) <- tcSkolType rigid_info sigma_ty
-	; let poly_id  = mkLocalId name sigma_ty
-	      bale_out = failWithTc $
-		         sigContextsErr (sig_id sig1) name sigma_ty 
+	; let rigid_info = SigSkol name
+	      poly_id    = mkLocalId name sigma_ty
+	; (tvs, theta, tau) <- tcSkolSigType rigid_info sigma_ty
+	; loc <- getInstLoc (SigOrigin rigid_info)
+	; return (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, 
+			      sig_theta = theta, sig_tau = tau, 
+			      sig_loc = loc }) }
 
-	-- Try to match the context of this signature with 
+checkSigCtxt :: TcSigInfo -> TcSigInfo -> TcM TcSigInfo
+checkSigCtxt sig1 sig@(TcSigInfo { sig_tvs = tvs, sig_theta = theta, sig_tau = tau })
+  = 	-- Try to match the context of this signature with 
 	-- that of the first signature
-	; case tcMatchPreds tvs theta (sig_theta sig1) of { 
-	    Nothing   -> bale_out
-	;   Just tenv -> do
-	; case check_tvs tenv tvs of
-	    Nothing   -> bale_out
-	    Just tvs' -> do {
-
-	  let subst  = mkTvSubst tenv
-	      theta' = substTheta subst theta
-	      tau'   = substTy subst tau
-	; loc <- getInstLoc (SigOrigin rigid_info)
-	; return (TcSigInfo { sig_id = poly_id, sig_tvs = tvs', 
-			      sig_theta = theta', sig_tau = tau', 
-			      sig_loc = loc }) }}}
+    case tcMatchPreds (sig_tvs sig) (sig_theta sig) (sig_theta sig1) of {
+	Nothing   -> bale_out ;
+	Just tenv ->
+
+    case check_tvs tenv tvs of {
+	Nothing   -> bale_out ;
+	Just tvs' -> 
+
+    let 
+	subst  = mkTvSubst tenv
+    in
+    return (sig { sig_tvs   = tvs', 
+		  sig_theta = substTheta subst theta, 
+		  sig_tau   = substTy subst tau }) }}
+
   where
-    rigid_info = SigSkol name
+    bale_out =	setSrcSpan (instLocSrcSpan (sig_loc sig)) $
+	 	failWithTc $
+		sigContextsErr (sig_id sig1) (sig_id sig)
 
 	-- Rather tedious check that the type variables
 	-- have been matched only with another type variable,
@@ -832,10 +839,10 @@ valSpecSigCtxt v ty
 	 nest 4 (ppr v <+> dcolon <+> ppr ty)]
 
 -----------------------------------------------
-sigContextsErr id1 name ty
+sigContextsErr id1 id2
   = vcat [ptext SLIT("Mis-match between the contexts of the signatures for"), 
 	  nest 2 (vcat [ppr id1 <+> dcolon <+> ppr (idType id1),
-			ppr name <+> dcolon <+> ppr ty]),
+			ppr id2 <+> dcolon <+> ppr (idType id2)]),
 	  ptext SLIT("The signature contexts in a mutually recursive group should all be identical")]
 
 
diff --git a/ghc/compiler/typecheck/TcClassDcl.lhs b/ghc/compiler/typecheck/TcClassDcl.lhs
index 17121754f70423c530b077671bc0a0686db9c27d..8b12865d592abc7ba6282b723516e11967a4a20c 100644
--- a/ghc/compiler/typecheck/TcClassDcl.lhs
+++ b/ghc/compiler/typecheck/TcClassDcl.lhs
@@ -20,7 +20,7 @@ import RnEnv		( lookupTopBndrRn, lookupImportedName )
 
 import Inst		( Inst, InstOrigin(..), instToId, newDicts, newDictsAtLoc, newMethod )
 import TcEnv		( tcLookupLocatedClass, tcExtendIdEnv2, 
-			  tcExtendTyVarEnv2,
+			  tcExtendTyVarEnv, 
 			  InstInfo(..), pprInstInfoDetails,
 			  simpleInstInfoTyCon, simpleInstInfoTy,
 			  InstBindings(..), newDFunName
@@ -29,7 +29,7 @@ import TcBinds		( tcMonoBinds, tcSpecSigs )
 import TcHsType		( TcSigInfo(..), mkTcSig, tcHsKindedType, tcHsSigType )
 import TcSimplify	( tcSimplifyCheck, bindInstsOfLocalFuns )
 import TcUnify		( checkSigTyVars, sigCtxt )
-import TcMType		( tcSkolTyVars, UserTypeCtxt( GenPatCtxt ) )
+import TcMType		( tcSkolSigTyVars, UserTypeCtxt( GenPatCtxt ) )
 import TcType		( Type, SkolemInfo(ClsSkol, InstSkol), 
 			  TcType, TcThetaType, TcTyVar, mkTyVarTys,
 			  mkClassPred, tcSplitSigmaTy, tcSplitFunTys,
@@ -51,7 +51,6 @@ import NameSet		( emptyNameSet, unitNameSet, nameSetToList )
 import OccName		( reportIfUnused, mkDefaultMethodOcc )
 import RdrName		( RdrName, mkDerivedRdrName )
 import Outputable
-import Var		( TyVar )
 import PrelNames	( genericTyConNames )
 import CmdLineOpts
 import UnicodeUtil	( stringToUtf8 )
@@ -263,19 +262,17 @@ tcClassDecl2 (L loc (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
     
 tcDefMeth clas tyvars binds_in prags sel_id
   = do	{ dm_name <- lookupTopBndrRn (mkDefMethRdrName sel_id)
-	; let rigid_info = ClsSkol clas
-	; clas_tyvars <- tcSkolTyVars rigid_info tyvars
-	; let
+	; let	rigid_info  = ClsSkol clas
+		clas_tyvars = tcSkolSigTyVars rigid_info tyvars
 		inst_tys    = mkTyVarTys clas_tyvars
 		dm_ty       = idType sel_id	-- Same as dict selector!
 	        theta       = [mkClassPred clas inst_tys]
 		local_dm_id = mkDefaultMethodId dm_name dm_ty
-		xtve 	    = tyvars `zip` clas_tyvars
 		origin 	    = SigOrigin rigid_info
 
 	; (_, meth_info) <- mkMethodBind origin clas inst_tys binds_in (sel_id, DefMeth)
 	; [this_dict] <- newDicts origin theta
-	; (defm_bind, insts_needed) <- getLIE (tcMethodBind xtve clas_tyvars theta 
+	; (defm_bind, insts_needed) <- getLIE (tcMethodBind clas_tyvars theta 
 							    [this_dict] prags meth_info)
     
 	; addErrCtxt (defltMethCtxt clas) $ do
@@ -322,11 +319,11 @@ type MethodSpec = (Id, 			-- Global selector Id
 		   LHsBind Name)	-- Binding for the method
 
 tcMethodBind 
-	:: [(TyVar,TcTyVar)]	-- Bindings for type environment
-	-> [TcTyVar]		-- Instantiated type variables for the
+	:: [TcTyVar]		-- Skolemised type variables for the
 				--  	enclosing class/instance decl. 
 				--  	They'll be signature tyvars, and we
 				--  	want to check that they don't get bound
+				-- Also they are scoped, so we bring them into scope
 				-- Always equal the range of the type envt
 	-> TcThetaType		-- Available theta; it's just used for the error message
 	-> [Inst]		-- Available from context, used to simplify constraints 
@@ -335,7 +332,7 @@ tcMethodBind
 	-> MethodSpec		-- Details of this method
 	-> TcM (LHsBinds Id)
 
-tcMethodBind xtve inst_tyvars inst_theta avail_insts prags
+tcMethodBind inst_tyvars inst_theta avail_insts prags
 	     (sel_id, meth_id, meth_bind)
   = recoverM (returnM emptyLHsBinds) $
 	-- If anything fails, recover returning no bindings.
@@ -349,7 +346,7 @@ tcMethodBind xtve inst_tyvars inst_theta avail_insts prags
      let lookup_sig name = ASSERT( name == idName meth_id ) 
 			   Just meth_sig
      in
-     tcExtendTyVarEnv2 xtve (
+     tcExtendTyVarEnv inst_tyvars (
 	addErrCtxt (methodCtxt sel_id)			$
 	getLIE 						$
 	tcMonoBinds (unitBag meth_bind) lookup_sig NonRecursive
diff --git a/ghc/compiler/typecheck/TcDeriv.lhs b/ghc/compiler/typecheck/TcDeriv.lhs
index a81f8fbfee289f7655e7daf54773fc278a31f69f..bc1fa9ace4f07264ac4ed36195663b893dcac8be 100644
--- a/ghc/compiler/typecheck/TcDeriv.lhs
+++ b/ghc/compiler/typecheck/TcDeriv.lhs
@@ -20,7 +20,7 @@ import TcEnv		( newDFunName, pprInstInfoDetails,
 			  tcLookupClass, tcLookupTyCon, tcExtendTyVarEnv
 			)
 import TcGenDeriv	-- Deriv stuff
-import InstEnv		( simpleDFunClassTyCon, extendInstEnv )
+import InstEnv		( simpleDFunClassTyCon, extendInstEnvList )
 import TcHsType		( tcHsDeriv )
 import TcSimplify	( tcSimplifyDeriv )
 
@@ -723,7 +723,7 @@ extendLocalInstEnv :: [DFunId] -> TcM a -> TcM a
 -- for functional dependency errors -- that'll happen in TcInstDcls
 extendLocalInstEnv dfuns thing_inside
  = do { env <- getGblEnv
-      ; let  inst_env' = foldl extendInstEnv (tcg_inst_env env) dfuns 
+      ; let  inst_env' = extendInstEnvList (tcg_inst_env env) dfuns 
 	     env'      = env { tcg_inst_env = inst_env' }
       ; setGblEnv env' thing_inside }
 \end{code}
diff --git a/ghc/compiler/typecheck/TcEnv.lhs b/ghc/compiler/typecheck/TcEnv.lhs
index 50f5c2b10697dd4cfe9c50ed4c8cf62fd0d098bb..967e3c33b6e02a67936c0d71e1304974c1dfff33 100644
--- a/ghc/compiler/typecheck/TcEnv.lhs
+++ b/ghc/compiler/typecheck/TcEnv.lhs
@@ -17,7 +17,7 @@ module TcEnv(
 	
 	-- Local environment
 	tcExtendKindEnv,
-	tcExtendTyVarEnv, tcExtendTyVarEnv2, tcExtendTyVarEnv3, 
+	tcExtendTyVarEnv, tcExtendTyVarEnv3, 
 	tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2, 
 	tcLookup, tcLookupLocated, tcLookupLocalIds,
 	tcLookupId, tcLookupTyVar,
@@ -250,10 +250,6 @@ tcExtendTyVarEnv :: [TyVar] -> TcM r -> TcM r
 tcExtendTyVarEnv tvs thing_inside
   = tc_extend_tv_env [ATyVar tv (mkTyVarTy tv) | tv <- tvs] thing_inside
 
-tcExtendTyVarEnv2 :: [(TyVar,TcTyVar)] -> TcM r -> TcM r
-tcExtendTyVarEnv2 tv_pairs thing_inside
-  = tc_extend_tv_env [ATyVar tv1 (mkTyVarTy tv2) | (tv1,tv2) <- tv_pairs] thing_inside
-
 tcExtendTyVarEnv3 :: [(TyVar,TcType)] -> TcM r -> TcM r
 tcExtendTyVarEnv3 ty_pairs thing_inside
   = tc_extend_tv_env [ATyVar tv1 ty2 | (tv1,ty2) <- ty_pairs] thing_inside
@@ -559,8 +555,8 @@ as well as explicit user written ones.
 \begin{code}
 data InstInfo
   = InstInfo {
-      iDFunId :: DFunId,		-- The dfun id
-      iBinds  :: InstBindings
+      iDFunId :: DFunId,		-- The dfun id.  Its forall'd type variables 
+      iBinds  :: InstBindings		-- scope over the stuff in InstBindings!
     }
 
 data InstBindings
diff --git a/ghc/compiler/typecheck/TcHsType.lhs b/ghc/compiler/typecheck/TcHsType.lhs
index e25d0ad0896f6101b2d4679a4b20c97c86a4e426..04aa6868cbdccd2ee9e104c747c281c728af31be 100644
--- a/ghc/compiler/typecheck/TcHsType.lhs
+++ b/ghc/compiler/typecheck/TcHsType.lhs
@@ -41,8 +41,7 @@ import TcUnify		( unifyFunKind, checkExpectedKind )
 import TcType		( Type, PredType(..), ThetaType, 
 			  SkolemInfo(SigSkol), MetaDetails(Flexi),
 			  TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
-			  mkTyVarTy, mkFunTy, 
-		 	  mkForAllTys, mkFunTys, tcEqType, isPredTy,
+		 	  mkForAllTys, mkFunTys, tcEqType, isPredTy, mkFunTy, 
 			  mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, 
 			  tcSplitFunTy_maybe, tcSplitForAllTys )
 import Kind 		( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, 
diff --git a/ghc/compiler/typecheck/TcInstDcls.lhs b/ghc/compiler/typecheck/TcInstDcls.lhs
index 6049fe598c4f46840faa9c140fa0ec8db01ec7ae..afada00b16645d956664d20871b6afd2e8dbdc8c 100644
--- a/ghc/compiler/typecheck/TcInstDcls.lhs
+++ b/ghc/compiler/typecheck/TcInstDcls.lhs
@@ -13,14 +13,14 @@ import TcBinds		( tcSpecSigs )
 import TcClassDcl	( tcMethodBind, mkMethodBind, badMethodErr, 
 			  tcClassDecl2, getGenericInstances )
 import TcRnMonad       
-import TcMType		( tcSkolType, checkValidTheta, checkValidInstHead, instTypeErr, 
+import TcMType		( tcSkolSigType, checkValidTheta, checkValidInstHead, instTypeErr, 
 			  checkAmbiguity, SourceTyCtxt(..) )
-import TcType		( mkClassPred, tcSplitForAllTys, tyVarsOfType, 
-			  tcSplitSigmaTy, getClassPredTys, tcSplitPredTy_maybe, mkTyVarTys,
+import TcType		( mkClassPred, tyVarsOfType, 
+			  tcSplitSigmaTy, getClassPredTys, tcSplitDFunHead, mkTyVarTys,
 			  SkolemInfo(InstSkol), tcSplitDFunTy, pprClassPred )
 import Inst		( tcInstClassOp, newDicts, instToId, showLIE, tcExtendLocalInstEnv )
 import TcDeriv		( tcDeriving )
-import TcEnv		( tcExtendGlobalValEnv, tcExtendTyVarEnv2,
+import TcEnv		( tcExtendGlobalValEnv, tcExtendTyVarEnv,
  			  InstInfo(..), InstBindings(..), 
 			  newDFunName, tcExtendIdEnv
 			)
@@ -313,20 +313,18 @@ tcInstDecl2 (InstInfo { iDFunId = dfun_id, iBinds = binds })
     recoverM (returnM emptyLHsBinds)		$
     setSrcSpan (srcLocSpan (getSrcLoc dfun_id))	$
     addErrCtxt (instDeclCtxt2 (idType dfun_id))	$
+
+	-- Instantiate the instance decl with skolem constants 
     let
-	rigid_info	 = InstSkol dfun_id
-	inst_ty 	 = idType dfun_id
-	(inst_tyvars, _) = tcSplitForAllTys inst_ty
-		-- The tyvars of the instance decl scope over the 'where' part
+	rigid_info = InstSkol dfun_id
+	inst_ty    = idType dfun_id
+    in
+    tcSkolSigType rigid_info inst_ty	`thenM` \ (inst_tyvars', dfun_theta', inst_head') ->
+		-- These inst_tyvars' scope over the 'where' part
 		-- Those tyvars are inside the dfun_id's type, which is a bit
 		-- bizarre, but OK so long as you realise it!
-    in
-
-	-- Instantiate the instance decl with tc-style type variables
-    tcSkolType rigid_info inst_ty	`thenM` \ (inst_tyvars', dfun_theta', inst_head') ->
     let
-	Just pred         = tcSplitPredTy_maybe inst_head'
-	(clas, inst_tys') = getClassPredTys pred
+	(clas, inst_tys') = tcSplitDFunHead inst_head'
         (class_tyvars, sc_theta, _, op_items) = classBigSig clas
 
         -- Instantiate the super-class context with inst_tys
@@ -334,9 +332,9 @@ tcInstDecl2 (InstInfo { iDFunId = dfun_id, iBinds = binds })
 	origin	  = SigOrigin rigid_info
     in
 	 -- Create dictionary Ids from the specified instance contexts.
-    newDicts InstScOrigin sc_theta'	`thenM` \ sc_dicts ->
-    newDicts origin dfun_theta'		`thenM` \ dfun_arg_dicts ->
-    newDicts origin [pred] 		`thenM` \ [this_dict] ->
+    newDicts InstScOrigin sc_theta'			`thenM` \ sc_dicts ->
+    newDicts origin dfun_theta'				`thenM` \ dfun_arg_dicts ->
+    newDicts origin [mkClassPred clas inst_tys'] 	`thenM` \ [this_dict] ->
 		-- Default-method Ids may be mentioned in synthesised RHSs,
 		-- but they'll already be in the environment.
 
@@ -345,7 +343,7 @@ tcInstDecl2 (InstInfo { iDFunId = dfun_id, iBinds = binds })
     let		-- These insts are in scope; quite a few, eh?
 	avail_insts = [this_dict] ++ dfun_arg_dicts ++ sc_dicts
     in
-    tcMethods origin clas inst_tyvars inst_tyvars' 
+    tcMethods origin clas inst_tyvars' 
 	      dfun_theta' inst_tys' avail_insts 
 	      op_items binds		`thenM` \ (meth_ids, meth_binds) ->
 
@@ -364,10 +362,9 @@ tcInstDecl2 (InstInfo { iDFunId = dfun_id, iBinds = binds })
 		       other		    -> []
 	spec_prags = [ L loc (SpecSig (L loc (idName dfun_id)) ty)
 		     | L loc (SpecInstSig ty) <- uprags ]
-	xtve = inst_tyvars `zip` inst_tyvars'
     in
     tcExtendGlobalValEnv [dfun_id] (
-	tcExtendTyVarEnv2 xtve		$
+	tcExtendTyVarEnv inst_tyvars'	$
 	tcSpecSigs spec_prags
     )					`thenM` \ prag_binds ->
 
@@ -428,7 +425,7 @@ tcInstDecl2 (InstInfo { iDFunId = dfun_id, iBinds = binds })
 	     sc_binds_outer)
 
 
-tcMethods origin clas inst_tyvars inst_tyvars' dfun_theta' inst_tys' 
+tcMethods origin clas inst_tyvars' dfun_theta' inst_tys' 
 	  avail_insts op_items (VanillaInst monobinds uprags)
   = 	-- Check that all the method bindings come from this class
     let
@@ -474,8 +471,7 @@ tcMethods origin clas inst_tyvars inst_tyvars' dfun_theta' inst_tys'
 	-- looks like 'op at Int'.  But they are not the same.
     let
 	all_insts      = avail_insts ++ catMaybes meth_insts
-	xtve	       = inst_tyvars `zip` inst_tyvars'
-	tc_method_bind = tcMethodBind xtve inst_tyvars' dfun_theta' all_insts uprags 
+	tc_method_bind = tcMethodBind inst_tyvars' dfun_theta' all_insts uprags 
 	meth_ids       = [meth_id | (_,meth_id,_) <- meth_infos]
     in
 
@@ -485,7 +481,7 @@ tcMethods origin clas inst_tyvars inst_tyvars' dfun_theta' inst_tys'
 
 
 -- Derived newtype instances
-tcMethods origin clas inst_tyvars inst_tyvars' dfun_theta' inst_tys' 
+tcMethods origin clas inst_tyvars' dfun_theta' inst_tys' 
 	  avail_insts op_items (NewTypeDerived rep_tys)
   = getInstLoc origin				`thenM` \ inst_loc ->
     mapAndUnzip3M (do_one inst_loc) op_items	`thenM` \ (meth_ids, meth_binds, rhs_insts) ->
@@ -512,8 +508,11 @@ tcMethods origin clas inst_tyvars inst_tyvars' dfun_theta' inst_tys'
 	  return (meth_id, noLoc (VarBind meth_id (nlHsVar (instToId rhs_inst))), rhs_inst)
 
 	-- Instantiate rep_tys with the relevant type variables
+	-- This looks a bit odd, because inst_tyvars' are the skolemised version
+	-- of the type variables in the instance declaration; but rep_tys doesn't
+	-- have the skolemised version, so we substitute them in here
     rep_tys' = substTys subst rep_tys
-    subst    = zipTvSubst inst_tyvars (mkTyVarTys inst_tyvars')
+    subst    = zipTvSubst inst_tyvars' (mkTyVarTys inst_tyvars')
 \end{code}
 
 Note: [Superclass loops]
diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index 09bbc26fbd3aeb721bbc7c946843b492072d6740..4db7ae39e1d5203fd3625f5477f4c6b5b089288d 100644
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -21,7 +21,8 @@ module TcMType (
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 
-  tcSkolTyVar, tcSkolTyVars, tcSkolType,
+  tcSkolType, tcSkolTyVars,
+  tcSkolSigType, tcSkolSigTyVars,
 
   --------------------------------
   -- Checking type validity
@@ -80,6 +81,7 @@ import Name		( Name, setNameUnique, mkSysTvName )
 import VarSet
 import VarEnv
 import CmdLineOpts	( dopt, DynFlag(..) )
+import UniqSupply	( uniqsFromSupply )
 import Util		( nOfThem, isSingleton, equalLength, notNull )
 import ListSetOps	( removeDups )
 import SrcLoc		( unLoc )
@@ -185,49 +187,57 @@ tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- tcInstType instantiates the outer-level for-alls of a TcType with
 -- fresh (mutable) type variables, splits off the dictionary part, 
 -- and returns the pieces.
-tcInstType ty
-  = case tcSplitForAllTys ty of
-	([],     rho) -> 	-- There may be overloading despite no type variables;
-				-- 	(?x :: Int) => Int -> Int
-			 let
-			   (theta, tau) = tcSplitPhiTy rho
-			 in
-			 returnM ([], theta, tau)
+tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
 
-	(tyvars, rho) -> tcInstTyVars tyvars		`thenM` \ (tyvars', _, tenv) ->
-			 let
-			   (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-			 in
-			 returnM (tyvars', theta, tau)
 
 ---------------------------------------------
--- Similar functions but for skolem constants
+tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
 
 tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcSkolTyVars info tyvars = mappM (tcSkolTyVar info) tyvars
-  
-tcSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcSkolTyVar info tyvar
-  = do	{ uniq <- newUnique
-	; let name = setNameUnique (tyVarName tyvar) uniq
-		-- See Note [TyVarName]
-	; return (mkTcTyVar name (tyVarKind tyvar) 
-			    (SkolemTv info)) }
+tcSkolTyVars info tyvars
+  = do	{ us <- newUniqueSupply
+	; return (zipWith skol_tv tyvars (uniqsFromSupply us)) }
+  where
+    skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq)
+				(tyVarKind tv) (SkolemTv info)
+	-- See Note [TyVarName]
+			    
 
-tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-tcSkolType info ty
+---------------------------------------------
+tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants, but 
+-- do *not* give them fresh names, because we want the name to
+-- be in the type environment -- it is lexically scoped.
+tcSkolSigType info ty
+  = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+
+tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info) 
+			      | tv <- tyvars ]
+
+-----------------------
+tc_inst_type :: ([TyVar] -> TcM [TcTyVar]) 		-- How to instantiate the type variables
+	     -> TcType 					-- Type to instantiate
+	     -> TcM ([TcTyVar], TcThetaType, TcType)	-- Result
+tc_inst_type inst_tyvars ty
   = case tcSplitForAllTys ty of
-	([],     rho) -> let
+	([],     rho) -> let	-- There may be overloading despite no type variables;
+				-- 	(?x :: Int) => Int -> Int
 			   (theta, tau) = tcSplitPhiTy rho
 			 in
-			 returnM ([], theta, tau)
+			 return ([], theta, tau)
 
-	(tyvars, rho) -> tcSkolTyVars info tyvars	`thenM` \ tyvars' ->
-			 let
-			   tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
-			   (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-			 in
-			 returnM (tyvars', theta, tau)
+	(tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
+
+			    ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+				-- Either the tyvars are freshly made, by inst_tyvars,
+				-- or (in the call from tcSkolSigType) any nested foralls
+				-- have different binders.  Either way, zipTopTvSubst is ok
+
+			    ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+			    ; return (tyvars', theta, tau) }
 \end{code}
 
 
diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs
index 2d84f05036937291fb6235dcd000ec6bdb0ba84f..51d68bb9fd946a073ac5498616cf56f8708be74c 100644
--- a/ghc/compiler/typecheck/TcPat.lhs
+++ b/ghc/compiler/typecheck/TcPat.lhs
@@ -42,7 +42,7 @@ import DataCon		( DataCon, dataConTyCon, isVanillaDataCon, dataConInstOrigArgTys
 import PrelNames	( eqStringName, eqName, geName, negateName, minusName, 
 			  integralClassName )
 import BasicTypes	( isBoxed )
-import SrcLoc		( Located(..), SrcSpan, noLoc, unLoc, getLoc )
+import SrcLoc		( Located(..), SrcSpan, noLoc, unLoc )
 import Maybes		( catMaybes )
 import ErrUtils		( Message )
 import Outputable
diff --git a/ghc/compiler/typecheck/TcRnMonad.lhs b/ghc/compiler/typecheck/TcRnMonad.lhs
index d6227abea0c5a2c8a2e994121c719889b74e4125..88a2e6940ce7c54f778d1f06816cfa0ea5f1bd40 100644
--- a/ghc/compiler/typecheck/TcRnMonad.lhs
+++ b/ghc/compiler/typecheck/TcRnMonad.lhs
@@ -23,7 +23,7 @@ import RdrName		( GlobalRdrEnv, emptyGlobalRdrEnv,
 import Name		( Name, isInternalName )
 import Type		( Type )
 import NameEnv		( extendNameEnvList )
-import InstEnv		( InstEnv, emptyInstEnv, extendInstEnv )
+import InstEnv		( InstEnv, emptyInstEnv, extendInstEnvList )
 
 import VarSet		( emptyVarSet )
 import VarEnv		( TidyEnv, emptyTidyEnv, emptyVarEnv )
@@ -85,7 +85,7 @@ initTc hsc_env mod do_this
 		tcg_default  = Nothing,
 		tcg_type_env = emptyNameEnv,
 		tcg_type_env_var = type_env_var,
-		tcg_inst_env  = mkImpInstEnv hsc_env,
+		tcg_inst_env  = mkHomePackageInstEnv hsc_env,
 		tcg_inst_uses = dfuns_var,
 		tcg_th_used   = th_var,
 		tcg_exports  = emptyNameSet,
@@ -145,15 +145,15 @@ initTcPrintErrors env mod todo = do
   printErrorsAndWarnings msgs
   return res
 
-mkImpInstEnv :: HscEnv -> InstEnv
+mkHomePackageInstEnv :: HscEnv -> InstEnv
 -- At the moment we (wrongly) build an instance environment from all the
 -- home-package modules we have already compiled.
 -- We should really only get instances from modules below us in the 
 -- module import tree.
-mkImpInstEnv (HscEnv {hsc_dflags = dflags, hsc_HPT = hpt})
+mkHomePackageInstEnv (HscEnv {hsc_HPT = hpt})
   = foldModuleEnv (add . md_insts . hm_details) emptyInstEnv hpt
   where
-    add dfuns inst_env = foldl extendInstEnv inst_env dfuns
+    add dfuns inst_env = extendInstEnvList inst_env dfuns
 
 -- mkImpTypeEnv makes the imported symbol table
 mkImpTypeEnv :: ExternalPackageState -> HomePackageTable
diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 93ba1311c0e5b9002fc5b1abb3119a6f0c74ee7f..0c3c6319d05f0bae95cb9eda39a546c5668de5d4 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -60,7 +60,7 @@ module TcType (
   getClassPredTys_maybe, getClassPredTys, 
   isClassPred, isTyVarClassPred, 
   mkDictTy, tcSplitPredTy_maybe, 
-  isPredTy, isDictTy, tcSplitDFunTy, predTyUnique, 
+  isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
   mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
 
   ---------------------------------
@@ -485,9 +485,14 @@ tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
 -- Split the type of a dictionary function
 tcSplitDFunTy ty 
-  = case tcSplitSigmaTy ty       of { (tvs, theta, tau) ->
-    case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) -> 
+  = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
+    case tcSplitDFunHead tau of { (clas, tys) -> 
     (tvs, theta, clas, tys) }}
+
+tcSplitDFunHead :: Type -> (Class, [Type])
+tcSplitDFunHead tau  
+  = case tcSplitPredTy_maybe tau of 
+	Just (ClassP clas tys) -> (clas, tys)
 \end{code}
 
 
diff --git a/ghc/compiler/types/InstEnv.lhs b/ghc/compiler/types/InstEnv.lhs
index cc1c4453fe23bd260da9bf3aa45ccf5960869e8f..d0877c4627829ceeb635ccd4da9445c23c6cb530 100644
--- a/ghc/compiler/types/InstEnv.lhs
+++ b/ghc/compiler/types/InstEnv.lhs
@@ -9,7 +9,7 @@ The bits common to TcInstDcls and TcDeriv.
 module InstEnv (
 	DFunId, InstEnv,
 
-	emptyInstEnv, extendInstEnv,
+	emptyInstEnv, extendInstEnv, extendInstEnvList,
 	lookupInstEnv, instEnvElts,
 	classInstances, simpleDFunClassTyCon, checkFunDeps
     ) where
@@ -69,6 +69,9 @@ classInstances (pkg_ie, home_ie) cls
 		Just (ClsIE insts _) -> insts
 		Nothing		     -> []
 
+extendInstEnvList :: InstEnv -> [DFunId] -> InstEnv
+extendInstEnvList inst_env dfuns = foldl extendInstEnv inst_env dfuns
+
 extendInstEnv :: InstEnv -> DFunId -> InstEnv
 extendInstEnv inst_env dfun_id
   = addToUFM_C add inst_env clas (ClsIE [ins_item] ins_tyvar)
diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs
index 004d003c00a1cda879ab1d37dd7592677a6fcc6c..a8b893c9250b9870a7dcf74a59b35c4c67659b22 100644
--- a/ghc/compiler/types/Unify.lhs
+++ b/ghc/compiler/types/Unify.lhs
@@ -13,7 +13,6 @@ module Unify (
 
 #include "HsVersions.h"
 
-import Type		( pprParendType )
 import Var		( Var, TyVar, tyVarKind )
 import VarEnv
 import VarSet
@@ -100,7 +99,7 @@ tcMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2	-- Rename for export
 Now the internals of matching
 
 \begin{code}
-match :: MatchEnv	-- For the ost part this is pushed downwards
+match :: MatchEnv	-- For the most part this is pushed downwards
       -> TvSubstEnv 	-- Substitution so far:
 			--   Domain is subset of template tyvars
 			--   Free vars of range is subset of 
@@ -118,6 +117,8 @@ match menv subst (TyVarTy tv1) ty2
   = case lookupVarEnv subst tv1' of
 	Nothing | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 		-> Nothing	-- Occurs check
+		| not (typeKind ty2 `isSubKind` tyVarKind tv1)
+		-> Nothing	-- Kind mis-match
 		| otherwise
 		-> Just (extendVarEnv subst tv1 ty2)
 
diff --git a/ghc/docs/users_guide/flags.xml b/ghc/docs/users_guide/flags.xml
index ee3f19bef37c5ac4801e2abf9308bff4c5abab6b..a148fce58ab7a63fc17bdeda97401d6628ba7711 100644
--- a/ghc/docs/users_guide/flags.xml
+++ b/ghc/docs/users_guide/flags.xml
@@ -495,7 +495,8 @@
 	    </row>
 	    <row>
 	      <entry><option>-fimplicit-params</option></entry>
-	      <entry>Enable Implicit Parameters</entry>
+	      <entry>Enable Implicit Parameters.
+	      Implied by <option>-fglasgow-exts</option>.</entry>
 	      <entry>dynamic</entry>
 	      <entry><option>-fno-implicit-params</option></entry>
 	    </row>
@@ -517,9 +518,17 @@
 	      <entry>dynamic</entry>
 	      <entry><option>-fmonomorphism-restriction</option></entry>
 	    </row>
+	    <row>
+	      <entry><option>-fscoped-type-variables</option></entry>
+	      <entry>Enable lexically-scoped type variables.
+	      Implied by <option>-fglasgow-exts</option>.</entry>
+	      <entry>dynamic</entry>
+	      <entry><option>-fno-scoped-type-variables</option></entry>
+	    </row>
 	    <row>
 	      <entry><option>-fth</option></entry>
-	      <entry>Enable Template Haskell</entry>
+	      <entry>Enable Template Haskell. 
+		Implied by <option>-fglasgow-exts</option>.</entry>
 	      <entry>dynamic</entry>
 	      <entry><option>-fno-th</option></entry>
 	    </row>
diff --git a/ghc/docs/users_guide/glasgow_exts.xml b/ghc/docs/users_guide/glasgow_exts.xml
index d058119da0e69bea994a76027e8a3b9e72a6d11b..da22a151743b0aff5c7017c34c3b242ea22cb9e1 100644
--- a/ghc/docs/users_guide/glasgow_exts.xml
+++ b/ghc/docs/users_guide/glasgow_exts.xml
@@ -218,6 +218,28 @@ documentation</ulink> describes all the libraries that come with GHC.
 	</listitem>
       </varlistentry>
 
+      <varlistentry>
+	<term><option>-fimplicit-params</option></term>
+	<listitem>
+	  <para>Enables implicit parameters (see <xref
+	  linkend="implicit-parameters"/>).  Currently also implied by 
+	  <option>-fglasgow-exts</option>.</para>
+
+	  <para>Syntax stolen:
+	  <literal>?<replaceable>varid</replaceable></literal>,
+	  <literal>%<replaceable>varid</replaceable></literal>.</para>
+	</listitem>
+      </varlistentry>
+
+      <varlistentry>
+	<term><option>-fscoped-type-variables</option></term>
+	<listitem>
+	  <para>Enables lexically-scoped type variables (see <xref
+	  linkend="scoped-type-variables"/>).  Implied by
+	  <option>-fglasgow-exts</option>.</para>
+	</listitem>
+      </varlistentry>
+
       <varlistentry>
 	<term><option>-fth</option></term>
 	<listitem>
@@ -233,19 +255,6 @@ documentation</ulink> describes all the libraries that come with GHC.
 	</listitem>
       </varlistentry>
 
-      <varlistentry>
-	<term><option>-fimplicit-params</option></term>
-	<listitem>
-	  <para>Enables implicit parameters (see <xref
-	  linkend="implicit-parameters"/>).  Currently also implied by 
-	  <option>-fglasgow-exts</option>.</para>
-
-	  <para>Syntax stolen:
-	  <literal>?<replaceable>varid</replaceable></literal>,
-	  <literal>%<replaceable>varid</replaceable></literal>.</para>
-	</listitem>
-      </varlistentry>
-
     </variablelist>
   </sect1>