ghc/compiler/types/Type.lhs

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