[project @ 2005-03-01 21:40:40 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index 54cb451..b9ff393 100644 (file)
-%
+
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcType]{Types used in the typechecker}
 
-\begin{code}
-module TcType (
-  
-  TcTyVar, TcBox,
-  TcTyVarSet,
-  newTcTyVar,
-  newTyVarTy,  -- Kind -> NF_TcM s (TcType s)
-  newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
-
-  -----------------------------------------
-  TcType, TcMaybe(..),
-  TcTauType, TcThetaType, TcRhoType,
-
-       -- Find the type to which a type variable is bound
-  tcWriteTyVar,                -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
-  tcReadTyVar,         -- :: TcTyVar s -> NF_TcM (TcMaybe s)
+This module provides the Type interface for front-end parts of the 
+compiler.  These parts 
 
+       * treat "source types" as opaque: 
+               newtypes, and predicates are meaningful. 
+       * look through usage types
 
-  tcSplitRhoTy,
+The "tc" prefix is for "typechechecker", because the type checker
+is the principal client.
 
-  tcInstTyVars,
-  tcInstTcType,
+\begin{code}
+module TcType (
+  --------------------------------
+  -- Types 
+  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
+  TcTyVar, TcTyVarSet, TcKind, 
 
-  typeToTcType,
+  --------------------------------
+  -- MetaDetails
+  Expected(..), TcRef, TcTyVarDetails(..),
+  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+  isFlexi, isIndirect, 
 
   --------------------------------
-  TcKind,
-  newKindVar, newKindVars,
-  kindToTcKind,
-  zonkTcKind,
+  -- Builders
+  mkPhiTy, mkSigmaTy, hoistForAllTys,
 
   --------------------------------
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
-  zonkTcType, zonkTcTypes, zonkTcThetaType,
+  -- Splitters  
+  -- These are important because they do not look through newtypes
+  tcSplitForAllTys, tcSplitPhiTy, 
+  tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
+  tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
+  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
+  tcGetTyVar_maybe, tcGetTyVar,
+
+  ---------------------------------
+  -- Predicates. 
+  -- Again, newtypes are opaque
+  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
+  isSigmaTy, isOverloadedTy, 
+  isDoubleTy, isFloatTy, isIntTy,
+  isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
+  isTauTy, tcIsTyVarTy, tcIsForAllTy,
+
+  ---------------------------------
+  -- Misc type manipulators
+  deNoteType, classesOfTheta,
+  tyClsNamesOfType, tyClsNamesOfDFunHead, 
+  getDFunTyKey,
+
+  ---------------------------------
+  -- Predicate types  
+  getClassPredTys_maybe, getClassPredTys, 
+  isClassPred, isTyVarClassPred, 
+  mkDictTy, tcSplitPredTy_maybe, 
+  isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
+  mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
+
+  ---------------------------------
+  -- Foreign import and export
+  isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
+  isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
+  isFFIExportResultTy, -- :: Type -> Bool
+  isFFIExternalTy,     -- :: Type -> Bool
+  isFFIDynArgumentTy,  -- :: Type -> Bool
+  isFFIDynResultTy,    -- :: Type -> Bool
+  isFFILabelTy,        -- :: Type -> Bool
+  isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
+  isFFIDotnetObjTy,    -- :: Type -> Bool
+  isFFITy,            -- :: Type -> Bool
+  
+  toDNType,            -- :: Type -> DNType
 
-  zonkTcTypeToType, zonkTcTyVarToTyVar,
-  zonkTcKindToKind
+  --------------------------------
+  -- Rexported from Type
+  Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
+  unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
+  isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, 
+  isArgTypeKind, isSubKind, defaultKind, 
+
+  Type, PredType(..), ThetaType, 
+  mkForAllTy, mkForAllTys, 
+  mkFunTy, mkFunTys, zipFunTys, 
+  mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+  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
+  isPrimitiveType, 
+
+  tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
+  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
+  typeKind, 
+
+  tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
+
+  pprKind, pprParendKind,
+  pprType, pprParendType, pprTyThingCategory,
+  pprPred, pprTheta, pprThetaArrow, pprClassPred
 
   ) where
 
 #include "HsVersions.h"
 
-
 -- friends:
-import PprType         ()
-import Type            ( Type, Kind, ThetaType, GenType(..), TyNote(..), 
-                         mkAppTy,
-                         splitDictTy_maybe, splitForAllTys,
-                         isTyVarTy, mkTyVarTys, 
-                         fullSubstTy, substFlexiTy, 
-                         boxedTypeKind, superKind
-                       )
-import VarEnv
-import VarSet          ( emptyVarSet )
-import Var             ( TyVar, GenTyVar, tyVarKind, tyVarFlexi, tyVarName,
-                         mkFlexiTyVar, removeTyVarFlexi, isFlexiTyVar, isTyVar
+import TypeRep         ( Type(..), TyNote(..), funTyCon )  -- friend
+
+import Type            (       -- Re-exports
+                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
+                         tyVarsOfTheta, Kind, PredType(..),
+                         ThetaType, unliftedTypeKind, 
+                         liftedTypeKind, openTypeKind, mkArrowKind,
+                         isLiftedTypeKind, isUnliftedTypeKind, 
+                         mkArrowKinds, mkForAllTy, mkForAllTys,
+                         defaultKind, isArgTypeKind, isOpenTypeKind,
+                         mkFunTy, mkFunTys, zipFunTys, 
+                         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, 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 TcMonad
-import Name            ( changeUnique )
-
-import TysWiredIn      ( voidTy )
-
-import Name            ( NamedThing(..), changeUnique, mkSysLocalName )
-import Unique          ( Unique )
-import Util            ( nOfThem )
+import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
+import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
+import NameSet
+import VarEnv          ( TidyEnv )
+import OccName         ( OccName, mkDictOcc )
+import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
+import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
+import BasicTypes      ( IPName(..), ipNameName )
+import SrcLoc          ( SrcLoc, SrcSpan )
+import Util            ( snocView )
+import Maybes          ( maybeToBool, expectJust )
 import Outputable
+import DATA_IOREF
 \end{code}
 
 
+%************************************************************************
+%*                                                                     *
+\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
 
-Data types
-~~~~~~~~~~
-See TcMonad.lhs
+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}
-tcTyVarToTyVar :: TcTyVar s -> TyVar
-tcTyVarToTyVar = removeTyVarFlexi
+type TcType = Type             -- A TcType can have mutable type variables
+       -- Invariant on ForAllTy in TcTypes:
+       --      forall a. T
+       -- a cannot occur inside a MutTyVar in T; that is,
+       -- T is "flattened" before quantifying over a
+
+type TcPredType     = PredType
+type TcThetaType    = ThetaType
+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}
 
-Utility functions
-~~~~~~~~~~~~~~~~~
-These tcSplit functions are like their non-Tc analogues, but they
-follow through bound type variables.
 
-No need for tcSplitForAllTy because a type variable can't be instantiated
-to a for-all type.
+%************************************************************************
+%*                                                                     *
+\subsection{TyVarDetails}
+%*                                                                     *
+%************************************************************************
+
+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}
-tcSplitRhoTy :: TcType s -> NF_TcM s (TcThetaType s, TcType s)
-tcSplitRhoTy t
-  = go t t []
- where
-       -- A type variable is never instantiated to a dictionary type,
-       -- so we don't need to do a tcReadVar on the "arg".
-    go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
-                                       Just pair -> go res res (pair:ts)
-                                       Nothing   -> returnNF_Tc (reverse ts, syn_t)
-    go syn_t (NoteTy _ t)    ts = go syn_t t ts
-    go syn_t (TyVarTy tv)    ts = tcReadTyVar tv       `thenNF_Tc` \ maybe_ty ->
-                                 case maybe_ty of
-                                   BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
-                                   other                           -> returnNF_Tc (reverse ts, syn_t)
-    go syn_t t              ts = returnNF_Tc (reverse ts, syn_t)
+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}
 
 
-New type variables
-~~~~~~~~~~~~~~~~~~
+%************************************************************************
+%*                                                                     *
+\subsection{Tau, sigma and rho}
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
-newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
-newTcTyVar kind
-  = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutVar UnBound        `thenNF_Tc` \ box ->
-    let
-       name = mkSysLocalName uniq
-    in
-    returnNF_Tc (mkFlexiTyVar name kind box)
-
-newTyVarTy  :: Kind -> NF_TcM s (TcType s)
-newTyVarTy kind
-  = newTcTyVar kind    `thenNF_Tc` \ tc_tyvar ->
-    returnNF_Tc (TyVarTy tc_tyvar)
-
-newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
-newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
-
-newKindVar :: NF_TcM s (TcKind s)
-newKindVar = newTyVarTy superKind
-
-newKindVars :: Int -> NF_TcM s [TcKind s]
-newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
+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}
 
