From 77a8c0dbd5c5ad90fe483cb9ddc2b6ef36d3f4d8 Mon Sep 17 00:00:00 2001
From: simonpj <unknown>
Date: Fri, 14 Jul 2000 08:17:41 +0000
Subject: [PATCH] [project @ 2000-07-14 08:17:36 by simonpj] This commit
 completely re-does the kind-inference mechanism. Previously it was
 inter-wound with type inference, but that was always hard to understand, and
 it finally broke when we started checking for ambiguity when type-checking a
 type signature (details irrelevant).

So now kind inference is more clearly separated, so that it never
takes place at the same time as type inference.  The biggest change
is in TcTyClsDecls, which does the kind inference for a group of
type and class declarations.  It now contains comments to explain
how it all works.

There are also comments in TypeRep which describes the slightly
tricky way in which we deal with the fact that kind 'type' (written
'*') actually has 'boxed type' and 'unboxed type' as sub-kinds.
The whole thing is a bit of a hack, because we don't really have
sub-kinding, but it's less of a hack than before.

A lot of general tidying up happened at the same time.
In particular, I removed some dead code here and there
---
 ghc/compiler/Makefile                   |   4 +-
 ghc/compiler/basicTypes/MkId.lhs        |  13 +-
 ghc/compiler/basicTypes/Name.lhs        |  32 +-
 ghc/compiler/basicTypes/VarEnv.lhs      |   4 +-
 ghc/compiler/deSugar/DsCCall.lhs        |  22 +-
 ghc/compiler/hsSyn/HsDecls.lhs          |  19 +-
 ghc/compiler/hsSyn/HsPat.lhs            |  24 +-
 ghc/compiler/hsSyn/HsSyn.lhs            |   3 -
 ghc/compiler/hsSyn/HsTypes.lhs          |   8 +-
 ghc/compiler/nativeGen/MachCode.lhs     |   8 +-
 ghc/compiler/nativeGen/StixMacro.lhs    |   1 -
 ghc/compiler/parser/Lex.lhs             |   1 -
 ghc/compiler/parser/RdrHsSyn.lhs        |  27 +-
 ghc/compiler/rename/Rename.lhs          |  17 +-
 ghc/compiler/rename/RnEnv.lhs           |  11 +-
 ghc/compiler/rename/RnHsSyn.lhs         |   3 +-
 ghc/compiler/rename/RnIfaces.lhs        |   9 +-
 ghc/compiler/rename/RnMonad.lhs         |   6 +-
 ghc/compiler/rename/RnNames.lhs         |   3 +-
 ghc/compiler/rename/RnSource.lhs        |   4 +-
 ghc/compiler/simplCore/LiberateCase.lhs |   4 +-
 ghc/compiler/simplCore/OccurAnal.lhs    |  10 +-
 ghc/compiler/simplCore/SetLevels.lhs    |   1 -
 ghc/compiler/simplCore/SimplCore.lhs    |   6 +-
 ghc/compiler/simplCore/SimplMonad.lhs   |   1 -
 ghc/compiler/simplCore/SimplUtils.lhs   |   9 +-
 ghc/compiler/specialise/Specialise.lhs  |  16 +-
 ghc/compiler/typecheck/TcBinds.lhs      |  14 +-
 ghc/compiler/typecheck/TcClassDcl.lhs   | 165 +++------
 ghc/compiler/typecheck/TcEnv.lhs        | 115 +++---
 ghc/compiler/typecheck/TcExpr.lhs       |  10 +-
 ghc/compiler/typecheck/TcForeign.lhs    |  17 +-
 ghc/compiler/typecheck/TcGenDeriv.lhs   |   2 -
 ghc/compiler/typecheck/TcHsSyn.lhs      |  10 +-
 ghc/compiler/typecheck/TcIfaceSig.lhs   |   7 +-
 ghc/compiler/typecheck/TcInstDcls.lhs   |  10 +-
 ghc/compiler/typecheck/TcMatches.lhs    |  25 +-
 ghc/compiler/typecheck/TcModule.lhs     |  17 +-
 ghc/compiler/typecheck/TcMonad.lhs      |   5 +-
 ghc/compiler/typecheck/TcMonoType.lhs   | 463 ++++++++++++++----------
 ghc/compiler/typecheck/TcPat.lhs        |   2 +-
 ghc/compiler/typecheck/TcRules.lhs      |   8 +-
 ghc/compiler/typecheck/TcSimplify.lhs   |   7 +-
 ghc/compiler/typecheck/TcTyClsDecls.lhs | 379 +++++++++++++------
 ghc/compiler/typecheck/TcTyDecls.lhs    | 238 +++++-------
 ghc/compiler/typecheck/TcType.lhs       | 209 +++--------
 ghc/compiler/typecheck/TcUnify.lhs      | 170 +++++----
 ghc/compiler/types/Class.lhs            |   9 +-
 ghc/compiler/types/FunDeps.lhs          |  19 +-
 ghc/compiler/types/Type.lhs             |  47 +--
 ghc/compiler/types/TypeRep.lhs          | 101 +++---
 ghc/compiler/types/Unify.lhs            |   8 +-
 ghc/compiler/types/Variance.lhs         |  16 +-
 53 files changed, 1180 insertions(+), 1159 deletions(-)

