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