[project @ 2002-09-06 14:40:28 by simonmar]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index b1e52a9..531709a 100644 (file)
@@ -17,7 +17,7 @@ is the principal client.
 module TcType (
   --------------------------------
   -- Types 
-  TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType, 
+  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
   TcTyVar, TcTyVarSet, TcKind, 
 
   --------------------------------
@@ -27,12 +27,12 @@ module TcType (
 
   --------------------------------
   -- Builders
-  mkRhoTy, mkSigmaTy, 
+  mkPhiTy, mkSigmaTy, 
 
   --------------------------------
   -- Splitters  
   -- These are important because they do not look through newtypes
-  tcSplitForAllTys, tcSplitRhoTy, 
+  tcSplitForAllTys, tcSplitPhiTy, 
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
@@ -41,15 +41,16 @@ module TcType (
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
-  tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
+  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
   isSigmaTy, isOverloadedTy, 
   isDoubleTy, isFloatTy, isIntTy,
-  isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, 
+  isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
   isTauTy, tcIsTyVarTy, tcIsForAllTy,
+  allDistinctTyVars,
 
   ---------------------------------
   -- Misc type manipulators
-  hoistForAllTys, deNoteType,
+  deNoteType, 
   namesOfType, namesOfDFunHead,
   getDFunTyKey,
 
@@ -59,7 +60,7 @@ module TcType (
   isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
   mkDictTy, tcSplitPredTy_maybe, predTyUnique,
   isDictTy, tcSplitDFunTy, predTyUnique, 
-  mkClassPred, inheritablePred, isIPPred, mkPredName, 
+  mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
 
   ---------------------------------
   -- Foreign import and export
@@ -74,7 +75,6 @@ module TcType (
   ---------------------------------
   -- Unifier and matcher  
   unifyTysX, unifyTyListsX, unifyExtendTysX,
-  allDistinctTyVars,
   matchTy, matchTys, match,
 
   --------------------------------
@@ -82,19 +82,17 @@ module TcType (
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
-  isTypeKind,
-
-  IPName, ipNameName, mapIPName,
+  isTypeKind, isAnyTypeKind,
 
   Type, SourceType(..), PredType, ThetaType, 
   mkForAllTy, mkForAllTys, 
   mkFunTy, mkFunTys, zipFunTys, 
-  mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+  mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, 
 
   isUnLiftedType,      -- Source types are always lifted
   isUnboxedTupleType,  -- Ditto
-  isPrimitiveType,
+  isPrimitiveType, isTyVarTy,
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
@@ -110,22 +108,20 @@ import {-# SOURCE #-} PprType( pprType )
 
 -- friends:
 import TypeRep         ( Type(..), TyNote(..), funTyCon )  -- friend
-import Type            ( mkUTyM, unUTy )       -- Used locally
 
 import Type            (       -- Re-exports
                          tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-                         IPName, Kind, Type, SourceType(..), PredType, ThetaType, 
+                         Kind, Type, SourceType(..), PredType, ThetaType, 
                          unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
-                         mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
-                         mkFunTy, mkFunTys, zipFunTys, 
-                         mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+                         mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
+                         mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
+                         mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
                          mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
                          isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
                          splitNewType_maybe, splitTyConApp_maybe,
                          tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
                          tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
-                         hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind,
-                         ipNameName, mapIPName
+                         hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
                        )
 import TyCon           ( TyCon, isUnLiftedTyCon )
 import Class           ( classHasFDs, Class )
@@ -136,11 +132,12 @@ import VarSet
 
 -- others:
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name            ( Name, NamedThing(..), mkLocalName, getSrcLoc )
+import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import OccName         ( OccName, mkDictOcc )
 import NameSet
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn      ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
+import BasicTypes      ( IPName(..), ipNameName )
 import Unique          ( Unique, Uniquable(..) )
 import SrcLoc          ( SrcLoc )
 import Util            ( cmpList, thenCmp, equalLength )
@@ -158,7 +155,7 @@ import Outputable
 The type checker divides the generic Type world into the 
 following more structured beasts:
 
-sigma ::= forall tyvars. theta => phi
+sigma ::= forall tyvars. phi
        -- A sigma type is a qualified type
        --
        -- Note that even if 'tyvars' is empty, theta
@@ -169,7 +166,9 @@ sigma ::= forall tyvars. theta => phi
        -- A 'phi' type has no foralls to the right of
        -- an arrow
 
-phi ::= sigma -> phi
+phi :: theta => rho
+
+rho ::= sigma -> rho
      |  tau
 
 -- A 'tau' type has no quantification anywhere
@@ -185,7 +184,7 @@ tau ::= tyvar
 
 \begin{code}
 type SigmaType = Type
-type PhiType   = Type
+type RhoType   = Type
 type TauType   = Type
 \end{code}
 
@@ -202,7 +201,7 @@ type TcType = Type          -- A TcType can have mutable type variables
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
 type TcSigmaType    = TcType
-type TcPhiType      = TcType
+type TcRhoType      = TcType
 type TcTauType      = TcType
 type TcKind         = TcType
 \end{code}
@@ -253,7 +252,9 @@ isUserTyVar tv = case mutTyVarDetails tv of
 
 isSkolemTyVar :: TcTyVar -> Bool
 isSkolemTyVar tv = case mutTyVarDetails tv of
-                     SigTv -> True
+                     SigTv  -> True
+                     ClsTv  -> True
+                     InstTv -> True
                      oteher -> False
 
 isHoleTyVar :: TcTyVar -> Bool
@@ -288,12 +289,10 @@ tyVarBindingInfo tv
 %************************************************************************
 
 \begin{code}
-mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
-
-mkRhoTy :: [SourceType] -> Type -> Type
-mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
-                   foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
+mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
 
+mkPhiTy :: [SourceType] -> Type -> Type
+mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
 \end{code}
 
 
@@ -307,7 +306,6 @@ isTauTy (AppTy a b)  = isTauTy a && isTauTy b
 isTauTy (FunTy a b)     = isTauTy a && isTauTy b
 isTauTy (SourceTy p)    = True         -- Don't look through source types
 isTauTy (NoteTy _ ty)   = isTauTy ty
-isTauTy (UsageTy _ ty)   = isTauTy ty
 isTauTy other           = False
 \end{code}
 
@@ -320,7 +318,6 @@ getDFunTyKey (AppTy fun _)               = getDFunTyKey fun
 getDFunTyKey (NoteTy _ t)           = getDFunTyKey t
 getDFunTyKey (FunTy arg _)          = getOccName funTyCon
 getDFunTyKey (ForAllTy _ t)         = getDFunTyKey t
-getDFunTyKey (UsageTy _ t)          = getDFunTyKey t
 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc   -- Newtypes are quite reasonable
 getDFunTyKey ty                             = pprPanic "getDFunTyKey" (pprType ty)
 -- SourceTy shouldn't happen
@@ -347,26 +344,23 @@ tcSplitForAllTys ty = split ty ty []
    where
      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
      split orig_ty (NoteTy n  ty)   tvs = split orig_ty ty tvs
-     split orig_ty (UsageTy _ ty)   tvs = split orig_ty ty tvs
      split orig_ty t               tvs = (reverse tvs, orig_ty)
 
 tcIsForAllTy (ForAllTy tv ty) = True
 tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
-tcIsForAllTy (UsageTy n ty)   = tcIsForAllTy ty
 tcIsForAllTy t               = False
 
-tcSplitRhoTy :: Type -> ([PredType], Type)
-tcSplitRhoTy ty = split ty ty []
+tcSplitPhiTy :: Type -> ([PredType], Type)
+tcSplitPhiTy ty = split ty ty []
  where
   split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
                                        Just p  -> split res res (p:ts)
                                        Nothing -> (reverse ts, orig_ty)
   split orig_ty (NoteTy n ty)  ts = split orig_ty ty ts
-  split orig_ty (UsageTy _ ty)  ts = split orig_ty ty ts
   split orig_ty ty             ts = (reverse ts, orig_ty)
 
 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
-                       (tvs, rho) -> case tcSplitRhoTy rho of
+                       (tvs, rho) -> case tcSplitPhiTy rho of
                                        (theta, tau) -> (tvs, theta, tau)
 
 tcTyConAppTyCon :: Type -> TyCon
@@ -381,12 +375,11 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
                        Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 
 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
--- Newtypes are opaque, so they may be split
 tcSplitTyConApp_maybe (TyConApp tc tys)        = Just (tc, tys)
-tcSplitTyConApp_maybe (FunTy arg res)          = Just (funTyCon, [unUTy arg,unUTy res])
+tcSplitTyConApp_maybe (FunTy arg res)          = Just (funTyCon, [arg,res])
 tcSplitTyConApp_maybe (NoteTy n ty)            = tcSplitTyConApp_maybe ty
-tcSplitTyConApp_maybe (UsageTy _ ty)           = tcSplitTyConApp_maybe ty
 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
+       -- Newtypes are opaque, so they may be split
        -- However, predicates are not treated
        -- as tycon applications by the type checker
 tcSplitTyConApp_maybe other                    = Nothing
@@ -401,7 +394,6 @@ tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
 tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
 tcSplitFunTy_maybe (NoteTy n ty)    = tcSplitFunTy_maybe ty
-tcSplitFunTy_maybe (UsageTy _ ty)   = tcSplitFunTy_maybe ty
 tcSplitFunTy_maybe other           = Nothing
 
 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
@@ -409,10 +401,9 @@ tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 
 
 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
-tcSplitAppTy_maybe (FunTy ty1 ty2)          = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
+tcSplitAppTy_maybe (FunTy ty1 ty2)          = Just (TyConApp funTyCon [ty1], ty2)
 tcSplitAppTy_maybe (AppTy ty1 ty2)          = Just (ty1, ty2)
 tcSplitAppTy_maybe (NoteTy n ty)            = tcSplitAppTy_maybe ty
-tcSplitAppTy_maybe (UsageTy _ ty)           = tcSplitAppTy_maybe ty
 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
        --- Don't forget that newtype!
 tcSplitAppTy_maybe (TyConApp tc tys)        = tc_split_app tc tys
@@ -431,7 +422,6 @@ tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
 tcGetTyVar_maybe :: Type -> Maybe TyVar
 tcGetTyVar_maybe (TyVarTy tv)  = Just tv
 tcGetTyVar_maybe (NoteTy _ t)  = tcGetTyVar_maybe t
-tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
 tcGetTyVar_maybe other         = Nothing
 
 tcGetTyVar :: String -> Type -> TyVar
@@ -457,7 +447,6 @@ tcSplitMethodTy ty = split ty
                            Just p  -> (p, res)
                            Nothing -> panic "splitMethodTy"
   split (NoteTy n ty)  = split ty
-  split (UsageTy _ ty)  = split ty
   split _               = panic "splitMethodTy"
 
 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
@@ -468,6 +457,31 @@ tcSplitDFunTy ty
     (tvs, theta, clas, tys) }}
 \end{code}
 
+(allDistinctTyVars tys tvs) = True 
+       iff 
+all the types tys are type variables, 
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables.  For example, if the type sig is
+       f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't 
+       (a) been unified with a non-tyvar type
+       (b) been unified with each other (all distinct)
+       (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
+
+allDistinctTyVars []       acc
+  = True
+allDistinctTyVars (ty:tys) acc 
+  = case tcGetTyVar_maybe ty of
+       Nothing                       -> False  -- (a)
+       Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
+               | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}    
+
 
 %************************************************************************
 %*                                                                     *
@@ -485,14 +499,12 @@ isPred (NType _ _)  = False
 
 isPredTy :: Type -> Bool
 isPredTy (NoteTy _ ty)  = isPredTy ty
-isPredTy (UsageTy _ ty) = isPredTy ty
 isPredTy (SourceTy sty) = isPred sty
 isPredTy _             = False
 
 tcSplitPredTy_maybe :: Type -> Maybe PredType
    -- Returns Just for predicates only
 tcSplitPredTy_maybe (NoteTy _ ty)          = tcSplitPredTy_maybe ty
-tcSplitPredTy_maybe (UsageTy _ ty)         = tcSplitPredTy_maybe ty
 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
 tcSplitPredTy_maybe other                  = Nothing
        
@@ -507,16 +519,15 @@ predHasFDs (IParam _ _)   = True
 predHasFDs (ClassP cls _) = classHasFDs cls
 
 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
-mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
-mkPredName uniq loc (IParam ip ty)   = mkLocalName uniq (getOccName (ipNameName ip)) loc
+mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
+mkPredName uniq loc (IParam ip ty)   = mkInternalName uniq (getOccName (ipNameName ip)) loc
 \end{code}
 
 
 --------------------- Dictionary types ---------------------------------
 
 \begin{code}
-mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
-                       ClassP clas tys
+mkClassPred clas tys = ClassP clas tys
 
 isClassPred :: SourceType -> Bool
 isClassPred (ClassP clas tys) = True
@@ -533,13 +544,11 @@ getClassPredTys :: PredType -> (Class, [Type])
 getClassPredTys (ClassP clas tys) = (clas, tys)
 
 mkDictTy :: Class -> [Type] -> Type
-mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
-                    mkPredTy (ClassP clas tys)
+mkDictTy clas tys = mkPredTy (ClassP clas tys)
 
 isDictTy :: Type -> Bool
 isDictTy (SourceTy p)   = isClassPred p
 isDictTy (NoteTy _ ty) = isDictTy ty
-isDictTy (UsageTy _ ty) = isDictTy ty
 isDictTy other         = False
 \end{code}
 
@@ -550,7 +559,7 @@ isIPPred :: SourceType -> Bool
 isIPPred (IParam _ _) = True
 isIPPred other       = False
 
-inheritablePred :: PredType -> Bool
+isInheritablePred :: PredType -> Bool
 -- Can be inherited by a context.  For example, consider
 --     f x = let g y = (?v, y+x)
 --           in (g 3 with ?v = 8, 
@@ -559,8 +568,12 @@ inheritablePred :: PredType -> Bool
 --     g :: (?v :: a) => a -> a
 -- but it doesn't need to be quantified over the Num a dictionary
 -- which can be free in g's rhs, and shared by both calls to g
-inheritablePred (ClassP _ _) = True
-inheritablePred other       = False
+isInheritablePred (ClassP _ _) = True
+isInheritablePred other             = False
+
+isLinearPred :: TcPredType -> Bool
+isLinearPred (IParam (Linear n) _) = True
+isLinearPred other                = False
 \end{code}
 
 
@@ -577,6 +590,9 @@ But ignoring usage types
 tcEqType :: Type -> Type -> Bool
 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
 
+tcEqTypes :: [Type] -> [Type] -> Bool
+tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
+
 tcEqPred :: PredType -> PredType -> Bool
 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
 
@@ -596,11 +612,9 @@ cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
   -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
   -- we in effect substitute tv2 for tv1 in t1 before continuing
 
-    -- Look through NoteTy and UsageTy
+    -- Look through NoteTy
 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
-cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
-cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
 
     -- Deal with equal constructors
 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
@@ -673,21 +687,18 @@ isSigmaTy :: Type -> Bool
 isSigmaTy (ForAllTy tyvar ty) = True
 isSigmaTy (FunTy a b)        = isPredTy a
 isSigmaTy (NoteTy n ty)              = isSigmaTy ty
-isSigmaTy (UsageTy _ ty)      = isSigmaTy ty
 isSigmaTy _                  = False
 
 isOverloadedTy :: Type -> Bool
 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 isOverloadedTy (FunTy a b)        = isPredTy a
 isOverloadedTy (NoteTy n ty)      = isOverloadedTy ty
-isOverloadedTy (UsageTy _ ty)     = isOverloadedTy ty
 isOverloadedTy _                  = False
 \end{code}
 
 \begin{code}
 isFloatTy      = is_tc floatTyConKey
 isDoubleTy     = is_tc doubleTyConKey
-isForeignPtrTy = is_tc foreignPtrTyConKey
 isIntegerTy    = is_tc integerTyConKey
 isIntTy        = is_tc intTyConKey
 isAddrTy       = is_tc addrTyConKey
@@ -709,24 +720,6 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 %************************************************************************
 
 \begin{code}
-hoistForAllTys :: Type -> Type
-       -- Move all the foralls to the top
-       -- e.g.  T -> forall a. a  ==>   forall a. T -> a
-        -- Careful: LOSES USAGE ANNOTATIONS!
-hoistForAllTys ty
-  = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
-  where
-    hoist :: Type -> ([TyVar], Type)
-    hoist ty = case tcSplitFunTys    ty  of { (args, res) -> 
-              case tcSplitForAllTys res of {
-                 ([], body)  -> ([], ty) ;
-                 (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
-                                  (tvs1 ++ tvs2, mkFunTys args body2)
-              }}}
-\end{code}
-
-
-\begin{code}
 deNoteType :: Type -> Type
        -- Remove synonyms, but not source types
 deNoteType ty@(TyVarTy tyvar)  = ty
@@ -736,7 +729,6 @@ deNoteType (NoteTy _ ty)    = deNoteType ty
 deNoteType (AppTy fun arg)     = AppTy (deNoteType fun) (deNoteType arg)
 deNoteType (FunTy fun arg)     = FunTy (deNoteType fun) (deNoteType arg)
 deNoteType (ForAllTy tv ty)    = ForAllTy tv (deNoteType ty)
-deNoteType (UsageTy u ty)      = UsageTy u (deNoteType ty)
 
 deNoteSourceType :: SourceType -> SourceType
 deNoteSourceType (ClassP c tys)   = ClassP c (map deNoteType tys)
@@ -759,7 +751,6 @@ namesOfType (SourceTy (NType tc tys))       = unitNameSet (getName tc) `unionNameSets`
 namesOfType (FunTy arg res)            = namesOfType arg `unionNameSets` namesOfType res
 namesOfType (AppTy fun arg)            = namesOfType fun `unionNameSets` namesOfType arg
 namesOfType (ForAllTy tyvar ty)                = namesOfType ty `delFromNameSet` getName tyvar
-namesOfType (UsageTy u ty)             = namesOfType u `unionNameSets` namesOfType ty
 
 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
 
@@ -838,8 +829,7 @@ legalFEArgTyCon :: TyCon -> Bool
 -- bytearrays from a _ccall_ / foreign declaration
 -- (or be passed them as arguments in foreign exported functions).
 legalFEArgTyCon tc
-  | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
-                         byteArrayTyConKey, mutableByteArrayTyConKey ] 
+  | getUnique tc `elem` [ byteArrayTyConKey, mutableByteArrayTyConKey ] 
   = False
   -- It's also illegal to make foreign exports that take unboxed
   -- arguments.  The RTS API currently can't invoke such things.  --SDM 7/2000
@@ -849,16 +839,14 @@ legalFEArgTyCon tc
 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
 legalFIResultTyCon dflags tc
   | getUnique tc `elem`
-       [ foreignObjTyConKey, foreignPtrTyConKey,
-         byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
+       [ byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
   | tc == unitTyCon = True
   | otherwise      = marshalableTyCon dflags tc
 
 legalFEResultTyCon :: TyCon -> Bool
 legalFEResultTyCon tc
   | getUnique tc `elem` 
-       [ foreignObjTyConKey, foreignPtrTyConKey,
-         byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
+       [ byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
   | tc == unitTyCon = True
   | otherwise       = boxedMarshalableTyCon tc
 
@@ -881,8 +869,7 @@ boxedMarshalableTyCon tc
                         , word32TyConKey, word64TyConKey
                         , floatTyConKey, doubleTyConKey
                         , addrTyConKey, ptrTyConKey, funPtrTyConKey
-                        , charTyConKey, foreignObjTyConKey
-                        , foreignPtrTyConKey
+                        , charTyConKey
                         , stablePtrTyConKey
                         , byteArrayTyConKey, mutableByteArrayTyConKey
                         , boolTyConKey
@@ -896,38 +883,6 @@ boxedMarshalableTyCon tc
 %*                                                                     *
 %************************************************************************
 
-(allDistinctTyVars tys tvs) = True 
-       iff 
-all the types tys are type variables, 
-distinct from each other and from tvs.
-
-This is useful when checking that unification hasn't unified signature
-type variables.  For example, if the type sig is
-       f :: forall a b. a -> b -> b
-we want to check that 'a' and 'b' havn't 
-       (a) been unified with a non-tyvar type
-       (b) been unified with each other (all distinct)
-       (c) been unified with a variable free in the environment
-
-\begin{code}
-allDistinctTyVars :: [Type] -> TyVarSet -> Bool
-
-allDistinctTyVars []       acc
-  = True
-allDistinctTyVars (ty:tys) acc 
-  = case tcGetTyVar_maybe ty of
-       Nothing                       -> False  -- (a)
-       Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
-               | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
-\end{code}    
-
-
-%************************************************************************
-%*                                                                     *
-\subsection{Unification with an explicit substitution}
-%*                                                                     *
-%************************************************************************
-
 Unify types with an explicit substitution and no monad.
 Ignore usage annotations.
 
@@ -1014,10 +969,6 @@ uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
 #endif
 
-       -- Ignore usages
-uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
-uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
-
        -- Anything else fails
 uTysX ty1 ty2 k subst = Nothing
 
@@ -1038,7 +989,6 @@ uVarX tv1 ty2 k subst@(tmpls, env)
               |  typeKind ty2 `eqKind` tyVarKind tv1
               && occur_check_ok ty2
               ->     -- No kind mismatch nor occur check
-                 UASSERT( not (isUTy ty2) )
                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
 
               | otherwise -> Nothing   -- Fail if kind mis-match or occur check
@@ -1106,8 +1056,15 @@ match (TyVarTy v) ty tmpls k senv
   | v `elemVarSet` tmpls
   =     -- v is a template variable
     case lookupSubstEnv senv v of
-       Nothing -> UASSERT( not (isUTy ty) )
-                   k (extendSubstEnv senv v (DoneTy ty))
+       Nothing | typeKind ty `eqKind` tyVarKind v      
+                       -- We do a kind check, just as in the uVarX above
+                       -- The kind check is needed to avoid bogus matches
+                       -- of   (a b) with (c d), where the kinds don't match
+                       -- An occur check isn't needed when matching.
+               -> k (extendSubstEnv senv v (DoneTy ty))
+
+               | otherwise  -> Nothing -- Fails
+
        Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
                           | otherwise           -> Nothing  -- Fails
 
@@ -1148,9 +1105,6 @@ match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 
-match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
-match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
-
        -- With type synonyms, we have to be careful for the exact
        -- same reasons as in the unifier.  Please see the
        -- considerable commentary there before changing anything