diff --git a/ghc/compiler/Makefile b/ghc/compiler/Makefile
index 47b0d31a3ef1a77c73831a81cc6ffec5bf3a9d0d..724cbbcddbb857ecdda956a885fbb0bd27f9d1ed 100644
--- a/ghc/compiler/Makefile
+++ b/ghc/compiler/Makefile
@@ -1,5 +1,5 @@
 # -----------------------------------------------------------------------------
-# $Id: Makefile,v 1.82 2000/07/07 09:37:39 simonmar Exp $
+# $Id: Makefile,v 1.83 2000/07/14 08:17:36 simonpj Exp $
 
 TOP = ..
 include $(TOP)/mk/boilerplate.mk
@@ -107,7 +107,7 @@ space:= $(empty) $(empty)
 SRC_HC_OPTS += \
   -cpp -fglasgow-exts -Rghc-timing \
   -I. -IcodeGen -InativeGen -Iparser \
-  -i$(subst $(space),:,$(DIRS))
+  -i$(subst $(space),:,$(DIRS)) 
 
 SRC_CC_OPTS += -Iparser -I. -I$(TOP)/includes -O
 
diff --git a/ghc/compiler/basicTypes/MkId.lhs b/ghc/compiler/basicTypes/MkId.lhs
index 69ba8af2884a69f5429974b9915a37160c9f827d..3504caac3f07f2dcc6983c49d77f07976a2d01de 100644
--- a/ghc/compiler/basicTypes/MkId.lhs
+++ b/ghc/compiler/basicTypes/MkId.lhs
@@ -321,8 +321,8 @@ mkDataConWrapId data_con
 		MarkedUnboxed con tys ->
 		   Case (Var arg) arg [(DataAlt con, con_args,
 					body i' (reverse con_args++rep_args))]
-		   where n_tys = length tys
-			 (con_args,i') = mkLocals i tys
+		   where 
+			(con_args,i') = mkLocals i tys
 \end{code}
 
 
@@ -381,7 +381,6 @@ mkRecordSelId tycon field_label unpack_id
     sel_id     = mkId (fieldLabelName field_label) selector_ty info
 
     field_ty   = fieldLabelType field_label
-    field_name = fieldLabelName field_label
     data_cons  = tyConDataCons tycon
     tyvars     = tyConTyVars tycon	-- These scope over the types in 
 					-- the FieldLabels of constructors of this type
@@ -573,15 +572,15 @@ mkDictFunId :: Name		-- Name to use for the dict fun;
 mkDictFunId dfun_name clas inst_tyvars inst_tys inst_decl_theta
   = mkVanillaId dfun_name dfun_ty
   where
-    (class_tyvars, sc_theta, _, _) = classBigSig clas
-    sc_theta' = substClasses (mkTopTyVarSubst class_tyvars inst_tys) sc_theta
-
     dfun_theta = classesToPreds inst_decl_theta
 
 {-  1 dec 99: disable the Mark Jones optimisation for the sake
     of compatibility with Hugs.
     See `types/InstEnv' for a discussion related to this.
 
+    (class_tyvars, sc_theta, _, _) = classBigSig clas
+    not_const (clas, tys) = not (isEmptyVarSet (tyVarsOfTypes tys))
+    sc_theta' = substClasses (mkTopTyVarSubst class_tyvars inst_tys) sc_theta
     dfun_theta = case inst_decl_theta of
 		   []    -> []	-- If inst_decl_theta is empty, then we don't
 				-- want to have any dict arguments, so that we can
@@ -603,8 +602,6 @@ mkDictFunId dfun_name clas inst_tyvars inst_tys inst_decl_theta
 				-- Now sc_theta' has Foo T
 -}
     dfun_ty = mkSigmaTy inst_tyvars dfun_theta (mkDictTy clas inst_tys)
-
-    not_const (clas, tys) = not (isEmptyVarSet (tyVarsOfTypes tys))
 \end{code}
 
 
diff --git a/ghc/compiler/basicTypes/Name.lhs b/ghc/compiler/basicTypes/Name.lhs
index ff8096a9298862f0586d258cf02eeac320eee2bc..7ee54d5a0bfa206612bcebccb1cdfa3e3cb1302a 100644
--- a/ghc/compiler/basicTypes/Name.lhs
+++ b/ghc/compiler/basicTypes/Name.lhs
@@ -30,11 +30,11 @@ module Name (
 	isSystemName, isLocalName, isGlobalName, isExternallyVisibleName,
 	
 	-- Environment
-	NameEnv,
+	NameEnv, mkNameEnv,
 	emptyNameEnv, unitNameEnv, nameEnvElts, 
-	addToNameEnv_C, addToNameEnv, addListToNameEnv,
-	plusNameEnv, plusNameEnv_C, extendNameEnv, 
-	lookupNameEnv, delFromNameEnv, elemNameEnv, 
+	extendNameEnv_C, extendNameEnv, 
+	plusNameEnv, plusNameEnv_C, extendNameEnv, extendNameEnvList,
+	lookupNameEnv, lookupNameEnv_NF, delFromNameEnv, elemNameEnv, 
 
 
 	-- Provenance
@@ -59,6 +59,7 @@ import CmdLineOpts	( opt_Static, opt_PprStyle_NoPrags, opt_OmitInterfacePragmas,
 
 import SrcLoc		( noSrcLoc, mkBuiltinSrcLoc, SrcLoc )
 import Unique		( pprUnique, Unique, Uniquable(..), hasKey, unboundKey, u2i )
+import Maybes		( expectJust )
 import UniqFM
 import Outputable
 import GlaExts
@@ -552,30 +553,33 @@ instance NamedThing Name where
 type NameEnv a = UniqFM a	-- Domain is Name
 
 emptyNameEnv   	 :: NameEnv a
+mkNameEnv	 :: [(Name,a)] -> NameEnv a
 nameEnvElts    	 :: NameEnv a -> [a]
-addToNameEnv_C 	 :: (a->a->a) -> NameEnv a -> Name -> a -> NameEnv a
-addToNameEnv   	 :: NameEnv a -> Name -> a -> NameEnv a
-addListToNameEnv :: NameEnv a -> [(Name,a)] -> NameEnv a
+extendNameEnv_C  :: (a->a->a) -> NameEnv a -> Name -> a -> NameEnv a
+extendNameEnv  	 :: NameEnv a -> Name -> a -> NameEnv a
 plusNameEnv    	 :: NameEnv a -> NameEnv a -> NameEnv a
 plusNameEnv_C  	 :: (a->a->a) -> NameEnv a -> NameEnv a -> NameEnv a
-extendNameEnv  	 :: NameEnv a -> [(Name,a)] -> NameEnv a
-lookupNameEnv  	 :: NameEnv a -> Name -> Maybe a
+extendNameEnvList:: NameEnv a -> [(Name,a)] -> NameEnv a
 delFromNameEnv 	 :: NameEnv a -> Name -> NameEnv a
 elemNameEnv    	 :: Name -> NameEnv a -> Bool
 unitNameEnv    	 :: Name -> a -> NameEnv a
+lookupNameEnv  	 :: NameEnv a -> Name -> Maybe a
+lookupNameEnv_NF :: NameEnv a -> Name -> a
 
 emptyNameEnv   	 = emptyUFM
+mkNameEnv	 = listToUFM
 nameEnvElts    	 = eltsUFM
-addToNameEnv_C 	 = addToUFM_C
-addToNameEnv   	 = addToUFM
-addListToNameEnv = addListToUFM
+extendNameEnv_C  = addToUFM_C
+extendNameEnv  	 = addToUFM
 plusNameEnv    	 = plusUFM
 plusNameEnv_C  	 = plusUFM_C
-extendNameEnv  	 = addListToUFM
-lookupNameEnv  	 = lookupUFM
+extendNameEnvList= addListToUFM
 delFromNameEnv 	 = delFromUFM
 elemNameEnv    	 = elemUFM
 unitNameEnv    	 = unitUFM
+
+lookupNameEnv  	       = lookupUFM
+lookupNameEnv_NF env n = expectJust "lookupNameEnv_NF" (lookupUFM env n)
 \end{code}
 
 
diff --git a/ghc/compiler/basicTypes/VarEnv.lhs b/ghc/compiler/basicTypes/VarEnv.lhs
index 0cd670e3b55dbaca4a219bc9d464e4ff1df203a2..f8783f4e1bf990eb79950a182fc2d0acbc258c6d 100644
--- a/ghc/compiler/basicTypes/VarEnv.lhs
+++ b/ghc/compiler/basicTypes/VarEnv.lhs
@@ -142,6 +142,7 @@ foldVarEnv	  :: (a -> b -> b) -> b -> VarEnv a -> b
 \begin{code}
 elemVarEnv       = elemUFM
 extendVarEnv	 = addToUFM
+extendVarEnvList = addListToUFM
 plusVarEnv_C	 = plusUFM_C
 delVarEnvList	 = delListFromUFM
 delVarEnv	 = delFromUFM
@@ -156,8 +157,7 @@ unitVarEnv	 = unitUFM
 isEmptyVarEnv	 = isNullUFM
 foldVarEnv	 = foldUFM
 
-zipVarEnv tyvars tys       = listToUFM (zipEqual "zipVarEnv" tyvars tys)
-extendVarEnvList env pairs = plusUFM env (listToUFM pairs)
+zipVarEnv tyvars tys       = mkVarEnv (zipEqual "zipVarEnv" tyvars tys)
 lookupVarEnv_NF env id     = case (lookupVarEnv env id) of { Just xx -> xx }
 \end{code}
 
diff --git a/ghc/compiler/deSugar/DsCCall.lhs b/ghc/compiler/deSugar/DsCCall.lhs
index 4384e66f74b9b2558cc2773a1f12376fc00e8067..b10a0fa1772dd4b57f19d42b4abd38a6b74aef19 100644
--- a/ghc/compiler/deSugar/DsCCall.lhs
+++ b/ghc/compiler/deSugar/DsCCall.lhs
@@ -177,14 +177,12 @@ unboxArg arg
   = getSrcLocDs `thenDs` \ l ->
     pprPanic "unboxArg: " (ppr l <+> ppr arg_ty)
   where
-    arg_ty     = exprType arg
-    arg_rep_ty = repType arg_ty
-
-    maybe_product_type 			   	  = splitProductType_maybe arg_ty
-    is_product_type			   	  = maybeToBool maybe_product_type
-    Just (tycon, _, data_con, data_con_arg_tys)   = maybe_product_type
-    data_con_arity				  = dataConSourceArity data_con
-    (data_con_arg_ty1 : _)			  = data_con_arg_tys
+    arg_ty  					= exprType arg
+    maybe_product_type 			   	= splitProductType_maybe arg_ty
+    is_product_type			   	= maybeToBool maybe_product_type
+    Just (_, _, data_con, data_con_arg_tys)	= maybe_product_type
+    data_con_arity				= dataConSourceArity data_con
+    (data_con_arg_ty1 : _)			= data_con_arg_tys
 
     (_ : _ : data_con_arg_ty3 : _) = data_con_arg_tys
     maybe_arg3_tycon    	   = splitTyConApp_maybe data_con_arg_ty3
@@ -299,8 +297,8 @@ resultWrapper result_ty
   | otherwise
   = pprPanic "resultWrapper" (ppr result_ty)
   where
-    maybe_product_type 					    = splitProductType_maybe result_ty
-    is_product_type					    = maybeToBool maybe_product_type
-    Just (tycon, tycon_arg_tys, data_con, data_con_arg_tys) = maybe_product_type
-    data_con_arity					    = dataConSourceArity data_con
+    maybe_product_type 					= splitProductType_maybe result_ty
+    is_product_type					= maybeToBool maybe_product_type
+    Just (_, tycon_arg_tys, data_con, data_con_arg_tys) = maybe_product_type
+    data_con_arity					= dataConSourceArity data_con
 \end{code}
diff --git a/ghc/compiler/hsSyn/HsDecls.lhs b/ghc/compiler/hsSyn/HsDecls.lhs
index 033f426acb36f48dc14c0d6b364cc2056e824702..092ee68b0e3419a33a86cb147f5fb3570fed179d 100644
--- a/ghc/compiler/hsSyn/HsDecls.lhs
+++ b/ghc/compiler/hsSyn/HsDecls.lhs
@@ -11,7 +11,8 @@ module HsDecls (
 	HsDecl(..), TyClDecl(..), InstDecl(..), RuleDecl(..), RuleBndr(..),
 	DefaultDecl(..), ForeignDecl(..), ForKind(..),
 	ExtName(..), isDynamicExtName, extNameStatic,
-	ConDecl(..), ConDetails(..), BangType(..),
+	ConDecl(..), ConDetails(..), 
+	BangType(..), getBangType,
 	IfaceSig(..),  SpecDataSig(..), 
 	DeprecDecl(..), DeprecTxt,
 	hsDeclName, tyClDeclName, isClassDecl, isSynDecl, isDataDecl, countTyClDecls, toHsRule
@@ -313,12 +314,6 @@ data ConDetails name
 		(HsType name)
 		(Maybe name)	-- Just x => labelled field 'x'
 
-data BangType name
-  = Banged   (HsType name)	-- HsType: to allow Haskell extensions
-  | Unbanged (HsType name)	-- (MonoType only needed for straight Haskell)
-  | Unpacked (HsType name)	-- Field is strict and to be unpacked if poss.
-
-
 eq_ConDecl env (ConDecl n1 _ tvs1 cxt1 cds1 _)
 	       (ConDecl n2 _ tvs2 cxt2 cds2 _)
   = n1 == n2 &&
@@ -338,6 +333,16 @@ eq_ConDetails env _ _ = False
 
 eq_fld env (ns1,bt1) (ns2, bt2) = ns1==ns2 && eq_btype env bt1 bt2
 
+  
+data BangType name
+  = Banged   (HsType name)	-- HsType: to allow Haskell extensions
+  | Unbanged (HsType name)	-- (MonoType only needed for straight Haskell)
+  | Unpacked (HsType name)	-- Field is strict and to be unpacked if poss.
+
+getBangType (Banged ty)   = ty
+getBangType (Unbanged ty) = ty
+getBangType (Unpacked ty) = ty
+
 eq_btype env (Banged t1)   (Banged t2)   = eq_hsType env t1 t2
 eq_btype env (Unbanged t1) (Unbanged t2) = eq_hsType env t1 t2
 eq_btype env (Unpacked t1) (Unpacked t2) = eq_hsType env t1 t2
diff --git a/ghc/compiler/hsSyn/HsPat.lhs b/ghc/compiler/hsSyn/HsPat.lhs
index 6e4051ec83286affb70c2ed0450a050454fd5401..09494a1ad1c047660ebd4b3468bf2b9b44b263a3 100644
--- a/ghc/compiler/hsSyn/HsPat.lhs
+++ b/ghc/compiler/hsSyn/HsPat.lhs
@@ -12,7 +12,8 @@ module HsPat (
 	failureFreePat, isWildPat,
 	patsAreAllCons, isConPat,
 	patsAreAllLits,	isLitPat,
-	collectPatBinders, collectPatsBinders
+	collectPatBinders, collectPatsBinders,
+	collectSigTysFromPats
     ) where
 
 #include "HsVersions.h"
@@ -330,3 +331,24 @@ collect (ListPatIn pats)    	 bndrs = foldr collect bndrs pats
 collect (TuplePatIn pats _)  	 bndrs = foldr collect bndrs pats
 collect (RecPatIn c fields) 	 bndrs = foldr (\ (f,pat,_) bndrs -> collect pat bndrs) bndrs fields
 \end{code}
+
+
+\begin{code}
+collectSigTysFromPats :: [InPat name] -> [HsType name]
+collectSigTysFromPats pats = foldr collect_pat [] pats
+
+collect_pat (SigPatIn pat ty)	   acc = collect_pat pat (ty:acc)
+collect_pat WildPatIn	      	   acc = acc
+collect_pat (VarPatIn var)         acc = acc
+collect_pat (LitPatIn _)	   acc = acc
+collect_pat (LazyPatIn pat)        acc = collect_pat pat acc
+collect_pat (AsPatIn a pat)        acc = collect_pat pat acc
+collect_pat (NPlusKPatIn n _)      acc = acc
+collect_pat (ConPatIn c pats)      acc = foldr collect_pat acc pats
+collect_pat (ConOpPatIn p1 c f p2) acc = collect_pat p1 (collect_pat p2 acc)
+collect_pat (NegPatIn  pat)        acc = collect_pat pat acc
+collect_pat (ParPatIn  pat)        acc = collect_pat pat acc
+collect_pat (ListPatIn pats)       acc = foldr collect_pat acc pats
+collect_pat (TuplePatIn pats _)    acc = foldr collect_pat acc pats
+collect_pat (RecPatIn c fields)    acc = foldr (\ (f,pat,_) acc -> collect_pat pat acc) acc fields
+\end{code}
diff --git a/ghc/compiler/hsSyn/HsSyn.lhs b/ghc/compiler/hsSyn/HsSyn.lhs
index 42731ccc13dc0a99bf402dd917653c3fd4836415..bf722a508cff871e464ce566571a7fd0a000df03 100644
--- a/ghc/compiler/hsSyn/HsSyn.lhs
+++ b/ghc/compiler/hsSyn/HsSyn.lhs
@@ -92,9 +92,6 @@ instance (Outputable name, Outputable pat)
 
 	pp_nonnull [] = empty
 	pp_nonnull xs = vcat (map ppr xs)
-
-	pp_iface_version Nothing  = empty
-	pp_iface_version (Just n) = hsep [text "{-# INTERFACE", int n, text "#-}"]
 \end{code}
 
 
diff --git a/ghc/compiler/hsSyn/HsTypes.lhs b/ghc/compiler/hsSyn/HsTypes.lhs
index 62255d767f09621fe694d172eef25ddb35f5db71..86a14675f7702fbd882db08b5c6af36167b714bb 100644
--- a/ghc/compiler/hsSyn/HsTypes.lhs
+++ b/ghc/compiler/hsSyn/HsTypes.lhs
@@ -10,7 +10,7 @@ module HsTypes (
 	, HsTupCon(..), hsTupParens, mkHsTupCon,
 
 	, mkHsForAllTy, mkHsUsForAllTy, mkHsDictTy, mkHsIParamTy
-	, getTyVarName, replaceTyVarName
+	, hsTyVarName, hsTyVarNames, replaceTyVarName
 
 	-- Printing
 	, pprParendHsType, pprHsForAll, pprHsContext, pprHsTyVarBndr
@@ -128,8 +128,10 @@ data HsTyVarBndr name
 	-- for-alls in it, (mostly to do with dictionaries).  These
 	-- must be explicitly Kinded.
 
-getTyVarName (UserTyVar n)    = n
-getTyVarName (IfaceTyVar n _) = n
+hsTyVarName (UserTyVar n)    = n
+hsTyVarName (IfaceTyVar n _) = n
+
+hsTyVarNames tvs = map hsTyVarName tvs
 
 replaceTyVarName :: HsTyVarBndr name1 -> name2 -> HsTyVarBndr name2
 replaceTyVarName (UserTyVar n)    n' = UserTyVar n'
diff --git a/ghc/compiler/nativeGen/MachCode.lhs b/ghc/compiler/nativeGen/MachCode.lhs
index f54c759ee6e9ea117b95ea3cc54821dbc3c8fb07..a45f7dbc5f5cf42036091e8e4db261121fad9fa3 100644
--- a/ghc/compiler/nativeGen/MachCode.lhs
+++ b/ghc/compiler/nativeGen/MachCode.lhs
@@ -587,11 +587,6 @@ getRegister (StPrim primop [x]) -- unary PrimOps
       Int2DoubleOp -> coerceInt2FP DoubleRep x
 
       other_op ->
-        let
-	    fixed_x = if   is_float_op  -- promote to double
-		      then StPrim Float2DoubleOp [x]
-		      else x
-	in
 	getRegister (StCall fn cCallConv DoubleRep [x])
        where
 	(is_float_op, fn)
@@ -956,6 +951,8 @@ getRegister (StPrim primop [x]) -- unary PrimOps
       FloatNegOp     -> trivialUFCode FloatRep (FNEG F) x
       DoubleNegOp    -> trivialUFCode DoubleRep (FNEG DF) x
 
+      DoubleNegOp -> trivialUFCode DoubleRep (FNEG DF) x
+
       Double2FloatOp -> trivialUFCode FloatRep  (FxTOy DF F) x
       Float2DoubleOp -> trivialUFCode DoubleRep (FxTOy F DF) x
 
@@ -1555,7 +1552,6 @@ condFltCode cond x y
     	code1 = registerCode register1 tmp1
     	src1  = registerName register1 tmp1
 
-    	pk2   = registerRep register2
     	code2 = registerCode register2 tmp2
     	src2  = registerName register2 tmp2
 
diff --git a/ghc/compiler/nativeGen/StixMacro.lhs b/ghc/compiler/nativeGen/StixMacro.lhs
index 19c02d2e52536455a5e92cf7edb5dcda76a99f60..415d7c8c5de9827ebab34080c8394d0af4aec170 100644
--- a/ghc/compiler/nativeGen/StixMacro.lhs
+++ b/ghc/compiler/nativeGen/StixMacro.lhs
@@ -74,7 +74,6 @@ macroCode UPD_CAF args
 	[cafptr,bhptr] = map amodeToStix args
     	w0 = StInd PtrRep cafptr
 	w1 = StInd PtrRep (StIndex PtrRep cafptr fixedHS)
-	blocking_queue = StInd PtrRep (StIndex PtrRep bhptr fixedHS)
 	a1 = StAssign PtrRep w0 ind_static_info
 	a2 = StAssign PtrRep w1 bhptr
 	a3 = StCall SLIT("newCAF") cCallConv VoidRep [cafptr]
diff --git a/ghc/compiler/parser/Lex.lhs b/ghc/compiler/parser/Lex.lhs
index 9a2ab9c9c07f375e6bd163615236e1a5872e01ee..dd020e750a5beef49dba99c00917d5a3f76e73f8 100644
--- a/ghc/compiler/parser/Lex.lhs
+++ b/ghc/compiler/parser/Lex.lhs
@@ -1006,7 +1006,6 @@ mk_var_token pk_str
   | otherwise		= ITvarsym pk_str
   where
       (C# f) = _HEAD_ pk_str
-      tl     = _TAIL_ pk_str
 
 mk_qvar_token m token =
  case mk_var_token token of
diff --git a/ghc/compiler/parser/RdrHsSyn.lhs b/ghc/compiler/parser/RdrHsSyn.lhs
index 0884f54e07640947bfe16bb463153b6d5ea1213f..a4cbc8047b63f5301299511eab77815b53b75ff6 100644
--- a/ghc/compiler/parser/RdrHsSyn.lhs
+++ b/ghc/compiler/parser/RdrHsSyn.lhs
@@ -66,6 +66,7 @@ module RdrHsSyn (
 #include "HsVersions.h"
 
 import HsSyn
+import HsPat		( collectSigTysFromPats )
 import Name		( mkClassTyConOcc, mkClassDataConOcc )
 import OccName		( mkClassTyConOcc, mkClassDataConOcc, mkWorkerOcc,
                           mkSuperDictSelOcc, mkDefaultMethodOcc
@@ -144,7 +145,7 @@ extractHsTyRdrTyVars	 :: RdrNameHsType -> [RdrName]
 extractHsTyRdrTyVars ty =  filter isRdrTyVar (extractHsTyRdrNames ty)
 
 extractHsTysRdrTyVars	  :: [RdrNameHsType] -> [RdrName]
-extractHsTysRdrTyVars tys =  filter isRdrTyVar (nub (extract_tys tys []))
+extractHsTysRdrTyVars tys =  filter isRdrTyVar (nub (extract_tys tys))
 
 extractRuleBndrsTyVars :: [RuleBndr RdrName] -> [RdrName]
 extractRuleBndrsTyVars bndrs = filter isRdrTyVar (nub (foldr go [] bndrs))
@@ -162,7 +163,7 @@ extract_ctxt ctxt acc = foldr extract_pred acc ctxt
 extract_pred (HsPClass cls tys) acc	= foldr extract_ty (cls : acc) tys
 extract_pred (HsPIParam n ty) acc	= extract_ty ty acc
 
-extract_tys tys acc = foldr extract_ty acc tys
+extract_tys tys = foldr extract_ty [] tys
 
 extract_ty (HsAppTy ty1 ty2)          acc = extract_ty ty1 (extract_ty ty2 acc)
 extract_ty (HsListTy ty)              acc = extract_ty ty acc
@@ -178,26 +179,14 @@ extract_ty (HsForAllTy (Just tvs) ctxt ty)
                                       (filter (`notElem` locals) $
 				       extract_ctxt ctxt (extract_ty ty []))
 				    where
-				      locals = map getTyVarName tvs
+				      locals = hsTyVarNames tvs
 
 
 extractPatsTyVars :: [RdrNamePat] -> [RdrName]
-extractPatsTyVars pats = filter isRdrTyVar (nub (foldr extract_pat [] pats))
-
-extract_pat (SigPatIn pat ty)	   acc = extract_ty ty acc
-extract_pat WildPatIn	      	   acc = acc
-extract_pat (VarPatIn var)         acc = acc
-extract_pat (LitPatIn _)	   acc = acc
-extract_pat (LazyPatIn pat)        acc = extract_pat pat acc
-extract_pat (AsPatIn a pat)        acc = extract_pat pat acc
-extract_pat (NPlusKPatIn n _)      acc = acc
-extract_pat (ConPatIn c pats)      acc = foldr extract_pat acc pats
-extract_pat (ConOpPatIn p1 c f p2) acc = extract_pat p1 (extract_pat p2 acc)
-extract_pat (NegPatIn  pat)        acc = extract_pat pat acc
-extract_pat (ParPatIn  pat)        acc = extract_pat pat acc
-extract_pat (ListPatIn pats)       acc = foldr extract_pat acc pats
-extract_pat (TuplePatIn pats _)    acc = foldr extract_pat acc pats
-extract_pat (RecPatIn c fields)    acc = foldr (\ (f,pat,_) acc -> extract_pat pat acc) acc fields
+extractPatsTyVars = filter isRdrTyVar . 
+		    nub . 
+		    extract_tys .
+		    collectSigTysFromPats
 \end{code}
 
 mkClassDecl builds a RdrClassDecl, filling in the names for tycon and datacon
diff --git a/ghc/compiler/rename/Rename.lhs b/ghc/compiler/rename/Rename.lhs
index e6229017d36477eb556124f28bd95913f65e0a47..f2f86144876eb683fcce09198a5962dead493231 100644
--- a/ghc/compiler/rename/Rename.lhs
+++ b/ghc/compiler/rename/Rename.lhs
@@ -39,7 +39,8 @@ import Name		( Name, isLocallyDefined, NamedThing(..), getSrcLoc,
 			  nameOccName, nameUnique, nameModule, maybeUserImportedFrom,
 			  isUserImportedExplicitlyName, isUserImportedName,
 			  maybeWiredInTyConName, maybeWiredInIdName,
-			  isUserExportedName, toRdrName
+			  isUserExportedName, toRdrName,
+			  nameEnvElts, extendNameEnv
 			)
 import OccName		( occNameFlavour, isValOcc )
 import Id		( idType )
@@ -489,7 +490,7 @@ getGates source_fvs (SigD (IfaceSig _ ty _ _))
 
 getGates source_fvs (TyClD (ClassDecl ctxt cls tvs _ sigs _ _ _ _ _ _ _))
   = (delListFromNameSet (foldr (plusFV . get) (extractHsCtxtTyNames ctxt) sigs)
-		       (map getTyVarName tvs)
+		        (hsTyVarNames tvs)
      `addOneToNameSet` cls)
     `plusFV` maybe_double
   where
@@ -509,12 +510,12 @@ getGates source_fvs (TyClD (ClassDecl ctxt cls tvs _ sigs _ _ _ _ _ _ _))
 
 getGates source_fvs (TyClD (TySynonym tycon tvs ty _))
   = delListFromNameSet (extractHsTyNames ty)
-		       (map getTyVarName tvs)
+		       (hsTyVarNames tvs)
 	-- A type synonym type constructor isn't a "gate" for instance decls
 
 getGates source_fvs (TyClD (TyData _ ctxt tycon tvs cons _ _ _ _))
   = delListFromNameSet (foldr (plusFV . get) (extractHsCtxtTyNames ctxt) cons)
-		       (map getTyVarName tvs)
+		       (hsTyVarNames tvs)
     `addOneToNameSet` tycon
   where
     get (ConDecl n _ tvs ctxt details _)
@@ -522,7 +523,7 @@ getGates source_fvs (TyClD (TyData _ ctxt tycon tvs cons _ _ _ _))
 		-- If the constructor is method, get fvs from all its fields
 	= delListFromNameSet (get_details details `plusFV` 
 		  	      extractHsCtxtTyNames ctxt)
-			     (map getTyVarName tvs)
+			     (hsTyVarNames tvs)
     get (ConDecl n _ tvs ctxt (RecCon fields) _)
 		-- Even if the constructor isn't mentioned, the fields
 		-- might be, as selectors.  They can't mention existentially
@@ -540,9 +541,7 @@ getGates source_fvs (TyClD (TyData _ ctxt tycon tvs cons _ _ _ _))
     get_field (fs,t) | any (`elemNameSet` source_fvs) fs = get_bang t
 		     | otherwise			 = emptyFVs
 
-    get_bang (Banged   t) = extractHsTyNames t
-    get_bang (Unbanged t) = extractHsTyNames t
-    get_bang (Unpacked t) = extractHsTyNames t
+    get_bang bty = extractHsTyNames (getBangType bty)
 
 getGates source_fvs other_decl = emptyFVs
 \end{code}
@@ -612,7 +611,7 @@ fixitiesFromLocalDecls gbl_env decls
 	    Just (FixitySig _ _ loc') -> addErrRn (dupFixityDecl rdr_name loc loc')
 					 `thenRn_` returnRn acc ;
 
-	    Nothing -> returnRn (addToNameEnv acc name (FixitySig name fixity loc))
+	    Nothing -> returnRn (extendNameEnv acc name (FixitySig name fixity loc))
 	  }}
 \end{code}
 
diff --git a/ghc/compiler/rename/RnEnv.lhs b/ghc/compiler/rename/RnEnv.lhs
index 14a833959abb42f950d93858b8b974507e0e0b54..823a1222c2b22b75298dead84fa1c4b8766d5891 100644
--- a/ghc/compiler/rename/RnEnv.lhs
+++ b/ghc/compiler/rename/RnEnv.lhs
@@ -16,7 +16,7 @@ import RnHsSyn		( RenamedHsType )
 import RdrName		( RdrName, rdrNameModule, rdrNameOcc, isQual, isUnqual,
 			  mkRdrUnqual, qualifyRdrName
 			)
-import HsTypes		( getTyVarName, replaceTyVarName )
+import HsTypes		( hsTyVarName, hsTyVarNames, replaceTyVarName )
 
 import RnMonad
 import Name		( Name, Provenance(..), ExportFlag(..), NamedThing(..),
@@ -25,7 +25,8 @@ import Name		( Name, Provenance(..), ExportFlag(..), NamedThing(..),
 			  mkIPName, isWiredInName, hasBetterProv,
 			  nameOccName, setNameModule, nameModule,
 			  pprOccName, isLocallyDefined, nameUnique, nameOccName,
-			  setNameProvenance, getNameProvenance, pprNameProvenance
+			  setNameProvenance, getNameProvenance, pprNameProvenance,
+			  extendNameEnv_C, plusNameEnv_C, nameEnvElts
 			)
 import NameSet
 import OccName		( OccName,
@@ -351,7 +352,7 @@ extendTyVarEnvFVRn :: [HsTyVarBndr Name] -> RnMS (a, FreeVars) -> RnMS (a, FreeV
 extendTyVarEnvFVRn tyvars enclosed_scope
   = getLocalNameEnv		`thenRn` \ env ->
     let
-	tyvar_names = map getTyVarName tyvars
+	tyvar_names = hsTyVarNames tyvars
 	new_env = addListToRdrEnv env [ (mkRdrUnqual (getOccName name), name) 
 				      | name <- tyvar_names
 				      ]
@@ -373,7 +374,7 @@ bindTyVars2Rn :: SDoc -> [HsTyVarBndr RdrName]
 bindTyVars2Rn doc_str tyvar_names enclosed_scope
   = getSrcLocRn					`thenRn` \ loc ->
     let
-	located_tyvars = [(getTyVarName tv, loc) | tv <- tyvar_names] 
+	located_tyvars = [(hsTyVarName tv, loc) | tv <- tyvar_names] 
     in
     bindLocatedLocalsRn doc_str located_tyvars	$ \ names ->
     enclosed_scope names (zipWith replaceTyVarName tyvar_names names)
@@ -633,7 +634,7 @@ plusAvail a1 a2 = pprPanic "RnEnv.plusAvail" (hsep [pprAvail a1,pprAvail a2])
 #endif
 
 addAvail :: AvailEnv -> AvailInfo -> AvailEnv
-addAvail avails avail = addToNameEnv_C plusAvail avails (availName avail) avail
+addAvail avails avail = extendNameEnv_C plusAvail avails (availName avail) avail
 
 emptyAvailEnv = emptyNameEnv
 unitAvailEnv :: AvailInfo -> AvailEnv
diff --git a/ghc/compiler/rename/RnHsSyn.lhs b/ghc/compiler/rename/RnHsSyn.lhs
index 60dfedb452e5320880a1559b1dd753b9175ee63f..05412f5f8d33a13c614b12631c97b8bf0b6636f4 100644
--- a/ghc/compiler/rename/RnHsSyn.lhs
+++ b/ghc/compiler/rename/RnHsSyn.lhs
@@ -41,6 +41,7 @@ type RenamedMatch		= Match			Name RenamedPat
 type RenamedMonoBinds		= MonoBinds		Name RenamedPat
 type RenamedPat			= InPat			Name
 type RenamedHsType		= HsType		Name
+type RenamedHsPred		= HsPred		Name
 type RenamedRecordBinds		= HsRecordBinds		Name RenamedPat
 type RenamedSig			= Sig			Name
 type RenamedStmt		= Stmt			Name RenamedPat
@@ -87,7 +88,7 @@ extractHsTyNames ty
     get (HsForAllTy (Just tvs) 
 		    ctxt ty)   = (extractHsCtxtTyNames ctxt `unionNameSets` get ty)
 					    `minusNameSet`
-				    mkNameSet (map getTyVarName tvs)
+				    mkNameSet (hsTyVarNames tvs)
     get ty@(HsForAllTy Nothing _ _) = pprPanic "extractHsTyNames" (ppr ty)
 
 extractHsTyNames_s  :: [RenamedHsType] -> NameSet
diff --git a/ghc/compiler/rename/RnIfaces.lhs b/ghc/compiler/rename/RnIfaces.lhs
index 3f775a47961ee88ed8e494f2ac175f601be870ee..dbb90e517666469acb8ad1f2d4f68a2ddb96b95b 100644
--- a/ghc/compiler/rename/RnIfaces.lhs
+++ b/ghc/compiler/rename/RnIfaces.lhs
@@ -41,7 +41,8 @@ import ParseIface	( parseIface, IfaceStuff(..) )
 
 import Name		( Name {-instance NamedThing-}, nameOccName,
 			  nameModule, isLocallyDefined, 
-			  isWiredInName, nameUnique, NamedThing(..)
+			  isWiredInName, nameUnique, NamedThing(..),
+			  elemNameEnv, extendNameEnv
 			 )
 import Module		( Module, moduleString, pprModule,
 			  mkVanillaModule, pprModuleName,
@@ -300,7 +301,7 @@ loadDecl mod decls_map (version, decl)
 				       | name <- availNames full_avail]
 	add_decl decls_map (name, stuff)
 	  = WARN( name `elemNameEnv` decls_map, ppr name )
-	    addToNameEnv decls_map name stuff
+	    extendNameEnv decls_map name stuff
     in
     returnRn new_decls_map
     }
@@ -343,7 +344,7 @@ loadFixDecls mod_name fixity_env (version, decls)
 
   | otherwise
   = mapRn (loadFixDecl mod_name) decls	`thenRn` \ to_add ->
-    returnRn (addListToNameEnv fixity_env to_add)
+    returnRn (extendNameEnvList fixity_env to_add)
 
 loadFixDecl mod_name sig@(FixitySig rdr_name fixity loc)
   = mkImportedGlobalName mod_name (rdrNameOcc rdr_name) 	`thenRn` \ name ->
@@ -438,7 +439,7 @@ loadDeprec mod deprec_env (Deprecation ie txt _)
   = setModuleRn (moduleName mod) $
     mapRn mkImportedGlobalFromRdrName (ieNames ie) `thenRn` \ names ->
     traceRn (text "loaded deprecation(s) for" <+> hcat (punctuate comma (map ppr names)) <> colon <+> ppr txt) `thenRn_`
-    returnRn (extendNameEnv deprec_env (zip names (repeat txt)))
+    returnRn (extendNameEnvList deprec_env (zip names (repeat txt)))
 \end{code}
 
 
diff --git a/ghc/compiler/rename/RnMonad.lhs b/ghc/compiler/rename/RnMonad.lhs
index 1159bfe6511bffa8b7cbbc796f0921fb93648e4d..457f2c1d788f93447675f35967819d3b98e02140 100644
--- a/ghc/compiler/rename/RnMonad.lhs
+++ b/ghc/compiler/rename/RnMonad.lhs
@@ -47,9 +47,7 @@ import RdrName		( RdrName, dummyRdrVarName, rdrNameOcc,
 import Name		( Name, OccName, NamedThing(..), getSrcLoc,
 			  isLocallyDefinedName, nameModule, nameOccName,
 			  decode, mkLocalName, mkUnboundName,
-			  NameEnv, lookupNameEnv, emptyNameEnv, unitNameEnv, extendNameEnv,
-			  addToNameEnv_C, plusNameEnv_C, nameEnvElts, 
-			  elemNameEnv, addToNameEnv, addListToNameEnv
+			  NameEnv, lookupNameEnv, emptyNameEnv, unitNameEnv, extendNameEnvList
 			)
 import Module		( Module, ModuleName, ModuleHiMap, SearchPath, WhereFrom,
 			  mkModuleHiMaps, moduleName, mkSearchPath
@@ -696,7 +694,7 @@ extendFixityEnv :: [(Name, RenamedFixitySig)] -> RnMS a -> RnMS a
 extendFixityEnv fixes enclosed_scope
 	        rn_down l_down@(SDown {rn_fixenv = fixity_env})
   = let
-	new_fixity_env = extendNameEnv fixity_env fixes
+	new_fixity_env = extendNameEnvList fixity_env fixes
     in
     enclosed_scope rn_down (l_down {rn_fixenv = new_fixity_env})
 \end{code}
diff --git a/ghc/compiler/rename/RnNames.lhs b/ghc/compiler/rename/RnNames.lhs
index f07651e24f60c5c961cff2c99041bde561dd456d..7bcd56506ac75575f75fdcd8a1ea6ecccc81f960 100644
--- a/ghc/compiler/rename/RnNames.lhs
+++ b/ghc/compiler/rename/RnNames.lhs
@@ -37,7 +37,8 @@ import Module	( ModuleName, mkThisModule, pprModuleName, WhereFrom(..) )
 import NameSet
 import Name	( Name, ExportFlag(..), ImportReason(..), Provenance(..),
 		  isLocallyDefined, setNameProvenance,
-		  nameOccName, getSrcLoc, pprProvenance, getNameProvenance
+		  nameOccName, getSrcLoc, pprProvenance, getNameProvenance,
+		  nameEnvElts
 		)
 import RdrName	( RdrName, rdrNameOcc, setRdrNameOcc, mkRdrQual, mkRdrUnqual, isQual, isUnqual )
 import OccName	( setOccNameSpace, dataName )
diff --git a/ghc/compiler/rename/RnSource.lhs b/ghc/compiler/rename/RnSource.lhs
index b2c4aa26f888470539950c4e3fdebe3ac0876408..1b19d4b69ff7cfd9bb1ded963872110cefa5dd20 100644
--- a/ghc/compiler/rename/RnSource.lhs
+++ b/ghc/compiler/rename/RnSource.lhs
@@ -11,7 +11,7 @@ module RnSource ( rnDecl, rnSourceDecls, rnHsType, rnHsSigType ) where
 import RnExpr
 import HsSyn
 import HsPragmas
-import HsTypes		( getTyVarName, pprHsContext )
+import HsTypes		( hsTyVarNames, pprHsContext )
 import RdrName		( RdrName, isRdrDataCon, rdrNameOcc, isRdrTyVar, mkRdrNameWkr )
 import RdrHsSyn		( RdrNameContext, RdrNameHsType, RdrNameConDecl,
 			  extractRuleBndrsTyVars, extractHsTyRdrTyVars,
@@ -570,7 +570,7 @@ rnHsType doc (HsForAllTy (Just forall_tyvars) ctxt tau)
 	mentioned_in_tau		= extractHsTyRdrTyVars tau
 	mentioned_in_ctxt		= extractHsCtxtRdrTyVars ctxt
 	mentioned			= nub (mentioned_in_tau ++ mentioned_in_ctxt)
-	forall_tyvar_names		= map getTyVarName forall_tyvars
+	forall_tyvar_names		= hsTyVarNames forall_tyvars
 
 	-- Explicitly quantified but not mentioned in ctxt or tau
 	warn_guys			= filter (`notElem` mentioned) forall_tyvar_names
diff --git a/ghc/compiler/simplCore/LiberateCase.lhs b/ghc/compiler/simplCore/LiberateCase.lhs
index bd9bac25e72f9f036be87eabc7bb0dc1ff7a0630..baa8bdaa26bf5f60bdc9e427a88e62082104c5c2 100644
--- a/ghc/compiler/simplCore/LiberateCase.lhs
+++ b/ghc/compiler/simplCore/LiberateCase.lhs
@@ -237,10 +237,10 @@ libCase env (Let bind body)
 libCase env (Case scrut bndr alts)
   = Case (libCase env scrut) bndr (map (libCaseAlt env_alts) alts)
   where
-    env_alts = addBinders env [bndr]
+    env_alts = addBinders env_with_scrut [bndr]
     env_with_scrut = case scrut of
 		  	Var scrut_var -> addScrutedVar env scrut_var
-			other		  -> env
+			other	      -> env
 
 libCaseAlt env (con,args,rhs) = (con, args, libCase (addBinders env args) rhs)
 \end{code}
diff --git a/ghc/compiler/simplCore/OccurAnal.lhs b/ghc/compiler/simplCore/OccurAnal.lhs
index 4681aa3edae27969f273f4d6ee5741e19aeab7b1..4d856f77049754ee24732106b264a9abbcc7ebf3 100644
--- a/ghc/compiler/simplCore/OccurAnal.lhs
+++ b/ghc/compiler/simplCore/OccurAnal.lhs
@@ -74,8 +74,8 @@ occurAnalyseRule (Rule str tpl_vars tpl_args rhs)
 		-- Add occ info to tpl_vars, rhs
   = Rule str tpl_vars' tpl_args rhs'
   where
-    (rhs_uds, rhs')	  = occurAnalyseExpr isLocallyDefined rhs
-    (rhs_uds1, tpl_vars') = tagBinders rhs_uds tpl_vars
+    (rhs_uds, rhs') = occurAnalyseExpr isLocallyDefined rhs
+    (_, tpl_vars')  = tagBinders rhs_uds tpl_vars
 \end{code}
 
 
@@ -286,8 +286,6 @@ It isn't easy to do a perfect job in one blow.  Consider
 occAnalBind env (Rec pairs) body_usage
   = foldr (_scc_ "occAnalBind.dofinal" do_final_bind) (body_usage, []) sccs
   where
-    pp_item (_, bndr, _)     = ppr bndr
-
     binders = map fst pairs
     rhs_env = env `addNewCands` binders
 
@@ -613,8 +611,8 @@ occAnal env expr@(Lam _ _)
     (really_final_usage,
      mkLams tagged_binders body') }
   where
-    (binders, body)    = collectBinders expr
-    (linear, env_body, binders') = oneShotGroup env binders
+    (binders, body)       = collectBinders expr
+    (linear, env_body, _) = oneShotGroup env binders
 
 occAnal env (Case scrut bndr alts)
   = case mapAndUnzip (occAnalAlt alt_env) alts of { (alts_usage_s, alts')   -> 
diff --git a/ghc/compiler/simplCore/SetLevels.lhs b/ghc/compiler/simplCore/SetLevels.lhs
index 91dbe75aee45903d82049d2e2257387eb4c40a23..4aa1c5b227f130fb9e86e8a4a945262196246ca9 100644
--- a/ghc/compiler/simplCore/SetLevels.lhs
+++ b/ghc/compiler/simplCore/SetLevels.lhs
@@ -250,7 +250,6 @@ lvlExpr ctxt_lvl env (_, AnnCase expr case_bndr alts)
     mapLvl (lvl_alt alts_env) alts	`thenLvl` \ alts' ->
     returnLvl (Case expr' (case_bndr, incd_lvl) alts')
   where
-      expr_type = exprType (deAnnotate expr)
       incd_lvl  = incMinorLvl ctxt_lvl
 
       lvl_alt alts_env (con, bs, rhs)
diff --git a/ghc/compiler/simplCore/SimplCore.lhs b/ghc/compiler/simplCore/SimplCore.lhs
index fda56fe4eae7056bccc6d80a20f8ec40de480e5c..0321bf7dadd426e678b152ef6aa86031e9292520 100644
--- a/ghc/compiler/simplCore/SimplCore.lhs
+++ b/ghc/compiler/simplCore/SimplCore.lhs
@@ -65,8 +65,7 @@ core2core :: [CoreToDo]		-- Spec of what core-to-core passes to do
 core2core core_todos binds rules
   = do
 	us <-  mkSplitUniqSupply 's'
-	let (cp_us, us1)   = splitUniqSupply us
-	    (ru_us, ps_us) = splitUniqSupply us1
+	let (cp_us, ru_us) = splitUniqSupply us
 
         let (local_rules, imported_rules) = partition localRule rules
 
@@ -258,9 +257,6 @@ simplifyPgm (imported_rule_ids, rule_lhs_fvs)
     max_iterations = getSimplIntSwitch sw_chkr MaxSimplifierIterations
     black_list_fn  = blackListed rule_lhs_fvs (intSwitchSet sw_chkr SimplInlinePhase)
 
-    core_iter_dump binds | opt_D_verbose_core2core = pprCoreBindings binds
-		         | otherwise		   = empty
-
     iteration us iteration_no counts binds
       -- Try and force thunks off the binds; significantly reduces
       -- space usage, especially with -O.  JRS, 000620.
diff --git a/ghc/compiler/simplCore/SimplMonad.lhs b/ghc/compiler/simplCore/SimplMonad.lhs
index a5d5a9806ae8bd5f31a857b05a7df8a6a8691409..697fb715365e8405a7351f12bdcdc80c4f75b0be 100644
--- a/ghc/compiler/simplCore/SimplMonad.lhs
+++ b/ghc/compiler/simplCore/SimplMonad.lhs
@@ -569,7 +569,6 @@ switchOffInlining m env us sc
 	-- may as well do the same here.
   where
     subst	   = seSubst env
-    old_black_list = seBlackList env
 \end{code}
 
 
diff --git a/ghc/compiler/simplCore/SimplUtils.lhs b/ghc/compiler/simplCore/SimplUtils.lhs
index d346292c332ca9ca4bf968ee58b4b2ef59cd93d8..544a791144c63be92306ceed759bae3f644ec167 100644
--- a/ghc/compiler/simplCore/SimplUtils.lhs
+++ b/ghc/compiler/simplCore/SimplUtils.lhs
@@ -444,7 +444,6 @@ mkRhsTyLam tyvars body			-- Only does something if there's a let
     whnf_in_middle (Let _ e) = whnf_in_middle e
     whnf_in_middle e	     = exprIsCheap e
 
-    main_tyvar_set = mkVarSet tyvars
 
     go fn (Let bind@(NonRec var rhs) body) | exprIsTrivial rhs
       = go (fn . Let bind) body
@@ -455,6 +454,8 @@ mkRhsTyLam tyvars body			-- Only does something if there's a let
 	returnSmpl (Let (NonRec var' (mkLams tyvars_here (fn rhs))) body')
       where
 	tyvars_here = tyvars
+		--	main_tyvar_set = mkVarSet tyvars
+		--	var_ty = idType var
 		-- varSetElems (main_tyvar_set `intersectVarSet` tyVarsOfType var_ty)
 		-- tyvars_here was an attempt to reduce the number of tyvars
 		-- wrt which the new binding is abstracted.  But the naive
@@ -472,8 +473,6 @@ mkRhsTyLam tyvars body			-- Only does something if there's a let
 		-- abstracting wrt *all* the tyvars.  We'll see if that
 		-- gives rise to problems.   SLPJ June 98
 
-	var_ty = idType var
-
     go fn (Let (Rec prs) body)
        = mapAndUnzipSmpl (mk_poly tyvars_here) vars	`thenSmpl` \ (vars', rhss') ->
 	 let
@@ -485,9 +484,9 @@ mkRhsTyLam tyvars body			-- Only does something if there's a let
 	 (vars,rhss) = unzip prs
 	 tyvars_here = tyvars
 		-- varSetElems (main_tyvar_set `intersectVarSet` tyVarsOfTypes var_tys)
+		-- 	 var_tys     = map idType vars
 		-- See notes with tyvars_here above
 
-	 var_tys     = map idType vars
 
     go fn body = returnSmpl (mkLams tyvars (fn body))
 
@@ -589,7 +588,7 @@ tryEtaExpansion rhs
 	-- and we are going to make extra term binders (y_bndrs) from the type
 	-- which will be processed with the rhs substitution environment.
 	-- This only went wrong in a mind bendingly complicated case.
-    (potential_extra_arg_tys, inner_ty) = splitFunTys (exprType body)
+    (potential_extra_arg_tys, _) = splitFunTys (exprType body)
 	
     y_tys :: [InType]
     y_tys  = take no_extras_wanted potential_extra_arg_tys
diff --git a/ghc/compiler/specialise/Specialise.lhs b/ghc/compiler/specialise/Specialise.lhs
index d73e2c3f412c8dc657135a6b5b6b2c8d169d665d..884d70be5cbbd3b357a76a2eab30f85cd3b71d2a 100644
--- a/ghc/compiler/specialise/Specialise.lhs
+++ b/ghc/compiler/specialise/Specialise.lhs
@@ -820,10 +820,10 @@ specDefn subst calls (fn, rhs)
 	-- It's role as a holder for a call instance is o'er
 	-- But it might be alive for some other reason by now.
 
-    fn_type		 = idType fn
-    (tyvars, theta, tau) = splitSigmaTy fn_type
-    n_tyvars		 = length tyvars
-    n_dicts		 = length theta
+    fn_type	       = idType fn
+    (tyvars, theta, _) = splitSigmaTy fn_type
+    n_tyvars	       = length tyvars
+    n_dicts	       = length theta
 
     (rhs_tyvars, rhs_ids, rhs_body) = collectTyAndValBinders rhs
     rhs_dicts = take n_dicts rhs_ids
@@ -985,10 +985,10 @@ mkCallUDs subst f args
 	  calls      = singleCall f spec_tys dicts
     }
   where
-    (tyvars, theta, tau) = splitSigmaTy (idType f)
-    constrained_tyvars   = tyVarsOfTheta theta 
-    n_tyvars		 = length tyvars
-    n_dicts		 = length theta
+    (tyvars, theta, _) = splitSigmaTy (idType f)
+    constrained_tyvars = tyVarsOfTheta theta 
+    n_tyvars	       = length tyvars
+    n_dicts	       = length theta
 
     spec_tys = [mk_spec_ty tv ty | (tv, Type ty) <- tyvars `zip` args]
     dicts    = [dict_expr | (_, dict_expr) <- theta `zip` (drop n_tyvars args)]
diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs
index 7d8b4c3b0312c48a0a9d01ed813d8b30e3b4c73d..775a36d41e4c77bb589abd83c61509f164f06232 100644
--- a/ghc/compiler/typecheck/TcBinds.lhs
+++ b/ghc/compiler/typecheck/TcBinds.lhs
@@ -37,7 +37,7 @@ import TcPat		( tcPat )
 import TcSimplify	( bindInstsOfLocalFuns )
 import TcType		( TcType, TcThetaType,
 			  TcTyVar,
-			  newTyVarTy, newTyVar, newTyVarTy_OpenKind, tcInstTcType,
+			  newTyVarTy, newTyVar, tcInstTcType,
 			  zonkTcType, zonkTcTypes, zonkTcThetaType, zonkTcTyVarToTyVar
 			)
 import TcUnify		( unifyTauTy, unifyTauTyLists )
@@ -50,7 +50,7 @@ import NameSet
 import Type		( mkTyVarTy, tyVarsOfTypes, mkTyConApp,
 			  splitSigmaTy, mkForAllTys, mkFunTys, getTyVar, 
 			  mkPredTy, splitRhoTy, mkForAllTy, isUnLiftedType, 
-			  isUnboxedType, unboxedTypeKind, boxedTypeKind
+			  isUnboxedType, unboxedTypeKind, boxedTypeKind, openTypeKind
 			)
 import FunDeps		( tyVarFunDep, oclose )
 import Var		( TyVar, tyVarKind )
@@ -680,7 +680,7 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
 		  lie_avail1 `plusLIE` lie_avail2)
 
     tc_mb_pats (FunMonoBind name inf matches locn)
-      = new_lhs_ty 			`thenNF_Tc` \ bndr_ty ->
+      = newTyVarTy kind 		`thenNF_Tc` \ bndr_ty -> 
 	tc_pat_bndr name bndr_ty	`thenTc` \ bndr_id ->
 	let
 	   complete_it xve = tcAddSrcLoc locn				$
@@ -691,7 +691,7 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
 
     tc_mb_pats bind@(PatMonoBind pat grhss locn)
       = tcAddSrcLoc locn	 	$
-	new_lhs_ty			`thenNF_Tc` \ pat_ty -> 
+	newTyVarTy kind 		`thenNF_Tc` \ pat_ty -> 
 
 		-- 	Now typecheck the pattern
 		-- We don't support binding fresh type variables in the
@@ -715,9 +715,9 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
 
 	-- Figure out the appropriate kind for the pattern,
 	-- and generate a suitable type variable 
-    new_lhs_ty = case is_rec of
-		     Recursive    -> newTyVarTy boxedTypeKind	-- Recursive, so no unboxed types
-		     NonRecursive -> newTyVarTy_OpenKind 	-- Non-recursive, so we permit unboxed types
+    kind = case is_rec of
+		Recursive    -> boxedTypeKind	-- Recursive, so no unboxed types
+		NonRecursive -> openTypeKind 	-- Non-recursive, so we permit unboxed types
 \end{code}
 
 %************************************************************************
diff --git a/ghc/compiler/typecheck/TcClassDcl.lhs b/ghc/compiler/typecheck/TcClassDcl.lhs
index eae1c69d277a5a815e4779ab123267aca08a60b4..7b6765cf6222aa0cb45e37817a58e85b11a42e06 100644
--- a/ghc/compiler/typecheck/TcClassDcl.lhs
+++ b/ghc/compiler/typecheck/TcClassDcl.lhs
@@ -4,7 +4,7 @@
 \section[TcClassDcl]{Typechecking class declarations}
 
 \begin{code}
-module TcClassDcl ( kcClassDecl, tcClassDecl1, tcClassDecls2, mkImplicitClassBinds,
+module TcClassDcl ( tcClassDecl1, tcClassDecls2, mkImplicitClassBinds,
 		    tcMethodBind, checkFromThisClass
 		  ) where
 
@@ -14,7 +14,7 @@ import HsSyn		( HsDecl(..), TyClDecl(..), Sig(..), MonoBinds(..),
 			  InPat(..), HsBinds(..), GRHSs(..),
 			  HsExpr(..), HsLit(..), HsType(..), HsPred(..),
 			  mkSimpleMatch,
-			  andMonoBinds, andMonoBindList, getTyVarName, 
+			  andMonoBinds, andMonoBindList, 
 			  isClassDecl, isClassOpSig, isPragSig, collectMonoBinders
 			)
 import BasicTypes	( NewOrData(..), TopLevelFlag(..), RecFlag(..) )
@@ -25,22 +25,20 @@ import RnHsSyn		( RenamedTyClDecl, RenamedClassPragmas,
 import TcHsSyn		( TcMonoBinds, idsToMonoBinds )
 
 import Inst		( Inst, InstOrigin(..), LIE, emptyLIE, plusLIE, plusLIEs, newDicts, newMethod )
-import TcEnv		( TcId, ValueEnv, TcTyThing(..), tcAddImportedIdInfo,
+import TcEnv		( TcId, ValueEnv, TyThing(..), TyThingDetails(..), tcAddImportedIdInfo,
 			  tcLookupTy, tcExtendTyVarEnvForMeths, tcExtendGlobalTyVars,
-			  tcExtendLocalValEnv
+			  tcExtendLocalValEnv, tcExtendTyVarEnv
 			)
 import TcBinds		( tcBindWithSigs, tcSpecSigs )
 import TcTyDecls	( mkNewTyConRep )
-import TcMonad
-import TcMonoType	( kcHsType, tcHsTopType, tcExtendTopTyVarScope, 
-			  tcContext, checkSigTyVars, sigCtxt, mkTcSig
-			)
+import TcMonoType	( tcHsSigType, tcClassContext, checkSigTyVars, sigCtxt, mkTcSig )
 import TcSimplify	( tcSimplifyAndCheck, bindInstsOfLocalFuns )
-import TcType		( TcType, TcTyVar, tcInstTyVars, zonkTcTyVarBndr, tcGetTyVar )
+import TcType		( TcType, TcTyVar, tcInstTyVars, tcGetTyVar, zonkTcSigTyVars )
 import TcInstUtil	( classDataCon )
+import TcMonad
 import PrelInfo		( nO_METHOD_BINDING_ERROR_ID )
 import Bag		( unionManyBags, bagToList )
-import Class		( mkClass, classBigSig, classSelIds, Class, ClassOpItem )
+import Class		( classTyVars, classBigSig, classSelIds, classTyCon, Class, ClassOpItem )
 import CmdLineOpts      ( opt_GlasgowExts, opt_WarnMissingMethods )
 import MkId		( mkDictSelId, mkDataConId, mkDataConWrapId, mkDefaultMethodId )
 import DataCon		( mkDataCon, dataConId, dataConWrapId, notMarkedStrict )
@@ -50,7 +48,7 @@ import NameSet		( emptyNameSet )
 import Outputable
 import Type		( Type, ThetaType, ClassContext,
 			  mkFunTy, mkTyVarTy, mkTyVarTys, mkDictTy, mkDictTys,
-			  mkSigmaTy, mkForAllTys, mkClassPred, classesOfPreds,
+			  mkSigmaTy, mkClassPred, classesOfPreds,
 			  boxedTypeKind, mkArrowKind
 			)
 import Var		( tyVarKind, TyVar )
@@ -95,37 +93,6 @@ Now DictTy in Type is just a form of type synomym:
 Death to "ExpandingDicts".
 
 
-%************************************************************************
-%*									*
-\subsection{Kind checking}
-%*									*
-%************************************************************************
-
-\begin{code}
-kcClassDecl (ClassDecl	context class_name
-			tyvar_names fundeps class_sigs def_methods pragmas
-			_ _ _ _ src_loc)
-  =         -- CHECK ARITY 1 FOR HASKELL 1.4
-    checkTc (opt_GlasgowExts || length tyvar_names == 1)
-	    (classArityErr class_name)		`thenTc_`
-
-	-- Get the (mutable) class kind
-    tcLookupTy class_name			`thenNF_Tc` \ (kind, _) ->
-
-	-- Make suitable tyvars and do kind checking
-	-- The net effect is to mutate the class kind
-    tcExtendTopTyVarScope kind tyvar_names	$ \ _ _ ->
-    tcContext context				`thenTc_`
-    mapTc kc_sig the_class_sigs			`thenTc_`
-
-    returnTc ()
-  where
-    the_class_sigs = filter isClassOpSig class_sigs
-  
-    kc_sig (ClassOpSig _ _ _ op_ty loc) = tcAddSrcLoc loc (kcHsType op_ty)
-\end{code}
-
-
 %************************************************************************
 %*									*
 \subsection{Type checking}
@@ -133,40 +100,34 @@ kcClassDecl (ClassDecl	context class_name
 %************************************************************************
 
 \begin{code}
-tcClassDecl1 rec_env rec_vrcs
+tcClassDecl1 rec_env
       	     (ClassDecl context class_name
 			tyvar_names fundeps class_sigs def_methods pragmas 
 			tycon_name datacon_name datacon_wkr_name sc_sel_names src_loc)
-  = 	-- LOOK THINGS UP IN THE ENVIRONMENT
-    tcLookupTy class_name				`thenTc` \ (class_kind, AClass rec_class arity) ->
-    tcExtendTopTyVarScope class_kind tyvar_names	$ \ tyvars _ ->
-	-- The class kind is by now immutable
+  = 	-- CHECK ARITY 1 FOR HASKELL 1.4
+    checkTc (opt_GlasgowExts || length tyvar_names == 1)
+	    (classArityErr class_name)			`thenTc_`
+
+	-- LOOK THINGS UP IN THE ENVIRONMENT
+    tcLookupTy class_name				`thenTc` \ (AClass clas) ->
+    let
+	tyvars = classTyVars clas
+    in
+    tcExtendTyVarEnv tyvars			$ 
 	
 	-- CHECK THE CONTEXT
---  traceTc (text "tcClassCtxt" <+> ppr class_name)	`thenTc_`
-    tcClassContext class_name rec_class tyvars context sc_sel_names
-						`thenTc` \ (sc_theta, sc_tys, sc_sel_ids) ->
---  traceTc (text "tcClassCtxt done" <+> ppr class_name)	`thenTc_`
-
-	-- CHECK THE FUNCTIONAL DEPENDENCIES,
-    tcFundeps fundeps				`thenTc` \ fds ->
+    tcSuperClasses class_name clas
+		   context sc_sel_names		`thenTc` \ (sc_theta, sc_sel_ids) ->
 
 	-- CHECK THE CLASS SIGNATURES,
-    mapTc (tcClassSig rec_env rec_class tyvars) 
-	  (filter isClassOpSig class_sigs)
-						`thenTc` \ sig_stuff ->
+    mapTc (tcClassSig rec_env clas tyvars) 
+	  (filter isClassOpSig class_sigs)		`thenTc` \ sig_stuff ->
 
-	-- MAKE THE CLASS OBJECT ITSELF
+	-- MAKE THE CLASS DETAILS
     let
 	(op_tys, op_items) = unzip sig_stuff
-	clas = mkClass class_name tyvars fds
-		       sc_theta sc_sel_ids op_items
-		       tycon
-
+        sc_tys		   = mkDictTys sc_theta
 	dict_component_tys = sc_tys ++ op_tys
- 	new_or_data = case dict_component_tys of
-			[_]   -> NewTyCon (mkNewTyConRep tycon)
-			other -> DataTyCon
 
         dict_con = mkDataCon datacon_name
 			   [notMarkedStrict | _ <- dict_component_tys]
@@ -175,70 +136,45 @@ tcClassDecl1 rec_env rec_vrcs
 		      	   [{-No context-}]
 			   [{-No existential tyvars-}] [{-Or context-}]
 			   dict_component_tys
-		      	   tycon dict_con_id dict_wrap_id
+		      	   (classTyCon clas)
+			   dict_con_id dict_wrap_id
 
 	dict_con_id  = mkDataConId datacon_wkr_name dict_con
 	dict_wrap_id = mkDataConWrapId dict_con
-
-        argvrcs = lookupWithDefaultFM rec_vrcs (pprPanic "tcClassDecl1: argvrcs:" $
-                                                         ppr tycon_name)
-                                      tycon_name
-
-	tycon = mkClassTyCon tycon_name
-			     class_kind
-			     tyvars
-                             argvrcs
-			     dict_con		-- Constructors
-			     clas 		-- Yes!  It's a dictionary 
-			     new_or_data
     in
-    returnTc (class_name, AClass clas arity)
+    returnTc (class_name, ClassDetails sc_theta sc_sel_ids op_items dict_con)
 \end{code}
 
 \begin{code}
-tcFundeps = mapTc tc_fundep
-tc_fundep (us, vs) =
-    mapTc tc_fd_tyvar us	`thenTc` \ us' ->
-    mapTc tc_fd_tyvar vs	`thenTc` \ vs' ->
-    returnTc (us', vs')
-tc_fd_tyvar v =
-    tcLookupTy v	 `thenTc` \(_, ATyVar tv) ->
-    returnTc tv
-\end{code}
-
-\begin{code}
-tcClassContext :: Name -> Class -> [TyVar]
+tcSuperClasses :: Name -> Class
 	       -> RenamedContext 	-- class context
 	       -> [Name]		-- Names for superclass selectors
 	       -> TcM s (ClassContext,	-- the superclass context
-			 [Type],	-- types of the superclass dictionaries
 		         [Id])  	-- superclass selector Ids
 
-tcClassContext class_name rec_class rec_tyvars context sc_sel_names
+tcSuperClasses class_name clas context sc_sel_names
   = 	-- Check the context.
 	-- The renamer has already checked that the context mentions
 	-- only the type variable of the class decl.
 
 	-- For std Haskell check that the context constrains only tyvars
     (if opt_GlasgowExts then
-	returnTc []
+	returnTc ()
      else
-	mapTc check_constraint context
+	mapTc_ check_constraint context
     )					`thenTc_`
 
-    tcContext context			`thenTc` \ sc_theta ->
-
+	-- Context is already kind-checked
+    tcClassContext context			`thenTc` \ sc_theta ->
     let
-       sc_theta' = classesOfPreds sc_theta
-       sc_tys = mkDictTys sc_theta'
-       sc_sel_ids = [mkDictSelId sc_name rec_class | sc_name <- sc_sel_names]
+       sc_sel_ids = [mkDictSelId sc_name clas | sc_name <- sc_sel_names]
     in
 	-- Done
-    returnTc (sc_theta', sc_tys, sc_sel_ids)
+    returnTc (sc_theta, sc_sel_ids)
 
   where
-    check_constraint sc@(HsPClass c tys) = checkTc (all is_tyvar tys)
-						   (superClassErr class_name sc)
+    check_constraint sc@(HsPClass c tys) 
+	= checkTc (all is_tyvar tys) (superClassErr class_name sc)
 
     is_tyvar (HsTyVar _) = True
     is_tyvar other	 = False
@@ -252,9 +188,8 @@ tcClassSig :: ValueEnv		-- Knot tying only!
 		     ClassOpItem)	-- Selector Id, default-method Id, True if explicit default binding
 
 
-tcClassSig rec_env rec_clas rec_clas_tyvars
-	   (ClassOpSig op_name dm_name explicit_dm
-		       op_ty src_loc)
+tcClassSig rec_env clas clas_tyvars
+	   (ClassOpSig op_name dm_name explicit_dm op_ty src_loc)
   = tcAddSrcLoc src_loc $
 
 	-- Check the type signature.  NB that the envt *already has*
@@ -262,19 +197,17 @@ tcClassSig rec_env rec_clas rec_clas_tyvars
 
     -- NB: Renamer checks that the class type variable is mentioned in local_ty,
     -- and that it is not constrained by theta
---  traceTc (text "tcClassSig" <+> ppr op_name)	`thenTc_`
-    tcHsTopType op_ty				`thenTc` \ local_ty ->
+    tcHsSigType op_ty				`thenTc` \ local_ty ->
     let
-	global_ty   = mkSigmaTy rec_clas_tyvars 
-			        [mkClassPred rec_clas (mkTyVarTys rec_clas_tyvars)]
+	global_ty   = mkSigmaTy clas_tyvars 
+			        [mkClassPred clas (mkTyVarTys clas_tyvars)]
 			        local_ty
 
 	-- Build the selector id and default method id
-	sel_id      = mkDictSelId op_name rec_clas
-	dm_id	    = mkDefaultMethodId dm_name rec_clas global_ty
+	sel_id      = mkDictSelId op_name clas
+	dm_id	    = mkDefaultMethodId dm_name clas global_ty
 	final_dm_id = tcAddImportedIdInfo rec_env dm_id
     in
---  traceTc (text "tcClassSig done" <+> ppr op_name)	`thenTc_`
     returnTc (local_ty, (sel_id, final_dm_id, explicit_dm))
 \end{code}
 
@@ -331,7 +264,7 @@ tcClassDecl2 (ClassDecl context class_name
   | otherwise	-- It is locally defined
   = recoverNF_Tc (returnNF_Tc (emptyLIE, EmptyMonoBinds)) $ 
     tcAddSrcLoc src_loc		     		          $
-    tcLookupTy class_name				`thenNF_Tc` \ (_, AClass clas _) ->
+    tcLookupTy class_name				`thenNF_Tc` \ (AClass clas) ->
     tcDefaultMethodBinds clas default_binds class_sigs
 \end{code}
 
@@ -471,7 +404,7 @@ tcDefaultMethodBinds clas default_binds sigs
 	    -- tcMethodBind has checked that the class_tyvars havn't
 	    -- been unified with each other or another type, but we must
 	    -- still zonk them before passing them to tcSimplifyAndCheck
-	mapNF_Tc zonkTcTyVarBndr clas_tyvars	`thenNF_Tc` \ clas_tyvars' ->
+        zonkTcSigTyVars clas_tyvars	`thenNF_Tc` \ clas_tyvars' ->
     
 	    -- Check the context
 	tcSimplifyAndCheck
@@ -577,6 +510,8 @@ tcMethodBind clas origin inst_tyvars inst_tys inst_theta
 	-- Now check that the instance type variables
 	-- (or, in the case of a class decl, the class tyvars)
 	-- have not been unified with anything in the environment
+	--	
+	-- We do this for each method independently to localise error messages
    tcAddErrCtxtM (sigCtxt sig_msg inst_tyvars inst_theta (idType meth_id))	$
    checkSigTyVars inst_tyvars emptyVarSet					`thenTc_` 
 
diff --git a/ghc/compiler/typecheck/TcEnv.lhs b/ghc/compiler/typecheck/TcEnv.lhs
index c99244d20496f343590c1e4db1fab79ede3530db..ab3021767fb21111d089b157caba1158e98c69c4 100644
--- a/ghc/compiler/typecheck/TcEnv.lhs
+++ b/ghc/compiler/typecheck/TcEnv.lhs
@@ -3,13 +3,14 @@ module TcEnv(
 	TcId, TcIdSet, tcInstId,
 	tcLookupDataCon,
 
-	TcEnv, ValueEnv, TcTyThing(..),
+	TcEnv, ValueEnv, TyThing(..), TyThingDetails(..), tyThingKind, 
 
-	initEnv, getEnvTyCons, getEnvClasses, getEnvAllTyCons,
+	initEnv, getEnvTyCons, getEnvClasses, 
 	
         tcExtendUVarEnv, tcLookupUVar,
 
-	tcExtendTyVarEnv, tcExtendTyVarEnvForMeths, tcExtendTypeEnv, tcGetInScopeTyVars,
+	tcExtendKindEnv, tcExtendTyVarEnv, 
+	tcExtendTyVarEnvForMeths, tcExtendTypeEnv, tcGetInScopeTyVars,
 
 	tcLookupTy,
 	tcLookupTyConByKey, 
@@ -43,11 +44,11 @@ import Var	( TyVar, Id, setVarName,
 		)
 import TcType	( TcType, TcTyVar, TcTyVarSet, TcThetaType,
 		  tcInstTyVars, zonkTcTyVars,
-		  TcKind, kindToTcKind
+		  TcKind, 
 		)
 import VarSet
 import Type	( Kind, Type, superKind,
-		  tyVarsOfType, tyVarsOfTypes, mkTyVarTy,
+		  tyVarsOfType, tyVarsOfTypes,
 		  splitForAllTys, splitRhoTy, splitFunTys,
 		  splitAlgTyConApp_maybe, getTyVar
 		)
@@ -55,7 +56,7 @@ import Subst	( substTy )
 import UsageSPUtils ( unannotTy )
 import DataCon	( DataCon )
 import TyCon	( TyCon, tyConKind, tyConArity, isSynTyCon )
-import Class	( Class, classTyCon )
+import Class	( Class, ClassOpItem, ClassContext, classTyCon )
 
 import TcMonad
 
@@ -64,8 +65,8 @@ import IdInfo		( vanillaIdInfo )
 import Name		( Name, OccName, nameOccName, getSrcLoc,
 			  maybeWiredInTyConName, maybeWiredInIdName, isLocallyDefined,
 			  NamedThing(..), 
-			  NameEnv, emptyNameEnv, addToNameEnv, 
-				   extendNameEnv, lookupNameEnv, nameEnvElts
+			  NameEnv, emptyNameEnv, lookupNameEnv, nameEnvElts, 
+				   extendNameEnv, extendNameEnvList
 			)
 import Unify		( unifyTyListsX, matchTys )
 import Unique		( pprUnique10, Unique, Uniquable(..) )
@@ -153,41 +154,40 @@ data TcEnv = TcEnv
 					-- Includes the in-scope tyvars
 
 type UsageEnv   = NameEnv UVar
-type TypeEnv	= NameEnv (TcKind, TcTyThing)
+type TypeEnv	= NameEnv TyThing
 type ValueEnv	= NameEnv Id	
 
 valueEnvIds :: ValueEnv -> [Id]
 valueEnvIds ve = nameEnvElts ve
 
-data TcTyThing = ATyVar TcTyVar		-- Mutable only so that the kind can be mutable
-					-- if the kind is mutable, the tyvar must be so that
-					-- zonking works
-	       | ADataTyCon TyCon
-	       | ASynTyCon TyCon Arity
-	       | AClass Class Arity
-
+data TyThing = ATyVar TyVar
+	     | ATyCon TyCon
+	     | AClass Class
+	     | AThing TcKind	-- Used temporarily, during kind checking
+-- For example, when 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
+
+tyThingKind :: TyThing -> TcKind
+tyThingKind (ATyVar tv) = tyVarKind tv
+tyThingKind (ATyCon tc) = tyConKind tc
+tyThingKind (AClass cl) = tyConKind (classTyCon cl)	-- For some odd reason, 
+							-- a class doesn't include its kind
+tyThingKind (AThing k)  = k
+
+data TyThingDetails = SynTyDetails Type
+		    | DataTyDetails ClassContext [DataCon] [Class]
+		    | ClassDetails ClassContext [Id] [ClassOpItem] DataCon
 
 initEnv :: TcRef TcTyVarSet -> TcEnv
 initEnv mut = TcEnv emptyNameEnv emptyNameEnv emptyNameEnv emptyInstEnv (emptyVarSet, mut)
 
-getEnvClasses (TcEnv _ te _ _ _) = [cl | (_, AClass cl _) <- nameEnvElts te]
-
-getEnvTyCons  (TcEnv _ te _ _ _) = catMaybes (map get_tc (nameEnvElts te))
-    where
-      get_tc (_, ADataTyCon tc)  = Just tc
-      get_tc (_, ASynTyCon tc _) = Just tc
-      get_tc other		 = Nothing
-
-getEnvAllTyCons te_list = catMaybes (map get_tc te_list)
-	-- The 'all' means 'including the tycons from class decls'
-    where                          
-      get_tc (_, ADataTyCon tc)  = Just tc
-      get_tc (_, ASynTyCon tc _) = Just tc
-      get_tc (_, AClass cl _)    = Just (classTyCon cl)
-      get_tc other               = Nothing
+getEnvClasses (TcEnv _ te _ _ _) = [cl | AClass cl <- nameEnvElts te]
+getEnvTyCons  (TcEnv _ te _ _ _) = [tc | ATyCon tc <- nameEnvElts te]
 \end{code}
 
-
 %************************************************************************
 %*									*
 \subsection{The usage environment}
@@ -200,7 +200,7 @@ Extending the usage environment
 tcExtendUVarEnv :: Name -> UVar -> TcM s r -> TcM s r
 tcExtendUVarEnv uv_name uv scope
   = tcGetEnv                 `thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
-    tcSetEnv (TcEnv (addToNameEnv ue uv_name uv) te ve ie gtvs) scope
+    tcSetEnv (TcEnv (extendNameEnv ue uv_name uv) te ve ie gtvs) scope
 \end{code}
 
 Looking up in the environments.
@@ -222,14 +222,20 @@ tcLookupUVar uv_name
 %************************************************************************
 
 \begin{code}
+tcExtendKindEnv :: [(Name,TcKind)] -> TcM s r -> TcM s r
+tcExtendKindEnv pairs scope
+  = tcGetEnv				`thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
+    let
+ 	te' = extendNameEnvList te [(n, AThing k) | (n,k) <- pairs]
+	-- No need to extend global tyvars for kind checking
+    in
+    tcSetEnv (TcEnv ue te' ve ie gtvs) scope
+    
 tcExtendTyVarEnv :: [TyVar] -> TcM s r -> TcM s r
 tcExtendTyVarEnv tyvars scope
   = tcGetEnv				`thenNF_Tc` \ (TcEnv ue te ve ie (in_scope_tvs, gtvs)) ->
     let
-	extend_list = [ (getName tv, (kindToTcKind (tyVarKind tv), ATyVar tv))
-		      | tv <- tyvars
-		      ]
- 	te'           = extendNameEnv te extend_list
+ 	te'           = extendNameEnvList te [ (getName tv, ATyVar tv) | tv <- tyvars]
 	new_tv_set    = mkVarSet tyvars
 	in_scope_tvs' = in_scope_tvs `unionVarSet` new_tv_set
     in
@@ -252,11 +258,11 @@ tcExtendTyVarEnvForMeths :: [TyVar] -> [TcTyVar] -> TcM s r -> TcM s r
 tcExtendTyVarEnvForMeths sig_tyvars inst_tyvars thing_inside
   = tcGetEnv					`thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
     let
-	te' = extendNameEnv te stuff
+	te' = extendNameEnvList te stuff
     in
     tcSetEnv (TcEnv ue te' ve ie gtvs) thing_inside
   where
-    stuff = [ (getName sig_tv, (kindToTcKind (tyVarKind inst_tv), ATyVar inst_tv))
+    stuff = [ (getName sig_tv, ATyVar inst_tv)
 	    | (sig_tv, inst_tv) <- zipEqual "tcMeth" sig_tyvars inst_tyvars
 	    ]
 
@@ -299,13 +305,13 @@ tcGetInScopeTyVars
 Type constructors and classes
 
 \begin{code}
-tcExtendTypeEnv :: [(Name, (TcKind, TcTyThing))] -> TcM s r -> TcM s r
+tcExtendTypeEnv :: [(Name, TyThing)] -> TcM s r -> TcM s r
 tcExtendTypeEnv bindings scope
-  = ASSERT( null [tv | (_, (_,ATyVar tv)) <- bindings] )
+  = ASSERT( null [tv | (_, ATyVar tv) <- bindings] )
 	-- Not for tyvars; use tcExtendTyVarEnv
-    tcGetEnv					`thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
+    tcGetEnv				`thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
     let
-	te' = extendNameEnv te bindings
+	te' = extendNameEnvList te bindings
     in
     tcSetEnv (TcEnv ue te' ve ie gtvs) scope
 \end{code}
@@ -314,7 +320,7 @@ tcExtendTypeEnv bindings scope
 Looking up in the environments.
 
 \begin{code}
-tcLookupTy :: Name ->  NF_TcM s (TcKind, TcTyThing)
+tcLookupTy :: Name ->  NF_TcM s TyThing
 tcLookupTy name
   = tcGetEnv	`thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
     case lookupNameEnv te name of {
@@ -322,8 +328,7 @@ tcLookupTy name
  	Nothing    -> 
 
     case maybeWiredInTyConName name of
-	Just tc | isSynTyCon tc -> returnNF_Tc (kindToTcKind (tyConKind tc), ASynTyCon tc (tyConArity tc))
-		| otherwise     -> returnNF_Tc (kindToTcKind (tyConKind tc), ADataTyCon tc)
+	Just tc -> returnNF_Tc (ATyCon tc)
 
 	Nothing -> 	-- This can happen if an interface-file
 			-- unfolding is screwed up
@@ -334,23 +339,22 @@ tcLookupClassByKey :: Unique -> NF_TcM s Class
 tcLookupClassByKey key
   = tcGetEnv		`thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
     case lookupUFM_Directly te key of
-	Just (_, AClass cl _) -> returnNF_Tc cl
-	other		      -> pprPanic "tcLookupClassByKey:" (pprUnique10 key)
+	Just (AClass cl) -> returnNF_Tc cl
+	other		 -> pprPanic "tcLookupClassByKey:" (pprUnique10 key)
 
 tcLookupClassByKey_maybe :: Unique -> NF_TcM s (Maybe Class)
 tcLookupClassByKey_maybe key
   = tcGetEnv		`thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
     case lookupUFM_Directly te key of
-	Just (_, AClass cl _) -> returnNF_Tc (Just cl)
-	other		      -> returnNF_Tc Nothing
+	Just (AClass cl) -> returnNF_Tc (Just cl)
+	other		 -> returnNF_Tc Nothing
 
 tcLookupTyConByKey :: Unique -> NF_TcM s TyCon
 tcLookupTyConByKey key
   = tcGetEnv		`thenNF_Tc` \ (TcEnv ue te ve ie gtvs) ->
     case lookupUFM_Directly te key of
-	Just (_, ADataTyCon tc)  -> returnNF_Tc tc
-	Just (_, ASynTyCon tc _) -> returnNF_Tc tc
-	other		         -> pprPanic "tcLookupTyConByKey:" (pprUnique10 key)
+	Just (ATyCon tc)  -> returnNF_Tc tc
+	other		  -> pprPanic "tcLookupTyConByKey:" (pprUnique10 key)
 \end{code}
 
 
@@ -376,7 +380,7 @@ tcExtendLocalValEnv names_w_ids scope
   = tcGetEnv		`thenNF_Tc` \ (TcEnv ue te ve ie (in_scope_tvs,gtvs)) ->
     tcReadMutVar gtvs	`thenNF_Tc` \ global_tvs ->
     let
-	ve'		    = extendNameEnv ve names_w_ids
+	ve'		    = extendNameEnvList ve names_w_ids
 	extra_global_tyvars = tyVarsOfTypes (map (idType . snd) names_w_ids)
     in
     tc_extend_gtvs gtvs extra_global_tyvars	`thenNF_Tc` \ gtvs' ->
@@ -445,8 +449,7 @@ tcAddImportedIdInfo unf_env id
   = id `lazySetIdInfo` new_info
 	-- The Id must be returned without a data dependency on maybe_id
   where
-    new_info = -- pprTrace "tcAdd" (ppr id) $
-	       case explicitLookupValue unf_env (getName id) of
+    new_info = case explicitLookupValue unf_env (getName id) of
 		     Nothing	      -> vanillaIdInfo
 		     Just imported_id -> idInfo imported_id
 		-- ToDo: could check that types are the same
diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs
index d171a36d80c12546f18968826e816ceabca55832..649722118fda8357cd4e9fd2fe198cecab09ab2d 100644
--- a/ghc/compiler/typecheck/TcExpr.lhs
+++ b/ghc/compiler/typecheck/TcExpr.lhs
@@ -42,7 +42,7 @@ import TcImprove	( tcImprove )
 import TcType		( TcType, TcTauType,
 			  tcInstTyVars,
 			  tcInstTcType, tcSplitRhoTy,
-			  newTyVarTy, newTyVarTy_OpenKind, zonkTcType )
+			  newTyVarTy, newTyVarTys, zonkTcType )
 
 import FieldLabel	( FieldLabel, fieldLabelName, fieldLabelType, fieldLabelTyCon )
 import Id		( idType, recordSelectorFieldLabel, isRecordSelector,
@@ -59,7 +59,7 @@ import Type		( mkFunTy, mkAppTy, mkTyVarTy, mkTyVarTys,
 			  splitRhoTy,
 			  isTauTy, tyVarsOfType, tyVarsOfTypes, 
 			  isSigmaTy, splitAlgTyConApp, splitAlgTyConApp_maybe,
-			  boxedTypeKind, mkArrowKind,
+			  boxedTypeKind, openTypeKind, mkArrowKind,
 			  tidyOpenType
 			)
 import TyCon		( TyCon, tyConTyVars )
@@ -371,7 +371,7 @@ tcMonoExpr (HsCCall lbl args may_gc is_asm ignored_fake_result_ty) res_ty
 	tv_idxs | n_args == 0 = []
 		| otherwise   = [1..n_args]
     in
-    mapNF_Tc (\ _ -> newTyVarTy_OpenKind) tv_idxs	`thenNF_Tc` \ arg_tys ->
+    newTyVarTys (length tv_idxs) openTypeKind		`thenNF_Tc` \ arg_tys ->
     tcMonoExprs args arg_tys		   		`thenTc`    \ (args', args_lie) ->
 
 	-- The argument types can be unboxed or boxed; the result
@@ -747,7 +747,7 @@ tcMonoExpr (HsWith expr binds) res_ty
 	revBinds b = b
 
 tcIPBinds ((name, expr) : binds)
-  = newTyVarTy_OpenKind		`thenTc` \ ty ->
+  = newTyVarTy openTypeKind	`thenTc` \ ty ->
     tcGetSrcLoc			`thenTc` \ loc ->
     let id = ipToId name ty loc in
     tcMonoExpr expr ty		`thenTc` \ (expr', lie) ->
@@ -782,7 +782,7 @@ tcExpr_id id_expr
  = case id_expr of
 	HsVar name -> tcId name			`thenNF_Tc` \ stuff -> 
 		      returnTc stuff
-	other	   -> newTyVarTy_OpenKind	`thenNF_Tc` \ id_ty ->
+	other	   -> newTyVarTy openTypeKind	`thenNF_Tc` \ id_ty ->
 		      tcMonoExpr id_expr id_ty	`thenTc`    \ (id_expr', lie_id) ->
 		      returnTc (id_expr', lie_id, id_ty) 
 \end{code}
diff --git a/ghc/compiler/typecheck/TcForeign.lhs b/ghc/compiler/typecheck/TcForeign.lhs
index 7e4140799b175208e5fa1e890c4c7edf4baa3ae0..69991070609ae2920b943f8b9962973aa0f02133 100644
--- a/ghc/compiler/typecheck/TcForeign.lhs
+++ b/ghc/compiler/typecheck/TcForeign.lhs
@@ -27,8 +27,8 @@ import RnHsSyn		( RenamedHsDecl, RenamedForeignDecl )
 
 import TcMonad
 import TcEnv		( newLocalId )
-import TcType		( typeToTcType, tcSplitRhoTy, zonkTcTypeToType )
-import TcMonoType	( tcHsTopBoxedType )
+import TcType		( tcSplitRhoTy, zonkTcTypeToType )
+import TcMonoType	( tcHsBoxedSigType )
 import TcHsSyn		( TcMonoBinds, TypecheckedForeignDecl,
 			  TcForeignExportDecl )
 import TcExpr		( tcId, tcPolyExpr )			
@@ -84,7 +84,7 @@ tcFImport :: RenamedForeignDecl -> TcM s (Id, TypecheckedForeignDecl)
 tcFImport fo@(ForeignDecl nm FoExport hs_ty Dynamic cconv src_loc) =
    tcAddSrcLoc src_loc		     $
    tcAddErrCtxt (foreignDeclCtxt fo) $
-   tcHsTopBoxedType hs_ty	     `thenTc`	\ sig_ty ->
+   tcHsBoxedSigType hs_ty	     `thenTc`	\ sig_ty ->
    let
       -- drop the foralls before inspecting the structure
       -- of the foreign type.
@@ -99,7 +99,7 @@ tcFImport fo@(ForeignDecl nm FoExport hs_ty Dynamic cconv src_loc) =
 tcFImport fo@(ForeignDecl nm FoLabel hs_ty ext_nm cconv src_loc) =
    tcAddSrcLoc src_loc		     $
    tcAddErrCtxt (foreignDeclCtxt fo) $
-   tcHsTopBoxedType hs_ty	    `thenTc`	\ sig_ty ->
+   tcHsBoxedSigType hs_ty	    `thenTc`	\ sig_ty ->
    let
       -- drop the foralls before inspecting the structure
       -- of the foreign type.
@@ -113,7 +113,7 @@ tcFImport fo@(ForeignDecl nm imp_exp@(FoImport isUnsafe) hs_ty ext_nm cconv src_
    tcAddSrcLoc src_loc		     $
    tcAddErrCtxt (foreignDeclCtxt fo) $
 
-   tcHsTopBoxedType hs_ty	     `thenTc` \ ty ->
+   tcHsBoxedSigType hs_ty	     `thenTc` \ ty ->
     -- Check that the type has the right shape
     -- and that the argument and result types are acceptable.
    let
@@ -132,9 +132,8 @@ tcFExport fo@(ForeignDecl nm imp_exp hs_ty ext_nm cconv src_loc) =
    tcAddSrcLoc src_loc		     $
    tcAddErrCtxt (foreignDeclCtxt fo) $
 
-   tcHsTopBoxedType hs_ty	       `thenTc`	\ sig_ty ->
-   let sig_tc_ty = typeToTcType sig_ty in
-   tcPolyExpr (HsVar nm) sig_tc_ty     `thenTc`    \ (rhs, lie, _, _, _) ->
+   tcHsBoxedSigType hs_ty	       `thenTc`	\ sig_ty ->
+   tcPolyExpr (HsVar nm) sig_ty     `thenTc`    \ (rhs, lie, _, _, _) ->
 
    let
       -- drop the foralls before inspecting the structure
@@ -148,7 +147,7 @@ tcFExport fo@(ForeignDecl nm imp_exp hs_ty ext_nm cconv src_loc) =
 	  -- than its declared/inferred type. Hence the need
 	  -- to create a local binding which will call the exported function
 	  -- at a particular type (and, maybe, overloading).
-	newLocalId (nameOccName nm) sig_tc_ty src_loc	`thenNF_Tc` \ i ->
+	newLocalId (nameOccName nm) sig_ty src_loc	`thenNF_Tc` \ i ->
 	let
 	    bind  = VarMonoBind i rhs
 	in
diff --git a/ghc/compiler/typecheck/TcGenDeriv.lhs b/ghc/compiler/typecheck/TcGenDeriv.lhs
index b19f84e434b094defafcafdf0966f38a1b2d24b4..fb87c891222bf0a824975a3ae3dcbad810710206 100644
--- a/ghc/compiler/typecheck/TcGenDeriv.lhs
+++ b/ghc/compiler/typecheck/TcGenDeriv.lhs
@@ -1023,8 +1023,6 @@ gen_Show_binds fixity_env tycon
 				 (map show_label labels) 
 				 real_show_thingies
 			       
-	     (con_left_assoc, con_right_assoc) = isLRAssoc fixity_env dc_nm
-
 	      {-
 	        c.f. Figure 16 and 17 in Haskell 1.1 report
 	      -}  
diff --git a/ghc/compiler/typecheck/TcHsSyn.lhs b/ghc/compiler/typecheck/TcHsSyn.lhs
index 1252cfd913dec93742809473c73950a1ef2ba6af..102071b91b9596c2c5afacaee17b102b74ce5823 100644
--- a/ghc/compiler/typecheck/TcHsSyn.lhs
+++ b/ghc/compiler/typecheck/TcHsSyn.lhs
@@ -47,7 +47,7 @@ import TcEnv	( tcLookupValueMaybe, tcExtendGlobalValEnv, tcGetValueEnv,
 
 import TcMonad
 import TcType	( TcType, TcTyVar,
-		  zonkTcTypeToType, zonkTcTyVarToTyVar, zonkTcTyVarBndr, zonkTcType
+		  zonkTcTypeToType, zonkTcTyVarToTyVar, zonkTcType, zonkTcSigTyVars
 		)
 import Name	( isLocallyDefined )
 import CoreSyn  ( Expr )
@@ -276,9 +276,11 @@ zonkMonoBinds (AbsBinds tyvars dicts exports inlines val_bind)
 		 new_globals)
   where
     zonkExport (tyvars, global, local)
-	= mapNF_Tc zonkTcTyVarBndr tyvars	`thenNF_Tc` \ new_tyvars ->
-	  zonkIdBndr global			`thenNF_Tc` \ new_global ->
-	  zonkIdOcc local			`thenNF_Tc` \ new_local -> 
+	= zonkTcSigTyVars tyvars	`thenNF_Tc` \ new_tyvars ->
+		-- This isn't the binding occurrence of these tyvars
+		-- but they should *be* tyvars.  Hence zonkTcSigTyVars.
+	  zonkIdBndr global		`thenNF_Tc` \ new_global ->
+	  zonkIdOcc local		`thenNF_Tc` \ new_local -> 
 	  returnNF_Tc (new_tyvars, new_global, new_local)
 \end{code}
 
diff --git a/ghc/compiler/typecheck/TcIfaceSig.lhs b/ghc/compiler/typecheck/TcIfaceSig.lhs
index 27b4f1845fca6aaa15b1ad9074d0152c0f9b92df..4bce6a4b00554b0ba889588035e616467b05e416 100644
--- a/ghc/compiler/typecheck/TcIfaceSig.lhs
+++ b/ghc/compiler/typecheck/TcIfaceSig.lhs
@@ -10,12 +10,11 @@ module TcIfaceSig ( tcInterfaceSigs, tcVar, tcCoreExpr, tcCoreLamBndrs ) where
 
 import HsSyn		( HsDecl(..), IfaceSig(..), HsTupCon(..) )
 import TcMonad
-import TcMonoType	( tcHsType, tcHsTypeKind, 
+import TcMonoType	( tcHsType )
 				-- NB: all the tyars in interface files are kinded,
 				-- so tcHsType will do the Right Thing without
 				-- having to mess about with zonking
-			  tcExtendTyVarScope
-			)
+
 import TcEnv		( ValueEnv, tcExtendTyVarEnv, 
 			  tcExtendGlobalValEnv, tcSetValueEnv,
 			  tcLookupValueMaybe,
@@ -186,7 +185,7 @@ UfCore expressions.
 tcCoreExpr :: UfExpr Name -> TcM s CoreExpr
 
 tcCoreExpr (UfType ty)
-  = tcHsTypeKind ty	`thenTc` \ (_, ty') ->
+  = tcHsType ty		`thenTc` \ ty' ->
 	-- It might not be of kind type
     returnTc (Type ty')
 
diff --git a/ghc/compiler/typecheck/TcInstDcls.lhs b/ghc/compiler/typecheck/TcInstDcls.lhs
index e55ea763f1fb13cda7b5037e2b0741f23b2d6c0a..fd2b5dd881f5a04f15dc6a83455b0123eca6ebc5 100644
--- a/ghc/compiler/typecheck/TcInstDcls.lhs
+++ b/ghc/compiler/typecheck/TcInstDcls.lhs
@@ -28,9 +28,9 @@ import TcEnv		( ValueEnv, tcExtendGlobalValEnv, tcExtendTyVarEnvForMeths,
 			  tcAddImportedIdInfo, tcInstId
 			)
 import TcInstUtil	( InstInfo(..), classDataCon )
-import TcMonoType	( tcHsTopType )
+import TcMonoType	( tcHsSigType )
 import TcSimplify	( tcSimplifyAndCheck )
-import TcType		( TcTyVar, zonkTcTyVarBndr )
+import TcType		( TcTyVar, zonkTcSigTyVars )
 
 import Bag		( emptyBag, unitBag, unionBags, unionManyBags,
 			  foldBag, Bag
@@ -169,7 +169,7 @@ tcInstDecl1 unf_env (InstDecl poly_ty binds uprags dfun_name src_loc)
     tcAddSrcLoc src_loc			$
 
 	-- Type-check all the stuff before the "where"
-    tcHsTopType poly_ty			`thenTc` \ poly_ty' ->
+    tcHsSigType poly_ty			`thenTc` \ poly_ty' ->
     let
 	(tyvars, theta, dict_ty) = splitSigmaTy poly_ty'
 	constr			 = classesOfPreds theta
@@ -365,8 +365,8 @@ tcInstDecl2 (InstInfo clas inst_tyvars inst_tys
 
 	-- tcMethodBind has checked that the class_tyvars havn't
 	-- been unified with each other or another type, but we must
-	-- still zonk them
-    mapNF_Tc zonkTcTyVarBndr inst_tyvars' 	`thenNF_Tc` \ zonked_inst_tyvars ->
+	-- still zonk them before passing them to tcSimplifyAndCheck
+    zonkTcSigTyVars inst_tyvars' 	`thenNF_Tc` \ zonked_inst_tyvars ->
     let
         inst_tyvars_set = mkVarSet zonked_inst_tyvars
 
diff --git a/ghc/compiler/typecheck/TcMatches.lhs b/ghc/compiler/typecheck/TcMatches.lhs
index 4d73dbe36bc00ba61c9293b9be1d55be0e6569e6..edebb87d88ef178e2f3e11679ae5c399e3ae4e41 100644
--- a/ghc/compiler/typecheck/TcMatches.lhs
+++ b/ghc/compiler/typecheck/TcMatches.lhs
@@ -13,17 +13,17 @@ import {-# SOURCE #-}	TcExpr( tcExpr )
 import HsSyn		( HsBinds(..), Match(..), GRHSs(..), GRHS(..),
 			  MonoBinds(..), StmtCtxt(..), Stmt(..),
 			  pprMatch, getMatchLoc, consLetStmt,
-			  mkMonoBind
+			  mkMonoBind, collectSigTysFromPats
 			)
 import RnHsSyn		( RenamedMatch, RenamedGRHSs, RenamedStmt )
 import TcHsSyn		( TcMatch, TcGRHSs, TcStmt )
 
 import TcMonad
-import TcMonoType	( checkSigTyVars, tcHsTyVar, tcHsSigType, sigPatCtxt )
+import TcMonoType	( kcHsSigType, kcTyVarScope, checkSigTyVars, tcHsTyVar, tcHsSigType, sigPatCtxt )
 import Inst		( Inst, LIE, plusLIE, emptyLIE, plusLIEs )
-import TcEnv		( tcExtendLocalValEnv, tcExtendGlobalTyVars, tcExtendTyVarEnv, tcGetGlobalTyVars )
+import TcEnv		( tcExtendTyVarEnv, tcExtendLocalValEnv, tcExtendGlobalTyVars, tcGetGlobalTyVars )
 import TcPat		( tcPat, tcPatBndr_NoSigs, polyPatSig )
-import TcType		( TcType, newTyVarTy, newTyVarTy_OpenKind, zonkTcTyVars )
+import TcType		( TcType, newTyVarTy )
 import TcBinds		( tcBindsAndThen )
 import TcSimplify	( tcSimplifyAndCheck, bindInstsOfLocalFuns )
 import TcUnify		( unifyFunTy, unifyTauTy )
@@ -31,7 +31,7 @@ import Name		( Name )
 import TysWiredIn	( boolTy )
 
 import BasicTypes	( RecFlag(..) )
-import Type		( Kind, tyVarsOfType, isTauTy, mkFunTy, boxedTypeKind )
+import Type		( Kind, tyVarsOfType, isTauTy, mkFunTy, boxedTypeKind, openTypeKind )
 import VarSet
 import Var		( Id )
 import Bag
@@ -88,7 +88,7 @@ tcMatchesCase :: [RenamedMatch]		-- The case alternatives
 			LIE)
 
 tcMatchesCase matches expr_ty
-  = newTyVarTy_OpenKind 					`thenNF_Tc` \ scrut_ty ->
+  = newTyVarTy openTypeKind 					`thenNF_Tc` \ scrut_ty ->
     tcMatches [] matches (mkFunTy scrut_ty expr_ty) CaseAlt	`thenTc` \ (matches', lie) ->
     returnTc (scrut_ty, matches', lie)
 
@@ -138,12 +138,12 @@ tcMatch xve1 match@(Match sig_tvs pats maybe_rhs_sig grhss) expected_ty ctxt
 	-- If there are sig tvs we must be careful *not* to use
 	-- expected_ty right away, else we'll unify with tyvars free
 	-- in the envt.  So invent a fresh tyvar and use that instead
-	newTyVarTy_OpenKind		`thenNF_Tc` \ tyvar_ty ->
+	newTyVarTy openTypeKind		`thenNF_Tc` \ tyvar_ty ->
 
 	-- Extend the tyvar env and check the match itself
-	mapNF_Tc tcHsTyVar sig_tvs 	`thenNF_Tc` \ sig_tyvars ->
+	kcTyVarScope sig_tvs (mapTc_ kcHsSigType sig_tys)	`thenTc` \ sig_tyvars ->
 	tcExtendTyVarEnv sig_tyvars (
-		tc_match tyvar_ty
+		tc_match tyvar_ty	
 	)				`thenTc` \ (pat_ids, match_and_lie) ->
 
 	-- Check that the scoped type variables from the patterns
@@ -158,6 +158,9 @@ tcMatch xve1 match@(Match sig_tvs pats maybe_rhs_sig grhss) expected_ty ctxt
 	returnTc match_and_lie
 
   where
+    sig_tys = case maybe_rhs_sig of { Just t -> [t]; Nothing -> [] }
+	      ++ collectSigTysFromPats pats
+	      
     tc_match expected_ty 	-- Any sig tyvars are in scope by now
       = -- STEP 1: Typecheck the patterns
 	tcMatchPats pats expected_ty	`thenTc` \ (rhs_ty, pats', lie_req1, ex_tvs, pat_bndrs, lie_avail) ->
@@ -174,7 +177,7 @@ tcMatch xve1 match@(Match sig_tvs pats maybe_rhs_sig grhss) expected_ty ctxt
 	-- STEP 3: Unify with the rhs type signature if any
 	(case maybe_rhs_sig of
 	    Nothing  -> returnTc ()
-	    Just sig -> tcHsSigType sig	`thenTc` \ sig_ty ->
+	    Just sig -> tcHsSigType sig		`thenTc` \ sig_ty ->
 
 			-- Check that the signature isn't a polymorphic one, which
 			-- we don't permit (at present, anyway)
@@ -288,7 +291,7 @@ tcStmts do_or_lc m (stmt@(ExprStmt exp src_loc) : stmts) elt_ty
     tcAddSrcLoc src_loc 		(
 	tcSetErrCtxt (stmtCtxt do_or_lc stmt)	$
 	    -- exp has type (m tau) for some tau (doesn't matter what)
-  	newTyVarTy_OpenKind			`thenNF_Tc` \ any_ty ->
+  	newTyVarTy openTypeKind		`thenNF_Tc` \ any_ty ->
   	tcExpr exp (m any_ty)
     )					`thenTc` \ (exp', exp_lie) ->
     tcStmts do_or_lc m stmts elt_ty	`thenTc` \ (stmts', stmts_lie) ->
diff --git a/ghc/compiler/typecheck/TcModule.lhs b/ghc/compiler/typecheck/TcModule.lhs
index d10c84b307d1586a701c9681ba36a65162a105a2..f4a3934faebe4d0d2e86cc0b527d226ea52f9468 100644
--- a/ghc/compiler/typecheck/TcModule.lhs
+++ b/ghc/compiler/typecheck/TcModule.lhs
@@ -27,9 +27,9 @@ import TcClassDcl	( tcClassDecls2, mkImplicitClassBinds )
 import TcDefaults	( tcDefaults )
 import TcEnv		( tcExtendGlobalValEnv, tcExtendTypeEnv,
 			  getEnvTyCons, getEnvClasses, tcLookupValueByKeyMaybe,
-			  explicitLookupValueByKey, tcSetValueEnv, tcSetInstEnv,
+			  tcSetValueEnv, tcSetInstEnv,
 			  initEnv, 
-			  ValueEnv, TcTyThing(..)
+			  ValueEnv, 
 			)
 import TcRules		( tcRules )
 import TcForeign	( tcForeignImports, tcForeignExports )
@@ -39,10 +39,7 @@ import TcInstUtil	( buildInstanceEnv, InstInfo )
 import TcSimplify	( tcSimplifyTop )
 import TcTyClsDecls	( tcTyAndClassDecls )
 import TcTyDecls	( mkImplicitDataBinds )
-import TcType		( TcType, typeToTcType,
-			  TcKind, kindToTcKind,
-			  newTyVarTy
-			)
+import TcType		( TcType, TcKind )
 
 import RnMonad		( RnNameSupply, FixityEnv )
 import Bag		( isEmptyBag )
@@ -171,14 +168,6 @@ tcModule rn_name_supply fixities
     	tcDefaults decls		`thenTc` \ defaulting_tys ->
     	tcSetDefaultTys defaulting_tys 	$
     	
-	-- Extend the TyCon envt with the tycons corresponding to
-	-- the classes.
-	--  They are mentioned in types in interface files.
-        tcExtendTypeEnv [ (getName tycon, (kindToTcKind (tyConKind tycon), ADataTyCon tycon))
-		        | clas <- classes,
-			  let tycon = classTyCon clas
-		        ]				$
-
 	-- Interface type signatures
 	-- We tie a knot so that the Ids read out of interfaces are in scope
 	--   when we read their pragmas.
diff --git a/ghc/compiler/typecheck/TcMonad.lhs b/ghc/compiler/typecheck/TcMonad.lhs
index 8e4b1906250f853915af69ebbfdfb16250f635a0..0f86e0743695b92d93e20290c232655c12949dd7 100644
--- a/ghc/compiler/typecheck/TcMonad.lhs
+++ b/ghc/compiler/typecheck/TcMonad.lhs
@@ -8,7 +8,7 @@ module TcMonad(
 	TcM, NF_TcM, TcDown, TcEnv, 
 
 	initTc,
-	returnTc, thenTc, thenTc_, mapTc, listTc,
+	returnTc, thenTc, thenTc_, mapTc, mapTc_, listTc,
 	foldrTc, foldlTc, mapAndUnzipTc, mapAndUnzip3Tc,
 	mapBagTc, fixTc, tryTc, tryTc_, getErrsTc, 
 	traceTc, ioToTc,
@@ -166,11 +166,14 @@ listTc (x:xs) = x			`thenTc` \ r ->
 		returnTc (r:rs)
 
 mapTc    :: (a -> TcM s b)    -> [a] -> TcM s [b]
+mapTc_   :: (a -> TcM s b)    -> [a] -> TcM s ()
 mapNF_Tc :: (a -> NF_TcM s b) -> [a] -> NF_TcM s [b]
 mapTc f []     = returnTc []
 mapTc f (x:xs) = f x		`thenTc` \ r ->
 		 mapTc f xs	`thenTc` \ rs ->
 		 returnTc (r:rs)
+mapTc_ f xs = mapTc f xs  `thenTc_` returnTc ()
+
 
 foldrTc    :: (a -> b -> TcM s b)    -> b -> [a] -> TcM s b
 foldrNF_Tc :: (a -> b -> NF_TcM s b) -> b -> [a] -> NF_TcM s b
diff --git a/ghc/compiler/typecheck/TcMonoType.lhs b/ghc/compiler/typecheck/TcMonoType.lhs
index f734b782368269c8f927db908a9543c111ad1911..ee3b281ac78703cf3ab05d5076cfaf7fb94806ec 100644
--- a/ghc/compiler/typecheck/TcMonoType.lhs
+++ b/ghc/compiler/typecheck/TcMonoType.lhs
@@ -4,9 +4,14 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
-module TcMonoType ( tcHsType, tcHsSigType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsTopTypeKind,
-		    tcContext, tcHsTyVar, kcHsTyVar, kcHsType,
-		    tcExtendTyVarScope, tcExtendTopTyVarScope,
+module TcMonoType ( tcHsType, tcHsSigType, tcHsBoxedSigType, 
+		    tcContext, tcClassContext, tcHsTyVar, 
+
+			-- Kind checking
+		    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
+		    kcHsType, kcHsSigType, kcHsBoxedSigType, kcHsContext,
+		    kcTyVarScope, 
+
 		    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
 		    checkSigTyVars, sigCtxt, sigPatCtxt
 	          ) where
@@ -14,41 +19,44 @@ module TcMonoType ( tcHsType, tcHsSigType, tcHsTypeKind, tcHsTopType, tcHsTopBox
 #include "HsVersions.h"
 
 import HsSyn		( HsType(..), HsTyVarBndr(..), HsUsageAnn(..),
-                          Sig(..), HsPred(..), pprParendHsType, HsTupCon(..) )
-import RnHsSyn		( RenamedHsType, RenamedContext, RenamedSig )
+                          Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
+import RnHsSyn		( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
 import TcHsSyn		( TcId )
 
 import TcMonad
 import TcEnv		( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
                           tcExtendUVarEnv, tcLookupUVar,
-			  tcGetGlobalTyVars, valueEnvIds, TcTyThing(..)
+			  tcGetGlobalTyVars, valueEnvIds, 
+		 	  TyThing(..), tyThingKind, tcExtendKindEnv
 			)
 import TcType		( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
-			  typeToTcType, kindToTcKind,
 			  newKindVar, tcInstSigVar,
-			  zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType, zonkTcTyVar
+			  zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
 			)
 import Inst		( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
 			  instFunDeps, instFunDepsOfTheta )
 import FunDeps		( tyVarFunDep, oclose )
-import TcUnify		( unifyKind, unifyKinds, unifyTypeKind )
-import Type		( Type, PredType(..), ThetaType, UsageAnn(..),
+import TcUnify		( unifyKind, unifyKinds, unifyOpenTypeKind )
+import Type		( Type, Kind, PredType(..), ThetaType, UsageAnn(..),
 			  mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
                           mkUsForAllTy, zipFunTys, hoistForAllTys,
 			  mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
 			  mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
-			  boxedTypeKind, unboxedTypeKind, 
-			  mkArrowKinds, getTyVar_maybe, getTyVar,
+			  boxedTypeKind, unboxedTypeKind, mkArrowKind,
+			  mkArrowKinds, getTyVar_maybe, getTyVar, splitFunTy_maybe,
 		  	  tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
-			  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, mkForAllTys
+			  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, mkForAllTys,
+			  classesOfPreds
 			)
 import PprType		( pprConstraint, pprType, pprPred )
 import Subst		( mkTopTyVarSubst, substTy )
 import Id		( mkVanillaId, idName, idType, idFreeTyVars )
-import Var		( TyVar, mkTyVar, mkNamedUVar, varName )
+import Var		( TyVar, mkTyVar, tyVarKind, mkNamedUVar, varName )
 import VarEnv
 import VarSet
 import ErrUtils		( Message )
+import TyCon		( TyCon, isSynTyCon, tyConArity, tyConKind )
+import Class		( ClassContext, classArity, classTyCon )
 import Name		( Name, OccName, isLocallyDefined )
 import TysWiredIn	( mkListTy, mkTupleTy )
 import UniqFM		( elemUFM, foldUFM )
@@ -59,6 +67,146 @@ import Outputable
 \end{code}
 
 
+%************************************************************************
+%*									*
+\subsection{Checking types}
+%*									*
+%************************************************************************
+
+\begin{code}
+
+kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM s (name, TcKind)
+kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM s [(name, TcKind)]
+
+kcHsTyVar (UserTyVar name)       = newKindVar	`thenNF_Tc` \ kind ->
+				   returnNF_Tc (name, kind)
+kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
+
+kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
+
+---------------------------
+kcBoxedType :: RenamedHsType -> TcM s ()
+	-- The type ty must be a *boxed* *type*
+kcBoxedType ty
+  = kcHsType ty				`thenTc` \ kind ->
+    tcAddErrCtxt (typeKindCtxt ty)	$
+    unifyKind boxedTypeKind kind
+    
+---------------------------
+kcTypeType :: RenamedHsType -> TcM s ()
+	-- The type ty must be a *type*, but it can be boxed or unboxed.
+kcTypeType ty
+  = kcHsType ty				`thenTc` \ kind ->
+    tcAddErrCtxt (typeKindCtxt ty)	$
+    unifyOpenTypeKind kind
+
+---------------------------
+kcHsSigType, kcHsBoxedSigType :: RenamedHsType -> TcM s ()
+	-- Used for type signatures
+kcHsSigType  	 = kcTypeType
+kcHsBoxedSigType = kcBoxedType
+
+---------------------------
+kcHsType :: RenamedHsType -> TcM s TcKind
+kcHsType (HsTyVar name)	      
+  = tcLookupTy name	`thenTc` \ thing ->
+    case thing of
+	ATyVar tv -> returnTc (tyVarKind tv)
+	ATyCon tc -> returnTc (tyConKind tc)
+	AThing k  -> returnTc k
+	other	  -> failWithTc (wrongThingErr "type" thing name)
+
+kcHsType (HsUsgTy _ ty)       = kcHsType ty
+kcHsType (HsUsgForAllTy _ ty) = kcHsType ty
+
+kcHsType (HsListTy ty)
+  = kcBoxedType ty		`thenTc` \ tau_ty ->
+    returnTc boxedTypeKind
+
+kcHsType (HsTupleTy (HsTupCon _ Boxed) tys)
+  = mapTc kcBoxedType tys	`thenTc_` 
+    returnTc boxedTypeKind
+
+kcHsType (HsTupleTy (HsTupCon _ Unboxed) tys)
+  = mapTc kcTypeType tys	`thenTc_` 
+    returnTc unboxedTypeKind
+
+kcHsType (HsFunTy ty1 ty2)
+  = kcTypeType ty1	`thenTc_`
+    kcTypeType ty2	`thenTc_`
+    returnTc boxedTypeKind
+
+kcHsType (HsPredTy pred)
+  = kcHsPred pred		`thenTc_`
+    returnTc boxedTypeKind
+
+kcHsType ty@(HsAppTy ty1 ty2)
+  = kcHsType ty1		`thenTc` \ tc_kind ->
+    kcHsType ty2		`thenTc` \ arg_kind ->
+
+    tcAddErrCtxt (appKindCtxt (ppr ty))	$
+    case splitFunTy_maybe tc_kind of 
+	Just (arg_kind', res_kind)
+		-> unifyKind arg_kind arg_kind'	`thenTc_`
+		   returnTc res_kind
+
+	Nothing -> newKindVar 						`thenNF_Tc` \ res_kind ->
+		   unifyKind tc_kind (mkArrowKind arg_kind res_kind)	`thenTc_`
+		   returnTc res_kind
+
+kcHsType (HsForAllTy (Just tv_names) context ty)
+  = kcHsTyVars tv_names			`thenNF_Tc` \ kind_env ->
+    tcExtendKindEnv kind_env		$
+    kcHsContext context		`thenTc_`
+    kcHsType ty			`thenTc` \ kind ->
+ 
+		-- Context behaves like a function type
+		-- This matters.  Return-unboxed-tuple analysis can
+		-- give overloaded functions like
+		--	f :: forall a. Num a => (# a->a, a->a #)
+		-- And we want these to get through the type checker
+    returnTc (if null context then
+		 kind
+	      else
+		  boxedTypeKind)
+
+---------------------------
+kcHsContext ctxt = mapTc_ kcHsPred ctxt
+
+kcHsPred :: RenamedHsPred -> TcM s ()
+kcHsPred pred@(HsPIParam name ty)
+  = tcAddErrCtxt (appKindCtxt (ppr pred))	$
+    kcBoxedType ty
+
+kcHsPred pred@(HsPClass cls tys)
+  = tcAddErrCtxt (appKindCtxt (ppr pred))	$
+    tcLookupTy cls 				`thenNF_Tc` \ thing -> 
+    (case thing of
+	AClass cls  -> returnTc (tyConKind (classTyCon cls))
+	AThing kind -> returnTc kind
+	other -> failWithTc (wrongThingErr "class" thing cls))	`thenTc` \ kind ->
+    mapTc kcHsType tys						`thenTc` \ arg_kinds ->
+    unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)
+\end{code}
+
+\begin{code}
+kcTyVarScope :: [HsTyVarBndr Name] 
+	     -> TcM s a				-- The kind checker
+	     -> TcM s [TyVar]
+	-- Do a kind check to find out the kinds of the type variables
+	-- Then return the type variables
+
+kcTyVarScope [] kind_check = returnTc []
+	-- A useful short cut for a common case!
+  
+kcTyVarScope tv_names kind_check 
+  = kcHsTyVars tv_names 				`thenNF_Tc` \ tv_names_w_kinds ->
+    tcExtendKindEnv tv_names_w_kinds kind_check		`thenTc_`
+    zonkKindEnv tv_names_w_kinds			`thenNF_Tc` \ zonked_pairs ->
+    returnTc (map mk_tyvar zonked_pairs)
+\end{code}
+    
+
 %************************************************************************
 %*									*
 \subsection{Checking types}
@@ -68,65 +216,27 @@ import Outputable
 tcHsType and tcHsTypeKind
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-tcHsType checks that the type really is of kind Type!
+tcHsSigType and tcHsBoxedSigType are used for type signatures written by the programmer
 
-\begin{code}
-kcHsType :: RenamedHsType -> TcM c ()
-  -- Kind-check the type
-kcHsType ty = tc_type ty	`thenTc_`
-	      returnTc ()
+  * We hoist any inner for-alls to the top
 
+  * Notice that we kind-check first, because the type-check assumes
+	that the kinds are already checked.
+  * They are only called when there are no kind vars in the environment
+  	so the kind returned is indeed a Kind not a TcKind
+
+\begin{code}
 tcHsSigType :: RenamedHsType -> TcM s TcType
-  -- Used for type sigs written by the programmer
-  -- Hoist any inner for-alls to the top
 tcHsSigType ty
-  = tcHsType ty		`thenTc` \ ty' ->
+  = kcTypeType ty	`thenTc_`
+    tcHsType ty		`thenTc` \ ty' ->
     returnTc (hoistForAllTys ty')
 
-tcHsType :: RenamedHsType -> TcM s TcType
-tcHsType ty
-  = -- tcAddErrCtxt (typeCtxt ty)		$
-    tc_type ty
-
-tcHsTypeKind    :: RenamedHsType -> TcM s (TcKind, TcType)
-tcHsTypeKind ty 
-  = -- tcAddErrCtxt (typeCtxt ty)		$
-    tc_type_kind ty
-
--- Type-check a type, *and* then lazily zonk it.  The important
--- point is that this zonks all the uncommitted *kind* variables
--- in kinds of any any nested for-all tyvars.
--- There won't be any mutable *type* variables at all.
---
--- NOTE the forkNF_Tc.  This makes the zonking lazy, which is
--- absolutely necessary.  During the type-checking of a recursive
--- group of tycons/classes (TcTyClsDecls.tcGroup) we use an
--- environment in which we aren't allowed to look at the actual
--- tycons/classes returned from a lookup. Because tc_app does
--- look at the tycon to build the type, we can't look at the type
--- either, until we get out of the loop.   The fork delays the
--- zonking till we've completed the loop.  Sigh.
-
-tcHsTopType :: RenamedHsType -> TcM s Type
-tcHsTopType ty
-  = -- tcAddErrCtxt (typeCtxt ty)		$
-    tc_type ty				`thenTc` \ ty' ->
-    forkNF_Tc (zonkTcTypeToType ty')	`thenTc` \ ty'' ->
-    returnTc (hoistForAllTys ty'')
-
-tcHsTopBoxedType :: RenamedHsType -> TcM s Type
-tcHsTopBoxedType ty
-  = -- tcAddErrCtxt (typeCtxt ty)		$
-    tc_boxed_type ty			`thenTc` \ ty' ->
-    forkNF_Tc (zonkTcTypeToType ty')	`thenTc` \ ty'' ->
-    returnTc (hoistForAllTys ty'')
-
-tcHsTopTypeKind :: RenamedHsType -> TcM s (TcKind, Type)
-tcHsTopTypeKind ty
-  = -- tcAddErrCtxt (typeCtxt ty)		$
-    tc_type_kind ty				`thenTc` \ (kind, ty') ->
-    forkNF_Tc (zonkTcTypeToType ty')		`thenTc` \ zonked_ty ->
-    returnNF_Tc (kind, hoistForAllTys zonked_ty)
+tcHsBoxedSigType :: RenamedHsType -> TcM s Type
+tcHsBoxedSigType ty
+  = kcBoxedType ty	`thenTc_`
+    tcHsType ty		`thenTc` \ ty' ->
+    returnTc (hoistForAllTys ty')
 \end{code}
 
 
@@ -134,83 +244,58 @@ The main work horse
 ~~~~~~~~~~~~~~~~~~~
 
 \begin{code}
-tc_boxed_type :: RenamedHsType -> TcM s Type
-tc_boxed_type ty
-  = tc_type_kind ty					`thenTc` \ (actual_kind, tc_ty) ->
-    tcAddErrCtxt (typeKindCtxt ty)
-		 (unifyKind boxedTypeKind actual_kind)	`thenTc_`
-    returnTc tc_ty
-
-tc_type :: RenamedHsType -> TcM s Type
-tc_type ty
-	-- The type ty must be a *type*, but it can be boxed
-	-- or unboxed.  So we check that is is of form (Type bv)
-	-- using unifyTypeKind
-  = tc_type_kind ty				`thenTc` \ (actual_kind, tc_ty) ->
-    tcAddErrCtxt (typeKindCtxt ty)
-		 (unifyTypeKind actual_kind)	`thenTc_`
-    returnTc tc_ty
-
-tc_type_kind :: RenamedHsType -> TcM s (TcKind, Type)
-tc_type_kind ty@(HsTyVar name)
+tcHsType :: RenamedHsType -> TcM s Type
+tcHsType ty@(HsTyVar name)
   = tc_app ty []
 
-tc_type_kind (HsListTy ty)
-  = tc_boxed_type ty		`thenTc` \ tau_ty ->
-    returnTc (boxedTypeKind, mkListTy tau_ty)
-
-tc_type_kind (HsTupleTy (HsTupCon _ Boxed) tys)
-  = mapTc tc_boxed_type tys	`thenTc` \ tau_tys ->
-    returnTc (boxedTypeKind, mkTupleTy Boxed (length tys) tau_tys)
+tcHsType (HsListTy ty)
+  = tcHsType ty		`thenTc` \ tau_ty ->
+    returnTc (mkListTy tau_ty)
 
-tc_type_kind (HsTupleTy (HsTupCon _ Unboxed) tys)
-  = mapTc tc_type tys			`thenTc` \ tau_tys ->
-    returnTc (unboxedTypeKind, mkTupleTy Unboxed (length tys) tau_tys)
+tcHsType (HsTupleTy (HsTupCon _ boxity) tys)
+  = mapTc tcHsType tys	`thenTc` \ tau_tys ->
+    returnTc (mkTupleTy boxity (length tys) tau_tys)
 
-tc_type_kind (HsFunTy ty1 ty2)
-  = tc_type ty1	`thenTc` \ tau_ty1 ->
-    tc_type ty2	`thenTc` \ tau_ty2 ->
-    returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
+tcHsType (HsFunTy ty1 ty2)
+  = tcHsType ty1	`thenTc` \ tau_ty1 ->
+    tcHsType ty2	`thenTc` \ tau_ty2 ->
+    returnTc (mkFunTy tau_ty1 tau_ty2)
 
-tc_type_kind (HsAppTy ty1 ty2)
+tcHsType (HsAppTy ty1 ty2)
   = tc_app ty1 [ty2]
 
-tc_type_kind (HsPredTy pred)
+tcHsType (HsPredTy pred)
   = tcClassAssertion True pred	`thenTc` \ pred' ->
-    returnTc (boxedTypeKind, mkPredTy pred')
+    returnTc (mkPredTy pred')
 
-tc_type_kind (HsUsgTy usg ty)
-  = newUsg usg                          `thenTc` \ usg' ->
-    tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
-    returnTc (kind, mkUsgTy usg' tc_ty)
+tcHsType (HsUsgTy usg ty)
+  = newUsg usg			`thenTc` \ usg' ->
+    tcHsType ty			`thenTc` \ tc_ty ->
+    returnTc (mkUsgTy usg' tc_ty)
   where
     newUsg usg = case usg of
                    HsUsOnce        -> returnTc UsOnce
                    HsUsMany        -> returnTc UsMany
                    HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
-                                        returnTc (UsVar uv)
+                                      returnTc (UsVar uv)
 
-tc_type_kind (HsUsgForAllTy uv_name ty)
+tcHsType (HsUsgForAllTy uv_name ty)
   = let
         uv = mkNamedUVar uv_name
     in
     tcExtendUVarEnv uv_name uv $
-      tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
-      returnTc (kind, mkUsForAllTy uv tc_ty)
+    tcHsType ty                     `thenTc` \ tc_ty ->
+    returnTc (mkUsForAllTy uv tc_ty)
 
-tc_type_kind full_ty@(HsForAllTy (Just tv_names) context ty)
-  = tcExtendTyVarScope tv_names		$ \ forall_tyvars ->
+tcHsType full_ty@(HsForAllTy (Just tv_names) context ty)
+  = let
+	kind_check = kcHsContext context `thenTc_` kcHsType ty
+    in
+    kcTyVarScope tv_names kind_check 	`thenTc` \ forall_tyvars ->
+    tcExtendTyVarEnv forall_tyvars	$
     tcContext context			`thenTc` \ theta ->
-    tc_type_kind ty			`thenTc` \ (kind, tau) ->
+    tcHsType ty				`thenTc` \ tau ->
     let
-	body_kind | null theta = kind
-		  | otherwise  = boxedTypeKind
-		-- Context behaves like a function type
-		-- This matters.  Return-unboxed-tuple analysis can
-		-- give overloaded functions like
-		--	f :: forall a. Num a => (# a->a, a->a #)
-		-- And we want these to get through the type checker
-
 	-- Check for ambiguity
 	--   forall V. P => tau
 	-- is ambiguous if P contains generic variables
@@ -263,7 +348,7 @@ tc_type_kind full_ty@(HsForAllTy (Just tv_names) context ty)
 				other		  -> False
     in
     mapTc check_pred theta		`thenTc_`
-    returnTc (body_kind, mkSigmaTy forall_tyvars theta tau)
+    returnTc (mkSigmaTy forall_tyvars theta tau)
 \end{code}
 
 Help functions for type applications
@@ -274,79 +359,74 @@ tc_app (HsAppTy ty1 ty2) tys
   = tc_app ty1 (ty2:tys)
 
 tc_app ty tys
-  | null tys
-  = tc_fun_type ty []
-
-  | otherwise
   = tcAddErrCtxt (appKindCtxt pp_app)	$
-    mapAndUnzipTc tc_type_kind tys	`thenTc` \ (arg_kinds, arg_tys) ->
-    tc_fun_type ty arg_tys		`thenTc` \ (fun_kind, result_ty) ->
-
-	-- Check argument compatibility
-    newKindVar					`thenNF_Tc` \ result_kind ->
-    unifyKind fun_kind (mkArrowKinds arg_kinds result_kind)
-					`thenTc_`
-    returnTc (result_kind, result_ty)
+    mapTc tcHsType tys			`thenTc` \ arg_tys ->
+    tc_fun_type ty arg_tys
   where
     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 
--- (tc_fun_type ty arg_tys) returns (kind-of ty, mkAppTys ty arg_tys)
+-- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 -- 	hence the rather strange functionality.
 
 tc_fun_type (HsTyVar name) arg_tys
-  = tcLookupTy name			`thenTc` \ (tycon_kind, thing) ->
+  = tcLookupTy name			`thenTc` \ thing ->
     case thing of
-	ATyVar tv     -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
-	AClass clas _ -> failWithTc (classAsTyConErr name)
-
-	ADataTyCon tc ->  -- Data or newtype
-			  returnTc (tycon_kind, mkTyConApp tc arg_tys)
-
-	ASynTyCon tc arity ->  	-- Type synonym
-			          checkTc (arity <= n_args) err_msg	`thenTc_`
-	  		          returnTc (tycon_kind, result_ty)
-			   where
-				-- It's OK to have an *over-applied* type synonym
-				--	data Tree a b = ...
-				--	type Foo a = Tree [a]
-				--	f :: Foo a b -> ...
-			      result_ty = mkAppTys (mkSynTy tc (take arity arg_tys))
-						   (drop arity arg_tys)
-			      err_msg = arityErr "type synonym" name arity n_args
-			      n_args  = length arg_tys
+	ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
+
+	ATyCon tc | isSynTyCon tc ->  checkTc arity_ok err_msg	`thenTc_`
+				      returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
+							 (drop arity arg_tys))
+
+		  | otherwise	  ->  returnTc (mkTyConApp tc arg_tys)
+		  where
+
+		    arity_ok = arity <= n_args 
+		    arity = tyConArity tc
+			-- It's OK to have an *over-applied* type synonym
+			--	data Tree a b = ...
+			--	type Foo a = Tree [a]
+			--	f :: Foo a b -> ...
+		    err_msg = arityErr "type synonym" name arity n_args
+		    n_args  = length arg_tys
+
+	other -> failWithTc (wrongThingErr "type constructor" thing name)
 
 tc_fun_type ty arg_tys
-  = tc_type_kind ty		`thenTc` \ (fun_kind, fun_ty) ->
-    returnTc (fun_kind, mkAppTys fun_ty arg_tys)
+  = tcHsType ty		`thenTc` \ fun_ty ->
+    returnNF_Tc (mkAppTys fun_ty arg_tys)
 \end{code}
 
 
 Contexts
 ~~~~~~~~
 \begin{code}
+tcClassContext :: RenamedContext -> TcM s ClassContext
+	-- Used when we are expecting a ClassContext (i.e. no implicit params)
+tcClassContext context
+  = tcContext context 	`thenTc` \ theta ->
+    returnTc (classesOfPreds theta)
 
 tcContext :: RenamedContext -> TcM s ThetaType
 tcContext context = mapTc (tcClassAssertion False) context
 
 tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
   = tcAddErrCtxt (appKindCtxt (ppr assn))	$
-    mapAndUnzipTc tc_type_kind tys		`thenTc` \ (arg_kinds, arg_tys) ->
-    tcLookupTy class_name			`thenTc` \ (kind, thing) ->
+    mapTc tcHsType tys				`thenTc` \ arg_tys ->
+    tcLookupTy class_name			`thenTc` \ thing ->
     case thing of
-	AClass clas arity ->
-		    	-- Check with kind mis-match
-		checkTc (arity == n_tys) err				`thenTc_`
-		unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)	`thenTc_`
-		returnTc (Class clas arg_tys)
+	AClass clas -> checkTc (arity == n_tys) err				`thenTc_`
+		       returnTc (Class clas arg_tys)
 	    where
+		arity = classArity clas
 		n_tys = length tys
 		err   = arityErr "Class" class_name arity n_tys
-	other -> failWithTc (tyVarAsClassErr class_name)
+
+	other -> failWithTc (wrongThingErr "class" thing class_name)
 
 tcClassAssertion ccall_ok assn@(HsPIParam name ty)
   = tcAddErrCtxt (appKindCtxt (ppr assn))	$
-    tc_type_kind ty	`thenTc` \ (arg_kind, arg_ty) ->
+    tcHsType ty					`thenTc` \ arg_ty ->
     returnTc (IParam name arg_ty)
 \end{code}
 
@@ -358,38 +438,24 @@ tcClassAssertion ccall_ok assn@(HsPIParam name ty)
 %************************************************************************
 
 \begin{code}
-tcExtendTopTyVarScope :: TcKind -> [HsTyVarBndr Name]
-		      -> ([TcTyVar] -> TcKind -> TcM s a)
-		      -> TcM s a
-tcExtendTopTyVarScope kind tyvar_names thing_inside
-  = let
-	(tyvars_w_kinds, result_kind) = zipFunTys tyvar_names kind
-	tyvars 			      = map mk_tv tyvars_w_kinds
-    in
-    tcExtendTyVarEnv tyvars (thing_inside tyvars result_kind)	
+mk_tyvar (tv_bndr, kind) = mkTyVar tv_bndr kind
+
+mkTyClTyVars :: Kind 			-- Kind of the tycon or class
+	     -> [HsTyVarBndr Name]
+	     -> [TyVar]
+mkTyClTyVars kind tyvar_names
+  = map mk_tyvar tyvars_w_kinds
   where
-    mk_tv (UserTyVar name,    kind) = mkTyVar name kind
-    mk_tv (IfaceTyVar name _, kind) = mkTyVar name kind
-	-- NB: immutable tyvars, but perhaps with mutable kinds
-
-tcExtendTyVarScope :: [HsTyVarBndr Name] 
-		   -> ([TcTyVar] -> TcM s a) -> TcM s a
-tcExtendTyVarScope tv_names thing_inside
-  = mapNF_Tc tcHsTyVar tv_names 	`thenNF_Tc` \ tyvars ->
-    tcExtendTyVarEnv tyvars		$
-    thing_inside tyvars
-    
+    (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
+
 tcHsTyVar :: HsTyVarBndr Name -> NF_TcM s TcTyVar
 tcHsTyVar (UserTyVar name)       = newKindVar		`thenNF_Tc` \ kind ->
 			           tcNewMutTyVar name kind
 	-- NB: mutable kind => mutable tyvar, so that zonking can bind
 	-- the tyvar to its immutable form
 
-tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name (kindToTcKind kind))
+tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name kind)
 
-kcHsTyVar :: HsTyVarBndr name -> NF_TcM s TcKind
-kcHsTyVar (UserTyVar name)       = newKindVar
-kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (kindToTcKind kind)
 \end{code}
 
 
@@ -707,7 +773,7 @@ sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
     let
 	(env1, tidy_sig_tyvars)  = tidyTyVars tidy_env sig_tyvars
 	(env2, tidy_sig_rho)	 = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
-	(env3, tidy_actual_tau)  = tidyOpenType env1 actual_tau
+	(env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
 	msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
 		    ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
 		    when
@@ -748,14 +814,13 @@ typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 appKindCtxt :: SDoc -> Message
 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 
-classAsTyConErr name
-  = ptext SLIT("Class used as a type constructor:") <+> ppr name
-
-tyConAsClassErr name
-  = ptext SLIT("Type constructor used as a class:") <+> ppr name
-
-tyVarAsClassErr name
-  = ptext SLIT("Type variable used as a class:") <+> ppr name
+wrongThingErr expected actual name
+  = pp_actual actual <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
+  where
+    pp_actual (ATyCon _) = ptext SLIT("Type constructor")
+    pp_actual (AClass _) = ptext SLIT("Class")
+    pp_actual (ATyVar _) = ptext SLIT("Type variable")
+    pp_actual (AThing _) = ptext SLIT("Utterly bogus")
 
 ambigErr pred ty
   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs
index e974cfaa2d9c397459dd5ec7fdc090e12d2083d7..e0cb157bac260f263388e73a2a9e2eb0ed1ae819 100644
--- a/ghc/compiler/typecheck/TcPat.lhs
+++ b/ghc/compiler/typecheck/TcPat.lhs
@@ -392,7 +392,7 @@ tcConstructor pat con_name pat_ty
 
 	-- Instantiate it
     let 
-	(tvs, theta, ex_tvs, ex_theta, arg_tys, tycon) = dataConSig data_con
+	(tvs, _, ex_tvs, ex_theta, arg_tys, tycon) = dataConSig data_con
 	     -- Ignore the theta; overloaded constructors only
 	     -- behave differently when called, not when used for
 	     -- matching.
diff --git a/ghc/compiler/typecheck/TcRules.lhs b/ghc/compiler/typecheck/TcRules.lhs
index 616d717b7f09bcf0f6d19c9963b8a5cfb6ea3bf5..ec9176134b19f16f31a5ba00f34e8a250d86b212 100644
--- a/ghc/compiler/typecheck/TcRules.lhs
+++ b/ghc/compiler/typecheck/TcRules.lhs
@@ -14,7 +14,7 @@ import RnHsSyn		( RenamedHsDecl )
 import TcHsSyn		( TypecheckedRuleDecl, mkHsLet )
 import TcMonad
 import TcSimplify	( tcSimplifyToDicts, tcSimplifyAndCheck )
-import TcType		( zonkTcTypes, newTyVarTy_OpenKind )
+import TcType		( zonkTcTypes, newTyVarTy )
 import TcIfaceSig	( tcCoreExpr, tcCoreLamBndrs, tcVar )
 import TcMonoType	( tcHsSigType, tcHsTyVar, checkSigTyVars )
 import TcExpr		( tcExpr )
@@ -24,7 +24,7 @@ import TcEnv		( tcExtendLocalValEnv, newLocalId,
 import Inst		( LIE, emptyLIE, plusLIEs, instToId )
 import Id		( idType, idName, mkVanillaId )
 import VarSet
-import Type		( tyVarsOfTypes )
+import Type		( tyVarsOfTypes, openTypeKind )
 import Bag		( bagToList )
 import Outputable
 import Util
@@ -51,7 +51,7 @@ tcRule (IfaceRuleOut fun rule)
 tcRule (HsRule name sig_tvs vars lhs rhs src_loc)
   = tcAddSrcLoc src_loc 				$
     tcAddErrCtxt (ruleCtxt name)			$
-    newTyVarTy_OpenKind					`thenNF_Tc` \ rule_ty ->
+    newTyVarTy openTypeKind				`thenNF_Tc` \ rule_ty ->
 
 	-- Deal with the tyvars mentioned in signatures
 	-- Yuk to the UserTyVar
@@ -106,7 +106,7 @@ tcRule (HsRule name sig_tvs vars lhs rhs src_loc)
 				(mkHsLet rhs_binds rhs')
 				src_loc)
   where
-    new_id (RuleBndr var) 	   = newTyVarTy_OpenKind	`thenNF_Tc` \ ty ->
+    new_id (RuleBndr var) 	   = newTyVarTy openTypeKind	`thenNF_Tc` \ ty ->
 		          	     returnNF_Tc (mkVanillaId var ty)
     new_id (RuleBndrSig var rn_ty) = tcHsSigType rn_ty	`thenTc` \ ty ->
 				     returnNF_Tc (mkVanillaId var ty)
diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs
index 861f908f5d620c5874683df4c899d7410af34435..f51ae48aaceedc367691ee5cbdf2eb0a2b76fcc2 100644
--- a/ghc/compiler/typecheck/TcSimplify.lhs
+++ b/ghc/compiler/typecheck/TcSimplify.lhs
@@ -146,7 +146,7 @@ import Inst		( lookupInst, lookupSimpleInst, LookupInstResult(..),
 import TcEnv		( tcGetGlobalTyVars, tcGetInstEnv,
 			  InstEnv, lookupInstEnv, InstLookupResult(..) 
 			)
-import TcType		( TcType, TcTyVarSet, typeToTcType )
+import TcType		( TcType, TcTyVarSet )
 import TcUnify		( unifyTauTy )
 import Id		( idType )
 import Class		( Class, classBigSig )
@@ -1141,10 +1141,7 @@ disambigGroup dicts
     try_default default_tys		 	`thenTc` \ chosen_default_ty ->
 
 	-- Bind the type variable and reduce the context, for real this time
-    let
-	chosen_default_tc_ty = typeToTcType chosen_default_ty	-- Tiresome!
-    in
-    unifyTauTy chosen_default_tc_ty (mkTyVarTy tyvar)	`thenTc_`
+    unifyTauTy chosen_default_ty (mkTyVarTy tyvar)	`thenTc_`
     reduceContext (text "disambig" <+> ppr dicts)
 		  try_me [] dicts			`thenTc` \ (binds, frees, ambigs) ->
     ASSERT( null frees && null ambigs )
diff --git a/ghc/compiler/typecheck/TcTyClsDecls.lhs b/ghc/compiler/typecheck/TcTyClsDecls.lhs
index 030e7102133bf430886267399f954ef2485d4157..a194ed34ebe4a2ea1676d0ee81c945f56243e08f 100644
--- a/ghc/compiler/typecheck/TcTyClsDecls.lhs
+++ b/ghc/compiler/typecheck/TcTyClsDecls.lhs
@@ -14,38 +14,50 @@ import HsSyn		( HsDecl(..), TyClDecl(..),
 			  HsType(..), HsTyVarBndr,
 			  ConDecl(..), ConDetails(..), BangType(..),
 			  Sig(..), HsPred(..), HsTupCon(..),
-			  tyClDeclName, isClassDecl, isSynDecl
+			  tyClDeclName, hsTyVarNames, isClassDecl, isSynDecl, isClassOpSig, getBangType
 			)
 import RnHsSyn		( RenamedHsDecl, RenamedTyClDecl, listTyCon_name )
 import BasicTypes	( RecFlag(..), NewOrData(..), Arity )
 
 import TcMonad
-import TcClassDcl	( kcClassDecl, tcClassDecl1 )
-import TcEnv		( ValueEnv, TcTyThing(..),
-			  tcExtendTypeEnv, getEnvAllTyCons
+import TcEnv		( ValueEnv, TyThing(..), TyThingDetails(..), tyThingKind,
+			  tcExtendTypeEnv, tcExtendKindEnv, tcLookupTy
 			)
-import TcTyDecls	( tcTyDecl, kcTyDecl )
-import TcMonoType	( kcHsTyVar )
-import TcType		( TcKind, newKindVar, newKindVars, kindToTcKind, zonkTcKindToKind )
-
-import Type		( mkArrowKind, boxedTypeKind )
+import TcTyDecls	( tcTyDecl1, kcConDetails, mkNewTyConRep )
+import TcClassDcl	( tcClassDecl1 )
+import TcMonoType	( kcHsTyVars, kcHsType, kcHsBoxedSigType, kcHsContext, mkTyClTyVars )
+import TcType		( TcKind, newKindVar, newKindVars, zonkKindEnv )
 
+import TcUnify		( unifyKind )
+import Type		( Kind, mkArrowKind, boxedTypeKind, zipFunTys )
+import Variance         ( calcTyConArgVrcs )
+import Class		( Class, mkClass, classTyCon )
+import TyCon		( TyCon, ArgVrcs, AlgTyConFlavour(..), mkSynTyCon, mkAlgTyCon, mkClassTyCon )
+import DataCon		( isNullaryDataCon )
+import Var		( TyVar, tyVarKind, varName )
+import VarEnv
 import FiniteMap
 import Bag	
 import Digraph		( stronglyConnComp, SCC(..) )
-import Name		( Name, NamedThing(..), getSrcLoc, isTvOcc, nameOccName )
+import Name		( Name, NamedThing(..), NameEnv, getSrcLoc, isTvOcc, nameOccName,
+			  mkNameEnv, lookupNameEnv_NF
+			)
 import Outputable
-import Maybes		( mapMaybe, catMaybes, expectJust )
+import Maybes		( mapMaybe, catMaybes )
 import UniqSet		( UniqSet, emptyUniqSet,
 			  unitUniqSet, unionUniqSets, 
 			  unionManyUniqSets, uniqSetToList ) 
 import ErrUtils		( Message )
-import TyCon		( TyCon, ArgVrcs )
-import Variance         ( calcTyConArgVrcs )
 import Unique		( Unique, Uniquable(..) )
-import UniqFM		( listToUFM, lookupUFM )
 \end{code}
 
+
+%************************************************************************
+%*									*
+\subsection{Type checking for type and class declarations}
+%*									*
+%************************************************************************
+
 The main function
 ~~~~~~~~~~~~~~~~~
 \begin{code}
@@ -70,98 +82,124 @@ tcGroups unf_env (group:groups)
 Dealing with a group
 ~~~~~~~~~~~~~~~~~~~~
 
-The knot-tying parameters: @rec_tyclss@ is an alist mapping @Name@s to
-@TcTyThing@s.  @rec_vrcs@ is a finite map from @Name@s to @ArgVrcs@s.
+Consider a mutually-recursive group, binding 
+a type constructor T and a class C.
+
+Step 1: 	getInitialKind
+	Construct a KindEnv by binding T and C to a kind variable 
+
+Step 2: 	kcTyClDecl
+	In that environment, do a kind check
+
+Step 3: Zonk the kinds
+
+Step 4: 	buildTyConOrClass
+	Construct an environment binding T to a TyCon and C to a Class.
+	a) Their kinds comes from zonking the relevant kind variable
+	b) Their arity (for synonyms) comes direct from the decl
+	c) The funcional dependencies come from the decl
+	d) The rest comes a knot-tied binding of T and C, returned from Step 4
+	e) The variances of the tycons in the group is calculated from 
+		the knot-tied stuff
+
+Step 5: 	tcTyClDecl1
+	In this environment, walk over the decls, constructing the TyCons and Classes.
+	This uses in a strict way items (a)-(c) above, which is why they must
+	be constructed in Step 4.
+	Feed the results back to Step 4.
+	
+The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
+@TyThing@s.  @rec_vrcs@ is a finite map from @Name@s to @ArgVrcs@s.
 
 \begin{code}
 tcGroup :: ValueEnv -> SCC RenamedTyClDecl -> TcM s TcEnv
 tcGroup unf_env scc
-  = 	-- Do kind checking
-    mapNF_Tc getTyBinding1 decls 			`thenNF_Tc` \ ty_env_stuff1 ->
-    tcExtendTypeEnv ty_env_stuff1 (mapTc kcDecl decls)	`thenTc_`
+  = 	-- Step 1
+    mapNF_Tc getInitialKind decls 				`thenNF_Tc` \ initial_kinds ->
+
+	-- Step 2
+    tcExtendKindEnv initial_kinds (mapTc kcTyClDecl decls)	`thenTc_`
+
+	-- Step 3
+    zonkKindEnv initial_kinds			`thenNF_Tc` \ final_kinds ->
 
 	-- Tie the knot
---  traceTc (ppr (map fst ty_env_stuff1))		`thenTc_`
-    fixTc ( \ ~(rec_tyclss,  _) ->
-	let
-	    rec_env    = listToUFM rec_tyclss
-	    rec_tycons = getEnvAllTyCons rec_tyclss
-            rec_vrcs   = calcTyConArgVrcs rec_tycons
+    fixTc ( \ ~(rec_details_list,  _) ->
+		-- Step 4 
+ 	let
+	    kind_env    = mkNameEnv final_kinds
+	    rec_details = mkNameEnv rec_details_list
+
+	    tyclss, all_tyclss :: [(Name, TyThing)]
+	    tyclss      = map (buildTyConOrClass is_rec kind_env rec_vrcs rec_details) decls
+
+		-- Add the tycons that come from the classes
+		-- We want them in the environment because 
+		-- they are mentioned in interface files
+	    all_tyclss  = [ (getName tycon, ATyCon tycon) | (_, AClass clas) <- tyclss,
+							    let tycon = classTyCon clas
+			  ] ++ tyclss
+
+		-- Calculate variances, and (yes!) feed back into buildTyConOrClass.
+            rec_vrcs    = calcTyConArgVrcs [tc | (_, ATyCon tc) <- all_tyclss]
 	in
-	
-		-- Do type checking
-	mapNF_Tc (getTyBinding2 rec_env) ty_env_stuff1	`thenNF_Tc` \ ty_env_stuff2 ->
-	tcExtendTypeEnv ty_env_stuff2				$
-	mapTc (tcDecl is_rec_group unf_env rec_vrcs) decls	`thenTc` \ tyclss ->
-
-	tcGetEnv						`thenTc` \ env -> 
-	returnTc (tyclss, env)
+		-- Step 5
+	tcExtendTypeEnv all_tyclss		$
+	mapTc (tcTyClDecl1 unf_env) decls	`thenTc` \ tycls_details ->
+	tcGetEnv				`thenNF_Tc` \ env -> 
+	returnTc (tycls_details, env)
     )								`thenTc` \ (_, env) ->
---  traceTc (text "done" <+> ppr (map fst ty_env_stuff1))	`thenTc_`
     returnTc env
   where
-    is_rec_group = case scc of
-			AcyclicSCC _ -> NonRecursive
-			CyclicSCC _  -> Recursive
+    is_rec = case scc of
+		AcyclicSCC _ -> NonRecursive
+		CyclicSCC _  -> Recursive
 
     decls = case scc of
 		AcyclicSCC decl -> [decl]
 		CyclicSCC decls -> decls
+
+tcTyClDecl1  :: ValueEnv -> RenamedTyClDecl -> TcM s (Name, TyThingDetails)
+
+tcTyClDecl1 unf_env decl
+  | isClassDecl decl = tcClassDecl1 unf_env decl
+  | otherwise	     = tcTyDecl1 decl
 \end{code}
 
-Dealing with one decl
-~~~~~~~~~~~~~~~~~~~~~
-\begin{code}
-kcDecl decl
-  = tcAddDeclCtxt decl		$
-    if isClassDecl decl then
-	kcClassDecl decl
-    else
-	kcTyDecl    decl
-
-tcDecl  :: RecFlag 			-- True => recursive group
-	 -> ValueEnv -> FiniteMap Name ArgVrcs
-	 -> RenamedTyClDecl -> TcM s (Name, TcTyThing)
-
-tcDecl is_rec_group unf_env vrcs_env decl
-  = tcAddDeclCtxt decl		$
-    if isClassDecl decl then
-	tcClassDecl1 unf_env vrcs_env decl
-    else
-	tcTyDecl is_rec_group vrcs_env decl
-		
 
-tcAddDeclCtxt decl thing_inside
-  = tcAddSrcLoc loc 	$
-    tcAddErrCtxt ctxt 	$
-    thing_inside
-  where
-     (name, loc, thing)
-	= case decl of
-	    (ClassDecl _ name _ _ _ _ _ _ _ _ _ loc) -> (name, loc, "class")
-	    (TySynonym name _ _ loc)	             -> (name, loc, "type synonym")
-	    (TyData NewType  _ name _ _ _ _ _ loc)   -> (name, loc, "data type")
-	    (TyData DataType _ name _ _ _ _ _ loc)   -> (name, loc, "newtype")
+%************************************************************************
+%*									*
+\subsection{Step 1: Initial environment}
+%*									*
+%************************************************************************
 
-     ctxt = hsep [ptext SLIT("In the"), text thing, 
-		  ptext SLIT("declaration for"), quotes (ppr name)]
-\end{code}
+\begin{code}
+getInitialKind :: RenamedTyClDecl -> NF_TcM s (Name, TcKind)
+getInitialKind (TySynonym name tyvars _ _)
+ = kcHsTyVars tyvars	`thenNF_Tc` \ arg_kinds ->
+   newKindVar		`thenNF_Tc` \ result_kind  ->
+   returnNF_Tc (name, mk_kind arg_kinds result_kind)
 
+getInitialKind (TyData _ _ name tyvars _ _ _ _ _)
+ = kcHsTyVars tyvars	`thenNF_Tc` \ arg_kinds ->
+   returnNF_Tc (name, mk_kind arg_kinds boxedTypeKind)
 
-getTyBinders
-~~~~~~~~~~~
-Extract *binding* names from type and class decls.  Type variables are
-bound in type, data, newtype and class declarations, 
-	*and* the polytypes in the class op sigs.
-	*and* the existentially quantified contexts in datacon decls
+getInitialKind (ClassDecl _ name tyvars _ _ _ _ _ _ _ _ _)
+ = kcHsTyVars tyvars	`thenNF_Tc` \ arg_kinds ->
+   returnNF_Tc (name, mk_kind arg_kinds boxedTypeKind)
+
+mk_kind tvs_w_kinds res_kind = foldr (mkArrowKind . snd) res_kind tvs_w_kinds
+\end{code}
 
-Why do we need to grab all these type variables at once, including
-those locally-quantified type variables in class op signatures?
 
-   [Incidentally, this only works because the names are all unique by now.]
+%************************************************************************
+%*									*
+\subsection{Step 2: Kind checking}
+%*									*
+%************************************************************************
 
-Because we can only commit to the final kind of a type variable when
-we've completed the mutually recursive group. For example:
+We need to kind check all types in the mutually recursive group
+before we know the kind of the type variables.  For example:
 
 class C a where
    op :: D b => a -> b -> b
@@ -173,35 +211,131 @@ Here, the kind of the locally-polymorphic type variable "b"
 depends on *all the uses of class D*.  For example, the use of
 Monad c in bop's type signature means that D must have kind Type->Type.
 
-    [April 00: looks as if we've dropped this subtlety; I'm not sure when]
+\begin{code}
+kcTyClDecl :: RenamedTyClDecl -> TcM s ()
+
+kcTyClDecl decl@(TySynonym tycon_name hs_tyvars rhs loc)
+  = tcAddDeclCtxt decl			$
+    kcTyClDeclBody tycon_name hs_tyvars	$ \ result_kind ->
+    kcHsType rhs			`thenTc` \ rhs_kind ->
+    unifyKind result_kind rhs_kind
+
+kcTyClDecl decl@(TyData _ context tycon_name hs_tyvars con_decls _ _ _ loc)
+  = tcAddDeclCtxt decl			$
+    kcTyClDeclBody tycon_name hs_tyvars	$ \ result_kind ->
+    kcHsContext context			`thenTc_` 
+    mapTc_ kc_con_decl con_decls
+  where
+    kc_con_decl (ConDecl _ _ ex_tvs ex_ctxt details loc)
+      = tcAddSrcLoc loc			$
+	kcHsTyVars ex_tvs		`thenNF_Tc` \ kind_env ->
+	tcExtendKindEnv kind_env	$
+	kcConDetails ex_ctxt details
+
+kcTyClDecl decl@(ClassDecl context class_name
+			   hs_tyvars fundeps class_sigs
+		      	   _ _ _ _ _ _ loc)
+  = tcAddDeclCtxt decl			$
+    kcTyClDeclBody class_name hs_tyvars	$ \ result_kind ->
+    kcHsContext context			`thenTc_`
+    mapTc_ kc_sig (filter isClassOpSig class_sigs)
+  where
+    kc_sig (ClassOpSig _ _ _ op_ty loc) = tcAddSrcLoc loc (kcHsBoxedSigType op_ty)
+
+kcTyClDeclBody :: Name -> [HsTyVarBndr Name] 	-- Kind of the tycon/cls and its tyvars
+	       -> (Kind -> TcM s a)		-- Thing inside
+	       -> TcM s a
+-- Extend the env with bindings for the tyvars, taken from
+-- the kind of the tycon/class.  Give it to the thing inside, and 
+-- check the result kind matches
+kcTyClDeclBody tc_name hs_tyvars thing_inside
+  = tcLookupTy tc_name		`thenNF_Tc` \ tc ->
+    let
+	(tyvars_w_kinds, result_kind) = zipFunTys (hsTyVarNames hs_tyvars) (tyThingKind tc)
+    in
+    tcExtendKindEnv tyvars_w_kinds (thing_inside result_kind)
+\end{code}
+
+
+%************************************************************************
+%*									*
+\subsection{Step 4: Building the tycon/class}
+%*									*
+%************************************************************************
 
 \begin{code}
-getTyBinding1 :: RenamedTyClDecl -> NF_TcM s (Name, (TcKind, TcTyThing))
-getTyBinding1 (TySynonym name tyvars _ _)
- = mapNF_Tc kcHsTyVar tyvars		`thenNF_Tc` \ arg_kinds ->
-   newKindVar				`thenNF_Tc` \ result_kind  ->
-   returnNF_Tc (name, (foldr mkArrowKind result_kind arg_kinds, 
-		       ASynTyCon (pprPanic "ATyCon: syn" (ppr name)) (length tyvars)))
-
-getTyBinding1 (TyData _ _ name tyvars _ _ _ _ _)
- = mapNF_Tc kcHsTyVar tyvars		`thenNF_Tc` \ arg_kinds ->
-   returnNF_Tc (name, (foldr mkArrowKind boxedTypeKind arg_kinds, 
-		       ADataTyCon (error "ATyCon: data")))
-
-getTyBinding1 (ClassDecl _ name tyvars _ _ _ _ _ _ _ _ _)
- = mapNF_Tc kcHsTyVar tyvars		`thenNF_Tc` \ arg_kinds ->
-   returnNF_Tc (name, (foldr mkArrowKind boxedTypeKind arg_kinds, 
-		       AClass (pprPanic "AClass" (ppr name)) (length tyvars)))
-
--- Zonk the kind to its final form, and lookup the 
--- recursive tycon/class
-getTyBinding2 rec_env (name, (tc_kind, thing))
-  = zonkTcKindToKind tc_kind		`thenNF_Tc` \ kind ->
-    returnNF_Tc (name, (kind, mk_thing thing (lookupUFM rec_env name)))
+buildTyConOrClass 
+	:: RecFlag -> NameEnv Kind
+	-> FiniteMap TyCon ArgVrcs -> NameEnv TyThingDetails
+	-> RenamedTyClDecl -> (Name, TyThing)
+	-- Can't fail; the only reason it's in the monad 
+	-- is so it can zonk the kinds
+
+buildTyConOrClass is_rec kenv rec_vrcs rec_details
+	          (TySynonym tycon_name tyvar_names rhs src_loc)
+  = (tycon_name, ATyCon tycon)
+  where
+	tycon = mkSynTyCon tycon_name tycon_kind arity tyvars rhs_ty argvrcs
+	tycon_kind	    = lookupNameEnv_NF kenv tycon_name
+	arity		    = length tyvar_names
+	tyvars		    = mkTyClTyVars tycon_kind tyvar_names
+	SynTyDetails rhs_ty = lookupNameEnv_NF rec_details tycon_name
+        argvrcs		    = lookupWithDefaultFM rec_vrcs bogusVrcs tycon
+
+buildTyConOrClass is_rec kenv rec_vrcs  rec_details
+	          (TyData data_or_new context tycon_name tyvar_names _ nconstrs _ _ src_loc)
+  = (tycon_name, ATyCon tycon)
   where
-    mk_thing (ADataTyCon _)      ~(Just (ADataTyCon tc))  = ADataTyCon tc
-    mk_thing (ASynTyCon _ arity) ~(Just (ASynTyCon tc _)) = ASynTyCon tc arity
-    mk_thing (AClass _ arity)    ~(Just (AClass cls _))   = AClass cls arity
+	tycon = mkAlgTyCon tycon_name tycon_kind tyvars ctxt argvrcs
+			   data_cons nconstrs
+			   derived_classes
+			   flavour is_rec
+
+	DataTyDetails ctxt data_cons derived_classes = lookupNameEnv_NF rec_details tycon_name
+
+	tycon_kind = lookupNameEnv_NF kenv tycon_name
+	tyvars	   = mkTyClTyVars tycon_kind tyvar_names
+        argvrcs	   = lookupWithDefaultFM rec_vrcs bogusVrcs tycon
+
+	flavour = case data_or_new of
+			NewType -> NewTyCon (mkNewTyConRep tycon)
+			DataType | all isNullaryDataCon data_cons -> EnumTyCon
+				 | otherwise			  -> DataTyCon
+
+buildTyConOrClass is_rec kenv rec_vrcs  rec_details
+                  (ClassDecl context class_name
+		             tyvar_names fundeps class_sigs def_methods pragmas 
+		             tycon_name datacon_name datacon_wkr_name sc_sel_names src_loc)
+  = (class_name, AClass clas)
+  where
+ 	clas = mkClass class_name tyvars fds
+		       sc_theta sc_sel_ids op_items
+		       tycon
+
+	tycon = mkClassTyCon tycon_name class_kind tyvars
+                             argvrcs dict_con
+			     clas 		-- Yes!  It's a dictionary 
+			     flavour
+
+	ClassDetails sc_theta sc_sel_ids op_items dict_con = lookupNameEnv_NF rec_details class_name
+
+	class_kind = lookupNameEnv_NF kenv class_name
+	tyvars	   = mkTyClTyVars class_kind tyvar_names
+        argvrcs	   = lookupWithDefaultFM rec_vrcs bogusVrcs tycon
+	n_fields   = length sc_sel_ids + length op_items
+
+ 	flavour | n_fields == 1 = NewTyCon (mkNewTyConRep tycon)
+		| otherwise	= DataTyCon
+
+	-- We can find the functional dependencies right away, 
+	-- and it is vital to do so. Why?  Because in the next pass
+	-- we check for ambiguity in all the type signatures, and we
+	-- need the functional dependcies to be done by then
+	fds	   = [(map lookup xs, map lookup ys) | (xs,ys) <- fundeps]
+	tyvar_env  = mkNameEnv [(varName tv, tv) | tv <- tyvars]
+	lookup     = lookupNameEnv_NF tyvar_env
+
+bogusVrcs = panic "Bogus tycon arg variances"
 \end{code}
 
 
@@ -296,9 +430,7 @@ get_con_details (NewCon ty _)        = get_ty ty
 get_con_details (RecCon nbtys)       = unionManyUniqSets (map (get_bty.snd) nbtys)
 
 ----------------------------------------------------
-get_bty (Banged ty)   = get_ty ty
-get_bty (Unbanged ty) = get_ty ty
-get_bty (Unpacked ty) = get_ty ty
+get_bty bty = get_ty (getBangType bty)
 
 ----------------------------------------------------
 get_ty (HsTyVar name) | isTvOcc (nameOccName name) = emptyUniqSet 
@@ -330,6 +462,29 @@ set_to_bag set = listToBag (uniqSetToList set)
 \end{code}
 
 
+%************************************************************************
+%*									*
+\subsection{Error management
+%*									*
+%************************************************************************
+
+\begin{code}
+tcAddDeclCtxt decl thing_inside
+  = tcAddSrcLoc loc 	$
+    tcAddErrCtxt ctxt 	$
+    thing_inside
+  where
+     (name, loc, thing)
+	= case decl of
+	    (ClassDecl _ name _ _ _ _ _ _ _ _ _ loc) -> (name, loc, "class")
+	    (TySynonym name _ _ loc)	             -> (name, loc, "type synonym")
+	    (TyData NewType  _ name _ _ _ _ _ loc)   -> (name, loc, "data type")
+	    (TyData DataType _ name _ _ _ _ _ loc)   -> (name, loc, "newtype")
+
+     ctxt = hsep [ptext SLIT("In the"), text thing, 
+		  ptext SLIT("declaration for"), quotes (ppr name)]
+\end{code}
+
 \begin{code}
 typeCycleErr, classCycleErr :: [[RenamedTyClDecl]] -> Message
 
diff --git a/ghc/compiler/typecheck/TcTyDecls.lhs b/ghc/compiler/typecheck/TcTyDecls.lhs
index 464d1b6240248092456290c4277e3d7d07558f54..5efdb208f0bcb88bc08c70349cdca200efb86669 100644
--- a/ghc/compiler/typecheck/TcTyDecls.lhs
+++ b/ghc/compiler/typecheck/TcTyDecls.lhs
@@ -5,8 +5,8 @@
 
 \begin{code}
 module TcTyDecls (
-	tcTyDecl, kcTyDecl, 
-	tcConDecl,
+	tcTyDecl1, 
+	kcConDetails, 
 	mkImplicitDataBinds, mkNewTyConRep
     ) where
 
@@ -14,23 +14,21 @@ module TcTyDecls (
 
 import HsSyn		( MonoBinds(..), 
 			  TyClDecl(..), ConDecl(..), ConDetails(..), BangType(..),
-			  andMonoBindList
+			  andMonoBindList, getBangType
 			)
-import RnHsSyn		( RenamedTyClDecl, RenamedConDecl )
+import RnHsSyn		( RenamedTyClDecl, RenamedConDecl, RenamedContext )
 import TcHsSyn		( TcMonoBinds, idsToMonoBinds )
 import BasicTypes	( RecFlag(..), NewOrData(..) )
 
-import TcMonoType	( tcExtendTopTyVarScope, tcExtendTyVarScope, 
-			  tcHsTypeKind, kcHsType, tcHsTopType, tcHsTopBoxedType,
-			  tcContext, tcHsTopTypeKind
+import TcMonoType	( tcHsSigType, tcHsBoxedSigType, kcTyVarScope, tcClassContext,
+			  kcHsContext, kcHsSigType
 			)
-import TcType		( zonkTcTyVarToTyVar, zonkTcClassConstraints )
-import TcEnv		( tcLookupTy, tcLookupValueByKey, TcTyThing(..) )
+import TcEnv		( tcExtendTyVarEnv, tcLookupTy, tcLookupValueByKey, TyThing(..), TyThingDetails(..) )
 import TcMonad
 import TcUnify		( unifyKind )
 
-import Class		( Class )
-import DataCon		( DataCon, mkDataCon, isNullaryDataCon,
+import Class		( Class, ClassContext )
+import DataCon		( DataCon, mkDataCon, 
 			  dataConFieldLabels, dataConId, dataConWrapId,
 			  markedStrict, notMarkedStrict, markedUnboxed, dataConRepType
 			)
@@ -57,49 +55,6 @@ import Util		( equivClasses )
 import FiniteMap        ( FiniteMap, lookupWithDefaultFM )
 \end{code}
 
-%************************************************************************
-%*									*
-\subsection{Kind checking}
-%*									*
-%************************************************************************
-
-\begin{code}
-kcTyDecl :: RenamedTyClDecl -> TcM s ()
-
-kcTyDecl (TySynonym name tyvar_names rhs src_loc)
-  = tcLookupTy name				`thenNF_Tc` \ (kind, _) ->
-    tcExtendTopTyVarScope kind tyvar_names	$ \ _ result_kind ->
-    tcHsTypeKind rhs				`thenTc` \ (rhs_kind, _) ->
-    unifyKind result_kind rhs_kind
-
-kcTyDecl (TyData _ context tycon_name tyvar_names con_decls _ _ _ src_loc)
-  = tcLookupTy tycon_name			`thenNF_Tc` \ (kind, _) ->
-    tcExtendTopTyVarScope kind tyvar_names	$ \ result_kind _ ->
-    tcContext context				`thenTc_` 
-    mapTc kcConDecl con_decls			`thenTc_`
-    returnTc ()
-
-kcConDecl (ConDecl _ _ ex_tvs ex_ctxt details loc)
-  = tcAddSrcLoc loc			(
-    tcExtendTyVarScope ex_tvs		( \ tyvars -> 
-    tcContext ex_ctxt			`thenTc_`
-    kc_con details			`thenTc_`
-    returnTc ()
-    ))
-  where
-    kc_con (VanillaCon btys)    = mapTc kc_bty btys		`thenTc_` returnTc ()
-    kc_con (InfixCon bty1 bty2) = mapTc kc_bty [bty1,bty2]	`thenTc_` returnTc ()
-    kc_con (NewCon ty _)        = kcHsType ty
-    kc_con (RecCon flds)        = mapTc kc_field flds		`thenTc_` returnTc ()
-
-    kc_bty (Banged ty)   = kcHsType ty
-    kc_bty (Unbanged ty) = kcHsType ty
-    kc_bty (Unpacked ty) = kcHsType ty
-
-    kc_field (_, bty)    = kc_bty bty
-\end{code}
-
-
 %************************************************************************
 %*									*
 \subsection{Type checking}
@@ -107,58 +62,36 @@ kcConDecl (ConDecl _ _ ex_tvs ex_ctxt details loc)
 %************************************************************************
 
 \begin{code}
-tcTyDecl :: RecFlag -> FiniteMap Name ArgVrcs -> RenamedTyClDecl -> TcM s (Name, TcTyThing)
-
-tcTyDecl is_rec rec_vrcs (TySynonym tycon_name tyvar_names rhs src_loc)
-  = tcLookupTy tycon_name				`thenNF_Tc` \ (tycon_kind, ASynTyCon _ arity) ->
-    tcExtendTopTyVarScope tycon_kind tyvar_names	$ \ tyvars _ ->
-    tcHsTopTypeKind rhs					`thenTc` \ (_, rhs_ty) ->
+tcTyDecl1 :: RenamedTyClDecl -> TcM s (Name, TyThingDetails)
+tcTyDecl1 (TySynonym tycon_name tyvar_names rhs src_loc)
+  = tcLookupTy tycon_name			`thenNF_Tc` \ (ATyCon tycon) ->
+    tcExtendTyVarEnv (tyConTyVars tycon)	$
+    tcHsSigType rhs				`thenTc` \ rhs_ty ->
 	-- If the RHS mentions tyvars that aren't in scope, we'll 
 	-- quantify over them.  With gla-exts that's right, but for H98
-	-- we should complain. We can't do that here without falling into
-	-- a black hole, so we do it in rnDecl (TySynonym case)
+	-- we should complain. We can now do that here without falling into
+	-- a black hole, we still do it in rnDecl (TySynonym case)
+    returnTc (tycon_name, SynTyDetails rhs_ty)
+
+tcTyDecl1 (TyData _ context tycon_name _ con_decls _ derivings _  src_loc)
+  = tcLookupTy tycon_name			`thenNF_Tc` \ (ATyCon tycon) ->
     let
-	-- Construct the tycon
-        argvrcs = lookupWithDefaultFM rec_vrcs (pprPanic "tcTyDecl: argvrcs:" $ ppr tycon_name)
-                                      tycon_name
-	tycon = mkSynTyCon tycon_name tycon_kind arity tyvars rhs_ty argvrcs
+	tyvars = tyConTyVars tycon
     in
-    returnTc (tycon_name, ASynTyCon tycon arity)
-
-
-tcTyDecl is_rec rec_vrcs (TyData data_or_new context tycon_name tyvar_names con_decls nconstrs derivings pragmas src_loc)
-  = 	-- Lookup the pieces
-    tcLookupTy tycon_name				`thenNF_Tc` \ (tycon_kind, ADataTyCon rec_tycon) ->
-    tcExtendTopTyVarScope tycon_kind tyvar_names	$ \ tyvars _ ->
+    tcExtendTyVarEnv tyvars				$
 
 	-- Typecheck the pieces
-    tcContext context					`thenTc` \ ctxt ->
-    let ctxt' = classesOfPreds ctxt in
-    mapTc (tcConDecl rec_tycon tyvars ctxt') con_decls	`thenTc` \ data_cons ->
+    tcClassContext context				`thenTc` \ ctxt ->
     tc_derivs derivings					`thenTc` \ derived_classes ->
+    mapTc (tcConDecl tycon tyvars ctxt) con_decls	`thenTc` \ data_cons ->
 
-    let
-	-- Construct the tycon
-	flavour = case data_or_new of
-			NewType -> NewTyCon (mkNewTyConRep tycon)
-			DataType | all isNullaryDataCon data_cons -> EnumTyCon
-				 | otherwise			  -> DataTyCon
-
-        argvrcs = lookupWithDefaultFM rec_vrcs (pprPanic "tcTyDecl: argvrcs:" $ ppr tycon_name)
-                                      tycon_name
-
-	tycon = mkAlgTyCon tycon_name tycon_kind tyvars ctxt' argvrcs
-			   data_cons nconstrs
-			   derived_classes
-			   flavour is_rec
-    in
-    returnTc (tycon_name, ADataTyCon tycon)
+    returnTc (tycon_name, DataTyDetails ctxt data_cons derived_classes)
   where
-	tc_derivs Nothing   = returnTc []
-	tc_derivs (Just ds) = mapTc tc_deriv ds
+    tc_derivs Nothing   = returnTc []
+    tc_derivs (Just ds) = mapTc tc_deriv ds
 
-	tc_deriv name = tcLookupTy name `thenTc` \ (_, AClass clas _) ->
-			returnTc clas
+    tc_deriv name = tcLookupTy name `thenTc` \ (AClass clas) ->
+		    returnTc clas
 \end{code}
 
 \begin{code}
@@ -185,39 +118,48 @@ mkNewTyConRep tc
 
 %************************************************************************
 %*									*
-\subsection{Type check constructors}
+\subsection{Kind and type check constructors}
 %*									*
 %************************************************************************
 
 \begin{code}
-tcConDecl :: TyCon -> [TyVar] -> [(Class,[Type])] -> RenamedConDecl -> TcM s DataCon
+kcConDetails :: RenamedContext -> ConDetails Name -> TcM s ()
+kcConDetails ex_ctxt details
+  = kcHsContext ex_ctxt		`thenTc_`
+    kc_con_details details
+  where
+    kc_con_details (VanillaCon btys)    = mapTc_ kc_bty btys
+    kc_con_details (InfixCon bty1 bty2) = mapTc_ kc_bty [bty1,bty2]
+    kc_con_details (NewCon ty _)        = kcHsSigType ty
+    kc_con_details (RecCon flds)        = mapTc_ kc_field flds
+
+    kc_field (_, bty) = kc_bty bty
+
+    kc_bty bty = kcHsSigType (getBangType bty)
+
+tcConDecl :: TyCon -> [TyVar] -> ClassContext -> RenamedConDecl -> TcM s DataCon
 
 tcConDecl tycon tyvars ctxt (ConDecl name wkr_name ex_tvs ex_ctxt details src_loc)
-  = tcAddSrcLoc src_loc			$
-    tcExtendTyVarScope ex_tvs		$ \ ex_tyvars -> 
-    tcContext ex_ctxt			`thenTc` \ ex_theta ->
-    let 
-	ex_ctxt' = classesOfPreds ex_theta
-    in
-    tc_con_decl_help tycon tyvars ctxt name wkr_name ex_tyvars ex_ctxt' details
-
-tc_con_decl_help tycon tyvars ctxt name wkr_name ex_tyvars ex_theta details
-  = case details of
-	VanillaCon btys    -> tc_datacon btys
-	InfixCon bty1 bty2 -> tc_datacon [bty1,bty2]
-	NewCon ty mb_f	   -> tc_newcon ty mb_f
-	RecCon fields	   -> tc_rec_con fields
+  = tcAddSrcLoc src_loc					$
+    kcTyVarScope ex_tvs (kcConDetails ex_ctxt details)	`thenTc` \ ex_tyvars -> 
+    tcExtendTyVarEnv ex_tyvars				$
+    tcClassContext ex_ctxt				`thenTc` \ ex_theta ->
+    case details of
+	VanillaCon btys    -> tc_datacon ex_tyvars ex_theta btys
+	InfixCon bty1 bty2 -> tc_datacon ex_tyvars ex_theta [bty1,bty2]
+	NewCon ty mb_f	   -> tc_newcon  ex_tyvars ex_theta ty mb_f
+	RecCon fields	   -> tc_rec_con ex_tyvars ex_theta fields
   where
-    tc_datacon btys
+    tc_datacon ex_tyvars ex_theta btys
       = let
-	    arg_stricts = map get_strictness btys
-	    tys	        = map get_pty btys
+	    arg_stricts = map getBangStrictness btys
+	    tys	        = map getBangType btys
         in
-	mapTc tcHsTopType tys `thenTc` \ arg_tys ->
-	mk_data_con arg_stricts arg_tys []
+	mapTc tcHsSigType tys 	`thenTc` \ arg_tys ->
+	mk_data_con ex_tyvars ex_theta arg_stricts arg_tys []
 
-    tc_newcon ty mb_f
-      = tcHsTopBoxedType ty	`thenTc` \ arg_ty ->
+    tc_newcon ex_tyvars ex_theta ty mb_f
+      = tcHsBoxedSigType ty	`thenTc` \ arg_ty ->
 	    -- can't allow an unboxed type here, because we're effectively
 	    -- going to remove the constructor while coercing it to a boxed type.
 	let
@@ -226,39 +168,33 @@ tc_con_decl_help tycon tyvars ctxt name wkr_name ex_tyvars ex_theta details
 	      Nothing -> []
 	      Just f  -> [mkFieldLabel (getName f) tycon arg_ty (head allFieldLabelTags)]
         in	      
-	mk_data_con [notMarkedStrict] [arg_ty] field_label
+	mk_data_con ex_tyvars ex_theta [notMarkedStrict] [arg_ty] field_label
 
-    tc_rec_con fields
-      = checkTc (null ex_tyvars) (exRecConErr name)	    `thenTc_`
-	mapTc tc_field fields	`thenTc` \ field_label_infos_s ->
+    tc_rec_con ex_tyvars ex_theta fields
+      = checkTc (null ex_tyvars) (exRecConErr name)	`thenTc_`
+	mapTc tc_field (fields `zip` allFieldLabelTags)	`thenTc` \ field_labels_s ->
 	let
-	    field_label_infos = concat field_label_infos_s
-	    arg_stricts       = [strict | (_, _, strict) <- field_label_infos]
-	    arg_tys	      = [ty     | (_, ty, _)     <- field_label_infos]
-
-	    field_labels      = [ mkFieldLabel (getName name) tycon ty tag 
-			      | ((name, ty, _), tag) <- field_label_infos `zip` allFieldLabelTags ]
+	    field_labels = concat field_labels_s
+	    arg_stricts = [str | (ns, bty) <- fields, 
+				  let str = getBangStrictness bty, 
+				  n <- ns		-- One for each.  E.g   x,y,z :: !Int
+			  ]
 	in
-	mk_data_con arg_stricts arg_tys field_labels
-
-    tc_field (field_label_names, bty)
-      = tcHsTopType (get_pty bty)	`thenTc` \ field_ty ->
-	returnTc [(name, field_ty, get_strictness bty) | name <- field_label_names]
-
-    mk_data_con arg_stricts arg_tys fields
-      = 	-- Now we've checked all the field types we must
-		-- zonk the existential tyvars to finish the kind
-		-- inference on their kinds, and commit them to being
-		-- immutable type variables.  (The top-level tyvars are
-		-- already fixed, by the preceding kind-inference pass.)
-	mapNF_Tc zonkTcTyVarToTyVar ex_tyvars	`thenNF_Tc` \ ex_tyvars' ->
-	zonkTcClassConstraints	ex_theta	`thenNF_Tc` \ ex_theta' ->
-	let
+	mk_data_con ex_tyvars ex_theta arg_stricts 
+		    (map fieldLabelType field_labels) field_labels
+
+    tc_field ((field_label_names, bty), tag)
+      = tcHsSigType (getBangType bty)	`thenTc` \ field_ty ->
+	returnTc [mkFieldLabel (getName name) tycon field_ty tag | name <- field_label_names]
+
+    mk_data_con ex_tyvars ex_theta arg_stricts arg_tys fields
+      = let
 	   data_con = mkDataCon name arg_stricts fields
 		      	   tyvars (thinContext arg_tys ctxt)
-			   ex_tyvars' ex_theta'
+			   ex_tyvars ex_theta
 		      	   arg_tys
 		      	   tycon data_con_id data_con_wrap_id
+
 	   data_con_id      = mkDataConId wkr_name data_con
 	   data_con_wrap_id = mkDataConWrapId data_con
 	in
@@ -272,14 +208,10 @@ thinContext arg_tys ctxt
       arg_tyvars = tyVarsOfTypes arg_tys
       in_arg_tys (clas,tys) = not $ isEmptyVarSet $ 
 			      tyVarsOfTypes tys `intersectVarSet` arg_tyvars
-  
-get_strictness (Banged   _) = markedStrict
-get_strictness (Unbanged _) = notMarkedStrict
-get_strictness (Unpacked _) = markedUnboxed
-
-get_pty (Banged ty)   = ty
-get_pty (Unbanged ty) = ty
-get_pty (Unpacked ty) = ty
+
+getBangStrictness (Banged   _) = markedStrict
+getBangStrictness (Unbanged _) = notMarkedStrict
+getBangStrictness (Unpacked _) = markedUnboxed
 \end{code}
 
 
diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 81b4ee8ecd4be4fcb560116402f2474d88b26f0c..509bea6f6cc10d11f4816f3b2fdd03ac286d0b9c 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -12,9 +12,6 @@ module TcType (
   newTyVarTy,		-- Kind -> NF_TcM s TcType
   newTyVarTys,		-- Int -> Kind -> NF_TcM s [TcType]
 
-  newTyVarTy_OpenKind,	-- NF_TcM s TcType
-  newOpenTypeKind,	-- NF_TcM s TcKind
-
   -----------------------------------------
   TcType, TcTauType, TcThetaType, TcRhoType,
 
@@ -29,21 +26,15 @@ module TcType (
   tcInstSigVar,
   tcInstTcType,
 
-  typeToTcType,
-
-  tcTypeKind,		-- :: TcType -> NF_TcM s TcKind
   --------------------------------
   TcKind,
-  newKindVar, newKindVars,
-  kindToTcKind,
-  zonkTcKind,
+  newKindVar, newKindVars, newBoxityVar,
 
   --------------------------------
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
+  zonkTcTyVar, zonkTcTyVars, zonkTcSigTyVars,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
 
-  zonkTcTypeToType, zonkTcTyVarToTyVar,
-  zonkTcKindToKind
+  zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
 
   ) where
 
@@ -51,13 +42,14 @@ module TcType (
 
 
 -- friends:
-import TypeRep		( Type(..), Kind, TyNote(..), 
-			  typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
-			)  -- friend
+import TypeRep		( Type(..), Kind, TyNote(..) )  -- friend
 import Type		( ThetaType, PredType(..),
-			  mkAppTy, mkTyConApp,
+			  getTyVar, mkAppTy, mkTyConApp,
 			  splitPredTy_maybe, splitForAllTys, isNotUsgTy,
 			  isTyVarTy, mkTyVarTy, mkTyVarTys, 
+			  openTypeKind, boxedTypeKind, 
+			  superKind, superBoxity, 
+			  defaultKind, boxedBoxity
 			)
 import Subst		( Subst, mkTopTyVarSubst, substTy )
 import TyCon		( tyConKind, mkPrimTyCon )
@@ -68,7 +60,7 @@ import Var		( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
 import TcMonad
 import TysWiredIn	( voidTy )
 
-import Name		( NamedThing(..), setNameUnique, mkSysLocalName,
+import Name		( Name, NamedThing(..), setNameUnique, mkSysLocalName,
 			  mkDerivedName, mkDerivedTyConOcc
 			)
 import Unique		( Unique, Uniquable(..) )
@@ -77,19 +69,6 @@ import Outputable
 \end{code}
 
 
-
-Coercions
-~~~~~~~~~~
-Type definitions are in TcMonad.lhs
-
-\begin{code}
-typeToTcType :: Type -> TcType
-typeToTcType ty =  ty
-
-kindToTcKind :: Kind -> TcKind
-kindToTcKind kind = kind
-\end{code}
-
 Utility functions
 ~~~~~~~~~~~~~~~~~
 These tcSplit functions are like their non-Tc analogues, but they
@@ -146,16 +125,11 @@ newKindVar
 newKindVars :: Int -> NF_TcM s [TcKind]
 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 
--- Returns a type variable of kind (Type bv) where bv is a new boxity var
--- Used when you need a type variable that's definitely a , but you don't know
--- what kind of type (boxed or unboxed).
-newTyVarTy_OpenKind :: NF_TcM s TcType
-newTyVarTy_OpenKind = newOpenTypeKind	`thenNF_Tc` \ kind -> 
-		      newTyVarTy kind
-
-newOpenTypeKind :: NF_TcM s TcKind
-newOpenTypeKind = newTyVarTy superBoxity	`thenNF_Tc` \ bv ->
-	   	  returnNF_Tc (mkTyConApp typeCon [bv])
+newBoxityVar :: NF_TcM s TcKind
+newBoxityVar
+  = tcGetUnique 						`thenNF_Tc` \ uniq ->
+    tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity	`thenNF_Tc` \ kv ->
+    returnNF_Tc (TyVarTy kv)
 \end{code}
 
 
@@ -191,26 +165,8 @@ tcInstTyVar tyvar
 	-- in an error message.  -dppr-debug will show up the difference
 	-- Better watch out for this.  If worst comes to worst, just
 	-- use mkSysLocalName.
-
-	kind = tyVarKind tyvar
     in
-
-	-- Hack alert!  Certain system functions (like error) are quantified
-	-- over type variables with an 'open' kind (a :: ?).  When we instantiate
-	-- these tyvars we want to make a type variable whose kind is (Type bv)
-	-- where bv is a boxity variable.  This makes sure it's a type, but 
-	-- is open about its boxity.  We *don't* want to give the thing the
-	-- kind '?' (= Type AnyBox).  
-	--
-	-- This is all a hack to avoid giving error it's "proper" type:
-	--	 error :: forall bv. forall a::Type bv. String -> a
-
-    (if kind == openTypeKind then
-	newOpenTypeKind	
-     else
-	returnNF_Tc kind)	`thenNF_Tc` \ kind' ->
-
-    tcNewMutTyVar name kind'
+    tcNewMutTyVar name (tyVarKind tyvar)
 
 tcInstSigVar tyvar	-- Very similar to tcInstTyVar
   = tcGetUnique 	`thenNF_Tc` \ uniq ->
@@ -307,16 +263,16 @@ short_out other_ty = returnNF_Tc other_ty
 zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 
-zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
-zonkTcTyVarBndr tyvar
-  = zonkTcTyVar tyvar	`thenNF_Tc` \ ty ->
-    case ty of
-	TyVarTy tyvar' -> returnNF_Tc tyvar'
-	_	       -> pprTrace "zonkTcTyVarBndr" (ppr tyvar <+> ppr ty) $
-			  returnNF_Tc tyvar
-	
 zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
+
+zonkTcSigTyVars :: [TcTyVar] -> NF_TcM s [TcTyVar]
+-- This guy is to zonk the tyvars we're about to feed into tcSimplify
+-- Usually this job is done by checkSigTyVars, but in a couple of places
+-- that is overkill, so we use this simpler chap
+zonkTcSigTyVars tyvars
+  = zonkTcTyVars tyvars	`thenNF_Tc` \ tys ->
+    returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
 \end{code}
 
 -----------------  Types
@@ -343,42 +299,40 @@ zonkTcPredType (Class c ts) =
 zonkTcPredType (IParam n t) =
     zonkTcType t	`thenNF_Tc` \ new_t ->
     returnNF_Tc (IParam n new_t)
-
-zonkTcKind :: TcKind -> NF_TcM s TcKind
-zonkTcKind = zonkTcType
 \end{code}
 
 -------------------  These ...ToType, ...ToKind versions
 		     are used at the end of type checking
 
 \begin{code}
-zonkTcKindToKind :: TcKind -> NF_TcM s Kind
-zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
-  where
-	-- Zonk a mutable but unbound kind variable to
-	--	(Type Boxed) 	if it has kind superKind
-	--	Boxed		if it has kind superBoxity
-    zonk_unbound_kind_var kv
-	| super_kind == superKind = tcPutTyVar kv boxedTypeKind
-	| otherwise 		  = ASSERT( super_kind == superBoxity )
-				    tcPutTyVar kv boxedKind
-	where
-	  super_kind = tyVarKind kv
+zonkKindEnv :: [(Name, TcKind)] -> NF_TcM s [(Name, Kind)]
+zonkKindEnv pairs 
+  = mapNF_Tc zonk_it pairs
+ where
+    zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
+			      returnNF_Tc (name, kind)
+
+	-- When zonking a kind, we want to
+	--	zonk a *kind* variable to (Type *)
+	--	zonk a *boxity* variable to *
+    zonk_unbound_kind_var kv | tyVarKind kv == superKind   = tcPutTyVar kv boxedTypeKind
+			     | tyVarKind kv == superBoxity = tcPutTyVar kv boxedBoxity
+			     | otherwise		   = pprPanic "zonkKindEnv" (ppr kv)
 			
-
 zonkTcTypeToType :: TcType -> NF_TcM s Type
 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
   where
 	-- Zonk a mutable but unbound type variable to
-	--	Void		if it has kind (Type Boxed)
-	--	Voidxxx		otherwise
+	--	Void		if it has kind Boxed
+	--	:Void		otherwise
     zonk_unbound_tyvar tv
-	= zonkTcKindToKind (tyVarKind tv)	`thenNF_Tc` \ kind ->
-	  if kind == boxedTypeKind then
-		tcPutTyVar tv voidTy	-- Just to avoid creating a new tycon in
-					-- this vastly common case
-	  else
-		tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
+	| kind == boxedTypeKind
+	= tcPutTyVar tv voidTy	-- Just to avoid creating a new tycon in
+				-- this vastly common case
+	| otherwise
+	= tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
+	where
+	  kind = tyVarKind tv
 
     mk_void_tycon tv kind	-- Make a new TyCon with the same kind as the 
 				-- type variable tv.  Same name too, apart from
@@ -388,18 +342,19 @@ zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 	  tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
 
 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
--- of a type variable, at the *end* of type checking.
--- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
--- zonks its kind, and then makes an immutable version of tv and binds tv to it.
+-- of a type variable, at the *end* of type checking.  It changes
+-- the *mutable* type variable into an *immutable* one.
+-- 
+-- It does this by making an immutable version of tv and binds tv to it.
 -- Now any bound occurences of the original type variable will get 
 -- zonked to the immutable version.
 
 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar
 zonkTcTyVarToTyVar tv
-  = zonkTcKindToKind (tyVarKind tv)	`thenNF_Tc` \ kind ->
-    let
-		-- Make an immutable version
-	immut_tv    = mkTyVar (tyVarName tv) kind
+  = let
+		-- Make an immutable version, defaulting 
+		-- the kind to boxed if necessary
+	immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
 	immut_tv_ty = mkTyVarTy immut_tv
 
         zap tv = tcPutTyVar tv immut_tv_ty
@@ -408,7 +363,8 @@ zonkTcTyVarToTyVar tv
 	-- If the type variable is mutable, then bind it to immut_tv_ty
 	-- so that all other occurrences of the tyvar will get zapped too
     zonkTyVar zap tv		`thenNF_Tc` \ ty2 ->
-    ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
+
+    WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
 
     returnNF_Tc immut_tv
 \end{code}
@@ -463,12 +419,11 @@ zonkType unbound_var_fn ty
 				    returnNF_Tc (mkAppTy fun' arg')
 
 	-- The two interesting cases!
-    go (TyVarTy tyvar)  	  = zonkTyVar unbound_var_fn tyvar
+    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 
-    go (ForAllTy tyvar ty)
-	= zonkTcTyVarToTyVar tyvar	`thenNF_Tc` \ tyvar' ->
-	  go ty				`thenNF_Tc` \ ty' ->
-	  returnNF_Tc (ForAllTy tyvar' ty')
+    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar	`thenNF_Tc` \ tyvar' ->
+			     go ty			`thenNF_Tc` \ ty' ->
+			     returnNF_Tc (ForAllTy tyvar' ty')
 
 
 zonkTyVar :: (TcTyVar -> NF_TcM s Type)		-- What to do for an unbound mutable variable
@@ -488,49 +443,3 @@ zonkTyVar unbound_var_fn tyvar
                            zonkType unbound_var_fn other_ty	-- Bound
 \end{code}
 
-%************************************************************************
-%*									*
-\subsection{tcTypeKind}
-%*									*
-%************************************************************************
-
-Sadly, we need a Tc version of typeKind, that looks though mutable
-kind variables.  See the notes with Type.typeKind for the typeKindF nonsense
-
-This is pretty gruesome.
-
-\begin{code}
-tcTypeKind :: TcType -> NF_TcM s TcKind
-
-tcTypeKind (TyVarTy tyvar)	= returnNF_Tc (tyVarKind tyvar)
-tcTypeKind (TyConApp tycon tys)	= foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
-tcTypeKind (NoteTy _ ty)	= tcTypeKind ty
-tcTypeKind (AppTy fun arg)	= tcTypeKind fun	`thenNF_Tc` \ fun_kind ->
-				  tcFunResultTy fun_kind
-tcTypeKind (FunTy fun arg)	= tcTypeKindF arg
-tcTypeKind (ForAllTy _ ty)	= tcTypeKindF ty
-
-tcTypeKindF :: TcType -> NF_TcM s TcKind
-tcTypeKindF (NoteTy _ ty)   = tcTypeKindF ty
-tcTypeKindF (FunTy _ ty)    = tcTypeKindF ty
-tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
-tcTypeKindF other	    = tcTypeKind other	`thenNF_Tc` \ kind ->
-			      fix_up kind
-  where
-    fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
-		-- Functions at the type level are always boxed
-    fix_up (NoteTy _ kind)   = fix_up kind
-    fix_up kind@(TyVarTy tv) = tcGetTyVar tv	`thenNF_Tc` \ maybe_ty ->
-			       case maybe_ty of
-				  Just kind' -> fix_up kind'
-				  Nothing  -> returnNF_Tc kind
-    fix_up kind              = returnNF_Tc kind
-
-tcFunResultTy (NoteTy _ ty)   = tcFunResultTy ty
-tcFunResultTy (FunTy arg res) = returnNF_Tc res
-tcFunResultTy (TyVarTy tv)    = tcGetTyVar tv	`thenNF_Tc` \ maybe_ty ->
-			        case maybe_ty of
-				  Just ty' -> tcFunResultTy ty'
-	-- The Nothing case, and the other cases for tcFunResultTy
-	-- should never happen... pattern match failure
-\end{code}
diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index ba131c09d5a33afa9a1df03a72f065a6ddd10eef..7c92681dd5719e5ba095c93a1a8453c08d4d490b 100644
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -9,29 +9,27 @@ updatable substitution).
 \begin{code}
 module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, 
 	         unifyFunTy, unifyListTy, unifyTupleTy,
-	 	 unifyKind, unifyKinds, unifyTypeKind
+	 	 unifyKind, unifyKinds, unifyOpenTypeKind
  ) where
 
 #include "HsVersions.h"
 
 -- friends: 
 import TcMonad
-import TypeRep	( Type(..), funTyCon,
-		  Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
-		)  -- friend
-import Type	( tyVarsOfType,
-		  mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
-                  isNotUsgTy,
-		  splitAppTy_maybe,
+import TypeRep	( Type(..) )  -- friend
+import Type	( funTyCon, Kind, unboxedTypeKind, boxedTypeKind, openTypeKind, 
+		  superBoxity, typeCon, openKindCon, hasMoreBoxityInfo, 
+		  tyVarsOfType, typeKind,
+		  mkTyVarTy, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
+                  isNotUsgTy, splitAppTy_maybe, mkTyConApp, 
 	   	  tidyOpenType, tidyOpenTypes, tidyTyVar
 		)
 import TyCon	( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
 import Name	( hasBetterProv )
 import Var	( TyVar, tyVarKind, varName, isSigTyVar )
 import VarSet	( varSetElems )
-import TcType	( TcType, TcTauType, TcTyVar, TcKind, 
-		  newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind,
-		  tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind
+import TcType	( TcType, TcTauType, TcTyVar, TcKind, newBoxityVar,
+		  newTyVarTy, newTyVarTys, tcGetTyVar, tcPutTyVar, zonkTcType
 		)
 
 -- others:
@@ -62,6 +60,27 @@ unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 	`thenTc_`
 unifyKinds _ _ = panic "unifyKinds: length mis-match"
 \end{code}
 
+\begin{code}
+unifyOpenTypeKind :: TcKind -> TcM s ()	
+-- Ensures that the argument kind is of the form (Type bx)
+-- for some boxity bx
+
+unifyOpenTypeKind ty@(TyVarTy tyvar)
+  = tcGetTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
+    case maybe_ty of
+	Just ty' -> unifyOpenTypeKind ty'
+	other	 -> unify_open_kind_help ty
+
+unifyOpenTypeKind ty
+  = case splitTyConApp_maybe ty of
+	Just (tycon, [_]) | tycon == typeCon -> returnTc ()
+	other				     -> unify_open_kind_help ty
+
+unify_open_kind_help ty	-- Revert to ordinary unification
+  = newBoxityVar 	`thenNF_Tc` \ boxity ->
+    unifyKind ty (mkTyConApp typeCon [boxity])
+\end{code}
+
 
 %************************************************************************
 %*									*
@@ -122,7 +141,10 @@ We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 
 \begin{code}
 uTys :: TcTauType -> TcTauType	-- Error reporting ty1 and real ty1
+				-- ty1 is the *expected* type
+
      -> TcTauType -> TcTauType	-- Error reporting ty2 and real ty2
+				-- ty2 is the *actual* type
      -> TcM s ()
 
 	-- Always expand synonyms (see notes at end)
@@ -141,14 +163,18 @@ uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
 
 	-- Type constructors must match
 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
-  = checkTcM (cons_match && length tys1 == length tys2) 
-	     (unifyMisMatch ps_ty1 ps_ty2)			`thenTc_`
-    unifyTauTyLists tys1 tys2
-  where
-	-- The AnyBox wild card matches anything
-    cons_match =  con1 == con2 
-	       || con1 == anyBoxCon
-	       || con2 == anyBoxCon
+  | con1 == con2 && length tys1 == length tys2
+  = unifyTauTyLists tys1 tys2
+
+  | con1 == openKindCon
+	-- When we are doing kind checking, we might match a kind '?' 
+	-- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
+	-- (CCallable Int) and (CCallable Int#) are both OK
+  = unifyOpenTypeKind ps_ty2
+
+  | otherwise
+  = unifyMisMatch ps_ty1 ps_ty2
+
 
 	-- Applications need a bit of care!
 	-- They can match FunTy and TyConApp, so use splitAppTy_maybe
@@ -270,34 +296,37 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
     case maybe_ty2 of
 	Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 
-	Nothing -> checkKinds swapped tv1 ty2			`thenTc_`
+	Nothing | tv1_dominates_tv2 
+
+		-> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
+		   tcPutTyVar tv2 (TyVarTy tv1)		`thenNF_Tc_`
+		   returnTc ()
+		|  otherwise
 
-		   if tv1 `dominates` tv2 then
-			tcPutTyVar tv2 (TyVarTy tv1)		`thenNF_Tc_`
-			returnTc ()
-		   else
-                        ASSERT( isNotUsgTy ps_ty2 )
-			tcPutTyVar tv1 ps_ty2			`thenNF_Tc_`
-			returnTc ()
+		-> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
+                   (ASSERT( isNotUsgTy ps_ty2 )
+		    tcPutTyVar tv1 ps_ty2		`thenNF_Tc_`
+	  	    returnTc ())
   where
-    tv1 `dominates` tv2 =  isSigTyVar tv1 
+    k1 = tyVarKind tv1
+    k2 = tyVarKind tv2
+    tv1_dominates_tv2 =    isSigTyVar tv1 
 				-- Don't unify a signature type variable if poss
+			|| k2 == openTypeKind
+				-- Try to get rid of open type variables as soon as poss
 			|| varName tv1 `hasBetterProv` varName tv2 
 				-- Try to update sys-y type variables in preference to sig-y ones
 
 	-- Second one isn't a type variable
 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
-  | non_var_ty2 == anyBoxKind
-	-- If the 
-  = returnTc ()
-
-  | otherwise
   = checkKinds swapped tv1 non_var_ty2			`thenTc_`
     occur_check non_var_ty2				`thenTc_`
     ASSERT( isNotUsgTy ps_ty2 )
     checkTcM (not (isSigTyVar tv1))
 	     (failWithTcM (unifyWithSigErr tv1 ps_ty2))	`thenTc_`
 
+    WARN( not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1), (ppr tv1 <+> ppr (tyVarKind tv1)) $$
+									(ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)) )
     tcPutTyVar tv1 non_var_ty2				`thenNF_Tc_`
 	-- This used to say "ps_ty2" instead of "non_var_ty2"
 
@@ -334,21 +363,22 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 		other	  -> returnTc ()
 
 checkKinds swapped tv1 ty2
+-- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
+-- We need to check that we don't unify a boxed type variable with an
+-- unboxed type: e.g.  (id 3#) is illegal
+  | tk1 == boxedTypeKind && tk2 == unboxedTypeKind
   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)	$
-
-	-- We have to use tcTypeKind not just typeKind to get the
-	-- kind of ty2, because there might be mutable kind variables
-	-- in the way.  For example, suppose that ty2 :: (a b), and
-	-- the kind of 'a' is a kind variable 'k' that has (presumably)
-	-- been unified with 'k1 -> k2'.
-    tcTypeKind ty2		`thenNF_Tc` \ k2 ->
-
-    if swapped then
-	unifyKind k2 (tyVarKind tv1)
-    else
-	unifyKind (tyVarKind tv1) k2
+    unifyMisMatch k1 k2
+  | otherwise
+  = returnTc ()
+  where
+    (k1,k2) | swapped   = (tk2,tk1)
+	    | otherwise = (tk1,tk2)
+    tk1 = tyVarKind tv1
+    tk2 = typeKind ty2
 \end{code}
 
+
 %************************************************************************
 %*									*
 \subsection[Unify-fun]{@unifyFunTy@}
@@ -373,8 +403,8 @@ unifyFunTy ty
 	Nothing 	 -> unify_fun_ty_help ty
 
 unify_fun_ty_help ty	-- Special cases failed, so revert to ordinary unification
-  = newTyVarTy_OpenKind		`thenNF_Tc` \ arg ->
-    newTyVarTy_OpenKind		`thenNF_Tc` \ res ->
+  = newTyVarTy openTypeKind	`thenNF_Tc` \ arg ->
+    newTyVarTy openTypeKind	`thenNF_Tc` \ res ->
     unifyTauTy ty (mkFunTy arg res)	`thenTc_`
     returnTc (arg,res)
 \end{code}
@@ -418,32 +448,12 @@ unifyTupleTy boxity arity ty
 	other -> unify_tuple_ty_help boxity arity ty
 
 unify_tuple_ty_help boxity arity ty
-  = mapNF_Tc new_tyvar [1..arity]			`thenNF_Tc` \ arg_tys ->
+  = newTyVarTys arity kind				`thenNF_Tc` \ arg_tys ->
     unifyTauTy ty (mkTupleTy boxity arity arg_tys)	`thenTc_`
     returnTc arg_tys
   where
-    new_tyvar _ | isBoxed boxity = newTyVarTy boxedTypeKind
-	        | otherwise      = newTyVarTy_OpenKind
-\end{code}
-
-Make sure a kind is of the form (Type b) for some boxity b.
-
-\begin{code}
-unifyTypeKind  :: TcKind -> TcM s ()
-unifyTypeKind kind@(TyVarTy kv)
-  = tcGetTyVar kv 	`thenNF_Tc` \ maybe_kind ->
-    case maybe_kind of
-	Just kind' -> unifyTypeKind kind'
-	Nothing    -> unify_type_kind_help kind
-
-unifyTypeKind kind
-  = case splitTyConApp_maybe kind of
-	Just (tycon, [_]) | tycon == typeCon -> returnTc ()
-	other				     -> unify_type_kind_help kind
-
-unify_type_kind_help kind
-  = newOpenTypeKind	`thenNF_Tc` \ expected_kind ->
-    unifyKind expected_kind kind
+    kind | isBoxed boxity = boxedTypeKind
+	 | otherwise      = openTypeKind
 \end{code}
 
 
@@ -472,15 +482,19 @@ unifyCtxt s ty1 ty2 tidy_env	-- ty1 expected, ty2 inferred
 		    (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
 
 unifyKindCtxt swapped tv1 ty2 tidy_env	-- not swapped => tv1 expected, ty2 inferred
-  = returnNF_Tc (env2, ptext SLIT("When matching types") <+> 
-		       sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
+	-- tv1 is zonked already
+  = zonkTcType ty2	`thenNF_Tc` \ ty2' ->
+    returnNF_Tc (err ty2')
   where
-    (pp_expected, pp_actual) | swapped   = (pp2, pp1)
-			     | otherwise = (pp1, pp2)
-    (env1, tv1') = tidyTyVar tidy_env tv1
-    (env2, ty2') = tidyOpenType  env1     ty2
-    pp1 = ppr tv1'
-    pp2 = ppr ty2'
+    err ty2 = (env2, ptext SLIT("When matching types") <+> 
+		     sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
+	    where
+	      (pp_expected, pp_actual) | swapped   = (pp2, pp1)
+				       | otherwise = (pp1, pp2)
+	      (env1, tv1') = tidyTyVar tidy_env tv1
+	      (env2, ty2') = tidyOpenType  env1 ty2
+	      pp1 = ppr tv1'
+	      pp2 = ppr ty2'
 
 unifyMisMatch ty1 ty2
   = zonkTcType ty1	`thenNF_Tc` \ ty1' ->
diff --git a/ghc/compiler/types/Class.lhs b/ghc/compiler/types/Class.lhs
index a04cdcc3ac7feddcfc55f752016ed377441e87c4..b3e47e415383d45756f8d3b123dcfdcfa32ca3fd 100644
--- a/ghc/compiler/types/Class.lhs
+++ b/ghc/compiler/types/Class.lhs
@@ -7,7 +7,7 @@
 module Class (
 	Class, ClassOpItem, ClassPred, ClassContext, FunDep,
 
-	mkClass, classTyVars,
+	mkClass, classTyVars, classArity,
 	classKey, className, classSelIds, classTyCon,
 	classBigSig, classExtraBigSig, classTvsFds
     ) where
@@ -19,6 +19,7 @@ import {-# SOURCE #-} TypeRep	( Type )
 
 import Var		( Id, TyVar )
 import Name		( NamedThing(..), Name )
+import BasicTypes	( Arity )
 import Unique		( Unique, Uniquable(..) )
 import Outputable
 import Util
@@ -69,7 +70,7 @@ The @mkClass@ function fills in the indirect superclasses.
 mkClass :: Name -> [TyVar]
 	-> [([TyVar], [TyVar])]
 	-> [(Class,[Type])] -> [Id]
-	-> [(Id, Id, Bool)]
+	-> [ClassOpItem]
 	-> TyCon
 	-> Class
 
@@ -94,6 +95,10 @@ mkClass name tyvars fds super_classes superdict_sels
 The rest of these functions are just simple selectors.
 
 \begin{code}
+classArity :: Class -> Arity
+classArity clas = length (classTyVars clas)
+	-- Could memoise this
+
 classSelIds (Class {classSCSels = sc_sels, classOpStuff = op_stuff})
   = sc_sels ++ [op_sel | (op_sel, _, _) <- op_stuff]
 
diff --git a/ghc/compiler/types/FunDeps.lhs b/ghc/compiler/types/FunDeps.lhs
index 108fb1c6435aea413536eca3d31b1c5a296b8dc5..dc7c3914314bddee49ded406daa883c9c80e9c2e 100644
--- a/ghc/compiler/types/FunDeps.lhs
+++ b/ghc/compiler/types/FunDeps.lhs
@@ -21,8 +21,10 @@ import Type		( Type, tyVarsOfTypes )
 import Outputable	( Outputable, SDoc, interppSP, ptext, empty, hsep, punctuate, comma )
 import UniqSet
 import VarSet
+import VarEnv
 import Unique		( Uniquable )
 import List		( elemIndex )
+import Util		( zipEqual )
 \end{code}
 
 
@@ -64,23 +66,20 @@ ounion (x:xs) ys
     where
 	(ys', b) = ounion xs ys
 
-instantiateFdClassTys :: Class -> [a] -> [([a], [a])]
+instantiateFdClassTys :: Class -> [Type] -> [FunDep Type]
 -- Get the FDs of the class, and instantiate them
-instantiateFdClassTys clas ts
-  = map (lookupInstFundep tyvars ts) fundeps
+instantiateFdClassTys clas tys
+  = [(map lookup us, map lookup vs) | (us,vs) <- fundeps]
   where
     (tyvars, fundeps) = classTvsFds clas
-    lookupInstFundep tyvars ts (us, vs)
-	= (lookupInstTys tyvars ts us, lookupInstTys tyvars ts vs)
-
-lookupInstTys tyvars ts = map (lookupInstTy tyvars ts)
-lookupInstTy tyvars ts u = ts !! i
-    where Just i = elemIndex u tyvars
+    env       = mkVarEnv (zipEqual "instantiateFdClassTys" tyvars tys)
+    lookup tv = lookupVarEnv_NF env tv
 
 tyVarFunDep :: [FunDep Type] -> [FunDep TyVar]
 tyVarFunDep fdtys 
   = [(getTyvars xs, getTyvars ys) | (xs, ys) <- fdtys]
-  where getTyvars = varSetElems . tyVarsOfTypes
+  where 
+    getTyvars = varSetElems . tyVarsOfTypes
 
 pprFundeps :: Outputable a => [FunDep a] -> SDoc
 pprFundeps [] = empty
diff --git a/ghc/compiler/types/Type.lhs b/ghc/compiler/types/Type.lhs
index e3c4b78e5c376d689772576ef78cbd348bc50f3f..109c8e4e5448ef4bd71652e5fbc4bcf397713150 100644
--- a/ghc/compiler/types/Type.lhs
+++ b/ghc/compiler/types/Type.lhs
@@ -9,21 +9,17 @@ module Type (
 	Type,
 	Kind, TyVarSubst,
 
-	superKind, superBoxity,				-- :: SuperKind
-
-	boxedKind,					-- :: Kind :: BX
-	anyBoxKind,					-- :: Kind :: BX
-	typeCon,					-- :: KindCon :: BX -> KX
-	anyBoxCon,					-- :: KindCon :: BX
-
-	boxedTypeKind, unboxedTypeKind, openTypeKind, 	-- Kind :: superKind
-
-	mkArrowKind, mkArrowKinds, -- mentioned below: hasMoreBoxityInfo,
+	superKind, superBoxity,				-- KX and BX respectively
+	boxedBoxity, unboxedBoxity, 			-- :: BX
+	openKindCon, 					-- :: KX
+	typeCon,					-- :: BX -> KX
+	boxedTypeKind, unboxedTypeKind, openTypeKind, 	-- :: KX
+	mkArrowKind, mkArrowKinds,			-- :: KX -> KX -> KX
 
 	funTyCon,
 
         -- exports from this module:
-        hasMoreBoxityInfo,
+        hasMoreBoxityInfo, defaultKind,
 
 	mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
 
@@ -122,13 +118,13 @@ import UniqSet		( sizeUniqSet )		-- Should come via VarSet
 \begin{code}
 hasMoreBoxityInfo :: Kind -> Kind -> Bool
 hasMoreBoxityInfo k1 k2
-  | k2 == openTypeKind = ASSERT( is_type_kind k1) True
+  | k2 == openTypeKind = True
   | otherwise	       = k1 == k2
-  where
-	-- Returns true for things of form (Type x)
-    is_type_kind k = case splitTyConApp_maybe k of
-			Just (tc,[_]) -> tc == typeCon
-			Nothing	      -> False
+
+defaultKind :: Kind -> Kind
+-- Used when generalising: default kind '?' to '*'
+defaultKind kind | kind == openTypeKind = boxedTypeKind
+	         | otherwise	 	= kind
 \end{code}
 
 
@@ -710,9 +706,8 @@ ipName_maybe _		  = Nothing
 
 classesToPreds cts = map (uncurry Class) cts
 
-classesOfPreds theta = concatMap cvt theta
-    where cvt (Class clas tys) = [(clas, tys)]
-	  cvt (IParam _   _  ) = []
+classesOfPreds :: ThetaType -> ClassContext
+classesOfPreds theta = [(clas,tys) | Class clas tys <- theta]
 \end{code}
 
 @isTauTy@ tests for nested for-alls.
@@ -785,9 +780,15 @@ typeKind (TyConApp tycon tys)	= foldr (\_ k -> funResultTy k) (tyConKind tycon)
 typeKind (NoteTy _ ty)		= typeKind ty
 typeKind (AppTy fun arg)	= funResultTy (typeKind fun)
 
-typeKind (FunTy arg res)	= boxedTypeKind	-- A function is boxed regardless of its result type
-						-- No functions at the type level, hence we don't need
-						-- to say (typeKind res).
+typeKind (FunTy arg res)	= fix_up (typeKind res)
+				where
+				  fix_up kind = case splitTyConApp_maybe kind of
+						  Just (tycon, [_]) | tycon == typeCon	-> boxedTypeKind
+						  other					-> kind
+		-- The basic story is 
+		-- 	typeKind (FunTy arg res) = typeKind res
+		-- But a function is boxed regardless of its result type
+		-- Hencd the strange fix-up
 
 typeKind (ForAllTy tv ty)	= typeKind ty
 \end{code}
diff --git a/ghc/compiler/types/TypeRep.lhs b/ghc/compiler/types/TypeRep.lhs
index b71576bf060359506b4ee86852c4fbe6723bd013..26e507839403b096c9f9b110e3cdbc91f8c5cba6 100644
--- a/ghc/compiler/types/TypeRep.lhs
+++ b/ghc/compiler/types/TypeRep.lhs
@@ -8,16 +8,12 @@ module TypeRep (
 	Type(..), TyNote(..), UsageAnn(..),		-- Representation visible to friends
 	Kind, TyVarSubst,
 
-	superKind, superBoxity,				-- :: SuperKind
-
-	boxedKind,					-- :: Kind :: BX
-	anyBoxKind,					-- :: Kind :: BX
-	typeCon,					-- :: KindCon :: BX -> KX
-	anyBoxCon,					-- :: KindCon :: BX
-
-	boxedTypeKind, unboxedTypeKind, openTypeKind, 	-- Kind :: superKind
-
-	mkArrowKind, mkArrowKinds,
+	superKind, superBoxity,				-- KX and BX respectively
+	boxedBoxity, unboxedBoxity, 			-- :: BX
+	openKindCon, 					-- :: KX
+	typeCon,					-- :: BX -> KX
+	boxedTypeKind, unboxedTypeKind, openTypeKind, 	-- :: KX
+	mkArrowKind, mkArrowKinds,			-- :: KX -> KX -> KX
 
 	funTyCon
     ) where
@@ -150,27 +146,41 @@ data UsageAnn
 
 Kinds
 ~~~~~
-k::K = Type bx
-     | k -> k
-     | kv
+kind :: KX = kind -> kind
+           | Type boxity	-- (Type *) is printed as just *
+				-- (Type #) is printed as just #
+
+           | OpenKind		-- Can be boxed or unboxed
+				-- Printed '?'
+
+           | kv			-- A kind variable; *only* happens during kind checking
+
+boxity :: BX = *	-- Boxed
+	     | #	-- Unboxed
+	     | bv	-- A boxity variable; *only* happens during kind checking
+
+There's a little subtyping at the kind level:  
+	forall b. Type b <: OpenKind
 
-kv :: KX is a kind variable
+That is, a type of kind (Type b) OK in a context requiring an AnyBox.
 
-Type :: BX -> KX
+OpenKind, written '?', is used as the kind for certain type variables,
+in two situations:
 
-bx::BX = Boxed 
-      |  Unboxed
-      |  AnyBox		-- Used *only* for special built-in things
-			-- like error :: forall (a::*?). String -> a
-			-- Here, the 'a' can be instantiated to a boxed or
-			-- unboxed type.
-      |  bv
+1.  The universally quantified type variable(s) for special built-in 
+    things like error :: forall (a::?). String -> a. 
+    Here, the 'a' can be instantiated to a boxed or unboxed type.  
 
-bxv :: BX is a boxity variable
+2.  Kind '?' is also used when the typechecker needs to create a fresh
+    type variable, one that may very well later be unified with a type.
+    For example, suppose f::a, and we see an application (f x).  Then a
+    must be a function type, so we unify a with (b->c).  But what kind
+    are b and c?  They can be boxed or unboxed types, so we give them kind '?'.
+
+    When the type checker generalises over a bunch of type variables, it
+    makes any that still have kind '?' into kind '*'.  So kind '?' is never
+    present in an inferred type.
 
-sk = KX		-- A kind
-   | BX		-- A boxity
-   | sk -> sk	-- In ptic (BX -> KX)
 
 \begin{code}
 mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str)
@@ -181,7 +191,9 @@ mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str)
 	-- It's used for both Kinds and Boxities
 \end{code}
 
-Define KX, BX.
+------------------------------------------
+Define  KX, the type of a kind
+	BX, the type of a boxity
 
 \begin{code}
 superKind :: SuperKind 		-- KX, the type of all kinds
@@ -193,38 +205,41 @@ superBoxityName = mk_kind_name boxityConKey SLIT("BX")
 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 \end{code}
 
-Define Boxed, Unboxed, AnyBox
+------------------------------------------
+Define boxities: @*@ and @#@
 
 \begin{code}
-boxedKind, unboxedKind, anyBoxKind :: Kind	-- Of superkind superBoxity
+boxedBoxity, unboxedBoxity :: Kind		-- :: BX
 
 boxedConName = mk_kind_name boxedConKey SLIT("*")
-boxedKind    = TyConApp (mkKindCon boxedConName superBoxity) []
+boxedBoxity  = TyConApp (mkKindCon boxedConName superBoxity) []
 
 unboxedConName = mk_kind_name unboxedConKey SLIT("#")
-unboxedKind    = TyConApp (mkKindCon unboxedConName superBoxity) []
-
-anyBoxConName = mk_kind_name anyBoxConKey SLIT("?")
-anyBoxCon     = mkKindCon anyBoxConName superBoxity	-- A kind of wild card
-anyBoxKind    = TyConApp anyBoxCon []
+unboxedBoxity  = TyConApp (mkKindCon unboxedConName superBoxity) []
 \end{code}
 
-Define Type
+------------------------------------------
+Define kinds: Type, Type *, Type #, and OpenKind
 
 \begin{code}
-typeCon :: KindCon
+typeCon :: KindCon	-- :: BX -> KX
 typeConName = mk_kind_name typeConKey SLIT("Type")
 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
+
+boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind	-- Of superkind superKind
+
+boxedTypeKind   = TyConApp typeCon [boxedBoxity]
+unboxedTypeKind = TyConApp typeCon [unboxedBoxity]
+
+openKindConName = mk_kind_name anyBoxConKey SLIT("?")
+openKindCon     = mkKindCon openKindConName superKind
+openTypeKind    = TyConApp openKindCon []
 \end{code}
 
-Define (Type Boxed), (Type Unboxed), (Type AnyBox)
+------------------------------------------
+Define arrow kinds
 
 \begin{code}
-boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind
-boxedTypeKind   = TyConApp typeCon [boxedKind]
-unboxedTypeKind = TyConApp typeCon [unboxedKind]
-openTypeKind	= TyConApp typeCon [anyBoxKind]
-
 mkArrowKind :: Kind -> Kind -> Kind
 mkArrowKind k1 k2 = k1 `FunTy` k2
 
diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs
index 756a5ed31439938b4db709d04ab8662049b5b8d9..bbeb51aafa4808dc0883745d579bae1c316e253e 100644
--- a/ghc/compiler/types/Unify.lhs
+++ b/ghc/compiler/types/Unify.lhs
@@ -11,9 +11,9 @@ module Unify ( unifyTysX, unifyTyListsX,
 	       match, matchTy, matchTys
   ) where 
 
-import TypeRep	( Type(..), funTyCon
-		)  -- friend
-import Type	( typeKind, tyVarsOfType, splitAppTy_maybe
+import TypeRep	( Type(..) )	 -- friend
+import Type	( Kind, funTyCon, 
+		  typeKind, tyVarsOfType, splitAppTy_maybe
 		)
 
 import PprType	()	-- Instances
@@ -28,7 +28,6 @@ import VarEnv	( TyVarSubstEnv, emptySubstEnv, lookupSubstEnv, extendSubstEnv,
 		)
 
 import Outputable( panic )
-import Util	( snocView )
 \end{code}
 
 %************************************************************************
@@ -232,3 +231,4 @@ match_list (ty1:tys1) []         tmpls k senv = Nothing	-- Not enough arg tys =>
 match_list (ty1:tys1) (ty2:tys2) tmpls k senv = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv
 \end{code}
 
+
diff --git a/ghc/compiler/types/Variance.lhs b/ghc/compiler/types/Variance.lhs
index b3fe0a5f1a75b8a0a5c6c50d1149dcf82a114694..57119ff98816466ae97a73254dd72cdc6e820a59 100644
--- a/ghc/compiler/types/Variance.lhs
+++ b/ghc/compiler/types/Variance.lhs
@@ -40,21 +40,19 @@ tycons as a whole.  It returns a list of @tyconVrcInfo@ data, ready to
 be (knot-tyingly?) stuck back into the appropriate fields.
 
 \begin{code}
-calcTyConArgVrcs :: [TyCon]
-		 -> FiniteMap Name ArgVrcs
+calcTyConArgVrcs :: [TyCon] -> FiniteMap TyCon ArgVrcs
 
 calcTyConArgVrcs tycons
-  = let oi           = foldl (\fm tc -> addToFM fm tc (initial tc)) emptyFM tycons
-        initial tc   = if isAlgTyCon tc && null (tyConDataConsIfAvailable tc) then
+  = tcaoFix initial_oi
+  where
+
+    initial_oi :: FiniteMap TyCon ArgVrcs
+    initial_oi   = foldl (\fm tc -> addToFM fm tc (initial tc)) emptyFM tycons
+    initial tc   = if isAlgTyCon tc && null (tyConDataConsIfAvailable tc) then
                          -- make pessimistic assumption (and warn)
                          take (tyConArity tc) abstractVrcs
                        else
                          replicate (tyConArity tc) (False,False)
-        oi''         = tcaoFix oi
-        go (tc,vrcs) = (getName tc,vrcs)
-    in  listToFM (map go (fmToList oi''))
-        
-  where
 
     tcaoFix :: FiniteMap TyCon ArgVrcs   -- initial ArgVrcs per tycon
 	    -> FiniteMap TyCon ArgVrcs   -- fixpointed ArgVrcs per tycon