-Type instantiation
-~~~~~~~~~~~~~~~~~~
+@isTauTy@ tests for nested for-alls.
 
-Instantiating a bunch of type variables
+\begin{code}
+isTauTy :: Type -> Bool
+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 (PredTy p)      = True         -- Don't look through source types
+isTauTy (NoteTy _ ty)   = isTauTy ty
+isTauTy other           = False
+\end{code}
 
 \begin{code}
-tcInstTyVars :: [GenTyVar flexi] 
-            -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s))
-
-tcInstTyVars tyvars
-  = mapNF_Tc inst_tyvar tyvars `thenNF_Tc` \ tc_tyvars ->
-    let
-       tys = mkTyVarTys tc_tyvars
-    in
-    returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
-
-inst_tyvar tyvar       -- Could use the name from the tyvar?
-  = tcGetUnique                `thenNF_Tc` \ uniq ->
-    tcNewMutVar UnBound                `thenNF_Tc` \ box ->
-    let
-       name = changeUnique (tyVarName tyvar) uniq
-       -- Note that we don't change the print-name
-       -- This won't confuse the type checker but there's a chance
-       -- that two different tyvars will print the same way 
-       -- in an error message.  -dppr-debug will show up the difference
-       -- Better watch out for this.  If worst comes to worst, just
-       -- use mkSysLocalName.
-    in
-    returnNF_Tc (mkFlexiTyVar name (tyVarKind tyvar) box)
+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 ty                     = pprPanic "getDFunTyKey" (pprType ty)
+-- PredTy shouldn't happen
 \end{code}
 
