[project @ 2005-03-01 21:40:40 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..b9ff393 100644 (file)
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -1,4 +1,4 @@
-%
+

 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcType]{Types used in the typechecker}
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcType]{Types used in the typechecker}

@@ -17,48 +17,51 @@ is the principal client.
 module TcType (
   --------------------------------
   -- Types 
 module TcType (
   --------------------------------
   -- Types 

-  TcType, TcTauType, TcPredType, TcThetaType, TcRhoType,
-  TcTyVar, TcTyVarSet, TcKind,
+  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
+  TcTyVar, TcTyVarSet, TcKind, 

 
   --------------------------------
 
   --------------------------------

-  -- TyVarDetails
-  TyVarDetails(..), isUserTyVar, isSkolemTyVar,
+  -- MetaDetails
+  Expected(..), TcRef, TcTyVarDetails(..),
+  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+  isFlexi, isIndirect, 

 
   --------------------------------
   -- Builders
 
   --------------------------------
   -- Builders

-  mkRhoTy, mkSigmaTy, 
+  mkPhiTy, mkSigmaTy, hoistForAllTys,

 
   --------------------------------
   -- 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,
-  tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
+  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
+  tcGetTyVar_maybe, tcGetTyVar,

 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque

-  tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
-  isQualifiedTy, isOverloadedTy, 
+  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
+  isSigmaTy, isOverloadedTy, 

   isDoubleTy, isFloatTy, isIntTy,
   isDoubleTy, isFloatTy, isIntTy,

-  isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, 
+  isIntegerTy, isAddrTy, isBoolTy, isUnitTy,

   isTauTy, tcIsTyVarTy, tcIsForAllTy,
 
   ---------------------------------
   -- Misc type manipulators
   isTauTy, tcIsTyVarTy, tcIsForAllTy,
 
   ---------------------------------
   -- Misc type manipulators

-  hoistForAllTys, deNoteType,
-  namesOfType, namesOfDFunHead,
+  deNoteType, classesOfTheta,
+  tyClsNamesOfType, tyClsNamesOfDFunHead, 

   getDFunTyKey,
 
   ---------------------------------
   -- Predicate types  
   getDFunTyKey,
 
   ---------------------------------
   -- Predicate types  

-  PredType, getClassPredTys_maybe, getClassPredTys, 
-  isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
-  mkDictTy, tcSplitPredTy_maybe, predTyUnique,
-  isDictTy, tcSplitDFunTy, predTyUnique, 
-  mkClassPred, inheritablePred, isIPPred, mkPredName,
+  getClassPredTys_maybe, getClassPredTys, 
+  isClassPred, isTyVarClassPred, 
+  mkDictTy, tcSplitPredTy_maybe, 
+  isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
+  mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 

 
   ---------------------------------
   -- Foreign import and export
 
   ---------------------------------
   -- Foreign import and export

@@ -69,79 +72,111 @@ module TcType (
   isFFIDynArgumentTy,  -- :: Type -> Bool
   isFFIDynResultTy,    -- :: Type -> Bool
   isFFILabelTy,        -- :: Type -> Bool
   isFFIDynArgumentTy,  -- :: Type -> Bool
   isFFIDynResultTy,    -- :: Type -> Bool
   isFFILabelTy,        -- :: Type -> Bool

-
-  ---------------------------------
-  -- Unifier and matcher  
-  unifyTysX, unifyTyListsX, unifyExtendTysX,
-  allDistinctTyVars,
-  matchTy, matchTys, match,
+  isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
+  isFFIDotnetObjTy,    -- :: Type -> Bool
+  isFFITy,            -- :: Type -> Bool
+  
+  toDNType,            -- :: Type -> DNType

 
   --------------------------------
   -- Rexported from Type
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
 
   --------------------------------
   -- Rexported from Type
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 

-  superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
-  isTypeKind,
+  isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, 
+  isArgTypeKind, isSubKind, defaultKind, 

 
 

-  Type, SourceType(..), PredType, ThetaType, 
+  Type, PredType(..), ThetaType, 

   mkForAllTy, mkForAllTys, 
   mkFunTy, mkFunTys, zipFunTys, 
   mkForAllTy, mkForAllTys, 
   mkFunTy, mkFunTys, zipFunTys, 

-  mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+  mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,

   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, 
 
   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, 
 

+  -- Type substitutions
+  TvSubst(..),         -- Representation visible to a few friends
+  TvSubstEnv, emptyTvSubst,
+  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
+  getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
+  extendTvSubst, extendTvSubstList, isInScope,
+  substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
+

   isUnLiftedType,      -- Source types are always lifted
   isUnboxedTupleType,  -- Ditto
   isUnLiftedType,      -- Source types are always lifted
   isUnboxedTupleType,  -- Ditto

-  isPrimitiveType,
+  isPrimitiveType, 

 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,

-  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
-  typeKind, eqKind, eqUsage,
+  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
+  typeKind, 

 
 

-  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
-  ) where
+  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,

 
 

-#include "HsVersions.h"
+  pprKind, pprParendKind,
+  pprType, pprParendType, pprTyThingCategory,
+  pprPred, pprTheta, pprThetaArrow, pprClassPred

 
 

+  ) where

 
 

-import {-# SOURCE #-} PprType( pprType )
+#include "HsVersions.h"

 
 -- 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,
+                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
+                         tyVarsOfTheta, Kind, PredType(..),
+                         ThetaType, unliftedTypeKind, 
+                         liftedTypeKind, openTypeKind, mkArrowKind,
+                         isLiftedTypeKind, isUnliftedTypeKind, 
+                         mkArrowKinds, mkForAllTy, mkForAllTys,
+                         defaultKind, isArgTypeKind, isOpenTypeKind,

                          mkFunTy, mkFunTys, zipFunTys, 
                          mkFunTy, mkFunTys, zipFunTys, 

-                         mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
-                         mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
-                         isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
-                         splitNewType_maybe, splitTyConApp_maybe,
-                         tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-                         tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
-                         hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
+                         mkTyConApp, mkGenTyConApp, mkAppTy,
+                         mkAppTys, mkSynTy, applyTy, applyTys,
+                         mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
+                         mkPredTys, isUnLiftedType, 
+                         isUnboxedTupleType, isPrimitiveType,
+                         splitTyConApp_maybe,
+                         tidyTopType, tidyType, tidyPred, tidyTypes,
+                         tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
+                         tidyTyVarBndr, tidyOpenTyVar,
+                         tidyOpenTyVars, 
+                         isSubKind, deShadowTy,
+
+                         tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
+                         tcEqPred, tcCmpPred, tcEqTypeX, 
+
+                         TvSubst(..),
+                         TvSubstEnv, emptyTvSubst,
+                         mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
+                         getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
+                         extendTvSubst, extendTvSubstList, isInScope,
+                         substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
+
+                         typeKind, repType,
+                         pprKind, pprParendKind,
+                         pprType, pprParendType, pprTyThingCategory,
+                         pprPred, pprTheta, pprThetaArrow, pprClassPred

                        )
                        )

