projects / ghc-hetmet.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
[project @ 2003-06-20 11:14:18 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index dbf52a6..f3e864c 100644 (file)
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -16,49 +16,55 @@ is the principal client.
 \begin{code}
 module TcType (
   --------------------------------
 \begin{code}
 module TcType (
   --------------------------------
+  -- TyThing
+  TyThing(..), -- instance NamedThing
+
+  --------------------------------
   -- Types 
   -- Types 
-  TcType, TcTauType, TcPredType, TcThetaType, TcRhoType,
-  TcTyVar, TcTyVarSet, TcKind,
+  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
+  TcTyVar, TcTyVarSet, TcKind, 
 
   --------------------------------
   -- TyVarDetails
 
   --------------------------------
   -- TyVarDetails
-  TyVarDetails(..), isUserTyVar, isSkolemTyVar,
+  TyVarDetails(..), isUserTyVar, isSkolemTyVar, 
+  tyVarBindingInfo,
 
   --------------------------------
   -- Builders
 
   --------------------------------
   -- Builders
-  mkRhoTy, mkSigmaTy, 
+  mkPhiTy, mkSigmaTy, 
 
   --------------------------------
   -- Splitters  
   -- These are important because they do not look through newtypes
 
   --------------------------------
   -- 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,
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
-  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
+  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
   tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
   tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
-  tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
-  isQualifiedTy, isOverloadedTy, 
+  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
+  isSigmaTy, isOverloadedTy, 
   isDoubleTy, isFloatTy, isIntTy,
   isDoubleTy, isFloatTy, isIntTy,
-  isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, 
+  isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
   isTauTy, tcIsTyVarTy, tcIsForAllTy,
   isTauTy, tcIsTyVarTy, tcIsForAllTy,
+  allDistinctTyVars,
 
   ---------------------------------
   -- Misc type manipulators
 
   ---------------------------------
   -- Misc type manipulators
-  hoistForAllTys, deNoteType,
-  namesOfType, namesOfDFunHead,
+  deNoteType, classNamesOfTheta,
+  tyClsNamesOfType, tyClsNamesOfDFunHead, 
   getDFunTyKey,
 
   ---------------------------------
   -- Predicate types  
   getDFunTyKey,
 
   ---------------------------------
   -- Predicate types  
-  PredType, getClassPredTys_maybe, getClassPredTys, 
-  isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
-  mkDictTy, tcSplitPredTy_maybe, predTyUnique,
+  getClassPredTys_maybe, getClassPredTys, 
+  isPredTy, isClassPred, isTyVarClassPred, 
+  mkDictTy, tcSplitPredTy_maybe, 
   isDictTy, tcSplitDFunTy, predTyUnique, 
   isDictTy, tcSplitDFunTy, predTyUnique, 
-  mkClassPred, inheritablePred, isIPPred, mkPredName,
+  mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
 
   ---------------------------------
   -- Foreign import and export
 
   ---------------------------------
   -- Foreign import and export
@@ -69,11 +75,14 @@ module TcType (
   isFFIDynArgumentTy,  -- :: Type -> Bool
   isFFIDynResultTy,    -- :: Type -> Bool
   isFFILabelTy,        -- :: Type -> Bool
   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,
 
   ---------------------------------
   -- Unifier and matcher  
   unifyTysX, unifyTyListsX, unifyExtendTysX,
-  allDistinctTyVars,
   matchTy, matchTys, match,
 
   --------------------------------
   matchTy, matchTys, match,
 
   --------------------------------
@@ -81,21 +90,21 @@ module TcType (
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
-  isTypeKind,
+  isTypeKind, isAnyTypeKind,
 
   Type, SourceType(..), PredType, ThetaType, 
   mkForAllTy, mkForAllTys, 
   mkFunTy, mkFunTys, zipFunTys, 
 
   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
   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,
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
-  typeKind, eqKind, eqUsage,
+  typeKind, eqKind,
 
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
   ) where
 
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
   ) where
@@ -104,42 +113,53 @@ module TcType (
 
 
 import {-# SOURCE #-} PprType( pprType )
 
 
 import {-# SOURCE #-} PprType( pprType )
+-- PprType imports TcType so that it can print intelligently
 
 -- friends:
 import TypeRep         ( Type(..), TyNote(..), funTyCon )  -- friend
 
 -- friends:
 import TypeRep         ( Type(..), TyNote(..), funTyCon )  -- friend
-import Type            ( mkUTyM, unUTy )       -- Used locally
 
 import Type            (       -- Re-exports
 
 import Type            (       -- Re-exports
-                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-                         Kind, Type, TauType, SourceType(..), PredType, ThetaType, 
-                         unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
-                         mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
-                         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
+                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
+                         tyVarsOfTheta, Kind, Type, SourceType(..),
+                         PredType, ThetaType, unliftedTypeKind,
+                         liftedTypeKind, openTypeKind, mkArrowKind,
+                         mkArrowKinds, mkForAllTy, mkForAllTys,
+                         defaultKind, isTypeKind, isAnyTypeKind,
+                         mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
+                         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
                        )
                        )
-import TyCon           ( TyCon, isUnLiftedTyCon )
+import DataCon         ( DataCon )
+import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
 import Class           ( classHasFDs, Class )
 import Class           ( classHasFDs, Class )
-import Var             ( TyVar, tyVarKind )
-import ForeignCall     ( Safety, playSafe )
+import Var             ( TyVar, Id, tyVarKind, isMutTyVar, mutTyVarDetails )
+import ForeignCall     ( Safety, playSafe
+                         , DNType(..)
+                       )
 import VarEnv
 import VarSet
 
 -- others:
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 import VarEnv
 import VarSet
 
 -- others:
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name            ( Name, NamedThing(..), mkLocalName )
+import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import OccName         ( OccName, mkDictOcc )
 import NameSet
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
 import OccName         ( OccName, mkDictOcc )
 import NameSet
 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 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}
 import Maybes          ( maybeToBool, expectJust )
 import Outputable
 \end{code}
@@ -147,10 +167,66 @@ import Outputable
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
+                       TyThing
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+data TyThing = AnId     Id
+            | ADataCon DataCon
+            | ATyCon   TyCon
+            | AClass   Class
+
+instance NamedThing TyThing where
+  getName (AnId id)     = getName id
+  getName (ATyCon tc)   = getName tc
+  getName (AClass cl)   = getName cl
+  getName (ADataCon dc) = getName dc
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
 \subsection{Types}
 %*                                                                     *
 %************************************************************************
 
 \subsection{Types}
 %*                                                                     *
 %************************************************************************
 
+The type checker divides the generic Type world into the 
+following more structured beasts:
+
+sigma ::= forall tyvars. phi
+       -- A sigma type is a qualified type
+       --
+       -- Note that even if 'tyvars' is empty, theta
+       -- may not be: e.g.   (?x::Int) => Int
+
+       -- Note that 'sigma' is in prenex form:
+       -- all the foralls are at the front.
+       -- A 'phi' type has no foralls to the right of
+       -- an arrow
+
+phi :: theta => rho
+
+rho ::= sigma -> rho
+     |  tau
+
+-- A 'tau' type has no quantification anywhere
+-- Note that the args of a type constructor must be taus
+tau ::= tyvar
+     |  tycon tau_1 .. tau_n
+     |  tau_1 tau_2
+     |  tau_1 -> tau_2
+
+-- In all cases, a (saturated) type synonym application is legal,
+-- provided it expands to the required form.
+
+
+\begin{code}
+type SigmaType = Type
+type RhoType   = Type
+type TauType   = Type
+\end{code}
+
 \begin{code}
 type TcTyVar    = TyVar                -- Might be a mutable tyvar
 type TcTyVarSet = TyVarSet
 \begin{code}
 type TcTyVar    = TyVar                -- Might be a mutable tyvar
 type TcTyVarSet = TyVarSet
@@ -163,8 +239,9 @@ type TcType = Type          -- A TcType can have mutable type variables
 
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
 
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
-type TcRhoType      = Type
-type TcTauType      = TauType
+type TcSigmaType    = TcType
+type TcRhoType      = TcType
+type TcTauType      = TcType
 type TcKind         = TcType
 \end{code}
 
 type TcKind         = TcType
 \end{code}
 
@@ -177,6 +254,8 @@ type TcKind         = TcType
 
 TyVarDetails gives extra info about type variables, used during type
 checking.  It's attached to mutable type variables only.
 
 TyVarDetails gives extra info about type variables, used during type
 checking.  It's attached to mutable type variables only.
+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
 
 \begin{code}
 data TyVarDetails
@@ -200,20 +279,31 @@ data TyVarDetails
 
    | VanillaTv -- Everything else
 
 
    | VanillaTv -- Everything else
 
-isUserTyVar :: TyVarDetails -> Bool    -- Avoid unifying these if possible
-isUserTyVar VanillaTv = False
-isUserTyVar other     = True
-
-isSkolemTyVar :: TyVarDetails -> Bool
-isSkolemTyVar SigTv = True
-isSkolemTyVar other = False
-
-instance Outputable TyVarDetails where
-  ppr SigTv    = ptext SLIT("type signature")
-  ppr ClsTv     = ptext SLIT("class declaration")
-  ppr InstTv    = ptext SLIT("instance declaration")
-  ppr PatSigTv  = ptext SLIT("pattern type signature")
-  ppr VanillaTv = ptext SLIT("???")
+isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
+isUserTyVar tv = case mutTyVarDetails tv of
+                  VanillaTv -> False
+                  other     -> True
+
+isSkolemTyVar :: TcTyVar -> Bool
+isSkolemTyVar tv = case mutTyVarDetails tv of
+                     SigTv  -> True
+                     ClsTv  -> True
+                     InstTv -> True
+                     oteher -> False
+
+tyVarBindingInfo :: TyVar -> SDoc      -- Used in checkSigTyVars
+tyVarBindingInfo tv
+  | isMutTyVar tv
+  = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails 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 VanillaTv = ptext SLIT("//vanilla//")      -- Ditto
 \end{code}
 
 
 \end{code}
 
 
@@ -224,12 +314,10 @@ instance Outputable TyVarDetails where
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \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}
 
 
 \end{code}
 
 
@@ -243,7 +331,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 (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}
 
 isTauTy other           = False
 \end{code}
 
@@ -256,7 +343,6 @@ getDFunTyKey (AppTy fun _)               = getDFunTyKey fun
 getDFunTyKey (NoteTy _ t)           = getDFunTyKey t
 getDFunTyKey (FunTy arg _)          = getOccName funTyCon
 getDFunTyKey (ForAllTy _ t)         = getDFunTyKey t
 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
 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc   -- Newtypes are quite reasonable
 getDFunTyKey ty                             = pprPanic "getDFunTyKey" (pprType ty)
 -- SourceTy shouldn't happen
@@ -283,26 +369,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
    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
      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
 
 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
  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
   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
                                        (theta, tau) -> (tvs, theta, tau)
 
 tcTyConAppTyCon :: Type -> TyCon
@@ -317,12 +400,11 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
                        Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 
 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
                        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 (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 (NoteTy n ty)            = tcSplitTyConApp_maybe ty
-tcSplitTyConApp_maybe (UsageTy _ ty)           = tcSplitTyConApp_maybe ty
 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
 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
        -- However, predicates are not treated
        -- as tycon applications by the type checker
 tcSplitTyConApp_maybe other                    = Nothing
@@ -337,7 +419,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 :: 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 }
 tcSplitFunTy_maybe other           = Nothing
 
 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
@@ -345,29 +426,32 @@ tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 
 
 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
 
 
 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 (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 (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
 
 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)
+tc_split_app tc tys = case snocView tys of
+                       Just (tys',ty') -> Just (TyConApp tc tys', ty')
+                       Nothing         -> Nothing
 
 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
                    Just stuff -> stuff
                    Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
 
 
 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
 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
 tcGetTyVar_maybe other         = Nothing
 
 tcGetTyVar :: String -> Type -> TyVar
@@ -382,8 +466,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
 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)
 
 \begin{code}
 tcSplitMethodTy :: Type -> (PredType, Type)
@@ -393,7 +476,6 @@ tcSplitMethodTy ty = split ty
                            Just p  -> (p, res)
                            Nothing -> panic "splitMethodTy"
   split (NoteTy n 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])
   split _               = panic "splitMethodTy"
 
 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
@@ -404,6 +486,31 @@ tcSplitDFunTy ty
     (tvs, theta, clas, tys) }}
 \end{code}
 
     (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}    
+
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
@@ -417,42 +524,33 @@ tcSplitDFunTy ty
 isPred :: SourceType -> Bool
 isPred (ClassP _ _) = True
 isPred (IParam _ _) = True
 isPred :: SourceType -> Bool
 isPred (ClassP _ _) = True
 isPred (IParam _ _) = True
-isPred (NType _ __) = False
+isPred (NType _ _)  = False
 
 isPredTy :: Type -> Bool
 isPredTy (NoteTy _ ty)  = isPredTy ty
 
 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
 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
        
 predTyUnique :: PredType -> Unique
 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
 tcSplitPredTy_maybe other                  = Nothing
        
 predTyUnique :: PredType -> Unique
-predTyUnique (IParam n _)      = getUnique n
+predTyUnique (IParam n _)      = getUnique (ipNameName n)
 predTyUnique (ClassP clas tys) = getUnique clas
 
 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 :: Unique -> SrcLoc -> SourceType -> Name
-mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
-mkPredName uniq loc (IParam name ty) = 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}
 
 
 --------------------- Dictionary types ---------------------------------
 
 \begin{code}
 \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
 
 isClassPred :: SourceType -> Bool
 isClassPred (ClassP clas tys) = True