-@tcInstTcType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, returning them and the instantiated body of the for-all.
 
+%************************************************************************
+%*                                                                     *
+\subsection{Expanding and splitting}
+%*                                                                     *
+%************************************************************************
+
+These tcSplit functions are like their non-Tc analogues, but
+       a) they do not look through newtypes
+       b) they do not look through PredTys
+       c) [future] they ignore usage-type annotations
+
+However, they are non-monadic and do not follow through mutable type
+variables.  It's up to you to make sure this doesn't matter.
 
 \begin{code}
-tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
-tcInstTcType ty
-  = let
-       (tyvars, rho) = splitForAllTys ty
-    in
-    case tyvars of
-       []    -> returnNF_Tc ([], ty)   -- Nothing to do
-       other -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
-                returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho)
-                                       -- Since the tyvars are freshly made,
-                                       -- they cannot possibly be captured by
-                                       -- any existing for-alls.  Hence emptyVarSet
+tcSplitForAllTys :: Type -> ([TyVar], Type)
+tcSplitForAllTys ty = split ty ty []
+   where
+     split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
+     split orig_ty (NoteTy n  ty)   tvs = split orig_ty ty tvs
+     split orig_ty t               tvs = (reverse tvs, orig_ty)
+
+tcIsForAllTy (ForAllTy tv ty) = True
+tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
+tcIsForAllTy t               = False
+
+tcSplitPhiTy :: Type -> ([PredType], Type)
+tcSplitPhiTy ty = split ty ty []
+ where
+  split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
+                                       Just p  -> split res res (p:ts)
+                                       Nothing -> (reverse ts, orig_ty)
+  split orig_ty (NoteTy n ty)  ts = split orig_ty ty ts
+  split orig_ty ty             ts = (reverse ts, orig_ty)
+
+tcSplitSigmaTy ty = case tcSplitForAllTys ty of
+                       (tvs, rho) -> case tcSplitPhiTy rho of
+                                       (theta, tau) -> (tvs, theta, tau)
+
+tcTyConAppTyCon :: Type -> TyCon
+tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
+
+tcTyConAppArgs :: Type -> [Type]
+tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
+
+tcSplitTyConApp :: Type -> (TyCon, [Type])
+tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
+                       Just stuff -> stuff
+                       Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
+
+tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+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
+
+tcSplitFunTys :: Type -> ([Type], Type)
+tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
+                       Nothing        -> ([], ty)
+                       Just (arg,res) -> (arg:args, res')
+                                      where
+                                         (args,res') = tcSplitFunTys res
+
+tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
+tcSplitFunTy_maybe (NoteTy n ty)    = tcSplitFunTy_maybe ty
+tcSplitFunTy_maybe other           = Nothing
+
+tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
+tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
+
+
+tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
+tcSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
+tcSplitAppTy_maybe (NoteTy n ty)     = tcSplitAppTy_maybe ty
+tcSplitAppTy_maybe (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)
+
+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 other         = Nothing
+
+tcGetTyVar :: String -> Type -> TyVar
+tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
+
+tcIsTyVarTy :: Type -> Bool
+tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
+
+tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
+-- Split the type of a dictionary function
+tcSplitDFunTy ty 
+  = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
+    case tcSplitDFunHead tau of { (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}
 
-Sometimes we have to convert a Type to a TcType.  I wonder whether we could
-do this less than we do?
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Predicate types}
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
-typeToTcType :: Type -> TcType s
-typeToTcType t = substFlexiTy emptyVarEnv t
+tcSplitPredTy_maybe :: Type -> Maybe PredType
+   -- Returns Just for predicates only
+tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
+tcSplitPredTy_maybe (PredTy p)    = Just p
+tcSplitPredTy_maybe other        = Nothing
+       
+predTyUnique :: PredType -> Unique
+predTyUnique (IParam n _)      = getUnique (ipNameName n)
+predTyUnique (ClassP clas tys) = getUnique clas
 
-kindToTcKind :: Kind -> TcKind s
-kindToTcKind = typeToTcType
+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}
 
 
-Reading and writing TcTyVars
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--------------------- Dictionary types ---------------------------------
+
 \begin{code}
-tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
-tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
+mkClassPred clas tys = ClassP clas tys
+
+isClassPred :: PredType -> Bool
+isClassPred (ClassP clas tys) = True
+isClassPred other            = False
+
+isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
+isTyVarClassPred other            = False
+
+getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
+getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
+getClassPredTys_maybe _                        = Nothing
+
+getClassPredTys :: PredType -> (Class, [Type])
+getClassPredTys (ClassP clas tys) = (clas, tys)
+
+mkDictTy :: Class -> [Type] -> Type
+mkDictTy clas tys = mkPredTy (ClassP clas tys)
+
+isDictTy :: Type -> Bool
+isDictTy (PredTy p)   = isClassPred p
+isDictTy (NoteTy _ ty) = isDictTy ty
+isDictTy other         = False
 \end{code}
 
-Writing is easy:
+--------------------- Implicit parameters ---------------------------------
 
 \begin{code}
-tcWriteTyVar tyvar ty = tcWriteMutVar (tyVarFlexi tyvar) (BoundTo ty)
+isIPPred :: PredType -> Bool
+isIPPred (IParam _ _) = True
+isIPPred other       = False
+
+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, 
+--               g 4 with ?v = 9)
+-- The point is that g's type must be quantifed over ?v:
+--     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
+isInheritablePred (ClassP _ _) = True
+isInheritablePred other             = False
+
+isLinearPred :: TcPredType -> Bool
+isLinearPred (IParam (Linear n) _) = True
+isLinearPred other                = False
 \end{code}
 
