Super-monster patch implementing the new typechecker -- at last
[ghc-hetmet.git] / compiler / typecheck / TcType.lhs
index 728b0be..0025a5e 100644 (file)
@@ -19,16 +19,15 @@ module TcType (
   --------------------------------
   -- Types 
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
-  TcTyVar, TcTyVarSet, TcKind, 
-
-  BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,
+  TcTyVar, TcTyVarSet, TcKind, TcCoVar,
 
   --------------------------------
   -- MetaDetails
   UserTypeCtxt(..), pprUserTypeCtxt,
-  TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
-  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
-  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, 
+  TcTyVarDetails(..), pprTcTyVarDetails,
+  MetaDetails(Flexi, Indirect), MetaInfo(..), 
+  SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy,
   isSigTyVar, isExistentialTyVar,  isTyConableTyVar,
   metaTvRef, 
   isFlexi, isIndirect, isRuntimeUnk, isUnk,
@@ -47,18 +46,18 @@ module TcType (
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
   tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
   tcGetTyVar_maybe, tcGetTyVar,
-  tcSplitSigmaTy, tcMultiSplitSigmaTy, 
+  tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe, 
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
   tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
   eqKind, 
-  isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
+  isSigmaTy, isOverloadedTy, isRigidTy, 
   isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, 
-  isOpenSynTyConApp,
+  isSynFamilyTyConApp,
 
   ---------------------------------
   -- Misc type manipulators
@@ -70,12 +69,21 @@ module TcType (
   -- Predicate types  
   getClassPredTys_maybe, getClassPredTys, 
   isClassPred, isTyVarClassPred, isEqPred, 
-  mkDictTy, tcSplitPredTy_maybe, 
+  mkClassPred, mkIPPred, tcSplitPredTy_maybe, 
+  mkDictTy, evVarPred,
   isPredTy, isDictTy, isDictLikeTy,
   tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
-  mkClassPred, isInheritablePred, isIPPred, 
+  isIPPred, 
   isRefineableTy, isRefineablePred,
 
+  -- * Tidying type related things up for printing
+  tidyType,      tidyTypes,
+  tidyOpenType,  tidyOpenTypes,
+  tidyTyVarBndr, tidyFreeTyVars,
+  tidyOpenTyVar, tidyOpenTyVars,
+  tidyTopType,   tidyPred,
+  tidyKind, tidySkolemTyVar,
+
   ---------------------------------
   -- Foreign import and export
   isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
@@ -94,6 +102,10 @@ module TcType (
   tcSplitIOType_maybe, -- :: Type -> Maybe Type  
 
   --------------------------------
+  -- Rexported from Coercion
+  typeKind,
+
+  --------------------------------
   -- Rexported from Type
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, argTypeKind,
@@ -120,10 +132,6 @@ module TcType (
   isUnboxedTupleType,  -- Ditto
   isPrimitiveType, 
 
-  tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
-  typeKind, tidyKind,
-
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
   tcTyVarsOfType, tcTyVarsOfTypes, tcTyVarsOfPred, exactTyVarsOfType,
   exactTyVarsOfTypes, 
@@ -146,6 +154,7 @@ import VarSet
 import Type
 import Coercion
 import TyCon
+import HsExpr( HsMatchContext )
 
 -- others:
 import DynFlags
@@ -161,6 +170,7 @@ import ListSetOps
 import Outputable
 import FastString
 
+import Data.List( mapAccumL )
 import Data.IORef
 \end{code}
 
@@ -201,6 +211,7 @@ 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
@@ -215,13 +226,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}
 
 
@@ -268,43 +272,39 @@ TcBinds.tcInstSig, and its use_skols parameter.
 \begin{code}
 -- A TyVarDetails is inside a TyVar
 data TcTyVarDetails
-  = SkolemTv SkolemInfo                        -- A skolem constant
+  = SkolemTv SkolemInfo          -- A skolem constant
 
-  | MetaTv BoxInfo (IORef MetaDetails)
+  | 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.
 
-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.
+  | MetaTv MetaInfo (IORef MetaDetails)
 
 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
-
--- Generally speaking, SkolemInfo should not contain location info
--- that is contained in the Name of the tyvar with this SkolemInfo
+  = Flexi      -- Flexi type variables unify to become Indirects  
+  | Indirect TcType
+
+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 Name           -- 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
+                  -- The Name is the name of the function from whose
+                  -- type signature we got this skolem
+
+----------------------------------
+-- SkolemInfo describes a site where 
+--   a) type variables are skolemised
+--   b) an implication constraint is generated
 data SkolemInfo
   = SigSkol UserTypeCtxt       -- A skolem that is created by instantiating
                                -- a programmer-supplied type signature
@@ -314,21 +314,26 @@ data SkolemInfo
   | ClsSkol Class      -- Bound at a class decl
   | InstSkol           -- Bound at an instance decl
   | FamInstSkol        -- Bound at a family instance decl
-  | PatSkol DataCon    -- An existential type variable bound by a pattern for
-                       -- 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          -- An arrow form (see TcArrows)
+  | PatSkol            -- An existential type variable bound by a pattern for
+      DataCon           -- a data constructor with an existential type.
+      (HsMatchContext Name)    
+            -- 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'.  
 
-  | RuleSkol RuleName  -- The LHS of a RULE
-  | GenSkol [TcTyVar]  -- Bound when doing a subsumption check for 
-           TcType      --      (forall tvs. ty)
+  | ArrowSkol          -- An arrow form (see TcArrows)
+
+  | IPSkol [IPName Name]  -- Binding site of an implicit parameter
 
+  | RuleSkol RuleName  -- The LHS of a RULE
+  | GenSkol TcType     -- Bound when doing a subsumption check for ty
   | RuntimeUnkSkol      -- a type variable used to represent an unknown
                         -- runtime type (used in the GHCi debugger)
 
+  | NoScSkol           -- Used for the "self" superclass when solving
+                       -- superclasses; don't generate superclasses of me
+
   | UnkSkol            -- Unhelpful info (until I improve it)
 
 -------------------------------------
@@ -400,7 +405,7 @@ kind_var_occ = mkOccName tvName "k"
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 -- For debugging
 pprTcTyVarDetails (SkolemTv _)         = ptext (sLit "sk")
-pprTcTyVarDetails (MetaTv BoxTv _)     = ptext (sLit "box")
+pprTcTyVarDetails (FlatSkol _)         = ptext (sLit "fsk")
 pprTcTyVarDetails (MetaTv TauTv _)     = ptext (sLit "tau")
 pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext (sLit "sig")
 
@@ -418,29 +423,6 @@ pprUserTypeCtxt (ForSigCtxt n)  = ptext (sLit "the foreign declaration for") <+>
 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( isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv ) )
-    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
-  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) = (env2, GenSkol tvs1 ty1)
-                           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
@@ -448,33 +430,38 @@ pprSkolTvBinding tv
   = ASSERT ( isTcTyVar tv )
     quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
   where