@@ -469,13 +567,11 @@ getClassPredTys :: PredType -> (Class, [Type])
 getClassPredTys (ClassP clas tys) = (clas, tys)
 
 mkDictTy :: Class -> [Type] -> 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 :: Type -> Bool
 isDictTy (SourceTy p)   = isClassPred p
 isDictTy (NoteTy _ ty) = isDictTy ty
-isDictTy (UsageTy _ ty) = isDictTy ty
 isDictTy other         = False
 \end{code}
 
 isDictTy other         = False
 \end{code}
 
@@ -486,7 +582,7 @@ isIPPred :: SourceType -> Bool
 isIPPred (IParam _ _) = True
 isIPPred other       = False
 
 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, 
 -- Can be inherited by a context.  For example, consider
 --     f x = let g y = (?v, y+x)
 --           in (g 3 with ?v = 8, 
@@ -495,8 +591,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
 --     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}
 
 
 \end{code}
 
 
@@ -513,6 +613,9 @@ But ignoring usage types
 tcEqType :: Type -> Type -> Bool
 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
 
 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 }
 
 tcEqPred :: PredType -> PredType -> Bool
 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
 
@@ -532,11 +635,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
 
   -- 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 (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
 
     -- Deal with equal constructors
 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
@@ -571,7 +672,7 @@ cmpTy env _ _ = LT
 
 \begin{code}
 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
 
 \begin{code}
 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
-cmpSourceTy env (IParam n1 ty1)   (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
+cmpSourceTy 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
        -- Compare types as well as names for implicit parameters
        -- This comparison is used exclusively (I think) for the
        -- finite map built in TcSimplify
@@ -600,30 +701,27 @@ instance Ord SourceType where { compare = tcCmpPred }
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-isQualifiedTy returns true of any qualified type.  It doesn't *necessarily* have 
+isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have 
 any foralls.  E.g.
        f :: (?x::Int) => Int -> Int
 
 \begin{code}
 any foralls.  E.g.
        f :: (?x::Int) => Int -> Int
 
 \begin{code}
-isQualifiedTy :: Type -> Bool
-isQualifiedTy (ForAllTy tyvar ty) = True
-isQualifiedTy (FunTy a b)        = isPredTy a
-isQualifiedTy (NoteTy n ty)      = isQualifiedTy ty
-isQualifiedTy (UsageTy _ ty)     = isQualifiedTy ty
-isQualifiedTy _                          = False
+isSigmaTy :: Type -> Bool
+isSigmaTy (ForAllTy tyvar ty) = True
+isSigmaTy (FunTy a b)        = isPredTy a
+isSigmaTy (NoteTy n 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 :: 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
 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
 isIntegerTy    = is_tc integerTyConKey
 isIntTy        = is_tc intTyConKey
 isAddrTy       = is_tc addrTyConKey
@@ -645,24 +743,6 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \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
 deNoteType :: Type -> Type
        -- Remove synonyms, but not source types
 deNoteType ty@(TyVarTy tyvar)  = ty
@@ -672,43 +752,45 @@ 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 (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 :: 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)
+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)
 \end{code}
 
 \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}
 
 \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
-namesOfType (UsageTy u ty)             = namesOfType u `unionNameSets` namesOfType ty
-
-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 (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
+tyClsNamesOfType (NoteTy other_note    ty2) = tyClsNamesOfType ty2
+tyClsNamesOfType (SourceTy (IParam n ty))   = tyClsNamesOfType ty
+tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (SourceTy (NType tc tys))  = unitNameSet (getName tc) `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
 -- 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
+
+classNamesOfTheta :: ThetaType -> [Name]
+-- Looks just for ClassP things; maybe it should check
+classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
 \end{code}
 
 
 \end{code}
 
 
@@ -742,26 +824,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 :: 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 :: 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 :: 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,
 
 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 
 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}
 
 ----------------------------------------------
 \end{code}
 
 ----------------------------------------------
@@ -774,8 +917,7 @@ legalFEArgTyCon :: TyCon -> Bool
 -- bytearrays from a _ccall_ / foreign declaration
 -- (or be passed them as arguments in foreign exported functions).
 legalFEArgTyCon tc
 -- 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
   = 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
@@ -784,24 +926,20 @@ legalFEArgTyCon tc
 
 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
 legalFIResultTyCon dflags 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
 
 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
 
 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
   = False
   | otherwise
   = marshalableTyCon dflags tc
@@ -817,45 +955,16 @@ boxedMarshalableTyCon tc
                         , word32TyConKey, word64TyConKey
                         , floatTyConKey, doubleTyConKey
                         , addrTyConKey, ptrTyConKey, funPtrTyConKey
                         , word32TyConKey, word64TyConKey
                         , floatTyConKey, doubleTyConKey
                         , addrTyConKey, ptrTyConKey, funPtrTyConKey
-                        , charTyConKey, foreignObjTyConKey
-                        , foreignPtrTyConKey
+                        , charTyConKey
                         , stablePtrTyConKey
                         , byteArrayTyConKey, mutableByteArrayTyConKey
                         , boolTyConKey
                         ]
                         , 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}
 
 
 %************************************************************************
 
 
 %************************************************************************
@@ -950,10 +1059,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
 
 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
 
        -- Anything else fails
 uTysX ty1 ty2 k subst = Nothing
 
@@ -974,7 +1079,6 @@ uVarX tv1 ty2 k subst@(tmpls, env)
               |  typeKind ty2 `eqKind` tyVarKind tv1
               && occur_check_ok ty2
               ->     -- No kind mismatch nor occur check
               |  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
                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
 
               | otherwise -> Nothing   -- Fail if kind mis-match or occur check
@@ -1042,8 +1146,15 @@ match (TyVarTy v) ty tmpls k senv
   | v `elemVarSet` tmpls
   =     -- v is a template variable
     case lookupSubstEnv senv v of
   | 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
 
        Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
                           | otherwise           -> Nothing  -- Fails
 
@@ -1084,9 +1195,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 (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
        -- 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
Glasgow Haskell Compiler with heterogeneous metaprogramming (generalized arrows and modal types)