ghc/compiler/types/Type.lhs

   1 \begin{code}
   2 module Type (
   3         Type(..), TyNote(..),           -- Representation visible to friends
   4         Kind, TyVarSubst,
   5
   6         superKind, superBoxity,                         -- :: SuperKind
   7
   8         boxedKind,                                      -- :: Kind :: BX
   9         anyBoxKind,                                     -- :: Kind :: BX
  10         typeCon,                                        -- :: KindCon :: BX -> KX
  11         anyBoxCon,                                      -- :: KindCon :: BX
  12
  13         boxedTypeKind, unboxedTypeKind, openTypeKind,   -- Kind :: superKind
  14
  15         mkArrowKind, mkArrowKinds, hasMoreBoxityInfo,
  16
  17         funTyCon,
  18
  19         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
  20
  21         mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
  22
  23         mkFunTy, mkFunTys, splitFunTy_maybe, splitFunTys, funResultTy,
  24         zipFunTys,
  25
  26         mkTyConApp, mkTyConTy, splitTyConApp_maybe,
  27         splitAlgTyConApp_maybe, splitAlgTyConApp,
  28         mkDictTy, splitDictTy_maybe, isDictTy,
  29
  30         mkSynTy, isSynTy, deNoteType,
  31
  32         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
  33         applyTy, applyTys, isForAllTy,
  34         mkPiType,
  35
  36         TauType, RhoType, SigmaType, ThetaType,
  37         isTauTy,
  38         mkRhoTy, splitRhoTy,
  39         mkSigmaTy, splitSigmaTy,
  40
  41         -- Lifting and boxity
  42         isUnLiftedType, isUnboxedType, isUnboxedTupleType, isAlgType, isDataType,
  43         typePrimRep,
  44
  45         -- Free variables
  46         tyVarsOfType, tyVarsOfTypes, namesOfType, typeKind,
  47         addFreeTyVars,
  48
  49         -- Substitution
  50         substTy, substTheta, fullSubstTy, substTyVar,
  51         substTopTy, substTopTheta,
  52
  53         -- Tidying up for printing
  54         tidyType,     tidyTypes,
  55         tidyOpenType, tidyOpenTypes,
  56         tidyTyVar,    tidyTyVars,
  57         tidyTopType
  58     ) where
  59
  60 #include "HsVersions.h"
  61
  62 import {-# SOURCE #-}   DataCon( DataCon )
  63 import {-# SOURCE #-}   PprType( pprType )      -- Only called in debug messages
  64
  65 -- friends:
  66 import Var      ( Id, TyVar, IdOrTyVar,
  67                   tyVarKind, isId, idType, setVarOcc
  68                 )
  69 import VarEnv
  70 import VarSet
  71
  72 import Name     ( NamedThing(..), Provenance(..), ExportFlag(..),
  73                   mkWiredInTyConName, mkGlobalName, tcOcc,
  74                   tidyOccName, TidyOccEnv
  75                 )
  76 import NameSet
  77 import Class    ( classTyCon, Class )
  78 import TyCon    ( TyCon, KindCon,
  79                   mkFunTyCon, mkKindCon, mkSuperKindCon,
  80                   matchesTyCon, isUnboxedTupleTyCon, isUnLiftedTyCon,
  81                   isFunTyCon, isDataTyCon,
  82                   isAlgTyCon, isSynTyCon, tyConArity,
  83                   tyConKind, tyConDataCons, getSynTyConDefn,
  84                   tyConPrimRep, tyConClass_maybe
  85                 )
  86
  87 -- others
  88 import BasicTypes       ( Unused )
  89 import SrcLoc           ( mkBuiltinSrcLoc )
  90 import PrelMods         ( pREL_GHC )
  91 import Maybes           ( maybeToBool )
  92 import PrimRep          ( PrimRep(..), isFollowableRep )
  93 import Unique           -- quite a few *Keys
  94 import Util             ( thenCmp, mapAccumL )
  95 import Outputable
  96
  97 \end{code}
  98
  99 %************************************************************************
 100 %*                                                                      *
 101 \subsection{Type Classifications}
 102 %*                                                                      *
 103 %************************************************************************
 104
 105 A type is
 106
 107         *unboxed*       iff its representation is other than a pointer
 108                         Unboxed types cannot instantiate a type variable
 109                         Unboxed types are always unlifted.
 110
 111         *lifted*        A type is lifted iff it has bottom as an element.
 112                         Closures always have lifted types:  i.e. any
 113                         let-bound identifier in Core must have a lifted
 114                         type.  Operationally, a lifted object is one that
 115                         can be entered.
 116                         (NOTE: previously "pointed").
 117
 118         *algebraic*     A type with one or more constructors, whether declared
 119                         with "data" or "newtype".
 120                         An algebraic type is one that can be deconstructed
 121                         with a case expression.
 122
 123                         *NOT* the same as lifted types,  because we also
 124                         include unboxed tuples in this classification.
 125
 126         *data*          A type declared with "data".  Also boxed tuples.
 127
 128         *primitive*     iff it is a built-in type that can't be expressed
 129                         in Haskell.
 130
 131 Currently, all primitive types are unlifted, but that's not necessarily
 132 the case.  (E.g. Int could be primitive.)
 133
 134 Some primitive types are unboxed, such as Int#, whereas some are boxed
 135 but unlifted (such as ByteArray#).  The only primitive types that we
 136 classify as algebraic are the unboxed tuples.
 137
 138 examples of type classifications:
 139
 140 Type            primitive       boxed           lifted          algebraic
 141 -----------------------------------------------------------------------------
 142 Int#,           Yes             No              No              No
 143 ByteArray#      Yes             Yes             No              No
 144 (# a, b #)      Yes             No              No              Yes
 145 (  a, b  )      No              Yes             Yes             Yes
 146 [a]             No              Yes             Yes             Yes
 147
 148 %************************************************************************
 149 %*                                                                      *
 150 \subsection{The data type}
 151 %*                                                                      *
 152 %************************************************************************
 153
 154
 155 \begin{code}
 156 type SuperKind = Type
 157 type Kind      = Type
 158
 159 type TyVarSubst          = TyVarEnv Type
 160
 161 data Type
 162   = TyVarTy TyVar
 163
 164   | AppTy
 165         Type            -- Function is *not* a TyConApp
 166         Type
 167
 168   | TyConApp                    -- Application of a TyCon
 169         TyCon                   -- *Invariant* saturated appliations of FunTyCon and
 170                                 --      synonyms have their own constructors, below.
 171         [Type]          -- Might not be saturated.
 172
 173   | FunTy                       -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 174         Type
 175         Type
 176
 177   | NoteTy                      -- Saturated application of a type synonym
 178         TyNote
 179         Type            -- The expanded version
 180
 181   | ForAllTy
 182         TyVar
 183         Type            -- TypeKind
 184
 185 data TyNote
 186   = SynNote Type        -- The unexpanded version of the type synonym; always a TyConApp
 187   | FTVNote TyVarSet    -- The free type variables of the noted expression
 188 \end{code}
 189
 190
 191 %************************************************************************
 192 %*                                                                      *
 193 \subsection{Kinds}
 194 %*                                                                      *
 195 %************************************************************************
 196
 197 Kinds
 198 ~~~~~
 199 k::K = Type bx
 200      | k -> k
 201      | kv
 202
 203 kv :: KX is a kind variable
 204
 205 Type :: BX -> KX
 206
 207 bx::BX = Boxed
 208       |  Unboxed
 209       |  AnyBox         -- Used *only* for special built-in things
 210                         -- like error :: forall (a::*?). String -> a
 211                         -- Here, the 'a' can be instantiated to a boxed or
 212                         -- unboxed type.
 213       |  bv
 214
 215 bxv :: BX is a boxity variable
 216
 217 sk = KX         -- A kind
 218    | BX         -- A boxity
 219    | sk -> sk   -- In ptic (BX -> KX)
 220
 221 \begin{code}
 222 mk_kind_name key str = mkGlobalName key pREL_GHC (tcOcc str)
 223                                     (LocalDef mkBuiltinSrcLoc NotExported)
 224         -- mk_kind_name is a bit of a hack
 225         -- The LocalDef means that we print the name without
 226         -- a qualifier, which is what we want for these kinds.
 227         -- It's used for both Kinds and Boxities
 228 \end{code}
 229
 230 Define KX, BX.
 231
 232 \begin{code}
 233 superKind :: SuperKind          -- KX, the type of all kinds
 234 superKindName = mk_kind_name kindConKey SLIT("KX")
 235 superKind = TyConApp (mkSuperKindCon superKindName) []
 236
 237 superBoxity :: SuperKind                -- BX, the type of all boxities
 238 superBoxityName = mk_kind_name boxityConKey SLIT("BX")
 239 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 240 \end{code}
 241
 242 Define Boxed, Unboxed, AnyBox
 243
 244 \begin{code}
 245 boxedKind, unboxedKind, anyBoxKind :: Kind      -- Of superkind superBoxity
 246
 247 boxedConName = mk_kind_name boxedConKey SLIT("*")
 248 boxedKind    = TyConApp (mkKindCon boxedConName superBoxity) []
 249
 250 unboxedConName = mk_kind_name unboxedConKey SLIT("#")
 251 unboxedKind    = TyConApp (mkKindCon unboxedConName superBoxity) []
 252
 253 anyBoxConName = mk_kind_name anyBoxConKey SLIT("?")
 254 anyBoxCon     = mkKindCon anyBoxConName superBoxity     -- A kind of wild card
 255 anyBoxKind    = TyConApp anyBoxCon []
 256 \end{code}
 257
 258 Define Type
 259
 260 \begin{code}
 261 typeCon :: KindCon
 262 typeConName = mk_kind_name typeConKey SLIT("Type")
 263 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 264 \end{code}
 265
 266 Define (Type Boxed), (Type Unboxed), (Type AnyBox)
 267
 268 \begin{code}
 269 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind
 270 boxedTypeKind   = TyConApp typeCon [boxedKind]
 271 unboxedTypeKind = TyConApp typeCon [unboxedKind]
 272 openTypeKind    = TyConApp typeCon [anyBoxKind]
 273
 274 mkArrowKind :: Kind -> Kind -> Kind
 275 mkArrowKind k1 k2 = k1 `FunTy` k2
 276
 277 mkArrowKinds :: [Kind] -> Kind -> Kind
 278 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 279 \end{code}
 280
 281 \begin{code}
 282 hasMoreBoxityInfo :: Kind -> Kind -> Bool
 283 hasMoreBoxityInfo k1 k2
 284   | k2 == openTypeKind = ASSERT( is_type_kind k1) True
 285   | otherwise          = k1 == k2
 286   where
 287         -- Returns true for things of form (Type x)
 288     is_type_kind k = case splitTyConApp_maybe k of
 289                         Just (tc,[_]) -> tc == typeCon
 290                         Nothing       -> False
 291 \end{code}
 292
 293
 294 %************************************************************************
 295 %*                                                                      *
 296 \subsection{Wired-in type constructors
 297 %*                                                                      *
 298 %************************************************************************
 299
 300 We define a few wired-in type constructors here to avoid module knots
 301
 302 \begin{code}
 303 funTyConName = mkWiredInTyConName funTyConKey pREL_GHC SLIT("->") funTyCon
 304 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
 305 \end{code}
 306
 307
 308
 309 %************************************************************************
 310 %*                                                                      *
 311 \subsection{Constructor-specific functions}
 312 %*                                                                      *
 313 %************************************************************************
 314
 315
 316 ---------------------------------------------------------------------
 317                                 TyVarTy
 318                                 ~~~~~~~
 319 \begin{code}
 320 mkTyVarTy  :: TyVar   -> Type
 321 mkTyVarTy  = TyVarTy
 322
 323 mkTyVarTys :: [TyVar] -> [Type]
 324 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
 325
 326 getTyVar :: String -> Type -> TyVar
 327 getTyVar msg (TyVarTy tv) = tv
 328 getTyVar msg (NoteTy _ t) = getTyVar msg t
 329 getTyVar msg other        = panic ("getTyVar: " ++ msg)
 330
 331 getTyVar_maybe :: Type -> Maybe TyVar
 332 getTyVar_maybe (TyVarTy tv) = Just tv
 333 getTyVar_maybe (NoteTy _ t) = getTyVar_maybe t
 334 getTyVar_maybe other        = Nothing
 335
 336 isTyVarTy :: Type -> Bool
 337 isTyVarTy (TyVarTy tv)  = True
 338 isTyVarTy (NoteTy _ ty) = isTyVarTy ty
 339 isTyVarTy other         = False
 340 \end{code}
 341
 342
 343 ---------------------------------------------------------------------
 344                                 AppTy
 345                                 ~~~~~
 346 We need to be pretty careful with AppTy to make sure we obey the
 347 invariant that a TyConApp is always visibly so.  mkAppTy maintains the
 348 invariant: use it.
 349
 350 \begin{code}
 351 mkAppTy orig_ty1 orig_ty2 = mk_app orig_ty1
 352   where
 353     mk_app (NoteTy _ ty1)    = mk_app ty1
 354     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
 355     mk_app ty1               = AppTy orig_ty1 orig_ty2
 356
 357 mkAppTys :: Type -> [Type] -> Type
 358 mkAppTys orig_ty1 []        = orig_ty1
 359         -- This check for an empty list of type arguments
 360         -- avoids the needless of a type synonym constructor.
 361         -- For example: mkAppTys Rational []
 362         --   returns to (Ratio Integer), which has needlessly lost
 363         --   the Rational part.
 364 mkAppTys orig_ty1 orig_tys2 = mk_app orig_ty1
 365   where
 366     mk_app (NoteTy _ ty1)    = mk_app ty1
 367     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
 368     mk_app ty1               = foldl AppTy orig_ty1 orig_tys2
 369
 370 splitAppTy_maybe :: Type -> Maybe (Type, Type)
 371 splitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 372 splitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 373 splitAppTy_maybe (NoteTy _ ty)     = splitAppTy_maybe ty
 374 splitAppTy_maybe (TyConApp tc [])  = Nothing
 375 splitAppTy_maybe (TyConApp tc tys) = split tys []
 376                             where
 377                                split [ty2]    acc = Just (TyConApp tc (reverse acc), ty2)
 378                                split (ty:tys) acc = split tys (ty:acc)
 379
 380 splitAppTy_maybe other            = Nothing
 381
 382 splitAppTy :: Type -> (Type, Type)
 383 splitAppTy ty = case splitAppTy_maybe ty of
 384                         Just pr -> pr
 385                         Nothing -> panic "splitAppTy"
 386
 387 splitAppTys :: Type -> (Type, [Type])
 388 splitAppTys ty = split ty ty []
 389   where
 390     split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
 391     split orig_ty (NoteTy _ ty)         args = split orig_ty ty args
 392     split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
 393                                                (TyConApp funTyCon [], [ty1,ty2])
 394     split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
 395     split orig_ty ty                    args = (orig_ty, args)
 396 \end{code}
 397
 398
 399 ---------------------------------------------------------------------
 400                                 FunTy
 401                                 ~~~~~
 402
 403 \begin{code}
 404 mkFunTy :: Type -> Type -> Type
 405 mkFunTy arg res = FunTy arg res
 406
 407 mkFunTys :: [Type] -> Type -> Type
 408 mkFunTys tys ty = foldr FunTy ty tys
 409
 410 splitFunTy_maybe :: Type -> Maybe (Type, Type)
 411 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
 412 splitFunTy_maybe (NoteTy _ ty)   = splitFunTy_maybe ty
 413 splitFunTy_maybe other           = Nothing
 414
 415
 416 splitFunTys :: Type -> ([Type], Type)
 417 splitFunTys ty = split [] ty ty
 418   where
 419     split args orig_ty (FunTy arg res) = split (arg:args) res res
 420     split args orig_ty (NoteTy _ ty)   = split args orig_ty ty
 421     split args orig_ty ty              = (reverse args, orig_ty)
 422
 423 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
 424 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
 425   where
 426     split acc []     nty ty              = (reverse acc, nty)
 427     split acc (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res
 428     split acc xs     nty (NoteTy _ ty)   = split acc           xs nty ty
 429     split acc (x:xs) nty ty              = pprPanic "zipFunTys" (ppr orig_xs <+> pprType orig_ty)
 430
 431 funResultTy :: Type -> Type
 432 funResultTy (FunTy arg res) = res
 433 funResultTy (NoteTy _ ty)   = funResultTy ty
 434 funResultTy ty              = pprPanic "funResultTy" (pprType ty)
 435 \end{code}
 436
 437
 438
 439 ---------------------------------------------------------------------
 440                                 TyConApp
 441                                 ~~~~~~~~
 442
 443 \begin{code}
 444 mkTyConApp :: TyCon -> [Type] -> Type
 445 mkTyConApp tycon tys
 446   | isFunTyCon tycon && length tys == 2
 447   = case tys of
 448         (ty1:ty2:_) -> FunTy ty1 ty2
 449
 450   | otherwise
 451   = ASSERT(not (isSynTyCon tycon))
 452     TyConApp tycon tys
 453
 454 mkTyConTy :: TyCon -> Type
 455 mkTyConTy tycon = ASSERT( not (isSynTyCon tycon) )
 456                   TyConApp tycon []
 457
 458 -- splitTyConApp "looks through" synonyms, because they don't
 459 -- mean a distinct type, but all other type-constructor applications
 460 -- including functions are returned as Just ..
 461
 462 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 463 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 464 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
 465 splitTyConApp_maybe (NoteTy _ ty)     = splitTyConApp_maybe ty
 466 splitTyConApp_maybe other             = Nothing
 467
 468 -- splitAlgTyConApp_maybe looks for
 469 --      *saturated* applications of *algebraic* data types
 470 -- "Algebraic" => newtype, data type, or dictionary (not function types)
 471 -- We return the constructors too.
 472
 473 splitAlgTyConApp_maybe :: Type -> Maybe (TyCon, [Type], [DataCon])
 474 splitAlgTyConApp_maybe (TyConApp tc tys)
 475   | isAlgTyCon tc &&
 476     tyConArity tc == length tys      = Just (tc, tys, tyConDataCons tc)
 477 splitAlgTyConApp_maybe (NoteTy _ ty) = splitAlgTyConApp_maybe ty
 478 splitAlgTyConApp_maybe other         = Nothing
 479
 480 splitAlgTyConApp :: Type -> (TyCon, [Type], [DataCon])
 481         -- Here the "algebraic" property is an *assertion*
 482 splitAlgTyConApp (TyConApp tc tys) = ASSERT( isAlgTyCon tc && tyConArity tc == length tys )
 483                                      (tc, tys, tyConDataCons tc)
 484 splitAlgTyConApp (NoteTy _ ty)     = splitAlgTyConApp ty
 485 \end{code}
 486
 487 "Dictionary" types are just ordinary data types, but you can
 488 tell from the type constructor whether it's a dictionary or not.
 489
 490 \begin{code}
 491 mkDictTy :: Class -> [Type] -> Type
 492 mkDictTy clas tys = TyConApp (classTyCon clas) tys
 493
 494 splitDictTy_maybe :: Type -> Maybe (Class, [Type])
 495 splitDictTy_maybe (TyConApp tc tys)
 496   |  maybeToBool maybe_class
 497   && tyConArity tc == length tys = Just (clas, tys)
 498   where
 499      maybe_class = tyConClass_maybe tc
 500      Just clas   = maybe_class
 501
 502 splitDictTy_maybe (NoteTy _ ty) = splitDictTy_maybe ty
 503 splitDictTy_maybe other         = Nothing
 504
 505 isDictTy :: Type -> Bool
 506         -- This version is slightly more efficient than (maybeToBool . splitDictTy)
 507 isDictTy (TyConApp tc tys)
 508   |  maybeToBool (tyConClass_maybe tc)
 509   && tyConArity tc == length tys
 510   = True
 511 isDictTy (NoteTy _ ty)  = isDictTy ty
 512 isDictTy other          = False
 513 \end{code}
 514
 515
 516 ---------------------------------------------------------------------
 517                                 SynTy
 518                                 ~~~~~
 519
 520 \begin{code}
 521 mkSynTy syn_tycon tys
 522   = ASSERT(isSynTyCon syn_tycon)
 523     NoteTy (SynNote (TyConApp syn_tycon tys))
 524            (substTopTy (zipVarEnv tyvars tys) body)
 525   where
 526     (tyvars, body) = getSynTyConDefn syn_tycon
 527
 528 isSynTy (NoteTy (SynNote _) _) = True
 529 isSynTy other                  = False
 530
 531 deNoteType :: Type -> Type
 532         -- Sorry for the cute name
 533 deNoteType ty@(TyVarTy tyvar)   = ty
 534 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
 535 deNoteType (NoteTy _ ty)        = deNoteType ty
 536 deNoteType (AppTy fun arg)      = AppTy (deNoteType fun) (deNoteType arg)
 537 deNoteType (FunTy fun arg)      = FunTy (deNoteType fun) (deNoteType arg)
 538 deNoteType (ForAllTy tv ty)     = ForAllTy tv (deNoteType ty)
 539 \end{code}
 540
 541 Notes on type synonyms
 542 ~~~~~~~~~~~~~~~~~~~~~~
 543 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
 544 to return type synonyms whereever possible. Thus
 545
 546         type Foo a = a -> a
 547
 548 we want
 549         splitFunTys (a -> Foo a) = ([a], Foo a)
 550 not                                ([a], a -> a)
 551
 552 The reason is that we then get better (shorter) type signatures in
 553 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
 554
 555
 556
 557
 558 ---------------------------------------------------------------------
 559                                 ForAllTy
 560                                 ~~~~~~~~
 561
 562 \begin{code}
 563 mkForAllTy = ForAllTy
 564
 565 mkForAllTys :: [TyVar] -> Type -> Type
 566 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 567
 568 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
 569 splitForAllTy_maybe (NoteTy _ ty)       = splitForAllTy_maybe ty
 570 splitForAllTy_maybe (ForAllTy tyvar ty) = Just(tyvar, ty)
 571 splitForAllTy_maybe _                   = Nothing
 572
 573 isForAllTy :: Type -> Bool
 574 isForAllTy (NoteTy _ ty)       = isForAllTy ty
 575 isForAllTy (ForAllTy tyvar ty) = True
 576 isForAllTy _                 = False
 577
 578 splitForAllTys :: Type -> ([TyVar], Type)
 579 splitForAllTys ty = split ty ty []
 580    where
 581      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
 582      split orig_ty (NoteTy _ ty)    tvs = split orig_ty ty tvs
 583      split orig_ty t                tvs = (reverse tvs, orig_ty)
 584 \end{code}
 585
 586 @mkPiType@ makes a (->) type or a forall type, depending on whether
 587 it is given a type variable or a term variable.
 588
 589 \begin{code}
 590 mkPiType :: IdOrTyVar -> Type -> Type   -- The more polymorphic version doesn't work...
 591 mkPiType v ty | isId v    = mkFunTy (idType v) ty
 592               | otherwise = ForAllTy v ty
 593 \end{code}
 594
 595 \begin{code}
 596 applyTy :: Type -> Type -> Type
 597 applyTy (NoteTy _ fun)   arg = applyTy fun arg
 598 applyTy (ForAllTy tv ty) arg = substTy (mkVarEnv [(tv,arg)]) ty
 599 applyTy other            arg = panic "applyTy"
 600
 601 applyTys :: Type -> [Type] -> Type
 602 applyTys fun_ty arg_tys
 603  = go [] fun_ty arg_tys
 604  where
 605    go env ty               []         = substTy (mkVarEnv env) ty
 606    go env (NoteTy _ fun)   args       = go env fun args
 607    go env (ForAllTy tv ty) (arg:args) = go ((tv,arg):env) ty args
 608    go env other            args       = panic "applyTys"
 609 \end{code}
 610
 611
 612 %************************************************************************
 613 %*                                                                      *
 614 \subsection{Stuff to do with the source-language types}
 615 %*                                                                      *
 616 %************************************************************************
 617
 618 \begin{code}
 619 type RhoType   = Type
 620 type TauType   = Type
 621 type ThetaType = [(Class, [Type])]
 622 type SigmaType = Type
 623 \end{code}
 624
 625 @isTauTy@ tests for nested for-alls.
 626
 627 \begin{code}
 628 isTauTy :: Type -> Bool
 629 isTauTy (TyVarTy v)      = True
 630 isTauTy (TyConApp _ tys) = all isTauTy tys
 631 isTauTy (AppTy a b)      = isTauTy a && isTauTy b
 632 isTauTy (FunTy a b)      = isTauTy a && isTauTy b
 633 isTauTy (NoteTy _ ty)    = isTauTy ty
 634 isTauTy other            = False
 635 \end{code}
 636
 637 \begin{code}
 638 mkRhoTy :: [(Class, [Type])] -> Type -> Type
 639 mkRhoTy theta ty = foldr (\(c,t) r -> FunTy (mkDictTy c t) r) ty theta
 640
 641 splitRhoTy :: Type -> ([(Class, [Type])], Type)
 642 splitRhoTy ty = split ty ty []
 643  where
 644   split orig_ty (FunTy arg res) ts = case splitDictTy_maybe arg of
 645                                         Just pair -> split res res (pair:ts)
 646                                         Nothing   -> (reverse ts, orig_ty)
 647   split orig_ty (NoteTy _ ty) ts   = split orig_ty ty ts
 648   split orig_ty ty ts              = (reverse ts, orig_ty)
 649 \end{code}
 650
 651
 652
 653 \begin{code}
 654 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
 655
 656 splitSigmaTy :: Type -> ([TyVar], [(Class, [Type])], Type)
 657 splitSigmaTy ty =
 658   (tyvars, theta, tau)
 659  where
 660   (tyvars,rho) = splitForAllTys ty
 661   (theta,tau)  = splitRhoTy rho
 662 \end{code}
 663
 664
 665 %************************************************************************
 666 %*                                                                      *
 667 \subsection{Kinds and free variables}
 668 %*                                                                      *
 669 %************************************************************************
 670
 671 ---------------------------------------------------------------------
 672                 Finding the kind of a type
 673                 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 674 \begin{code}
 675 typeKind :: Type -> Kind
 676
 677 typeKind (TyVarTy tyvar)        = tyVarKind tyvar
 678 typeKind (TyConApp tycon tys)   = foldr (\_ k -> funResultTy k) (tyConKind tycon) tys
 679 typeKind (NoteTy _ ty)          = typeKind ty
 680 typeKind (AppTy fun arg)        = funResultTy (typeKind fun)
 681 typeKind (FunTy fun arg)        = typeKindF arg
 682 typeKind (ForAllTy _ ty)        = typeKindF ty  -- We could make this a new kind polyTypeKind
 683                                                 -- to prevent a forall type unifying with a
 684                                                 -- boxed type variable, but I didn't think it
 685                                                 -- was worth it yet.
 686
 687 -- The complication is that a *function* is boxed even if
 688 -- its *result* type is unboxed.  Seems wierd.
 689
 690 typeKindF :: Type -> Kind
 691 typeKindF (NoteTy _ ty)   = typeKindF ty
 692 typeKindF (FunTy _ ty)    = typeKindF ty
 693 typeKindF (ForAllTy _ ty) = typeKindF ty
 694 typeKindF other           = fix_up (typeKind other)
 695   where
 696     fix_up (TyConApp kc _) | kc == typeCon = boxedTypeKind
 697                 -- Functions at the type level are always boxed
 698     fix_up (NoteTy _ kind) = fix_up kind
 699     fix_up kind            = kind
 700 \end{code}
 701
 702
 703 ---------------------------------------------------------------------
 704                 Free variables of a type
 705                 ~~~~~~~~~~~~~~~~~~~~~~~~
 706 \begin{code}
 707 tyVarsOfType :: Type -> TyVarSet
 708
 709 tyVarsOfType (TyVarTy tv)               = unitVarSet tv
 710 tyVarsOfType (TyConApp tycon tys)       = tyVarsOfTypes tys
 711 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
 712 tyVarsOfType (NoteTy (SynNote ty1) ty2) = tyVarsOfType ty1
 713 tyVarsOfType (FunTy arg res)            = tyVarsOfType arg `unionVarSet` tyVarsOfType res
 714 tyVarsOfType (AppTy fun arg)            = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
 715 tyVarsOfType (ForAllTy tyvar ty)        = tyVarsOfType ty `minusVarSet` unitVarSet tyvar
 716
 717 tyVarsOfTypes :: [Type] -> TyVarSet
 718 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
 719
 720 -- Add a Note with the free tyvars to the top of the type
 721 addFreeTyVars :: Type -> Type
 722 addFreeTyVars ty@(NoteTy (FTVNote _) _) = ty
 723 addFreeTyVars ty                        = NoteTy (FTVNote (tyVarsOfType ty)) ty
 724
 725 -- Find the free names of a type, including the type constructors and classes it mentions
 726 namesOfType :: Type -> NameSet
 727 namesOfType (TyVarTy tv)                = unitNameSet (getName tv)
 728 namesOfType (TyConApp tycon tys)        = unitNameSet (getName tycon) `unionNameSets`
 729                                           namesOfTypes tys
 730 namesOfType (NoteTy (SynNote ty1) ty2)  = namesOfType ty1
 731 namesOfType (NoteTy other_note    ty2)  = namesOfType ty2
 732 namesOfType (FunTy arg res)             = namesOfType arg `unionNameSets` namesOfType res
 733 namesOfType (AppTy fun arg)             = namesOfType fun `unionNameSets` namesOfType arg
 734 namesOfType (ForAllTy tyvar ty)         = namesOfType ty `minusNameSet` unitNameSet (getName tyvar)
 735
 736 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
 737 \end{code}
 738
 739
 740 %************************************************************************
 741 %*                                                                      *
 742 \subsection{Instantiating a type}
 743 %*                                                                      *
 744 %************************************************************************
 745
 746 @substTy@ applies a substitution to a type.  It deals correctly with name capture.
 747
 748 \begin{code}
 749 substTy :: TyVarSubst -> Type -> Type
 750 substTy tenv ty
 751   | isEmptyVarEnv tenv = ty
 752   | otherwise          = subst_ty tenv tset ty
 753   where
 754     tset = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet tenv
 755                 -- If ty doesn't have any for-alls, then this thunk
 756                 -- will never be evaluated
 757
 758 substTheta :: TyVarSubst -> ThetaType -> ThetaType
 759 substTheta tenv theta
 760   | isEmptyVarEnv tenv = theta
 761   | otherwise          = [(clas, map (subst_ty tenv tset) tys) | (clas, tys) <- theta]
 762   where
 763     tset = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet tenv
 764                 -- If ty doesn't have any for-alls, then this thunk
 765                 -- will never be evaluated
 766
 767 substTopTy :: TyVarSubst -> Type -> Type
 768 substTopTy = substTy    -- Called when doing top-level substitutions.
 769                         -- Here we expect that the free vars of the range of the
 770                         -- substitution will be empty; but during typechecking I'm
 771                         -- a bit dubious about that (mutable tyvars bouund to Int, say)
 772                         -- So I've left it as substTy for the moment.  SLPJ Nov 98
 773 substTopTheta = substTheta
 774 \end{code}
 775
 776 @fullSubstTy@ is like @substTy@ except that it needs to be given a set
 777 of in-scope type variables.  In exchange it's a bit more efficient, at least
 778 if you happen to have that set lying around.
 779
 780 \begin{code}
 781 fullSubstTy :: TyVarSubst               -- Substitution to apply
 782             -> TyVarSet                 -- Superset of the free tyvars of
 783                                         -- the range of the tyvar env
 784             -> Type  -> Type
 785 -- ASSUMPTION: The substitution is idempotent.
 786 -- Equivalently: No tyvar is both in scope, and in the domain of the substitution.
 787 fullSubstTy tenv tset ty | isEmptyVarEnv tenv = ty
 788                          | otherwise          = subst_ty tenv tset ty
 789
 790 -- subst_ty does the business
 791 subst_ty tenv tset ty
 792    = go ty
 793   where
 794     go (TyConApp tc tys)           = TyConApp tc (map go tys)
 795     go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote (go ty1)) (go ty2)
 796     go (NoteTy (FTVNote _) ty2)    = go ty2             -- Discard the free tyvar note
 797     go (FunTy arg res)             = FunTy (go arg) (go res)
 798     go (AppTy fun arg)             = mkAppTy (go fun) (go arg)
 799     go ty@(TyVarTy tv)             = case (lookupVarEnv tenv tv) of
 800                                       Nothing  -> ty
 801                                       Just ty' -> ty'
 802     go (ForAllTy tv ty)            = case substTyVar tenv tset tv of
 803                                         (tenv', tset', tv') -> ForAllTy tv' (subst_ty tenv' tset' ty)
 804
 805 substTyVar ::  TyVarSubst -> TyVarSet -> TyVar
 806            -> (TyVarSubst,   TyVarSet,   TyVar)
 807
 808 substTyVar tenv tset tv
 809   | not (tv `elemVarSet` tset)  -- No need to clone
 810                                 -- But must delete from substitution
 811   = (tenv `delVarEnv` tv, tset `extendVarSet` tv, tv)
 812
 813   | otherwise   -- The forall's variable is in scope so
 814                 -- we'd better rename it away from the in-scope variables
 815                 -- Extending the substitution to do this renaming also
 816                 -- has the (correct) effect of discarding any existing
 817                 -- substitution for that variable
 818   = (extendVarEnv tenv tv (TyVarTy tv'), tset `extendVarSet` tv', tv')
 819   where
 820      tv' = uniqAway tset tv
 821 \end{code}
 822
 823
 824 %************************************************************************
 825 %*                                                                      *
 826 \subsection{TidyType}
 827 %*                                                                      *
 828 %************************************************************************
 829
 830 tidyTy tidies up a type for printing in an error message, or in
 831 an interface file.
 832
 833 It doesn't change the uniques at all, just the print names.
 834
 835 \begin{code}
 836 tidyTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 837 tidyTyVar env@(tidy_env, subst) tyvar
 838   = case lookupVarEnv subst tyvar of
 839
 840         Just tyvar' ->  -- Already substituted
 841                 (env, tyvar')
 842
 843         Nothing ->      -- Make a new nice name for it
 844
 845                 case tidyOccName tidy_env (getOccName tyvar) of
 846                     (tidy', occ') ->    -- New occname reqd
 847                                 ((tidy', subst'), tyvar')
 848                               where
 849                                 subst' = extendVarEnv subst tyvar tyvar'
 850                                 tyvar' = setVarOcc tyvar occ'
 851
 852 tidyTyVars env tyvars = mapAccumL tidyTyVar env tyvars
 853
 854 tidyType :: TidyEnv -> Type -> Type
 855 tidyType env@(tidy_env, subst) ty
 856   = go ty
 857   where
 858     go (TyVarTy tv)         = case lookupVarEnv subst tv of
 859                                 Nothing  -> TyVarTy tv
 860                                 Just tv' -> TyVarTy tv'
 861     go (TyConApp tycon tys) = TyConApp tycon (map go tys)
 862     go (NoteTy note ty)     = NoteTy (go_note note) (go ty)
 863     go (AppTy fun arg)      = AppTy (go fun) (go arg)
 864     go (FunTy fun arg)      = FunTy (go fun) (go arg)
 865     go (ForAllTy tv ty)     = ForAllTy tv' (tidyType env' ty)
 866                             where
 867                               (env', tv') = tidyTyVar env tv
 868
 869     go_note (SynNote ty)        = SynNote (go ty)
 870     go_note note@(FTVNote ftvs) = note  -- No need to tidy the free tyvars
 871
 872 tidyTypes  env tys    = map (tidyType env) tys
 873 \end{code}
 874
 875
 876 @tidyOpenType@ grabs the free type varibles, tidies them
 877 and then uses @tidyType@ to work over the type itself
 878
 879 \begin{code}
 880 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
 881 tidyOpenType env ty
 882   = (env', tidyType env' ty)
 883   where
 884     env'         = foldl go env (varSetElems (tyVarsOfType ty))
 885     go env tyvar = fst (tidyTyVar env tyvar)
 886
 887 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
 888 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
 889
 890 tidyTopType :: Type -> Type
 891 tidyTopType ty = tidyType emptyTidyEnv ty
 892 \end{code}
 893
 894
 895 %************************************************************************
 896 %*                                                                      *
 897 \subsection{Boxedness and liftedness}
 898 %*                                                                      *
 899 %************************************************************************
 900
 901 \begin{code}
 902 isUnboxedType :: Type -> Bool
 903 isUnboxedType ty = not (isFollowableRep (typePrimRep ty))
 904
 905 isUnLiftedType :: Type -> Bool
 906 isUnLiftedType ty = case splitTyConApp_maybe ty of
 907                            Just (tc, ty_args) -> isUnLiftedTyCon tc
 908                            other              -> False
 909
 910 isUnboxedTupleType :: Type -> Bool
 911 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
 912                            Just (tc, ty_args) -> isUnboxedTupleTyCon tc
 913                            other              -> False
 914
 915 -- Should only be applied to *types*; hence the assert
 916 isAlgType :: Type -> Bool
 917 isAlgType ty = case splitTyConApp_maybe ty of
 918                         Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
 919                                               isAlgTyCon tc
 920                         other              -> False
 921
 922 -- Should only be applied to *types*; hence the assert
 923 isDataType :: Type -> Bool
 924 isDataType ty = case splitTyConApp_maybe ty of
 925                         Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
 926                                               isDataTyCon tc
 927                         other              -> False
 928
 929 typePrimRep :: Type -> PrimRep
 930 typePrimRep ty = case splitTyConApp_maybe ty of
 931                    Just (tc, ty_args) -> tyConPrimRep tc
 932                    other              -> PtrRep
 933 \end{code}
 934
 935 %************************************************************************
 936 %*                                                                      *
 937 \subsection{Equality on types}
 938 %*                                                                      *
 939 %************************************************************************
 940
 941 For the moment at least, type comparisons don't work if
 942 there are embedded for-alls.
 943
 944 \begin{code}
 945 instance Eq Type where
 946   ty1 == ty2 = case ty1 `cmpTy` ty2 of { EQ -> True; other -> False }
 947
 948 instance Ord Type where
 949   compare ty1 ty2 = cmpTy ty1 ty2
 950
 951 cmpTy :: Type -> Type -> Ordering
 952 cmpTy ty1 ty2
 953   = cmp emptyVarEnv ty1 ty2
 954   where
 955   -- The "env" maps type variables in ty1 to type variables in ty2
 956   -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
 957   -- we in effect substitute tv2 for tv1 in t1 before continuing
 958     lookup env tv1 = case lookupVarEnv env tv1 of
 959                           Just tv2 -> tv2
 960                           Nothing  -> tv1
 961
 962     -- Get rid of NoteTy
 963     cmp env (NoteTy _ ty1) ty2 = cmp env ty1 ty2
 964     cmp env ty1 (NoteTy _ ty2) = cmp env ty1 ty2
 965
 966     -- Deal with equal constructors
 967     cmp env (TyVarTy tv1) (TyVarTy tv2) = lookup env tv1 `compare` tv2
 968     cmp env (AppTy f1 a1) (AppTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
 969     cmp env (FunTy f1 a1) (FunTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
 970     cmp env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmps env tys1 tys2)
 971     cmp env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmp (extendVarEnv env tv1 tv2) t1 t2
 972
 973     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy
 974     cmp env (AppTy _ _) (TyVarTy _) = GT
 975
 976     cmp env (FunTy _ _) (TyVarTy _) = GT
 977     cmp env (FunTy _ _) (AppTy _ _) = GT
 978
 979     cmp env (TyConApp _ _) (TyVarTy _) = GT
 980     cmp env (TyConApp _ _) (AppTy _ _) = GT
 981     cmp env (TyConApp _ _) (FunTy _ _) = GT
 982
 983     cmp env (ForAllTy _ _) other       = GT
 984
 985     cmp env _ _                        = LT
 986
 987     cmps env []     [] = EQ
 988     cmps env (t:ts) [] = GT
 989     cmps env [] (t:ts) = LT
 990     cmps env (t1:t1s) (t2:t2s) = cmp env t1 t2 `thenCmp` cmps env t1s t2s
 991 \end{code}
 992
 993