-Reading is more interesting.  The easy thing to do is just to read, thus:
-\begin{verbatim}
-tcReadTyVar tyvar = tcReadMutVar (tyVarFlexi tyvar)
-\end{verbatim}
 
-But it's more fun to short out indirections on the way: If this
-version returns a TyVar, then that TyVar is unbound.  If it returns
-any other type, then there might be bound TyVars embedded inside it.
+%************************************************************************
+%*                                                                     *
+\subsection{Predicates}
+%*                                                                     *
+%************************************************************************
 
-We return Nothing iff the original box was unbound.
+isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have 
+any foralls.  E.g.
+       f :: (?x::Int) => Int -> Int
 
 \begin{code}
-tcReadTyVar tyvar
-  = tcReadMutVar box   `thenNF_Tc` \ maybe_ty ->
-    case maybe_ty of
-       BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
-                     tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
-                     returnNF_Tc (BoundTo ty')
-
-       other      -> returnNF_Tc other
-  where
-    box = tyVarFlexi tyvar
+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 _                  = 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}
 
-short_out :: TcType s -> NF_TcM s (TcType s)
-short_out ty@(TyVarTy tyvar)
-  = tcReadMutVar box   `thenNF_Tc` \ maybe_ty ->
-    case maybe_ty of
-       BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
-                      tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
-                      returnNF_Tc ty'
+\begin{code}
+isFloatTy      = is_tc floatTyConKey
+isDoubleTy     = is_tc doubleTyConKey
+isIntegerTy    = is_tc integerTyConKey
+isIntTy        = is_tc intTyConKey
+isAddrTy       = is_tc addrTyConKey
+isBoolTy       = is_tc boolTyConKey
+isUnitTy       = is_tc unitTyConKey
+
+is_tc :: Unique -> Type -> Bool
+-- Newtypes are opaque to this
+is_tc uniq ty = case tcSplitTyConApp_maybe ty of
+                       Just (tc, _) -> uniq == getUnique tc
+                       Nothing      -> False
+\end{code}
 