-import TyCon           ( TyCon, isUnLiftedTyCon )
-import Class           ( classHasFDs, Class )
-import Var             ( TyVar, tyVarKind )
-import ForeignCall     ( Safety, playSafe )
-import VarEnv
+import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
+import DataCon         ( DataCon )
+import Class           ( Class )
+import Var             ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
+import ForeignCall     ( Safety, playSafe, DNType(..) )

 import VarSet
 
 -- others:
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 import VarSet
 
 -- others:
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )

-import Name            ( Name, NamedThing(..), mkLocalName )
-import OccName         ( OccName, mkDictOcc )
+import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )

 import NameSet
 import NameSet

+import VarEnv          ( TidyEnv )
+import OccName         ( OccName, mkDictOcc )

 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)

-import TysWiredIn      ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
-import Unique          ( Unique, Uniquable(..) )
-import SrcLoc          ( SrcLoc )
-import Util            ( cmpList, thenCmp, equalLength )
+import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
+import BasicTypes      ( IPName(..), ipNameName )
+import SrcLoc          ( SrcLoc, SrcSpan )
+import Util            ( snocView )

 import Maybes          ( maybeToBool, expectJust )
 import Outputable
 import Maybes          ( maybeToBool, expectJust )
 import Outputable

+import DATA_IOREF

 \end{code}
 
 
 \end{code}
 
 

@@ -151,10 +186,36 @@ import Outputable
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 

-\begin{code}
-type TcTyVar    = TyVar                -- Might be a mutable tyvar
-type TcTyVarSet = TyVarSet
+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 TcType = Type             -- A TcType can have mutable type variables
        -- Invariant on ForAllTy in TcTypes:
        --      forall a. T
 type TcType = Type             -- A TcType can have mutable type variables
        -- Invariant on ForAllTy in TcTypes:
        --      forall a. T

