compiler/types/TypeRep.lhs

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