fix haddock submodule pointer
[ghc-hetmet.git] / compiler / typecheck / TcType.lhs
index 9cc9170..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}
@@ -10,7 +11,7 @@ compiler.  These parts
                newtypes, and predicates are meaningful. 
        * look through usage types
 
-The "tc" prefix is for "typechechecker", because the type checker
+The "tc" prefix is for "TypeChecker", because the type checker
 is the principal client.
 
 \begin{code}
@@ -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,36 +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, 
-  tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
-  tcSplitSigmaTy, tcMultiSplitSigmaTy, 
+  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
+  tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
+  tcGetTyVar_maybe, tcGetTyVar,
+  tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe, 
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
-  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
-  isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
-  isDoubleTy, isFloatTy, isIntTy, isStringTy,
-  isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
+  eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
+  eqKind, 
+  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, 
-  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
@@ -78,120 +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
-  unliftedTypeKind, liftedTypeKind, unboxedTypeKind,
+  -- Rexported from Kind
+  Kind, typeKind,
+  unliftedTypeKind, liftedTypeKind, argTypeKind,
   openTypeKind, mkArrowKind, mkArrowKinds, 
-  isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, 
-  isArgTypeKind, isSubKind, defaultKind, 
+  isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind, 
+  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,
-  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 )  -- friend
-
-import Type            (       -- Re-exports
-                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
-                         tyVarsOfTheta, Kind, PredType(..),
-                         ThetaType, unliftedTypeKind, unboxedTypeKind,
-                         liftedTypeKind, openTypeKind, mkArrowKind,
-                         isLiftedTypeKind, isUnliftedTypeKind, 
-                         mkArrowKinds, mkForAllTy, mkForAllTys,
-                         defaultKind, isArgTypeKind, isOpenTypeKind,
-                         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, 
-
-                         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,
-                         pprKind, pprParendKind,
-                         pprType, pprParendType, pprTyThingCategory,
-                         pprPred, pprTheta, pprThetaArrow, pprClassPred
-                       )
-import TyCon           ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )
-import DataCon         ( DataCon, dataConStupidTheta, dataConResTys )
-import Class           ( Class )
-import Var             ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
-import ForeignCall     ( Safety, playSafe, 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 )
+import DynFlags
+import Name hiding (varName)
 import NameSet
-import VarEnv          ( TidyEnv )
-import OccName         ( OccName, mkDictOcc )
-import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
-import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
-import BasicTypes      ( IPName(..), Arity, ipNameName )
-import SrcLoc          ( SrcLoc, SrcSpan )
-import Util            ( snocView, 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}
 
 %************************************************************************
 %*                                                                     *
@@ -230,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
@@ -244,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}
 
 
@@ -284,80 +260,72 @@ 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 would 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.  
+constant, SigTv, which can unify with other SigTvs.  These are *not* treated
+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.
 
 
 \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
-  | 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
@@ -372,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 = []
@@ -385,6 +357,31 @@ data UserTypeCtxt
 -- will become type T = forall a. a->a
 --
 -- With gla-exts that's right, but for H98 we should complain. 
+
+---------------------------------
+-- Kind variables:
+
+mkKindName :: Unique -> Name
+mkKindName unique = mkSystemName unique kind_var_occ
+
+kindVarRef :: KindVar -> IORef MetaDetails
+kindVarRef tc = 
+  ASSERT ( isTcTyVar tc )
+  case tcTyVarDetails tc of
+    MetaTv TauTv ref -> ref
+    _                -> pprPanic "kindVarRef" (ppr tc)
+
+mkKindVar :: Unique -> IORef MetaDetails -> KindVar
+mkKindVar u r 
+  = mkTcTyVar (mkKindName u)
+              tySuperKind  -- not sure this is right,
+                            -- do we need kind vars for
+                            -- coercions?
+              (MetaTv TauTv r)
+
+kind_var_occ :: OccName        -- Just one for all KindVars
+                       -- They may be jiggled by tidying
+kind_var_occ = mkOccName tvName "k"
 \end{code}
 
 %************************************************************************
@@ -396,76 +393,171 @@ data UserTypeCtxt
 \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 )
