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