diff --git a/ghc/compiler/Makefile b/ghc/compiler/Makefile
index 47b0d31a3ef1..724cbbcddbb8 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 69ba8af2884a..3504caac3f07 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 ff8096a92988..7ee54d5a0bfa 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 0cd670e3b55d..f8783f4e1bf9 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 4384e66f74b9..b10a0fa1772d 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 033f426acb36..092ee68b0e34 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 6e4051ec8328..09494a1ad1c0 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 42731ccc13dc..bf722a508cff 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 62255d767f09..86a14675f770 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 f54c759ee6e9..a45f7dbc5f5c 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 19c02d2e5253..415d7c8c5de9 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 9a2ab9c9c07f..dd020e750a5b 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 0884f54e0764..a4cbc8047b63 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 e6229017d364..f2f86144876e 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 14a833959abb..823a1222c2b2 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 60dfedb452e5..05412f5f8d33 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 3f775a47961e..dbb90e517666 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 1159bfe6511b..457f2c1d788f 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 f07651e24f60..7bcd56506ac7 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 b2c4aa26f888..1b19d4b69ff7 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 bd9bac25e72f..baa8bdaa26bf 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 4681aa3edae2..4d856f770497 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 91dbe75aee45..4aa1c5b227f1 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 fda56fe4eae7..0321bf7dadd4 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 a5d5a9806ae8..697fb715365e 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 d346292c332c..544a791144c6 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 d73e2c3f412c..884d70be5cbb 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 7d8b4c3b0312..775a36d41e4c 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 eae1c69d277a..7b6765cf6222 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 c99244d20496..ab3021767fb2 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 d171a36d80c1..649722118fda 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 7e4140799b17..69991070609a 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 b19f84e434b0..fb87c891222b 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 1252cfd913de..102071b91b95 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 27b4f1845fca..4bce6a4b0055 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 e55ea763f1fb..fd2b5dd881f5 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 4d73dbe36bc0..edebb87d88ef 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 d10c84b307d1..f4a3934faebe 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 8e4b1906250f..0f86e0743695 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 f734b7823682..ee3b281ac787 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 e974cfaa2d9c..e0cb157bac26 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 616d717b7f09..ec9176134b19 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 861f908f5d62..f51ae48aacee 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 030e7102133b..a194ed34ebe4 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 464d1b624024..5efdb208f0bc 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 81b4ee8ecd4b..509bea6f6cc1 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 ba131c09d5a3..7c92681dd571 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 a04cdcc3ac7f..b3e47e415383 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 108fb1c6435a..dc7c3914314b 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 e3c4b78e5c37..109c8e4e5448 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 b71576bf0603..26e507839403 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 756a5ed31439..bbeb51aafa48 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 b3fe0a5f1a75..57119ff98816 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
-- 
GitLab