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