@@ -163,9 +224,15 @@ 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 TcKind         = TcType
+type TcSigmaType    = TcType
+type TcRhoType      = TcType
+type TcTauType      = TcType
+type TcKind         = Kind
+type TcTyVarSet     = TyVarSet
+
+type TcRef a    = IORef a
+data Expected ty = Infer (TcRef ty)    -- The hole to fill in for type inference
+                | Check ty             -- The type to check during type checking

 \end{code}
 
 
 \end{code}
 
 

@@ -177,43 +244,146 @@ 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.
+
+Note [Signature skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+  x :: [a]
+  y :: b
+  (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment.  We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+       ( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to 
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other.  Alas.
+
+On the other hand, we *must* use skolems for signature type variables, 
+becuase GADT type refinement refines skolems only.  
+
+One solution woudl be insist that in the above defn the programmer uses
+the same type variable in both type signatures.  But that takes explanation.
+
+The alternative (currently implemented) is to have a special kind of skolem
+constant, SigSkokTv, which can unify with other SigSkolTvs.  
+

 
 \begin{code}
 
 \begin{code}

-data TyVarDetails
-  = SigTv      -- Introduced when instantiating a type signature,
-               -- prior to checking that the defn of a fn does 
-               -- have the expected type.  Should not be instantiated.
-               --
-               --      f :: forall a. a -> a
-               --      f = e
-               -- When checking e, with expected type (a->a), we 
-               -- should not instantiate a
-
-   | ClsTv     -- Scoped type variable introduced by a class decl
-               --      class C a where ...
-
-   | InstTv    -- Ditto, but instance decl
-
-   | PatSigTv  -- Scoped type variable, introduced by a pattern
-               -- type signature
-               --      \ x::a -> e
-
-   | 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("???")
+type TcTyVar = TyVar   -- Used only during type inference
+
+-- A TyVarDetails is inside a TyVar
+data TcTyVarDetails
+  = MetaTv (IORef MetaDetails)         -- A meta type variable stands for a tau-type
+  | SkolemTv SkolemInfo                        -- A skolem constant
+  | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature;
+                                       --      see Note [Signature skolems]
+                                       --      The MetaDetails, if filled in, will 
+                                       --      always be another SigSkolTv
+
+data SkolemInfo
+  = SigSkol Name       -- Bound at a type signature
+  | ClsSkol Class      -- Bound at a class decl
+  | InstSkol Id                -- Bound at an instance decl
+  | PatSkol DataCon    -- An existential type variable bound by a pattern for
+           SrcSpan     -- a data constructor with an existential type. E.g.
+                       --      data T = forall a. Eq a => MkT a
+                       --      f (MkT x) = ...
+                       -- The pattern MkT x will allocate an existential type
+                       -- variable for 'a'.  
+  | ArrowSkol SrcSpan  -- An arrow form (see TcArrows)
+
+  | GenSkol [TcTyVar]  -- Bound when doing a subsumption check for 
+           TcType      --      (forall tvs. ty)
+           SrcSpan
+
+data MetaDetails
+  = Flexi          -- Flexi type variables unify to become 
+                   -- Indirects.  
+
+  | Indirect TcType  -- Type indirections, treated as wobbly 
+                     -- for the purpose of GADT unification.
+
+tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
+-- Tidy the type inside a GenSkol, preparatory to printing it
+tidySkolemTyVar env tv
+  = ASSERT( isSkolemTyVar tv )
+    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
+  where
+    (env1, info1) = case tcTyVarDetails tv of
+                     SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
+                           where
+                             (env1, tvs1) = tidyOpenTyVars env tvs
+                             (env2, ty1)  = tidyOpenType env1 ty
+                     info -> (env, info)
+                    
+pprTcTyVar :: TcTyVar -> SDoc
+-- Print tyvar with info about its binding
+pprTcTyVar tv
+  = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
+  where
+    ppr_details (MetaTv _)      = ptext SLIT("is a meta type variable")
+    ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
+    ppr_details (SkolemTv info)  = ptext SLIT("is bound by") <+> pprSkolInfo info
+ 
+pprSkolInfo :: SkolemInfo -> SDoc
+pprSkolInfo (SigSkol id)     = ptext SLIT("the type signature for") <+> quotes (ppr id)
+pprSkolInfo (ClsSkol cls)    = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo (InstSkol df)    = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
+pprSkolInfo (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
+pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
+                                   nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type") 
+                                       <+> quotes (ppr (mkForAllTys tvs ty)),
+                                       nest 2 (ptext SLIT("at") <+> ppr loc)]
+
+instance Outputable MetaDetails where
+  ppr Flexi        = ptext SLIT("Flexi")
+  ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty
+
+isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isMetaTyVar :: TyVar -> Bool
+isImmutableTyVar tv
+  | isTcTyVar tv = isSkolemTyVar tv
+  | otherwise    = True
+
+isSkolemTyVar tv 
+  = ASSERT( isTcTyVar tv )
+    case tcTyVarDetails tv of
+       SkolemTv _    -> True
+       SigSkolTv _ _ -> True
+       MetaTv _      -> False
+
+isExistentialTyVar tv  -- Existential type variable, bound by a pattern
+  = ASSERT( isTcTyVar tv )
+    case tcTyVarDetails tv of
+       SkolemTv (PatSkol _ _) -> True
+       other                  -> False
+
+isMetaTyVar tv 
+  = ASSERT( isTcTyVar tv )
+    case tcTyVarDetails tv of
+       MetaTv _   -> True
+       other      -> False
+
+metaTvRef :: TyVar -> IORef MetaDetails
+metaTvRef tv 
+  = ASSERT( isTcTyVar tv )
+    case tcTyVarDetails tv of
+       MetaTv ref -> ref
+       other      -> pprPanic "metaTvRef" (ppr tv)
+
+isFlexi, isIndirect :: MetaDetails -> Bool
+isFlexi Flexi = True
+isFlexi other = False
+
+isIndirect (Indirect _) = True
+isIndirect other        = False

 \end{code}
 
 
 \end{code}
 
 

@@ -224,15 +394,12 @@ 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 :: [PredType] -> Type -> Type
+mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta

 \end{code}
 
 \end{code}
 

-

 @isTauTy@ tests for nested for-alls.
 
 \begin{code}
 @isTauTy@ tests for nested for-alls.
 
 \begin{code}

@@ -241,25 +408,22 @@ isTauTy (TyVarTy v)        = True
 isTauTy (TyConApp _ tys) = all isTauTy tys
 isTauTy (AppTy a b)     = isTauTy a && isTauTy b
 isTauTy (FunTy a b)     = isTauTy a && isTauTy b
 isTauTy (TyConApp _ 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 (NoteTy _ ty)   = isTauTy ty

-isTauTy (UsageTy _ ty)   = isTauTy ty

 isTauTy other           = False
 \end{code}
 
 \begin{code}
 getDFunTyKey :: Type -> OccName        -- Get some string from a type, to be used to 
                                -- construct a dictionary function name
 isTauTy other           = False
 \end{code}
 
 \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 (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 (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 ty                     = pprPanic "getDFunTyKey" (pprType ty)
+-- PredTy shouldn't happen

 \end{code}
 
 
 \end{code}
 
 

@@ -283,26 +447,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 +478,10 @@ 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 (FunTy arg res)          = Just (funTyCon, [unUTy arg,unUTy res])
-tcSplitTyConApp_maybe (NoteTy n ty)            = tcSplitTyConApp_maybe ty
-tcSplitTyConApp_maybe (UsageTy _ ty)           = tcSplitTyConApp_maybe ty
-tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
+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
+       -- 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 +496,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 +503,29 @@ 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 (AppTy ty1 ty2)          = Just (ty1, ty2)
-tcSplitAppTy_maybe (NoteTy n ty)            = tcSplitAppTy_maybe ty
-tcSplitAppTy_maybe (UsageTy _ ty)           = tcSplitAppTy_maybe ty
-tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
-       --- Don't forget that newtype!
-tcSplitAppTy_maybe (TyConApp tc tys)        = tc_split_app tc tys
-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 other            = 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

@@ -375,93 +533,58 @@ tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 
 tcIsTyVarTy :: Type -> Bool
 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 
 tcIsTyVarTy :: Type -> Bool
 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)

-\end{code}

 
 

-The type of a method for class C is always of the form:
-       Forall a1..an. C a1..an => sig_ty
-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.
-
-\begin{code}
-tcSplitMethodTy :: Type -> (PredType, Type)
-tcSplitMethodTy ty = split ty
- where
-  split (FunTy arg res) = case tcSplitPredTy_maybe arg of
-                           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])
+tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])

 -- Split the type of a dictionary function
 tcSplitDFunTy ty 
 -- Split the type of a dictionary function
 tcSplitDFunTy ty 

-  = case tcSplitSigmaTy ty       of { (tvs, theta, tau) ->
-    case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) -> 
+  = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
+    case tcSplitDFunHead tau of { (clas, tys) -> 

     (tvs, theta, clas, tys) }}
     (tvs, theta, clas, tys) }}