-       other       -> returnNF_Tc ty
-  where
-    box = tyVarFlexi tyvar
 
-short_out other_ty = returnNF_Tc other_ty
+
+
+%************************************************************************
+%*                                                                     *
+               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
+hoistForAllTys ty
+  = 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
+    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}
 
 
-Zonking Tc types to Tc types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+%************************************************************************
+%*                                                                     *
+\subsection{Misc}
+%*                                                                     *
+%************************************************************************
+
 \begin{code}
-zonkTcTyVars :: [TcTyVar s] -> NF_TcM s [TcType s]
-zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
-
-zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
-zonkTcTyVar tyvar 
-  | not (isFlexiTyVar tyvar)   -- Not a flexi tyvar.  This can happen when
-                               -- zonking a forall type, when the bound type variable
-                               -- needn't be a flexi.
-  = ASSERT( isTyVar tyvar )
-    returnNF_Tc (TyVarTy tyvar)
-
-  | otherwise  -- Is a flexi tyvar
-  = tcReadTyVar tyvar          `thenNF_Tc` \ maybe_ty ->
-    case maybe_ty of
-       BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty           -- tcReadTyVar never returns a bound tyvar
-       BoundTo other               -> zonkTcType other
-       other                       -> returnNF_Tc (TyVarTy tyvar)
-
-zonkTcTyVarBndr :: TcTyVar s -> NF_TcM s (TcTyVar s)
-zonkTcTyVarBndr tyvar
-  = zonkTcTyVar tyvar  `thenNF_Tc` \ (TyVarTy tyvar') ->
-    returnNF_Tc tyvar'
-       
-zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s]
-zonkTcTypes tys = mapNF_Tc zonkTcType tys
-
-zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s)
-zonkTcThetaType theta = mapNF_Tc zonk theta
-                   where
-                     zonk (c,ts) = zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
-                                   returnNF_Tc (c, new_ts)
-
-zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
-zonkTcKind = zonkTcType
-
-zonkTcType :: TcType s -> NF_TcM s (TcType s)
-
-zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
-
-zonkTcType (AppTy ty1 ty2)
-  = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
-    zonkTcType ty2             `thenNF_Tc` \ ty2' ->
-    returnNF_Tc (mkAppTy ty1' ty2')
-
-zonkTcType (TyConApp tc tys)
-  = mapNF_Tc zonkTcType tys    `thenNF_Tc` \ tys' ->
-    returnNF_Tc (TyConApp tc tys')
-
-zonkTcType (NoteTy (SynNote ty1) ty2)
-  = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
-    zonkTcType ty2             `thenNF_Tc` \ ty2' ->
-    returnNF_Tc (NoteTy (SynNote ty1') ty2')
-
-zonkTcType (NoteTy (FTVNote _) ty2) = zonkTcType ty2
-
-zonkTcType (ForAllTy tv ty)
-  = zonkTcTyVar tv             `thenNF_Tc` \ tv_ty ->
-    zonkTcType ty              `thenNF_Tc` \ ty' ->
-    case tv_ty of      -- Should be a tyvar!
-      TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty')
-      _ -> panic "zonkTcType"
-          -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $
-          -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
-
-zonkTcType (FunTy ty1 ty2)
-  = zonkTcType ty1             `thenNF_Tc` \ ty1' ->
-    zonkTcType ty2             `thenNF_Tc` \ ty2' ->
-    returnNF_Tc (FunTy ty1' ty2')
+deNoteType :: Type -> Type
+       -- Remove synonyms, but not predicate types
+deNoteType ty@(TyVarTy tyvar)  = ty
+deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
+deNoteType (PredTy p)          = PredTy (deNotePredType p)
+deNoteType (NoteTy _ ty)       = deNoteType ty
+deNoteType (AppTy fun arg)     = AppTy (deNoteType fun) (deNoteType arg)
+deNoteType (FunTy fun arg)     = FunTy (deNoteType fun) (deNoteType arg)
+deNoteType (ForAllTy tv ty)    = ForAllTy tv (deNoteType ty)
+
+deNotePredType :: PredType -> PredType
+deNotePredType (ClassP c tys)   = ClassP c (map deNoteType tys)
+deNotePredType (IParam n ty)    = IParam n (deNoteType ty)
 \end{code}
 
-Zonking Tc types to Type/Kind
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Find the free tycons and classes of a type.  This is used in the front
+end of the compiler.
+
 \begin{code}
-zonkTcKindToKind :: TcKind s -> NF_TcM s Kind
-zonkTcKindToKind kind = zonkTcToType boxedTypeKind emptyVarEnv kind
+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
+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}
 
-zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
-zonkTcTypeToType env ty = zonkTcToType voidTy env ty
 
-zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
-zonkTcTyVarToTyVar tv
-  = zonkTcTyVarBndr tv `thenNF_Tc` \ tv' ->
-    returnNF_Tc (tcTyVarToTyVar tv')
+%************************************************************************
+%*                                                                     *
+\subsection[TysWiredIn-ext-type]{External types}
+%*                                                                     *
+%************************************************************************
 
--- zonkTcToType is used for Kinds as well
-zonkTcToType :: Type -> TyVarEnv Type -> TcType s -> NF_TcM s Type
-zonkTcToType unbound_var_ty env ty
-  = go ty
-  where
-    go (TyConApp tycon tys)      = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
-                                   returnNF_Tc (TyConApp tycon tys')
+The compiler's foreign function interface supports the passing of a
+restricted set of types as arguments and results (the restricting factor
+being the )
 
-    go (NoteTy (SynNote ty1) ty2) = go ty1             `thenNF_Tc` \ ty1' ->
-                                   go ty2              `thenNF_Tc` \ ty2' ->
-                                   returnNF_Tc (NoteTy (SynNote ty1') ty2')
+\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 
+   = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
+
+isFFIExternalTy :: Type -> Bool
+-- Types that are allowed as arguments of a 'foreign export'
+isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
+
+isFFIImportResultTy :: DynFlags -> Type -> Bool
+isFFIImportResultTy dflags ty 
+  = checkRepTyCon (legalFIResultTyCon dflags) ty
+
+isFFIExportResultTy :: Type -> Bool
+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 = 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 = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
+
+isFFILabelTy :: Type -> Bool
+-- The type of a foreign label must be Ptr, FunPtr, Addr,
+-- or a newtype of either.
+isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
+
+isFFIDotnetTy :: DynFlags -> Type -> Bool
+isFFIDotnetTy dflags ty
+  = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
+                          (legalFIResultTyCon dflags tc || 
+                          isFFIDotnetObjTy ty || isStringTy ty)) ty
+
+-- Support String as an argument or result from a .NET FFI call.
+isStringTy ty = 
+  case tcSplitTyConApp_maybe (repType ty) of
+    Just (tc, [arg_ty])
+      | tc == listTyCon ->
+        case tcSplitTyConApp_maybe (repType arg_ty) of
+         Just (cc,[]) -> cc == charTyCon
+         _ -> False
+    _ -> False
+
+-- Support String as an argument or result from a .NET FFI call.
+isFFIDotnetObjTy ty = 
+  let
+   (_, t_ty) = tcSplitForAllTys ty
+  in
+  case tcSplitTyConApp_maybe (repType t_ty) of
+    Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
+    _ -> False
+
+toDNType :: Type -> DNType
+toDNType ty
+  | isStringTy ty = DNString
+  | isFFIDotnetObjTy ty = DNObject
+  | Just (tc,argTys) <- tcSplitTyConApp_maybe ty = 
+     case lookup (getUnique tc) dn_assoc of
+       Just x  -> x
+       Nothing 
+         | tc `hasKey` ioTyConKey -> toDNType (head argTys)
+        | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
+    where
+      dn_assoc :: [ (Unique, DNType) ]
+      dn_assoc = [ (unitTyConKey,   DNUnit)
+                , (intTyConKey,    DNInt)
+                , (int8TyConKey,   DNInt8)
+                , (int16TyConKey,  DNInt16)
+                , (int32TyConKey,  DNInt32)
+                , (int64TyConKey,  DNInt64)
+                , (wordTyConKey,   DNInt)
+                , (word8TyConKey,  DNWord8)
+                , (word16TyConKey, DNWord16)
+                , (word32TyConKey, DNWord32)
+                , (word64TyConKey, DNWord64)
+                , (floatTyConKey,  DNFloat)
+                , (doubleTyConKey, DNDouble)
+                , (addrTyConKey,   DNPtr)
+                , (ptrTyConKey,    DNPtr)
+                , (funPtrTyConKey, DNPtr)
+                , (charTyConKey,   DNChar)
+                , (boolTyConKey,   DNBool)
+                ]
+
+checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
+       -- Look through newtypes
+       -- Non-recursive ones are transparent to splitTyConApp,
+       -- but recursive ones aren't.  Manuel had:
+       --      newtype T = MkT (Ptr T)
+       -- and wanted it to work...
+checkRepTyCon check_tc ty 
+  | 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}
 
-    go (NoteTy (FTVNote _) ty2)   = go ty2     -- Discard free-tyvar annotations
+----------------------------------------------
+These chaps do the work; they are not exported
+----------------------------------------------
 
-    go (FunTy arg res)           = go arg              `thenNF_Tc` \ arg' ->
-                                   go res              `thenNF_Tc` \ res' ->
-                                   returnNF_Tc (FunTy arg' res')
-    go (AppTy fun arg)           = go fun              `thenNF_Tc` \ fun' ->
-                                   go arg              `thenNF_Tc` \ arg' ->
-                                   returnNF_Tc (mkAppTy fun' arg')
-
-       -- The two interesting cases!
-       -- c.f. zonkTcTyVar
-    go (TyVarTy tyvar)  
-       | not (isFlexiTyVar tyvar) = lookup env tyvar
-
-       | otherwise     =  tcReadTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
-                          case maybe_ty of
-                             BoundTo (TyVarTy tyvar') -> lookup env tyvar'
-                             BoundTo other_ty         -> go other_ty
-                             other                    -> lookup env tyvar
-
-    go (ForAllTy tyvar ty)
-       = zonkTcTyVarToTyVar tyvar      `thenNF_Tc` \ tyvar' ->
-         let
-            new_env = extendVarEnv env tyvar (TyVarTy tyvar')
-         in
-         zonkTcToType unbound_var_ty new_env ty        `thenNF_Tc` \ ty' ->
-         returnNF_Tc (ForAllTy tyvar' ty')
-
-
-    lookup env tyvar = returnNF_Tc (case lookupVarEnv env tyvar of
-                                         Just ty -> ty
-                                         Nothing -> unbound_var_ty)
+\begin{code}
+legalFEArgTyCon :: TyCon -> Bool
+-- It's illegal to return foreign objects and (mutable)
+-- bytearrays from a _ccall_ / foreign declaration
+-- (or be passed them as arguments in foreign exported functions).
+legalFEArgTyCon tc
+  | 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
+  | otherwise
+  = boxedMarshalableTyCon tc
+
+legalFIResultTyCon :: DynFlags -> TyCon -> Bool
+legalFIResultTyCon dflags tc
+  | isByteArrayLikeTyCon tc = False
+  | tc == unitTyCon         = True
+  | otherwise              = marshalableTyCon dflags tc
+
+legalFEResultTyCon :: TyCon -> Bool
+legalFEResultTyCon tc
+  | isByteArrayLikeTyCon tc = False
+  | tc == unitTyCon         = True
+  | otherwise               = boxedMarshalableTyCon tc
+
+legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
+-- Checks validity of types going from Haskell -> external world
+legalOutgoingTyCon dflags safety tc
+  | playSafe safety && isByteArrayLikeTyCon 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
+
+boxedMarshalableTyCon tc
+   = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
+                        , int32TyConKey, int64TyConKey
+                        , wordTyConKey, word8TyConKey, word16TyConKey
+                        , word32TyConKey, word64TyConKey
+                        , floatTyConKey, doubleTyConKey
+                        , addrTyConKey, ptrTyConKey, funPtrTyConKey
+                        , charTyConKey
+                        , stablePtrTyConKey
+                        , byteArrayTyConKey, mutableByteArrayTyConKey
+                        , boolTyConKey
+                        ]
+
+isByteArrayLikeTyCon :: TyCon -> Bool
+isByteArrayLikeTyCon tc = 
+  getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
 \end{code}