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