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        -- See Note [PredTy], and Note [Equality predicates]
 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                 Note [PredTy]
 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 Note [Equality predicates]
 263 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 264         forall a b. (a :=: S b) => a -> b
 265 could be represented by
 266         ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
 267 OR
 268         ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
 269
 270 The latter is what we do.  (Unlike for class and implicit parameter
 271 constraints, which do use FunTy.)
 272
 273 Reason:
 274         * FunTy is always a *value* function
 275         * ForAllTy is discarded at runtime
 276
 277 We often need to make a "wildcard" (c::PredTy..).  We always use the same
 278 name (wildCoVarName), since it's not mentioned.
 279
 280
 281 %************************************************************************
 282 %*                                                                      *
 283                         TyThing
 284 %*                                                                      *
 285 %************************************************************************
 286
 287 Despite the fact that DataCon has to be imported via a hi-boot route,
 288 this module seems the right place for TyThing, because it's needed for
 289 funTyCon and all the types in TysPrim.
 290
 291 \begin{code}
 292 data TyThing = AnId     Id
 293              | ADataCon DataCon
 294              | ATyCon   TyCon
 295              | AClass   Class
 296
 297 instance Outputable TyThing where
 298   ppr thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
 299
 300 pprTyThingCategory :: TyThing -> SDoc
 301 pprTyThingCategory (ATyCon _)   = ptext SLIT("Type constructor")
 302 pprTyThingCategory (AClass _)   = ptext SLIT("Class")
 303 pprTyThingCategory (AnId   _)   = ptext SLIT("Identifier")
 304 pprTyThingCategory (ADataCon _) = ptext SLIT("Data constructor")
 305
 306 instance NamedThing TyThing where       -- Can't put this with the type
 307   getName (AnId id)     = getName id    -- decl, because the DataCon instance
 308   getName (ATyCon tc)   = getName tc    -- isn't visible there
 309   getName (AClass cl)   = getName cl
 310   getName (ADataCon dc) = dataConName dc
 311 \end{code}
 312
 313
 314 %************************************************************************
 315 %*                                                                      *
 316                 Wired-in type constructors
 317 %*                                                                      *
 318 %************************************************************************
 319
 320 We define a few wired-in type constructors here to avoid module knots
 321
 322 \begin{code}
 323 --------------------------
 324 -- First the TyCons...
 325
 326 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
 327         -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
 328         -- But if we do that we get kind errors when saying
 329         --      instance Control.Arrow (->)
 330         -- becuase the expected kind is (*->*->*).  The trouble is that the
 331         -- expected/actual stuff in the unifier does not go contra-variant, whereas
 332         -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
 333         -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
 334
 335
 336 tySuperKindTyCon     = mkSuperKindTyCon tySuperKindTyConName
 337 coSuperKindTyCon     = mkSuperKindTyCon coSuperKindTyConName
 338
 339 liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName
 340 openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName
 341 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
 342 ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName
 343 argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName
 344 eqCoercionKindTyCon =
 345   mkCoercionTyCon eqCoercionKindTyConName 2 (\ _ -> coSuperKind)
 346
 347 mkKindTyCon :: Name -> TyCon
 348 mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
 349
 350 --------------------------
 351 -- ... and now their names
 352
 353 tySuperKindTyConName      = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
 354 coSuperKindTyConName      = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
 355 liftedTypeKindTyConName   = mkPrimTyConName FSLIT("*") liftedTypeKindTyConKey liftedTypeKindTyCon
 356 openTypeKindTyConName     = mkPrimTyConName FSLIT("?") openTypeKindTyConKey openTypeKindTyCon
 357 unliftedTypeKindTyConName = mkPrimTyConName FSLIT("#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
 358 ubxTupleKindTyConName     = mkPrimTyConName FSLIT("(##)") ubxTupleKindTyConKey ubxTupleKindTyCon
 359 argTypeKindTyConName      = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
 360 funTyConName              = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon
 361
 362 eqCoercionKindTyConName   = mkWiredInName gHC_PRIM (mkOccNameFS tcName (FSLIT(":=:")))
 363                                         eqCoercionKindTyConKey Nothing (ATyCon eqCoercionKindTyCon)
 364                                         BuiltInSyntax
 365
 366 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
 367                                               key
 368                                               Nothing           -- No parent object
 369                                               (ATyCon tycon)
 370                                               BuiltInSyntax
 371         -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
 372         -- because they are never in scope in the source
 373
 374 ------------------
 375 -- We also need Kinds and SuperKinds, locally and in TyCon
 376
 377 kindTyConType :: TyCon -> Type
 378 kindTyConType kind = TyConApp kind []
 379
 380 liftedTypeKind   = kindTyConType liftedTypeKindTyCon
 381 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
 382 openTypeKind     = kindTyConType openTypeKindTyCon
 383 argTypeKind      = kindTyConType argTypeKindTyCon
 384 ubxTupleKind     = kindTyConType ubxTupleKindTyCon
 385
 386 mkArrowKind :: Kind -> Kind -> Kind
 387 mkArrowKind k1 k2 = FunTy k1 k2
 388
 389 mkArrowKinds :: [Kind] -> Kind -> Kind
 390 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 391
 392 tySuperKind, coSuperKind :: SuperKind
 393 tySuperKind = kindTyConType tySuperKindTyCon
 394 coSuperKind = kindTyConType coSuperKindTyCon
 395
 396 isTySuperKind (NoteTy _ ty)    = isTySuperKind ty
 397 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
 398 isTySuperKind other            = False
 399
 400 isCoSuperKind :: SuperKind -> Bool
 401 isCoSuperKind (NoteTy _ ty)    = isCoSuperKind ty
 402 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
 403 isCoSuperKind other            = False
 404
 405 isCoercionKindTyCon kc = kc `hasKey` eqCoercionKindTyConKey
 406
 407
 408 -------------------
 409 -- lastly we need a few functions on Kinds
 410
 411 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
 412
 413 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
 414 isLiftedTypeKind other            = False
 415
 416
 417 \end{code}
 418
 419
 420
 421 %************************************************************************
 422 %*                                                                      *
 423 \subsection{The external interface}
 424 %*                                                                      *
 425 %************************************************************************
 426
 427 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
 428 defined to use this.  @pprParendType@ is the same, except it puts
 429 parens around the type, except for the atomic cases.  @pprParendType@
 430 works just by setting the initial context precedence very high.
 431
 432 \begin{code}
 433 data Prec = TopPrec     -- No parens
 434           | FunPrec     -- Function args; no parens for tycon apps
 435           | TyConPrec   -- Tycon args; no parens for atomic
 436           deriving( Eq, Ord )
 437
 438 maybeParen :: Prec -> Prec -> SDoc -> SDoc
 439 maybeParen ctxt_prec inner_prec pretty
 440   | ctxt_prec < inner_prec = pretty
 441   | otherwise              = parens pretty
 442
 443 ------------------
 444 pprType, pprParendType :: Type -> SDoc
 445 pprType       ty = ppr_type TopPrec   ty
 446 pprParendType ty = ppr_type TyConPrec ty
 447
 448 ------------------
 449 pprPred :: PredType -> SDoc
 450 pprPred (ClassP cls tys) = pprClassPred cls tys
 451 pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
 452 pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT(":=:")), ppr ty2]
 453
 454 pprClassPred :: Class -> [Type] -> SDoc
 455 pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas)
 456                         <+> sep (map pprParendType tys)
 457
 458 pprTheta :: ThetaType -> SDoc
 459 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
 460
 461 pprThetaArrow :: ThetaType -> SDoc
 462 pprThetaArrow theta
 463   | null theta = empty
 464   | otherwise  = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
 465
 466 ------------------
 467 instance Outputable Type where
 468     ppr ty = pprType ty
 469
 470 instance Outputable PredType where
 471     ppr = pprPred
 472
 473 instance Outputable name => OutputableBndr (IPName name) where
 474     pprBndr _ n = ppr n -- Simple for now
 475
 476 ------------------
 477         -- OK, here's the main printer
 478
 479 pprKind = pprType
 480 pprParendKind = pprParendType
 481
 482 ppr_type :: Prec -> Type -> SDoc
 483 ppr_type p (TyVarTy tv)       = ppr tv
 484 ppr_type p (PredTy pred)      = braces (ppr pred)
 485 ppr_type p (NoteTy other ty2) = ppr_type p ty2
 486 ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
 487
 488 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
 489                            pprType t1 <+> ppr_type TyConPrec t2
 490
 491 ppr_type p ty@(ForAllTy _ _)       = ppr_forall_type p ty
 492 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
 493
 494 ppr_type p (FunTy ty1 ty2)
 495   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
 496     maybeParen p FunPrec $
 497     sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
 498   where
 499     ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
 500     ppr_fun_tail other_ty        = [arrow <+> pprType other_ty]
 501
 502 ppr_forall_type :: Prec -> Type -> SDoc
 503 ppr_forall_type p ty
 504   = maybeParen p FunPrec $
 505     sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
 506   where
 507     (tvs,  rho) = split1 [] ty
 508     (ctxt, tau) = split2 [] rho
 509
 510     split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
 511     split1 tvs (NoteTy _ ty)    = split1 tvs ty
 512     split1 tvs ty               = (reverse tvs, ty)
 513
 514     split2 ps (NoteTy _ arg     -- Rather a disgusting case
 515                `FunTy` res)           = split2 ps (arg `FunTy` res)
 516     split2 ps (PredTy p `FunTy` ty)   = split2 (p:ps) ty
 517     split2 ps (NoteTy _ ty)           = split2 ps ty
 518     split2 ps ty                      = (reverse ps, ty)
 519
 520 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
 521 ppr_tc_app p tc []
 522   = ppr_tc tc
 523 ppr_tc_app p tc [ty]
 524   | tc `hasKey` listTyConKey = brackets (pprType ty)
 525   | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
 526   | tc `hasKey` liftedTypeKindTyConKey   = ptext SLIT("*")
 527   | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#")
 528   | tc `hasKey` openTypeKindTyConKey     = ptext SLIT("(?)")
 529   | tc `hasKey` ubxTupleKindTyConKey     = ptext SLIT("(#)")
 530   | tc `hasKey` argTypeKindTyConKey      = ptext SLIT("??")
 531
 532 ppr_tc_app p tc tys
 533   | isTupleTyCon tc && tyConArity tc == length tys
 534   = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
 535   | otherwise
 536   = maybeParen p TyConPrec $
 537     ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)
 538
 539 ppr_tc :: TyCon -> SDoc
 540 ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
 541   where
 542    pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
 543                                              then ptext SLIT("<recnt>")
 544                                              else ptext SLIT("<nt>"))
 545                | otherwise     = empty
 546
 547 -------------------
 548 pprForAll []  = empty
 549 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
 550
 551 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
 552              | otherwise             = parens (ppr tv <+> dcolon <+> pprKind kind)
 553              where
 554                kind = tyVarKind tv
 555 \end{code}
 556