-    ppr_details (MetaTv TauTv _)       = ptext (sLit "is a meta type variable")
-    ppr_details (MetaTv BoxTv _)       = ptext (sLit "is a boxy type variable")
-    ppr_details (MetaTv (SigTv info) _) = ppr_skol info
-    ppr_details (SkolemTv info)                = ppr_skol info
+    ppr_details (SkolemTv info)      = ppr_skol info
+    ppr_details (FlatSkol _)        = ptext (sLit "is a flattening type variable")
+    ppr_details (MetaTv TauTv _)     = ptext (sLit "is a meta type variable")
+    ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for") <+> quotes (ppr n)
 
     ppr_skol UnkSkol       = ptext (sLit "is an unknown type variable")        -- Unhelpful
     ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type")
     ppr_skol info           = sep [ptext (sLit "is a rigid type variable bound by"),
                                   sep [pprSkolInfo info, 
-                                        nest 2 (ptext (sLit "at") <+> ppr (getSrcLoc tv))]]
+                                       nest 2 (ptext (sLit "at") <+> ppr (getSrcLoc tv))]]
  
 pprSkolInfo :: SkolemInfo -> SDoc
-pprSkolInfo (SigSkol ctxt)   = pprUserTypeCtxt ctxt
-pprSkolInfo (ClsSkol cls)    = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
-pprSkolInfo InstSkol         = ptext (sLit "the instance declaration")
-pprSkolInfo FamInstSkol      = ptext (sLit "the family instance declaration")
-pprSkolInfo (RuleSkol name)  = ptext (sLit "the RULE") <+> doubleQuotes (ftext name)
-pprSkolInfo ArrowSkol        = ptext (sLit "the arrow form")
-pprSkolInfo (PatSkol dc)     = sep [ptext (sLit "the constructor") <+> quotes (ppr dc)]
-pprSkolInfo (GenSkol tvs ty) = sep [ptext (sLit "the polymorphic type"), 
-                                   nest 2 (quotes (ppr (mkForAllTys tvs ty)))]
+-- Complete the sentence "is a rigid type variable bound by..."
+pprSkolInfo (SigSkol ctxt)  = pprUserTypeCtxt ctxt
+pprSkolInfo (IPSkol ips)    = ptext (sLit "the implicit-parameter bindings for")
+                              <+> pprWithCommas ppr ips
+pprSkolInfo (ClsSkol cls)   = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo InstSkol        = ptext (sLit "the instance declaration")
+pprSkolInfo NoScSkol        = ptext (sLit "the instance declaration (self)")
+pprSkolInfo FamInstSkol     = ptext (sLit "the family instance declaration")
+pprSkolInfo (RuleSkol name) = ptext (sLit "the RULE") <+> doubleQuotes (ftext name)
+pprSkolInfo ArrowSkol       = ptext (sLit "the arrow form")
+pprSkolInfo (PatSkol dc _)  = sep [ ptext (sLit "a pattern with constructor")
+                                    , ppr dc <+> dcolon <+> ppr (dataConUserType dc) ]
+pprSkolInfo (GenSkol ty)    = sep [ ptext (sLit "the polymorphic type")
+                                 , quotes (ppr ty) ]
 
 -- UnkSkol
 -- For type variables the others are dealt with by pprSkolTvBinding.  
 -- For Insts, these cases should not happen