+
+tcSplitDFunHead :: Type -> (Class, [Type])
+tcSplitDFunHead tau  
+  = case tcSplitPredTy_maybe tau of 
+       Just (ClassP clas tys) -> (clas, tys)

 \end{code}
 
 
 \end{code}
 
 

+

 %************************************************************************
 %*                                                                     *
 \subsection{Predicate types}
 %*                                                                     *
 %************************************************************************
 
 %************************************************************************
 %*                                                                     *
 \subsection{Predicate types}
 %*                                                                     *
 %************************************************************************
 

-"Predicates" are particular source types, namelyClassP or IParams
-

 \begin{code}
 \begin{code}

-isPred :: SourceType -> Bool
-isPred (ClassP _ _) = True
-isPred (IParam _ _) = True
-isPred (NType _ __) = False
-
-isPredTy :: Type -> Bool
-isPredTy (NoteTy _ ty)  = isPredTy ty
-isPredTy (UsageTy _ ty) = isPredTy ty
-isPredTy (SourceTy sty) = isPred sty
-isPredTy _             = False
-

 tcSplitPredTy_maybe :: Type -> Maybe PredType
    -- Returns Just for predicates only
 tcSplitPredTy_maybe :: 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
+tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
+tcSplitPredTy_maybe (PredTy p)    = Just p
+tcSplitPredTy_maybe other        = Nothing

        
 predTyUnique :: PredType -> Unique
        
 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 uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
