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