-pprSkolInfo UnkSkol = panic "UnkSkol"
-pprSkolInfo RuntimeUnkSkol = panic "RuntimeUnkSkol"
+pprSkolInfo UnkSkol        = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "UnkSkol")
+pprSkolInfo RuntimeUnkSkol = WARN( True, text "pprSkolInfo: RuntimeUnkSkol" ) ptext (sLit "RuntimeUnkSkol")
 
 instance Outputable MetaDetails where
   ppr Flexi         = ptext (sLit "Flexi")
@@ -484,6 +471,129 @@ instance Outputable MetaDetails where
 
 %************************************************************************
 %*                                                                     *
+\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 env@(tidy_env, subst) tyvar
+  = case tidyOccName tidy_env (getOccName name) of
+      (tidy', occ') -> ((tidy', subst'), tyvar'')
+       where
+         subst' = extendVarEnv subst tyvar tyvar''
+         tyvar' = setTyVarName tyvar name'
+         name'  = tidyNameOcc name occ'
+               -- Don't forget to tidy the kind for coercions!
+         tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
+                 | otherwise     = tyvar'
+         kind'  = tidyType env (tyVarKind tyvar)
+  where
+    name = tyVarName tyvar
+
+---------------
+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
+    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
+
+---------------
+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
+
+---------------
+tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
+-- Tidy the type inside a GenSkol, preparatory to printing it
+tidySkolemTyVar env tv
+  = ASSERT( isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv ) )
+    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
+  where
+    (env1, info1) = case tcTyVarDetails tv of
+                       SkolemTv info -> (env1, SkolemTv info')
+                               where
+                                 (env1, info') = tidy_skol_info env info
+                       info -> (env, info)
+
+    tidy_skol_info env (GenSkol ty) = (env1, GenSkol ty1)
+                           where
+                             (env1, ty1)  = tidyOpenType env ty
+    tidy_skol_info env info = (env, info)
+
+---------------
+tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
+tidyKind env k = tidyOpenType env k
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
                Predicates
 %*                                                                     *
 %************************************************************************
@@ -496,7 +606,7 @@ isImmutableTyVar tv
   | otherwise    = True
 
 isTyConableTyVar, isSkolemTyVar, isExistentialTyVar, 
-  isBoxyTyVar, isMetaTyVar :: TcTyVar -> Bool 
+  isMetaTyVar :: TcTyVar -> Bool 
 
 isTyConableTyVar tv    
        -- True of a meta-type variable that can be filled in 
@@ -504,16 +614,15 @@ isTyConableTyVar tv
        -- not a SigTv
   = ASSERT( isTcTyVar tv) 
     case tcTyVarDetails tv of
-       MetaTv BoxTv      _ -> True
-       MetaTv TauTv      _ -> True
-       MetaTv (SigTv {}) _ -> False
-       SkolemTv {}         -> False
+       MetaTv TauTv _ -> True
+       _              -> False
        
 isSkolemTyVar tv 
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-       SkolemTv _         -> True
-       MetaTv _ _         -> False
+       SkolemTv {} -> True
+        FlatSkol {} -> True
+       MetaTv {}   -> False
 
 isExistentialTyVar tv  -- Existential type variable, bound by a pattern
   = ASSERT( isTcTyVar tv )
@@ -527,11 +636,9 @@ isMetaTyVar tv
        MetaTv _ _ -> True
        _          -> False
 
-isBoxyTyVar tv 
-  = ASSERT( isTcTyVar tv )
-    case tcTyVarDetails tv of
-       MetaTv BoxTv _ -> True
-       _              -> False
+isMetaTyVarTy :: TcType -> Bool
+isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
+isMetaTyVarTy _            = False
 
 isSigTyVar :: Var -> Bool
 isSigTyVar tv 
@@ -585,8 +692,7 @@ mkPhiTy theta ty = foldr (\p r -> mkFunTy (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
@@ -601,9 +707,6 @@ isTauTyCon 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 isImmutableTyVar (varSetElems (tcTyVarsOfType ty))
@@ -686,22 +789,21 @@ 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
-       ([], [], _) -> ([], 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
@@ -864,6 +966,12 @@ tcInstHeadTyAppAllTyVars ty
 %************************************************************************
 
 \begin{code}
+evVarPred :: EvVar -> PredType
+evVarPred var
+  = case tcSplitPredTy_maybe (varType var) of
+      Just pred -> pred
+      Nothing   -> pprPanic "evVarPred" (ppr var <+> ppr (varType var))
+
 tcSplitPredTy_maybe :: Type -> Maybe PredType
    -- Returns Just for predicates only
 tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
@@ -902,6 +1010,8 @@ getClassPredTys _ = panic "getClassPredTys"
 mkDictTy :: Class -> [Type] -> Type
 mkDictTy clas tys = mkPredTy (ClassP clas tys)
 
+
+
 isDictLikeTy :: Type -> Bool
 -- Note [Dictionary-like types]
 isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
@@ -943,22 +1053,12 @@ constraints build tuples.
 --------------------- Implicit parameters ---------------------------------
 
 \begin{code}
+mkIPPred :: IPName Name -> Type -> PredType
+mkIPPred ip ty = IParam ip ty
+
 isIPPred :: PredType -> Bool
 isIPPred (IParam _ _) = True
 isIPPred _            = 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 (EqPred _ _) = True
-isInheritablePred _            = False
 \end{code}
 
 --------------------- Equality predicates ---------------------------------
@@ -988,7 +1088,7 @@ isSigmaTy _              = False
 
 isOverloadedTy :: Type -> Bool
 -- Yes for a type of a function that might require evidence-passing
--- Used only by bindInstsOfLocalFuns/Pats
+-- Used only by bindLocalMethods
 -- NB: be sure to check for type with an equality predicate; hence isCoVar
 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
 isOverloadedTy (ForAllTy tv ty) = isCoVar tv || isOverloadedTy ty
@@ -1031,10 +1131,10 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 -- NB: Currently used in places where we have already expanded type synonyms;
 --     hence no 'coreView'.  This could, however, be changed without breaking
 --     any code.
-isOpenSynTyConApp :: TcTauType -> Bool
-isOpenSynTyConApp (TyConApp tc tys) = isOpenSynTyCon tc && 
+isSynFamilyTyConApp :: TcTauType -> Bool
+isSynFamilyTyConApp (TyConApp tc tys) = isSynFamilyTyCon tc && 
                                       length tys == tyConArity tc 
-isOpenSynTyConApp _other            = False
+isSynFamilyTyConApp _other            = False
 \end{code}
 
 
@@ -1185,7 +1285,7 @@ tcSplitIOType_maybe ty
 
        Just (io_tycon, [io_res_ty]) 
           |  io_tycon `hasKey` ioTyConKey 
-          -> Just (io_tycon, io_res_ty, IdCo)
+          -> Just (io_tycon, io_res_ty, IdCo ty)
 
        Just (tc, tys)
           | not (isRecursiveTyCon tc)