ghc/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         TyVarSubst,
  14
  15         superKind, superBoxity,                         -- KX and BX respectively
  16         liftedBoxity, unliftedBoxity,                   -- :: BX
  17         openKindCon,                                    -- :: KX
  18         typeCon,                                        -- :: BX -> KX
  19         liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
  20         mkArrowKind, mkArrowKinds,                      -- :: KX -> KX -> KX
  21
  22         funTyCon,
  23
  24         crudePprType            -- Prints type representations for debugging
  25     ) where
  26
  27 #include "HsVersions.h"
  28
  29 import {-# SOURCE #-} DataCon( DataCon )
  30
  31 -- friends:
  32 import Var        ( Id, TyVar, tyVarKind )
  33 import VarEnv     ( TyVarEnv )
  34 import VarSet     ( TyVarSet )
  35 import Name       ( Name, mkWiredInName, mkInternalName )
  36 import OccName    ( mkOccFS, mkKindOccFS, tcName )
  37 import BasicTypes ( IPName )
  38 import TyCon      ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon, isNewTyCon )
  39 import Class      ( Class )
  40
  41 -- others
  42 import PrelNames        ( gHC_PRIM, kindConKey, boxityConKey, liftedConKey,
  43                           unliftedConKey, typeConKey, anyBoxConKey,
  44                           funTyConKey
  45                         )
  46 import SrcLoc           ( noSrcLoc )
  47 import Outputable
  48 \end{code}
  49
  50 %************************************************************************
  51 %*                                                                      *
  52 \subsection{Type Classifications}
  53 %*                                                                      *
  54 %************************************************************************
  55
  56 A type is
  57
  58         *unboxed*       iff its representation is other than a pointer
  59                         Unboxed types are also unlifted.
  60
  61         *lifted*        A type is lifted iff it has bottom as an element.
  62                         Closures always have lifted types:  i.e. any
  63                         let-bound identifier in Core must have a lifted
  64                         type.  Operationally, a lifted object is one that
  65                         can be entered.
  66
  67                         Only lifted types may be unified with a type variable.
  68
  69         *algebraic*     A type with one or more constructors, whether declared
  70                         with "data" or "newtype".
  71                         An algebraic type is one that can be deconstructed
  72                         with a case expression.
  73                         *NOT* the same as lifted types,  because we also
  74                         include unboxed tuples in this classification.
  75
  76         *data*          A type declared with "data".  Also boxed tuples.
  77
  78         *primitive*     iff it is a built-in type that can't be expressed
  79                         in Haskell.
  80
  81 Currently, all primitive types are unlifted, but that's not necessarily
  82 the case.  (E.g. Int could be primitive.)
  83
  84 Some primitive types are unboxed, such as Int#, whereas some are boxed
  85 but unlifted (such as ByteArray#).  The only primitive types that we
  86 classify as algebraic are the unboxed tuples.
  87
  88 examples of type classifications:
  89
  90 Type            primitive       boxed           lifted          algebraic
  91 -----------------------------------------------------------------------------
  92 Int#,           Yes             No              No              No
  93 ByteArray#      Yes             Yes             No              No
  94 (# a, b #)      Yes             No              No              Yes
  95 (  a, b  )      No              Yes             Yes             Yes
  96 [a]             No              Yes             Yes             Yes
  97
  98
  99
 100         ----------------------
 101         A note about newtypes
 102         ----------------------
 103
 104 Consider
 105         newtype N = MkN Int
 106
 107 Then we want N to be represented as an Int, and that's what we arrange.
 108 The front end of the compiler [TcType.lhs] treats N as opaque,
 109 the back end treats it as transparent [Type.lhs].
 110
 111 There's a bit of a problem with recursive newtypes
 112         newtype P = MkP P
 113         newtype Q = MkQ (Q->Q)
 114
 115 Here the 'implicit expansion' we get from treating P and Q as transparent
 116 would give rise to infinite types, which in turn makes eqType diverge.
 117 Similarly splitForAllTys and splitFunTys can get into a loop.
 118
 119 Solution:
 120
 121 * Newtypes are always represented using NewTcApp, never as TyConApp.
 122
 123 * For non-recursive newtypes, P, treat P just like a type synonym after
 124   type-checking is done; i.e. it's opaque during type checking (functions
 125   from TcType) but transparent afterwards (functions from Type).
 126   "Treat P as a type synonym" means "all functions expand NewTcApps
 127   on the fly".
 128
 129   Applications of the data constructor P simply vanish:
 130         P x = x
 131
 132
 133 * For recursive newtypes Q, treat the Q and its representation as
 134   distinct right through the compiler.  Applications of the data consructor
 135   use a coerce:
 136         Q = \(x::Q->Q). coerce Q x
 137   They are rare, so who cares if they are a tiny bit less efficient.
 138
 139 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
 140 to cut all loops.  The other members of the loop may be marked 'non-recursive'.
 141
 142
 143 %************************************************************************
 144 %*                                                                      *
 145 \subsection{The data type}
 146 %*                                                                      *
 147 %************************************************************************
 148
 149
 150 \begin{code}
 151 type SuperKind = Type
 152 type Kind      = Type
 153
 154 type TyVarSubst = TyVarEnv Type
 155
 156 data Type
 157   = TyVarTy TyVar
 158
 159   | AppTy
 160         Type            -- Function is *not* a TyConApp
 161         Type
 162
 163   | TyConApp            -- Application of a TyCon
 164         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 165                         --      synonyms have their own constructors, below.
 166         [Type]          -- Might not be saturated.
 167
 168   | NewTcApp            -- Application of a NewType TyCon.   All newtype applications
 169         TyCon           -- show up like this until they are fed through newTypeRep,
 170                         -- which returns
 171                         --      * an ordinary TyConApp for non-saturated,
 172                         --       or recursive newtypes
 173                         --
 174                         --      * the representation type of the newtype for satuarted,
 175                         --        non-recursive ones
 176                         -- [But the result of a call to newTypeRep is always consumed
 177                         --  immediately; it never lives on in another type.  So in any
 178                         --  type, newtypes are always represented with NewTcApp.]
 179         [Type]          -- Might not be saturated.
 180
 181   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 182         Type
 183         Type
 184
 185   | ForAllTy            -- A polymorphic type
 186         TyVar
 187         Type
 188
 189   | PredTy              -- A high level source type
 190         PredType        -- ...can be expanded to a representation type...
 191
 192   | NoteTy              -- A type with a note attached
 193         TyNote
 194         Type            -- The expanded version
 195
 196 data TyNote
 197   = FTVNote TyVarSet    -- The free type variables of the noted expression
 198
 199   | SynNote Type        -- Used for type synonyms
 200                         -- The Type is always a TyConApp, and is the un-expanded form.
 201                         -- The type to which the note is attached is the expanded form.
 202 \end{code}
 203
 204 -------------------------------------
 205                 Source types
 206
 207 A type of the form
 208         PredTy p
 209 represents a value whose type is the Haskell predicate p,
 210 where a predicate is what occurs before the '=>' in a Haskell type.
 211 It can be expanded into its representation, but:
 212
 213         * The type checker must treat it as opaque
 214         * The rest of the compiler treats it as transparent
 215
 216 Consider these examples:
 217         f :: (Eq a) => a -> Int
 218         g :: (?x :: Int -> Int) => a -> Int
 219         h :: (r\l) => {r} => {l::Int | r}
 220
 221 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 222 Predicates are represented inside GHC by PredType:
 223
 224 \begin{code}
 225 data PredType
 226   = ClassP Class [Type]         -- Class predicate
 227   | IParam (IPName Name) Type   -- Implicit parameter
 228
 229 type ThetaType = [PredType]
 230 \end{code}
 231
 232 (We don't support TREX records yet, but the setup is designed
 233 to expand to allow them.)
 234
 235 A Haskell qualified type, such as that for f,g,h above, is
 236 represented using
 237         * a FunTy for the double arrow
 238         * with a PredTy as the function argument
 239
 240 The predicate really does turn into a real extra argument to the
 241 function.  If the argument has type (PredTy p) then the predicate p is
 242 represented by evidence (a dictionary, for example, of type (predRepTy p).
 243
 244
 245 %************************************************************************
 246 %*                                                                      *
 247 \subsection{Kinds}
 248 %*                                                                      *
 249 %************************************************************************
 250
 251 Kinds
 252 ~~~~~
 253 kind :: KX = kind -> kind
 254
 255            | Type liftedness    -- (Type *) is printed as just *
 256                                 -- (Type #) is printed as just #
 257
 258            | OpenKind           -- Can be lifted or unlifted
 259                                 -- Printed '?'
 260
 261            | kv                 -- A kind variable; *only* happens during kind checking
 262
 263 boxity :: BX = *        -- Lifted
 264              | #        -- Unlifted
 265              | bv       -- A boxity variable; *only* happens during kind checking
 266
 267 There's a little subtyping at the kind level:
 268         forall b. Type b <: OpenKind
 269
 270 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 271
 272 OpenKind, written '?', is used as the kind for certain type variables,
 273 in two situations:
 274
 275 1.  The universally quantified type variable(s) for special built-in
 276     things like error :: forall (a::?). String -> a.
 277     Here, the 'a' can be instantiated to a lifted or unlifted type.
 278
 279 2.  Kind '?' is also used when the typechecker needs to create a fresh
 280     type variable, one that may very well later be unified with a type.
 281     For example, suppose f::a, and we see an application (f x).  Then a
 282     must be a function type, so we unify a with (b->c).  But what kind
 283     are b and c?  They can be lifted or unlifted types, or indeed type schemes,
 284     so we give them kind '?'.
 285
 286     When the type checker generalises over a bunch of type variables, it
 287     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 288     present in an inferred type.
 289
 290
 291 ------------------------------------------
 292 Define  KX, the type of a kind
 293         BX, the type of a boxity
 294
 295 \begin{code}
 296 superKindName    = kindQual FSLIT("KX") kindConKey
 297 superBoxityName  = kindQual FSLIT("BX") boxityConKey
 298 liftedConName    = kindQual FSLIT("*") liftedConKey
 299 unliftedConName  = kindQual FSLIT("#") unliftedConKey
 300 openKindConName  = kindQual FSLIT("?") anyBoxConKey
 301 typeConName      = kindQual FSLIT("Type") typeConKey
 302
 303 kindQual str uq = mkInternalName uq (mkKindOccFS tcName str) noSrcLoc
 304         -- Kinds are not z-encoded in interface file, hence mkKindOccFS
 305         -- And they don't come from any particular module; indeed we always
 306         -- want to print them unqualified.  Hence the InternalName.
 307 \end{code}
 308
 309 \begin{code}
 310 superKind :: SuperKind          -- KX, the type of all kinds
 311 superKind = TyConApp (mkSuperKindCon superKindName) []
 312
 313 superBoxity :: SuperKind                -- BX, the type of all boxities
 314 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 315 \end{code}
 316
 317 ------------------------------------------
 318 Define boxities: @*@ and @#@
 319
 320 \begin{code}
 321 liftedBoxity, unliftedBoxity :: Kind            -- :: BX
 322 liftedBoxity   = TyConApp liftedBoxityCon   []
 323 unliftedBoxity = TyConApp unliftedBoxityCon []
 324
 325 liftedBoxityCon   = mkKindCon liftedConName superBoxity
 326 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
 327 \end{code}
 328
 329 ------------------------------------------
 330 Define kinds: Type, Type *, Type #, OpenKind
 331
 332 \begin{code}
 333 typeCon :: KindCon      -- :: BX -> KX
 334 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 335
 336 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 337
 338 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 339 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 340
 341 openKindCon     = mkKindCon openKindConName superKind
 342 openTypeKind    = TyConApp openKindCon []
 343 \end{code}
 344
 345 ------------------------------------------
 346 Define arrow kinds
 347
 348 \begin{code}
 349 mkArrowKind :: Kind -> Kind -> Kind
 350 mkArrowKind k1 k2 = k1 `FunTy` k2
 351
 352 mkArrowKinds :: [Kind] -> Kind -> Kind
 353 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 354 \end{code}
 355
 356
 357 %************************************************************************
 358 %*                                                                      *
 359                         TyThing
 360 %*                                                                      *
 361 %************************************************************************
 362
 363 Despite the fact that DataCon has to be imported via a hi-boot route,
 364 this module seems the right place for TyThing, because it's needed for
 365 funTyCon and all the types in TysPrim.
 366
 367 \begin{code}
 368 data TyThing = AnId     Id
 369              | ADataCon DataCon
 370              | ATyCon   TyCon
 371              | AClass   Class
 372 \end{code}
 373
 374
 375 %************************************************************************
 376 %*                                                                      *
 377 \subsection{Wired-in type constructors
 378 %*                                                                      *
 379 %************************************************************************
 380
 381 We define a few wired-in type constructors here to avoid module knots
 382
 383 \begin{code}
 384 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 385         -- You might think that (->) should have type (? -> ? -> *), and you'd be right
 386         -- But if we do that we get kind errors when saying
 387         --      instance Control.Arrow (->)
 388         -- becuase the expected kind is (*->*->*).  The trouble is that the
 389         -- expected/actual stuff in the unifier does not go contra-variant, whereas
 390         -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
 391         -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
 392
 393 funTyConName = mkWiredInName gHC_PRIM
 394                         (mkOccFS tcName FSLIT("(->)"))
 395                         funTyConKey
 396                         Nothing                 -- No parent object
 397                         (ATyCon funTyCon)       -- Relevant TyCon
 398 \end{code}
 399
 400
 401
 402 %************************************************************************
 403 %*                                                                      *
 404                 Crude printing
 405         For debug purposes, we may want to print a type directly
 406 %*                                                                      *
 407 %************************************************************************
 408
 409 \begin{code}
 410 crudePprType :: Type -> SDoc
 411 crudePprType (TyVarTy tv)      = ppr tv
 412 crudePprType (AppTy t1 t2)     = crudePprType t1 <+> (parens (crudePprType t2))
 413 crudePprType (FunTy t1 t2)     = crudePprType t1 <+> (parens (crudePprType t2))
 414 crudePprType (TyConApp tc tys) = ppr_tc_app (ppr tc <> pp_nt tc) tys
 415 crudePprType (NewTcApp tc tys) = ptext SLIT("<nt>") <+> ppr_tc_app (ppr tc <> pp_nt tc) tys
 416 crudePprType (ForAllTy tv ty)  = sep [ptext SLIT("forall") <+>
 417                                         parens (ppr tv <+> crudePprType (tyVarKind tv)) <> dot,
 418                                       crudePprType ty]
 419 crudePprType (PredTy st)                = braces (crudePprPredTy st)
 420 crudePprType (NoteTy (SynNote ty1) ty2) = crudePprType ty1
 421 crudePprType (NoteTy other ty)          = crudePprType ty
 422
 423 crudePprPredTy (ClassP cls tys) = ppr_tc_app (ppr cls) tys
 424 crudePprPredTy (IParam ip ty)   = ppr ip <> dcolon <> crudePprType ty
 425
 426 ppr_tc_app :: SDoc -> [Type] -> SDoc
 427 ppr_tc_app tc tys = tc <+> sep (map (parens . crudePprType) tys)
 428
 429 pp_nt tc | isNewTyCon tc = ptext SLIT("(nt)")
 430          | otherwise     = empty
 431 \end{code}