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