fix haddock submodule pointer
[ghc-hetmet.git] / compiler / typecheck / TcType.lhs
index c10c2eb..a825d23 100644 (file)
@@ -1,4 +1,5 @@
-
+%
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcType]{Types used in the typechecker}
@@ -18,18 +19,17 @@ module TcType (
   --------------------------------
   -- Types 
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
-  TcTyVar, TcTyVarSet, TcKind, 
-
-  BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,
+  TcCoercion, TcTyVar, TcTyVarSet, TcKind, TcCoVar,
 
   --------------------------------
   -- MetaDetails
   UserTypeCtxt(..), pprUserTypeCtxt,
-  TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
-  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
-  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, isSigTyVar, isExistentialTyVar, 
+  TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
+  MetaDetails(Flexi, Indirect), MetaInfo(..), 
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy,
+  isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
   metaTvRef, 
-  isFlexi, isIndirect, 
+  isFlexi, isIndirect, isRuntimeUnkSkol,
 
   --------------------------------
   -- Builders
@@ -39,37 +39,43 @@ module TcType (
   -- Splitters  
   -- These are important because they do not look through newtypes
   tcView,
-  tcSplitForAllTys, tcSplitPhiTy, 
+  tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
-  tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
-  tcSplitSigmaTy, tcMultiSplitSigmaTy, 
+  tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
+  tcGetTyVar_maybe, tcGetTyVar,
+  tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe, 
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
-  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
+  eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
   eqKind, 
-  isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
-  isDoubleTy, isFloatTy, isIntTy, isStringTy,
-  isIntegerTy, isBoolTy, isUnitTy,
+  isSigmaTy, isOverloadedTy,
+  isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
+  isIntegerTy, isBoolTy, isUnitTy, isCharTy,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, 
+  isSynFamilyTyConApp,
 
   ---------------------------------
   -- Misc type manipulators
-  deNoteType, classesOfTheta,
-  tyClsNamesOfType, tyClsNamesOfDFunHead, 
+  deNoteType,
+  orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo,
   getDFunTyKey,
 
   ---------------------------------
   -- Predicate types  
-  getClassPredTys_maybe, getClassPredTys, 
-  isClassPred, isTyVarClassPred, isEqPred, 
-  mkDictTy, tcSplitPredTy_maybe, 
-  isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
-  mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
-  dataConsStupidTheta, isRefineableTy,
+  mkMinimalBySCs, transSuperClasses, immSuperClasses,
+
+  -- * Tidying type related things up for printing
+  tidyType,      tidyTypes,
+  tidyOpenType,  tidyOpenTypes,
+  tidyTyVarBndr, tidyFreeTyVars,
+  tidyOpenTyVar, tidyOpenTyVars,
+  tidyTopType,   tidyPred,
+  tidyKind, 
+  tidyCo, tidyCos,
 
   ---------------------------------
   -- Foreign import and export
@@ -79,123 +85,93 @@ module TcType (
   isFFIExternalTy,     -- :: Type -> Bool
   isFFIDynArgumentTy,  -- :: Type -> Bool
   isFFIDynResultTy,    -- :: Type -> Bool
+  isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
+  isFFIPrimResultTy,   -- :: DynFlags -> Type -> Bool
   isFFILabelTy,        -- :: Type -> Bool
   isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
   isFFIDotnetObjTy,    -- :: Type -> Bool
   isFFITy,            -- :: Type -> Bool
+  isFunPtrTy,          -- :: Type -> Bool
   tcSplitIOType_maybe, -- :: Type -> Maybe Type  
-  toDNType,            -- :: Type -> DNType
 
   --------------------------------
-  -- Rexported from Type
-  Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
+  -- Rexported from Kind
+  Kind, typeKind,
   unliftedTypeKind, liftedTypeKind, argTypeKind,
   openTypeKind, mkArrowKind, mkArrowKinds, 
   isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind, 
-  isSubArgTypeKind, isSubKind, defaultKind,
+  isSubArgTypeKind, isSubKind, splitKindFunTys, defaultKind,
   kindVarRef, mkKindVar,  
 
-  Type, PredType(..), ThetaType, 
+  --------------------------------
+  -- Rexported from Type
+  Type, Pred(..), PredType, ThetaType,
   mkForAllTy, mkForAllTys, 
   mkFunTy, mkFunTys, zipFunTys, 
   mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, 
 
+  getClassPredTys_maybe, getClassPredTys, 
+  isClassPred, isTyVarClassPred, isEqPred, 
+  mkClassPred, mkIPPred, splitPredTy_maybe, 
+  mkDictTy, isPredTy, isDictTy, isDictLikeTy,
+  tcSplitDFunTy, tcSplitDFunHead, 
+  isIPPred, mkEqPred,
+
   -- Type substitutions
   TvSubst(..),         -- Representation visible to a few friends
-  TvSubstEnv, emptyTvSubst, substEqSpec,
-  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
-  getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
-  extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
-  substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
+  TvSubstEnv, emptyTvSubst, 
+  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, 
+  mkTopTvSubst, notElemTvSubst, unionTvSubst,
+  getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, 
+  Type.lookupTyVar, Type.extendTvSubst, Type.substTyVarBndr,
+  extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
+  Type.substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars, 
 
   isUnLiftedType,      -- Source types are always lifted
   isUnboxedTupleType,  -- Ditto
   isPrimitiveType, 
 
-  tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
-  typeKind, tidyKind,
-
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-  tcTyVarsOfType, tcTyVarsOfTypes, exactTyVarsOfType, exactTyVarsOfTypes,
+  tcTyVarsOfType, tcTyVarsOfTypes, tcTyVarsOfPred, exactTyVarsOfType,
+  exactTyVarsOfTypes, 
 
   pprKind, pprParendKind,
-  pprType, pprParendType, pprTyThingCategory,
-  pprPred, pprTheta, pprThetaArrow, pprClassPred
+  pprType, pprParendType, pprTypeApp, pprTyThingCategory,
+  pprPred, pprTheta, pprThetaArrow, pprThetaArrowTy, pprClassPred
 
   ) where
 
 #include "HsVersions.h"
 
 -- friends:
-import TypeRep         ( Type(..), funTyCon, Kind )  -- friend
-
-import Type            (       -- Re-exports
-                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
-                         tyVarsOfTheta, Kind, PredType(..), KindVar,
-                         ThetaType, isUnliftedTypeKind, unliftedTypeKind, 
-                         argTypeKind,
-                         liftedTypeKind, openTypeKind, mkArrowKind,
-                         tySuperKind, isLiftedTypeKind,
-                         mkArrowKinds, mkForAllTy, mkForAllTys,
-                         defaultKind, isSubArgTypeKind, isSubOpenTypeKind,
-                         mkFunTy, mkFunTys, zipFunTys, 
-                         mkTyConApp, mkAppTy,
-                         mkAppTys, applyTy, applyTys,
-                         mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
-                         mkPredTys, isUnLiftedType, 
-                         isUnboxedTupleType, isPrimitiveType,
-                         splitTyConApp_maybe,
-                         tidyTopType, tidyType, tidyPred, tidyTypes,
-                         tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-                         tidyTyVarBndr, tidyOpenTyVar,
-                         tidyOpenTyVars, tidyKind,
-                         isSubKind, tcView,
-
-                         tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
-                         tcEqPred, tcCmpPred, tcEqTypeX, eqKind,
-
-                         TvSubst(..),
-                         TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv,
-                         mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
-                         getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
-                         extendTvSubst, extendTvSubstList, isInScope, notElemTvSubst,
-                         substTy, substTys, substTyWith, substTheta, 
-                         substTyVar, substTyVarBndr, substPred, lookupTyVar,
-
-                         typeKind, repType, coreView, repSplitAppTy_maybe,
-                         pprKind, pprParendKind,
-                         pprType, pprParendType, pprTyThingCategory,
-                         pprPred, pprTheta, pprThetaArrow, pprClassPred
-                       )
-import TyCon           ( TyCon, isUnLiftedTyCon, isSynTyCon, isOpenTyCon,
-                         synTyConDefn, tyConUnique )    
-import DataCon         ( DataCon, dataConStupidTheta, dataConResTys )
-import Class           ( Class )
-import Var             ( TyVar, Id, isCoVar, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
-import ForeignCall     ( Safety, DNType(..) )
-import Unify           ( tcMatchTys )
+import Kind
+import TypeRep
+import Class
+import Var
+import ForeignCall
 import VarSet
+import Type
+import Coercion
+import TyCon
 
 -- others:
-import DynFlags                ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc, mkSystemName )
+import DynFlags
+import Name hiding (varName)
 import NameSet
-import VarEnv          ( TidyEnv )
-import OccName         ( OccName, mkDictOcc, mkOccName, tvName )
-import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
-import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
-import BasicTypes      ( IPName(..), Arity, ipNameName )
-import SrcLoc          ( SrcLoc, SrcSpan )
-import Util            ( equalLength )
-import Maybes          ( maybeToBool, expectJust, mapCatMaybes )
-import ListSetOps      ( hasNoDups )
-import List            ( nubBy )
+import VarEnv
+import PrelNames
+import TysWiredIn
+import BasicTypes
+import Util
+import Maybes
+import ListSetOps
 import Outputable
-import DATA_IOREF
-\end{code}
+import FastString
 
+import Data.List( mapAccumL )
+import Data.IORef
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -234,12 +210,15 @@ tau ::= tyvar
 
 \begin{code}
 type TcTyVar = TyVar   -- Used only during type inference
+type TcCoVar = CoVar   -- Used only during type inference; mutable
 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 TcCoercion = Coercion  -- A TcCoercion can contain TcTypes.
+
 -- These types do not have boxy type variables in them
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
@@ -248,13 +227,6 @@ type TcRhoType      = TcType
 type TcTauType      = TcType
 type TcKind         = Kind
 type TcTyVarSet     = TyVarSet
-
--- These types may have boxy type variables in them
-type BoxyTyVar     = TcTyVar
-type BoxyRhoType    = TcType   
-type BoxyThetaType  = TcThetaType      
-type BoxySigmaType  = TcType           
-type BoxyType       = TcType           
 \end{code}
 
 
@@ -293,7 +265,7 @@ 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, SigTv, which can unify with other SigTvs.  These are *not* treated
-as righd for the purposes of GADTs.  And they are used *only* for pattern 
+as rigid for the purposes of GADTs.  And they are used *only* for pattern
 bindings and mutually recursive function bindings.  See the function
 TcBinds.tcInstSig, and its use_skols parameter.
 
@@ -301,68 +273,59 @@ TcBinds.tcInstSig, and its use_skols parameter.
 \begin{code}
 -- A TyVarDetails is inside a TyVar
 data TcTyVarDetails
-  = SkolemTv SkolemInfo                        -- A skolem constant
-
-  | MetaTv BoxInfo (IORef MetaDetails)
-
-data BoxInfo 
-   = BoxTv     -- The contents is a (non-boxy) sigma-type
-               -- That is, this MetaTv is a "box"
-
-   | TauTv     -- The contents is a (non-boxy) tau-type
-               -- That is, this MetaTv is an ordinary unification variable
-
-   | SigTv SkolemInfo  -- A variant of TauTv, except that it should not be
-                       -- unified with a type, only with a type variable
-                       -- SigTvs are only distinguished to improve error messages
-                       --      see Note [Signature skolems]        
-                       --      The MetaDetails, if filled in, will 
-                       --      always be another SigTv or a SkolemTv
-
--- INVARIANTS:
---     A TauTv is always filled in with a tau-type, which
---     never contains any BoxTvs, nor any ForAlls 
---
---     However, a BoxTv can contain a type that contains further BoxTvs
---     Notably, when typechecking an explicit list, say [e1,e2], with
---     expected type being a box b1, we fill in b1 with (List b2), where
---     b2 is another (currently empty) box.
+  = SkolemTv      -- A skolem
+       Bool       -- True <=> this skolem type variable can be overlapped
+                  --          when looking up instances
+                  -- See Note [Binding when looking up instances] in InstEnv
+
+  | RuntimeUnk    -- Stands for an as-yet-unknown type in the GHCi
+                  -- interactive context
+
+  | FlatSkol TcType
+           -- The "skolem" obtained by flattening during
+          -- constraint simplification
+    
+           -- In comments we will use the notation alpha[flat = ty]
+           -- to represent a flattening skolem variable alpha
+           -- identified with type ty.
+          
+  | MetaTv MetaInfo (IORef MetaDetails)
+
+vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
+-- See Note [Binding when looking up instances] in InstEnv
+vanillaSkolemTv = SkolemTv False  -- Might be instantiated
+superSkolemTv   = SkolemTv True   -- Treat this as a completely distinct type
 
 data MetaDetails
-  = Flexi          -- Flexi type variables unify to become 
-                   -- Indirects.  
-
-  | Indirect TcType  -- INVARIANT:
-                    --   For a BoxTv, this type must be non-boxy
-                     --   For a TauTv, this type must be a tau-type
-
-data SkolemInfo
-  = SigSkol UserTypeCtxt       -- A skolem that is created by instantiating
-                               -- a programmer-supplied type signature
-                               -- Location of the binding site is on the TyVar
-
-       -- The rest are for non-scoped skolems
-  | ClsSkol Class      -- Bound at a class decl
-  | InstSkol Id                -- Bound at an instance decl
-  | FamInstSkol TyCon  -- Bound at a family 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
-
-  | UnkSkol            -- Unhelpful info (until I improve it)
+  = Flexi  -- Flexi type variables unify to become Indirects  
+  | Indirect TcType
+
+instance Outputable MetaDetails where
+  ppr Flexi         = ptext (sLit "Flexi")
+  ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
+
+data MetaInfo
+   = TauTv        -- This MetaTv is an ordinary unification variable
+                  -- A TauTv is always filled in with a tau-type, which
+                  -- never contains any ForAlls 
+
+   | SigTv        -- A variant of TauTv, except that it should not be
+                  -- unified with a type, only with a type variable
+                  -- SigTvs are only distinguished to improve error messages
+                  --      see Note [Signature skolems]        
+                  --      The MetaDetails, if filled in, will 
+                  --      always be another SigTv or a SkolemTv
+
+   | TcsTv        -- A MetaTv allocated by the constraint solver
+                  -- Its particular property is that it is always "touchable"
+                  -- Nevertheless, the constraint solver has to try to guess
+                  -- what type to instantiate it to
 
 -------------------------------------
--- UserTypeCtxt describes the places where a 
--- programmer-written type signature can occur
-data UserTypeCtxt 
+-- UserTypeCtxt describes the origin of the polymorphic type
+-- in the places where we need to an expression has that type
+
+data UserTypeCtxt
   = FunSigCtxt Name    -- Function type signature
                        -- Also used for types in SPECIALISE pragmas
   | ExprSigCtxt                -- Expression type signature
@@ -377,9 +340,13 @@ data UserTypeCtxt
   | ResSigCtxt         -- Result type sig
                        --      f x :: t = ....
   | ForSigCtxt Name    -- Foreign inport or export signature
-  | RuleSigCtxt Name   -- Signature on a forall'd variable in a RULE
   | DefaultDeclCtxt    -- Types in a default declaration
   | SpecInstCtxt       -- SPECIALISE instance pragma
+  | ThBrackCtxt                -- Template Haskell type brackets [t| ... |]
+
+  | GenSigCtxt          -- Higher-rank or impredicative situations
+                        -- e.g. (f e) where f has a higher-rank type
+                        -- We might want to elaborate this
 
 -- Notes re TySynCtxt
 -- We allow type synonyms that aren't types; e.g.  type List = []
@@ -402,7 +369,7 @@ kindVarRef tc =
   ASSERT ( isTcTyVar tc )
   case tcTyVarDetails tc of
     MetaTv TauTv ref -> ref
-    other            -> pprPanic "kindVarRef" (ppr tc)
+    _                -> pprPanic "kindVarRef" (ppr tc)
 
 mkKindVar :: Unique -> IORef MetaDetails -> KindVar
 mkKindVar u r 
@@ -416,7 +383,6 @@ kind_var_occ :: OccName     -- Just one for all KindVars
                        -- They may be jiggled by tidying
 kind_var_occ = mkOccName tvName "k"
 \end{code}
-\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -427,90 +393,171 @@ kind_var_occ = mkOccName tvName "k"
 \begin{code}
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 -- For debugging
-pprTcTyVarDetails (SkolemTv _)         = ptext SLIT("sk")
-pprTcTyVarDetails (MetaTv BoxTv _)     = ptext SLIT("box")
-pprTcTyVarDetails (MetaTv TauTv _)     = ptext SLIT("tau")
-pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext SLIT("sig")
+pprTcTyVarDetails (SkolemTv {})     = ptext (sLit "sk")
+pprTcTyVarDetails (RuntimeUnk {})  = ptext (sLit "rt")
+pprTcTyVarDetails (FlatSkol {})    = ptext (sLit "fsk")
+pprTcTyVarDetails (MetaTv TauTv _) = ptext (sLit "tau")
+pprTcTyVarDetails (MetaTv TcsTv _) = ptext (sLit "tcs")
+pprTcTyVarDetails (MetaTv SigTv _) = ptext (sLit "sig")
 
 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
-pprUserTypeCtxt (FunSigCtxt n)  = ptext SLIT("the type signature for") <+> quotes (ppr n)
-pprUserTypeCtxt ExprSigCtxt     = ptext SLIT("an expression type signature")
-pprUserTypeCtxt (ConArgCtxt c)  = ptext SLIT("the type of the constructor") <+> quotes (ppr c)
-pprUserTypeCtxt (TySynCtxt c)   = ptext SLIT("the RHS of the type synonym") <+> quotes (ppr c)
-pprUserTypeCtxt GenPatCtxt      = ptext SLIT("the type pattern of a generic definition")
-pprUserTypeCtxt LamPatSigCtxt   = ptext SLIT("a pattern type signature")
-pprUserTypeCtxt BindPatSigCtxt  = ptext SLIT("a pattern type signature")
-pprUserTypeCtxt ResSigCtxt      = ptext SLIT("a result type signature")
-pprUserTypeCtxt (ForSigCtxt n)  = ptext SLIT("the foreign declaration for") <+> quotes (ppr n)
-pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
-pprUserTypeCtxt DefaultDeclCtxt = ptext SLIT("a type in a `default' declaration")
-pprUserTypeCtxt SpecInstCtxt    = ptext SLIT("a SPECIALISE instance pragma")
-
-
---------------------------------
-tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
--- Tidy the type inside a GenSkol, preparatory to printing it
-tidySkolemTyVar env tv
-  = ASSERT( isSkolemTyVar tv || isSigTyVar tv )
-    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
+pprUserTypeCtxt (FunSigCtxt n)  = ptext (sLit "the type signature for") <+> quotes (ppr n)
+pprUserTypeCtxt ExprSigCtxt     = ptext (sLit "an expression type signature")
+pprUserTypeCtxt (ConArgCtxt c)  = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
+pprUserTypeCtxt (TySynCtxt c)   = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
+pprUserTypeCtxt GenPatCtxt      = ptext (sLit "the type pattern of a generic definition")
+pprUserTypeCtxt ThBrackCtxt     = ptext (sLit "a Template Haskell quotation [t|...|]")
+pprUserTypeCtxt LamPatSigCtxt   = ptext (sLit "a pattern type signature")
+pprUserTypeCtxt BindPatSigCtxt  = ptext (sLit "a pattern type signature")
+pprUserTypeCtxt ResSigCtxt      = ptext (sLit "a result type signature")
+pprUserTypeCtxt (ForSigCtxt n)  = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
+pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration")
+pprUserTypeCtxt SpecInstCtxt    = ptext (sLit "a SPECIALISE instance pragma")
+pprUserTypeCtxt GenSigCtxt      = ptext (sLit "a type expected by the context")
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{TidyType}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+-- | This tidies up a type for printing in an error message, or in
+-- an interface file.
+-- 
+-- It doesn't change the uniques at all, just the print names.
+tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
+tidyTyVarBndr (tidy_env, subst) tyvar
+  = case tidyOccName tidy_env occ1 of
+      (tidy', occ') -> ((tidy', subst'), tyvar')
+       where
+          subst' = extendVarEnv subst tyvar tyvar'
+          tyvar' = setTyVarName tyvar name'
+          name'  = tidyNameOcc name occ'
   where
-    (env1, info1) = case tcTyVarDetails tv of
-                       SkolemTv info -> (env1, SkolemTv info')
-                               where
-                                 (env1, info') = tidy_skol_info env info
-                       MetaTv (SigTv info) box -> (env1, MetaTv (SigTv info') box)
-                               where
-                                 (env1, info') = tidy_skol_info env info
-                       info -> (env, info)
-
-    tidy_skol_info env (GenSkol tvs ty loc) = (env2, GenSkol tvs1 ty1 loc)
-                           where
-                             (env1, tvs1) = tidyOpenTyVars env tvs
-                             (env2, ty1)  = tidyOpenType env1 ty
-    tidy_skol_info env info = (env, info)
-                    
-pprSkolTvBinding :: TcTyVar -> SDoc
--- Print info about the binding of a skolem tyvar, 
--- or nothing if we don't have anything useful to say
-pprSkolTvBinding tv
-  = ASSERT ( isTcTyVar tv )
-    ppr_details (tcTyVarDetails tv)
+    name = tyVarName tyvar
+    occ  = getOccName name
+    -- System Names are for unification variables;
+    -- when we tidy them we give them a trailing "0" (or 1 etc)
+    -- so that they don't take precedence for the un-modified name
+    occ1 | isSystemName name = mkTyVarOcc (occNameString occ ++ "0")
+         | otherwise         = occ
+
+
+---------------
+tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
+-- ^ Add the free 'TyVar's to the env in tidy form,
+-- so that we can tidy the type they are free in
+tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
+
+---------------
+tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
+tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
+
+---------------
+tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
+-- ^ Treat a new 'TyVar' as a binder, and give it a fresh tidy name
+-- using the environment if one has not already been allocated. See
+-- also 'tidyTyVarBndr'
+tidyOpenTyVar env@(_, subst) tyvar
+  = case lookupVarEnv subst tyvar of
+       Just tyvar' -> (env, tyvar')            -- Already substituted
+       Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
+
+---------------
+tidyType :: TidyEnv -> Type -> Type
+tidyType env@(_, subst) ty
+  = go ty
   where
-    ppr_details (MetaTv TauTv _)   = quotes (ppr tv) <+> ptext SLIT("is a meta type variable")
-    ppr_details (MetaTv BoxTv _)   = quotes (ppr tv) <+> ptext SLIT("is a boxy type variable")
-    ppr_details (MetaTv (SigTv info) _) = ppr_skol info
-    ppr_details (SkolemTv info)                = ppr_skol info
-
-    ppr_skol UnkSkol        = empty    -- Unhelpful; omit
-    ppr_skol (SigSkol ctxt)  = sep [quotes (ppr tv) <+> ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt,
-                                   nest 2 (ptext SLIT("at") <+> ppr (getSrcLoc tv))]
-    ppr_skol info            = quotes (ppr tv) <+> pprSkolInfo info
-pprSkolInfo :: SkolemInfo -> SDoc
-pprSkolInfo (SigSkol ctxt)   = ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt
-pprSkolInfo (ClsSkol cls)    = ptext SLIT("is bound by the class declaration for") <+> quotes (ppr cls)
-pprSkolInfo (InstSkol df)    = 
-  ptext SLIT("is bound by the instance declaration at") <+> ppr (getSrcLoc df)
-pprSkolInfo (FamInstSkol tc) = 
-  ptext SLIT("is bound by the family instance declaration at") <+> 
-  ppr (getSrcLoc tc)
-pprSkolInfo (ArrowSkol loc)  = 
-  ptext SLIT("is bound by the arrow form at") <+> ppr loc
-pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("is bound by the pattern for") <+> quotes (ppr dc),
-                                   nest 2 (ptext SLIT("at") <+> ppr loc)]
-pprSkolInfo (GenSkol tvs ty loc) = sep [sep [ptext SLIT("is bound by the polymorphic type"), 
-                                            nest 2 (quotes (ppr (mkForAllTys tvs ty)))],
-                                       nest 2 (ptext SLIT("at") <+> ppr loc)]
--- UnkSkol, SigSkol
--- For type variables the others are dealt with by pprSkolTvBinding.  
--- For Insts, these cases should not happen
-pprSkolInfo UnkSkol = panic "UnkSkol"
+    go (TyVarTy tv)        = case lookupVarEnv subst tv of
+                               Nothing  -> expand tv
+                               Just tv' -> expand tv'
+    go (TyConApp tycon tys) = let args = map go tys
+                             in args `seqList` TyConApp tycon args
+    go (PredTy sty)        = PredTy (tidyPred env sty)
+    go (AppTy fun arg)     = (AppTy $! (go fun)) $! (go arg)
+    go (FunTy fun arg)     = (FunTy $! (go fun)) $! (go arg)
+    go (ForAllTy tv ty)            = ForAllTy tvp $! (tidyType envp ty)
+                             where
+                               (envp, tvp) = tidyTyVarBndr env tv
+
+    -- Expand FlatSkols, the skolems introduced by flattening process
+    -- We don't want to show them in type error messages
+    expand tv | isTcTyVar tv
+              , FlatSkol ty <- tcTyVarDetails tv
+              = go ty
+              | otherwise
+              = TyVarTy tv
 
-instance Outputable MetaDetails where
-  ppr Flexi        = ptext SLIT("Flexi")
-  ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty
+---------------
+tidyTypes :: TidyEnv -> [Type] -> [Type]
+tidyTypes env tys = map (tidyType env) tys
+
+---------------
+tidyPred :: TidyEnv -> PredType -> PredType
+tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
+tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
+tidyPred env (EqPred ty1 ty2)  = EqPred (tidyType env ty1) (tidyType env ty2)
+
+---------------
+-- | Grabs the free type variables, tidies them
+-- and then uses 'tidyType' to work over the type itself
+tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
+tidyOpenType env ty
+  = (env', tidyType env' ty)
+  where
+    env' = tidyFreeTyVars env (tyVarsOfType ty)
+
+---------------
+tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
+tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
+
+---------------
+-- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
+tidyTopType :: Type -> Type
+tidyTopType ty = tidyType emptyTidyEnv ty
+
+---------------
+tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
+tidyKind env k = tidyOpenType env k
 \end{code}
 
+%************************************************************************
+%*                                                                     *
+                            Tidying coercions
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+
+tidyCo :: TidyEnv -> Coercion -> Coercion
+tidyCo env@(_, subst) co
+  = go co
+  where
+    go (Refl ty)             = Refl (tidyType env ty)
+    go (TyConAppCo tc cos)   = let args = map go cos
+                               in args `seqList` TyConAppCo tc args
+    go (AppCo co1 co2)       = (AppCo $! go co1) $! go co2
+    go (ForAllCo tv co)      = ForAllCo tvp $! (tidyCo envp co)
+                               where
+                                 (envp, tvp) = tidyTyVarBndr env tv
+    go (CoVarCo cv)          = case lookupVarEnv subst cv of
+                                 Nothing  -> CoVarCo cv
+                                 Just cv' -> CoVarCo cv'
+    go (AxiomInstCo con cos) = let args = tidyCos env cos
+                               in  args `seqList` AxiomInstCo con args
+    go (UnsafeCo ty1 ty2)    = (UnsafeCo $! tidyType env ty1) $! tidyType env ty2
+    go (SymCo co)            = SymCo $! go co
+    go (TransCo co1 co2)     = (TransCo $! go co1) $! go co2
+    go (NthCo d co)          = NthCo d $! go co
+    go (InstCo co ty)        = (InstCo $! go co) $! tidyType env ty
+
+tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
+tidyCos env = map (tidyCo env)
+
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -519,54 +566,74 @@ instance Outputable MetaDetails where
 %************************************************************************
 
 \begin{code}
-isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isBoxyTyVar, isMetaTyVar :: TyVar -> Bool
+isImmutableTyVar :: TyVar -> Bool
+
 isImmutableTyVar tv
   | isTcTyVar tv = isSkolemTyVar tv
   | otherwise    = True
 
+isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
+  isMetaTyVar :: TcTyVar -> Bool 
+
+isTyConableTyVar tv    
+       -- True of a meta-type variable that can be filled in 
+       -- with a type constructor application; in particular,
+       -- not a SigTv
+  = ASSERT( isTcTyVar tv) 
+    case tcTyVarDetails tv of
+       MetaTv SigTv _ -> False
+       _              -> True
+       
 isSkolemTyVar tv 
-  = ASSERT( isTcTyVar tv )
+  = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-       SkolemTv _         -> True
-       MetaTv _ _         -> False
+        SkolemTv {}   -> True
+        FlatSkol {}   -> True
+        RuntimeUnk {} -> True
+        MetaTv {}     -> False
 
-isExistentialTyVar tv  -- Existential type variable, bound by a pattern
+isOverlappableTyVar tv
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-       SkolemTv (PatSkol _ _) -> True
-       other                  -> False
+        SkolemTv overlappable -> overlappable
+        _                     -> False
 
 isMetaTyVar tv 
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
        MetaTv _ _ -> True
-       other      -> False
+       _          -> False
 
-isBoxyTyVar tv 
-  = ASSERT( isTcTyVar tv )
-    case tcTyVarDetails tv of
-       MetaTv BoxTv _ -> True
-       other          -> False
+isMetaTyVarTy :: TcType -> Bool
+isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
+isMetaTyVarTy _            = False
 
+isSigTyVar :: Var -> Bool
 isSigTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-       MetaTv (SigTv _) _ -> True
-       other              -> False
+       MetaTv SigTv _ -> True
+       _              -> False
 
 metaTvRef :: TyVar -> IORef MetaDetails
 metaTvRef tv 
-  = ASSERT( isTcTyVar tv )
+  = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
        MetaTv _ ref -> ref
-       other      -> pprPanic "metaTvRef" (ppr tv)
+       _          -> pprPanic "metaTvRef" (ppr tv)
 
 isFlexi, isIndirect :: MetaDetails -> Bool
 isFlexi Flexi = True
-isFlexi other = False
+isFlexi _     = False
 
 isIndirect (Indirect _) = True
-isIndirect other        = False
+isIndirect _            = False
+
+isRuntimeUnkSkol :: TyVar -> Bool
+-- Called only in TcErrors; see Note [Runtime skolems] there
+isRuntimeUnkSkol x
+  | isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True
+  | otherwise                                   = False
 \end{code}
 
 
@@ -581,7 +648,7 @@ mkSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
 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
+mkPhiTy theta ty = foldr (\p r -> mkFunTy (mkPredTy p) r) ty theta
 \end{code}
 
 @isTauTy@ tests for nested for-alls.  It should not be called on a boxy type.
@@ -589,44 +656,27 @@ mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
 \begin{code}
 isTauTy :: Type -> Bool
 isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
-isTauTy (TyVarTy tv)    = ASSERT( not (isTcTyVar tv && isBoxyTyVar tv) )
-                          True
+isTauTy (TyVarTy _)      = True
 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
 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 other            = False
-
+isTauTy (PredTy _)       = True                -- Don't look through source types
+isTauTy _                = False
 
 isTauTyCon :: TyCon -> Bool
 -- Returns False for type synonyms whose expansion is a polytype
 isTauTyCon tc 
-  | isSynTyCon tc && not (isOpenTyCon tc) = isTauTy (snd (synTyConDefn tc))
-  | otherwise                             = True
+  | isClosedSynTyCon tc = isTauTy (snd (synTyConDefn tc))
+  | otherwise           = True
 
 ---------------
-isBoxyTy :: TcType -> Bool
-isBoxyTy ty = any isBoxyTyVar (varSetElems (tcTyVarsOfType ty))
-
-isRigidTy :: TcType -> Bool
--- A type is rigid if it has no meta type variables in it
-isRigidTy ty = all isSkolemTyVar (varSetElems (tcTyVarsOfType ty))
-
-isRefineableTy :: TcType -> Bool
--- A type should have type refinements applied to it if it has
--- free type variables, and they are all rigid
-isRefineableTy ty = not (null tc_tvs) && all isSkolemTyVar tc_tvs
-                   where
-                     tc_tvs = varSetElems (tcTyVarsOfType ty)
-
----------------
-getDFunTyKey :: Type -> OccName        -- Get some string from a type, to be used to 
+getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
                                -- construct a dictionary function name
 getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
 getDFunTyKey (TyVarTy tv)    = getOccName tv
 getDFunTyKey (TyConApp tc _) = getOccName tc
 getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
-getDFunTyKey (FunTy arg _)   = getOccName funTyCon
+getDFunTyKey (FunTy _ _)     = getOccName funTyCon
 getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
 getDFunTyKey ty                     = pprPanic "getDFunTyKey" (pprType ty)
 -- PredTy shouldn't happen
@@ -642,7 +692,6 @@ getDFunTyKey ty                  = pprPanic "getDFunTyKey" (pprType ty)
 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.
@@ -652,26 +701,30 @@ tcSplitForAllTys :: Type -> ([TyVar], Type)
 tcSplitForAllTys ty = split ty ty []
    where
      split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
-     split orig_ty (ForAllTy tv ty) tvs 
-       | not (isCoVar tv) = split ty ty (tv:tvs)
-     split orig_ty t tvs = (reverse tvs, orig_ty)
+     split _ (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
+     split orig_ty _          tvs = (reverse tvs, orig_ty)
 
+tcIsForAllTy :: Type -> Bool
 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
-tcIsForAllTy (ForAllTy tv ty) = not (isCoVar tv)
-tcIsForAllTy t               = False
+tcIsForAllTy (ForAllTy {}) = True
+tcIsForAllTy _             = False
+
+tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
+-- Split off the first predicate argument from a type
+tcSplitPredFunTy_maybe ty | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
+tcSplitPredFunTy_maybe (FunTy arg res)
+  | Just p <- splitPredTy_maybe arg = Just (p, res)
+tcSplitPredFunTy_maybe _
+  = Nothing
 
 tcSplitPhiTy :: Type -> (ThetaType, Type)
-tcSplitPhiTy ty = split ty ty []
- where
-  split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
-
-  split orig_ty (ForAllTy tv ty) ts
-        | isCoVar tv = split ty ty (eq_pred:ts)
-        where
-           PredTy eq_pred = tyVarKind tv
-  split orig_ty (FunTy arg res) ts 
-       | Just p <- tcSplitPredTy_maybe arg = split res res (p:ts)
-  split orig_ty ty             ts = (reverse ts, orig_ty)
+tcSplitPhiTy ty
+  = split ty []
+  where
+    split ty ts 
+      = case tcSplitPredFunTy_maybe ty of
+         Just (pred, ty) -> split ty (pred:ts)
+         Nothing         -> (reverse ts, ty)
 
 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
@@ -679,29 +732,32 @@ tcSplitSigmaTy ty = case tcSplitForAllTys ty of
                                        (theta, tau) -> (tvs, theta, tau)
 
 -----------------------
-tcMultiSplitSigmaTy
-       :: TcSigmaType
-       -> ( [([TyVar], ThetaType)],    -- forall as.C => forall bs.D
-            TcSigmaType)               -- The rest of the type
-
--- We need a loop here because we are now prepared to entertain
--- types like
---     f:: forall a. Eq a => forall b. Baz b => tau
--- We want to instantiate this to
---     f2::tau         {f2 = f1 b (Baz b), f1 = f a (Eq a)}
-
-tcMultiSplitSigmaTy sigma
-  = case (tcSplitSigmaTy sigma) of
-       ([],[],ty) -> ([], sigma)
-       (tvs, theta, ty) -> case tcMultiSplitSigmaTy ty of
-                               (pairs, rest) -> ((tvs,theta):pairs, rest)
+tcDeepSplitSigmaTy_maybe
+  :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
+-- Looks for a *non-trivial* quantified type, under zero or more function arrows
+-- By "non-trivial" we mean either tyvars or constraints are non-empty
+
+tcDeepSplitSigmaTy_maybe ty
+  | Just (arg_ty, res_ty)           <- tcSplitFunTy_maybe ty
+  , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
+  = Just (arg_ty:arg_tys, tvs, theta, rho)
+
+  | (tvs, theta, rho) <- tcSplitSigmaTy ty
+  , not (null tvs && null theta)
+  = Just ([], tvs, theta, rho)
+
+  | otherwise = Nothing
 
 -----------------------
 tcTyConAppTyCon :: Type -> TyCon
-tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
+tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
+                       Just (tc, _) -> tc
+                       Nothing      -> pprPanic "tcTyConAppTyCon" (pprType ty)
 
 tcTyConAppArgs :: Type -> [Type]
-tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
+tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
+                       Just (_, args) -> args
+                       Nothing        -> pprPanic "tcTyConAppArgs" (pprType ty)
 
 tcSplitTyConApp :: Type -> (TyCon, [Type])
 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
@@ -712,18 +768,10 @@ tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 tcSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
-tcSplitTyConApp_maybe (AppTy arg res)   = Just (funTyCon, [arg,res])
        -- Newtypes are opaque, so they may be split
        -- However, predicates are not treated
        -- as tycon applications by the type checker
-
--- XXX - 2006-09-24: This case is hard-coded in (rendering predicates opaque as well)
---       to make the newly reworked newtype-deriving work on the trivial case:
---              newtype T = T () deriving (Eq, Ord)
---       Please remove this if the newtype-deriving scheme no longer produces a PredTy.
-tcSplitTyConApp_maybe (PredTy (ClassP _ [ty']))   = tcSplitTyConApp_maybe ty'
-
-tcSplitTyConApp_maybe other            = Nothing
+tcSplitTyConApp_maybe _                 = Nothing
 
 -----------------------
 tcSplitFunTys :: Type -> ([Type], Type)
@@ -734,9 +782,16 @@ tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
                                          (args,res') = tcSplitFunTys res
 
 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
-tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
-tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
-tcSplitFunTy_maybe other           = Nothing
+tcSplitFunTy_maybe ty | Just ty' <- tcView ty           = tcSplitFunTy_maybe ty'
+tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
+tcSplitFunTy_maybe _                                    = Nothing
+       -- Note the (not (isPredTy arg)) guard
+       -- Consider     (?x::Int) => Bool
+       -- We don't want to treat this as a function type!
+       -- A concrete example is test tc230:
+       --      f :: () -> (?p :: ()) => () -> ()
+       --
+       --      g = f () ()
 
 tcSplitFunTysN
        :: TcRhoType 
@@ -753,8 +808,13 @@ tcSplitFunTysN ty n_args
   | otherwise
   = ([], ty)
 
+tcSplitFunTy :: Type -> (Type, Type)
 tcSplitFunTy  ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
+
+tcFunArgTy :: Type -> Type
 tcFunArgTy    ty = fst (tcSplitFunTy ty)
+
+tcFunResultTy :: Type -> Type
 tcFunResultTy ty = snd (tcSplitFunTy ty)
 
 -----------------------
@@ -778,8 +838,8 @@ tcSplitAppTys ty
 -----------------------
 tcGetTyVar_maybe :: Type -> Maybe TyVar
 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
-tcGetTyVar_maybe (TyVarTy tv)  = Just tv
-tcGetTyVar_maybe other         = Nothing
+tcGetTyVar_maybe (TyVarTy tv)   = Just tv
+tcGetTyVar_maybe _              = Nothing
 
 tcGetTyVar :: String -> Type -> TyVar
 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
@@ -788,29 +848,50 @@ tcIsTyVarTy :: Type -> Bool
 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 
 -----------------------
-tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
+tcSplitDFunTy :: Type -> ([TyVar], Int, Class, [Type])
 -- Split the type of a dictionary function
+-- We don't use tcSplitSigmaTy,  because a DFun may (with NDP)
+-- have non-Pred arguments, such as
+--     df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
 tcSplitDFunTy ty 
-  = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
-    case tcSplitDFunHead tau of { (clas, tys) -> 
-    (tvs, theta, clas, tys) }}
+  = case tcSplitForAllTys ty   of { (tvs, rho)  ->
+    case split_dfun_args 0 rho of { (n_theta, tau) ->
+    case tcSplitDFunHead tau   of { (clas, tys) ->
+    (tvs, n_theta, clas, tys) }}}
+  where
+    -- Count the context of the dfun.  This can be a mix of
+    -- coercion and class constraints; or (in the general NDP case)
+    -- some other function argument
+    split_dfun_args n ty | Just ty' <- tcView ty = split_dfun_args n ty'
+    split_dfun_args n (FunTy _ ty)     = split_dfun_args (n+1) ty
+    split_dfun_args n ty               = (n, ty)
 
 tcSplitDFunHead :: Type -> (Class, [Type])
 tcSplitDFunHead tau  
-  = case tcSplitPredTy_maybe tau of 
+  = case splitPredTy_maybe tau of 
        Just (ClassP clas tys) -> (clas, tys)
-       other -> panic "tcSplitDFunHead"
+       _ -> pprPanic "tcSplitDFunHead" (ppr tau)
 
-tcValidInstHeadTy :: Type -> Bool
+tcInstHeadTyNotSynonym :: Type -> Bool
 -- Used in Haskell-98 mode, for the argument types of an instance head
 -- These must not be type synonyms, but everywhere else type synonyms
 -- are transparent, so we need a special function here
-tcValidInstHeadTy ty
+tcInstHeadTyNotSynonym ty
+  = case ty of
+        TyConApp tc _ -> not (isSynTyCon tc)
+        _ -> True
+
+tcInstHeadTyAppAllTyVars :: Type -> Bool
+-- Used in Haskell-98 mode, for the argument types of an instance head
+-- These must be a constructor applied to type variable arguments
+tcInstHeadTyAppAllTyVars ty
+  | Just ty' <- tcView ty       -- Look through synonyms
+  = tcInstHeadTyAppAllTyVars ty'
+  | otherwise
   = case ty of
-       NoteTy _ ty     -> tcValidInstHeadTy ty
-       TyConApp tc tys -> not (isSynTyCon tc) && ok tys
+       TyConApp _ tys  -> ok tys
        FunTy arg res   -> ok [arg, res]
-       other           -> False
+       _               -> False
   where
        -- Check that all the types are type variables,
        -- and that each is distinct
@@ -818,9 +899,8 @@ tcValidInstHeadTy ty
           where
             tvs = mapCatMaybes get_tv tys
 
-    get_tv (NoteTy _ ty) = get_tv ty   -- Again, do not look
     get_tv (TyVarTy tv)  = Just tv     -- through synonyms
-    get_tv other        = Nothing
+    get_tv _             = Nothing
 \end{code}
 
 
@@ -831,107 +911,33 @@ tcValidInstHeadTy ty
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
-tcSplitPredTy_maybe :: Type -> Maybe PredType
-   -- Returns Just for predicates only
-tcSplitPredTy_maybe ty | Just ty' <- tcView 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
-
-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}
-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)
-getClassPredTys other = panic "getClassPredTys"
-
-isEqPred :: PredType -> Bool
-isEqPred (EqPred {}) = True
-isEqPred _          = False
-
-mkDictTy :: Class -> [Type] -> Type
-mkDictTy clas tys = mkPredTy (ClassP clas tys)
-
-isDictTy :: Type -> Bool
-isDictTy ty | Just ty' <- tcView ty = isDictTy ty'
-isDictTy (PredTy p) = isClassPred p
-isDictTy other     = False
-\end{code}
-
---------------------- Implicit parameters ---------------------------------
+Superclasses
 
 \begin{code}
-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}
-
---------------------- Equality predicates ---------------------------------
-\begin{code}
-substEqSpec :: TvSubst -> [(TyVar,Type)] -> [(TcType,TcType)]
-substEqSpec subst eq_spec = [ (substTyVar subst tv, substTy subst ty)
-                           | (tv,ty) <- eq_spec]
-\end{code}
-
---------------------- The stupid theta (sigh) ---------------------------------
-
-\begin{code}
-dataConsStupidTheta :: [DataCon] -> ThetaType
--- Union the stupid thetas from all the specified constructors (non-empty)
--- All the constructors should have the same result type, modulo alpha conversion
--- The resulting ThetaType uses type variables from the *first* constructor in the list
---
--- It's here because it's used in MkId.mkRecordSelId, and in TcExpr
-dataConsStupidTheta (con1:cons)
-  = nubBy tcEqPred all_preds
-  where
-    all_preds    = dataConStupidTheta con1 ++ other_stupids
-    res_tys1     = dataConResTys con1
-    tvs1         = tyVarsOfTypes res_tys1
-    other_stupids = [ substPred subst pred
-                   | con <- cons
-                   , let Just subst = tcMatchTys tvs1 res_tys1 (dataConResTys con)
-                   , pred <- dataConStupidTheta con ]
-dataConsStupidTheta [] = panic "dataConsStupidTheta"
+mkMinimalBySCs :: [PredType] -> [PredType]
+-- Remove predicates that can be deduced from others by superclasses
+mkMinimalBySCs ptys = [ ploc |  ploc <- ptys
+                             ,  ploc `not_in_preds` rec_scs ]
+ where
+   rec_scs = concatMap trans_super_classes ptys
+   not_in_preds p ps = null (filter (eqPred p) ps)
+   trans_super_classes (ClassP cls tys) = transSuperClasses cls tys
+   trans_super_classes _other_pty       = []
+
+transSuperClasses :: Class -> [Type] -> [PredType]
+transSuperClasses cls tys
+  = foldl (\pts p -> trans_sc p ++ pts) [] $
+    immSuperClasses cls tys
+  where trans_sc :: PredType -> [PredType]
+        trans_sc this_pty@(ClassP cls tys)
+          = foldl (\pts p -> trans_sc p ++ pts) [this_pty] $
+            immSuperClasses cls tys
+        trans_sc pty = [pty]
+
+immSuperClasses :: Class -> [Type] -> [PredType]
+immSuperClasses cls tys
+  = substTheta (zipTopTvSubst tyvars tys) sc_theta
+  where (tyvars,sc_theta,_,_) = classBigSig cls
 \end{code}
 
 
@@ -948,30 +954,36 @@ any foralls.  E.g.
 \begin{code}
 isSigmaTy :: Type -> Bool
 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
-isSigmaTy (ForAllTy tyvar ty) = True
-isSigmaTy (FunTy a b)        = isPredTy a
-isSigmaTy _                  = False
+isSigmaTy (ForAllTy _ _) = True
+isSigmaTy (FunTy a _)    = isPredTy a
+isSigmaTy _              = False
 
 isOverloadedTy :: Type -> Bool
+-- Yes for a type of a function that might require evidence-passing
+-- Used only by bindLocalMethods
 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
-isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
-isOverloadedTy (FunTy a b)        = isPredTy a
-isOverloadedTy _                  = False
-
-isPredTy :: Type -> Bool       -- Belongs in TcType because it does 
-                               -- not look through newtypes, or predtypes (of course)
-isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
-isPredTy (PredTy sty)  = True
-isPredTy _            = False
+isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
+isOverloadedTy (FunTy a _)     = isPredTy a
+isOverloadedTy _               = False
 \end{code}
 
 \begin{code}
+isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
+    isUnitTy, isCharTy :: Type -> Bool
 isFloatTy      = is_tc floatTyConKey
 isDoubleTy     = is_tc doubleTyConKey
 isIntegerTy    = is_tc integerTyConKey
 isIntTy        = is_tc intTyConKey
+isWordTy       = is_tc wordTyConKey
 isBoolTy       = is_tc boolTyConKey
 isUnitTy       = is_tc unitTyConKey
+isCharTy       = is_tc charTyConKey
+
+isStringTy :: Type -> Bool
+isStringTy ty
+  = case tcSplitTyConApp_maybe ty of
+      Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
+      _                   -> False
 
 is_tc :: Unique -> Type -> Bool
 -- Newtypes are opaque to this
@@ -980,6 +992,16 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
                        Nothing      -> False
 \end{code}
 
+\begin{code}
+-- NB: Currently used in places where we have already expanded type synonyms;
+--     hence no 'coreView'.  This could, however, be changed without breaking
+--     any code.
+isSynFamilyTyConApp :: TcTauType -> Bool
+isSynFamilyTyConApp (TyConApp tc tys) = isSynFamilyTyCon tc && 
+                                      length tys == tyConArity tc 
+isSynFamilyTyConApp _other            = False
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
@@ -1000,19 +1022,13 @@ tcTyVarsOfType :: Type -> TcTyVarSet
 -- (Types.tyVarsOfTypes finds all free TyVars)
 tcTyVarsOfType (TyVarTy tv)        = if isTcTyVar tv then unitVarSet tv
                                                      else emptyVarSet
-tcTyVarsOfType (TyConApp tycon tys) = tcTyVarsOfTypes tys
-tcTyVarsOfType (NoteTy _ ty)       = tcTyVarsOfType ty
+tcTyVarsOfType (TyConApp _ tys)     = tcTyVarsOfTypes tys
 tcTyVarsOfType (PredTy sty)        = tcTyVarsOfPred sty
 tcTyVarsOfType (FunTy arg res)     = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
 tcTyVarsOfType (AppTy fun arg)     = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
-tcTyVarsOfType (ForAllTy tyvar ty)  = (tcTyVarsOfType ty `delVarSet` tyvar)
-                                      `unionVarSet` tcTyVarsOfTyVar tyvar
+tcTyVarsOfType (ForAllTy tyvar ty)  = tcTyVarsOfType ty `delVarSet` tyvar
        -- We do sometimes quantify over skolem TcTyVars
 
-tcTyVarsOfTyVar :: TcTyVar -> TyVarSet
-tcTyVarsOfTyVar tv | isCoVar tv = tcTyVarsOfType (tyVarKind tv)
-                   | otherwise  = emptyVarSet
-
 tcTyVarsOfTypes :: [Type] -> TyVarSet
 tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
 
@@ -1022,83 +1038,58 @@ tcTyVarsOfPred (ClassP _ tys)   = tcTyVarsOfTypes tys
 tcTyVarsOfPred (EqPred ty1 ty2) = tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
 \end{code}
 
-Note [Silly type synonym]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-       type T a = Int
-What are the free tyvars of (T x)?  Empty, of course!  
-Here's the example that Ralf Laemmel showed me:
-       foo :: (forall a. C u a -> C u a) -> u
-       mappend :: Monoid u => u -> u -> u
-
-       bar :: Monoid u => u
-       bar = foo (\t -> t `mappend` t)
-We have to generalise at the arg to f, and we don't
-want to capture the constraint (Monad (C u a)) because
-it appears to mention a.  Pretty silly, but it was useful to him.
-
-exactTyVarsOfType is used by the type checker to figure out exactly
-which type variables are mentioned in a type.  It's also used in the
-smart-app checking code --- see TcExpr.tcIdApp
-
-\begin{code}
-exactTyVarsOfType :: TcType -> TyVarSet
--- Find the free type variables (of any kind)
--- but *expand* type synonyms.  See Note [Silly type synonym] above.
-exactTyVarsOfType ty
-  = go ty
-  where
-    go ty | Just ty' <- tcView ty = go ty'     -- This is the key line
-    go (TyVarTy tv)              = unitVarSet tv
-    go (TyConApp tycon tys)      = exactTyVarsOfTypes tys
-    go (PredTy ty)               = go_pred ty
-    go (FunTy arg res)           = go arg `unionVarSet` go res
-    go (AppTy fun arg)           = go fun `unionVarSet` go arg
-    go (ForAllTy tyvar ty)       = delVarSet (go ty) tyvar
-                                    `unionVarSet` go_tv tyvar
-
-    go_pred (IParam _ ty)    = go ty
-    go_pred (ClassP _ tys)   = exactTyVarsOfTypes tys
-    go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
-
-    go_tv tyvar | isCoVar tyvar = go (tyVarKind tyvar)
-                | otherwise     = emptyVarSet
-
-exactTyVarsOfTypes :: [TcType] -> TyVarSet
-exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
-\end{code}
-
 Find the free tycons and classes of a type.  This is used in the front
 end of the compiler.
 
 \begin{code}
-tyClsNamesOfType :: Type -> NameSet
-tyClsNamesOfType (TyVarTy tv)              = emptyNameSet
-tyClsNamesOfType (TyConApp tycon tys)      = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
-tyClsNamesOfType (NoteTy _ ty2)            = tyClsNamesOfType ty2
-tyClsNamesOfType (PredTy (IParam n ty))     = tyClsNamesOfType ty
-tyClsNamesOfType (PredTy (ClassP cl tys))   = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
-tyClsNamesOfType (PredTy (EqPred ty1 ty2))  = tyClsNamesOfType ty1 `unionNameSets` tyClsNamesOfType ty2
-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
+orphNamesOfType :: Type -> NameSet
+orphNamesOfType ty | Just ty' <- tcView ty = orphNamesOfType ty'
+               -- Look through type synonyms (Trac #4912)
+orphNamesOfType (TyVarTy _)               = emptyNameSet
+orphNamesOfType (TyConApp tycon tys)       = unitNameSet (getName tycon) 
+                                             `unionNameSets` orphNamesOfTypes tys
+orphNamesOfType (PredTy (IParam _ ty))    = orphNamesOfType ty
+orphNamesOfType (PredTy (ClassP cl tys))  = unitNameSet (getName cl) 
+                                            `unionNameSets` orphNamesOfTypes tys
+orphNamesOfType (PredTy (EqPred ty1 ty2)) = orphNamesOfType ty1 
+                                            `unionNameSets` orphNamesOfType ty2
+orphNamesOfType (FunTy arg res)            = orphNamesOfType arg `unionNameSets` orphNamesOfType res
+orphNamesOfType (AppTy fun arg)            = orphNamesOfType fun `unionNameSets` orphNamesOfType arg
+orphNamesOfType (ForAllTy _ ty)            = orphNamesOfType ty
+
+orphNamesOfTypes :: [Type] -> NameSet
+orphNamesOfTypes tys = foldr (unionNameSets . orphNamesOfType) emptyNameSet tys
+
+orphNamesOfDFunHead :: 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 
+orphNamesOfDFunHead 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 ]
+       (_, _, head_ty) -> orphNamesOfType head_ty
+        
+orphNamesOfCo :: Coercion -> NameSet
+orphNamesOfCo (Refl ty)             = orphNamesOfType ty
+orphNamesOfCo (TyConAppCo tc cos)   = unitNameSet (getName tc) `unionNameSets` orphNamesOfCos cos
+orphNamesOfCo (AppCo co1 co2)       = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2
+orphNamesOfCo (ForAllCo _ co)       = orphNamesOfCo co
+orphNamesOfCo (CoVarCo _)           = emptyNameSet
+orphNamesOfCo (AxiomInstCo con cos) = orphNamesOfCoCon con `unionNameSets` orphNamesOfCos cos
+orphNamesOfCo (UnsafeCo ty1 ty2)    = orphNamesOfType ty1 `unionNameSets` orphNamesOfType ty2
+orphNamesOfCo (SymCo co)            = orphNamesOfCo co
+orphNamesOfCo (TransCo co1 co2)     = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2
+orphNamesOfCo (NthCo _ co)          = orphNamesOfCo co
+orphNamesOfCo (InstCo co ty)        = orphNamesOfCo co `unionNameSets` orphNamesOfType ty
+
+orphNamesOfCos :: [Coercion] -> NameSet
+orphNamesOfCos = foldr (unionNameSets . orphNamesOfCo) emptyNameSet
+
+orphNamesOfCoCon :: CoAxiom -> NameSet
+orphNamesOfCoCon (CoAxiom { co_ax_lhs = ty1, co_ax_rhs = ty2 })
+  = orphNamesOfType ty1 `unionNameSets` orphNamesOfType ty2
 \end{code}
 
 
@@ -1113,22 +1104,28 @@ restricted set of types as arguments and results (the restricting factor
 being the )
 
 \begin{code}
-tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type)
--- (isIOType t) returns (Just (IO,t')) if t is of the form (IO t'), or
---                                    some newtype wrapping thereof
+tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type, Coercion)
+-- (isIOType t) returns Just (IO,t',co)
+--                             if co : t ~ IO t'
 --             returns Nothing otherwise
 tcSplitIOType_maybe ty 
-  | Just (io_tycon, [io_res_ty]) <- tcSplitTyConApp_maybe ty,
+  = case tcSplitTyConApp_maybe ty of
        -- This split absolutely has to be a tcSplit, because we must
        -- see the IO type; and it's a newtype which is transparent to splitTyConApp.
-    io_tycon `hasKey` ioTyConKey
-  = Just (io_tycon, io_res_ty)
 
-  | Just ty' <- coreView ty    -- Look through non-recursive newtypes
-  = tcSplitIOType_maybe ty'
+       Just (io_tycon, [io_res_ty]) 
+          |  io_tycon `hasKey` ioTyConKey 
+           -> Just (io_tycon, io_res_ty, mkReflCo ty)
 
-  | otherwise
-  = Nothing
+       Just (tc, tys)
+          | not (isRecursiveTyCon tc)
+          , Just (ty, co1) <- instNewTyCon_maybe tc tys
+                 -- Newtypes that require a coercion are ok
+          -> case tcSplitIOType_maybe ty of
+               Nothing             -> Nothing
+               Just (tc, ty', co2) -> Just (tc, ty', co1 `mkTransCo` co2)
+
+       _ -> Nothing
 
 isFFITy :: Type -> Bool
 -- True for any TyCon that can possibly be an arg or result of an FFI call
@@ -1165,72 +1162,50 @@ isFFILabelTy :: Type -> Bool
 -- or a newtype of either.
 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
 
+isFFIPrimArgumentTy :: DynFlags -> Type -> Bool
+-- Checks for valid argument type for a 'foreign import prim'
+-- Currently they must all be simple unlifted types.
+isFFIPrimArgumentTy dflags ty
+   = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
+
+isFFIPrimResultTy :: DynFlags -> Type -> Bool
+-- Checks for valid result type for a 'foreign import prim'
+-- Currently it must be an unlifted type, including unboxed tuples.
+isFFIPrimResultTy dflags ty
+   = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
+
 isFFIDotnetTy :: DynFlags -> Type -> Bool
 isFFIDotnetTy dflags ty
   = checkRepTyCon (\ tc -> (legalFIResultTyCon dflags tc || 
                           isFFIDotnetObjTy ty || isStringTy ty)) ty
+       -- NB: isStringTy used to look through newtypes, but
+       --     it no longer does so.  May need to adjust isFFIDotNetTy
+       --     if we do want to look through newtypes.
 
--- 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
+isFFIDotnetObjTy :: Type -> Bool
+isFFIDotnetObjTy ty
+  = checkRepTyCon check_tc t_ty
+  where
    (_, 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)
-  | otherwise = panic "toDNType"       -- Is this right?
-    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)
-                , (ptrTyConKey,    DNPtr)
-                , (funPtrTyConKey, DNPtr)
-                , (charTyConKey,   DNChar)
-                , (boolTyConKey,   DNBool)
-                ]
+   check_tc tc = getName tc == objectTyConName
+
+isFunPtrTy :: Type -> Bool
+isFunPtrTy = checkRepTyConKey [funPtrTyConKey]
 
 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
+-- Look through newtypes, but *not* foralls
+-- Should work even for recursive newtypes
+-- eg Manuel had:      newtype T = MkT (Ptr T)
+checkRepTyCon check_tc ty
+  = go [] ty
+  where
+    go rec_nts ty
+      | Just (tc,tys) <- splitTyConApp_maybe ty
+      = case carefullySplitNewType_maybe rec_nts tc tys of
+          Just (rec_nts', ty') -> go rec_nts' ty'
+          Nothing              -> check_tc tc
+      | otherwise
+      = False
 
 checkRepTyConKey :: [Unique] -> Type -> Bool
 -- Like checkRepTyCon, but just looks at the TyCon key
@@ -1261,7 +1236,7 @@ legalFEResultTyCon tc
 
 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
 -- Checks validity of types going from Haskell -> external world
-legalOutgoingTyCon dflags safety tc
+legalOutgoingTyCon dflags _ tc
   = marshalableTyCon dflags tc
 
 legalFFITyCon :: TyCon -> Bool
@@ -1269,10 +1244,17 @@ legalFFITyCon :: TyCon -> Bool
 legalFFITyCon tc
   = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
 
+marshalableTyCon :: DynFlags -> TyCon -> Bool
 marshalableTyCon dflags tc
-  =  (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
+  =  (xopt Opt_UnliftedFFITypes dflags 
+      && isUnLiftedTyCon tc
+      && not (isUnboxedTupleTyCon tc)
+      && case tyConPrimRep tc of       -- Note [Marshalling VoidRep]
+          VoidRep -> False
+          _       -> True)
   || boxedMarshalableTyCon tc
 
+boxedMarshalableTyCon :: TyCon -> Bool
 boxedMarshalableTyCon tc
    = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
                         , int32TyConKey, int64TyConKey
@@ -1284,4 +1266,33 @@ boxedMarshalableTyCon tc
                         , stablePtrTyConKey
                         , boolTyConKey
                         ]
+
+legalFIPrimArgTyCon :: DynFlags -> TyCon -> Bool
+-- Check args of 'foreign import prim', only allow simple unlifted types.
+-- Strictly speaking it is unnecessary to ban unboxed tuples here since
+-- currently they're of the wrong kind to use in function args anyway.
+legalFIPrimArgTyCon dflags tc
+  = xopt Opt_UnliftedFFITypes dflags
+    && isUnLiftedTyCon tc
+    && not (isUnboxedTupleTyCon tc)
+
+legalFIPrimResultTyCon :: DynFlags -> TyCon -> Bool
+-- Check result type of 'foreign import prim'. Allow simple unlifted
+-- types and also unboxed tuple result types '... -> (# , , #)'
+legalFIPrimResultTyCon dflags tc
+  = xopt Opt_UnliftedFFITypes dflags
+    && isUnLiftedTyCon tc
+    && (isUnboxedTupleTyCon tc
+        || case tyConPrimRep tc of     -- Note [Marshalling VoidRep]
+          VoidRep -> False
+          _       -> True)
 \end{code}
+
+Note [Marshalling VoidRep]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+We don't treat State# (whose PrimRep is VoidRep) as marshalable.
+In turn that means you can't write
+       foreign import foo :: Int -> State# RealWorld
+
+Reason: the back end falls over with panic "primRepHint:VoidRep";
+       and there is no compelling reason to permit it