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