remove empty dir
[ghc-hetmet.git] / ghc / compiler / types / Type.lhs
index 925357f..872feb0 100644 (file)
@@ -5,61 +5,46 @@
 
 \begin{code}
 module Type (
-        -- re-exports from TypeRep:
-       Type, PredType, TauType, ThetaType,
-       Kind, TyVarSubst,
-
-       superKind, superBoxity,                         -- KX and BX respectively
-       liftedBoxity, unliftedBoxity,                   -- :: BX
-       openKindCon,                                    -- :: KX
-       typeCon,                                        -- :: BX -> KX
-       liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
-       mkArrowKind, mkArrowKinds,                      -- :: KX -> KX -> KX
-       isTypeKind,
+        -- re-exports from TypeRep
+       TyThing(..), Type, PredType(..), ThetaType, 
        funTyCon,
 
-        usageKindCon,                                  -- :: KX
-        usageTypeKind,                                 -- :: KX
-        usOnceTyCon, usManyTyCon,                      -- :: $
-        usOnce, usMany,                                        -- :: $
+       -- Re-exports from Kind
+       module Kind,
 
-        -- exports from this module:
-        hasMoreBoxityInfo, defaultKind,
+       -- Re-exports from TyCon
+       PrimRep(..),
 
        mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
 
        mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
 
-       mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, splitFunTys, 
-       funResultTy, funArgTy, zipFunTys,
+       mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, 
+       splitFunTys, splitFunTysN,
+       funResultTy, funArgTy, zipFunTys, isFunTy,
 
        mkTyConApp, mkTyConTy, 
        tyConAppTyCon, tyConAppArgs, 
        splitTyConApp_maybe, splitTyConApp,
 
-       mkUTy, splitUTy, splitUTy_maybe,
-        isUTy, uaUTy, unUTy, liftUTy, mkUTyM,
-        isUsageKind, isUsage, isUTyVar,
-
-       mkSynTy, 
-
-       repType, splitRepFunTys, typePrimRep,
+       repType, typePrimRep, coreView, tcView,
 
        mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
-       applyTy, applyTys, isForAllTy,
+       applyTy, applyTys, isForAllTy, dropForAlls,
 
        -- Source types
-       SourceType(..), sourceTypeRep, mkPredTy, mkPredTys,
+       predTypeRep, mkPredTy, mkPredTys,
 
        -- Newtypes
-       splitNewType_maybe,
+       splitRecNewType_maybe,
 
        -- Lifting and boxity
-       isUnLiftedType, isUnboxedTupleType, isAlgType, isStrictType, isPrimitiveType,
+       isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
+       isStrictType, isStrictPred, 
 
        -- Free variables
        tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-       usageAnnOfType, typeKind, addFreeTyVars,
+       typeKind, addFreeTyVars,
 
        -- Tidying up for printing
        tidyType,      tidyTypes,
@@ -67,13 +52,29 @@ module Type (
        tidyTyVarBndr, tidyFreeTyVars,
        tidyOpenTyVar, tidyOpenTyVars,
        tidyTopType,   tidyPred,
+       tidyKind,
 
        -- Comparison
-       eqType, eqKind, eqUsage, 
+       coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
+       tcEqPred, tcCmpPred, tcEqTypeX, 
 
        -- Seq
-       seqType, seqTypes
-
+       seqType, seqTypes,
+
+       -- Type substitutions
+       TvSubstEnv, emptyTvSubstEnv,    -- Representation widely visible
+       TvSubst(..), emptyTvSubst,      -- Representation visible to a few friends
+       mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
+       getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
+       extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
+
+       -- Performing substitution on types
+       substTy, substTys, substTyWith, substTheta, 
+       substPred, substTyVar, substTyVarBndr, deShadowTy, lookupTyVar,
+
+       -- Pretty-printing
+       pprType, pprParendType, pprTyThingCategory,
+       pprPred, pprTheta, pprThetaArrow, pprClassPred
     ) where
 
 #include "HsVersions.h"
@@ -83,60 +84,80 @@ module Type (
 
 import TypeRep
 
--- Other imports:
-
-import {-# SOURCE #-}  PprType( pprType )      -- Only called in debug messages
-import {-# SOURCE #-}   Subst  ( substTyWith )
-
 -- friends:
-import Var     ( Var, TyVar, tyVarKind, tyVarName, setTyVarName )
+import Kind
+import Var     ( Var, TyVar, tyVarKind, tyVarName, setTyVarName, mkTyVar )
 import VarEnv
 import VarSet
 
-import Name    ( NamedThing(..), mkLocalName, tidyOccName )
-import Class   ( classTyCon )
+import OccName ( tidyOccName )
+import Name    ( NamedThing(..), mkInternalName, tidyNameOcc )
+import Class   ( Class, classTyCon )
 import TyCon   ( TyCon, isRecursiveTyCon, isPrimTyCon,
                  isUnboxedTupleTyCon, isUnLiftedTyCon,
-                 isFunTyCon, isNewTyCon, newTyConRep,
-                 isAlgTyCon, isSynTyCon, tyConArity, 
-                 tyConKind, getSynTyConDefn,
-                 tyConPrimRep, 
+                 isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
+                 isAlgTyCon, tyConArity, 
+                 tcExpandTyCon_maybe, coreExpandTyCon_maybe,
+                 tyConKind, PrimRep(..), tyConPrimRep,
                )
 
 -- others
-import CmdLineOpts     ( opt_DictsStrict )
-import Maybes          ( maybeToBool )
+import StaticFlags     ( opt_DictsStrict )
 import SrcLoc          ( noSrcLoc )
-import PrimRep         ( PrimRep(..) )
-import Unique          ( Uniquable(..) )
-import Util            ( mapAccumL, seqList, lengthIs )
+import Util            ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
 import Outputable
 import UniqSet         ( sizeUniqSet )         -- Should come via VarSet
+import Maybe           ( isJust )
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Stuff to do with kinds.}
+               Type representation
 %*                                                                     *
 %************************************************************************
 
+In Core, we "look through" non-recursive newtypes and PredTypes.
+
 \begin{code}
-hasMoreBoxityInfo :: Kind -> Kind -> Bool
-hasMoreBoxityInfo k1 k2
-  | k2 `eqKind` openTypeKind = True
-  | otherwise               = k1 `eqType` k2
-
-defaultKind :: Kind -> Kind
--- Used when generalising: default kind '?' to '*'
-defaultKind kind | kind `eqKind` openTypeKind = liftedTypeKind
-                | otherwise                  = kind
-
-isTypeKind :: Kind -> Bool
--- True of kind * and *#
-isTypeKind k = case splitTyConApp_maybe k of
-                Just (tc,[k]) -> tc == typeCon
-                other         -> False
+{-# INLINE coreView #-}
+coreView :: Type -> Maybe Type
+-- Srips off the *top layer only* of a type to give 
+-- its underlying representation type. 
+-- Returns Nothing if there is nothing to look through.
+--
+-- In the case of newtypes, it returns
+--     *either* a vanilla TyConApp (recursive newtype, or non-saturated)
+--     *or*     the newtype representation (otherwise), meaning the
+--                     type written in the RHS of the newtype decl,
+--                     which may itself be a newtype
+--
+-- Example: newtype R = MkR S
+--         newtype S = MkS T
+--         newtype T = MkT (T -> T)
+--   expandNewTcApp on R gives Just S
+--                 on S gives Just T
+--                 on T gives Nothing   (no expansion)
+
+-- 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)               = Just (predTypeRep p)
+coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
+                          = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
+                               -- 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
+
+-----------------------------------------------
+{-# 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
 \end{code}
 
 
@@ -158,25 +179,17 @@ mkTyVarTys :: [TyVar] -> [Type]
 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
 
 getTyVar :: String -> Type -> TyVar
-getTyVar msg (TyVarTy tv)     = tv
-getTyVar msg (SourceTy p)     = getTyVar msg (sourceTypeRep p)
-getTyVar msg (NoteTy _ t)     = getTyVar msg t
-getTyVar msg ty@(UsageTy _ _) = pprPanic "getTyVar: UTy:" (text msg $$ pprType ty)
-getTyVar msg other           = panic ("getTyVar: " ++ msg)
-
-getTyVar_maybe :: Type -> Maybe TyVar
-getTyVar_maybe (TyVarTy tv)    = Just tv
-getTyVar_maybe (NoteTy _ t)    = getTyVar_maybe t
-getTyVar_maybe (SourceTy p)    = getTyVar_maybe (sourceTypeRep p)
-getTyVar_maybe ty@(UsageTy _ _) = pprPanic "getTyVar_maybe: UTy:" (pprType ty)
-getTyVar_maybe other           = Nothing
+getTyVar msg ty = case getTyVar_maybe ty of
+                   Just tv -> tv
+                   Nothing -> panic ("getTyVar: " ++ msg)
 
 isTyVarTy :: Type -> Bool
-isTyVarTy (TyVarTy tv)     = True
-isTyVarTy (NoteTy _ ty)    = isTyVarTy ty
-isTyVarTy (SourceTy p)     = isTyVarTy (sourceTypeRep p)
-isTyVarTy ty@(UsageTy _ _) = pprPanic "isTyVarTy: UTy:" (pprType ty)
-isTyVarTy other            = False
+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
 \end{code}
 
 
@@ -189,15 +202,19 @@ invariant: use it.
 
 \begin{code}
 mkAppTy orig_ty1 orig_ty2
-  = ASSERT( not (isSourceTy orig_ty1) )        -- Source types are of kind *
-    UASSERT2( not (isUTy orig_ty2), pprType orig_ty1 <+> pprType orig_ty2 )
-                                        -- argument must be unannotated
-    mk_app orig_ty1
+  = mk_app orig_ty1
   where
     mk_app (NoteTy _ ty1)    = mk_app ty1
     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
-    mk_app ty@(UsageTy _ _)  = pprPanic "mkAppTy: UTy:" (pprType ty)
     mk_app ty1              = 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
+       --      type Id x = x
+       --      foo :: Foo Id -> Foo Id
+       --
+       -- Here Id is partially applied in the type sig for Foo,
+       -- but once the type synonyms are expanded all is well
 
 mkAppTys :: Type -> [Type] -> Type
 mkAppTys orig_ty1 []       = orig_ty1
@@ -207,29 +224,21 @@ mkAppTys orig_ty1 []          = orig_ty1
        --   returns to (Ratio Integer), which has needlessly lost
        --   the Rational part.
 mkAppTys orig_ty1 orig_tys2
-  = ASSERT( not (isSourceTy orig_ty1) )        -- Source types are of kind *
-    UASSERT2( not (any isUTy orig_tys2), pprType orig_ty1 <+> fsep (map pprType orig_tys2) )
-                                        -- arguments must be unannotated
-    mk_app orig_ty1
+  = mk_app orig_ty1
   where
     mk_app (NoteTy _ ty1)    = mk_app ty1
     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
-    mk_app ty@(UsageTy _ _)  = pprPanic "mkAppTys: UTy:" (pprType ty)
+                               -- mkTyConApp: see notes with mkAppTy
     mk_app ty1              = foldl AppTy orig_ty1 orig_tys2
 
 splitAppTy_maybe :: Type -> Maybe (Type, Type)
-splitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
+splitAppTy_maybe ty | Just ty' <- coreView ty = splitAppTy_maybe ty'
+splitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 splitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
-splitAppTy_maybe (NoteTy _ ty)     = splitAppTy_maybe ty
-splitAppTy_maybe (SourceTy p)        = splitAppTy_maybe (sourceTypeRep p)
-splitAppTy_maybe (TyConApp tc [])  = Nothing
-splitAppTy_maybe (TyConApp tc tys) = split tys []
-                           where
-                              split [ty2]    acc = Just (TyConApp tc (reverse acc), ty2)
-                              split (ty:tys) acc = split tys (ty:acc)
-
-splitAppTy_maybe ty@(UsageTy _ _)  = pprPanic "splitAppTy_maybe: UTy:" (pprType ty)
-splitAppTy_maybe other           = Nothing
+splitAppTy_maybe (TyConApp tc tys) = case snocView tys of
+                                       Nothing         -> Nothing
+                                       Just (tys',ty') -> Just (TyConApp tc tys', ty')
+splitAppTy_maybe other            = Nothing
 
 splitAppTy :: Type -> (Type, Type)
 splitAppTy ty = case splitAppTy_maybe ty of
@@ -239,13 +248,11 @@ splitAppTy ty = case splitAppTy_maybe ty of
 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 (NoteTy _ ty)         args = split orig_ty ty args
-    split orig_ty (SourceTy p)            args = split orig_ty (sourceTypeRep p) args
-    split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
-                                              (TyConApp funTyCon [], [unUTy ty1,unUTy ty2])
     split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
-    split orig_ty (UsageTy _ _)         args = pprPanic "splitAppTys: UTy:" (pprType orig_ty)
+    split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
+                                              (TyConApp funTyCon [], [ty1,ty2])
     split orig_ty ty                   args = (orig_ty, args)
 \end{code}
 
@@ -256,87 +263,76 @@ splitAppTys ty = split ty ty []
 
 \begin{code}
 mkFunTy :: Type -> Type -> Type
-mkFunTy arg res = UASSERT2( isUTy arg && isUTy res, pprType arg <+> pprType res )
-                  FunTy arg res
+mkFunTy arg res = FunTy arg res
 
 mkFunTys :: [Type] -> Type -> Type
-mkFunTys tys ty = UASSERT2( all isUTy (ty:tys), fsep (map pprType (tys++[ty])) )
-                  foldr FunTy ty tys
+mkFunTys tys ty = foldr FunTy ty tys
+
+isFunTy :: Type -> Bool 
+isFunTy ty = isJust (splitFunTy_maybe ty)
 
 splitFunTy :: Type -> (Type, Type)
-splitFunTy (FunTy arg res) = (arg, res)
-splitFunTy (NoteTy _ ty)   = splitFunTy ty
-splitFunTy (SourceTy p)      = splitFunTy (sourceTypeRep p)
-splitFunTy ty@(UsageTy _ _) = pprPanic "splitFunTy: UTy:" (pprType ty)
+splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
+splitFunTy (FunTy arg res)   = (arg, res)
+splitFunTy other            = pprPanic "splitFunTy" (ppr other)
 
 splitFunTy_maybe :: Type -> Maybe (Type, Type)
-splitFunTy_maybe (FunTy arg res) = Just (arg, res)
-splitFunTy_maybe (NoteTy _ ty)   = splitFunTy_maybe ty
-splitFunTy_maybe (SourceTy p)           = splitFunTy_maybe (sourceTypeRep p)
-splitFunTy_maybe ty@(UsageTy _ _) = pprPanic "splitFunTy_maybe: UTy:" (pprType ty)
-splitFunTy_maybe other          = Nothing
+splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
+splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
+splitFunTy_maybe other            = Nothing
 
 splitFunTys :: Type -> ([Type], Type)
 splitFunTys ty = split [] ty ty
   where
-    split args orig_ty (FunTy arg res) = split (arg:args) res res
-    split args orig_ty (NoteTy _ ty)   = split args orig_ty ty
-    split args orig_ty (SourceTy p)      = split args orig_ty (sourceTypeRep p)
-    split args orig_ty (UsageTy _ _)   = pprPanic "splitFunTys: UTy:" (pprType orig_ty)
-    split args orig_ty ty              = (reverse args, orig_ty)
+    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)
+
+splitFunTysN :: Int -> Type -> ([Type], Type)
+-- Split off exactly n arg tys
+splitFunTysN 0 ty = ([], ty)
+splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
+                   case splitFunTysN (n-1) res of { (args, res) ->
+                   (arg:args, 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 (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res
-    split acc xs     nty (NoteTy _ ty)   = split acc           xs nty ty
-    split acc xs     nty (SourceTy p)      = split acc           xs nty (sourceTypeRep p)
-    split acc xs     nty (UsageTy _ _)   = pprPanic "zipFunTys: UTy:" (ppr orig_xs <+> pprType orig_ty)
-    split acc (x:xs) nty ty              = pprPanic "zipFunTys" (ppr orig_xs <+> pprType orig_ty)
+    split acc []     nty ty               = (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)
     
 funResultTy :: Type -> Type
-funResultTy (FunTy arg res) = res
-funResultTy (NoteTy _ ty)   = funResultTy ty
-funResultTy (SourceTy p)      = funResultTy (sourceTypeRep p)
-funResultTy (UsageTy _ ty)  = funResultTy ty
-funResultTy ty             = pprPanic "funResultTy" (pprType ty)
+funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
+funResultTy (FunTy arg res)   = res
+funResultTy ty               = pprPanic "funResultTy" (ppr ty)
 
 funArgTy :: Type -> Type
-funArgTy (FunTy arg res) = arg
-funArgTy (NoteTy _ ty)   = funArgTy ty
-funArgTy (SourceTy p)      = funArgTy (sourceTypeRep p)
-funArgTy (UsageTy _ ty)  = funArgTy ty
-funArgTy ty             = pprPanic "funArgTy" (pprType ty)
+funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
+funArgTy (FunTy arg res)   = arg
+funArgTy ty               = pprPanic "funArgTy" (ppr ty)
 \end{code}
 
 
 ---------------------------------------------------------------------
                                TyConApp
                                ~~~~~~~~
-@mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or SourceTy,
+@mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
 as apppropriate.
 
 \begin{code}
 mkTyConApp :: TyCon -> [Type] -> Type
--- Assumes TyCon is not a SynTyCon; use mkSynTy instead for those
 mkTyConApp tycon tys
   | isFunTyCon tycon, [ty1,ty2] <- tys
-  = FunTy (mkUTyM ty1) (mkUTyM ty2)
-
-  | isNewTyCon tycon,                  -- A saturated newtype application;
-    not (isRecursiveTyCon tycon),      -- Not recursive (we don't use SourceTypes for them)
-    tys `lengthIs` tyConArity tycon     -- use the SourceType form
-  = SourceTy (NType tycon tys)
+  = FunTy ty1 ty2
 
   | otherwise
-  = ASSERT(not (isSynTyCon tycon))
-    UASSERT2( not (any isUTy tys), ppr tycon <+> fsep (map pprType tys) )
-    TyConApp tycon tys
+  = TyConApp tycon tys
 
 mkTyConTy :: TyCon -> Type
-mkTyConTy tycon = ASSERT( not (isSynTyCon tycon) ) 
-                 TyConApp tycon []
+mkTyConTy tycon = mkTyConApp tycon []
 
 -- splitTyConApp "looks through" synonyms, because they don't
 -- mean a distinct type, but all other type-constructor applications
@@ -351,14 +347,12 @@ tyConAppArgs ty = snd (splitTyConApp ty)
 splitTyConApp :: Type -> (TyCon, [Type])
 splitTyConApp ty = case splitTyConApp_maybe ty of
                        Just stuff -> stuff
-                       Nothing    -> pprPanic "splitTyConApp" (pprType ty)
+                       Nothing    -> pprPanic "splitTyConApp" (ppr ty)
 
 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, [unUTy arg,unUTy res])
-splitTyConApp_maybe (NoteTy _ ty)     = splitTyConApp_maybe ty
-splitTyConApp_maybe (SourceTy p)      = splitTyConApp_maybe (sourceTypeRep p)
-splitTyConApp_maybe (UsageTy _ ty)    = splitTyConApp_maybe ty
+splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
 splitTyConApp_maybe other            = Nothing
 \end{code}
 
@@ -367,29 +361,6 @@ splitTyConApp_maybe other        = Nothing
                                SynTy
                                ~~~~~
 
-\begin{code}
-mkSynTy tycon tys
-  | n_args == arity    -- Exactly saturated
-  = mk_syn tys
-  | n_args >  arity    -- Over-saturated
-  = case splitAt arity tys of { (as,bs) -> foldl AppTy (mk_syn as) bs }
-  | otherwise          -- Un-saturated
-  = TyConApp tycon tys
-       -- For the un-saturated case we build TyConApp directly
-       -- (mkTyConApp ASSERTs that the tc isn't a SynTyCon).
-       -- Here we are relying on checkValidType to find
-       -- the error.  What we can't do is use mkSynTy with
-       -- too few arg tys, because that is utterly bogus.
-
-  where
-    mk_syn tys = NoteTy (SynNote (TyConApp tycon tys))
-                       (substTyWith tyvars tys body)
-
-    (tyvars, body) = ASSERT( isSynTyCon tycon ) getSynTyConDefn tycon
-    arity         = tyConArity tycon
-    n_args        = length tys
-\end{code}
-
 Notes on type synonyms
 ~~~~~~~~~~~~~~~~~~~~~~
 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
@@ -407,44 +378,51 @@ interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
 
                Representation types
                ~~~~~~~~~~~~~~~~~~~~
-
 repType looks through 
        (a) for-alls, and
        (b) synonyms
        (c) predicates
        (d) usage annotations
-       (e) [recursive] newtypes
+       (e) all newtypes, including recursive ones
 It's useful in the back end.
 
-Remember, non-recursive newtypes get expanded as part of the SourceTy case,
-but recursive ones are represented by TyConApps and have to be expanded
-by steam.
-
 \begin{code}
 repType :: Type -> Type
-repType (ForAllTy _ ty)   = repType ty
-repType (NoteTy   _ ty)   = repType ty
-repType (SourceTy  p)     = repType (sourceTypeRep p)
-repType (UsageTy  _ ty)   = repType ty
-repType (TyConApp tc tys) | isNewTyCon tc && tys `lengthIs` tyConArity tc
-                         = repType (newTypeRep tc tys)
-repType ty               = ty
-
-splitRepFunTys :: Type -> ([Type], Type)
--- Like splitFunTys, but looks through newtypes and for-alls
-splitRepFunTys ty = split [] (repType ty)
-  where
-    split args (FunTy arg res)  = split (arg:args) (repType res)
-    split args ty               = (reverse args, ty)
-
+-- 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)
+  | isNewTyCon 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
+
+-- ToDo: this could be moved to the code generator, using splitTyConApp instead
+-- of inspecting the type directly.
 typePrimRep :: Type -> PrimRep
 typePrimRep ty = case repType ty of
                   TyConApp tc _ -> tyConPrimRep tc
                   FunTy _ _     -> PtrRep
-                  AppTy _ _     -> PtrRep      -- ??
+                  AppTy _ _     -> PtrRep      -- See note below
                   TyVarTy _     -> PtrRep
-\end{code}
+                  other         -> 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}
 
 
 ---------------------------------------------------------------------
@@ -457,153 +435,74 @@ mkForAllTy tyvar ty
   = mkForAllTys [tyvar] ty
 
 mkForAllTys :: [TyVar] -> Type -> Type
-mkForAllTys tyvars ty
-  = case splitUTy_maybe ty of
-      Just (u,ty1) -> UASSERT2( not (mkVarSet tyvars `intersectsVarSet` tyVarsOfType u),
-                                ptext SLIT("mkForAllTys: usage scope")
-                                <+> ppr tyvars <+> pprType ty )
-                      mkUTy u (foldr ForAllTy ty1 tyvars)  -- we lift usage annotations over foralls
-      Nothing      -> foldr ForAllTy ty tyvars
+mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 
 isForAllTy :: Type -> Bool
 isForAllTy (NoteTy _ ty)  = isForAllTy ty
 isForAllTy (ForAllTy _ _) = True
-isForAllTy (UsageTy _ ty) = isForAllTy ty
 isForAllTy other_ty      = False
 
 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
 splitForAllTy_maybe ty = splitFAT_m ty
   where
-    splitFAT_m (NoteTy _ ty)           = splitFAT_m ty
-    splitFAT_m (SourceTy p)            = splitFAT_m (sourceTypeRep p)
-    splitFAT_m (ForAllTy tyvar ty)     = Just(tyvar, ty)
-    splitFAT_m (UsageTy _ ty)           = splitFAT_m ty
-    splitFAT_m _                       = Nothing
+    splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
+    splitFAT_m (ForAllTy tyvar ty)         = Just(tyvar, ty)
+    splitFAT_m _                           = Nothing
 
 splitForAllTys :: Type -> ([TyVar], Type)
 splitForAllTys ty = split ty ty []
    where
-     split orig_ty (ForAllTy tv ty)      tvs = split ty ty (tv:tvs)
-     split orig_ty (NoteTy _ ty)         tvs = split orig_ty ty tvs
-     split orig_ty (SourceTy p)                  tvs = split orig_ty (sourceTypeRep p) tvs
-     split orig_ty (UsageTy _ ty)         tvs = split orig_ty ty tvs
-     split orig_ty t                     tvs = (reverse tvs, orig_ty)
+     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)
+
+dropForAlls :: Type -> Type
+dropForAlls ty = snd (splitForAllTys ty)
 \end{code}
 
 -- (mkPiType now in CoreUtils)
 
-Applying a for-all to its arguments.  Lift usage annotation as required.
+applyTy, applyTys
+~~~~~~~~~~~~~~~~~
+Instantiate a for-all type with one or more type arguments.
+Used when we have a polymorphic function applied to type args:
+       f t1 t2
+Then we use (applyTys type-of-f [t1,t2]) to compute the type of
+the expression. 
 
 \begin{code}
 applyTy :: Type -> Type -> Type
-applyTy (SourceTy p)                   arg = applyTy (sourceTypeRep p) arg
-applyTy (NoteTy _ fun)                  arg = applyTy fun arg
-applyTy (ForAllTy tv ty)                arg = UASSERT2( not (isUTy arg),
-                                                        ptext SLIT("applyTy")
-                                                        <+> pprType ty <+> pprType arg )
-                                              substTyWith [tv] [arg] ty
-applyTy (UsageTy u ty)                  arg = UsageTy u (applyTy ty arg)
-applyTy other                          arg = panic "applyTy"
+applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
+applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
+applyTy other           arg = panic "applyTy"
 
 applyTys :: Type -> [Type] -> Type
-applyTys fun_ty arg_tys
- = UASSERT2( not (any isUTy arg_tys), ptext SLIT("applyTys") <+> pprType fun_ty )
-   (case mu of
-      Just u  -> UsageTy u
-      Nothing -> id) $
-   substTyWith tvs arg_tys ty
- where
-   (mu, tvs, ty) = split fun_ty arg_tys
-   
-   split fun_ty               []         = (Nothing, [], fun_ty)
-   split (NoteTy _ fun_ty)    args       = split fun_ty args
-   split (SourceTy p)        args       = split (sourceTypeRep p) args
-   split (ForAllTy tv fun_ty) (arg:args) = case split fun_ty args of
-                                                 (mu, tvs, ty) -> (mu, tv:tvs, ty)
-   split (UsageTy u ty)       args       = case split ty args of
-                                                  (Nothing, tvs, ty) -> (Just u, tvs, ty)
-                                                  (Just _ , _  , _ ) -> pprPanic "applyTys:"
-                                                                          (pprType fun_ty)
-   split other_ty             args       = panic "applyTys"
-\end{code}
-
-
----------------------------------------------------------------------
-                               UsageTy
-                               ~~~~~~~
-
-Constructing and taking apart usage types.
-
-\begin{code}
-mkUTy :: Type -> Type -> Type
-mkUTy u ty
-  = ASSERT2( typeKind u `eqKind` usageTypeKind, 
-            ptext SLIT("mkUTy:") <+> pprType u <+> pprType ty )
-    UASSERT2( not (isUTy ty), ptext SLIT("mkUTy:") <+> pprType u <+> pprType ty )
-    -- if u == usMany then ty else  : ToDo? KSW 2000-10
-#ifdef DO_USAGES
-    UsageTy u ty
-#else
-    ty
-#endif
-
-splitUTy :: Type -> (Type {- :: $ -}, Type)
-splitUTy orig_ty
-  = case splitUTy_maybe orig_ty of
-      Just (u,ty) -> (u,ty)
-#ifdef DO_USAGES
-      Nothing     -> pprPanic "splitUTy:" (pprType orig_ty)
-#else
-      Nothing     -> (usMany,orig_ty)  -- default annotation ToDo KSW 2000-10
-#endif
-
-splitUTy_maybe :: Type -> Maybe (Type {- :: $ -}, Type)
-splitUTy_maybe (UsageTy u ty) = Just (u,ty)
-splitUTy_maybe (NoteTy _ ty)  = splitUTy_maybe ty
-splitUTy_maybe other_ty       = Nothing
-
-isUTy :: Type -> Bool
-  -- has usage annotation
-isUTy = maybeToBool . splitUTy_maybe
-
-uaUTy :: Type -> Type
-  -- extract annotation
-uaUTy = fst . splitUTy
-
-unUTy :: Type -> Type
-  -- extract unannotated type
-unUTy = snd . splitUTy
-\end{code}
-
-\begin{code}
-liftUTy :: (Type -> Type) -> Type -> Type
-  -- lift outer usage annot over operation on unannotated types
-liftUTy f ty
-  = let
-      (u,ty') = splitUTy ty
-    in
-    mkUTy u (f ty')
-\end{code}
-
-\begin{code}
-mkUTyM :: Type -> Type
-  -- put TOP (no info) annotation on unannotated type
-mkUTyM ty = mkUTy usMany ty
-\end{code}
-
-\begin{code}
-isUsageKind :: Kind -> Bool
-isUsageKind k
-  = ASSERT( typeKind k `eqKind` superKind )
-    k `eqKind` usageTypeKind
-
-isUsage :: Type -> Bool
-isUsage ty
-  = isUsageKind (typeKind ty)
-
-isUTyVar :: Var -> Bool
-isUTyVar v
-  = isUsageKind (tyVarKind v)
+-- This function is interesting because 
+--     a) the function may have more for-alls than there are args
+--     b) less obviously, it may have fewer for-alls
+-- For case (b) think of 
+--     applyTys (forall a.a) [forall b.b, Int]
+-- This really can happen, via dressing up polymorphic types with newtype
+-- clothing.  Here's an example:
+--     newtype R = R (forall a. a->a)
+--     foo = case undefined :: R of
+--             R f -> f ()
+
+applyTys orig_fun_ty []      = orig_fun_ty
+applyTys orig_fun_ty arg_tys 
+  | n_tvs == n_args    -- The vastly common case
+  = substTyWith tvs arg_tys rho_ty
+  | n_tvs > n_args     -- Too many for-alls
+  = substTyWith (take n_args tvs) arg_tys 
+               (mkForAllTys (drop n_args tvs) rho_ty)
+  | otherwise          -- Too many type args
+  = ASSERT2( n_tvs > 0, ppr orig_fun_ty )      -- Zero case gives infnite loop!
+    applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
+            (drop n_tvs arg_tys)
+  where
+    (tvs, rho_ty) = splitForAllTys orig_fun_ty 
+    n_tvs = length tvs
+    n_args = length arg_tys     
 \end{code}
 
 
@@ -618,47 +517,49 @@ concerned, but which has low-level representation as far as the back end is conc
 
 Source types are always lifted.
 
-The key function is sourceTypeRep which gives the representation of a source type:
+The key function is predTypeRep which gives the representation of a source type:
 
 \begin{code}
 mkPredTy :: PredType -> Type
-mkPredTy pred = SourceTy pred
+mkPredTy pred = PredTy pred
 
 mkPredTys :: ThetaType -> [Type]
-mkPredTys preds = map SourceTy preds
-
-sourceTypeRep :: SourceType -> Type
--- Convert a predicate to its "representation type";
--- the type of evidence for that predicate, which is actually passed at runtime
-sourceTypeRep (IParam n ty)     = ty
-sourceTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
-       -- Note the mkTyConApp; the classTyCon might be a newtype!
-sourceTypeRep (NType  tc tys)   = newTypeRep tc tys
-       -- ToDo: Consider caching this substitution in a NType
-
-isSourceTy :: Type -> Bool
-isSourceTy (NoteTy _ ty)  = isSourceTy ty
-isSourceTy (UsageTy _ ty) = isSourceTy ty
-isSourceTy (SourceTy sty) = True
-isSourceTy _             = False
-
-
-splitNewType_maybe :: Type -> Maybe Type
--- Newtypes that are recursive are reprsented by TyConApp, just
--- as they always were.  Occasionally we want to find their representation type.
--- NB: remember that in this module, non-recursive newtypes are transparent
-
-splitNewType_maybe ty
-  = case splitTyConApp_maybe ty of
-       Just (tc,tys) | isNewTyCon tc -> ASSERT( tys `lengthIs` tyConArity tc )
-                                               -- The assert should hold because repType should
-                                               -- only be applied to *types* (of kind *)
-                                        Just (newTypeRep tc tys)
-       other -> Nothing
-                       
--- A local helper function (not exported)
-newTypeRep new_tycon tys = case newTyConRep new_tycon of
-                            (tvs, rep_ty) -> substTyWith tvs tys rep_ty
+mkPredTys preds = map PredTy preds
+
+predTypeRep :: PredType -> Type
+-- Convert a PredType to its "representation type";
+-- the post-type-checking type used by all the Core passes of GHC.
+-- Unwraps only the outermost level; for example, the result might
+-- be a newtype application
+predTypeRep (IParam _ ty)     = ty
+predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
+       -- Result might be a newtype application, but the consumer will
+       -- look through that too if necessary
+\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)
+  | isNewTyCon 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
 \end{code}
 
 
@@ -675,27 +576,13 @@ newTypeRep new_tycon tys = case newTyConRep new_tycon of
 typeKind :: Type -> Kind
 
 typeKind (TyVarTy tyvar)       = tyVarKind tyvar
-typeKind (TyConApp tycon tys)  = foldr (\_ k -> funResultTy k) (tyConKind tycon) tys
+typeKind (TyConApp tycon tys)  = foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
 typeKind (NoteTy _ ty)         = typeKind ty
-typeKind (SourceTy _)          = liftedTypeKind -- Predicates are always 
+typeKind (PredTy _)            = liftedTypeKind -- Predicates are always 
                                                 -- represented by lifted types
-typeKind (AppTy fun arg)       = funResultTy (typeKind fun)
-
-typeKind (FunTy arg res)       = fix_up (typeKind res)
-                               where
-                                 fix_up (TyConApp tycon _) |  tycon == typeCon
-                                                           || tycon == openKindCon = liftedTypeKind
-                                 fix_up (NoteTy _ kind) = fix_up kind
-                                 fix_up kind            = kind
-               -- The basic story is 
-               --      typeKind (FunTy arg res) = typeKind res
-               -- But a function is lifted regardless of its result type
-               -- Hence the strange fix-up.
-               -- Note that 'res', being the result of a FunTy, can't have 
-               -- a strange kind like (*->*).
-
+typeKind (AppTy fun arg)       = kindFunResult (typeKind fun)
+typeKind (FunTy arg res)       = liftedTypeKind
 typeKind (ForAllTy tv ty)      = typeKind ty
-typeKind (UsageTy _ ty)         = typeKind ty  -- we don't have separate kinds for ann/unann
 \end{code}
 
 
@@ -704,29 +591,24 @@ typeKind (UsageTy _ ty)         = typeKind ty  -- we don't have separate kinds f
                ~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
 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 (NoteTy (SynNote ty1) ty2)        = tyVarsOfType ty1
-tyVarsOfType (SourceTy sty)            = tyVarsOfSourceType sty
+tyVarsOfType (PredTy sty)              = tyVarsOfPred sty
 tyVarsOfType (FunTy arg res)           = tyVarsOfType arg `unionVarSet` tyVarsOfType res
 tyVarsOfType (AppTy fun arg)           = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
-tyVarsOfType (ForAllTy tyvar ty)       = tyVarsOfType ty `minusVarSet` unitVarSet tyvar
-tyVarsOfType (UsageTy u ty)            = tyVarsOfType u `unionVarSet` tyVarsOfType ty
+tyVarsOfType (ForAllTy tyvar ty)       = delVarSet (tyVarsOfType ty) tyvar
 
 tyVarsOfTypes :: [Type] -> TyVarSet
 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
 
 tyVarsOfPred :: PredType -> TyVarSet
-tyVarsOfPred = tyVarsOfSourceType      -- Just a subtype
-
-tyVarsOfSourceType :: SourceType -> TyVarSet
-tyVarsOfSourceType (IParam n ty)     = tyVarsOfType ty
-tyVarsOfSourceType (ClassP clas tys) = tyVarsOfTypes tys
-tyVarsOfSourceType (NType tc tys)    = tyVarsOfTypes tys
+tyVarsOfPred (IParam _ ty)  = tyVarsOfType ty
+tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
 
 tyVarsOfTheta :: ThetaType -> TyVarSet
-tyVarsOfTheta = foldr (unionVarSet . tyVarsOfSourceType) emptyVarSet
+tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
 
 -- Add a Note with the free tyvars to the top of the type
 addFreeTyVars :: Type -> Type
@@ -734,29 +616,6 @@ addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
 addFreeTyVars ty                            = NoteTy (FTVNote (tyVarsOfType ty)) ty
 \end{code}
 
-Usage annotations of a type
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Get a list of usage annotations of a type, *in left-to-right pre-order*.
-
-\begin{code}
-usageAnnOfType :: Type -> [Type]
-usageAnnOfType ty
-  = goS ty
-  where
-    goT (TyVarTy _)       = []
-    goT (AppTy ty1 ty2)   = goT ty1 ++ goT ty2
-    goT (TyConApp tc tys) = concatMap goT tys
-    goT (FunTy sty1 sty2) = goS sty1 ++ goS sty2
-    goT (ForAllTy mv ty)  = goT ty
-    goT (SourceTy p)      = goT (sourceTypeRep p)
-    goT ty@(UsageTy _ _)  = pprPanic "usageAnnOfType: unexpected usage:" (pprType ty)
-    goT (NoteTy note ty)  = goT ty
-
-    goS sty = case splitUTy sty of
-                (u,tty) -> u : goT tty
-\end{code}
-
 
 %************************************************************************
 %*                                                                     *
@@ -773,14 +632,11 @@ It doesn't change the uniques at all, just the print names.
 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 tidyTyVarBndr (tidy_env, subst) tyvar
   = case tidyOccName tidy_env (getOccName name) of
-      (tidy', occ') ->         -- New occname reqd
-                       ((tidy', subst'), tyvar')
+      (tidy', occ') ->         ((tidy', subst'), tyvar')
                    where
                        subst' = extendVarEnv subst tyvar tyvar'
                        tyvar' = setTyVarName tyvar name'
-                       name'  = mkLocalName (getUnique name) occ' noSrcLoc
-                               -- Note: make a *user* tyvar, so it printes nicely
-                               -- Could extract src loc, but no need.
+                       name'  = tidyNameOcc name occ'
   where
     name = tyVarName tyvar
 
@@ -809,26 +665,20 @@ tidyType env@(tidy_env, subst) ty
     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 (SourceTy sty)      = SourceTy (tidySourceType env sty)
+    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)
     go (ForAllTy tv ty)            = ForAllTy tvp $! (tidyType envp ty)
                              where
                                (envp, tvp) = tidyTyVarBndr env tv
-    go (UsageTy u ty)      = (UsageTy $! (go u)) $! (go ty)
 
-    go_note (SynNote ty)        = SynNote $! (go ty)
     go_note note@(FTVNote ftvs) = note -- No need to tidy the free tyvars
 
 tidyTypes env tys = map (tidyType env) tys
 
-tidyPred :: TidyEnv -> SourceType -> SourceType
-tidyPred = tidySourceType
-
-tidySourceType :: TidyEnv -> SourceType -> SourceType
-tidySourceType env (IParam n ty)     = IParam n (tidyType env ty)
-tidySourceType env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
-tidySourceType env (NType tc tys)    = NType  tc   (tidyTypes env tys)
+tidyPred :: TidyEnv -> PredType -> PredType
+tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
+tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
 \end{code}
 
 
@@ -850,6 +700,43 @@ tidyTopType ty = tidyType emptyTidyEnv ty
 \end{code}
 
 
+%************************************************************************
+%*                                                                     *
+               Tidying Kinds
+%*                                                                     *
+%************************************************************************
+
+We use a grevious hack for tidying KindVars.  A TidyEnv contains
+a (VarEnv Var) substitution, to express the renaming; but
+KindVars are not Vars.  The Right Thing ultimately is to make them
+into Vars (and perhaps make Kinds into Types), but I just do a hack
+here: I make up a TyVar just to remember the new OccName for the
+renamed KindVar
+
+\begin{code}
+tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
+tidyKind env@(tidy_env, subst) (KindVar kvar)
+  | Just tv <- lookupVarEnv_Directly subst uniq
+  = (env, KindVar (setKindVarOcc kvar (getOccName tv)))
+  | otherwise
+  = ((tidy', subst'), KindVar kvar')
+  where
+    uniq = kindVarUniq kvar
+    (tidy', occ') = tidyOccName tidy_env (kindVarOcc kvar)
+    kvar'   = setKindVarOcc kvar occ'
+    fake_tv = mkTyVar tv_name (panic "tidyKind:fake tv kind")
+    tv_name = mkInternalName uniq occ' noSrcLoc
+    subst'  = extendVarEnv subst fake_tv fake_tv
+
+tidyKind env (FunKind k1 k2) 
+  = (env2, FunKind k1' k2')
+  where
+    (env1, k1') = tidyKind env  k1
+    (env2, k2') = tidyKind env1 k2
+
+tidyKind env k = (env, k)      -- Atomic kinds
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
@@ -865,12 +752,10 @@ isUnLiftedType :: Type -> Bool
        -- They are pretty bogus types, mind you.  It would be better never to
        -- construct them
 
-isUnLiftedType (ForAllTy tv ty) = isUnLiftedType ty
-isUnLiftedType (NoteTy _ ty)   = isUnLiftedType ty
-isUnLiftedType (TyConApp tc _)  = isUnLiftedTyCon tc
-isUnLiftedType (UsageTy _ ty)  = isUnLiftedType ty
-isUnLiftedType (SourceTy _)    = False         -- All source types are lifted
-isUnLiftedType other           = False 
+isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
+isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
+isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
+isUnLiftedType other            = False        
 
 isUnboxedTupleType :: Type -> Bool
 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
@@ -893,16 +778,18 @@ 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 (ForAllTy tv ty)          = isStrictType ty
-isStrictType (NoteTy _ ty)             = isStrictType ty
-isStrictType (TyConApp tc _)           = isUnLiftedTyCon tc
-isStrictType (UsageTy _ ty)            = isStrictType ty
-isStrictType (SourceTy (ClassP clas _)) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
+isStrictType (PredTy pred)     = isStrictPred pred
+isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
+isStrictType (ForAllTy tv ty)  = isStrictType ty
+isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
+isStrictType other            = False  
+
+isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
+isStrictPred other          = 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
        --  poking the dictionary component, which is wrong.]
-isStrictType other                     = False 
 \end{code}
 
 \begin{code}
@@ -929,63 +816,417 @@ 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 (SourceTy p)     = seqPred p
+seqType (PredTy p)       = seqPred p
 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
-seqType (UsageTy u ty)   = seqType u `seq` seqType ty
 
 seqTypes :: [Type] -> ()
 seqTypes []       = ()
 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
 
 seqNote :: TyNote -> ()
-seqNote (SynNote ty)  = seqType ty
 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
 
-seqPred :: SourceType -> ()
+seqPred :: PredType -> ()
 seqPred (ClassP c tys) = c  `seq` seqTypes tys
-seqPred (NType tc tys) = tc `seq` seqTypes tys
 seqPred (IParam n ty)  = n  `seq` seqType ty
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Equality on types}
+               Equality for Core types 
+       (We don't use instances so that we know where it happens)
 %*                                                                     *
 %************************************************************************
 
-Comparison; don't use instances so that we know where it happens.
-Look through newtypes but not usage types.
+Note that eqType works right even for partial applications of newtypes.
+See Note [Newtype eta] in TyCon.lhs
 
 \begin{code}
-eqType t1 t2 = eq_ty emptyVarEnv t1 t2
-eqKind  = eqType       -- No worries about looking 
-eqUsage = eqType       -- through source types for these two
-
--- Look through Notes
-eq_ty env (NoteTy _ t1)       t2                 = eq_ty env t1 t2
-eq_ty env t1                 (NoteTy _ t2)       = eq_ty env t1 t2
-
--- Look through SourceTy.  This is where the looping danger comes from
-eq_ty env (SourceTy sty1)     t2                 = eq_ty env (sourceTypeRep sty1) t2
-eq_ty env t1                 (SourceTy sty2)     = eq_ty env t1 (sourceTypeRep sty2)
-
--- The rest is plain sailing
-eq_ty env (TyVarTy tv1)       (TyVarTy tv2)       = case lookupVarEnv env tv1 of
-                                                         Just tv1a -> tv1a == tv2
-                                                         Nothing   -> tv1  == tv2
-eq_ty env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   
-       | tv1 == tv2                              = eq_ty (delVarEnv env tv1)        t1 t2
-       | otherwise                               = eq_ty (extendVarEnv env tv1 tv2) t1 t2
-eq_ty env (AppTy s1 t1)       (AppTy s2 t2)       = (eq_ty env s1 s2) && (eq_ty env t1 t2)
-eq_ty env (FunTy s1 t1)       (FunTy s2 t2)       = (eq_ty env s1 s2) && (eq_ty env t1 t2)
-eq_ty env (UsageTy _ t1)      (UsageTy _ t2)     = eq_ty env t1 t2
-eq_ty env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 == tc2) && (eq_tys env tys1 tys2)
-eq_ty env t1                  t2                 = False
-
-eq_tys env []        []        = True
-eq_tys env (t1:tys1) (t2:tys2) = (eq_ty env t1 t2) && (eq_tys env tys1 tys2)
-eq_tys env tys1      tys2      = False
+coreEqType :: Type -> Type -> Bool
+coreEqType t1 t2
+  = eq rn_env t1 t2
+  where
+    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
+
+    eq env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
+    eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
+    eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
+    eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
+    eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
+       | tc1 == tc2, all2 (eq env) tys1 tys2 = True
+                       -- The lengths should be equal because
+                       -- the two types have the same kind
+       -- NB: if the type constructors differ that does not 
+       --     necessarily mean that the types aren't equal
+       --     (synonyms, newtypes)
+       -- Even if the type constructors are the same, but the arguments
+       -- differ, the two types could be the same (e.g. if the arg is just
+       -- ignored in the RHS).  In both these cases we fall through to an 
+       -- attempt to expand one side or the other.
+
+       -- Now deal with newtypes, synonyms, pred-tys
+    eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
+                | Just t2' <- coreView t2 = eq env t1 t2'
+
+       -- Fall through case; not equal!
+    eq env t1 t2 = False
 \end{code}
 
+
+%************************************************************************
+%*                                                                     *
+               Comparision for source types 
+       (We don't use instances so that we know where it happens)
+%*                                                                     *
+%************************************************************************
+
+Note that 
+       tcEqType, tcCmpType 
+do *not* look through newtypes, PredTypes
+
+\begin{code}
+tcEqType :: Type -> Type -> Bool
+tcEqType t1 t2 = isEqual $ cmpType t1 t2
+
+tcEqTypes :: [Type] -> [Type] -> Bool
+tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
+
+tcCmpType :: Type -> Type -> Ordering
+tcCmpType t1 t2 = cmpType t1 t2
+
+tcCmpTypes :: [Type] -> [Type] -> Ordering
+tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
+
+tcEqPred :: PredType -> PredType -> Bool
+tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
+
+tcCmpPred :: PredType -> PredType -> Ordering
+tcCmpPred p1 p2 = cmpPred p1 p2
+
+tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
+tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
+\end{code}
+
+Now here comes the real worker
+
+\begin{code}
+cmpType :: Type -> Type -> Ordering
+cmpType t1 t2 = cmpTypeX rn_env t1 t2
+  where
+    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
+
+cmpTypes :: [Type] -> [Type] -> Ordering
+cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
+  where
+    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
+
+cmpPred :: PredType -> PredType -> Ordering
+cmpPred p1 p2 = cmpPredX rn_env p1 p2
+  where
+    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
+
+cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
+cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
+                  | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
+
+cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
+cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
+cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
+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 env (PredTy _)   t2           = GT
+
+cmpTypeX env _ _ = LT
+
+-------------
+cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
+cmpTypesX env []        []        = EQ
+cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
+cmpTypesX env []        tys       = LT
+cmpTypesX env ty        []        = 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
+cmpPredX env (IParam _ _)     (ClassP _ _)     = LT
+cmpPredX env (ClassP _ _)     (IParam _ _)     = GT
+\end{code}
+
+PredTypes are used as a FM key in TcSimplify, 
+so we take the easy path and make them an instance of Ord
+
+\begin{code}
+instance Eq  PredType where { (==)    = tcEqPred }
+instance Ord PredType where { compare = tcCmpPred }
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+               Type substitutions
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+data TvSubst           
+  = TvSubst InScopeSet         -- The in-scope type variables
+           TvSubstEnv  -- The substitution itself
+                       -- See Note [Apply Once]
+
+{- ----------------------------------------------------------
+               Note [Apply Once]
+
+We use TvSubsts to instantiate things, and we might instantiate
+       forall a b. ty
+\with the types
+       [a, b], or [b, a].
+So the substition might go [a->b, b->a].  A similar situation arises in Core
+when we find a beta redex like
+       (/\ a /\ b -> e) b a
+Then we also end up with a substition that permutes type variables. Other
+variations happen to; for example [a -> (a, b)].  
+
+       ***************************************************
+       *** So a TvSubst must be applied precisely once ***
+       ***************************************************
+
+A TvSubst is not idempotent, but, unlike the non-idempotent substitution
+we use during unifications, it must not be repeatedly applied.
+-------------------------------------------------------------- -}
+
+
+type TvSubstEnv = TyVarEnv Type
+       -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
+       -- invariant discussed in Note [Apply Once]), and also independently
+       -- in the middle of matching, and unification (see Types.Unify)
+       -- So you have to look at the context to know if it's idempotent or
+       -- apply-once or whatever
+emptyTvSubstEnv :: TvSubstEnv
+emptyTvSubstEnv = emptyVarEnv
+
+composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
+-- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
+-- It assumes that both are idempotent
+-- Typically, env1 is the refinement to a base substitution env2
+composeTvSubst in_scope env1 env2
+  = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
+       -- First apply env1 to the range of env2
+       -- Then combine the two, making sure that env1 loses if
+       -- both bind the same variable; that's why env1 is the
+       --  *left* argument to plusVarEnv, because the right arg wins
+  where
+    subst1 = TvSubst in_scope env1
+
+emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
+
+isEmptyTvSubst :: TvSubst -> Bool
+isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
+
+mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
+mkTvSubst = TvSubst
+
+getTvSubstEnv :: TvSubst -> TvSubstEnv
+getTvSubstEnv (TvSubst _ env) = env
+
+getTvInScope :: TvSubst -> InScopeSet
+getTvInScope (TvSubst in_scope _) = in_scope
+
+isInScope :: Var -> TvSubst -> Bool
+isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
+
+notElemTvSubst :: TyVar -> TvSubst -> Bool
+notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
+
+setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
+setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
+
+extendTvInScope :: TvSubst -> [Var] -> TvSubst
+extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
+
+extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
+extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
+
+extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
+extendTvSubstList (TvSubst in_scope env) tvs tys 
+  = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
+
+-- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
+-- the types given; but it's just a thunk so with a bit of luck
+-- it'll never be evaluated
+
+mkOpenTvSubst :: TvSubstEnv -> TvSubst
+mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
+
+zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
+zipOpenTvSubst tyvars tys 
+#ifdef DEBUG
+  | 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.
+-- Here we expect that the free vars of the range of the
+-- substitution will be empty.
+mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
+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
+  | otherwise
+#endif
+  = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
+
+zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
+zipTyEnv tyvars tys
+#ifdef DEBUG
+  | 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 []       []       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 
+       --      ty == TyVarTy tv
+       -- (a not-uncommon case) in which case the substitution was dropped.
+       -- But the type-tidier changes the print-name of a type variable without
+       -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had 
+       -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
+       -- And it happened that t was the type variable of the class.  Post-tiding, 
+       -- it got turned into {Foo t2}.  The ext-core printer expanded this using
+       -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
+       -- and so generated a rep type mentioning t not t2.  
+       --
+       -- Simplest fix is to nuke the "optimisation"
+zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
+-- zip_ty_env _ _ env = env
+
+instance Outputable TvSubst where
+  ppr (TvSubst ins env) 
+    = sep[ ptext SLIT("<TvSubst"),
+          nest 2 (ptext SLIT("In scope:") <+> ppr ins), 
+          nest 2 (ptext SLIT("Env:") <+> ppr env) ]
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+               Performing type substitutions
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+substTyWith :: [TyVar] -> [Type] -> Type -> Type
+substTyWith tvs tys = ASSERT( length tvs == length tys )
+                     substTy (zipOpenTvSubst tvs tys)
+
+substTy :: TvSubst -> Type  -> Type
+substTy subst ty | isEmptyTvSubst subst = ty
+                | otherwise            = subst_ty subst ty
+
+substTys :: TvSubst -> [Type] -> [Type]
+substTys subst tys | isEmptyTvSubst subst = tys
+                  | otherwise            = map (subst_ty subst) tys
+
+substTheta :: TvSubst -> ThetaType -> ThetaType
+substTheta subst theta
+  | isEmptyTvSubst subst = theta
+  | otherwise           = map (substPred subst) theta
+
+substPred :: TvSubst -> PredType -> PredType
+substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
+substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
+
+deShadowTy :: TyVarSet -> Type -> Type -- Remove any nested binders mentioning tvs
+deShadowTy tvs ty 
+  = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
+  where
+    in_scope = mkInScopeSet tvs
+
+-- Note that the in_scope set is poked only if we hit a forall
+-- so it may often never be fully computed 
+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 (NoteTy (FTVNote _) ty2)    = go ty2            -- Discard the free tyvar note
+
+    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 tv
+  = case lookupTyVar subst tv of
+       Nothing  -> TyVarTy tv
+               Just ty' -> ty' -- See Note [Apply Once]
+
+lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
+lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv
+
+substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar) 
+substTyVarBndr subst@(TvSubst in_scope env) old_var
+  | old_var == new_var -- No need to clone
+                       -- But we *must* zap any current substitution for the variable.
+                       --  For example:
+                       --      (\x.e) with id_subst = [x |-> e']
+                       -- Here we must simply zap the substitution for x
+                       --
+                       -- The new_id isn't cloned, but it may have a different type
+                       -- etc, so we must return it, not the old id
+  = (TvSubst (in_scope `extendInScopeSet` new_var) 
+            (delVarEnv env old_var),
+     new_var)
+
+  | otherwise  -- The new binder is in scope so
+               -- we'd better rename it away from the in-scope variables
+               -- Extending the substitution to do this renaming also
+               -- has the (correct) effect of discarding any existing
+               -- substitution for that variable
+  = (TvSubst (in_scope `extendInScopeSet` new_var) 
+            (extendVarEnv env old_var (TyVarTy new_var)),
+     new_var)
+  where
+    new_var = uniqAway in_scope old_var
+       -- The uniqAway part makes sure the new variable is not already in scope
+\end{code}