-    (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 (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
-                           where
-                             (env1, tvs1) = tidyOpenTyVars env tvs
-                             (env2, ty1)  = tidyOpenType env1 ty
-                     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
-  = 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 (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}
 
 %************************************************************************
 %*                                                                     *
@@ -474,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}
 
 
@@ -532,10 +644,11 @@ isIndirect other        = False
 %************************************************************************
 
 \begin{code}
+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.
@@ -543,43 +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 = isTauTy (snd (synTyConDefn tc))
-             | otherwise     = True
+isTauTyCon tc 
+  | 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
@@ -595,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.
@@ -605,50 +701,63 @@ 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 = 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) = True
-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 -> ([PredType], Type)
-tcSplitPhiTy ty = split ty ty []
- where
-  split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
-  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 ty             ts = (reverse ts, orig_ty)
+tcSplitPhiTy :: Type -> (ThetaType, Type)
+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
                        (tvs, rho) -> case tcSplitPhiTy rho 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
@@ -662,7 +771,7 @@ tcSplitTyConApp_maybe (FunTy 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
-tcSplitTyConApp_maybe other            = Nothing
+tcSplitTyConApp_maybe _                 = Nothing
 
 -----------------------
 tcSplitFunTys :: Type -> ([Type], Type)
@@ -673,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 
@@ -692,20 +808,21 @@ tcSplitFunTysN ty n_args
   | otherwise
   = ([], ty)
 
-tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
-tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
+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)
 
 -----------------------
 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
-tcSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
-tcSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
-tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
-                                       Just (tys', ty') -> Just (TyConApp tc tys', ty')
-                                       Nothing          -> Nothing
-tcSplitAppTy_maybe other            = Nothing
+tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
 
+tcSplitAppTy :: Type -> (Type, Type)
 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
                    Just stuff -> stuff
                    Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
@@ -721,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)
@@ -731,28 +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)
+       _ -> 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
-       NoteTy _ ty     -> tcValidInstHeadTy ty
-       TyConApp tc tys -> not (isSynTyCon tc) && ok tys
+        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
+       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
@@ -760,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}
 
 
@@ -773,94 +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 ---------------------------------
+Superclasses
 
 \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)
-
-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 ---------------------------------
-
-\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}
-
---------------------- 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 ]
+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}
 
 
@@ -877,31 +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
-isAddrTy       = is_tc addrTyConKey
+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
@@ -910,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}
+
 
 %************************************************************************
 %*                                                                     *
@@ -926,11 +1018,11 @@ deNoteType ty = ty
 
 \begin{code}
 tcTyVarsOfType :: Type -> TcTyVarSet
--- Just the tc type variables free in the type
+-- Just the *TcTyVars* free in the type
+-- (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
@@ -941,81 +1033,63 @@ tcTyVarsOfTypes :: [Type] -> TyVarSet
 tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
 
 tcTyVarsOfPred :: PredType -> TyVarSet
-tcTyVarsOfPred (IParam _ ty)  = tcTyVarsOfType ty
-tcTyVarsOfPred (ClassP _ tys) = tcTyVarsOfTypes tys
-\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] belos.
-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
-
-    go_pred (IParam _ ty)  = go ty
-    go_pred (ClassP _ tys) = exactTyVarsOfTypes tys
-
-exactTyVarsOfTypes :: [TcType] -> TyVarSet
-exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
+tcTyVarsOfPred (IParam _ ty)   = tcTyVarsOfType ty
+tcTyVarsOfPred (ClassP _ tys)  = tcTyVarsOfTypes tys
+tcTyVarsOfPred (EqPred ty1 ty2) = tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
 \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 (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}
 
 
@@ -1030,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
@@ -1070,83 +1150,62 @@ 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]
+isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
 
 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]
+isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
 
 isFFILabelTy :: Type -> Bool
 -- The type of a foreign label must be Ptr, FunPtr, Addr,
 -- or a newtype of either.
-isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
+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)
-    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)
-                ]
+   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
@@ -1177,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
@@ -1185,19 +1244,55 @@ 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
                         , wordTyConKey, word8TyConKey, word16TyConKey
                         , word32TyConKey, word64TyConKey
                         , floatTyConKey, doubleTyConKey
-                        , addrTyConKey, ptrTyConKey, funPtrTyConKey
+                        , ptrTyConKey, funPtrTyConKey
                         , charTyConKey
                         , 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