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