Simon's big boxy-type commit
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index e1bfedb..448f10a 100644 (file)
@@ -20,12 +20,16 @@ module TcType (
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
   TcTyVar, TcTyVarSet, TcKind, 
 
+  BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,
+
   --------------------------------
   -- MetaDetails
-  TcTyVarDetails(..),
-  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
-  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, skolemTvInfo, metaTvRef,
-  isFlexi, isIndirect,
+  UserTypeCtxt(..), pprUserTypeCtxt,
+  TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
+  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, isSigTyVar, isExistentialTyVar, 
+  metaTvRef, 
+  isFlexi, isIndirect, 
 
   --------------------------------
   -- Builders
@@ -34,20 +38,22 @@ module TcType (
   --------------------------------
   -- Splitters  
   -- These are important because they do not look through newtypes
+  tcView,
   tcSplitForAllTys, tcSplitPhiTy, 
-  tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
+  tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
-  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
-  tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
+  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, 
+  tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
+  tcSplitSigmaTy, tcMultiSplitSigmaTy, 
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
-  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
-  isSigmaTy, isOverloadedTy, 
-  isDoubleTy, isFloatTy, isIntTy,
+  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
+  isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
+  isDoubleTy, isFloatTy, isIntTy, isStringTy,
   isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
-  isTauTy, tcIsTyVarTy, tcIsForAllTy,
+  isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, 
 
   ---------------------------------
   -- Misc type manipulators
@@ -60,8 +66,9 @@ module TcType (
   getClassPredTys_maybe, getClassPredTys, 
   isClassPred, isTyVarClassPred, 
   mkDictTy, tcSplitPredTy_maybe, 
-  isPredTy, isDictTy, tcSplitDFunTy, predTyUnique, 
+  isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
   mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
+  dataConsStupidTheta, isRefineableTy,
 
   ---------------------------------
   -- Foreign import and export
@@ -88,29 +95,30 @@ module TcType (
   Type, PredType(..), ThetaType, 
   mkForAllTy, mkForAllTys, 
   mkFunTy, mkFunTys, zipFunTys, 
-  mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+  mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, 
 
   -- Type substitutions
   TvSubst(..),         -- Representation visible to a few friends
   TvSubstEnv, emptyTvSubst,
-  mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
-  getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
-  extendTvSubst, extendTvSubstList, isInScope,
-  substTy, substTys, substTyWith, substTheta, substTyVar, 
+  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
+  getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
+  extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
+  substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
 
   isUnLiftedType,      -- Source types are always lifted
   isUnboxedTupleType,  -- Ditto
   isPrimitiveType, 
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
-  typeKind, 
+  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
+  typeKind, tidyKind,
 
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
+  tcTyVarsOfType, tcTyVarsOfTypes, exactTyVarsOfType, exactTyVarsOfTypes,
 
   pprKind, pprParendKind,
-  pprType, pprParendType,
+  pprType, pprParendType, pprTyThingCategory,
   pprPred, pprTheta, pprThetaArrow, pprClassPred
 
   ) where
@@ -118,20 +126,19 @@ module TcType (
 #include "HsVersions.h"
 
 -- friends:
-import TypeRep         ( Type(..), TyNote(..), funTyCon )  -- friend
+import TypeRep         ( Type(..), funTyCon )  -- friend
 
 import Type            (       -- Re-exports
                          tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
-                         tyVarsOfTheta, Kind, Type, PredType(..),
+                         tyVarsOfTheta, Kind, PredType(..),
                          ThetaType, unliftedTypeKind, 
                          liftedTypeKind, openTypeKind, mkArrowKind,
                          isLiftedTypeKind, isUnliftedTypeKind, 
-                         isOpenTypeKind, 
                          mkArrowKinds, mkForAllTy, mkForAllTys,
                          defaultKind, isArgTypeKind, isOpenTypeKind,
                          mkFunTy, mkFunTys, zipFunTys, 
-                         mkTyConApp, mkGenTyConApp, mkAppTy,
-                         mkAppTys, mkSynTy, applyTy, applyTys,
+                         mkTyConApp, mkAppTy,
+                         mkAppTys, applyTy, applyTys,
                          mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
                          mkPredTys, isUnLiftedType, 
                          isUnboxedTupleType, isPrimitiveType,
@@ -139,40 +146,47 @@ import Type               (       -- Re-exports
                          tidyTopType, tidyType, tidyPred, tidyTypes,
                          tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
                          tidyTyVarBndr, tidyOpenTyVar,
-                         tidyOpenTyVars, 
-                         isSubKind, 
+                         tidyOpenTyVars, tidyKind,
+                         isSubKind, tcView,
+
+                         tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
+                         tcEqPred, tcCmpPred, tcEqTypeX, 
+
                          TvSubst(..),
-                         TvSubstEnv, emptyTvSubst,
-                         mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+                         TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv,
+                         mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
                          getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
-                         extendTvSubst, extendTvSubstList, isInScope,
-                         substTy, substTys, substTyWith, substTheta, substTyVar, 
+                         extendTvSubst, extendTvSubstList, isInScope, notElemTvSubst,
+                         substTy, substTys, substTyWith, substTheta, 
+                         substTyVar, substTyVarBndr, substPred, lookupTyVar,
 
                          typeKind, repType,
                          pprKind, pprParendKind,
-                         pprType, pprParendType,
+                         pprType, pprParendType, pprTyThingCategory,
                          pprPred, pprTheta, pprThetaArrow, pprClassPred
                        )
-import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
-import DataCon         ( DataCon )
+import TyCon           ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )
+import DataCon         ( DataCon, dataConStupidTheta, dataConResTys )
 import Class           ( Class )
-import Var             ( TyVar, Id, isTcTyVar, tcTyVarDetails )
+import Var             ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
 import ForeignCall     ( Safety, playSafe, DNType(..) )
-import VarEnv
+import Unify           ( tcMatchTys )
 import VarSet
 
 -- others:
-import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
+import DynFlags                ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import NameSet
+import VarEnv          ( TidyEnv )
 import OccName         ( OccName, mkDictOcc )
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
-import BasicTypes      ( IPName(..), ipNameName )
-import Unique          ( Unique, Uniquable(..) )
+import BasicTypes      ( IPName(..), Arity, ipNameName )
 import SrcLoc          ( SrcLoc, SrcSpan )
-import Util            ( cmpList, thenCmp, snocView )
-import Maybes          ( maybeToBool, expectJust )
+import Util            ( snocView, equalLength )
+import Maybes          ( maybeToBool, expectJust, mapCatMaybes )
+import ListSetOps      ( hasNoDups )
+import List            ( nubBy )
 import Outputable
 import DATA_IOREF
 \end{code}
@@ -214,12 +228,14 @@ tau ::= tyvar
 -- provided it expands to the required form.
 
 \begin{code}
-type TcType = Type             -- A TcType can have mutable type variables
+type TcTyVar = TyVar   -- Used only during type inference
+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
 
+-- These types do not have boxy type variables in them
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
 type TcSigmaType    = TcType
@@ -227,6 +243,13 @@ 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}
 
 
@@ -241,16 +264,79 @@ checking.  It's attached to mutable type variables only.
 It's knot-tied back to Var.lhs.  There is no reason in principle
 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 
-\begin{code}
-type TcTyVar = TyVar   -- Used only during type inference
 
+Note [Signature skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+  x :: [a]
+  y :: b
+  (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment.  We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+       ( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to 
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other.  Alas.
+
+On the other hand, we *must* use skolems for signature type variables, 
+becuase GADT type refinement refines skolems only.  
+
+One solution 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.  
+
+
+\begin{code}
 -- A TyVarDetails is inside a TyVar
 data TcTyVarDetails
-  = SkolemTv SkolemInfo                -- A skolem constant
-  | MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
+  = 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.
+
+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 Name       -- Bound at a type signature
+  = 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
@@ -261,36 +347,133 @@ data SkolemInfo
                        -- variable for 'a'.  
   | ArrowSkol SrcSpan  -- An arrow form (see TcArrows)
 
-  | GenSkol TcType     -- Bound when doing a subsumption check for this type
+  | GenSkol [TcTyVar]  -- Bound when doing a subsumption check for 
+           TcType      --      (forall tvs. ty)
            SrcSpan
 
-data MetaDetails
-  = Flexi          -- Flexi type variables unify to become 
-                   -- Indirects.  
+  | UnkSkol            -- Unhelpful info (until I improve it)
+
+-------------------------------------
+-- UserTypeCtxt describes the places where a 
+-- programmer-written type signature can occur
+data UserTypeCtxt 
+  = FunSigCtxt Name    -- Function type signature
+                       -- Also used for types in SPECIALISE pragmas
+  | ExprSigCtxt                -- Expression type signature
+  | ConArgCtxt Name    -- Data constructor argument
+  | TySynCtxt Name     -- RHS of a type synonym decl
+  | GenPatCtxt         -- Pattern in generic decl
+                       --      f{| a+b |} (Inl x) = ...
+  | LamPatSigCtxt              -- Type sig in lambda pattern
+                       --      f (x::t) = ...
+  | BindPatSigCtxt     -- Type sig in pattern binding pattern
+                       --      (x::t, y) = e
+  | 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
+
+-- Notes re TySynCtxt
+-- We allow type synonyms that aren't types; e.g.  type List = []
+--
+-- If the RHS mentions tyvars that aren't in scope, we'll 
+-- quantify over them:
+--     e.g.    type T = a->a
+-- will become type T = forall a. a->a
+--
+-- With gla-exts that's right, but for H98 we should complain. 
+\end{code}
 
-  | Indirect TcType  -- Type indirections, treated as wobbly 
-                     -- for the purpose of GADT unification.
+%************************************************************************
+%*                                                                     *
+               Pretty-printing
+%*                                                                     *
+%************************************************************************
 
-pprSkolemTyVar :: TcTyVar -> SDoc
-pprSkolemTyVar tv
+\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")
+
+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 )
-    quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv)
-
-instance Outputable SkolemInfo where
-  ppr (SigSkol id)  = ptext SLIT("the type signature for") <+> quotes (ppr id)
-  ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
-  ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
-  ppr (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
-  ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
-                           nest 2 (ptext SLIT("at") <+> ppr loc)]
-  ppr (GenSkol ty loc) = sep [ptext SLIT("the polymorphic type") <+> quotes (ppr ty),
-                           nest 2 (ptext SLIT("at") <+> ppr loc)]
+    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
+  where
+    (env1, info1) = case tcTyVarDetails tv of
+                     SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
+                           where
+                             (env1, tvs1) = tidyOpenTyVars env tvs
+                             (env2, ty1)  = tidyOpenType env1 ty
+                     info -> (env, info)
+                    
+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)
+  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"
 
 instance Outputable MetaDetails where
   ppr Flexi        = ptext SLIT("Flexi")
   ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+               Predicates
+%*                                                                     *
+%************************************************************************
 
-isImmutableTyVar, isSkolemTyVar, isMetaTyVar :: TyVar -> Bool
+\begin{code}
+isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isBoxyTyVar, isMetaTyVar :: TyVar -> Bool
 isImmutableTyVar tv
   | isTcTyVar tv = isSkolemTyVar tv
   | otherwise    = True
@@ -298,26 +481,39 @@ isImmutableTyVar tv
 isSkolemTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-       SkolemTv _ -> True
-       MetaTv _   -> False
+       SkolemTv _         -> True
+       MetaTv _ _         -> False
+
+isExistentialTyVar tv  -- Existential type variable, bound by a pattern
+  = ASSERT( isTcTyVar tv )
+    case tcTyVarDetails tv of
+       SkolemTv (PatSkol _ _) -> True
+       other                  -> False
 
 isMetaTyVar tv 
+  = ASSERT2( isTcTyVar tv, ppr tv )
+    case tcTyVarDetails tv of
+       MetaTv _ _ -> True
+       other      -> False
+
+isBoxyTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-       SkolemTv _ -> False
-       MetaTv _   -> True
+       MetaTv BoxTv _ -> True
+       other          -> False
 
-skolemTvInfo :: TyVar -> SkolemInfo
-skolemTvInfo tv 
+isSigTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-       SkolemTv info -> info
+       MetaTv (SigTv _) _ -> True
+       other              -> False
 
 metaTvRef :: TyVar -> IORef MetaDetails
 metaTvRef tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-        MetaTv ref -> ref
+       MetaTv _ ref -> ref
+       other      -> pprPanic "metaTvRef" (ppr tv)
 
 isFlexi, isIndirect :: MetaDetails -> Bool
 isFlexi Flexi = True
@@ -341,28 +537,47 @@ mkPhiTy :: [PredType] -> Type -> Type
 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
 \end{code}
 
-@isTauTy@ tests for nested for-alls.
+@isTauTy@ tests for nested for-alls.  It should not be called on a boxy type.
 
 \begin{code}
 isTauTy :: Type -> Bool
-isTauTy (TyVarTy v)     = True
-isTauTy (TyConApp _ tys) = all isTauTy tys
-isTauTy (NewTcApp _ tys) = all isTauTy tys
-isTauTy (AppTy a b)     = isTauTy a && isTauTy b
-isTauTy (FunTy a b)     = isTauTy a && isTauTy b
-isTauTy (PredTy p)      = True         -- Don't look through source types
-isTauTy (NoteTy _ ty)   = isTauTy ty
-isTauTy other           = False
-\end{code}
-
-\begin{code}
+isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
+isTauTy (TyVarTy tv)    = ASSERT( not (isTcTyVar tv && isBoxyTyVar tv) )
+                          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
+
+
+isTauTyCon :: TyCon -> Bool
+-- Returns False for type synonyms whose expansion is a polytype
+isTauTyCon tc | isSynTyCon 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 
                                -- construct a dictionary function name
+getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
 getDFunTyKey (TyVarTy tv)    = getOccName tv
 getDFunTyKey (TyConApp tc _) = getOccName tc
-getDFunTyKey (NewTcApp tc _) = getOccName tc
 getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
-getDFunTyKey (NoteTy _ t)    = getDFunTyKey t
 getDFunTyKey (FunTy arg _)   = getOccName funTyCon
 getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
 getDFunTyKey ty                     = pprPanic "getDFunTyKey" (pprType ty)
@@ -388,27 +603,46 @@ variables.  It's up to you to make sure this doesn't matter.
 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 (NoteTy n  ty)   tvs = split orig_ty ty tvs
      split orig_ty t               tvs = (reverse tvs, orig_ty)
 
+tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
 tcIsForAllTy (ForAllTy tv ty) = True
-tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
 tcIsForAllTy t               = False
 
 tcSplitPhiTy :: Type -> ([PredType], Type)
 tcSplitPhiTy ty = split ty ty []
  where
+  split orig_ty 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 (NoteTy n ty)  ts = split orig_ty ty ts
   split orig_ty ty             ts = (reverse ts, orig_ty)
 
 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
                        (tvs, rho) -> case tcSplitPhiTy rho of
                                        (theta, tau) -> (tvs, theta, tau)
 
+-----------------------
+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)
+
+-----------------------
 tcTyConAppTyCon :: Type -> TyCon
 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
 
@@ -421,15 +655,15 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
                        Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 
 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
-tcSplitTyConApp_maybe (NewTcApp tc tys) = Just (tc, tys)
 tcSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
-tcSplitTyConApp_maybe (NoteTy n ty)     = tcSplitTyConApp_maybe ty
        -- Newtypes are opaque, so they may be split
        -- However, predicates are not treated
        -- as tycon applications by the type checker
-tcSplitTyConApp_maybe other                    = Nothing
+tcSplitTyConApp_maybe other            = Nothing
 
+-----------------------
 tcSplitFunTys :: Type -> ([Type], Type)
 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
                        Nothing        -> ([], ty)
@@ -438,24 +672,37 @@ 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 (NoteTy n ty)    = tcSplitFunTy_maybe ty
 tcSplitFunTy_maybe other           = Nothing
 
+tcSplitFunTysN
+       :: TcRhoType 
+       -> Arity                -- N: Number of desired args
+       -> ([TcSigmaType],      -- Arg types (N or fewer)
+           TcSigmaType)        -- The rest of the type
+
+tcSplitFunTysN ty n_args
+  | n_args == 0
+  = ([], ty)
+  | Just (arg,res) <- tcSplitFunTy_maybe ty
+  = case tcSplitFunTysN res (n_args - 1) of
+       (args, res) -> (arg:args, res)
+  | otherwise
+  = ([], ty)
+
 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 
 
+-----------------------
 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
+tcSplitAppTy_maybe 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 (NoteTy n ty)     = tcSplitAppTy_maybe ty
 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
                                        Just (tys', ty') -> Just (TyConApp tc tys', ty')
                                        Nothing          -> Nothing
-tcSplitAppTy_maybe (NewTcApp tc tys) = case snocView tys of
-                                       Just (tys', ty') -> Just (NewTcApp tc tys', ty')
-                                       Nothing          -> Nothing
 tcSplitAppTy_maybe other            = Nothing
 
 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
@@ -470,9 +717,10 @@ tcSplitAppTys ty
                   Just (ty', arg) -> go ty' (arg:args)
                   Nothing         -> (ty,args)
 
+-----------------------
 tcGetTyVar_maybe :: Type -> Maybe TyVar
+tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
 tcGetTyVar_maybe (TyVarTy tv)  = Just tv
-tcGetTyVar_maybe (NoteTy _ t)  = tcGetTyVar_maybe t
 tcGetTyVar_maybe other         = Nothing
 
 tcGetTyVar :: String -> Type -> TyVar
@@ -480,31 +728,40 @@ tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 
 tcIsTyVarTy :: Type -> Bool
 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
-\end{code}
-
-The type of a method for class C is always of the form:
-       Forall a1..an. C a1..an => sig_ty
-where sig_ty is the type given by the method's signature, and thus in general
-is a ForallTy.  At the point that splitMethodTy is called, it is expected
-that the outer Forall has already been stripped off.  splitMethodTy then
-returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
-
-\begin{code}
-tcSplitMethodTy :: Type -> (PredType, Type)
-tcSplitMethodTy ty = split ty
- where
-  split (FunTy arg res) = case tcSplitPredTy_maybe arg of
-                           Just p  -> (p, res)
-                           Nothing -> panic "splitMethodTy"
-  split (NoteTy n ty)  = split ty
-  split _               = panic "splitMethodTy"
 
+-----------------------
 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
 -- Split the type of a dictionary function
 tcSplitDFunTy ty 
-  = case tcSplitSigmaTy ty       of { (tvs, theta, tau) ->
-    case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) -> 
+  = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
+    case tcSplitDFunHead tau of { (clas, tys) -> 
     (tvs, theta, clas, tys) }}
+
+tcSplitDFunHead :: Type -> (Class, [Type])
+tcSplitDFunHead tau  
+  = case tcSplitPredTy_maybe tau of 
+       Just (ClassP clas tys) -> (clas, tys)
+
+tcValidInstHeadTy :: 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
+  = case ty of
+       NoteTy _ ty     -> tcValidInstHeadTy ty
+       TyConApp tc tys -> not (isSynTyCon tc) && ok tys
+       FunTy arg res   -> ok [arg, res]
+       other           -> False
+  where
+       -- Check that all the types are type variables,
+       -- and that each is distinct
+    ok tys = equalLength tvs tys && hasNoDups tvs
+          where
+            tvs = mapCatMaybes get_tv tys
+
+    get_tv (NoteTy _ ty) = get_tv ty   -- through synonyms
+    get_tv (TyVarTy tv)  = Just tv     -- Again, do not look
+    get_tv other        = Nothing
 \end{code}
 
 
@@ -518,7 +775,7 @@ tcSplitDFunTy ty
 \begin{code}
 tcSplitPredTy_maybe :: Type -> Maybe PredType
    -- Returns Just for predicates only
-tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
+tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
 tcSplitPredTy_maybe (PredTy p)    = Just p
 tcSplitPredTy_maybe other        = Nothing
        
@@ -555,8 +812,8 @@ 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 (NoteTy _ ty) = isDictTy ty
 isDictTy other         = False
 \end{code}
 
@@ -584,100 +841,25 @@ isLinearPred (IParam (Linear n) _) = True
 isLinearPred other                = False
 \end{code}
 
-
-%************************************************************************
-%*                                                                     *
-\subsection{Comparison}
-%*                                                                     *
-%************************************************************************
-
-Comparison, taking note of newtypes, predicates, etc,
-
-\begin{code}
-tcEqType :: Type -> Type -> Bool
-tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
-
-tcEqTypes :: [Type] -> [Type] -> Bool
-tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
-
-tcEqPred :: PredType -> PredType -> Bool
-tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
-
--------------
-tcCmpType :: Type -> Type -> Ordering
-tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
-
-tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
-
-tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2
--------------
-cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
-
--------------
-cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
-  -- The "env" maps type variables in ty1 to type variables in ty2
-  -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
-  -- we in effect substitute tv2 for tv1 in t1 before continuing
-
-    -- Look through NoteTy
-cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
-cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
-
-    -- Deal with equal constructors
-cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
-                                         Just tv1a -> tv1a `compare` tv2
-                                         Nothing   -> tv1  `compare` tv2
-
-cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
-cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
-cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
-cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
-cmpTy env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
-cmpTy env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTy (extendVarEnv env tv1 tv2) t1 t2
-    
-    -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < NewTcApp < ForAllTy < PredTy
-cmpTy env (AppTy _ _) (TyVarTy _) = GT
-    
-cmpTy env (FunTy _ _) (TyVarTy _) = GT
-cmpTy env (FunTy _ _) (AppTy _ _) = GT
-    
-cmpTy env (TyConApp _ _) (TyVarTy _) = GT
-cmpTy env (TyConApp _ _) (AppTy _ _) = GT
-cmpTy env (TyConApp _ _) (FunTy _ _) = GT
-    
-cmpTy env (NewTcApp _ _) (TyVarTy _)   = GT
-cmpTy env (NewTcApp _ _) (AppTy _ _)   = GT
-cmpTy env (NewTcApp _ _) (FunTy _ _)   = GT
-cmpTy env (NewTcApp _ _) (TyConApp _ _) = GT
-    
-cmpTy env (ForAllTy _ _) (TyVarTy _)    = GT
-cmpTy env (ForAllTy _ _) (AppTy _ _)    = GT
-cmpTy env (ForAllTy _ _) (FunTy _ _)    = GT
-cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
-cmpTy env (ForAllTy _ _) (NewTcApp _ _) = GT
-
-cmpTy env (PredTy _)   t2              = GT
-
-cmpTy env _ _ = LT
-\end{code}
-
-\begin{code}
-cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
-cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
-       -- Compare types as well as names for implicit parameters
-       -- This comparison is used exclusively (I think) for the
-       -- finite map built in TcSimplify
-cmpPredTy env (IParam _ _)     (ClassP _ _)      = LT
-cmpPredTy env (ClassP _ _)     (IParam _ _)     = GT
-cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
-\end{code}
-
-PredTypes are used as a FM key in TcSimplify, 
-so we take the easy path and make them an instance of Ord
+--------------------- The stupid theta (sigh) ---------------------------------
 
 \begin{code}
-instance Eq  PredType where { (==)    = tcEqPred }
-instance Ord PredType where { compare = tcCmpPred }
+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 ]
 \end{code}
 
 
@@ -693,20 +875,20 @@ 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 (NoteTy n ty)              = isSigmaTy ty
 isSigmaTy _                  = False
 
 isOverloadedTy :: Type -> Bool
+isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 isOverloadedTy (FunTy a b)        = isPredTy a
-isOverloadedTy (NoteTy n ty)      = isOverloadedTy ty
 isOverloadedTy _                  = False
 
 isPredTy :: Type -> Bool       -- Belongs in TcType because it does 
                                -- not look through newtypes, or predtypes (of course)
-isPredTy (NoteTy _ ty) = isPredTy ty
+isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
 isPredTy (PredTy sty)  = True
 isPredTy _            = False
 \end{code}
@@ -736,19 +918,71 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 
 \begin{code}
 deNoteType :: Type -> Type
-       -- Remove synonyms, but not predicate types
-deNoteType ty@(TyVarTy tyvar)  = ty
-deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
-deNoteType (NewTcApp tycon tys) = NewTcApp tycon (map deNoteType tys)
-deNoteType (PredTy p)          = PredTy (deNotePredType p)
-deNoteType (NoteTy _ ty)       = deNoteType ty
-deNoteType (AppTy fun arg)     = AppTy (deNoteType fun) (deNoteType arg)
-deNoteType (FunTy fun arg)     = FunTy (deNoteType fun) (deNoteType arg)
-deNoteType (ForAllTy tv ty)    = ForAllTy tv (deNoteType ty)
-
-deNotePredType :: PredType -> PredType
-deNotePredType (ClassP c tys)   = ClassP c (map deNoteType tys)
-deNotePredType (IParam n ty)    = IParam n (deNoteType ty)
+-- Remove all *outermost* type synonyms and other notes
+deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
+deNoteType ty = ty
+\end{code}
+
+\begin{code}
+tcTyVarsOfType :: Type -> TcTyVarSet
+-- Just the tc type variables free in the type
+tcTyVarsOfType (TyVarTy tv)        = if isTcTyVar tv then unitVarSet tv
+                                                     else emptyVarSet
+tcTyVarsOfType (TyConApp tycon tys) = tcTyVarsOfTypes tys
+tcTyVarsOfType (NoteTy _ ty)       = tcTyVarsOfType ty
+tcTyVarsOfType (PredTy sty)        = tcTyVarsOfPred sty
+tcTyVarsOfType (FunTy arg res)     = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
+tcTyVarsOfType (AppTy fun arg)     = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
+tcTyVarsOfType (ForAllTy tyvar ty)  = tcTyVarsOfType ty `delVarSet` tyvar
+       -- We do sometimes quantify over skolem TcTyVars
+
+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
 \end{code}
 
 Find the free tycons and classes of a type.  This is used in the front
@@ -758,11 +992,9 @@ end of the compiler.
 tyClsNamesOfType :: Type -> NameSet
 tyClsNamesOfType (TyVarTy tv)              = emptyNameSet
 tyClsNamesOfType (TyConApp tycon tys)      = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
-tyClsNamesOfType (NewTcApp tycon tys)      = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
-tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
-tyClsNamesOfType (NoteTy other_note    ty2) = tyClsNamesOfType ty2
-tyClsNamesOfType (PredTy (IParam n ty))   = tyClsNamesOfType ty
-tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (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
@@ -968,5 +1200,3 @@ isByteArrayLikeTyCon :: TyCon -> Bool
 isByteArrayLikeTyCon tc = 
   getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
 \end{code}
-
-