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