-mkPredName uniq loc (IParam name ty) = name
+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}
 
 
 --------------------- 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 :: PredType -> Bool

 isClassPred (ClassP clas tys) = True
 isClassPred other            = False
 
 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
 isTyVarClassPred other            = False
 
 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
 
 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
 getClassPredTys_maybe _                        = Nothing
 

@@ -469,24 +592,22 @@ 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 :: Type -> Bool

-isDictTy (SourceTy p)   = isClassPred p
+isDictTy (PredTy p)   = isClassPred p

 isDictTy (NoteTy _ ty) = isDictTy ty
 isDictTy (NoteTy _ ty) = isDictTy ty

-isDictTy (UsageTy _ ty) = isDictTy ty

 isDictTy other         = False
 \end{code}
 
 --------------------- Implicit parameters ---------------------------------
 
 \begin{code}
 isDictTy other         = False
 \end{code}
 
 --------------------- Implicit parameters ---------------------------------
 
 \begin{code}

-isIPPred :: SourceType -> Bool
+isIPPred :: PredType -> 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,102 +616,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
-\end{code}
-
+isInheritablePred (ClassP _ _) = True
+isInheritablePred other             = False

 
 

-%************************************************************************
-%*                                                                     *
-\subsection{Comparison}
-%*                                                                     *
-%************************************************************************
-
-Comparison, taking note of newtypes, predicates, etc,
-But ignoring usage types
-
-\begin{code}
-tcEqType :: Type -> Type -> Bool
-tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
-
-tcEqPred :: PredType -> PredType -> Bool
-tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
-
--------------
-tcCmpType :: Type -> Type -> Ordering
-tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
-
-tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
-
-tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
--------------
-cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
-
--------------
-cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
-  -- The "env" maps type variables in ty1 to type variables in ty2
-  -- 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
-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
-                                         Just tv1a -> tv1a `compare` tv2
-                                         Nothing   -> tv1  `compare` tv2
-
-cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy 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 (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTy (extendVarEnv env tv1 tv2) t1 t2
-    
-    -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
-cmpTy env (AppTy _ _) (TyVarTy _) = GT
-    
-cmpTy env (FunTy _ _) (TyVarTy _) = GT
-cmpTy env (FunTy _ _) (AppTy _ _) = GT
-    
-cmpTy env (TyConApp _ _) (TyVarTy _) = GT
-cmpTy env (TyConApp _ _) (AppTy _ _) = GT
-cmpTy env (TyConApp _ _) (FunTy _ _) = GT
-    
-cmpTy env (ForAllTy _ _) (TyVarTy _)    = GT
-cmpTy env (ForAllTy _ _) (AppTy _ _)    = GT
-cmpTy env (ForAllTy _ _) (FunTy _ _)    = GT
-cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
-
-cmpTy env (SourceTy _)   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)
-       -- 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
-\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 }
+isLinearPred :: TcPredType -> Bool
+isLinearPred (IParam (Linear n) _) = True
+isLinearPred other                = False

 \end{code}
 
 
 \end{code}
 
 

