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              -- The type of evidence for a type predictate
 196         PredType        -- Can be expanded to a representation type.
 197         -- NB: A PredTy (EqPred _ _) can appear only as the kind
 198         --     of a coercion variable; never as the argument or result
 199         --     of a FunTy (unlike ClassP, IParam)
 200
 201   | NoteTy              -- A type with a note attached
 202         TyNote
 203         Type            -- The expanded version
 204
 205 type Kind = Type        -- Invariant: a kind is always
 206                         --      FunTy k1 k2
 207                         -- or   TyConApp PrimTyCon [...]
 208                         -- or   TyVar kv (during inference only)
 209                         -- or   ForAll ... (for top-level coercions)
 210
 211 type SuperKind = Type   -- Invariant: a super kind is always
 212                         --   TyConApp SuperKindTyCon ...
 213
 214 type Coercion = Type
 215
 216 type CoercionKind = Kind
 217
 218 data TyNote = FTVNote TyVarSet  -- The free type variables of the noted expression
 219 \end{code}
 220
 221 -------------------------------------
 222                 Source types
 223
 224 A type of the form
 225         PredTy p
 226 represents a value whose type is the Haskell predicate p,
 227 where a predicate is what occurs before the '=>' in a Haskell type.
 228 It can be expanded into its representation, but:
 229
 230         * The type checker must treat it as opaque
 231         * The rest of the compiler treats it as transparent
 232
 233 Consider these examples:
 234         f :: (Eq a) => a -> Int
 235         g :: (?x :: Int -> Int) => a -> Int
 236         h :: (r\l) => {r} => {l::Int | r}
 237
 238 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 239 Predicates are represented inside GHC by PredType:
 240
 241 \begin{code}
 242 data PredType
 243   = ClassP Class [Type]         -- Class predicate
 244   | IParam (IPName Name) Type   -- Implicit parameter
 245   | EqPred Type Type            -- Equality predicate (ty1 :=: ty2)
 246
 247 type ThetaType = [PredType]
 248 \end{code}
 249
 250 (We don't support TREX records yet, but the setup is designed
 251 to expand to allow them.)
 252
 253 A Haskell qualified type, such as that for f,g,h above, is
 254 represented using
 255         * a FunTy for the double arrow
 256         * with a PredTy as the function argument
 257
 258 The predicate really does turn into a real extra argument to the
 259 function.  If the argument has type (PredTy p) then the predicate p is
 260 represented by evidence (a dictionary, for example, of type (predRepTy p).
 261
 262
 263 %************************************************************************
 264 %*                                                                      *
 265                         TyThing
 266 %*                                                                      *
 267 %************************************************************************
 268
 269 Despite the fact that DataCon has to be imported via a hi-boot route,
 270 this module seems the right place for TyThing, because it's needed for
 271 funTyCon and all the types in TysPrim.
 272
 273 \begin{code}
 274 data TyThing = AnId     Id
 275              | ADataCon DataCon
 276              | ATyCon   TyCon
 277              | AClass   Class
 278
 279 instance Outputable TyThing where
 280   ppr thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
 281
 282 pprTyThingCategory :: TyThing -> SDoc
 283 pprTyThingCategory (ATyCon _)   = ptext SLIT("Type constructor")
 284 pprTyThingCategory (AClass _)   = ptext SLIT("Class")
 285 pprTyThingCategory (AnId   _)   = ptext SLIT("Identifier")
 286 pprTyThingCategory (ADataCon _) = ptext SLIT("Data constructor")
 287
 288 instance NamedThing TyThing where       -- Can't put this with the type
 289   getName (AnId id)     = getName id    -- decl, because the DataCon instance
 290   getName (ATyCon tc)   = getName tc    -- isn't visible there
 291   getName (AClass cl)   = getName cl
 292   getName (ADataCon dc) = dataConName dc
 293 \end{code}
 294
 295
 296 %************************************************************************
 297 %*                                                                      *
 298                 Wired-in type constructors
 299 %*                                                                      *
 300 %************************************************************************
 301
 302 We define a few wired-in type constructors here to avoid module knots
 303
 304 \begin{code}
 305 --------------------------
 306 -- First the TyCons...
 307
 308 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
 309         -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
 310         -- But if we do that we get kind errors when saying
 311         --      instance Control.Arrow (->)
 312         -- becuase the expected kind is (*->*->*).  The trouble is that the
 313         -- expected/actual stuff in the unifier does not go contra-variant, whereas
 314         -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
 315         -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
 316
 317
 318 tySuperKindTyCon     = mkSuperKindTyCon tySuperKindTyConName
 319 coSuperKindTyCon     = mkSuperKindTyCon coSuperKindTyConName
 320
 321 liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName
 322 openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName
 323 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
 324 ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName
 325 argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName
 326 eqCoercionKindTyCon =
 327   mkCoercionTyCon eqCoercionKindTyConName 2 (\ _ -> coSuperKind)
 328
 329 mkKindTyCon :: Name -> TyCon
 330 mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
 331
 332 --------------------------
 333 -- ... and now their names
 334
 335 tySuperKindTyConName      = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
 336 coSuperKindTyConName      = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
 337 liftedTypeKindTyConName   = mkPrimTyConName FSLIT("*") liftedTypeKindTyConKey liftedTypeKindTyCon
 338 openTypeKindTyConName     = mkPrimTyConName FSLIT("?") openTypeKindTyConKey openTypeKindTyCon
 339 unliftedTypeKindTyConName = mkPrimTyConName FSLIT("#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
 340 ubxTupleKindTyConName     = mkPrimTyConName FSLIT("(##)") ubxTupleKindTyConKey ubxTupleKindTyCon
 341 argTypeKindTyConName      = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
 342 funTyConName              = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon
 343
 344 eqCoercionKindTyConName   = mkWiredInName gHC_PRIM (mkOccNameFS tcName (FSLIT(":=:")))
 345                                         eqCoercionKindTyConKey Nothing (ATyCon eqCoercionKindTyCon)
 346                                         BuiltInSyntax
 347
 348 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 349                                               key
 350                                               Nothing           -- No parent object
 351                                               (ATyCon tycon)
 352                                               BuiltInSyntax
 353         -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
 354         -- because they are never in scope in the source
 355
 356 ------------------
 357 -- We also need Kinds and SuperKinds, locally and in TyCon
 358
 359 kindTyConType :: TyCon -> Type
 360 kindTyConType kind = TyConApp kind []
 361
 362 liftedTypeKind   = kindTyConType liftedTypeKindTyCon
 363 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
 364 openTypeKind     = kindTyConType openTypeKindTyCon
 365 argTypeKind      = kindTyConType argTypeKindTyCon
 366 ubxTupleKind     = kindTyConType ubxTupleKindTyCon
 367
 368 mkArrowKind :: Kind -> Kind -> Kind
 369 mkArrowKind k1 k2 = FunTy k1 k2
 370
 371 mkArrowKinds :: [Kind] -> Kind -> Kind
 372 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 373
 374 tySuperKind, coSuperKind :: SuperKind
 375 tySuperKind = kindTyConType tySuperKindTyCon
 376 coSuperKind = kindTyConType coSuperKindTyCon
 377
 378 isTySuperKind (NoteTy _ ty)    = isTySuperKind ty
 379 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
 380 isTySuperKind other            = False
 381
 382 isCoSuperKind (NoteTy _ ty)    = isCoSuperKind ty
 383 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
 384 isCoSuperKind other            = False
 385
 386 isCoercionKindTyCon kc = kc `hasKey` eqCoercionKindTyConKey
 387
 388
 389 -------------------
 390 -- lastly we need a few functions on Kinds
 391
 392 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
 393
 394 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
 395 isLiftedTypeKind other            = False
 396
 397
 398 \end{code}
 399
 400
 401
 402 %************************************************************************
 403 %*                                                                      *
 404 \subsection{The external interface}
 405 %*                                                                      *
 406 %************************************************************************
 407
 408 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
 409 defined to use this.  @pprParendType@ is the same, except it puts
 410 parens around the type, except for the atomic cases.  @pprParendType@
 411 works just by setting the initial context precedence very high.
 412
 413 \begin{code}
 414 data Prec = TopPrec     -- No parens
 415           | FunPrec     -- Function args; no parens for tycon apps
 416           | TyConPrec   -- Tycon args; no parens for atomic
 417           deriving( Eq, Ord )
 418
 419 maybeParen :: Prec -> Prec -> SDoc -> SDoc
 420 maybeParen ctxt_prec inner_prec pretty
 421   | ctxt_prec < inner_prec = pretty
 422   | otherwise              = parens pretty
 423
 424 ------------------
 425 pprType, pprParendType :: Type -> SDoc
 426 pprType       ty = ppr_type TopPrec   ty
 427 pprParendType ty = ppr_type TyConPrec ty
 428
 429 ------------------
 430 pprPred :: PredType -> SDoc
 431 pprPred (ClassP cls tys) = pprClassPred cls tys
 432 pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
 433 pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT(":=:")), ppr ty2]
 434
 435 pprClassPred :: Class -> [Type] -> SDoc
 436 pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas)
 437                         <+> sep (map pprParendType tys)
 438
 439 pprTheta :: ThetaType -> SDoc
 440 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
 441
 442 pprThetaArrow :: ThetaType -> SDoc
 443 pprThetaArrow theta
 444   | null theta = empty
 445   | otherwise  = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
 446
 447 ------------------
 448 instance Outputable Type where
 449     ppr ty = pprType ty
 450
 451 instance Outputable PredType where
 452     ppr = pprPred
 453
 454 instance Outputable name => OutputableBndr (IPName name) where
 455     pprBndr _ n = ppr n -- Simple for now
 456
 457 ------------------
 458         -- OK, here's the main printer
 459
 460 pprKind = pprType
 461 pprParendKind = pprParendType
 462
 463 ppr_type :: Prec -> Type -> SDoc
 464 ppr_type p (TyVarTy tv)       = ppr tv
 465 ppr_type p (PredTy pred)      = braces (ppr pred)
 466 ppr_type p (NoteTy other ty2) = ppr_type p ty2
 467 ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
 468
 469 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
 470                            pprType t1 <+> ppr_type TyConPrec t2
 471
 472 ppr_type p ty@(ForAllTy _ _)       = ppr_forall_type p ty
 473 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
 474
 475 ppr_type p (FunTy ty1 ty2)
 476   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
 477     maybeParen p FunPrec $
 478     sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
 479   where
 480     ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
 481     ppr_fun_tail other_ty        = [arrow <+> pprType other_ty]
 482
 483 ppr_forall_type :: Prec -> Type -> SDoc
 484 ppr_forall_type p ty
 485   = maybeParen p FunPrec $
 486     sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
 487   where
 488     (tvs,  rho) = split1 [] ty
 489     (ctxt, tau) = split2 [] rho
 490
 491     split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
 492     split1 tvs (NoteTy _ ty)    = split1 tvs ty
 493     split1 tvs ty               = (reverse tvs, ty)
 494
 495     split2 ps (NoteTy _ arg     -- Rather a disgusting case
 496                `FunTy` res)           = split2 ps (arg `FunTy` res)
 497     split2 ps (PredTy p `FunTy` ty)   = split2 (p:ps) ty
 498     split2 ps (NoteTy _ ty)           = split2 ps ty
 499     split2 ps ty                      = (reverse ps, ty)
 500
 501 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
 502 ppr_tc_app p tc []
 503   = ppr_tc tc
 504 ppr_tc_app p tc [ty]
 505   | tc `hasKey` listTyConKey = brackets (pprType ty)
 506   | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
 507   | tc `hasKey` liftedTypeKindTyConKey   = ptext SLIT("*")
 508   | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#")
 509   | tc `hasKey` openTypeKindTyConKey     = ptext SLIT("(?)")
 510   | tc `hasKey` ubxTupleKindTyConKey     = ptext SLIT("(#)")
 511   | tc `hasKey` argTypeKindTyConKey      = ptext SLIT("??")
 512
 513 ppr_tc_app p tc tys
 514   | isTupleTyCon tc && tyConArity tc == length tys
 515   = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
 516   | otherwise
 517   = maybeParen p TyConPrec $
 518     ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)
 519
 520 ppr_tc :: TyCon -> SDoc
 521 ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
 522   where
 523    pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
 524                                              then ptext SLIT("<recnt>")
 525                                              else ptext SLIT("<nt>"))
 526                | otherwise     = empty
 527
 528 -------------------
 529 pprForAll []  = empty
 530 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
 531
 532 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
 533              | otherwise             = parens (ppr tv <+> dcolon <+> pprKind kind)
 534              where
 535                kind = tyVarKind tv
 536 \end{code}
 537