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