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                                               (ATyCon tycon)
 358                                               BuiltInSyntax
 359         -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
 360         -- because they are never in scope in the source
 361
 362 ------------------
 363 -- We also need Kinds and SuperKinds, locally and in TyCon
 364
 365 kindTyConType :: TyCon -> Type
 366 kindTyConType kind = TyConApp kind []
 367
 368 liftedTypeKind   = kindTyConType liftedTypeKindTyCon
 369 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
 370 openTypeKind     = kindTyConType openTypeKindTyCon
 371 argTypeKind      = kindTyConType argTypeKindTyCon
 372 ubxTupleKind     = kindTyConType ubxTupleKindTyCon
 373
 374 mkArrowKind :: Kind -> Kind -> Kind
 375 mkArrowKind k1 k2 = FunTy k1 k2
 376
 377 mkArrowKinds :: [Kind] -> Kind -> Kind
 378 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 379
 380 tySuperKind, coSuperKind :: SuperKind
 381 tySuperKind = kindTyConType tySuperKindTyCon
 382 coSuperKind = kindTyConType coSuperKindTyCon
 383
 384 isTySuperKind (NoteTy _ ty)    = isTySuperKind ty
 385 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
 386 isTySuperKind other            = False
 387
 388 isCoSuperKind :: SuperKind -> Bool
 389 isCoSuperKind (NoteTy _ ty)    = isCoSuperKind ty
 390 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
 391 isCoSuperKind other            = False
 392
 393 -------------------
 394 -- lastly we need a few functions on Kinds
 395
 396 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
 397
 398 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
 399 isLiftedTypeKind other            = False
 400
 401
 402 \end{code}
 403
 404
 405
 406 %************************************************************************
 407 %*                                                                      *
 408 \subsection{The external interface}
 409 %*                                                                      *
 410 %************************************************************************
 411
 412 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
 413 defined to use this.  @pprParendType@ is the same, except it puts
 414 parens around the type, except for the atomic cases.  @pprParendType@
 415 works just by setting the initial context precedence very high.
 416
 417 \begin{code}
 418 data Prec = TopPrec     -- No parens
 419           | FunPrec     -- Function args; no parens for tycon apps
 420           | TyConPrec   -- Tycon args; no parens for atomic
 421           deriving( Eq, Ord )
 422
 423 maybeParen :: Prec -> Prec -> SDoc -> SDoc
 424 maybeParen ctxt_prec inner_prec pretty
 425   | ctxt_prec < inner_prec = pretty
 426   | otherwise              = parens pretty
 427
 428 ------------------
 429 pprType, pprParendType :: Type -> SDoc
 430 pprType       ty = ppr_type TopPrec   ty
 431 pprParendType ty = ppr_type TyConPrec ty
 432
 433 ------------------
 434 pprPred :: PredType -> SDoc
 435 pprPred (ClassP cls tys) = pprClassPred cls tys
 436 pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
 437 pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT(":=:")), ppr ty2]
 438
 439 pprClassPred :: Class -> [Type] -> SDoc
 440 pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas)
 441                         <+> sep (map pprParendType tys)
 442
 443 pprTheta :: ThetaType -> SDoc
 444 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
 445
 446 pprThetaArrow :: ThetaType -> SDoc
 447 pprThetaArrow theta
 448   | null theta = empty
 449   | otherwise  = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
 450
 451 ------------------
 452 instance Outputable Type where
 453     ppr ty = pprType ty
 454
 455 instance Outputable PredType where
 456     ppr = pprPred
 457
 458 instance Outputable name => OutputableBndr (IPName name) where
 459     pprBndr _ n = ppr n -- Simple for now
 460
 461 ------------------
 462         -- OK, here's the main printer
 463
 464 pprKind = pprType
 465 pprParendKind = pprParendType
 466
 467 ppr_type :: Prec -> Type -> SDoc
 468 ppr_type p (TyVarTy tv)       = ppr tv
 469 ppr_type p (PredTy pred)      = braces (ppr pred)
 470 ppr_type p (NoteTy other ty2) = ppr_type p ty2
 471 ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
 472
 473 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
 474                            pprType t1 <+> ppr_type TyConPrec t2
 475
 476 ppr_type p ty@(ForAllTy _ _)       = ppr_forall_type p ty
 477 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
 478
 479 ppr_type p (FunTy ty1 ty2)
 480   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
 481     maybeParen p FunPrec $
 482     sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
 483   where
 484     ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
 485     ppr_fun_tail other_ty        = [arrow <+> pprType other_ty]
 486
 487 ppr_forall_type :: Prec -> Type -> SDoc
 488 ppr_forall_type p ty
 489   = maybeParen p FunPrec $
 490     sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
 491   where
 492     (tvs,  rho) = split1 [] ty
 493     (ctxt, tau) = split2 [] rho
 494
 495     split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
 496     split1 tvs (NoteTy _ ty)    = split1 tvs ty
 497     split1 tvs ty               = (reverse tvs, ty)
 498
 499     split2 ps (NoteTy _ arg     -- Rather a disgusting case
 500                `FunTy` res)           = split2 ps (arg `FunTy` res)
 501     split2 ps (PredTy p `FunTy` ty)   = split2 (p:ps) ty
 502     split2 ps (NoteTy _ ty)           = split2 ps ty
 503     split2 ps ty                      = (reverse ps, ty)
 504
 505 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
 506 ppr_tc_app p tc []
 507   = ppr_tc tc
 508 ppr_tc_app p tc [ty]
 509   | tc `hasKey` listTyConKey = brackets (pprType ty)
 510   | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
 511   | tc `hasKey` liftedTypeKindTyConKey   = ptext SLIT("*")
 512   | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#")
 513   | tc `hasKey` openTypeKindTyConKey     = ptext SLIT("(?)")
 514   | tc `hasKey` ubxTupleKindTyConKey     = ptext SLIT("(#)")
 515   | tc `hasKey` argTypeKindTyConKey      = ptext SLIT("??")
 516
 517 ppr_tc_app p tc tys
 518   | isTupleTyCon tc && tyConArity tc == length tys
 519   = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
 520   | otherwise
 521   = maybeParen p TyConPrec $
 522     ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)
 523
 524 ppr_tc :: TyCon -> SDoc
 525 ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
 526   where
 527    pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
 528                                              then ptext SLIT("<recnt>")
 529                                              else ptext SLIT("<nt>"))
 530                | otherwise     = empty
 531
 532 -------------------
 533 pprForAll []  = empty
 534 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
 535
 536 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
 537              | otherwise             = parens (ppr tv <+> dcolon <+> pprKind kind)
 538              where
 539                kind = tyVarKind tv
 540 \end{code}
 541