[project @ 2003-12-30 16:29:17 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index 1752026..ffcf392 100644 (file)
@@ -17,25 +17,25 @@ is the principal client.
 module TcType (
   --------------------------------
   -- Types 
-  TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType, 
+  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
   TcTyVar, TcTyVarSet, TcKind, 
 
   --------------------------------
   -- TyVarDetails
-  TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar, 
+  TyVarDetails(..), isUserTyVar, isSkolemTyVar, 
   tyVarBindingInfo,
 
   --------------------------------
   -- 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,
+  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
   tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
 
   ---------------------------------
@@ -44,22 +44,22 @@ module TcType (
   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,
-  namesOfType, namesOfDFunHead,
+  deNoteType, classesOfTheta,
+  tyClsNamesOfType, tyClsNamesOfDFunHead, 
   getDFunTyKey,
 
   ---------------------------------
   -- Predicate types  
-  PredType, getClassPredTys_maybe, getClassPredTys, 
-  isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
-  mkDictTy, tcSplitPredTy_maybe, predTyUnique,
-  isDictTy, tcSplitDFunTy, predTyUnique, 
+  getClassPredTys_maybe, getClassPredTys, 
+  isClassPred, isTyVarClassPred, 
+  mkDictTy, tcSplitPredTy_maybe, 
+  isPredTy, isDictTy, tcSplitDFunTy, predTyUnique, 
   mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
 
   ---------------------------------
@@ -71,6 +71,10 @@ module TcType (
   isFFIDynArgumentTy,  -- :: Type -> Bool
   isFFIDynResultTy,    -- :: Type -> Bool
   isFFILabelTy,        -- :: Type -> Bool
+  isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
+  isFFIDotnetObjTy,    -- :: Type -> Bool
+  
+  toDNType,            -- :: Type -> DNType
 
   ---------------------------------
   -- Unifier and matcher  
@@ -81,66 +85,81 @@ module TcType (
   -- Rexported from Type
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
-  superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
-  isTypeKind, isAnyTypeKind,
+  isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, 
+  isSubKind, defaultKind, 
+  isArgTypeKind, isOpenTypeKind, 
 
-  Type, SourceType(..), PredType, ThetaType, 
+  Type, 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, 
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
-  typeKind, eqKind, eqUsage,
+  typeKind, 
 
-  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
-  ) where
+  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
 
-#include "HsVersions.h"
+  pprKind, pprParendKind,
+  pprType, pprParendType,
+  pprPred, pprTheta, pprThetaArrow, pprClassPred
 
+  ) where
 
-import {-# SOURCE #-} PprType( pprType )
+#include "HsVersions.h"
 
 -- friends:
 import TypeRep         ( Type(..), TyNote(..), funTyCon )  -- friend
 
 import Type            (       -- Re-exports
-                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-                         Kind, Type, SourceType(..), PredType, ThetaType, 
-                         unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
-                         mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
+                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
+                         tyVarsOfTheta, Kind, Type, PredType(..),
+                         ThetaType, unliftedTypeKind, 
+                         liftedTypeKind, openTypeKind, mkArrowKind,
+                         isLiftedTypeKind, isUnliftedTypeKind, 
+                         isOpenTypeKind, 
+                         mkArrowKinds, mkForAllTy, mkForAllTys,
+                         defaultKind, isArgTypeKind, isOpenTypeKind,
                          mkFunTy, mkFunTys, zipFunTys, 
-                         mkTyConApp, 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
+                         mkTyConApp, mkGenTyConApp, mkAppTy,
+                         mkAppTys, mkSynTy, applyTy, applyTys,
+                         mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
+                         mkPredTys, isUnLiftedType, 
+                         isUnboxedTupleType, isPrimitiveType,
+                         splitTyConApp_maybe,
+                         tidyTopType, tidyType, tidyPred, tidyTypes,
+                         tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
+                         tidyTyVarBndr, tidyOpenTyVar,
+                         tidyOpenTyVars, 
+                         isSubKind, 
+                         typeKind, repType,
+                         pprKind, pprParendKind,
+                         pprType, pprParendType,
+                         pprPred, pprTheta, pprThetaArrow, pprClassPred
                        )
-import TyCon           ( TyCon, isUnLiftedTyCon )
-import Class           ( classHasFDs, Class )
-import Var             ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
-import ForeignCall     ( Safety, playSafe )
+import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
+import Class           ( Class )
+import Var             ( TyVar, tyVarKind, tcTyVarDetails )
+import ForeignCall     ( Safety, playSafe, DNType(..) )
 import VarEnv
 import VarSet
 
 -- others:
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name            ( Name, NamedThing(..), mkLocalName, getSrcLoc )
-import OccName         ( OccName, mkDictOcc )
+import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import NameSet
+import OccName         ( OccName, mkDictOcc )
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
-import TysWiredIn      ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
+import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
 import BasicTypes      ( IPName(..), ipNameName )
 import Unique          ( Unique, Uniquable(..) )
 import SrcLoc          ( SrcLoc )
-import Util            ( cmpList, thenCmp, equalLength )
+import Util            ( cmpList, thenCmp, equalLength, snocView )
 import Maybes          ( maybeToBool, expectJust )
 import Outputable
 \end{code}
@@ -155,7 +174,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
@@ -166,7 +185,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
@@ -179,17 +200,7 @@ tau ::= tyvar
 -- In all cases, a (saturated) type synonym application is legal,
 -- provided it expands to the required form.
 
-
-\begin{code}
-type SigmaType = Type
-type PhiType   = Type
-type TauType   = Type
-\end{code}
-
 \begin{code}
-type TcTyVar    = TyVar                -- Might be a mutable tyvar
-type TcTyVarSet = TyVarSet
-
 type TcType = Type             -- A TcType can have mutable type variables
        -- Invariant on ForAllTy in TcTypes:
        --      forall a. T
@@ -199,9 +210,10 @@ 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
+
+type TcKind         = Kind
 \end{code}
 
 
@@ -217,16 +229,12 @@ It's knot-tied back to Var.lhs.  There is no reason in principle
 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 
 \begin{code}
-data TyVarDetails
-  = HoleTv     -- Used *only* by the type checker when passing in a type
-               -- variable that should be side-effected to the result type.
-               -- Always has kind openTypeKind.
-               -- Never appears in types
+type TcTyVar = TyVar   -- Used only during type inference
 
-  | SigTv      -- Introduced when instantiating a type signature,
+data TyVarDetails
+  = SigTv      -- Introduced when instantiating a type signature,
                -- prior to checking that the defn of a fn does 
                -- have the expected type.  Should not be instantiated.
-               --
                --      f :: forall a. a -> a
                --      f = e
                -- When checking e, with expected type (a->a), we 
@@ -238,45 +246,37 @@ data TyVarDetails
    | InstTv    -- Ditto, but instance decl
 
    | PatSigTv  -- Scoped type variable, introduced by a pattern
-               -- type signature
-               --      \ x::a -> e
+               -- type signature       \ x::a -> e
 
    | VanillaTv -- Everything else
 
 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
-isUserTyVar tv = case mutTyVarDetails tv of
+isUserTyVar tv = case tcTyVarDetails tv of
                   VanillaTv -> False
                   other     -> True
 
 isSkolemTyVar :: TcTyVar -> Bool
-isSkolemTyVar tv = case mutTyVarDetails tv of
-                     SigTv -> True
+isSkolemTyVar tv = case tcTyVarDetails tv of
+                     SigTv  -> True
+                     ClsTv  -> True
+                     InstTv -> True
                      oteher -> False
 
-isHoleTyVar :: TcTyVar -> Bool
--- NB:  the hole might be filled in by now, and this
---     function does not check for that
-isHoleTyVar tv = ASSERT( isMutTyVar tv )
-                case mutTyVarDetails tv of
-                       HoleTv -> True
-                       other  -> False
-
-tyVarBindingInfo :: TyVar -> SDoc      -- Used in checkSigTyVars
+tyVarBindingInfo :: TcTyVar -> SDoc    -- Used in checkSigTyVars
 tyVarBindingInfo tv
-  | isMutTyVar tv
-  = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
+  = sep [ptext SLIT("is bound by the") <+> details (tcTyVarDetails tv),
         ptext SLIT("at") <+> ppr (getSrcLoc tv)]
-  | otherwise
-  = empty
   where
     details SigTv     = ptext SLIT("type signature")
     details ClsTv     = ptext SLIT("class declaration")
     details InstTv    = ptext SLIT("instance declaration")
     details PatSigTv  = ptext SLIT("pattern type signature")
-    details HoleTv    = ptext SLIT("//hole//")         -- Should not happen
     details VanillaTv = ptext SLIT("//vanilla//")      -- Ditto
 \end{code}
 
+\begin{code}
+type TcTyVarSet = TyVarSet
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -285,22 +285,22 @@ tyVarBindingInfo tv
 %************************************************************************
 
 \begin{code}
-mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
+mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
 
-mkRhoTy :: [SourceType] -> Type -> Type
-mkRhoTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
+mkPhiTy :: [PredType] -> Type -> Type
+mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
 \end{code}
 
-
 @isTauTy@ tests for nested for-alls.
 
 \begin{code}
 isTauTy :: Type -> Bool
 isTauTy (TyVarTy v)     = True
 isTauTy (TyConApp _ tys) = all isTauTy tys
+isTauTy (NewTcApp _ tys) = all isTauTy tys
 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 (PredTy p)      = True         -- Don't look through source types
 isTauTy (NoteTy _ ty)   = isTauTy ty
 isTauTy other           = False
 \end{code}
@@ -308,15 +308,15 @@ isTauTy other              = False
 \begin{code}
 getDFunTyKey :: Type -> OccName        -- Get some string from a type, to be used to 
                                -- construct a dictionary function name
-getDFunTyKey (TyVarTy tv)           = getOccName tv
-getDFunTyKey (TyConApp tc _)        = getOccName tc
-getDFunTyKey (AppTy fun _)          = getDFunTyKey fun
-getDFunTyKey (NoteTy _ t)           = getDFunTyKey t
-getDFunTyKey (FunTy arg _)          = getOccName funTyCon
-getDFunTyKey (ForAllTy _ t)         = getDFunTyKey t
-getDFunTyKey (SourceTy (NType tc _)) = getOccName tc   -- Newtypes are quite reasonable
-getDFunTyKey ty                             = pprPanic "getDFunTyKey" (pprType ty)
--- SourceTy shouldn't happen
+getDFunTyKey (TyVarTy tv)    = getOccName tv
+getDFunTyKey (TyConApp tc _) = getOccName tc
+getDFunTyKey (NewTcApp tc _) = getOccName tc
+getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
+getDFunTyKey (NoteTy _ t)    = getDFunTyKey t
+getDFunTyKey (FunTy arg _)   = getOccName funTyCon
+getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
+getDFunTyKey ty                     = pprPanic "getDFunTyKey" (pprType ty)
+-- PredTy shouldn't happen
 \end{code}
 
 
@@ -346,8 +346,8 @@ tcIsForAllTy (ForAllTy tv ty) = True
 tcIsForAllTy (NoteTy 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)
@@ -356,7 +356,7 @@ tcSplitRhoTy ty = split ty ty []
   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
@@ -371,11 +371,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, [arg,res])
-tcSplitTyConApp_maybe (NoteTy n ty)            = tcSplitTyConApp_maybe ty
-tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
+tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
+tcSplitTyConApp_maybe (NewTcApp tc tys) = Just (tc, tys)
+tcSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
+tcSplitTyConApp_maybe (NoteTy n ty)     = tcSplitTyConApp_maybe ty
+       -- Newtypes are opaque, so they may be split
        -- However, predicates are not treated
        -- as tycon applications by the type checker
 tcSplitTyConApp_maybe other                    = Nothing
@@ -397,24 +397,29 @@ 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 [ty1], ty2)
-tcSplitAppTy_maybe (AppTy ty1 ty2)          = Just (ty1, ty2)
-tcSplitAppTy_maybe (NoteTy n 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
-tcSplitAppTy_maybe other                    = Nothing
-
-tc_split_app tc []  = Nothing
-tc_split_app tc tys = split tys []
-                   where
-                     split [ty2]    acc = Just (TyConApp tc (reverse acc), ty2)
-                     split (ty:tys) acc = split tys (ty:acc)
+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 (TyConApp tc tys) = case snocView tys of
+                                       Just (tys', ty') -> Just (TyConApp tc tys', ty')
+                                       Nothing          -> Nothing
+tcSplitAppTy_maybe (NewTcApp tc tys) = case snocView tys of
+                                       Just (tys', ty') -> Just (NewTcApp tc tys', ty')
+                                       Nothing          -> Nothing
+tcSplitAppTy_maybe other            = Nothing
 
 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
                    Just stuff -> stuff
                    Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
 
+tcSplitAppTys :: Type -> (Type, [Type])
+tcSplitAppTys ty
+  = go ty []
+  where
+    go ty args = case tcSplitAppTy_maybe ty of
+                  Just (ty', arg) -> go ty' (arg:args)
+                  Nothing         -> (ty,args)
+
 tcGetTyVar_maybe :: Type -> Maybe TyVar
 tcGetTyVar_maybe (TyVarTy tv)  = Just tv
 tcGetTyVar_maybe (NoteTy _ t)  = tcGetTyVar_maybe t
@@ -432,8 +437,7 @@ The type of a method for class C is always of the form:
 where sig_ty is the type given by the method's signature, and thus in general
 is a ForallTy.  At the point that splitMethodTy is called, it is expected
 that the outer Forall has already been stripped off.  splitMethodTy then
-returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
-Usages stripped off.
+returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
 
 \begin{code}
 tcSplitMethodTy :: Type -> (PredType, Type)
@@ -445,7 +449,7 @@ tcSplitMethodTy ty = split ty
   split (NoteTy n ty)  = split ty
   split _               = panic "splitMethodTy"
 
-tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
+tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
 -- Split the type of a dictionary function
 tcSplitDFunTy ty 
   = case tcSplitSigmaTy ty       of { (tvs, theta, tau) ->
@@ -485,38 +489,20 @@ allDistinctTyVars (ty:tys) acc
 %*                                                                     *
 %************************************************************************
 
-"Predicates" are particular source types, namelyClassP or IParams
-
 \begin{code}
-isPred :: SourceType -> Bool
-isPred (ClassP _ _) = True
-isPred (IParam _ _) = True
-isPred (NType _ _)  = False
-
-isPredTy :: Type -> Bool
-isPredTy (NoteTy _ 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 (SourceTy p) | isPred p = Just p
-tcSplitPredTy_maybe other                  = Nothing
+tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
+tcSplitPredTy_maybe (PredTy p)  = Just p
+tcSplitPredTy_maybe other        = Nothing
        
 predTyUnique :: PredType -> Unique
 predTyUnique (IParam n _)      = getUnique (ipNameName n)
 predTyUnique (ClassP clas tys) = getUnique clas
 
-predHasFDs :: PredType -> Bool
--- True if the predicate has functional depenencies; 
--- I.e. should participate in improvement
-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 :: Unique -> SrcLoc -> PredType -> Name
+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}
 
 
@@ -525,14 +511,14 @@ mkPredName uniq loc (IParam ip ty)   = mkLocalName uniq (getOccName (ipNameName
 \begin{code}
 mkClassPred clas tys = ClassP clas tys
 
-isClassPred :: SourceType -> Bool
+isClassPred :: PredType -> Bool
 isClassPred (ClassP clas tys) = True
 isClassPred other            = False
 
 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
 isTyVarClassPred other            = False
 
-getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
+getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
 getClassPredTys_maybe _                        = Nothing
 
@@ -543,7 +529,7 @@ mkDictTy :: Class -> [Type] -> Type
 mkDictTy clas tys = mkPredTy (ClassP clas tys)
 
 isDictTy :: Type -> Bool
-isDictTy (SourceTy p)   = isClassPred p
+isDictTy (PredTy p)   = isClassPred p
 isDictTy (NoteTy _ ty) = isDictTy ty
 isDictTy other         = False
 \end{code}
@@ -551,7 +537,7 @@ isDictTy other              = False
 --------------------- Implicit parameters ---------------------------------
 
 \begin{code}
-isIPPred :: SourceType -> Bool
+isIPPred :: PredType -> Bool
 isIPPred (IParam _ _) = True
 isIPPred other       = False
 
@@ -580,7 +566,6 @@ isLinearPred other             = False
 %************************************************************************
 
 Comparison, taking note of newtypes, predicates, etc,
-But ignoring usage types
 
 \begin{code}
 tcEqType :: Type -> Type -> Bool
@@ -598,7 +583,7 @@ tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
 
 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
 
-tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
+tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2
 -------------
 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
 
@@ -617,13 +602,14 @@ cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
                                          Just tv1a -> tv1a `compare` tv2
                                          Nothing   -> tv1  `compare` tv2
 
-cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
+cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
+cmpTy env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
 cmpTy env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTy (extendVarEnv env tv1 tv2) t1 t2
     
-    -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
+    -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < NewTcApp < ForAllTy < PredTy
 cmpTy env (AppTy _ _) (TyVarTy _) = GT
     
 cmpTy env (FunTy _ _) (TyVarTy _) = GT
@@ -633,38 +619,39 @@ cmpTy env (TyConApp _ _) (TyVarTy _) = GT
 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
     
+cmpTy env (NewTcApp _ _) (TyVarTy _)   = GT
+cmpTy env (NewTcApp _ _) (AppTy _ _)   = GT
+cmpTy env (NewTcApp _ _) (FunTy _ _)   = GT
+cmpTy env (NewTcApp _ _) (TyConApp _ _) = GT
+    
 cmpTy env (ForAllTy _ _) (TyVarTy _)    = GT
 cmpTy env (ForAllTy _ _) (AppTy _ _)    = GT
 cmpTy env (ForAllTy _ _) (FunTy _ _)    = GT
 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
+cmpTy env (ForAllTy _ _) (NewTcApp _ _) = GT
 
-cmpTy env (SourceTy _)   t2            = GT
+cmpTy env (PredTy _)   t2              = GT
 
 cmpTy env _ _ = LT
 \end{code}
 
 \begin{code}
-cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
-cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
+cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
+cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy 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
-cmpSourceTy env (IParam _ _)     sty             = LT
-
-cmpSourceTy env (ClassP _ _)     (IParam _ _)     = GT
-cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
-cmpSourceTy env (ClassP _ _)     (NType _ _)      = LT
-
-cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
-cmpSourceTy env (NType _ _)     sty              = GT
+cmpPredTy env (IParam _ _)     (ClassP _ _)      = LT
+cmpPredTy env (ClassP _ _)     (IParam _ _)     = GT
+cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
 \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  SourceType where { (==)    = tcEqPred }
-instance Ord SourceType where { compare = tcCmpPred }
+instance Eq  PredType where { (==)    = tcEqPred }
+instance Ord PredType where { compare = tcCmpPred }
 \end{code}
 
 
@@ -690,12 +677,17 @@ isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 isOverloadedTy (FunTy a b)        = isPredTy a
 isOverloadedTy (NoteTy n ty)      = isOverloadedTy ty
 isOverloadedTy _                  = False
+
+isPredTy :: Type -> Bool       -- Belongs in TcType because it does 
+                               -- not look through newtypes, or predtypes (of course)
+isPredTy (NoteTy _ ty) = isPredTy ty
+isPredTy (PredTy sty)  = True
+isPredTy _            = 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
@@ -717,77 +709,54 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 %************************************************************************
 
 \begin{code}
-hoistForAllTys :: Type -> Type
--- Used for user-written type signatures only
--- Move all the foralls and constraints to the top
--- e.g.  T -> forall a. a        ==>   forall a. T -> a
---      T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
---
--- We want to 'look through' type synonyms when doing this
--- so it's better done on the Type than the HsType
-
-hoistForAllTys ty
-  = case hoist ty ty of 
-       (tvs, theta, body) -> mkForAllTys tvs (mkFunTys theta body)
-  where
-    hoist orig_ty (ForAllTy tv ty) = case hoist ty ty of
-                                       (tvs,theta,tau) -> (tv:tvs,theta,tau)
-    hoist orig_ty (FunTy arg res)
-       | isPredTy arg             = case hoist res res of
-                                       (tvs,theta,tau) -> (tvs,arg:theta,tau)
-       | otherwise                = case hoist res res of
-                                       (tvs,theta,tau) -> (tvs,theta,mkFunTy arg tau)
-
-    hoist orig_ty (NoteTy _ ty)    = hoist orig_ty ty
-    hoist orig_ty ty              = ([], [], orig_ty)
-\end{code}
-
-
-\begin{code}
 deNoteType :: Type -> Type
-       -- Remove synonyms, but not source types
+       -- Remove synonyms, but not predicate types
 deNoteType ty@(TyVarTy tyvar)  = ty
 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
-deNoteType (SourceTy p)                = SourceTy (deNoteSourceType p)
+deNoteType (NewTcApp tycon tys) = NewTcApp tycon (map deNoteType tys)
+deNoteType (PredTy p)          = PredTy (deNotePredType p)
 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)
 
-deNoteSourceType :: SourceType -> SourceType
-deNoteSourceType (ClassP c tys)   = ClassP c (map deNoteType tys)
-deNoteSourceType (IParam n ty)    = IParam n (deNoteType ty)
-deNoteSourceType (NType tc tys)   = NType tc (map deNoteType tys)
+deNotePredType :: PredType -> PredType
+deNotePredType (ClassP c tys)   = ClassP c (map deNoteType tys)
+deNotePredType (IParam n ty)    = IParam n (deNoteType ty)
 \end{code}
 
-Find the free names of a type, including the type constructors and classes it mentions
-This is used in the front end of the compiler
+Find the free tycons and classes of a type.  This is used in the front
+end of the compiler.
 
 \begin{code}
-namesOfType :: Type -> NameSet
-namesOfType (TyVarTy tv)               = unitNameSet (getName tv)
-namesOfType (TyConApp tycon tys)       = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
-namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
-namesOfType (NoteTy other_note    ty2) = namesOfType ty2
-namesOfType (SourceTy (IParam n ty))   = namesOfType ty
-namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
-namesOfType (SourceTy (NType tc tys))  = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
-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
-
-namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
-
-namesOfDFunHead :: Type -> NameSet
+tyClsNamesOfType :: Type -> NameSet
+tyClsNamesOfType (TyVarTy tv)              = emptyNameSet
+tyClsNamesOfType (TyConApp tycon tys)      = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (NewTcApp tycon tys)      = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
+tyClsNamesOfType (NoteTy other_note    ty2) = tyClsNamesOfType ty2
+tyClsNamesOfType (PredTy (IParam n ty))   = tyClsNamesOfType ty
+tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (FunTy arg res)           = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
+tyClsNamesOfType (AppTy fun arg)           = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
+tyClsNamesOfType (ForAllTy tyvar ty)       = tyClsNamesOfType ty
+
+tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
+
+tyClsNamesOfDFunHead :: Type -> NameSet
 -- Find the free type constructors and classes 
 -- of the head of the dfun instance type
 -- The 'dfun_head_type' is because of
 --     instance Foo a => Baz T where ...
 -- The decl is an orphan if Baz and T are both not locally defined,
 --     even if Foo *is* locally defined
-namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
-                               (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
-                                                                     (map getName tvs)
+tyClsNamesOfDFunHead dfun_ty 
+  = case tcSplitSigmaTy dfun_ty of
+       (tvs,_,head_ty) -> tyClsNamesOfType head_ty
+
+classesOfTheta :: ThetaType -> [Class]
+-- Looks just for ClassP things; maybe it should check
+classesOfTheta preds = [ c | ClassP c _ <- preds ]
 \end{code}
 
 
@@ -821,26 +790,87 @@ isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
 isFFIDynArgumentTy :: Type -> Bool
 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
 -- or a newtype of either.
-isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
 
 isFFIDynResultTy :: Type -> Bool
 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
 -- or a newtype of either.
-isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
 
 isFFILabelTy :: Type -> Bool
 -- The type of a foreign label must be Ptr, FunPtr, Addr,
 -- or a newtype of either.
-isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
+
+isFFIDotnetTy :: DynFlags -> Type -> Bool
+isFFIDotnetTy dflags ty
+  = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
+                          (legalFIResultTyCon dflags tc || 
+                          isFFIDotnetObjTy ty || isStringTy ty)) ty
+
+-- Support String as an argument or result from a .NET FFI call.
+isStringTy ty = 
+  case tcSplitTyConApp_maybe (repType ty) of
+    Just (tc, [arg_ty])
+      | tc == listTyCon ->
+        case tcSplitTyConApp_maybe (repType arg_ty) of
+         Just (cc,[]) -> cc == charTyCon
+         _ -> False
+    _ -> False
+
+-- Support String as an argument or result from a .NET FFI call.
+isFFIDotnetObjTy ty = 
+  let
+   (_, t_ty) = tcSplitForAllTys ty
+  in
+  case tcSplitTyConApp_maybe (repType t_ty) of
+    Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
+    _ -> False
+
+toDNType :: Type -> DNType
+toDNType ty
+  | isStringTy ty = DNString
+  | isFFIDotnetObjTy ty = DNObject
+  | Just (tc,argTys) <- tcSplitTyConApp_maybe ty = 
+     case lookup (getUnique tc) dn_assoc of
+       Just x  -> x
+       Nothing 
+         | tc `hasKey` ioTyConKey -> toDNType (head argTys)
+        | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
+    where
+      dn_assoc :: [ (Unique, DNType) ]
+      dn_assoc = [ (unitTyConKey,   DNUnit)
+                , (intTyConKey,    DNInt)
+                , (int8TyConKey,   DNInt8)
+                , (int16TyConKey,  DNInt16)
+                , (int32TyConKey,  DNInt32)
+                , (int64TyConKey,  DNInt64)
+                , (wordTyConKey,   DNInt)
+                , (word8TyConKey,  DNWord8)
+                , (word16TyConKey, DNWord16)
+                , (word32TyConKey, DNWord32)
+                , (word64TyConKey, DNWord64)
+                , (floatTyConKey,  DNFloat)
+                , (doubleTyConKey, DNDouble)
+                , (addrTyConKey,   DNPtr)
+                , (ptrTyConKey,    DNPtr)
+                , (funPtrTyConKey, DNPtr)
+                , (charTyConKey,   DNChar)
+                , (boolTyConKey,   DNBool)
+                ]
 
 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
        -- Look through newtypes
        -- Non-recursive ones are transparent to splitTyConApp,
-       -- but recursive ones aren't; hence the splitNewType_maybe
+       -- but recursive ones aren't
 checkRepTyCon check_tc ty 
-  | Just ty'    <- splitNewType_maybe ty  = checkRepTyCon check_tc ty'
-  | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
-  | otherwise                            = False
+  | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
+  | otherwise                                      = False
+
+checkRepTyConKey :: [Unique] -> Type -> Bool
+-- Like checkRepTyCon, but just looks at the TyCon key
+checkRepTyConKey keys
+  = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
 \end{code}
 
 ----------------------------------------------
@@ -853,8 +883,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 ] 
+  | isByteArrayLikeTyCon tc
   = 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
@@ -863,24 +892,20 @@ legalFEArgTyCon tc
 
 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
 legalFIResultTyCon dflags tc
-  | getUnique tc `elem`
-       [ foreignObjTyConKey, foreignPtrTyConKey,
-         byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
-  | tc == unitTyCon = True
-  | otherwise      = marshalableTyCon dflags tc
+  | isByteArrayLikeTyCon tc = False
+  | tc == unitTyCon         = True
+  | otherwise              = marshalableTyCon dflags tc
 
 legalFEResultTyCon :: TyCon -> Bool
 legalFEResultTyCon tc
-  | getUnique tc `elem` 
-       [ foreignObjTyConKey, foreignPtrTyConKey,
-         byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
-  | tc == unitTyCon = True
-  | otherwise       = boxedMarshalableTyCon tc
+  | isByteArrayLikeTyCon tc = False
+  | tc == unitTyCon         = True
+  | otherwise               = boxedMarshalableTyCon tc
 
 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
 -- Checks validity of types going from Haskell -> external world
 legalOutgoingTyCon dflags safety tc
-  | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
+  | playSafe safety && isByteArrayLikeTyCon tc
   = False
   | otherwise
   = marshalableTyCon dflags tc
@@ -896,12 +921,15 @@ boxedMarshalableTyCon tc
                         , word32TyConKey, word64TyConKey
                         , floatTyConKey, doubleTyConKey
                         , addrTyConKey, ptrTyConKey, funPtrTyConKey
-                        , charTyConKey, foreignObjTyConKey
-                        , foreignPtrTyConKey
+                        , charTyConKey
                         , stablePtrTyConKey
                         , byteArrayTyConKey, mutableByteArrayTyConKey
                         , boolTyConKey
                         ]
+
+isByteArrayLikeTyCon :: TyCon -> Bool
+isByteArrayLikeTyCon tc = 
+  getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
 \end{code}
 
 
@@ -961,18 +989,18 @@ uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
   = uVarX tyvar2 ty1 k subst
 
        -- Predicates
-uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
+uTysX (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) k subst
   | n1 == n2 = uTysX t1 t2 k subst
-uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
+uTysX (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) k subst
   | c1 == c2 = uTyListsX tys1 tys2 k subst
-uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
-  | tc1 == tc2 = uTyListsX tys1 tys2 k subst
 
        -- Functions; just check the two parts
 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
 
        -- Type constructors must match
+uTysX (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) k subst
+  | tc1 == tc2 = uTyListsX tys1 tys2 k subst
 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
   | (con1 == con2 && equalLength tys1 tys2)
   = uTyListsX tys1 tys2 k subst
@@ -1014,7 +1042,7 @@ uVarX tv1 ty2 k subst@(tmpls, env)
                     uTysX ty1 ty2 k subst
 
       Nothing       -- Not already bound
-              |  typeKind ty2 `eqKind` tyVarKind tv1
+              |  typeKind ty2 == tyVarKind tv1
               && occur_check_ok ty2
               ->     -- No kind mismatch nor occur check
                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
@@ -1084,10 +1112,10 @@ match (TyVarTy v) ty tmpls k senv
   | v `elemVarSet` tmpls
   =     -- v is a template variable
     case lookupSubstEnv senv v of
-       Nothing | typeKind ty `eqKind` tyVarKind v      
+       Nothing | typeKind ty == 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
+                       -- 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))
 
@@ -1110,12 +1138,10 @@ match (TyVarTy v) ty tmpls k senv
     -- expect, due to an intervening Note.  KSW 2000-06.
 
        -- Predicates
-match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
+match (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) tmpls k senv
   | n1 == n2 = match t1 t2 tmpls k senv
-match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
+match (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) tmpls k senv
   | c1 == c2 = match_list_exactly tys1 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
 
        -- Functions; just check the two parts
 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
@@ -1126,11 +1152,10 @@ match (AppTy fun1 arg1) ty2 tmpls k senv
        Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
        Nothing          -> Nothing     -- Fail
 
-match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
+-- Newtypes are opaque; predicate types should not happen
+match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
-
--- Newtypes are opaque; other source types should not happen
-match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
+match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 
        -- With type synonyms, we have to be careful for the exact