[project @ 2003-11-03 16:00:57 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index b8f0878..8815cf5 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,21 +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, 
 
   ---------------------------------
@@ -70,77 +71,97 @@ module TcType (
   isFFIDynArgumentTy,  -- :: Type -> Bool
   isFFIDynResultTy,    -- :: Type -> Bool
   isFFILabelTy,        -- :: Type -> Bool
+  isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
+  isFFIDotnetObjTy,    -- :: Type -> Bool
+  
+  toDNType,            -- :: Type -> DNType
 
   ---------------------------------
   -- Unifier and matcher  
   unifyTysX, unifyTyListsX, unifyExtendTysX,
-  allDistinctTyVars,
   matchTy, matchTys, match,
 
   --------------------------------
   -- Rexported from Type
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
+  isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, isSuperKind,
   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
-  isTypeKind, isAnyTypeKind,
+  isTypeKind, isAnyTypeKind, typeCon,
 
-  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, eqKind,
 
-  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, typeCon,
+                         liftedTypeKind, openTypeKind, mkArrowKind,
+                         isLiftedTypeKind, isUnliftedTypeKind, 
+                         isOpenTypeKind, isSuperKind,
+                         mkArrowKinds, mkForAllTy, mkForAllTys,
+                         defaultKind, isTypeKind, isAnyTypeKind,
                          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, eqKind, 
+                         hasMoreBoxityInfo, liftedBoxity,
+                         superBoxity, typeKind, superKind, repType,
+                         pprKind, pprParendKind,
+                         pprType, pprParendType,
+                         pprPred, pprTheta, pprThetaArrow, pprClassPred
                        )
-import TyCon           ( TyCon, isUnLiftedTyCon )
-import Class           ( classHasFDs, Class )
+import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
+import Class           ( Class )
 import Var             ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
-import ForeignCall     ( Safety, playSafe )
+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 +176,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 +187,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,13 +202,6 @@ 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
@@ -199,7 +215,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}
@@ -218,12 +234,7 @@ 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
-
-  | SigTv      -- Introduced when instantiating a type signature,
+  = 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.
                --
@@ -250,17 +261,11 @@ 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
--- 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 tv
   | isMutTyVar tv
@@ -273,7 +278,6 @@ tyVarBindingInfo tv
     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}
 
@@ -285,22 +289,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 +312,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 +350,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 +360,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 +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, [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 +401,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 +441,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 +453,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) ->
@@ -453,6 +461,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}    
+
 
 %************************************************************************
 %*                                                                     *
@@ -460,38 +493,20 @@ tcSplitDFunTy ty
 %*                                                                     *
 %************************************************************************
 
-"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}
 
 
@@ -500,14 +515,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
 
@@ -518,7 +533,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}
@@ -526,7 +541,7 @@ isDictTy other              = False
 --------------------- Implicit parameters ---------------------------------
 
 \begin{code}
-isIPPred :: SourceType -> Bool
+isIPPred :: PredType -> Bool
 isIPPred (IParam _ _) = True
 isIPPred other       = False
 
@@ -555,7 +570,6 @@ isLinearPred other             = False
 %************************************************************************
 
 Comparison, taking note of newtypes, predicates, etc,
-But ignoring usage types
 
 \begin{code}
 tcEqType :: Type -> Type -> Bool
@@ -573,7 +587,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
 
@@ -592,13 +606,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
@@ -608,38 +623,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}
 
 
@@ -665,12 +681,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
@@ -692,77 +713,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}
 
 
@@ -796,26 +794,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}
 
 ----------------------------------------------
@@ -828,8 +887,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
@@ -838,24 +896,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
@@ -871,45 +925,16 @@ boxedMarshalableTyCon tc
                         , word32TyConKey, word64TyConKey
                         , floatTyConKey, doubleTyConKey
                         , addrTyConKey, ptrTyConKey, funPtrTyConKey
-                        , charTyConKey, foreignObjTyConKey
-                        , foreignPtrTyConKey
+                        , charTyConKey
                         , stablePtrTyConKey
                         , byteArrayTyConKey, mutableByteArrayTyConKey
                         , boolTyConKey
                         ]
-\end{code}
-
 
-%************************************************************************
-%*                                                                     *
-\subsection{Unification with an explicit substitution}
-%*                                                                     *
-%************************************************************************
-
-(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}    
+isByteArrayLikeTyCon :: TyCon -> Bool
+isByteArrayLikeTyCon tc = 
+  getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
+\end{code}
 
 
 %************************************************************************
@@ -968,18 +993,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
@@ -1094,7 +1119,7 @@ match (TyVarTy v) ty tmpls k senv
        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
+                       -- 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))
 
@@ -1117,12 +1142,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
@@ -1133,11 +1156,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