ghc/compiler/types/TypeRep.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
   3 %
   4 \section[TypeRep]{Type - friends' interface}
   5
   6 \begin{code}
   7 module TypeRep (
   8         TyThing(..),
   9         Type(..), TyNote(..),           -- Representation visible
  10         PredType(..),                   -- to friends
  11
  12         Kind, ThetaType,                -- Synonyms
  13         TyVarSubst,
  14
  15         superKind, superBoxity,                         -- KX and BX respectively
  16         liftedBoxity, unliftedBoxity,                   -- :: BX
  17         openKindCon,                                    -- :: KX
  18         typeCon,                                        -- :: BX -> KX
  19         liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
  20         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
  21         mkArrowKind, mkArrowKinds,                      -- :: KX -> KX -> KX
  22
  23         funTyCon,
  24
  25         -- Pretty-printing
  26         pprKind, pprParendKind,
  27         pprType, pprParendType,
  28         pprPred, pprTheta, pprThetaArrow, pprClassPred
  29     ) where
  30
  31 #include "HsVersions.h"
  32
  33 import {-# SOURCE #-} DataCon( DataCon, dataConName )
  34
  35 -- friends:
  36 import Var        ( Id, TyVar, tyVarKind )
  37 import VarEnv     ( TyVarEnv )
  38 import VarSet     ( TyVarSet )
  39 import Name       ( Name, NamedThing(..), mkWiredInName, mkInternalName )
  40 import OccName    ( mkOccFS, mkKindOccFS, tcName )
  41 import BasicTypes ( IPName, tupleParens )
  42 import TyCon      ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon, isNewTyCon,
  43                     tyConArity, tupleTyConBoxity, isTupleTyCon, tyConName )
  44 import Class      ( Class )
  45
  46 -- others
  47 import PrelNames        ( gHC_PRIM, kindConKey, boxityConKey, liftedConKey,
  48                           unliftedConKey, typeConKey, anyBoxConKey,
  49                           funTyConKey, listTyConKey, parrTyConKey,
  50                           hasKey
  51                         )
  52 import SrcLoc           ( noSrcLoc )
  53 import Outputable
  54 \end{code}
  55
  56 %************************************************************************
  57 %*                                                                      *
  58 \subsection{Type Classifications}
  59 %*                                                                      *
  60 %************************************************************************
  61
  62 A type is
  63
  64         *unboxed*       iff its representation is other than a pointer
  65                         Unboxed types are also unlifted.
  66
  67         *lifted*        A type is lifted iff it has bottom as an element.
  68                         Closures always have lifted types:  i.e. any
  69                         let-bound identifier in Core must have a lifted
  70                         type.  Operationally, a lifted object is one that
  71                         can be entered.
  72
  73                         Only lifted types may be unified with a type variable.
  74
  75         *algebraic*     A type with one or more constructors, whether declared
  76                         with "data" or "newtype".
  77                         An algebraic type is one that can be deconstructed
  78                         with a case expression.
  79                         *NOT* the same as lifted types,  because we also
  80                         include unboxed tuples in this classification.
  81
  82         *data*          A type declared with "data".  Also boxed tuples.
  83
  84         *primitive*     iff it is a built-in type that can't be expressed
  85                         in Haskell.
  86
  87 Currently, all primitive types are unlifted, but that's not necessarily
  88 the case.  (E.g. Int could be primitive.)
  89
  90 Some primitive types are unboxed, such as Int#, whereas some are boxed
  91 but unlifted (such as ByteArray#).  The only primitive types that we
  92 classify as algebraic are the unboxed tuples.
  93
  94 examples of type classifications:
  95
  96 Type            primitive       boxed           lifted          algebraic
  97 -----------------------------------------------------------------------------
  98 Int#,           Yes             No              No              No
  99 ByteArray#      Yes             Yes             No              No
 100 (# a, b #)      Yes             No              No              Yes
 101 (  a, b  )      No              Yes             Yes             Yes
 102 [a]             No              Yes             Yes             Yes
 103
 104
 105
 106         ----------------------
 107         A note about newtypes
 108         ----------------------
 109
 110 Consider
 111         newtype N = MkN Int
 112
 113 Then we want N to be represented as an Int, and that's what we arrange.
 114 The front end of the compiler [TcType.lhs] treats N as opaque,
 115 the back end treats it as transparent [Type.lhs].
 116
 117 There's a bit of a problem with recursive newtypes
 118         newtype P = MkP P
 119         newtype Q = MkQ (Q->Q)
 120
 121 Here the 'implicit expansion' we get from treating P and Q as transparent
 122 would give rise to infinite types, which in turn makes eqType diverge.
 123 Similarly splitForAllTys and splitFunTys can get into a loop.
 124
 125 Solution:
 126
 127 * Newtypes are always represented using NewTcApp, never as TyConApp.
 128
 129 * For non-recursive newtypes, P, treat P just like a type synonym after
 130   type-checking is done; i.e. it's opaque during type checking (functions
 131   from TcType) but transparent afterwards (functions from Type).
 132   "Treat P as a type synonym" means "all functions expand NewTcApps
 133   on the fly".
 134
 135   Applications of the data constructor P simply vanish:
 136         P x = x
 137
 138
 139 * For recursive newtypes Q, treat the Q and its representation as
 140   distinct right through the compiler.  Applications of the data consructor
 141   use a coerce:
 142         Q = \(x::Q->Q). coerce Q x
 143   They are rare, so who cares if they are a tiny bit less efficient.
 144
 145 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
 146 to cut all loops.  The other members of the loop may be marked 'non-recursive'.
 147
 148
 149 %************************************************************************
 150 %*                                                                      *
 151 \subsection{The data type}
 152 %*                                                                      *
 153 %************************************************************************
 154
 155
 156 \begin{code}
 157 type SuperKind = Type
 158 type Kind      = Type
 159
 160 type TyVarSubst = TyVarEnv Type
 161
 162 data Type
 163   = TyVarTy TyVar
 164
 165   | AppTy
 166         Type            -- Function is *not* a TyConApp
 167         Type
 168
 169   | TyConApp            -- Application of a TyCon
 170         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 171                         --      synonyms have their own constructors, below.
 172         [Type]          -- Might not be saturated.
 173
 174   | NewTcApp            -- Application of a NewType TyCon.   All newtype applications
 175         TyCon           -- show up like this until they are fed through newTypeRep,
 176                         -- which returns
 177                         --      * an ordinary TyConApp for non-saturated,
 178                         --       or recursive newtypes
 179                         --
 180                         --      * the representation type of the newtype for satuarted,
 181                         --        non-recursive ones
 182                         -- [But the result of a call to newTypeRep is always consumed
 183                         --  immediately; it never lives on in another type.  So in any
 184                         --  type, newtypes are always represented with NewTcApp.]
 185         [Type]          -- Might not be saturated.
 186
 187   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 188         Type
 189         Type
 190
 191   | ForAllTy            -- A polymorphic type
 192         TyVar
 193         Type
 194
 195   | PredTy              -- A high level source type
 196         PredType        -- ...can be expanded to a representation type...
 197
 198   | NoteTy              -- A type with a note attached
 199         TyNote
 200         Type            -- The expanded version
 201
 202 data TyNote
 203   = FTVNote TyVarSet    -- The free type variables of the noted expression
 204
 205   | SynNote Type        -- Used for type synonyms
 206                         -- The Type is always a TyConApp, and is the un-expanded form.
 207                         -- The type to which the note is attached is the expanded form.
 208 \end{code}
 209
 210 -------------------------------------
 211                 Source types
 212
 213 A type of the form
 214         PredTy p
 215 represents a value whose type is the Haskell predicate p,
 216 where a predicate is what occurs before the '=>' in a Haskell type.
 217 It can be expanded into its representation, but:
 218
 219         * The type checker must treat it as opaque
 220         * The rest of the compiler treats it as transparent
 221
 222 Consider these examples:
 223         f :: (Eq a) => a -> Int
 224         g :: (?x :: Int -> Int) => a -> Int
 225         h :: (r\l) => {r} => {l::Int | r}
 226
 227 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 228 Predicates are represented inside GHC by PredType:
 229
 230 \begin{code}
 231 data PredType
 232   = ClassP Class [Type]         -- Class predicate
 233   | IParam (IPName Name) Type   -- Implicit parameter
 234
 235 type ThetaType = [PredType]
 236 \end{code}
 237
 238 (We don't support TREX records yet, but the setup is designed
 239 to expand to allow them.)
 240
 241 A Haskell qualified type, such as that for f,g,h above, is
 242 represented using
 243         * a FunTy for the double arrow
 244         * with a PredTy as the function argument
 245
 246 The predicate really does turn into a real extra argument to the
 247 function.  If the argument has type (PredTy p) then the predicate p is
 248 represented by evidence (a dictionary, for example, of type (predRepTy p).
 249
 250
 251 %************************************************************************
 252 %*                                                                      *
 253 \subsection{Kinds}
 254 %*                                                                      *
 255 %************************************************************************
 256
 257 Kinds
 258 ~~~~~
 259 kind :: KX = kind -> kind
 260
 261            | Type liftedness    -- (Type *) is printed as just *
 262                                 -- (Type #) is printed as just #
 263
 264            | OpenKind           -- Can be lifted or unlifted
 265                                 -- Printed '?'
 266
 267            | kv                 -- A kind variable; *only* happens during kind checking
 268
 269 boxity :: BX = *        -- Lifted
 270              | #        -- Unlifted
 271              | bv       -- A boxity variable; *only* happens during kind checking
 272
 273 There's a little subtyping at the kind level:
 274         forall b. Type b <: OpenKind
 275
 276 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 277
 278 OpenKind, written '?', is used as the kind for certain type variables,
 279 in two situations:
 280
 281 1.  The universally quantified type variable(s) for special built-in
 282     things like error :: forall (a::?). String -> a.
 283     Here, the 'a' can be instantiated to a lifted or unlifted type.
 284
 285 2.  Kind '?' is also used when the typechecker needs to create a fresh
 286     type variable, one that may very well later be unified with a type.
 287     For example, suppose f::a, and we see an application (f x).  Then a
 288     must be a function type, so we unify a with (b->c).  But what kind
 289     are b and c?  They can be lifted or unlifted types, or indeed type schemes,
 290     so we give them kind '?'.
 291
 292     When the type checker generalises over a bunch of type variables, it
 293     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 294     present in an inferred type.
 295
 296
 297 ------------------------------------------
 298 Define  KX, the type of a kind
 299         BX, the type of a boxity
 300
 301 \begin{code}
 302 superKindName    = kindQual FSLIT("KX") kindConKey
 303 superBoxityName  = kindQual FSLIT("BX") boxityConKey
 304 liftedConName    = kindQual FSLIT("*") liftedConKey
 305 unliftedConName  = kindQual FSLIT("#") unliftedConKey
 306 openKindConName  = kindQual FSLIT("?") anyBoxConKey
 307 typeConName      = kindQual FSLIT("Type") typeConKey
 308
 309 kindQual str uq = mkInternalName uq (mkKindOccFS tcName str) noSrcLoc
 310         -- Kinds are not z-encoded in interface file, hence mkKindOccFS
 311         -- And they don't come from any particular module; indeed we always
 312         -- want to print them unqualified.  Hence the InternalName.
 313 \end{code}
 314
 315 \begin{code}
 316 superKind :: SuperKind          -- KX, the type of all kinds
 317 superKind = TyConApp (mkSuperKindCon superKindName) []
 318
 319 superBoxity :: SuperKind                -- BX, the type of all boxities
 320 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 321 \end{code}
 322
 323 ------------------------------------------
 324 Define boxities: @*@ and @#@
 325
 326 \begin{code}
 327 liftedBoxity, unliftedBoxity :: Kind            -- :: BX
 328 liftedBoxity   = TyConApp liftedBoxityCon   []
 329 unliftedBoxity = TyConApp unliftedBoxityCon []
 330
 331 liftedBoxityCon   = mkKindCon liftedConName superBoxity
 332 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
 333 \end{code}
 334
 335 ------------------------------------------
 336 Define kinds: Type, Type *, Type #, OpenKind
 337
 338 \begin{code}
 339 typeCon :: KindCon      -- :: BX -> KX
 340 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 341
 342 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 343
 344 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 345 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 346
 347 openKindCon     = mkKindCon openKindConName superKind
 348 openTypeKind    = TyConApp openKindCon []
 349 \end{code}
 350
 351 \begin{code}
 352 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind :: Kind -> Bool
 353 isLiftedTypeKind (TyConApp tc [TyConApp bc []])   = tyConName tc == typeConName &&
 354                                                     tyConName bc == liftedConName
 355 isLiftedTypeKind other = False
 356
 357 isUnliftedTypeKind (TyConApp tc [TyConApp bc []]) = tyConName tc == typeConName &&
 358                                                     tyConName bc == unliftedConName
 359 isUnliftedTypeKind other = False
 360
 361 isOpenTypeKind (TyConApp tc []) = tyConName tc == openKindConName
 362 isOpenTypeKind other = False
 363
 364 isSuperKind (TyConApp tc []) = tyConName tc == superKindName
 365 isSuperTypeKind other = False
 366 \end{code}
 367
 368 ------------------------------------------
 369 Define arrow kinds
 370
 371 \begin{code}
 372 mkArrowKind :: Kind -> Kind -> Kind
 373 mkArrowKind k1 k2 = k1 `FunTy` k2
 374
 375 mkArrowKinds :: [Kind] -> Kind -> Kind
 376 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 377 \end{code}
 378
 379
 380 %************************************************************************
 381 %*                                                                      *
 382                         TyThing
 383 %*                                                                      *
 384 %************************************************************************
 385
 386 Despite the fact that DataCon has to be imported via a hi-boot route,
 387 this module seems the right place for TyThing, because it's needed for
 388 funTyCon and all the types in TysPrim.
 389
 390 \begin{code}
 391 data TyThing = AnId     Id
 392              | ADataCon DataCon
 393              | ATyCon   TyCon
 394              | AClass   Class
 395
 396 instance Outputable TyThing where
 397   ppr (AnId   id)   = ptext SLIT("AnId")     <+> ppr id
 398   ppr (ATyCon tc)   = ptext SLIT("ATyCon")   <+> ppr tc
 399   ppr (AClass cl)   = ptext SLIT("AClass")   <+> ppr cl
 400   ppr (ADataCon dc) = ptext SLIT("ADataCon") <+> ppr (dataConName dc)
 401
 402 instance NamedThing TyThing where       -- Can't put this with the type
 403   getName (AnId id)     = getName id    -- decl, because the DataCon instance
 404   getName (ATyCon tc)   = getName tc    -- isn't visible there
 405   getName (AClass cl)   = getName cl
 406   getName (ADataCon dc) = dataConName dc
 407 \end{code}
 408
 409
 410 %************************************************************************
 411 %*                                                                      *
 412 \subsection{Wired-in type constructors
 413 %*                                                                      *
 414 %************************************************************************
 415
 416 We define a few wired-in type constructors here to avoid module knots
 417
 418 \begin{code}
 419 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 420         -- You might think that (->) should have type (? -> ? -> *), and you'd be right
 421         -- But if we do that we get kind errors when saying
 422         --      instance Control.Arrow (->)
 423         -- becuase the expected kind is (*->*->*).  The trouble is that the
 424         -- expected/actual stuff in the unifier does not go contra-variant, whereas
 425         -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
 426         -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
 427
 428 funTyConName = mkWiredInName gHC_PRIM
 429                         (mkOccFS tcName FSLIT("(->)"))
 430                         funTyConKey
 431                         Nothing                 -- No parent object
 432                         (ATyCon funTyCon)       -- Relevant TyCon
 433 \end{code}
 434
 435
 436 %************************************************************************
 437 %*                                                                      *
 438 \subsection{The external interface}
 439 %*                                                                      *
 440 %************************************************************************
 441
 442 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
 443 defined to use this.  @pprParendType@ is the same, except it puts
 444 parens around the type, except for the atomic cases.  @pprParendType@
 445 works just by setting the initial context precedence very high.
 446
 447 \begin{code}
 448 data Prec = TopPrec     -- No parens
 449           | FunPrec     -- Function args; no parens for tycon apps
 450           | TyConPrec   -- Tycon args; no parens for atomic
 451           deriving( Eq, Ord )
 452
 453 maybeParen :: Prec -> Prec -> SDoc -> SDoc
 454 maybeParen ctxt_prec inner_prec pretty
 455   | ctxt_prec < inner_prec = pretty
 456   | otherwise              = parens pretty
 457
 458 ------------------
 459 pprType, pprParendType :: Type -> SDoc
 460 pprType       ty = ppr_type TopPrec   ty
 461 pprParendType ty = ppr_type TyConPrec ty
 462
 463 ------------------
 464 pprKind, pprParendKind :: Kind -> SDoc
 465 pprKind       k = ppr_kind TopPrec k
 466 pprParendKind k = ppr_kind TyConPrec k
 467
 468 ------------------
 469 pprPred :: PredType -> SDoc
 470 pprPred (ClassP cls tys) = pprClassPred cls tys
 471 pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
 472
 473 pprClassPred :: Class -> [Type] -> SDoc
 474 pprClassPred clas tys = ppr clas <+> sep (map pprParendType tys)
 475
 476 pprTheta :: ThetaType -> SDoc
 477 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
 478
 479 pprThetaArrow :: ThetaType -> SDoc
 480 pprThetaArrow theta
 481   | null theta = empty
 482   | otherwise  = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
 483
 484 ------------------
 485 instance Outputable Type where
 486     ppr ty = pprType ty
 487
 488 instance Outputable PredType where
 489     ppr = pprPred
 490
 491 instance Outputable name => OutputableBndr (IPName name) where
 492     pprBndr _ n = ppr n -- Simple for now
 493
 494 ------------------
 495         -- OK, here's the main printer
 496
 497 ppr_type :: Prec -> Type -> SDoc
 498 ppr_type p (TyVarTy tv)               = ppr tv
 499 ppr_type p (PredTy pred)              = braces (ppr pred)
 500 ppr_type p (NoteTy (SynNote ty1) ty2) = ppr_type p ty1
 501 ppr_type p (NoteTy other         ty2) = ppr_type p ty2
 502
 503 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
 504 ppr_type p (NewTcApp tc tys) = ifPprDebug (ptext SLIT("<nt>")) <>
 505                                ppr_tc_app p tc tys
 506
 507 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
 508                            pprType t1 <+> ppr_type TyConPrec t2
 509
 510 ppr_type p (FunTy ty1 ty2)
 511   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
 512     maybeParen p FunPrec $
 513     sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
 514   where
 515     ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
 516     ppr_fun_tail other_ty        = [arrow <+> pprType other_ty]
 517
 518 ppr_type p ty@(ForAllTy _ _)
 519   = maybeParen p FunPrec $
 520     sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
 521   where
 522     (tvs,  rho) = split1 [] ty
 523     (ctxt, tau) = split2 [] rho
 524
 525     split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
 526     split1 tvs ty               = (reverse tvs, ty)
 527
 528     split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
 529     split2 ps ty                    = (reverse ps, ty)
 530
 531 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
 532 ppr_tc_app p tc []
 533   = ppr tc
 534 ppr_tc_app p tc [ty]
 535   | tc `hasKey` listTyConKey = brackets (pprType ty)
 536   | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
 537 ppr_tc_app p tc tys
 538   | isTupleTyCon tc && tyConArity tc == length tys
 539   = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
 540   | otherwise
 541   = maybeParen p TyConPrec $
 542     ppr tc <+> sep (map (ppr_type TyConPrec) tys)
 543
 544 -------------------
 545 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
 546
 547 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
 548              | otherwise             = parens (ppr tv <+> dcolon <+> pprKind kind)
 549              where
 550                kind = tyVarKind tv
 551
 552
 553 -------------------
 554 ppr_kind :: Prec -> Kind -> SDoc
 555 ppr_kind p k
 556   | isOpenTypeKind k     = ptext SLIT("?")
 557   | isLiftedTypeKind k   = ptext SLIT("*")
 558   | isUnliftedTypeKind k = ptext SLIT("#")
 559 ppr_kind p (TyVarTy tv)  = ppr tv
 560 ppr_kind p (FunTy k1 k2) = maybeParen p FunPrec $
 561                                   sep [ ppr_kind FunPrec k1, arrow <+> pprKind k2]
 562 ppr_kind p other = ptext SLIT("STRANGE KIND:") <+> ppr_type p other
 563 \end{code}
 564