@@ -600,30 +631,33 @@ 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
 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
 \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

@@ -638,77 +672,132 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 \end{code}
 
 
 \end{code}
 
 

+
+

 %************************************************************************
 %*                                                                     *
 %************************************************************************
 %*                                                                     *

-\subsection{Misc}
+               Hoisting for-alls

 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 

+hoistForAllTys is used for user-written type signatures only
+We want to 'look through' type synonyms when doing this
+so it's better done on the Type than the HsType
+
+It moves 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
+
+Also: it eliminates duplicate constraints.  These can show up
+when hoisting constraints, notably implicit parameters.
+
+It tries hard to retain type synonyms if hoisting does not break one
+up.  Not only does this improve error messages, but there's a tricky
+interaction with Haskell 98.  H98 requires no unsaturated type
+synonyms, which is checked by checkValidType.  This runs after
+hoisting, so we don't want hoisting to remove the SynNotes!  (We can't
+run validity checking before hoisting because in mutually-recursive
+type definitions we postpone validity checking until after the knot is
+tied.)
+

 \begin{code}
 hoistForAllTys :: Type -> Type
 \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
 hoistForAllTys ty

-  = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
+  = go (deShadowTy ty)
+       -- Running over ty with an empty substitution gives it the
+       -- no-shadowing property.  This is important.  For example:
+       --      type Foo r = forall a. a -> r
+       --      foo :: Foo (Foo ())
+       -- Here the hoisting should give
+       --      foo :: forall a a1. a -> a1 -> ()
+       --
+       -- What about type vars that are lexically in scope in the envt?
+       -- We simply rely on them having a different unique to any
+       -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
+       -- out of the envt, which is boring and (I think) not necessary.
+

   where
   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)
-              }}}
+    go (TyVarTy tv)               = TyVarTy tv
+    go (TyConApp tc tys)          = TyConApp tc (map go tys)
+    go (PredTy pred)              = PredTy pred    -- No nested foralls 
+    go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote (go ty1)) (go ty2)
+    go (NoteTy (FTVNote _) ty2)    = go ty2        -- Discard the free tyvar note
+    go (FunTy arg res)            = mk_fun_ty (go arg) (go res)
+    go (AppTy fun arg)            = AppTy (go fun) (go arg)
+    go (ForAllTy tv ty)                   = ForAllTy tv (go ty)
+
+       -- mk_fun_ty does all the work.  
+       -- It's building t1 -> t2: 
+       --      if t2 is a for-all type, push t1 inside it
+       --      if t2 is (pred -> t3), check for duplicates
+    mk_fun_ty ty1 ty2
+       | not (isSigmaTy ty2)           -- No forall's, or context => 
+       = FunTy ty1 ty2         
+       | PredTy p1 <- ty1              -- ty1 is a predicate
+       = if p1 `elem` theta then       -- so check for duplicates
+               ty2
+         else
+               mkSigmaTy tvs (p1:theta) tau
+       | otherwise     
+       = mkSigmaTy tvs theta (FunTy ty1 tau)
+       where
+         (tvs, theta, tau) = tcSplitSigmaTy ty2

 \end{code}
 
 
 \end{code}
 
 

+%************************************************************************
+%*                                                                     *
+\subsection{Misc}
+%*                                                                     *
+%************************************************************************
+

 \begin{code}
 deNoteType :: Type -> Type
 \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 ty@(TyVarTy tyvar)  = ty
 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)

-deNoteType (SourceTy p)                = SourceTy (deNoteSourceType p)
+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)
 deNoteType (NoteTy _ ty)       = deNoteType ty
 deNoteType (AppTy fun arg)     = AppTy (deNoteType fun) (deNoteType arg)
 deNoteType (FunTy fun arg)     = FunTy (deNoteType fun) (deNoteType arg)
 deNoteType (ForAllTy tv ty)    = ForAllTy tv (deNoteType ty)

-deNoteType (UsageTy u ty)      = UsageTy u (deNoteType ty)

 
 

-deNoteSourceType :: SourceType -> SourceType
-deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
-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}
 
 \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 (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
 -- 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}
 
 
 \end{code}
 
 

