compiler/typecheck/TcType.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5 \section[TcType]{Types used in the typechecker}
   6
   7 This module provides the Type interface for front-end parts of the
   8 compiler.  These parts
   9
  10         * treat "source types" as opaque:
  11                 newtypes, and predicates are meaningful.
  12         * look through usage types
  13
  14 The "tc" prefix is for "TypeChecker", because the type checker
  15 is the principal client.
  16
  17 \begin{code}
  18 module TcType (
  19   --------------------------------
  20   -- Types
  21   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
  22   TcTyVar, TcTyVarSet, TcKind,
  23
  24   BoxyTyVar, BoxySigmaType, BoxyRhoType, BoxyThetaType, BoxyType,
  25
  26   --------------------------------
  27   -- MetaDetails
  28   UserTypeCtxt(..), pprUserTypeCtxt,
  29   TcTyVarDetails(..), BoxInfo(..), pprTcTyVarDetails,
  30   MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
  31   isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar,
  32   isSigTyVar, isExistentialTyVar,  isTyConableTyVar,
  33   metaTvRef,
  34   isFlexi, isIndirect, isRuntimeUnk, isUnk,
  35
  36   --------------------------------
  37   -- Builders
  38   mkPhiTy, mkSigmaTy,
  39
  40   --------------------------------
  41   -- Splitters
  42   -- These are important because they do not look through newtypes
  43   tcView,
  44   tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
  45   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
  46   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
  47   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
  48   tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
  49   tcGetTyVar_maybe, tcGetTyVar,
  50   tcSplitSigmaTy, tcMultiSplitSigmaTy,
  51
  52   ---------------------------------
  53   -- Predicates.
  54   -- Again, newtypes are opaque
  55   tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
  56   eqKind,
  57   isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
  58   isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
  59   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
  60   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
  61   isOpenSynTyConApp,
  62
  63   ---------------------------------
  64   -- Misc type manipulators
  65   deNoteType,
  66   tyClsNamesOfType, tyClsNamesOfDFunHead,
  67   getDFunTyKey,
  68
  69   ---------------------------------
  70   -- Predicate types
  71   getClassPredTys_maybe, getClassPredTys,
  72   isClassPred, isTyVarClassPred, isEqPred,
  73   mkDictTy, tcSplitPredTy_maybe,
  74   isPredTy, isDictTy, isDictLikeTy,
  75   tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
  76   mkClassPred, isInheritablePred, isIPPred,
  77   isRefineableTy, isRefineablePred,
  78
  79   ---------------------------------
  80   -- Foreign import and export
  81   isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
  82   isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
  83   isFFIExportResultTy, -- :: Type -> Bool
  84   isFFIExternalTy,     -- :: Type -> Bool
  85   isFFIDynArgumentTy,  -- :: Type -> Bool
  86   isFFIDynResultTy,    -- :: Type -> Bool
  87   isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
  88   isFFIPrimResultTy,   -- :: DynFlags -> Type -> Bool
  89   isFFILabelTy,        -- :: Type -> Bool
  90   isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
  91   isFFIDotnetObjTy,    -- :: Type -> Bool
  92   isFFITy,             -- :: Type -> Bool
  93   isFunPtrTy,          -- :: Type -> Bool
  94   tcSplitIOType_maybe, -- :: Type -> Maybe Type
  95   toDNType,            -- :: Type -> DNType
  96
  97   --------------------------------
  98   -- Rexported from Type
  99   Kind,         -- Stuff to do with kinds is insensitive to pre/post Tc
 100   unliftedTypeKind, liftedTypeKind, argTypeKind,
 101   openTypeKind, mkArrowKind, mkArrowKinds,
 102   isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind,
 103   isSubArgTypeKind, isSubKind, splitKindFunTys, defaultKind,
 104   kindVarRef, mkKindVar,
 105
 106   Type, PredType(..), ThetaType,
 107   mkForAllTy, mkForAllTys,
 108   mkFunTy, mkFunTys, zipFunTys,
 109   mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
 110   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
 111
 112   -- Type substitutions
 113   TvSubst(..),  -- Representation visible to a few friends
 114   TvSubstEnv, emptyTvSubst, substEqSpec,
 115   mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
 116   getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
 117   extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
 118   substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars, substTyVarBndr,
 119
 120   isUnLiftedType,       -- Source types are always lifted
 121   isUnboxedTupleType,   -- Ditto
 122   isPrimitiveType,
 123
 124   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 125   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
 126   typeKind, tidyKind,
 127
 128   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
 129   tcTyVarsOfType, tcTyVarsOfTypes, tcTyVarsOfPred, exactTyVarsOfType,
 130   exactTyVarsOfTypes,
 131
 132   pprKind, pprParendKind,
 133   pprType, pprParendType, pprTypeApp, pprTyThingCategory,
 134   pprPred, pprTheta, pprThetaArrow, pprClassPred
 135
 136   ) where
 137
 138 #include "HsVersions.h"
 139
 140 -- friends:
 141 import TypeRep
 142 import DataCon
 143 import Class
 144 import Var
 145 import ForeignCall
 146 import VarSet
 147 import Type
 148 import Coercion
 149 import TyCon
 150
 151 -- others:
 152 import DynFlags
 153 import Name
 154 import NameSet
 155 import VarEnv
 156 import OccName
 157 import PrelNames
 158 import TysWiredIn
 159 import BasicTypes
 160 import Util
 161 import Maybes
 162 import ListSetOps
 163 import Outputable
 164 import FastString
 165
 166 import Data.List
 167 import Data.IORef
 168 \end{code}
 169
 170 %************************************************************************
 171 %*                                                                      *
 172 \subsection{Types}
 173 %*                                                                      *
 174 %************************************************************************
 175
 176 The type checker divides the generic Type world into the
 177 following more structured beasts:
 178
 179 sigma ::= forall tyvars. phi
 180         -- A sigma type is a qualified type
 181         --
 182         -- Note that even if 'tyvars' is empty, theta
 183         -- may not be: e.g.   (?x::Int) => Int
 184
 185         -- Note that 'sigma' is in prenex form:
 186         -- all the foralls are at the front.
 187         -- A 'phi' type has no foralls to the right of
 188         -- an arrow
 189
 190 phi :: theta => rho
 191
 192 rho ::= sigma -> rho
 193      |  tau
 194
 195 -- A 'tau' type has no quantification anywhere
 196 -- Note that the args of a type constructor must be taus
 197 tau ::= tyvar
 198      |  tycon tau_1 .. tau_n
 199      |  tau_1 tau_2
 200      |  tau_1 -> tau_2
 201
 202 -- In all cases, a (saturated) type synonym application is legal,
 203 -- provided it expands to the required form.
 204
 205 \begin{code}
 206 type TcTyVar = TyVar    -- Used only during type inference
 207 type TcType = Type      -- A TcType can have mutable type variables
 208         -- Invariant on ForAllTy in TcTypes:
 209         --      forall a. T
 210         -- a cannot occur inside a MutTyVar in T; that is,
 211         -- T is "flattened" before quantifying over a
 212
 213 -- These types do not have boxy type variables in them
 214 type TcPredType     = PredType
 215 type TcThetaType    = ThetaType
 216 type TcSigmaType    = TcType
 217 type TcRhoType      = TcType
 218 type TcTauType      = TcType
 219 type TcKind         = Kind
 220 type TcTyVarSet     = TyVarSet
 221
 222 -- These types may have boxy type variables in them
 223 type BoxyTyVar      = TcTyVar
 224 type BoxyRhoType    = TcType
 225 type BoxyThetaType  = TcThetaType
 226 type BoxySigmaType  = TcType
 227 type BoxyType       = TcType
 228 \end{code}
 229
 230
 231 %************************************************************************
 232 %*                                                                      *
 233 \subsection{TyVarDetails}
 234 %*                                                                      *
 235 %************************************************************************
 236
 237 TyVarDetails gives extra info about type variables, used during type
 238 checking.  It's attached to mutable type variables only.
 239 It's knot-tied back to Var.lhs.  There is no reason in principle
 240 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 241
 242
 243 Note [Signature skolems]
 244 ~~~~~~~~~~~~~~~~~~~~~~~~
 245 Consider this
 246
 247   x :: [a]
 248   y :: b
 249   (x,y,z) = ([y,z], z, head x)
 250
 251 Here, x and y have type sigs, which go into the environment.  We used to
 252 instantiate their types with skolem constants, and push those types into
 253 the RHS, so we'd typecheck the RHS with type
 254         ( [a*], b*, c )
 255 where a*, b* are skolem constants, and c is an ordinary meta type varible.
 256
 257 The trouble is that the occurrences of z in the RHS force a* and b* to
 258 be the *same*, so we can't make them into skolem constants that don't unify
 259 with each other.  Alas.
 260
 261 One solution would be insist that in the above defn the programmer uses
 262 the same type variable in both type signatures.  But that takes explanation.
 263
 264 The alternative (currently implemented) is to have a special kind of skolem
 265 constant, SigTv, which can unify with other SigTvs.  These are *not* treated
 266 as righd for the purposes of GADTs.  And they are used *only* for pattern
 267 bindings and mutually recursive function bindings.  See the function
 268 TcBinds.tcInstSig, and its use_skols parameter.
 269
 270
 271 \begin{code}
 272 -- A TyVarDetails is inside a TyVar
 273 data TcTyVarDetails
 274   = SkolemTv SkolemInfo                 -- A skolem constant
 275
 276   | MetaTv BoxInfo (IORef MetaDetails)
 277
 278 data BoxInfo
 279    = BoxTv      -- The contents is a (non-boxy) sigma-type
 280                 -- That is, this MetaTv is a "box"
 281
 282    | TauTv      -- The contents is a (non-boxy) tau-type
 283                 -- That is, this MetaTv is an ordinary unification variable
 284
 285    | SigTv SkolemInfo   -- A variant of TauTv, except that it should not be
 286                         -- unified with a type, only with a type variable
 287                         -- SigTvs are only distinguished to improve error messages
 288                         --      see Note [Signature skolems]
 289                         --      The MetaDetails, if filled in, will
 290                         --      always be another SigTv or a SkolemTv
 291
 292 -- INVARIANTS:
 293 --      A TauTv is always filled in with a tau-type, which
 294 --      never contains any BoxTvs, nor any ForAlls
 295 --
 296 --      However, a BoxTv can contain a type that contains further BoxTvs
 297 --      Notably, when typechecking an explicit list, say [e1,e2], with
 298 --      expected type being a box b1, we fill in b1 with (List b2), where
 299 --      b2 is another (currently empty) box.
 300
 301 data MetaDetails
 302   = Flexi               -- Flexi type variables unify to become
 303                         -- Indirects.
 304
 305   | Indirect TcType     -- INVARIANT:
 306                         --   For a BoxTv, this type must be non-boxy
 307                         --   For a TauTv, this type must be a tau-type
 308
 309 -- Generally speaking, SkolemInfo should not contain location info
 310 -- that is contained in the Name of the tyvar with this SkolemInfo
 311 data SkolemInfo
 312   = SigSkol UserTypeCtxt        -- A skolem that is created by instantiating
 313                                 -- a programmer-supplied type signature
 314                                 -- Location of the binding site is on the TyVar
 315
 316         -- The rest are for non-scoped skolems
 317   | ClsSkol Class       -- Bound at a class decl
 318   | InstSkol            -- Bound at an instance decl
 319   | FamInstSkol         -- Bound at a family instance decl
 320   | PatSkol DataCon     -- An existential type variable bound by a pattern for
 321                         -- a data constructor with an existential type. E.g.
 322                         --      data T = forall a. Eq a => MkT a
 323                         --      f (MkT x) = ...
 324                         -- The pattern MkT x will allocate an existential type
 325                         -- variable for 'a'.
 326   | ArrowSkol           -- An arrow form (see TcArrows)
 327
 328   | RuleSkol RuleName   -- The LHS of a RULE
 329   | GenSkol [TcTyVar]   -- Bound when doing a subsumption check for
 330             TcType      --      (forall tvs. ty)
 331
 332   | RuntimeUnkSkol      -- a type variable used to represent an unknown
 333                         -- runtime type (used in the GHCi debugger)
 334
 335   | UnkSkol             -- Unhelpful info (until I improve it)
 336
 337 -------------------------------------
 338 -- UserTypeCtxt describes the places where a
 339 -- programmer-written type signature can occur
 340 -- Like SkolemInfo, no location info
 341 data UserTypeCtxt
 342   = FunSigCtxt Name     -- Function type signature
 343                         -- Also used for types in SPECIALISE pragmas
 344   | ExprSigCtxt         -- Expression type signature
 345   | ConArgCtxt Name     -- Data constructor argument
 346   | TySynCtxt Name      -- RHS of a type synonym decl
 347   | GenPatCtxt          -- Pattern in generic decl
 348                         --      f{| a+b |} (Inl x) = ...
 349   | LamPatSigCtxt               -- Type sig in lambda pattern
 350                         --      f (x::t) = ...
 351   | BindPatSigCtxt      -- Type sig in pattern binding pattern
 352                         --      (x::t, y) = e
 353   | ResSigCtxt          -- Result type sig
 354                         --      f x :: t = ....
 355   | ForSigCtxt Name     -- Foreign inport or export signature
 356   | DefaultDeclCtxt     -- Types in a default declaration
 357   | SpecInstCtxt        -- SPECIALISE instance pragma
 358   | ThBrackCtxt         -- Template Haskell type brackets [t| ... |]
 359
 360 -- Notes re TySynCtxt
 361 -- We allow type synonyms that aren't types; e.g.  type List = []
 362 --
 363 -- If the RHS mentions tyvars that aren't in scope, we'll
 364 -- quantify over them:
 365 --      e.g.    type T = a->a
 366 -- will become  type T = forall a. a->a
 367 --
 368 -- With gla-exts that's right, but for H98 we should complain.
 369
 370 ---------------------------------
 371 -- Kind variables:
 372
 373 mkKindName :: Unique -> Name
 374 mkKindName unique = mkSystemName unique kind_var_occ
 375
 376 kindVarRef :: KindVar -> IORef MetaDetails
 377 kindVarRef tc =
 378   ASSERT ( isTcTyVar tc )
 379   case tcTyVarDetails tc of
 380     MetaTv TauTv ref -> ref
 381     _                -> pprPanic "kindVarRef" (ppr tc)
 382
 383 mkKindVar :: Unique -> IORef MetaDetails -> KindVar
 384 mkKindVar u r
 385   = mkTcTyVar (mkKindName u)
 386               tySuperKind  -- not sure this is right,
 387                             -- do we need kind vars for
 388                             -- coercions?
 389               (MetaTv TauTv r)
 390
 391 kind_var_occ :: OccName -- Just one for all KindVars
 392                         -- They may be jiggled by tidying
 393 kind_var_occ = mkOccName tvName "k"
 394 \end{code}
 395
 396 %************************************************************************
 397 %*                                                                      *
 398                 Pretty-printing
 399 %*                                                                      *
 400 %************************************************************************
 401
 402 \begin{code}
 403 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 404 -- For debugging
 405 pprTcTyVarDetails (SkolemTv _)         = ptext (sLit "sk")
 406 pprTcTyVarDetails (MetaTv BoxTv _)     = ptext (sLit "box")
 407 pprTcTyVarDetails (MetaTv TauTv _)     = ptext (sLit "tau")
 408 pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext (sLit "sig")
 409
 410 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
 411 pprUserTypeCtxt (FunSigCtxt n)  = ptext (sLit "the type signature for") <+> quotes (ppr n)
 412 pprUserTypeCtxt ExprSigCtxt     = ptext (sLit "an expression type signature")
 413 pprUserTypeCtxt (ConArgCtxt c)  = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
 414 pprUserTypeCtxt (TySynCtxt c)   = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
 415 pprUserTypeCtxt GenPatCtxt      = ptext (sLit "the type pattern of a generic definition")
 416 pprUserTypeCtxt ThBrackCtxt     = ptext (sLit "a Template Haskell quotation [t|...|]")
 417 pprUserTypeCtxt LamPatSigCtxt   = ptext (sLit "a pattern type signature")
 418 pprUserTypeCtxt BindPatSigCtxt  = ptext (sLit "a pattern type signature")
 419 pprUserTypeCtxt ResSigCtxt      = ptext (sLit "a result type signature")
 420 pprUserTypeCtxt (ForSigCtxt n)  = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
 421 pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration")
 422 pprUserTypeCtxt SpecInstCtxt    = ptext (sLit "a SPECIALISE instance pragma")
 423
 424
 425 --------------------------------
 426 tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
 427 -- Tidy the type inside a GenSkol, preparatory to printing it
 428 tidySkolemTyVar env tv
 429   = ASSERT( isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv ) )
 430     (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
 431   where
 432     (env1, info1) = case tcTyVarDetails tv of
 433                         SkolemTv info -> (env1, SkolemTv info')
 434                                 where
 435                                   (env1, info') = tidy_skol_info env info
 436                         MetaTv (SigTv info) box -> (env1, MetaTv (SigTv info') box)
 437                                 where
 438                                   (env1, info') = tidy_skol_info env info
 439                         info -> (env, info)
 440
 441     tidy_skol_info env (GenSkol tvs ty) = (env2, GenSkol tvs1 ty1)
 442                             where
 443                               (env1, tvs1) = tidyOpenTyVars env tvs
 444                               (env2, ty1)  = tidyOpenType env1 ty
 445     tidy_skol_info env info = (env, info)
 446
 447 pprSkolTvBinding :: TcTyVar -> SDoc
 448 -- Print info about the binding of a skolem tyvar,
 449 -- or nothing if we don't have anything useful to say
 450 pprSkolTvBinding tv
 451   = ASSERT ( isTcTyVar tv )
 452     quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
 453   where
 454     ppr_details (MetaTv TauTv _)        = ptext (sLit "is a meta type variable")
 455     ppr_details (MetaTv BoxTv _)        = ptext (sLit "is a boxy type variable")
 456     ppr_details (MetaTv (SigTv info) _) = ppr_skol info
 457     ppr_details (SkolemTv info)         = ppr_skol info
 458
 459     ppr_skol UnkSkol        = ptext (sLit "is an unknown type variable")        -- Unhelpful
 460     ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type")
 461     ppr_skol info           = sep [ptext (sLit "is a rigid type variable bound by"),
 462                                    sep [pprSkolInfo info,
 463                                          nest 2 (ptext (sLit "at") <+> ppr (getSrcLoc tv))]]
 464
 465 pprSkolInfo :: SkolemInfo -> SDoc
 466 pprSkolInfo (SigSkol ctxt)   = pprUserTypeCtxt ctxt
 467 pprSkolInfo (ClsSkol cls)    = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
 468 pprSkolInfo InstSkol         = ptext (sLit "the instance declaration")
 469 pprSkolInfo FamInstSkol      = ptext (sLit "the family instance declaration")
 470 pprSkolInfo (RuleSkol name)  = ptext (sLit "the RULE") <+> doubleQuotes (ftext name)
 471 pprSkolInfo ArrowSkol        = ptext (sLit "the arrow form")
 472 pprSkolInfo (PatSkol dc)     = sep [ptext (sLit "the constructor") <+> quotes (ppr dc)]
 473 pprSkolInfo (GenSkol tvs ty) = sep [ptext (sLit "the polymorphic type"),
 474                                     nest 2 (quotes (ppr (mkForAllTys tvs ty)))]
 475
 476 -- UnkSkol
 477 -- For type variables the others are dealt with by pprSkolTvBinding.
 478 -- For Insts, these cases should not happen
 479 pprSkolInfo UnkSkol = panic "UnkSkol"
 480 pprSkolInfo RuntimeUnkSkol = panic "RuntimeUnkSkol"
 481
 482 instance Outputable MetaDetails where
 483   ppr Flexi         = ptext (sLit "Flexi")
 484   ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
 485 \end{code}
 486
 487
 488 %************************************************************************
 489 %*                                                                      *
 490                 Predicates
 491 %*                                                                      *
 492 %************************************************************************
 493
 494 \begin{code}
 495 isImmutableTyVar :: TyVar -> Bool
 496
 497 isImmutableTyVar tv
 498   | isTcTyVar tv = isSkolemTyVar tv
 499   | otherwise    = True
 500
 501 isTyConableTyVar, isSkolemTyVar, isExistentialTyVar,
 502   isBoxyTyVar, isMetaTyVar :: TcTyVar -> Bool
 503
 504 isTyConableTyVar tv
 505         -- True of a meta-type variable that can be filled in
 506         -- with a type constructor application; in particular,
 507         -- not a SigTv
 508   = ASSERT( isTcTyVar tv)
 509     case tcTyVarDetails tv of
 510         MetaTv BoxTv      _ -> True
 511         MetaTv TauTv      _ -> True
 512         MetaTv (SigTv {}) _ -> False
 513         SkolemTv {}         -> False
 514
 515 isSkolemTyVar tv
 516   = ASSERT2( isTcTyVar tv, ppr tv )
 517     case tcTyVarDetails tv of
 518         SkolemTv _         -> True
 519         MetaTv _ _         -> False
 520
 521 isExistentialTyVar tv   -- Existential type variable, bound by a pattern
 522   = ASSERT( isTcTyVar tv )
 523     case tcTyVarDetails tv of
 524         SkolemTv (PatSkol {}) -> True
 525         _                     -> False
 526
 527 isMetaTyVar tv
 528   = ASSERT2( isTcTyVar tv, ppr tv )
 529     case tcTyVarDetails tv of
 530         MetaTv _ _ -> True
 531         _          -> False
 532
 533 isBoxyTyVar tv
 534   = ASSERT( isTcTyVar tv )
 535     case tcTyVarDetails tv of
 536         MetaTv BoxTv _ -> True
 537         _              -> False
 538
 539 isSigTyVar :: Var -> Bool
 540 isSigTyVar tv
 541   = ASSERT( isTcTyVar tv )
 542     case tcTyVarDetails tv of
 543         MetaTv (SigTv _) _ -> True
 544         _                  -> False
 545
 546 metaTvRef :: TyVar -> IORef MetaDetails
 547 metaTvRef tv
 548   = ASSERT2( isTcTyVar tv, ppr tv )
 549     case tcTyVarDetails tv of
 550         MetaTv _ ref -> ref
 551         _          -> pprPanic "metaTvRef" (ppr tv)
 552
 553 isFlexi, isIndirect :: MetaDetails -> Bool
 554 isFlexi Flexi = True
 555 isFlexi _     = False
 556
 557 isIndirect (Indirect _) = True
 558 isIndirect _            = False
 559
 560 isRuntimeUnk :: TyVar -> Bool
 561 isRuntimeUnk x | isTcTyVar x
 562                , SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
 563                | otherwise = False
 564
 565 isUnk :: TyVar -> Bool
 566 isUnk x | isTcTyVar x
 567         , SkolemTv UnkSkol <- tcTyVarDetails x = True
 568         | otherwise = False
 569 \end{code}
 570
 571
 572 %************************************************************************
 573 %*                                                                      *
 574 \subsection{Tau, sigma and rho}
 575 %*                                                                      *
 576 %************************************************************************
 577
 578 \begin{code}
 579 mkSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
 580 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
 581
 582 mkPhiTy :: [PredType] -> Type -> Type
 583 mkPhiTy theta ty = foldr (\p r -> mkFunTy (mkPredTy p) r) ty theta
 584 \end{code}
 585
 586 @isTauTy@ tests for nested for-alls.  It should not be called on a boxy type.
 587
 588 \begin{code}
 589 isTauTy :: Type -> Bool
 590 isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
 591 isTauTy (TyVarTy tv)     = ASSERT( not (isTcTyVar tv && isBoxyTyVar tv) )
 592                            True
 593 isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
 594 isTauTy (AppTy a b)       = isTauTy a && isTauTy b
 595 isTauTy (FunTy a b)       = isTauTy a && isTauTy b
 596 isTauTy (PredTy _)        = True                -- Don't look through source types
 597 isTauTy _                 = False
 598
 599
 600 isTauTyCon :: TyCon -> Bool
 601 -- Returns False for type synonyms whose expansion is a polytype
 602 isTauTyCon tc
 603   | isClosedSynTyCon tc = isTauTy (snd (synTyConDefn tc))
 604   | otherwise           = True
 605
 606 ---------------
 607 isBoxyTy :: TcType -> Bool
 608 isBoxyTy ty = any isBoxyTyVar (varSetElems (tcTyVarsOfType ty))
 609
 610 isRigidTy :: TcType -> Bool
 611 -- A type is rigid if it has no meta type variables in it
 612 isRigidTy ty = all isImmutableTyVar (varSetElems (tcTyVarsOfType ty))
 613
 614 isRefineableTy :: TcType -> (Bool,Bool)
 615 -- A type should have type refinements applied to it if it has
 616 -- free type variables, and they are all rigid
 617 isRefineableTy ty = (null tc_tvs,  all isImmutableTyVar tc_tvs)
 618                     where
 619                       tc_tvs = varSetElems (tcTyVarsOfType ty)
 620
 621 isRefineablePred :: TcPredType -> Bool
 622 isRefineablePred pred = not (null tc_tvs) && all isImmutableTyVar tc_tvs
 623                       where
 624                         tc_tvs = varSetElems (tcTyVarsOfPred pred)
 625
 626 ---------------
 627 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
 628                                 -- construct a dictionary function name
 629 getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
 630 getDFunTyKey (TyVarTy tv)    = getOccName tv
 631 getDFunTyKey (TyConApp tc _) = getOccName tc
 632 getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
 633 getDFunTyKey (FunTy _ _)     = getOccName funTyCon
 634 getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
 635 getDFunTyKey ty              = pprPanic "getDFunTyKey" (pprType ty)
 636 -- PredTy shouldn't happen
 637 \end{code}
 638
 639
 640 %************************************************************************
 641 %*                                                                      *
 642 \subsection{Expanding and splitting}
 643 %*                                                                      *
 644 %************************************************************************
 645
 646 These tcSplit functions are like their non-Tc analogues, but
 647         a) they do not look through newtypes
 648         b) they do not look through PredTys
 649         c) [future] they ignore usage-type annotations
 650
 651 However, they are non-monadic and do not follow through mutable type
 652 variables.  It's up to you to make sure this doesn't matter.
 653
 654 \begin{code}
 655 tcSplitForAllTys :: Type -> ([TyVar], Type)
 656 tcSplitForAllTys ty = split ty ty []
 657    where
 658      split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
 659      split _ (ForAllTy tv ty) tvs
 660        | not (isCoVar tv) = split ty ty (tv:tvs)
 661      split orig_ty _ tvs = (reverse tvs, orig_ty)
 662
 663 tcIsForAllTy :: Type -> Bool
 664 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
 665 tcIsForAllTy (ForAllTy tv _) = not (isCoVar tv)
 666 tcIsForAllTy _               = False
 667
 668 tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
 669 -- Split off the first predicate argument from a type
 670 tcSplitPredFunTy_maybe ty | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
 671 tcSplitPredFunTy_maybe (ForAllTy tv ty)
 672   | isCoVar tv = Just (coVarPred tv, ty)
 673 tcSplitPredFunTy_maybe (FunTy arg res)
 674   | Just p <- tcSplitPredTy_maybe arg = Just (p, res)
 675 tcSplitPredFunTy_maybe _
 676   = Nothing
 677
 678 tcSplitPhiTy :: Type -> (ThetaType, Type)
 679 tcSplitPhiTy ty
 680   = split ty []
 681   where
 682     split ty ts
 683       = case tcSplitPredFunTy_maybe ty of
 684           Just (pred, ty) -> split ty (pred:ts)
 685           Nothing         -> (reverse ts, ty)
 686
 687 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
 688 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
 689                         (tvs, rho) -> case tcSplitPhiTy rho of
 690                                         (theta, tau) -> (tvs, theta, tau)
 691
 692 -----------------------
 693 tcMultiSplitSigmaTy
 694         :: TcSigmaType
 695         -> ( [([TyVar], ThetaType)],    -- forall as.C => forall bs.D
 696              TcSigmaType)               -- The rest of the type
 697
 698 -- We need a loop here because we are now prepared to entertain
 699 -- types like
 700 --      f:: forall a. Eq a => forall b. Baz b => tau
 701 -- We want to instantiate this to
 702 --      f2::tau         {f2 = f1 b (Baz b), f1 = f a (Eq a)}
 703
 704 tcMultiSplitSigmaTy sigma
 705   = case (tcSplitSigmaTy sigma) of
 706         ([], [], _) -> ([], sigma)
 707         (tvs, theta, ty) -> case tcMultiSplitSigmaTy ty of
 708                                 (pairs, rest) -> ((tvs,theta):pairs, rest)
 709
 710 -----------------------
 711 tcTyConAppTyCon :: Type -> TyCon
 712 tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
 713                         Just (tc, _) -> tc
 714                         Nothing      -> pprPanic "tcTyConAppTyCon" (pprType ty)
 715
 716 tcTyConAppArgs :: Type -> [Type]
 717 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
 718                         Just (_, args) -> args
 719                         Nothing        -> pprPanic "tcTyConAppArgs" (pprType ty)
 720
 721 tcSplitTyConApp :: Type -> (TyCon, [Type])
 722 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
 723                         Just stuff -> stuff
 724                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 725
 726 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 727 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
 728 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 729 tcSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
 730         -- Newtypes are opaque, so they may be split
 731         -- However, predicates are not treated
 732         -- as tycon applications by the type checker
 733 tcSplitTyConApp_maybe _                 = Nothing
 734
 735 -----------------------
 736 tcSplitFunTys :: Type -> ([Type], Type)
 737 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
 738                         Nothing        -> ([], ty)
 739                         Just (arg,res) -> (arg:args, res')
 740                                        where
 741                                           (args,res') = tcSplitFunTys res
 742
 743 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
 744 tcSplitFunTy_maybe ty | Just ty' <- tcView ty           = tcSplitFunTy_maybe ty'
 745 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
 746 tcSplitFunTy_maybe _                                    = Nothing
 747         -- Note the (not (isPredTy arg)) guard
 748         -- Consider     (?x::Int) => Bool
 749         -- We don't want to treat this as a function type!
 750         -- A concrete example is test tc230:
 751         --      f :: () -> (?p :: ()) => () -> ()
 752         --
 753         --      g = f () ()
 754
 755 tcSplitFunTysN
 756         :: TcRhoType
 757         -> Arity                -- N: Number of desired args
 758         -> ([TcSigmaType],      -- Arg types (N or fewer)
 759             TcSigmaType)        -- The rest of the type
 760
 761 tcSplitFunTysN ty n_args
 762   | n_args == 0
 763   = ([], ty)
 764   | Just (arg,res) <- tcSplitFunTy_maybe ty
 765   = case tcSplitFunTysN res (n_args - 1) of
 766         (args, res) -> (arg:args, res)
 767   | otherwise
 768   = ([], ty)
 769
 770 tcSplitFunTy :: Type -> (Type, Type)
 771 tcSplitFunTy  ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
 772
 773 tcFunArgTy :: Type -> Type
 774 tcFunArgTy    ty = fst (tcSplitFunTy ty)
 775
 776 tcFunResultTy :: Type -> Type
 777 tcFunResultTy ty = snd (tcSplitFunTy ty)
 778
 779 -----------------------
 780 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
 781 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
 782 tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
 783
 784 tcSplitAppTy :: Type -> (Type, Type)
 785 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
 786                     Just stuff -> stuff
 787                     Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
 788
 789 tcSplitAppTys :: Type -> (Type, [Type])
 790 tcSplitAppTys ty
 791   = go ty []
 792   where
 793     go ty args = case tcSplitAppTy_maybe ty of
 794                    Just (ty', arg) -> go ty' (arg:args)
 795                    Nothing         -> (ty,args)
 796
 797 -----------------------
 798 tcGetTyVar_maybe :: Type -> Maybe TyVar
 799 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
 800 tcGetTyVar_maybe (TyVarTy tv)   = Just tv
 801 tcGetTyVar_maybe _              = Nothing
 802
 803 tcGetTyVar :: String -> Type -> TyVar
 804 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 805
 806 tcIsTyVarTy :: Type -> Bool
 807 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 808
 809 -----------------------
 810 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
 811 -- Split the type of a dictionary function
 812 tcSplitDFunTy ty
 813   = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
 814     case tcSplitDFunHead tau of { (clas, tys) ->
 815     (tvs, theta, clas, tys) }}
 816
 817 tcSplitDFunHead :: Type -> (Class, [Type])
 818 tcSplitDFunHead tau
 819   = case tcSplitPredTy_maybe tau of
 820         Just (ClassP clas tys) -> (clas, tys)
 821         _ -> panic "tcSplitDFunHead"
 822
 823 tcInstHeadTyNotSynonym :: Type -> Bool
 824 -- Used in Haskell-98 mode, for the argument types of an instance head
 825 -- These must not be type synonyms, but everywhere else type synonyms
 826 -- are transparent, so we need a special function here
 827 tcInstHeadTyNotSynonym ty
 828   = case ty of
 829         TyConApp tc _ -> not (isSynTyCon tc)
 830         _ -> True
 831
 832 tcInstHeadTyAppAllTyVars :: Type -> Bool
 833 -- Used in Haskell-98 mode, for the argument types of an instance head
 834 -- These must be a constructor applied to type variable arguments
 835 tcInstHeadTyAppAllTyVars ty
 836   = case ty of
 837         TyConApp _ tys  -> ok tys
 838         FunTy arg res   -> ok [arg, res]
 839         _               -> False
 840   where
 841         -- Check that all the types are type variables,
 842         -- and that each is distinct
 843     ok tys = equalLength tvs tys && hasNoDups tvs
 844            where
 845              tvs = mapCatMaybes get_tv tys
 846
 847     get_tv (TyVarTy tv)  = Just tv      -- through synonyms
 848     get_tv _             = Nothing
 849 \end{code}
 850
 851
 852
 853 %************************************************************************
 854 %*                                                                      *
 855 \subsection{Predicate types}
 856 %*                                                                      *
 857 %************************************************************************
 858
 859 \begin{code}
 860 tcSplitPredTy_maybe :: Type -> Maybe PredType
 861    -- Returns Just for predicates only
 862 tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
 863 tcSplitPredTy_maybe (PredTy p)    = Just p
 864 tcSplitPredTy_maybe _             = Nothing
 865
 866 predTyUnique :: PredType -> Unique
 867 predTyUnique (IParam n _)    = getUnique (ipNameName n)
 868 predTyUnique (ClassP clas _) = getUnique clas
 869 predTyUnique (EqPred a b)    = pprPanic "predTyUnique" (ppr (EqPred a b))
 870 \end{code}
 871
 872
 873 --------------------- Dictionary types ---------------------------------
 874
 875 \begin{code}
 876 mkClassPred :: Class -> [Type] -> PredType
 877 mkClassPred clas tys = ClassP clas tys
 878
 879 isClassPred :: PredType -> Bool
 880 isClassPred (ClassP _ _) = True
 881 isClassPred _            = False
 882
 883 isTyVarClassPred :: PredType -> Bool
 884 isTyVarClassPred (ClassP _ tys) = all tcIsTyVarTy tys
 885 isTyVarClassPred _              = False
 886
 887 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
 888 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
 889 getClassPredTys_maybe _                 = Nothing
 890
 891 getClassPredTys :: PredType -> (Class, [Type])
 892 getClassPredTys (ClassP clas tys) = (clas, tys)
 893 getClassPredTys _ = panic "getClassPredTys"
 894
 895 mkDictTy :: Class -> [Type] -> Type
 896 mkDictTy clas tys = mkPredTy (ClassP clas tys)
 897
 898 isDictTy :: Type -> Bool
 899 isDictTy ty | Just ty' <- tcView ty = isDictTy ty'
 900 isDictTy (PredTy p) = isClassPred p
 901 isDictTy _          = False
 902
 903 isDictLikeTy :: Type -> Bool
 904 -- Note [Dictionary-like types]
 905 isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
 906 isDictLikeTy (PredTy p) = isClassPred p
 907 isDictLikeTy (TyConApp tc tys)
 908   | isTupleTyCon tc     = all isDictLikeTy tys
 909 isDictLikeTy _          = False
 910 \end{code}
 911
 912 Note [Dictionary-like types]
 913 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 914 Being "dictionary-like" means either a dictionary type or a tuple thereof.
 915 In GHC 6.10 we build implication constraints which construct such tuples,
 916 and if we land up with a binding
 917     t :: (C [a], Eq [a])
 918     t = blah
 919 then we want to treat t as cheap under "-fdicts-cheap" for example.
 920 (Implication constraints are normally inlined, but sadly not if the
 921 occurrence is itself inside an INLINE function!  Until we revise the
 922 handling of implication constraints, that is.)  This turned out to
 923 be important in getting good arities in DPH code.  Example:
 924
 925     class C a
 926     class D a where { foo :: a -> a }
 927     instance C a => D (Maybe a) where { foo x = x }
 928
 929     bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
 930     {-# INLINE bar #-}
 931     bar x y = (foo (Just x), foo (Just y))
 932
 933 Then 'bar' should jolly well have arity 4 (two dicts, two args), but
 934 we ended up with something like
 935    bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
 936                                 in \x,y. <blah>)
 937
 938 This is all a bit ad-hoc; eg it relies on knowing that implication
 939 constraints build tuples.
 940
 941 --------------------- Implicit parameters ---------------------------------
 942
 943 \begin{code}
 944 isIPPred :: PredType -> Bool
 945 isIPPred (IParam _ _) = True
 946 isIPPred _            = False
 947
 948 isInheritablePred :: PredType -> Bool
 949 -- Can be inherited by a context.  For example, consider
 950 --      f x = let g y = (?v, y+x)
 951 --            in (g 3 with ?v = 8,
 952 --                g 4 with ?v = 9)
 953 -- The point is that g's type must be quantifed over ?v:
 954 --      g :: (?v :: a) => a -> a
 955 -- but it doesn't need to be quantified over the Num a dictionary
 956 -- which can be free in g's rhs, and shared by both calls to g
 957 isInheritablePred (ClassP _ _) = True
 958 isInheritablePred (EqPred _ _) = True
 959 isInheritablePred _            = False
 960 \end{code}
 961
 962 --------------------- Equality predicates ---------------------------------
 963 \begin{code}
 964 substEqSpec :: TvSubst -> [(TyVar,Type)] -> [(TcType,TcType)]
 965 substEqSpec subst eq_spec = [ (substTyVar subst tv, substTy subst ty)
 966                             | (tv,ty) <- eq_spec]
 967 \end{code}
 968
 969
 970 %************************************************************************
 971 %*                                                                      *
 972 \subsection{Predicates}
 973 %*                                                                      *
 974 %************************************************************************
 975
 976 isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have
 977 any foralls.  E.g.
 978         f :: (?x::Int) => Int -> Int
 979
 980 \begin{code}
 981 isSigmaTy :: Type -> Bool
 982 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
 983 isSigmaTy (ForAllTy _ _) = True
 984 isSigmaTy (FunTy a _)    = isPredTy a
 985 isSigmaTy _              = False
 986
 987 isOverloadedTy :: Type -> Bool
 988 -- Yes for a type of a function that might require evidence-passing
 989 -- Used only by bindInstsOfLocalFuns/Pats
 990 -- NB: be sure to check for type with an equality predicate; hence isCoVar
 991 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
 992 isOverloadedTy (ForAllTy tv ty) = isCoVar tv || isOverloadedTy ty
 993 isOverloadedTy (FunTy a _)      = isPredTy a
 994 isOverloadedTy _                = False
 995
 996 isPredTy :: Type -> Bool        -- Belongs in TcType because it does
 997                                 -- not look through newtypes, or predtypes (of course)
 998 isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
 999 isPredTy (PredTy _) = True
1000 isPredTy _          = False
1001 \end{code}
1002
1003 \begin{code}
1004 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
1005     isUnitTy, isCharTy :: Type -> Bool
1006 isFloatTy      = is_tc floatTyConKey
1007 isDoubleTy     = is_tc doubleTyConKey
1008 isIntegerTy    = is_tc integerTyConKey
1009 isIntTy        = is_tc intTyConKey
1010 isWordTy       = is_tc wordTyConKey
1011 isBoolTy       = is_tc boolTyConKey
1012 isUnitTy       = is_tc unitTyConKey
1013 isCharTy       = is_tc charTyConKey
1014
1015 isStringTy :: Type -> Bool
1016 isStringTy ty
1017   = case tcSplitTyConApp_maybe ty of
1018       Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
1019       _                   -> False
1020
1021 is_tc :: Unique -> Type -> Bool
1022 -- Newtypes are opaque to this
1023 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
1024                         Just (tc, _) -> uniq == getUnique tc
1025                         Nothing      -> False
1026 \end{code}
1027
1028 \begin{code}
1029 -- NB: Currently used in places where we have already expanded type synonyms;
1030 --     hence no 'coreView'.  This could, however, be changed without breaking
1031 --     any code.
1032 isOpenSynTyConApp :: TcTauType -> Bool
1033 isOpenSynTyConApp (TyConApp tc tys) = isOpenSynTyCon tc &&
1034                                       length tys == tyConArity tc
1035 isOpenSynTyConApp _other            = False
1036 \end{code}
1037
1038
1039 %************************************************************************
1040 %*                                                                      *
1041 \subsection{Misc}
1042 %*                                                                      *
1043 %************************************************************************
1044
1045 \begin{code}
1046 deNoteType :: Type -> Type
1047 -- Remove all *outermost* type synonyms and other notes
1048 deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
1049 deNoteType ty = ty
1050 \end{code}
1051
1052 \begin{code}
1053 tcTyVarsOfType :: Type -> TcTyVarSet
1054 -- Just the *TcTyVars* free in the type
1055 -- (Types.tyVarsOfTypes finds all free TyVars)
1056 tcTyVarsOfType (TyVarTy tv)         = if isTcTyVar tv then unitVarSet tv
1057                                                       else emptyVarSet
1058 tcTyVarsOfType (TyConApp _ tys)     = tcTyVarsOfTypes tys
1059 tcTyVarsOfType (PredTy sty)         = tcTyVarsOfPred sty
1060 tcTyVarsOfType (FunTy arg res)      = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
1061 tcTyVarsOfType (AppTy fun arg)      = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
1062 tcTyVarsOfType (ForAllTy tyvar ty)  = (tcTyVarsOfType ty `delVarSet` tyvar)
1063                                       `unionVarSet` tcTyVarsOfTyVar tyvar
1064         -- We do sometimes quantify over skolem TcTyVars
1065
1066 tcTyVarsOfTyVar :: TcTyVar -> TyVarSet
1067 tcTyVarsOfTyVar tv | isCoVar tv = tcTyVarsOfType (tyVarKind tv)
1068                    | otherwise  = emptyVarSet
1069
1070 tcTyVarsOfTypes :: [Type] -> TyVarSet
1071 tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
1072
1073 tcTyVarsOfPred :: PredType -> TyVarSet
1074 tcTyVarsOfPred (IParam _ ty)    = tcTyVarsOfType ty
1075 tcTyVarsOfPred (ClassP _ tys)   = tcTyVarsOfTypes tys
1076 tcTyVarsOfPred (EqPred ty1 ty2) = tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
1077 \end{code}
1078
1079 Note [Silly type synonym]
1080 ~~~~~~~~~~~~~~~~~~~~~~~~~
1081 Consider
1082         type T a = Int
1083 What are the free tyvars of (T x)?  Empty, of course!
1084 Here's the example that Ralf Laemmel showed me:
1085         foo :: (forall a. C u a -> C u a) -> u
1086         mappend :: Monoid u => u -> u -> u
1087
1088         bar :: Monoid u => u
1089         bar = foo (\t -> t `mappend` t)
1090 We have to generalise at the arg to f, and we don't
1091 want to capture the constraint (Monad (C u a)) because
1092 it appears to mention a.  Pretty silly, but it was useful to him.
1093
1094 exactTyVarsOfType is used by the type checker to figure out exactly
1095 which type variables are mentioned in a type.  It's also used in the
1096 smart-app checking code --- see TcExpr.tcIdApp
1097
1098 On the other hand, consider a *top-level* definition
1099         f = (\x -> x) :: T a -> T a
1100 If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
1101 if we have an application like (f "x") we get a confusing error message
1102 involving Any.  So the conclusion is this: when generalising
1103   - at top level use tyVarsOfType
1104   - in nested bindings use exactTyVarsOfType
1105 See Trac #1813 for example.
1106
1107 \begin{code}
1108 exactTyVarsOfType :: TcType -> TyVarSet
1109 -- Find the free type variables (of any kind)
1110 -- but *expand* type synonyms.  See Note [Silly type synonym] above.
1111 exactTyVarsOfType ty
1112   = go ty
1113   where
1114     go ty | Just ty' <- tcView ty = go ty'      -- This is the key line
1115     go (TyVarTy tv)               = unitVarSet tv
1116     go (TyConApp _ tys)           = exactTyVarsOfTypes tys
1117     go (PredTy ty)                = go_pred ty
1118     go (FunTy arg res)            = go arg `unionVarSet` go res
1119     go (AppTy fun arg)            = go fun `unionVarSet` go arg
1120     go (ForAllTy tyvar ty)        = delVarSet (go ty) tyvar
1121                                     `unionVarSet` go_tv tyvar
1122
1123     go_pred (IParam _ ty)    = go ty
1124     go_pred (ClassP _ tys)   = exactTyVarsOfTypes tys
1125     go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
1126
1127     go_tv tyvar | isCoVar tyvar = go (tyVarKind tyvar)
1128                 | otherwise     = emptyVarSet
1129
1130 exactTyVarsOfTypes :: [TcType] -> TyVarSet
1131 exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
1132 \end{code}
1133
1134 Find the free tycons and classes of a type.  This is used in the front
1135 end of the compiler.
1136
1137 \begin{code}
1138 tyClsNamesOfType :: Type -> NameSet
1139 tyClsNamesOfType (TyVarTy _)                = emptyNameSet
1140 tyClsNamesOfType (TyConApp tycon tys)       = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
1141 tyClsNamesOfType (PredTy (IParam _ ty))     = tyClsNamesOfType ty
1142 tyClsNamesOfType (PredTy (ClassP cl tys))   = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
1143 tyClsNamesOfType (PredTy (EqPred ty1 ty2))  = tyClsNamesOfType ty1 `unionNameSets` tyClsNamesOfType ty2
1144 tyClsNamesOfType (FunTy arg res)            = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
1145 tyClsNamesOfType (AppTy fun arg)            = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
1146 tyClsNamesOfType (ForAllTy _ ty)            = tyClsNamesOfType ty
1147
1148 tyClsNamesOfTypes :: [Type] -> NameSet
1149 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
1150
1151 tyClsNamesOfDFunHead :: Type -> NameSet
1152 -- Find the free type constructors and classes
1153 -- of the head of the dfun instance type
1154 -- The 'dfun_head_type' is because of
1155 --      instance Foo a => Baz T where ...
1156 -- The decl is an orphan if Baz and T are both not locally defined,
1157 --      even if Foo *is* locally defined
1158 tyClsNamesOfDFunHead dfun_ty
1159   = case tcSplitSigmaTy dfun_ty of
1160         (_, _, head_ty) -> tyClsNamesOfType head_ty
1161 \end{code}
1162
1163
1164 %************************************************************************
1165 %*                                                                      *
1166 \subsection[TysWiredIn-ext-type]{External types}
1167 %*                                                                      *
1168 %************************************************************************
1169
1170 The compiler's foreign function interface supports the passing of a
1171 restricted set of types as arguments and results (the restricting factor
1172 being the )
1173
1174 \begin{code}
1175 tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type, CoercionI)
1176 -- (isIOType t) returns Just (IO,t',co)
1177 --                              if co : t ~ IO t'
1178 --              returns Nothing otherwise
1179 tcSplitIOType_maybe ty
1180   = case tcSplitTyConApp_maybe ty of
1181         -- This split absolutely has to be a tcSplit, because we must
1182         -- see the IO type; and it's a newtype which is transparent to splitTyConApp.
1183
1184         Just (io_tycon, [io_res_ty])
1185            |  io_tycon `hasKey` ioTyConKey
1186            -> Just (io_tycon, io_res_ty, IdCo)
1187
1188         Just (tc, tys)
1189            | not (isRecursiveTyCon tc)
1190            , Just (ty, co1) <- instNewTyCon_maybe tc tys
1191                   -- Newtypes that require a coercion are ok
1192            -> case tcSplitIOType_maybe ty of
1193                 Nothing             -> Nothing
1194                 Just (tc, ty', co2) -> Just (tc, ty', co1 `mkTransCoI` co2)
1195
1196         _ -> Nothing
1197
1198 isFFITy :: Type -> Bool
1199 -- True for any TyCon that can possibly be an arg or result of an FFI call
1200 isFFITy ty = checkRepTyCon legalFFITyCon ty
1201
1202 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
1203 -- Checks for valid argument type for a 'foreign import'
1204 isFFIArgumentTy dflags safety ty
1205    = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
1206
1207 isFFIExternalTy :: Type -> Bool
1208 -- Types that are allowed as arguments of a 'foreign export'
1209 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
1210
1211 isFFIImportResultTy :: DynFlags -> Type -> Bool
1212 isFFIImportResultTy dflags ty
1213   = checkRepTyCon (legalFIResultTyCon dflags) ty
1214
1215 isFFIExportResultTy :: Type -> Bool
1216 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
1217
1218 isFFIDynArgumentTy :: Type -> Bool
1219 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
1220 -- or a newtype of either.
1221 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1222
1223 isFFIDynResultTy :: Type -> Bool
1224 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
1225 -- or a newtype of either.
1226 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1227
1228 isFFILabelTy :: Type -> Bool
1229 -- The type of a foreign label must be Ptr, FunPtr, Addr,
1230 -- or a newtype of either.
1231 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
1232
1233 isFFIPrimArgumentTy :: DynFlags -> Type -> Bool
1234 -- Checks for valid argument type for a 'foreign import prim'
1235 -- Currently they must all be simple unlifted types.
1236 isFFIPrimArgumentTy dflags ty
1237    = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
1238
1239 isFFIPrimResultTy :: DynFlags -> Type -> Bool
1240 -- Checks for valid result type for a 'foreign import prim'
1241 -- Currently it must be an unlifted type, including unboxed tuples.
1242 isFFIPrimResultTy dflags ty
1243    = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
1244
1245 isFFIDotnetTy :: DynFlags -> Type -> Bool
1246 isFFIDotnetTy dflags ty
1247   = checkRepTyCon (\ tc -> (legalFIResultTyCon dflags tc ||
1248                            isFFIDotnetObjTy ty || isStringTy ty)) ty
1249         -- NB: isStringTy used to look through newtypes, but
1250         --     it no longer does so.  May need to adjust isFFIDotNetTy
1251         --     if we do want to look through newtypes.
1252
1253 isFFIDotnetObjTy :: Type -> Bool
1254 isFFIDotnetObjTy ty
1255   = checkRepTyCon check_tc t_ty
1256   where
1257    (_, t_ty) = tcSplitForAllTys ty
1258    check_tc tc = getName tc == objectTyConName
1259
1260 isFunPtrTy :: Type -> Bool
1261 isFunPtrTy = checkRepTyConKey [funPtrTyConKey]
1262
1263 toDNType :: Type -> DNType
1264 toDNType ty
1265   | isStringTy ty = DNString
1266   | isFFIDotnetObjTy ty = DNObject
1267   | Just (tc,argTys) <- tcSplitTyConApp_maybe ty
1268   =  case lookup (getUnique tc) dn_assoc of
1269        Just x  -> x
1270        Nothing
1271          | tc `hasKey` ioTyConKey -> toDNType (head argTys)
1272          | otherwise -> pprPanic ("toDNType: unsupported .NET type")
1273                           (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
1274   | otherwise = panic "toDNType"        -- Is this right?
1275     where
1276       dn_assoc :: [ (Unique, DNType) ]
1277       dn_assoc = [ (unitTyConKey,   DNUnit)
1278                  , (intTyConKey,    DNInt)
1279                  , (int8TyConKey,   DNInt8)
1280                  , (int16TyConKey,  DNInt16)
1281                  , (int32TyConKey,  DNInt32)
1282                  , (int64TyConKey,  DNInt64)
1283                  , (wordTyConKey,   DNInt)
1284                  , (word8TyConKey,  DNWord8)
1285                  , (word16TyConKey, DNWord16)
1286                  , (word32TyConKey, DNWord32)
1287                  , (word64TyConKey, DNWord64)
1288                  , (floatTyConKey,  DNFloat)
1289                  , (doubleTyConKey, DNDouble)
1290                  , (ptrTyConKey,    DNPtr)
1291                  , (funPtrTyConKey, DNPtr)
1292                  , (charTyConKey,   DNChar)
1293                  , (boolTyConKey,   DNBool)
1294                  ]
1295
1296 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
1297 -- Look through newtypes, but *not* foralls
1298 -- Should work even for recursive newtypes
1299 -- eg Manuel had:       newtype T = MkT (Ptr T)
1300 checkRepTyCon check_tc ty
1301   = go [] ty
1302   where
1303     go rec_nts ty
1304       | Just (tc,tys) <- splitTyConApp_maybe ty
1305       = case carefullySplitNewType_maybe rec_nts tc tys of
1306            Just (rec_nts', ty') -> go rec_nts' ty'
1307            Nothing              -> check_tc tc
1308       | otherwise
1309       = False
1310
1311 checkRepTyConKey :: [Unique] -> Type -> Bool
1312 -- Like checkRepTyCon, but just looks at the TyCon key
1313 checkRepTyConKey keys
1314   = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
1315 \end{code}
1316
1317 ----------------------------------------------
1318 These chaps do the work; they are not exported
1319 ----------------------------------------------
1320
1321 \begin{code}
1322 legalFEArgTyCon :: TyCon -> Bool
1323 legalFEArgTyCon tc
1324   -- It's illegal to make foreign exports that take unboxed
1325   -- arguments.  The RTS API currently can't invoke such things.  --SDM 7/2000
1326   = boxedMarshalableTyCon tc
1327
1328 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
1329 legalFIResultTyCon dflags tc
1330   | tc == unitTyCon         = True
1331   | otherwise               = marshalableTyCon dflags tc
1332
1333 legalFEResultTyCon :: TyCon -> Bool
1334 legalFEResultTyCon tc
1335   | tc == unitTyCon         = True
1336   | otherwise               = boxedMarshalableTyCon tc
1337
1338 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
1339 -- Checks validity of types going from Haskell -> external world
1340 legalOutgoingTyCon dflags _ tc
1341   = marshalableTyCon dflags tc
1342
1343 legalFFITyCon :: TyCon -> Bool
1344 -- True for any TyCon that can possibly be an arg or result of an FFI call
1345 legalFFITyCon tc
1346   = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
1347
1348 marshalableTyCon :: DynFlags -> TyCon -> Bool
1349 marshalableTyCon dflags tc
1350   =  (dopt Opt_UnliftedFFITypes dflags
1351       && isUnLiftedTyCon tc
1352       && not (isUnboxedTupleTyCon tc)
1353       && case tyConPrimRep tc of        -- Note [Marshalling VoidRep]
1354            VoidRep -> False
1355            _       -> True)
1356   || boxedMarshalableTyCon tc
1357
1358 boxedMarshalableTyCon :: TyCon -> Bool
1359 boxedMarshalableTyCon tc
1360    = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
1361                          , int32TyConKey, int64TyConKey
1362                          , wordTyConKey, word8TyConKey, word16TyConKey
1363                          , word32TyConKey, word64TyConKey
1364                          , floatTyConKey, doubleTyConKey
1365                          , ptrTyConKey, funPtrTyConKey
1366                          , charTyConKey
1367                          , stablePtrTyConKey
1368                          , boolTyConKey
1369                          ]
1370
1371 legalFIPrimArgTyCon :: DynFlags -> TyCon -> Bool
1372 -- Check args of 'foreign import prim', only allow simple unlifted types.
1373 -- Strictly speaking it is unnecessary to ban unboxed tuples here since
1374 -- currently they're of the wrong kind to use in function args anyway.
1375 legalFIPrimArgTyCon dflags tc
1376   = dopt Opt_UnliftedFFITypes dflags
1377     && isUnLiftedTyCon tc
1378     && not (isUnboxedTupleTyCon tc)
1379
1380 legalFIPrimResultTyCon :: DynFlags -> TyCon -> Bool
1381 -- Check result type of 'foreign import prim'. Allow simple unlifted
1382 -- types and also unboxed tuple result types '... -> (# , , #)'
1383 legalFIPrimResultTyCon dflags tc
1384   = dopt Opt_UnliftedFFITypes dflags
1385     && isUnLiftedTyCon tc
1386     && (isUnboxedTupleTyCon tc
1387         || case tyConPrimRep tc of      -- Note [Marshalling VoidRep]
1388            VoidRep -> False
1389            _       -> True)
1390 \end{code}
1391
1392 Note [Marshalling VoidRep]
1393 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1394 We don't treat State# (whose PrimRep is VoidRep) as marshalable.
1395 In turn that means you can't write
1396         foreign import foo :: Int -> State# RealWorld
1397
1398 Reason: the back end falls over with panic "primRepHint:VoidRep";
1399         and there is no compelling reason to permit it