Use MD5 checksums for recompilation checking (fixes #1372, #1959)
[ghc-hetmet.git] / compiler / types / Type.lhs
index 7c05b6d..6eaac8c 100644 (file)
@@ -1,10 +1,18 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1998
 %
-\section[Type]{Type - public interface}
 
+Type - public interface
 
 \begin{code}
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
 module Type (
         -- re-exports from TypeRep
        TyThing(..), Type, PredType(..), ThetaType, 
@@ -53,18 +61,21 @@ module Type (
        applyTy, applyTys, isForAllTy, dropForAlls,
 
        -- Source types
-       predTypeRep, mkPredTy, mkPredTys,
+       predTypeRep, mkPredTy, mkPredTys, pprSourceTyCon, mkFamilyTyConApp,
 
        -- Newtypes
-       splitRecNewType_maybe, newTyConInstRhs,
+       newTyConInstRhs,
 
        -- Lifting and boxity
-       isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
-       isStrictType, isStrictPred, 
+       isUnLiftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
+       isPrimitiveType, isStrictType, isStrictPred, 
 
        -- Free variables
        tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-       typeKind, addFreeTyVars,
+       typeKind,
+
+        -- Type families
+        tyFamInsts,
 
        -- Tidying up for printing
        tidyType,      tidyTypes,
@@ -76,7 +87,7 @@ module Type (
 
        -- Comparison
        coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
-       tcEqPred, tcCmpPred, tcEqTypeX, 
+       tcEqPred, tcEqPredX, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred,
 
        -- Seq
        seqType, seqTypes,
@@ -87,13 +98,14 @@ module Type (
        mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
        getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
        extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
+        isEmptyTvSubst,
 
        -- Performing substitution on types
        substTy, substTys, substTyWith, substTheta, 
-       substPred, substTyVar, substTyVarBndr, deShadowTy, lookupTyVar,
+       substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
 
        -- Pretty-printing
-       pprType, pprParendType, pprTyThingCategory,
+       pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
        pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
     ) where
 
@@ -105,32 +117,23 @@ module Type (
 import TypeRep
 
 -- friends:
-import Var     ( Var, TyVar, tyVarKind, tyVarName, 
-                 setTyVarName, setTyVarKind, mkWildCoVar )
+import Var
 import VarEnv
 import VarSet
 
-import OccName ( tidyOccName )
-import Name    ( NamedThing(..), tidyNameOcc )
-import Class   ( Class, classTyCon )
-import PrelNames( openTypeKindTyConKey, unliftedTypeKindTyConKey, 
-                  ubxTupleKindTyConKey, argTypeKindTyConKey )
-import TyCon   ( TyCon, isRecursiveTyCon, isPrimTyCon,
-                 isUnboxedTupleTyCon, isUnLiftedTyCon,
-                 isFunTyCon, isNewTyCon, isClosedNewTyCon, 
-                 newTyConRep, newTyConRhs, 
-                 isAlgTyCon, tyConArity, isSuperKindTyCon,
-                 tcExpandTyCon_maybe, coreExpandTyCon_maybe,
-                 tyConKind, PrimRep(..), tyConPrimRep, tyConUnique,
-                  isCoercionTyCon
-               )
+import Name
+import Class
+import PrelNames
+import TyCon
 
 -- others
-import StaticFlags     ( opt_DictsStrict )
-import Util            ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
+import StaticFlags
+import Util
 import Outputable
-import UniqSet         ( sizeUniqSet )         -- Should come via VarSet
-import Maybe           ( isJust )
+import FastString
+
+import Data.List
+import Data.Maybe      ( isJust )
 \end{code}
 
 
@@ -164,7 +167,6 @@ coreView :: Type -> Maybe Type
 
 -- By being non-recursive and inlined, this case analysis gets efficiently
 -- joined onto the case analysis that the caller is already doing
-coreView (NoteTy _ ty)            = Just ty
 coreView (PredTy p)
   | isEqPred p             = Nothing
   | otherwise             = Just (predTypeRep p)
@@ -173,7 +175,7 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc
                                -- Its important to use mkAppTys, rather than (foldl AppTy),
                                -- because the function part might well return a 
                                -- partially-applied type constructor; indeed, usually will!
-coreView ty               = Nothing
+coreView _                 = Nothing
 
 
 
@@ -181,18 +183,16 @@ coreView ty                  = Nothing
 {-# INLINE tcView #-}
 tcView :: Type -> Maybe Type
 -- Same, but for the type checker, which just looks through synonyms
-tcView (NoteTy _ ty)    = Just ty
 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys 
                         = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
-tcView ty               = Nothing
+tcView _                 = Nothing
 
 -----------------------------------------------
 {-# INLINE kindView #-}
 kindView :: Kind -> Maybe Kind
 -- C.f. coreView, tcView
 -- For the moment, we don't even handle synonyms in kinds
-kindView (NoteTy _ k) = Just k
-kindView other       = Nothing
+kindView _            = Nothing
 \end{code}
 
 
@@ -224,7 +224,7 @@ isTyVarTy ty = isJust (getTyVar_maybe ty)
 getTyVar_maybe :: Type -> Maybe TyVar
 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
 getTyVar_maybe (TyVarTy tv)                = Just tv  
-getTyVar_maybe other                       = Nothing
+getTyVar_maybe _                            = Nothing
 
 \end{code}
 
@@ -237,12 +237,12 @@ invariant that a TyConApp is always visibly so.  mkAppTy maintains the
 invariant: use it.
 
 \begin{code}
+mkAppTy :: Type -> Type -> Type
 mkAppTy orig_ty1 orig_ty2
   = mk_app orig_ty1
   where
-    mk_app (NoteTy _ ty1)    = mk_app ty1
     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
-    mk_app ty1              = AppTy orig_ty1 orig_ty2
+    mk_app _                 = AppTy orig_ty1 orig_ty2
        -- Note that the TyConApp could be an 
        -- under-saturated type synonym.  GHC allows that; e.g.
        --      type Foo k = k a -> k a
@@ -262,10 +262,9 @@ mkAppTys orig_ty1 []           = orig_ty1
 mkAppTys orig_ty1 orig_tys2
   = mk_app orig_ty1
   where
-    mk_app (NoteTy _ ty1)    = mk_app ty1
     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
                                -- mkTyConApp: see notes with mkAppTy
-    mk_app ty1              = foldl AppTy orig_ty1 orig_tys2
+    mk_app _                 = foldl AppTy orig_ty1 orig_tys2
 
 -------------
 splitAppTy_maybe :: Type -> Maybe (Type, Type)
@@ -278,10 +277,12 @@ repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 -- Does the AppTy split, but assumes that any view stuff is already done
 repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
-repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
-                                               Just (tys', ty') -> Just (TyConApp tc tys', ty')
-                                               Nothing          -> Nothing
-repSplitAppTy_maybe other = Nothing
+repSplitAppTy_maybe (TyConApp tc tys) 
+  | not (isOpenSynTyCon tc) || length tys > tyConArity tc 
+  = case snocView tys of       -- never create unsaturated type family apps
+      Just (tys', ty') -> Just (TyConApp tc tys', ty')
+      Nothing         -> Nothing
+repSplitAppTy_maybe _other = Nothing
 -------------
 splitAppTy :: Type -> (Type, Type)
 splitAppTy ty = case splitAppTy_maybe ty of
@@ -293,11 +294,17 @@ splitAppTys :: Type -> (Type, [Type])
 splitAppTys ty = split ty ty []
   where
     split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
-    split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
-    split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
-    split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
+    split _       (AppTy ty arg)        args = split ty ty (arg:args)
+    split _       (TyConApp tc tc_args) args
+      = let -- keep type families saturated
+            n | isOpenSynTyCon tc = tyConArity tc
+              | otherwise         = 0
+            (tc_args1, tc_args2)  = splitAt n tc_args
+        in
+        (TyConApp tc tc_args1, tc_args2 ++ args)
+    split _       (FunTy ty1 ty2)       args = ASSERT( null args )
                                               (TyConApp funTyCon [], [ty1,ty2])
-    split orig_ty ty                   args = (orig_ty, args)
+    split orig_ty _                     args = (orig_ty, args)
 
 \end{code}
 
@@ -325,14 +332,14 @@ splitFunTy other       = pprPanic "splitFunTy" (ppr other)
 splitFunTy_maybe :: Type -> Maybe (Type, Type)
 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
 splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
-splitFunTy_maybe other            = Nothing
+splitFunTy_maybe _                 = Nothing
 
 splitFunTys :: Type -> ([Type], Type)
 splitFunTys ty = split [] ty ty
   where
     split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
-    split args orig_ty (FunTy arg res)          = split (arg:args) res res
-    split args orig_ty ty                = (reverse args, orig_ty)
+    split args _       (FunTy arg res)   = split (arg:args) res res
+    split args orig_ty _                 = (reverse args, orig_ty)
 
 splitFunTysN :: Int -> Type -> ([Type], Type)
 -- Split off exactly n arg tys
@@ -344,21 +351,21 @@ splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
   where
-    split acc []     nty ty               = (reverse acc, nty)
+    split acc []     nty _                 = (reverse acc, nty)
     split acc xs     nty ty 
          | Just ty' <- coreView ty        = split acc xs nty ty'
-    split acc (x:xs) nty (FunTy arg res)   = split ((x,arg):acc) xs res res
-    split acc (x:xs) nty ty                = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
+    split acc (x:xs) _   (FunTy arg res)   = split ((x,arg):acc) xs res res
+    split _   _      _   _                 = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
     
 funResultTy :: Type -> Type
 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
-funResultTy (FunTy arg res)   = res
-funResultTy ty               = pprPanic "funResultTy" (ppr ty)
+funResultTy (FunTy _arg res)  = res
+funResultTy ty                = pprPanic "funResultTy" (ppr ty)
 
 funArgTy :: Type -> Type
 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
-funArgTy (FunTy arg res)   = arg
-funArgTy ty               = pprPanic "funArgTy" (ppr ty)
+funArgTy (FunTy arg _res)  = arg
+funArgTy ty                = pprPanic "funArgTy" (ppr ty)
 \end{code}
 
 
@@ -399,7 +406,7 @@ splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
-splitTyConApp_maybe other            = Nothing
+splitTyConApp_maybe _                 = Nothing
 
 -- Sometimes we do NOT want to look throught a newtype.  When case matching
 -- on a newtype we want a convenient way to access the arguments of a newty
@@ -412,14 +419,17 @@ splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty'
 splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 splitNewTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
-splitNewTyConApp_maybe other         = Nothing
+splitNewTyConApp_maybe _                 = Nothing
 
--- get instantiated newtype rhs, the arguments had better saturate 
--- the constructor
 newTyConInstRhs :: TyCon -> [Type] -> Type
-newTyConInstRhs tycon tys =
-    let (tvs, ty) = newTyConRhs tycon in substTyWith tvs tys ty
-
+-- Unwrap one 'layer' of newtype
+-- Use the eta'd version if possible
+newTyConInstRhs tycon tys 
+    = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
+      mkAppTys (substTyWith tvs tys1 ty) tys2
+  where
+    (tvs, ty)    = newTyConEtadRhs tycon
+    (tys1, tys2) = splitAtList tvs tys
 \end{code}
 
 
@@ -442,6 +452,31 @@ The reason is that we then get better (shorter) type signatures in
 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
 
 
+Note [Expanding newtypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+When expanding a type to expose a data-type constructor, we need to be
+careful about newtypes, lest we fall into an infinite loop. Here are
+the key examples:
+
+  newtype Id  x = MkId x
+  newtype Fix f = MkFix (f (Fix f))
+  newtype T     = MkT (T -> T) 
+  
+  Type          Expansion
+ --------------------------
+  T             T -> T
+  Fix Maybe      Maybe (Fix Maybe)
+  Id (Id Int)    Int
+  Fix Id         NO NO NO
+
+Notice that we can expand T, even though it's recursive.
+And we can expand Id (Id Int), even though the Id shows up
+twice at the outer level.  
+
+So, when expanding, we keep track of when we've seen a recursive
+newtype at outermost level; and bale out if we see it again.
+
+
                Representation types
                ~~~~~~~~~~~~~~~~~~~~
 repType looks through 
@@ -455,22 +490,28 @@ It's useful in the back end.
 \begin{code}
 repType :: Type -> Type
 -- Only applied to types of kind *; hence tycons are saturated
-repType ty | Just ty' <- coreView ty = repType ty'
-repType (ForAllTy _ ty)  = repType ty
-repType (TyConApp tc tys)
-  | isClosedNewTyCon tc  = -- Recursive newtypes are opaque to coreView
-                          -- but we must expand them here.  Sure to
-                          -- be saturated because repType is only applied
-                          -- to types of kind *
-                          ASSERT( {- isRecursiveTyCon tc && -} tys `lengthIs` tyConArity tc )
-                          repType (new_type_rep tc tys)
-repType ty = ty
-
--- new_type_rep doesn't ask any questions: 
--- it just expands newtype, whether recursive or not
-new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon )
-                            case newTyConRep new_tycon of
-                                (tvs, rep_ty) -> substTyWith tvs tys rep_ty
+repType ty
+  = go [] ty
+  where
+    go :: [TyCon] -> Type -> Type
+    go rec_nts ty | Just ty' <- coreView ty    -- Expand synonyms
+       = go rec_nts ty'        
+
+    go rec_nts (ForAllTy _ ty)                 -- Look through foralls
+       = go rec_nts ty
+
+    go rec_nts ty@(TyConApp tc tys)            -- Expand newtypes
+       | Just _co_con <- newTyConCo_maybe tc   -- See Note [Expanding newtypes]
+       = if tc `elem` rec_nts                  --  in Type.lhs
+         then ty
+         else go rec_nts' nt_rhs
+       where
+         nt_rhs = newTyConInstRhs tc tys
+         rec_nts' | isRecursiveTyCon tc = tc:rec_nts
+                  | otherwise           = rec_nts
+
+    go _ ty = ty
+
 
 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
 -- of inspecting the type directly.
@@ -480,13 +521,12 @@ typePrimRep ty = case repType ty of
                   FunTy _ _     -> PtrRep
                   AppTy _ _     -> PtrRep      -- See note below
                   TyVarTy _     -> PtrRep
-                  other         -> pprPanic "typePrimRep" (ppr ty)
+                  _             -> pprPanic "typePrimRep" (ppr ty)
        -- Types of the form 'f a' must be of kind *, not *#, so
        -- we are guaranteed that they are represented by pointers.
        -- The reason is that f must have kind *->*, not *->*#, because
        -- (we claim) there is no way to constrain f's kind any other
        -- way.
-
 \end{code}
 
 
@@ -503,9 +543,8 @@ mkForAllTys :: [TyVar] -> Type -> Type
 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 
 isForAllTy :: Type -> Bool
-isForAllTy (NoteTy _ ty)  = isForAllTy ty
 isForAllTy (ForAllTy _ _) = True
-isForAllTy other_ty      = False
+isForAllTy _              = False
 
 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
 splitForAllTy_maybe ty = splitFAT_m ty
@@ -518,8 +557,8 @@ splitForAllTys :: Type -> ([TyVar], Type)
 splitForAllTys ty = split ty ty []
    where
      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
-     split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
-     split orig_ty t                tvs = (reverse tvs, orig_ty)
+     split _       (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
+     split orig_ty _                 tvs = (reverse tvs, orig_ty)
 
 dropForAlls :: Type -> Type
 dropForAlls ty = snd (splitForAllTys ty)
@@ -539,7 +578,7 @@ the expression.
 applyTy :: Type -> Type -> Type
 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
-applyTy other           arg = panic "applyTy"
+applyTy _                _   = panic "applyTy"
 
 applyTys :: Type -> [Type] -> Type
 -- This function is interesting because 
@@ -601,34 +640,31 @@ predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
        -- Result might be a newtype application, but the consumer will
        -- look through that too if necessary
 predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
-\end{code}
-
-
-%************************************************************************
-%*                                                                     *
-               NewTypes
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
-splitRecNewType_maybe :: Type -> Maybe Type
--- Sometimes we want to look through a recursive newtype, and that's what happens here
--- It only strips *one layer* off, so the caller will usually call itself recursively
--- Only applied to types of kind *, hence the newtype is always saturated
-splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
-splitRecNewType_maybe (TyConApp tc tys)
-  | isClosedNewTyCon tc
-  = ASSERT( tys `lengthIs` tyConArity tc )     -- splitRecNewType_maybe only be applied 
-                                               --      to *types* (of kind *)
-    ASSERT( isRecursiveTyCon tc )              -- Guaranteed by coreView
-    case newTyConRhs tc of
-       (tvs, rep_ty) -> ASSERT( length tvs == length tys )
-                        Just (substTyWith tvs tys rep_ty)
-       
-splitRecNewType_maybe other = Nothing
-
-
 
+mkFamilyTyConApp :: TyCon -> [Type] -> Type
+-- Given a family instance TyCon and its arg types, return the
+-- corresponding family type.  E.g.
+--     data family T a
+--     data instance T (Maybe b) = MkT b       -- Instance tycon :RTL
+-- Then 
+--     mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
+mkFamilyTyConApp tc tys
+  | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
+  , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
+  = mkTyConApp fam_tc (substTys fam_subst fam_tys)
+  | otherwise
+  = mkTyConApp tc tys
+
+-- Pretty prints a tycon, using the family instance in case of a
+-- representation tycon.  For example
+--     e.g.  data T [a] = ...
+-- In that case we want to print `T [a]', where T is the family TyCon
+pprSourceTyCon :: TyCon -> SDoc
+pprSourceTyCon tycon 
+  | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
+  = ppr $ fam_tc `TyConApp` tys               -- can't be FunTyCon
+  | otherwise
+  = ppr tycon
 \end{code}
 
 
@@ -647,12 +683,11 @@ typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
                                   -- We should be looking for the coercion kind,
                                   -- not the type kind
                                foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
-typeKind (NoteTy _ ty)       = typeKind ty
 typeKind (PredTy pred)       = predKind pred
-typeKind (AppTy fun arg)      = kindFunResult (typeKind fun)
-typeKind (ForAllTy tv ty)     = typeKind ty
+typeKind (AppTy fun _)        = kindFunResult (typeKind fun)
+typeKind (ForAllTy _ ty)      = typeKind ty
 typeKind (TyVarTy tyvar)      = tyVarKind tyvar
-typeKind (FunTy arg res)
+typeKind (FunTy _arg res)
     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*), 
     --              not unliftedTypKind (#)
     -- The only things that can be after a function arrow are
@@ -677,8 +712,7 @@ predKind (IParam {}) = liftedTypeKind       -- always represented by lifted types
 tyVarsOfType :: Type -> TyVarSet
 -- NB: for type synonyms tyVarsOfType does *not* expand the synonym
 tyVarsOfType (TyVarTy tv)              = unitVarSet tv
-tyVarsOfType (TyConApp tycon tys)      = tyVarsOfTypes tys
-tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
+tyVarsOfType (TyConApp _ tys)           = tyVarsOfTypes tys
 tyVarsOfType (PredTy sty)              = tyVarsOfPred sty
 tyVarsOfType (FunTy arg res)           = tyVarsOfType arg `unionVarSet` tyVarsOfType res
 tyVarsOfType (AppTy fun arg)           = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
@@ -694,11 +728,28 @@ tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
 
 tyVarsOfTheta :: ThetaType -> TyVarSet
 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Type families}
+%*                                                                     *
+%************************************************************************
+
+Type family instances occuring in a type after expanding synonyms.
 
--- Add a Note with the free tyvars to the top of the type
-addFreeTyVars :: Type -> Type
-addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
-addFreeTyVars ty                            = NoteTy (FTVNote (tyVarsOfType ty)) ty
+\begin{code}
+tyFamInsts :: Type -> [(TyCon, [Type])]
+tyFamInsts ty 
+  | Just exp_ty <- tcView ty    = tyFamInsts exp_ty
+tyFamInsts (TyVarTy _)          = []
+tyFamInsts (TyConApp tc tys) 
+  | isOpenSynTyCon tc           = [(tc, tys)]
+  | otherwise                   = concat (map tyFamInsts tys)
+tyFamInsts (FunTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
+tyFamInsts (AppTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
+tyFamInsts (ForAllTy _ ty)      = tyFamInsts ty
 \end{code}
 
 
@@ -715,13 +766,17 @@ It doesn't change the uniques at all, just the print names.
 
 \begin{code}
 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
-tidyTyVarBndr (tidy_env, subst) tyvar
+tidyTyVarBndr env@(tidy_env, subst) tyvar
   = case tidyOccName tidy_env (getOccName name) of
-      (tidy', occ') ->         ((tidy', subst'), tyvar')
-                   where
-                       subst' = extendVarEnv subst tyvar tyvar'
-                       tyvar' = setTyVarName tyvar name'
-                       name'  = tidyNameOcc name occ'
+      (tidy', occ') -> ((tidy', subst'), tyvar'')
+       where
+         subst' = extendVarEnv subst tyvar tyvar''
+         tyvar' = setTyVarName tyvar name'
+         name'  = tidyNameOcc name occ'
+               -- Don't forget to tidy the kind for coercions!
+         tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
+                 | otherwise     = tyvar'
+         kind'  = tidyType env (tyVarKind tyvar)
   where
     name = tyVarName tyvar
 
@@ -735,13 +790,13 @@ tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
 
 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 -- Treat a new tyvar as a binder, and give it a fresh tidy name
-tidyOpenTyVar env@(tidy_env, subst) tyvar
+tidyOpenTyVar env@(_, subst) tyvar
   = case lookupVarEnv subst tyvar of
        Just tyvar' -> (env, tyvar')            -- Already substituted
        Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
 
 tidyType :: TidyEnv -> Type -> Type
-tidyType env@(tidy_env, subst) ty
+tidyType env@(_, subst) ty
   = go ty
   where
     go (TyVarTy tv)        = case lookupVarEnv subst tv of
@@ -749,7 +804,6 @@ tidyType env@(tidy_env, subst) ty
                                Just tv' -> TyVarTy tv'
     go (TyConApp tycon tys) = let args = map go tys
                              in args `seqList` TyConApp tycon args
-    go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
     go (PredTy sty)        = PredTy (tidyPred env sty)
     go (AppTy fun arg)     = (AppTy $! (go fun)) $! (go arg)
     go (FunTy fun arg)     = (FunTy $! (go fun)) $! (go arg)
@@ -757,8 +811,7 @@ tidyType env@(tidy_env, subst) ty
                              where
                                (envp, tvp) = tidyTyVarBndr env tv
 
-    go_note note@(FTVNote ftvs) = note -- No need to tidy the free tyvars
-
+tidyTypes :: TidyEnv -> [Type] -> [Type]
 tidyTypes env tys = map (tidyType env) tys
 
 tidyPred :: TidyEnv -> PredType -> PredType
@@ -808,21 +861,30 @@ isUnLiftedType :: Type -> Bool
        -- construct them
 
 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
-isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
+isUnLiftedType (ForAllTy _ ty)   = isUnLiftedType ty
 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
-isUnLiftedType other            = False        
+isUnLiftedType _                 = False
 
 isUnboxedTupleType :: Type -> Bool
 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
-                          Just (tc, ty_args) -> isUnboxedTupleTyCon tc
-                          other              -> False
+                           Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
+                           _                   -> False
 
 -- Should only be applied to *types*; hence the assert
 isAlgType :: Type -> Bool
-isAlgType ty = case splitTyConApp_maybe ty of
-                       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
-                                             isAlgTyCon tc
-                       other              -> False
+isAlgType ty 
+  = case splitTyConApp_maybe ty of
+      Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
+                           isAlgTyCon tc
+      _other            -> False
+
+-- Should only be applied to *types*; hence the assert
+isClosedAlgType :: Type -> Bool
+isClosedAlgType ty
+  = case splitTyConApp_maybe ty of
+      Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
+                           isAlgTyCon tc && not (isOpenTyCon tc)
+      _other            -> False
 \end{code}
 
 @isStrictType@ computes whether an argument (or let RHS) should
@@ -833,14 +895,16 @@ this function should be in TcType, but isStrictType is used by DataCon,
 which is below TcType in the hierarchy, so it's convenient to put it here.
 
 \begin{code}
+isStrictType :: Type -> Bool
 isStrictType (PredTy pred)     = isStrictPred pred
 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
-isStrictType (ForAllTy tv ty)  = isStrictType ty
+isStrictType (ForAllTy _ ty)   = isStrictType ty
 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
-isStrictType other            = False  
+isStrictType _                 = False
 
+isStrictPred :: PredType -> Bool
 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
-isStrictPred other          = False
+isStrictPred _               = False
        -- We may be strict in dictionary types, but only if it 
        -- has more than one component.
        -- [Being strict in a single-component dictionary risks
@@ -855,7 +919,7 @@ isPrimitiveType :: Type -> Bool
 isPrimitiveType ty = case splitTyConApp_maybe ty of
                        Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
                                              isPrimTyCon tc
-                       other              -> False
+                       _                  -> False
 \end{code}
 
 
@@ -870,7 +934,6 @@ seqType :: Type -> ()
 seqType (TyVarTy tv)     = tv `seq` ()
 seqType (AppTy t1 t2)    = seqType t1 `seq` seqType t2
 seqType (FunTy t1 t2)    = seqType t1 `seq` seqType t2
-seqType (NoteTy note t2)  = seqNote note `seq` seqType t2
 seqType (PredTy p)       = seqPred p
 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
@@ -879,9 +942,6 @@ seqTypes :: [Type] -> ()
 seqTypes []       = ()
 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
 
-seqNote :: TyNote -> ()
-seqNote (FTVNote set) = sizeUniqSet set `seq` ()
-
 seqPred :: PredType -> ()
 seqPred (ClassP c tys)   = c `seq` seqTypes tys
 seqPred (IParam n ty)    = n `seq` seqType ty
@@ -927,7 +987,7 @@ coreEqType t1 t2
                 | Just t2' <- coreView t2 = eq env t1 t2' 
 
        -- Fall through case; not equal!
-    eq env t1 t2 = False
+    eq _ _ _ = False
 \end{code}
 
 
@@ -958,6 +1018,9 @@ tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
 tcEqPred :: PredType -> PredType -> Bool
 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
 
+tcEqPredX :: RnEnv2 -> PredType -> PredType -> Bool
+tcEqPredX env p1 p2 = isEqual $ cmpPredX env p1 p2
+
 tcCmpPred :: PredType -> PredType -> Ordering
 tcCmpPred p1 p2 = cmpPred p1 p2
 
@@ -965,6 +1028,28 @@ tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
 \end{code}
 
+Checks whether the second argument is a subterm of the first.  (We don't care
+about binders, as we are only interested in syntactic subterms.)
+
+\begin{code}
+tcPartOfType :: Type -> Type -> Bool
+tcPartOfType t1              t2 
+  | tcEqType t1 t2              = True
+tcPartOfType t1              t2 
+  | Just t2' <- tcView t2       = tcPartOfType t1 t2'
+tcPartOfType _  (TyVarTy _)     = False
+tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2
+tcPartOfType t1 (AppTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
+tcPartOfType t1 (FunTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
+tcPartOfType t1 (PredTy p2)     = tcPartOfPred t1 p2
+tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts
+
+tcPartOfPred :: Type -> PredType -> Bool
+tcPartOfPred t1 (IParam _ t2)  = tcPartOfType t1 t2
+tcPartOfPred t1 (ClassP _ ts)  = any (tcPartOfType t1) ts
+tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
+\end{code}
+
 Now here comes the real worker
 
 \begin{code}
@@ -993,48 +1078,49 @@ cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenC
 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
-cmpTypeX env t1                        (NoteTy _ t2)        = cmpTypeX env t1 t2
 
     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
-cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
-    
-cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
-cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
-    
-cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
-cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
-cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
-    
-cmpTypeX env (ForAllTy _ _) (TyVarTy _)    = GT
-cmpTypeX env (ForAllTy _ _) (AppTy _ _)    = GT
-cmpTypeX env (ForAllTy _ _) (FunTy _ _)    = GT
-cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
+cmpTypeX _ (AppTy _ _)    (TyVarTy _)    = GT
 
-cmpTypeX env (PredTy _)   t2           = GT
+cmpTypeX _ (FunTy _ _)    (TyVarTy _)    = GT
+cmpTypeX _ (FunTy _ _)    (AppTy _ _)    = GT
 
-cmpTypeX env _ _ = LT
+cmpTypeX _ (TyConApp _ _) (TyVarTy _)    = GT
+cmpTypeX _ (TyConApp _ _) (AppTy _ _)    = GT
+cmpTypeX _ (TyConApp _ _) (FunTy _ _)    = GT
+
+cmpTypeX _ (ForAllTy _ _) (TyVarTy _)    = GT
+cmpTypeX _ (ForAllTy _ _) (AppTy _ _)    = GT
+cmpTypeX _ (ForAllTy _ _) (FunTy _ _)    = GT
+cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
+
+cmpTypeX _ (PredTy _)     _              = GT
+
+cmpTypeX _ _              _              = LT
 
 -------------
 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
-cmpTypesX env []        []        = EQ
+cmpTypesX _   []        []        = EQ
 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
-cmpTypesX env []        tys       = LT
-cmpTypesX env ty        []        = GT
+cmpTypesX _   []        _         = LT
+cmpTypesX _   _         []        = GT
 
 -------------
 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
-       -- Compare types as well as names for implicit parameters
-       -- This comparison is used exclusively (I think) for the
-       -- finite map built in TcSimplify
-cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
+       -- Compare names only for implicit parameters
+       -- This comparison is used exclusively (I believe) 
+       -- for the Avails finite map built in TcSimplify
+       -- If the types differ we keep them distinct so that we see 
+       -- a distinct pair to run improvement on 
+cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
 
 -- Constructor order: IParam < ClassP < EqPred
-cmpPredX env (IParam {})     _             = LT
-cmpPredX env (ClassP {})    (IParam {})     = GT
-cmpPredX env (ClassP {})    (EqPred {})     = LT
-cmpPredX env (EqPred {})    _              = GT
+cmpPredX _   (IParam {})     _              = LT
+cmpPredX _   (ClassP {})    (IParam {})     = GT
+cmpPredX _   (ClassP {})    (EqPred {})     = LT
+cmpPredX _   (EqPred {})    _               = GT
 \end{code}
 
 PredTypes are used as a FM key in TcSimplify, 
@@ -1056,11 +1142,13 @@ instance Ord PredType where { compare = tcCmpPred }
 data TvSubst           
   = TvSubst InScopeSet         -- The in-scope type variables
            TvSubstEnv  -- The substitution itself
-                       -- See Note [Apply Once]
+       -- See Note [Apply Once]
+       -- and Note [Extending the TvSubstEnv]
 
 {- ----------------------------------------------------------
-               Note [Apply Once]
 
+Note [Apply Once]
+~~~~~~~~~~~~~~~~~
 We use TvSubsts to instantiate things, and we might instantiate
        forall a b. ty
 \with the types
@@ -1077,6 +1165,38 @@ variations happen to; for example [a -> (a, b)].
 
 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
 we use during unifications, it must not be repeatedly applied.
+
+Note [Extending the TvSubst]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The following invariant should hold of a TvSubst
+
+       The in-scope set is needed *only* to
+       guide the generation of fresh uniques
+
+       In particular, the *kind* of the type variables in 
+       the in-scope set is not relevant
+
+This invariant allows a short-cut when the TvSubstEnv is empty:
+if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
+then (substTy subst ty) does nothing.
+
+For example, consider:
+       (/\a. /\b:(a~Int). ...b..) Int
+We substitute Int for 'a'.  The Unique of 'b' does not change, but
+nevertheless we add 'b' to the TvSubstEnv, because b's type does change
+
+This invariant has several crucial consequences:
+
+* In substTyVarBndr, we need extend the TvSubstEnv 
+       - if the unique has changed
+       - or if the kind has changed
+
+* In substTyVar, we do not need to consult the in-scope set;
+  the TvSubstEnv is enough
+
+* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
+  
+
 -------------------------------------------------------------- -}
 
 
@@ -1102,9 +1222,11 @@ composeTvSubst in_scope env1 env2
   where
     subst1 = TvSubst in_scope env1
 
+emptyTvSubst :: TvSubst
 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
 
 isEmptyTvSubst :: TvSubst -> Bool
+        -- See Note [Extending the TvSubstEnv]
 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
 
 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
@@ -1139,16 +1261,27 @@ extendTvSubstList (TvSubst in_scope env) tvs tys
 -- the types given; but it's just a thunk so with a bit of luck
 -- it'll never be evaluated
 
+-- Note [Generating the in-scope set for a substitution]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- If we want to substitute [a -> ty1, b -> ty2] I used to 
+-- think it was enough to generate an in-scope set that includes
+-- fv(ty1,ty2).  But that's not enough; we really should also take the
+-- free vars of the type we are substituting into!  Example:
+--     (forall b. (a,b,x)) [a -> List b]
+-- Then if we use the in-scope set {b}, there is a danger we will rename
+-- the forall'd variable to 'x' by mistake, getting this:
+--     (forall x. (List b, x, x)
+-- Urk!  This means looking at all the calls to mkOpenTvSubst....
+
+
 mkOpenTvSubst :: TvSubstEnv -> TvSubst
 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
 
 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
 zipOpenTvSubst tyvars tys 
-#ifdef DEBUG
-  | length tyvars /= length tys
+  | debugIsOn && (length tyvars /= length tys)
   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
   | otherwise
-#endif
   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
 
 -- mkTopTvSubst is called when doing top-level substitutions.
@@ -1159,24 +1292,21 @@ mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
 
 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
 zipTopTvSubst tyvars tys 
-#ifdef DEBUG
-  | length tyvars /= length tys
-  = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
+  | debugIsOn && (length tyvars /= length tys)
+  = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
   | otherwise
-#endif
   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
 
 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
 zipTyEnv tyvars tys
-#ifdef DEBUG
-  | length tyvars /= length tys
+  | debugIsOn && (length tyvars /= length tys)
   = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
   | otherwise
-#endif
   = zip_ty_env tyvars tys emptyVarEnv
 
 -- Later substitutions in the list over-ride earlier ones, 
 -- but there should be no loops
+zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
 zip_ty_env []       []       env = env
 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
        -- There used to be a special case for when 
@@ -1196,9 +1326,9 @@ zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr
 
 instance Outputable TvSubst where
   ppr (TvSubst ins env) 
-    = brackets $ sep[ ptext SLIT("TvSubst"),
-                     nest 2 (ptext SLIT("In scope:") <+> ppr ins), 
-                     nest 2 (ptext SLIT("Env:") <+> ppr env) ]
+    = brackets $ sep[ ptext (sLit "TvSubst"),
+                     nest 2 (ptext (sLit "In scope:") <+> ppr ins), 
+                     nest 2 (ptext (sLit "Env:") <+> ppr env) ]
 \end{code}
 
 %************************************************************************
@@ -1244,36 +1374,40 @@ subst_ty :: TvSubst -> Type -> Type
 subst_ty subst ty
    = go ty
   where
-    go (TyVarTy tv)               = substTyVar subst tv
-    go (TyConApp tc tys)          = let args = map go tys
-                                    in  args `seqList` TyConApp tc args
-
-    go (PredTy p)                 = PredTy $! (substPred subst p)
+    go (TyVarTy tv)                = substTyVar subst tv
+    go (TyConApp tc tys)           = let args = map go tys
+                                     in  args `seqList` TyConApp tc args
 
-    go (NoteTy (FTVNote _) ty2)    = go ty2            -- Discard the free tyvar note
+    go (PredTy p)                  = PredTy $! (substPred subst p)
 
-    go (FunTy arg res)            = (FunTy $! (go arg)) $! (go res)
-    go (AppTy fun arg)            = mkAppTy (go fun) $! (go arg)
-               -- The mkAppTy smart constructor is important
-               -- we might be replacing (a Int), represented with App
-               -- by [Int], represented with TyConApp
-    go (ForAllTy tv ty)                   = case substTyVarBndr subst tv of
-                                       (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
+    go (FunTy arg res)             = (FunTy $! (go arg)) $! (go res)
+    go (AppTy fun arg)             = mkAppTy (go fun) $! (go arg)
+                -- The mkAppTy smart constructor is important
+                -- we might be replacing (a Int), represented with App
+                -- by [Int], represented with TyConApp
+    go (ForAllTy tv ty)            = case substTyVarBndr subst tv of
+                                     (subst', tv') ->
+                                         ForAllTy tv' $! (subst_ty subst' ty)
 
 substTyVar :: TvSubst -> TyVar  -> Type
-substTyVar subst@(TvSubst in_scope env) tv
+substTyVar subst@(TvSubst _ _) tv
   = case lookupTyVar subst tv of {
-       Nothing  -> TyVarTy tv;
+       Nothing -> TyVarTy tv;
                Just ty -> ty   -- See Note [Apply Once]
     } 
 
+substTyVars :: TvSubst -> [TyVar] -> [Type]
+substTyVars subst tvs = map (substTyVar subst) tvs
+
 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
-lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv
+       -- See Note [Extending the TvSubst]
+lookupTyVar (TvSubst _ env) tv = lookupVarEnv env tv
 
 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar) 
 substTyVarBndr subst@(TvSubst in_scope env) old_var
   = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
   where
+    is_co_var = isCoVar old_var
 
     new_env | no_change = delVarEnv env old_var
            | otherwise = extendVarEnv env old_var (TyVarTy new_var)
@@ -1281,6 +1415,7 @@ substTyVarBndr subst@(TvSubst in_scope env) old_var
     no_change = new_var == old_var && not is_co_var
        -- no_change means that the new_var is identical in
        -- all respects to the old_var (same unique, same kind)
+       -- See Note [Extending the TvSubst]
        --
        -- In that case we don't need to extend the substitution
        -- to map old to new.  But instead we must zap any 
@@ -1292,12 +1427,10 @@ substTyVarBndr subst@(TvSubst in_scope env) old_var
        -- The uniqAway part makes sure the new variable is not already in scope
 
     subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
-                -- It's only worth doing the substitution for coercions,
-                -- becuase only they can have free type variables
-       | is_co_var = setTyVarKind old_var (substTy subst kind)
+                 -- It's only worth doing the substitution for coercions,
+                 -- becuase only they can have free type variables
+       | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
        | otherwise = old_var
-    kind = tyVarKind old_var
-    is_co_var = isCoercionKind kind
 \end{code}
 
 ----------------------------------------------------
@@ -1380,26 +1513,28 @@ splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
 splitKindFunTysN k = splitFunTysN k
 
 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
+isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
+        isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool
 
 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
 
 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
-isOpenTypeKind other           = False
+isOpenTypeKind _               = False
 
 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
 
 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
-isUbxTupleKind other          = False
+isUbxTupleKind _               = False
 
 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
 
 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
-isArgTypeKind other = False
+isArgTypeKind _               = False
 
 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
 
 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
-isUnliftedTypeKind other           = False
+isUnliftedTypeKind _               = False
 
 isSubOpenTypeKind :: Kind -> Bool
 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
@@ -1421,24 +1556,22 @@ isSubArgTypeKindCon kc
 isSubArgTypeKind :: Kind -> Bool
 -- True of any sub-kind of ArgTypeKind 
 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
-isSubArgTypeKind other            = False
+isSubArgTypeKind _                = False
 
 isSuperKind :: Type -> Bool
 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
-isSuperKind other = False
+isSuperKind _                   = False
 
 isKind :: Kind -> Bool
 isKind k = isSuperKind (typeKind k)
 
-
-
 isSubKind :: Kind -> Kind -> Bool
 -- (k1 `isSubKind` k2) checks that k1 <: k2
 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
 isSubKind (FunTy a1 r1) (FunTy a2 r2)        = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) 
   = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
-isSubKind k1           k2                    = False
+isSubKind _             _                     = False
 
 eqKind :: Kind -> Kind -> Bool
 eqKind = tcEqType
@@ -1473,15 +1606,7 @@ defaultKind k
   | isSubArgTypeKind k  = liftedTypeKind
   | otherwise        = k
 
-isCoercionKind :: Kind -> Bool
--- All coercions are of form (ty1 :=: ty2)
--- This function is here rather than in Coercion, 
--- because it's used by substTy
-isCoercionKind k | Just k' <- kindView k = isCoercionKind k'
-isCoercionKind (PredTy (EqPred {}))     = True
-isCoercionKind other                    = False
-
 isEqPred :: PredType -> Bool
 isEqPred (EqPred _ _) = True
-isEqPred other       = False
+isEqPred _            = False
 \end{code}