@@ -723,6 +812,10 @@ restricted set of types as arguments and results (the restricting factor
 being the )
 
 \begin{code}
 being the )
 
 \begin{code}

+isFFITy :: Type -> Bool
+-- True for any TyCon that can possibly be an arg or result of an FFI call
+isFFITy ty = checkRepTyCon legalFFITyCon ty
+

 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
 -- Checks for valid argument type for a 'foreign import'
 isFFIArgumentTy dflags safety ty 
 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
 -- Checks for valid argument type for a 'foreign import'
 isFFIArgumentTy dflags safety ty 

@@ -742,26 +835,89 @@ 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.  Manuel had:
+       --      newtype T = MkT (Ptr T)
+       -- and wanted it to work...

 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 +930,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,28 +939,29 @@ 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
 

+legalFFITyCon :: TyCon -> Bool
+-- True for any TyCon that can possibly be an arg or result of an FFI call
+legalFFITyCon tc
+  = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
+

 marshalableTyCon dflags tc
   =  (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
   || boxedMarshalableTyCon tc
 marshalableTyCon dflags tc
   =  (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
   || boxedMarshalableTyCon tc

@@ -817,294 +973,15 @@ 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}    

 
 

-
-%************************************************************************
-%*                                                                     *
-\subsection{Unification with an explicit substitution}
-%*                                                                     *
-%************************************************************************
-
-Unify types with an explicit substitution and no monad.
-Ignore usage annotations.
-
-\begin{code}
-type MySubst
-   = (TyVarSet,                -- Set of template tyvars
-      TyVarSubstEnv)   -- Not necessarily idempotent
-
-unifyTysX :: TyVarSet          -- Template tyvars
-         -> Type
-          -> Type
-          -> Maybe TyVarSubstEnv
-unifyTysX tmpl_tyvars ty1 ty2
-  = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
-
-unifyExtendTysX :: TyVarSet            -- Template tyvars
-               -> TyVarSubstEnv        -- Substitution to start with
-               -> Type
-               -> Type
-               -> Maybe TyVarSubstEnv  -- Extended substitution
-unifyExtendTysX tmpl_tyvars subst ty1 ty2
-  = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
-
-unifyTyListsX :: TyVarSet -> [Type] -> [Type]
-              -> Maybe TyVarSubstEnv
-unifyTyListsX tmpl_tyvars tys1 tys2
-  = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
-
-
-uTysX :: Type
-      -> Type
-      -> (MySubst -> Maybe result)
-      -> MySubst
-      -> Maybe result
-
-uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
-uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
-
-       -- Variables; go for uVar
-uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst 
-  | tyvar1 == tyvar2
-  = k subst
-uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
-  | tyvar1 `elemVarSet` tmpls
-  = uVarX tyvar1 ty2 k subst
-uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
-  | tyvar2 `elemVarSet` tmpls
-  = uVarX tyvar2 ty1 k subst
-
-       -- Predicates
-uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
-  | n1 == n2 = uTysX t1 t2 k subst
-uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (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 (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
-  | (con1 == con2 && equalLength tys1 tys2)
-  = uTyListsX tys1 tys2 k subst
-
-       -- Applications need a bit of care!
-       -- They can match FunTy and TyConApp, so use splitAppTy_maybe
-       -- NB: we've already dealt with type variables and Notes,
-       -- so if one type is an App the other one jolly well better be too
-uTysX (AppTy s1 t1) ty2 k subst
-  = case tcSplitAppTy_maybe ty2 of
-      Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
-      Nothing       -> Nothing    -- Fail
-
-uTysX ty1 (AppTy s2 t2) k subst
-  = case tcSplitAppTy_maybe ty1 of
-      Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
-      Nothing       -> Nothing    -- Fail
-
-       -- Not expecting for-alls in unification
-#ifdef DEBUG
-uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
-uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
-#endif
-
-       -- Ignore usages
-uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
-uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
-
-       -- Anything else fails
-uTysX ty1 ty2 k subst = Nothing
-
-
-uTyListsX []         []         k subst = k subst
-uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
-uTyListsX tys1      tys2       k subst = Nothing   -- Fail if the lists are different lengths
-\end{code}
-
-\begin{code}
--- Invariant: tv1 is a unifiable variable
-uVarX tv1 ty2 k subst@(tmpls, env)
-  = case lookupSubstEnv env tv1 of
-      Just (DoneTy ty1) ->    -- Already bound
-                    uTysX ty1 ty2 k subst
-
-      Nothing       -- Not already bound
-              |  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
-  where
-    occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
-    occur_check_ok_tv tv | tv1 == tv = False
-                        | otherwise = case lookupSubstEnv env tv of
-                                        Nothing           -> True
-                                        Just (DoneTy ty)  -> occur_check_ok ty
-\end{code}
-
-
-
-%************************************************************************
-%*                                                                     *
-\subsection{Matching on types}
-%*                                                                     *
-%************************************************************************
-
-Matching is a {\em unidirectional} process, matching a type against a
-template (which is just a type with type variables in it).  The
-matcher assumes that there are no repeated type variables in the
-template, so that it simply returns a mapping of type variables to
-types.  It also fails on nested foralls.
-
-@matchTys@ matches corresponding elements of a list of templates and
-types.  It and @matchTy@ both ignore usage annotations, unlike the
-main function @match@.
-
-\begin{code}
-matchTy :: TyVarSet                    -- Template tyvars
-       -> Type                         -- Template
-       -> Type                         -- Proposed instance of template
-       -> Maybe TyVarSubstEnv          -- Matching substitution
-                                       
-
-matchTys :: TyVarSet                   -- Template tyvars
-        -> [Type]                      -- Templates
-        -> [Type]                      -- Proposed instance of template
-        -> Maybe (TyVarSubstEnv,               -- Matching substitution
-                  [Type])              -- Left over instance types
-
-matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
-
-matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls 
-                                     (\ (senv,tys) -> Just (senv,tys))
-                                     emptySubstEnv
+isByteArrayLikeTyCon :: TyCon -> Bool
+isByteArrayLikeTyCon tc = 
+  getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]

 \end{code}
 
 \end{code}
 

-@match@ is the main function.  It takes a flag indicating whether
-usage annotations are to be respected.
-
-\begin{code}
-match :: Type -> Type                          -- Current match pair
-      -> TyVarSet                              -- Template vars
-      -> (TyVarSubstEnv -> Maybe result)       -- Continuation
-      -> TyVarSubstEnv                         -- Current subst
-      -> Maybe result
-
--- When matching against a type variable, see if the variable
--- has already been bound.  If so, check that what it's bound to
--- is the same as ty; if not, bind it and carry on.
-
-match (TyVarTy v) ty tmpls k senv
-  | v `elemVarSet` tmpls
-  =     -- v is a template variable
-    case lookupSubstEnv senv v of
-       Nothing -> UASSERT( not (isUTy ty) )
-                   k (extendSubstEnv senv v (DoneTy ty))
-       Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
-                          | otherwise           -> Nothing  -- Fails

 
 

-  | otherwise
-  =     -- v is not a template variable; ty had better match
-        -- Can't use (==) because types differ
-    case tcGetTyVar_maybe ty of
-        Just v' | v == v' -> k senv    -- Success
-        other            -> Nothing   -- Failure
-    -- This tcGetTyVar_maybe is *required* because it must strip Notes.
-    -- I guess the reason the Note-stripping case is *last* rather than first
-    -- is to preserve type synonyms etc., so I'm not moving it to the
-    -- top; but this means that (without the deNotetype) a type
-    -- variable may not match the pattern (TyVarTy v') as one would
-    -- expect, due to an intervening Note.  KSW 2000-06.
-
-       -- Predicates
-match (SourceTy (IParam n1 t1)) (SourceTy (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
-  | 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
-  = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
-
-match (AppTy fun1 arg1) ty2 tmpls k senv 
-  = case tcSplitAppTy_maybe ty2 of
-       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
-  | 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
-  | 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
-       -- here! (WDP 95/05)
-match (NoteTy n1 ty1) ty2      tmpls k senv = match ty1 ty2 tmpls k senv
-match ty1      (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
-
--- Catch-all fails
-match _ _ _ _ _ = Nothing
-
-match_list_exactly tys1 tys2 tmpls k senv
-  = match_list tys1 tys2 tmpls k' senv
-  where
-    k' (senv', tys2') | null tys2' = k senv'   -- Succeed
-                     | otherwise  = Nothing    -- Fail 
-
-match_list []         tys2       tmpls k senv = k (senv, tys2)
-match_list (ty1:tys1) []         tmpls k senv = Nothing        -- Not enough arg tys => failure
-match_list (ty1:tys1) (ty2:tys2) tmpls k senv
-  = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv
-\end{code}