ghc/compiler/typecheck/TcType.lhs

   1
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcType]{Types used in the typechecker}
   5
   6 This module provides the Type interface for front-end parts of the
   7 compiler.  These parts
   8
   9         * treat "source types" as opaque:
  10                 newtypes, and predicates are meaningful.
  11         * look through usage types
  12
  13 The "tc" prefix is for "typechechecker", because the type checker
  14 is the principal client.
  15
  16 \begin{code}
  17 module TcType (
  18   --------------------------------
  19   -- Types
  20   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
  21   TcTyVar, TcTyVarSet, TcKind,
  22
  23   --------------------------------
  24   -- MetaDetails
  25   Expected(..), TcRef, TcTyVarDetails(..),
  26   MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
  27   isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
  28   isFlexi, isIndirect,
  29
  30   --------------------------------
  31   -- Builders
  32   mkPhiTy, mkSigmaTy, hoistForAllTys,
  33
  34   --------------------------------
  35   -- Splitters
  36   -- These are important because they do not look through newtypes
  37   tcSplitForAllTys, tcSplitPhiTy,
  38   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
  39   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
  40   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
  41   tcGetTyVar_maybe, tcGetTyVar,
  42
  43   ---------------------------------
  44   -- Predicates.
  45   -- Again, newtypes are opaque
  46   tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
  47   isSigmaTy, isOverloadedTy,
  48   isDoubleTy, isFloatTy, isIntTy,
  49   isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
  50   isTauTy, tcIsTyVarTy, tcIsForAllTy,
  51
  52   ---------------------------------
  53   -- Misc type manipulators
  54   deNoteType, classesOfTheta,
  55   tyClsNamesOfType, tyClsNamesOfDFunHead,
  56   getDFunTyKey,
  57
  58   ---------------------------------
  59   -- Predicate types
  60   getClassPredTys_maybe, getClassPredTys,
  61   isClassPred, isTyVarClassPred,
  62   mkDictTy, tcSplitPredTy_maybe,
  63   isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
  64   mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
  65
  66   ---------------------------------
  67   -- Foreign import and export
  68   isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
  69   isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
  70   isFFIExportResultTy, -- :: Type -> Bool
  71   isFFIExternalTy,     -- :: Type -> Bool
  72   isFFIDynArgumentTy,  -- :: Type -> Bool
  73   isFFIDynResultTy,    -- :: Type -> Bool
  74   isFFILabelTy,        -- :: Type -> Bool
  75   isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
  76   isFFIDotnetObjTy,    -- :: Type -> Bool
  77   isFFITy,             -- :: Type -> Bool
  78
  79   toDNType,            -- :: Type -> DNType
  80
  81   --------------------------------
  82   -- Rexported from Type
  83   Kind,         -- Stuff to do with kinds is insensitive to pre/post Tc
  84   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
  85   isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
  86   isArgTypeKind, isSubKind, defaultKind,
  87
  88   Type, PredType(..), ThetaType,
  89   mkForAllTy, mkForAllTys,
  90   mkFunTy, mkFunTys, zipFunTys,
  91   mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
  92   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
  93
  94   -- Type substitutions
  95   TvSubst(..),  -- Representation visible to a few friends
  96   TvSubstEnv, emptyTvSubst,
  97   mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
  98   getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
  99   extendTvSubst, extendTvSubstList, isInScope,
 100   substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
 101
 102   isUnLiftedType,       -- Source types are always lifted
 103   isUnboxedTupleType,   -- Ditto
 104   isPrimitiveType,
 105
 106   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 107   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
 108   typeKind,
 109
 110   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
 111
 112   pprKind, pprParendKind,
 113   pprType, pprParendType, pprTyThingCategory,
 114   pprPred, pprTheta, pprThetaArrow, pprClassPred
 115
 116   ) where
 117
 118 #include "HsVersions.h"
 119
 120 -- friends:
 121 import TypeRep          ( Type(..), TyNote(..), funTyCon )  -- friend
 122
 123 import Type             (       -- Re-exports
 124                           tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
 125                           tyVarsOfTheta, Kind, PredType(..),
 126                           ThetaType, unliftedTypeKind,
 127                           liftedTypeKind, openTypeKind, mkArrowKind,
 128                           isLiftedTypeKind, isUnliftedTypeKind,
 129                           mkArrowKinds, mkForAllTy, mkForAllTys,
 130                           defaultKind, isArgTypeKind, isOpenTypeKind,
 131                           mkFunTy, mkFunTys, zipFunTys,
 132                           mkTyConApp, mkGenTyConApp, mkAppTy,
 133                           mkAppTys, mkSynTy, applyTy, applyTys,
 134                           mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
 135                           mkPredTys, isUnLiftedType,
 136                           isUnboxedTupleType, isPrimitiveType,
 137                           splitTyConApp_maybe,
 138                           tidyTopType, tidyType, tidyPred, tidyTypes,
 139                           tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 140                           tidyTyVarBndr, tidyOpenTyVar,
 141                           tidyOpenTyVars,
 142                           isSubKind, deShadowTy,
 143
 144                           tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
 145                           tcEqPred, tcCmpPred, tcEqTypeX,
 146
 147                           TvSubst(..),
 148                           TvSubstEnv, emptyTvSubst,
 149                           mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
 150                           getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
 151                           extendTvSubst, extendTvSubstList, isInScope,
 152                           substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
 153
 154                           typeKind, repType,
 155                           pprKind, pprParendKind,
 156                           pprType, pprParendType, pprTyThingCategory,
 157                           pprPred, pprTheta, pprThetaArrow, pprClassPred
 158                         )
 159 import TyCon            ( TyCon, isUnLiftedTyCon, tyConUnique )
 160 import DataCon          ( DataCon )
 161 import Class            ( Class )
 162 import Var              ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
 163 import ForeignCall      ( Safety, playSafe, DNType(..) )
 164 import VarSet
 165
 166 -- others:
 167 import CmdLineOpts      ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 168 import Name             ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 169 import NameSet
 170 import VarEnv           ( TidyEnv )
 171 import OccName          ( OccName, mkDictOcc )
 172 import PrelNames        -- Lots (e.g. in isFFIArgumentTy)
 173 import TysWiredIn       ( unitTyCon, charTyCon, listTyCon )
 174 import BasicTypes       ( IPName(..), ipNameName )
 175 import SrcLoc           ( SrcLoc, SrcSpan )
 176 import Util             ( snocView )
 177 import Maybes           ( maybeToBool, expectJust )
 178 import Outputable
 179 import DATA_IOREF
 180 \end{code}
 181
 182
 183 %************************************************************************
 184 %*                                                                      *
 185 \subsection{Types}
 186 %*                                                                      *
 187 %************************************************************************
 188
 189 The type checker divides the generic Type world into the
 190 following more structured beasts:
 191
 192 sigma ::= forall tyvars. phi
 193         -- A sigma type is a qualified type
 194         --
 195         -- Note that even if 'tyvars' is empty, theta
 196         -- may not be: e.g.   (?x::Int) => Int
 197
 198         -- Note that 'sigma' is in prenex form:
 199         -- all the foralls are at the front.
 200         -- A 'phi' type has no foralls to the right of
 201         -- an arrow
 202
 203 phi :: theta => rho
 204
 205 rho ::= sigma -> rho
 206      |  tau
 207
 208 -- A 'tau' type has no quantification anywhere
 209 -- Note that the args of a type constructor must be taus
 210 tau ::= tyvar
 211      |  tycon tau_1 .. tau_n
 212      |  tau_1 tau_2
 213      |  tau_1 -> tau_2
 214
 215 -- In all cases, a (saturated) type synonym application is legal,
 216 -- provided it expands to the required form.
 217
 218 \begin{code}
 219 type TcType = Type              -- A TcType can have mutable type variables
 220         -- Invariant on ForAllTy in TcTypes:
 221         --      forall a. T
 222         -- a cannot occur inside a MutTyVar in T; that is,
 223         -- T is "flattened" before quantifying over a
 224
 225 type TcPredType     = PredType
 226 type TcThetaType    = ThetaType
 227 type TcSigmaType    = TcType
 228 type TcRhoType      = TcType
 229 type TcTauType      = TcType
 230 type TcKind         = Kind
 231 type TcTyVarSet     = TyVarSet
 232
 233 type TcRef a     = IORef a
 234 data Expected ty = Infer (TcRef ty)     -- The hole to fill in for type inference
 235                  | Check ty             -- The type to check during type checking
 236 \end{code}
 237
 238
 239 %************************************************************************
 240 %*                                                                      *
 241 \subsection{TyVarDetails}
 242 %*                                                                      *
 243 %************************************************************************
 244
 245 TyVarDetails gives extra info about type variables, used during type
 246 checking.  It's attached to mutable type variables only.
 247 It's knot-tied back to Var.lhs.  There is no reason in principle
 248 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 249
 250 Note [Signature skolems]
 251 ~~~~~~~~~~~~~~~~~~~~~~~~
 252 Consider this
 253
 254   x :: [a]
 255   y :: b
 256   (x,y,z) = ([y,z], z, head x)
 257
 258 Here, x and y have type sigs, which go into the environment.  We used to
 259 instantiate their types with skolem constants, and push those types into
 260 the RHS, so we'd typecheck the RHS with type
 261         ( [a*], b*, c )
 262 where a*, b* are skolem constants, and c is an ordinary meta type varible.
 263
 264 The trouble is that the occurrences of z in the RHS force a* and b* to
 265 be the *same*, so we can't make them into skolem constants that don't unify
 266 with each other.  Alas.
 267
 268 On the other hand, we *must* use skolems for signature type variables,
 269 becuase GADT type refinement refines skolems only.
 270
 271 One solution woudl be insist that in the above defn the programmer uses
 272 the same type variable in both type signatures.  But that takes explanation.
 273
 274 The alternative (currently implemented) is to have a special kind of skolem
 275 constant, SigSkokTv, which can unify with other SigSkolTvs.
 276
 277
 278 \begin{code}
 279 type TcTyVar = TyVar    -- Used only during type inference
 280
 281 -- A TyVarDetails is inside a TyVar
 282 data TcTyVarDetails
 283   = MetaTv (IORef MetaDetails)          -- A meta type variable stands for a tau-type
 284   | SkolemTv SkolemInfo                 -- A skolem constant
 285   | SigSkolTv Name (IORef MetaDetails)  -- Ditto, but from a type signature;
 286                                         --      see Note [Signature skolems]
 287                                         --      The MetaDetails, if filled in, will
 288                                         --      always be another SigSkolTv
 289
 290 data SkolemInfo
 291   = SigSkol Name        -- Bound at a type signature
 292   | ClsSkol Class       -- Bound at a class decl
 293   | InstSkol Id         -- Bound at an instance decl
 294   | PatSkol DataCon     -- An existential type variable bound by a pattern for
 295             SrcSpan     -- a data constructor with an existential type. E.g.
 296                         --      data T = forall a. Eq a => MkT a
 297                         --      f (MkT x) = ...
 298                         -- The pattern MkT x will allocate an existential type
 299                         -- variable for 'a'.
 300   | ArrowSkol SrcSpan   -- An arrow form (see TcArrows)
 301
 302   | GenSkol [TcTyVar]   -- Bound when doing a subsumption check for
 303             TcType      --      (forall tvs. ty)
 304             SrcSpan
 305
 306 data MetaDetails
 307   = Flexi          -- Flexi type variables unify to become
 308                    -- Indirects.
 309
 310   | Indirect TcType  -- Type indirections, treated as wobbly
 311                      -- for the purpose of GADT unification.
 312
 313 tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
 314 -- Tidy the type inside a GenSkol, preparatory to printing it
 315 tidySkolemTyVar env tv
 316   = ASSERT( isSkolemTyVar tv )
 317     (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
 318   where
 319     (env1, info1) = case tcTyVarDetails tv of
 320                       SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
 321                             where
 322                               (env1, tvs1) = tidyOpenTyVars env tvs
 323                               (env2, ty1)  = tidyOpenType env1 ty
 324                       info -> (env, info)
 325
 326 pprTcTyVar :: TcTyVar -> SDoc
 327 -- Print tyvar with info about its binding
 328 pprTcTyVar tv
 329   = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
 330   where
 331     ppr_details (MetaTv _)       = ptext SLIT("is a meta type variable")
 332     ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
 333     ppr_details (SkolemTv info)  = ptext SLIT("is bound by") <+> pprSkolInfo info
 334
 335 pprSkolInfo :: SkolemInfo -> SDoc
 336 pprSkolInfo (SigSkol id)     = ptext SLIT("the type signature for") <+> quotes (ppr id)
 337 pprSkolInfo (ClsSkol cls)    = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
 338 pprSkolInfo (InstSkol df)    = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
 339 pprSkolInfo (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
 340 pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
 341                                     nest 2 (ptext SLIT("at") <+> ppr loc)]
 342 pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type")
 343                                         <+> quotes (ppr (mkForAllTys tvs ty)),
 344                                         nest 2 (ptext SLIT("at") <+> ppr loc)]
 345
 346 instance Outputable MetaDetails where
 347   ppr Flexi         = ptext SLIT("Flexi")
 348   ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty
 349
 350 isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isMetaTyVar :: TyVar -> Bool
 351 isImmutableTyVar tv
 352   | isTcTyVar tv = isSkolemTyVar tv
 353   | otherwise    = True
 354
 355 isSkolemTyVar tv
 356   = ASSERT( isTcTyVar tv )
 357     case tcTyVarDetails tv of
 358         SkolemTv _    -> True
 359         SigSkolTv _ _ -> True
 360         MetaTv _      -> False
 361
 362 isExistentialTyVar tv   -- Existential type variable, bound by a pattern
 363   = ASSERT( isTcTyVar tv )
 364     case tcTyVarDetails tv of
 365         SkolemTv (PatSkol _ _) -> True
 366         other                  -> False
 367
 368 isMetaTyVar tv
 369   = ASSERT( isTcTyVar tv )
 370     case tcTyVarDetails tv of
 371         MetaTv _   -> True
 372         other      -> False
 373
 374 metaTvRef :: TyVar -> IORef MetaDetails
 375 metaTvRef tv
 376   = ASSERT( isTcTyVar tv )
 377     case tcTyVarDetails tv of
 378         MetaTv ref -> ref
 379         other      -> pprPanic "metaTvRef" (ppr tv)
 380
 381 isFlexi, isIndirect :: MetaDetails -> Bool
 382 isFlexi Flexi = True
 383 isFlexi other = False
 384
 385 isIndirect (Indirect _) = True
 386 isIndirect other        = False
 387 \end{code}
 388
 389
 390 %************************************************************************
 391 %*                                                                      *
 392 \subsection{Tau, sigma and rho}
 393 %*                                                                      *
 394 %************************************************************************
 395
 396 \begin{code}
 397 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
 398
 399 mkPhiTy :: [PredType] -> Type -> Type
 400 mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
 401 \end{code}
 402
 403 @isTauTy@ tests for nested for-alls.
 404
 405 \begin{code}
 406 isTauTy :: Type -> Bool
 407 isTauTy (TyVarTy v)      = True
 408 isTauTy (TyConApp _ tys) = all isTauTy tys
 409 isTauTy (AppTy a b)      = isTauTy a && isTauTy b
 410 isTauTy (FunTy a b)      = isTauTy a && isTauTy b
 411 isTauTy (PredTy p)       = True         -- Don't look through source types
 412 isTauTy (NoteTy _ ty)    = isTauTy ty
 413 isTauTy other            = False
 414 \end{code}
 415
 416 \begin{code}
 417 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
 418                                 -- construct a dictionary function name
 419 getDFunTyKey (TyVarTy tv)    = getOccName tv
 420 getDFunTyKey (TyConApp tc _) = getOccName tc
 421 getDFunTyKey (AppTy fun _)   = getDFunTyKey fun
 422 getDFunTyKey (NoteTy _ t)    = getDFunTyKey t
 423 getDFunTyKey (FunTy arg _)   = getOccName funTyCon
 424 getDFunTyKey (ForAllTy _ t)  = getDFunTyKey t
 425 getDFunTyKey ty              = pprPanic "getDFunTyKey" (pprType ty)
 426 -- PredTy shouldn't happen
 427 \end{code}
 428
 429
 430 %************************************************************************
 431 %*                                                                      *
 432 \subsection{Expanding and splitting}
 433 %*                                                                      *
 434 %************************************************************************
 435
 436 These tcSplit functions are like their non-Tc analogues, but
 437         a) they do not look through newtypes
 438         b) they do not look through PredTys
 439         c) [future] they ignore usage-type annotations
 440
 441 However, they are non-monadic and do not follow through mutable type
 442 variables.  It's up to you to make sure this doesn't matter.
 443
 444 \begin{code}
 445 tcSplitForAllTys :: Type -> ([TyVar], Type)
 446 tcSplitForAllTys ty = split ty ty []
 447    where
 448      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
 449      split orig_ty (NoteTy n  ty)   tvs = split orig_ty ty tvs
 450      split orig_ty t                tvs = (reverse tvs, orig_ty)
 451
 452 tcIsForAllTy (ForAllTy tv ty) = True
 453 tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
 454 tcIsForAllTy t                = False
 455
 456 tcSplitPhiTy :: Type -> ([PredType], Type)
 457 tcSplitPhiTy ty = split ty ty []
 458  where
 459   split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
 460                                         Just p  -> split res res (p:ts)
 461                                         Nothing -> (reverse ts, orig_ty)
 462   split orig_ty (NoteTy n ty)   ts = split orig_ty ty ts
 463   split orig_ty ty              ts = (reverse ts, orig_ty)
 464
 465 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
 466                         (tvs, rho) -> case tcSplitPhiTy rho of
 467                                         (theta, tau) -> (tvs, theta, tau)
 468
 469 tcTyConAppTyCon :: Type -> TyCon
 470 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
 471
 472 tcTyConAppArgs :: Type -> [Type]
 473 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
 474
 475 tcSplitTyConApp :: Type -> (TyCon, [Type])
 476 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
 477                         Just stuff -> stuff
 478                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 479
 480 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 481 tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 482 tcSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
 483 tcSplitTyConApp_maybe (NoteTy n ty)     = tcSplitTyConApp_maybe ty
 484         -- Newtypes are opaque, so they may be split
 485         -- However, predicates are not treated
 486         -- as tycon applications by the type checker
 487 tcSplitTyConApp_maybe other                     = Nothing
 488
 489 tcSplitFunTys :: Type -> ([Type], Type)
 490 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
 491                         Nothing        -> ([], ty)
 492                         Just (arg,res) -> (arg:args, res')
 493                                        where
 494                                           (args,res') = tcSplitFunTys res
 495
 496 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
 497 tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
 498 tcSplitFunTy_maybe (NoteTy n ty)    = tcSplitFunTy_maybe ty
 499 tcSplitFunTy_maybe other            = Nothing
 500
 501 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
 502 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 503
 504
 505 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
 506 tcSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 507 tcSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 508 tcSplitAppTy_maybe (NoteTy n ty)     = tcSplitAppTy_maybe ty
 509 tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
 510                                         Just (tys', ty') -> Just (TyConApp tc tys', ty')
 511                                         Nothing          -> Nothing
 512 tcSplitAppTy_maybe other             = Nothing
 513
 514 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
 515                     Just stuff -> stuff
 516                     Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
 517
 518 tcSplitAppTys :: Type -> (Type, [Type])
 519 tcSplitAppTys ty
 520   = go ty []
 521   where
 522     go ty args = case tcSplitAppTy_maybe ty of
 523                    Just (ty', arg) -> go ty' (arg:args)
 524                    Nothing         -> (ty,args)
 525
 526 tcGetTyVar_maybe :: Type -> Maybe TyVar
 527 tcGetTyVar_maybe (TyVarTy tv)   = Just tv
 528 tcGetTyVar_maybe (NoteTy _ t)   = tcGetTyVar_maybe t
 529 tcGetTyVar_maybe other          = Nothing
 530
 531 tcGetTyVar :: String -> Type -> TyVar
 532 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 533
 534 tcIsTyVarTy :: Type -> Bool
 535 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 536
 537 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
 538 -- Split the type of a dictionary function
 539 tcSplitDFunTy ty
 540   = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
 541     case tcSplitDFunHead tau of { (clas, tys) ->
 542     (tvs, theta, clas, tys) }}
 543
 544 tcSplitDFunHead :: Type -> (Class, [Type])
 545 tcSplitDFunHead tau
 546   = case tcSplitPredTy_maybe tau of
 547         Just (ClassP clas tys) -> (clas, tys)
 548 \end{code}
 549
 550
 551
 552 %************************************************************************
 553 %*                                                                      *
 554 \subsection{Predicate types}
 555 %*                                                                      *
 556 %************************************************************************
 557
 558 \begin{code}
 559 tcSplitPredTy_maybe :: Type -> Maybe PredType
 560    -- Returns Just for predicates only
 561 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
 562 tcSplitPredTy_maybe (PredTy p)    = Just p
 563 tcSplitPredTy_maybe other         = Nothing
 564
 565 predTyUnique :: PredType -> Unique
 566 predTyUnique (IParam n _)      = getUnique (ipNameName n)
 567 predTyUnique (ClassP clas tys) = getUnique clas
 568
 569 mkPredName :: Unique -> SrcLoc -> PredType -> Name
 570 mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
 571 mkPredName uniq loc (IParam ip ty)   = mkInternalName uniq (getOccName (ipNameName ip)) loc
 572 \end{code}
 573
 574
 575 --------------------- Dictionary types ---------------------------------
 576
 577 \begin{code}
 578 mkClassPred clas tys = ClassP clas tys
 579
 580 isClassPred :: PredType -> Bool
 581 isClassPred (ClassP clas tys) = True
 582 isClassPred other             = False
 583
 584 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
 585 isTyVarClassPred other             = False
 586
 587 getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
 588 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
 589 getClassPredTys_maybe _                 = Nothing
 590
 591 getClassPredTys :: PredType -> (Class, [Type])
 592 getClassPredTys (ClassP clas tys) = (clas, tys)
 593
 594 mkDictTy :: Class -> [Type] -> Type
 595 mkDictTy clas tys = mkPredTy (ClassP clas tys)
 596
 597 isDictTy :: Type -> Bool
 598 isDictTy (PredTy p)   = isClassPred p
 599 isDictTy (NoteTy _ ty)  = isDictTy ty
 600 isDictTy other          = False
 601 \end{code}
 602
 603 --------------------- Implicit parameters ---------------------------------
 604
 605 \begin{code}
 606 isIPPred :: PredType -> Bool
 607 isIPPred (IParam _ _) = True
 608 isIPPred other        = False
 609
 610 isInheritablePred :: PredType -> Bool
 611 -- Can be inherited by a context.  For example, consider
 612 --      f x = let g y = (?v, y+x)
 613 --            in (g 3 with ?v = 8,
 614 --                g 4 with ?v = 9)
 615 -- The point is that g's type must be quantifed over ?v:
 616 --      g :: (?v :: a) => a -> a
 617 -- but it doesn't need to be quantified over the Num a dictionary
 618 -- which can be free in g's rhs, and shared by both calls to g
 619 isInheritablePred (ClassP _ _) = True
 620 isInheritablePred other      = False
 621
 622 isLinearPred :: TcPredType -> Bool
 623 isLinearPred (IParam (Linear n) _) = True
 624 isLinearPred other                 = False
 625 \end{code}
 626
 627
 628 %************************************************************************
 629 %*                                                                      *
 630 \subsection{Predicates}
 631 %*                                                                      *
 632 %************************************************************************
 633
 634 isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have
 635 any foralls.  E.g.
 636         f :: (?x::Int) => Int -> Int
 637
 638 \begin{code}
 639 isSigmaTy :: Type -> Bool
 640 isSigmaTy (ForAllTy tyvar ty) = True
 641 isSigmaTy (FunTy a b)         = isPredTy a
 642 isSigmaTy (NoteTy n ty)       = isSigmaTy ty
 643 isSigmaTy _                   = False
 644
 645 isOverloadedTy :: Type -> Bool
 646 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 647 isOverloadedTy (FunTy a b)         = isPredTy a
 648 isOverloadedTy (NoteTy n ty)       = isOverloadedTy ty
 649 isOverloadedTy _                   = False
 650
 651 isPredTy :: Type -> Bool        -- Belongs in TcType because it does
 652                                 -- not look through newtypes, or predtypes (of course)
 653 isPredTy (NoteTy _ ty) = isPredTy ty
 654 isPredTy (PredTy sty)  = True
 655 isPredTy _             = False
 656 \end{code}
 657
 658 \begin{code}
 659 isFloatTy      = is_tc floatTyConKey
 660 isDoubleTy     = is_tc doubleTyConKey
 661 isIntegerTy    = is_tc integerTyConKey
 662 isIntTy        = is_tc intTyConKey
 663 isAddrTy       = is_tc addrTyConKey
 664 isBoolTy       = is_tc boolTyConKey
 665 isUnitTy       = is_tc unitTyConKey
 666
 667 is_tc :: Unique -> Type -> Bool
 668 -- Newtypes are opaque to this
 669 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 670                         Just (tc, _) -> uniq == getUnique tc
 671                         Nothing      -> False
 672 \end{code}
 673
 674
 675
 676
 677 %************************************************************************
 678 %*                                                                      *
 679                 Hoisting for-alls
 680 %*                                                                      *
 681 %************************************************************************
 682
 683 hoistForAllTys is used for user-written type signatures only
 684 We want to 'look through' type synonyms when doing this
 685 so it's better done on the Type than the HsType
 686
 687 It moves all the foralls and constraints to the top
 688 e.g.    T -> forall a. a        ==>   forall a. T -> a
 689         T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
 690
 691 Also: it eliminates duplicate constraints.  These can show up
 692 when hoisting constraints, notably implicit parameters.
 693
 694 It tries hard to retain type synonyms if hoisting does not break one
 695 up.  Not only does this improve error messages, but there's a tricky
 696 interaction with Haskell 98.  H98 requires no unsaturated type
 697 synonyms, which is checked by checkValidType.  This runs after
 698 hoisting, so we don't want hoisting to remove the SynNotes!  (We can't
 699 run validity checking before hoisting because in mutually-recursive
 700 type definitions we postpone validity checking until after the knot is
 701 tied.)
 702
 703 \begin{code}
 704 hoistForAllTys :: Type -> Type
 705 hoistForAllTys ty
 706   = go (deShadowTy ty)
 707         -- Running over ty with an empty substitution gives it the
 708         -- no-shadowing property.  This is important.  For example:
 709         --      type Foo r = forall a. a -> r
 710         --      foo :: Foo (Foo ())
 711         -- Here the hoisting should give
 712         --      foo :: forall a a1. a -> a1 -> ()
 713         --
 714         -- What about type vars that are lexically in scope in the envt?
 715         -- We simply rely on them having a different unique to any
 716         -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
 717         -- out of the envt, which is boring and (I think) not necessary.
 718
 719   where
 720     go (TyVarTy tv)                = TyVarTy tv
 721     go (TyConApp tc tys)           = TyConApp tc (map go tys)
 722     go (PredTy pred)               = PredTy pred    -- No nested foralls
 723     go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote (go ty1)) (go ty2)
 724     go (NoteTy (FTVNote _) ty2)    = go ty2         -- Discard the free tyvar note
 725     go (FunTy arg res)             = mk_fun_ty (go arg) (go res)
 726     go (AppTy fun arg)             = AppTy (go fun) (go arg)
 727     go (ForAllTy tv ty)            = ForAllTy tv (go ty)
 728
 729         -- mk_fun_ty does all the work.
 730         -- It's building t1 -> t2:
 731         --      if t2 is a for-all type, push t1 inside it
 732         --      if t2 is (pred -> t3), check for duplicates
 733     mk_fun_ty ty1 ty2
 734         | not (isSigmaTy ty2)           -- No forall's, or context =>
 735         = FunTy ty1 ty2
 736         | PredTy p1 <- ty1              -- ty1 is a predicate
 737         = if p1 `elem` theta then       -- so check for duplicates
 738                 ty2
 739           else
 740                 mkSigmaTy tvs (p1:theta) tau
 741         | otherwise
 742         = mkSigmaTy tvs theta (FunTy ty1 tau)
 743         where
 744           (tvs, theta, tau) = tcSplitSigmaTy ty2
 745 \end{code}
 746
 747
 748 %************************************************************************
 749 %*                                                                      *
 750 \subsection{Misc}
 751 %*                                                                      *
 752 %************************************************************************
 753
 754 \begin{code}
 755 deNoteType :: Type -> Type
 756         -- Remove synonyms, but not predicate types
 757 deNoteType ty@(TyVarTy tyvar)   = ty
 758 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
 759 deNoteType (PredTy p)           = PredTy (deNotePredType p)
 760 deNoteType (NoteTy _ ty)        = deNoteType ty
 761 deNoteType (AppTy fun arg)      = AppTy (deNoteType fun) (deNoteType arg)
 762 deNoteType (FunTy fun arg)      = FunTy (deNoteType fun) (deNoteType arg)
 763 deNoteType (ForAllTy tv ty)     = ForAllTy tv (deNoteType ty)
 764
 765 deNotePredType :: PredType -> PredType
 766 deNotePredType (ClassP c tys)   = ClassP c (map deNoteType tys)
 767 deNotePredType (IParam n ty)    = IParam n (deNoteType ty)
 768 \end{code}
 769
 770 Find the free tycons and classes of a type.  This is used in the front
 771 end of the compiler.
 772
 773 \begin{code}
 774 tyClsNamesOfType :: Type -> NameSet
 775 tyClsNamesOfType (TyVarTy tv)               = emptyNameSet
 776 tyClsNamesOfType (TyConApp tycon tys)       = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
 777 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
 778 tyClsNamesOfType (NoteTy other_note    ty2) = tyClsNamesOfType ty2
 779 tyClsNamesOfType (PredTy (IParam n ty))   = tyClsNamesOfType ty
 780 tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
 781 tyClsNamesOfType (FunTy arg res)            = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
 782 tyClsNamesOfType (AppTy fun arg)            = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
 783 tyClsNamesOfType (ForAllTy tyvar ty)        = tyClsNamesOfType ty
 784
 785 tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
 786
 787 tyClsNamesOfDFunHead :: Type -> NameSet
 788 -- Find the free type constructors and classes
 789 -- of the head of the dfun instance type
 790 -- The 'dfun_head_type' is because of
 791 --      instance Foo a => Baz T where ...
 792 -- The decl is an orphan if Baz and T are both not locally defined,
 793 --      even if Foo *is* locally defined
 794 tyClsNamesOfDFunHead dfun_ty
 795   = case tcSplitSigmaTy dfun_ty of
 796         (tvs,_,head_ty) -> tyClsNamesOfType head_ty
 797
 798 classesOfTheta :: ThetaType -> [Class]
 799 -- Looks just for ClassP things; maybe it should check
 800 classesOfTheta preds = [ c | ClassP c _ <- preds ]
 801 \end{code}
 802
 803
 804 %************************************************************************
 805 %*                                                                      *
 806 \subsection[TysWiredIn-ext-type]{External types}
 807 %*                                                                      *
 808 %************************************************************************
 809
 810 The compiler's foreign function interface supports the passing of a
 811 restricted set of types as arguments and results (the restricting factor
 812 being the )
 813
 814 \begin{code}
 815 isFFITy :: Type -> Bool
 816 -- True for any TyCon that can possibly be an arg or result of an FFI call
 817 isFFITy ty = checkRepTyCon legalFFITyCon ty
 818
 819 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
 820 -- Checks for valid argument type for a 'foreign import'
 821 isFFIArgumentTy dflags safety ty
 822    = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
 823
 824 isFFIExternalTy :: Type -> Bool
 825 -- Types that are allowed as arguments of a 'foreign export'
 826 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
 827
 828 isFFIImportResultTy :: DynFlags -> Type -> Bool
 829 isFFIImportResultTy dflags ty
 830   = checkRepTyCon (legalFIResultTyCon dflags) ty
 831
 832 isFFIExportResultTy :: Type -> Bool
 833 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
 834
 835 isFFIDynArgumentTy :: Type -> Bool
 836 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
 837 -- or a newtype of either.
 838 isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
 839
 840 isFFIDynResultTy :: Type -> Bool
 841 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
 842 -- or a newtype of either.
 843 isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
 844
 845 isFFILabelTy :: Type -> Bool
 846 -- The type of a foreign label must be Ptr, FunPtr, Addr,
 847 -- or a newtype of either.
 848 isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
 849
 850 isFFIDotnetTy :: DynFlags -> Type -> Bool
 851 isFFIDotnetTy dflags ty
 852   = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
 853                            (legalFIResultTyCon dflags tc ||
 854                            isFFIDotnetObjTy ty || isStringTy ty)) ty
 855
 856 -- Support String as an argument or result from a .NET FFI call.
 857 isStringTy ty =
 858   case tcSplitTyConApp_maybe (repType ty) of
 859     Just (tc, [arg_ty])
 860       | tc == listTyCon ->
 861         case tcSplitTyConApp_maybe (repType arg_ty) of
 862           Just (cc,[]) -> cc == charTyCon
 863           _ -> False
 864     _ -> False
 865
 866 -- Support String as an argument or result from a .NET FFI call.
 867 isFFIDotnetObjTy ty =
 868   let
 869    (_, t_ty) = tcSplitForAllTys ty
 870   in
 871   case tcSplitTyConApp_maybe (repType t_ty) of
 872     Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
 873     _ -> False
 874
 875 toDNType :: Type -> DNType
 876 toDNType ty
 877   | isStringTy ty = DNString
 878   | isFFIDotnetObjTy ty = DNObject
 879   | Just (tc,argTys) <- tcSplitTyConApp_maybe ty =
 880      case lookup (getUnique tc) dn_assoc of
 881        Just x  -> x
 882        Nothing
 883          | tc `hasKey` ioTyConKey -> toDNType (head argTys)
 884          | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
 885     where
 886       dn_assoc :: [ (Unique, DNType) ]
 887       dn_assoc = [ (unitTyConKey,   DNUnit)
 888                  , (intTyConKey,    DNInt)
 889                  , (int8TyConKey,   DNInt8)
 890                  , (int16TyConKey,  DNInt16)
 891                  , (int32TyConKey,  DNInt32)
 892                  , (int64TyConKey,  DNInt64)
 893                  , (wordTyConKey,   DNInt)
 894                  , (word8TyConKey,  DNWord8)
 895                  , (word16TyConKey, DNWord16)
 896                  , (word32TyConKey, DNWord32)
 897                  , (word64TyConKey, DNWord64)
 898                  , (floatTyConKey,  DNFloat)
 899                  , (doubleTyConKey, DNDouble)
 900                  , (addrTyConKey,   DNPtr)
 901                  , (ptrTyConKey,    DNPtr)
 902                  , (funPtrTyConKey, DNPtr)
 903                  , (charTyConKey,   DNChar)
 904                  , (boolTyConKey,   DNBool)
 905                  ]
 906
 907 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
 908         -- Look through newtypes
 909         -- Non-recursive ones are transparent to splitTyConApp,
 910         -- but recursive ones aren't.  Manuel had:
 911         --      newtype T = MkT (Ptr T)
 912         -- and wanted it to work...
 913 checkRepTyCon check_tc ty
 914   | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
 915   | otherwise                                       = False
 916
 917 checkRepTyConKey :: [Unique] -> Type -> Bool
 918 -- Like checkRepTyCon, but just looks at the TyCon key
 919 checkRepTyConKey keys
 920   = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
 921 \end{code}
 922
 923 ----------------------------------------------
 924 These chaps do the work; they are not exported
 925 ----------------------------------------------
 926
 927 \begin{code}
 928 legalFEArgTyCon :: TyCon -> Bool
 929 -- It's illegal to return foreign objects and (mutable)
 930 -- bytearrays from a _ccall_ / foreign declaration
 931 -- (or be passed them as arguments in foreign exported functions).
 932 legalFEArgTyCon tc
 933   | isByteArrayLikeTyCon tc
 934   = False
 935   -- It's also illegal to make foreign exports that take unboxed
 936   -- arguments.  The RTS API currently can't invoke such things.  --SDM 7/2000
 937   | otherwise
 938   = boxedMarshalableTyCon tc
 939
 940 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
 941 legalFIResultTyCon dflags tc
 942   | isByteArrayLikeTyCon tc = False
 943   | tc == unitTyCon         = True
 944   | otherwise               = marshalableTyCon dflags tc
 945
 946 legalFEResultTyCon :: TyCon -> Bool
 947 legalFEResultTyCon tc
 948   | isByteArrayLikeTyCon tc = False
 949   | tc == unitTyCon         = True
 950   | otherwise               = boxedMarshalableTyCon tc
 951
 952 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
 953 -- Checks validity of types going from Haskell -> external world
 954 legalOutgoingTyCon dflags safety tc
 955   | playSafe safety && isByteArrayLikeTyCon tc
 956   = False
 957   | otherwise
 958   = marshalableTyCon dflags tc
 959
 960 legalFFITyCon :: TyCon -> Bool
 961 -- True for any TyCon that can possibly be an arg or result of an FFI call
 962 legalFFITyCon tc
 963   = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
 964
 965 marshalableTyCon dflags tc
 966   =  (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
 967   || boxedMarshalableTyCon tc
 968
 969 boxedMarshalableTyCon tc
 970    = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
 971                          , int32TyConKey, int64TyConKey
 972                          , wordTyConKey, word8TyConKey, word16TyConKey
 973                          , word32TyConKey, word64TyConKey
 974                          , floatTyConKey, doubleTyConKey
 975                          , addrTyConKey, ptrTyConKey, funPtrTyConKey
 976                          , charTyConKey
 977                          , stablePtrTyConKey
 978                          , byteArrayTyConKey, mutableByteArrayTyConKey
 979                          , boolTyConKey
 980                          ]
 981
 982 isByteArrayLikeTyCon :: TyCon -> Bool
 983 isByteArrayLikeTyCon tc =
 984   getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
 985 \end{code}
 986
 987