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         Type(..), TyNote(..),           -- Representation visible
   9         SourceType(..),                 -- to friends
  10
  11         Kind, PredType, ThetaType,              -- Synonyms
  12         TyVarSubst,
  13
  14         superKind, superBoxity,                         -- KX and BX respectively
  15         liftedBoxity, unliftedBoxity,                   -- :: BX
  16         openKindCon,                                    -- :: KX
  17         typeCon,                                        -- :: BX -> KX
  18         liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
  19         mkArrowKind, mkArrowKinds,                      -- :: KX -> KX -> KX
  20
  21         usageKindCon,                                   -- :: KX
  22         usageTypeKind,                                  -- :: KX
  23         usOnceTyCon, usManyTyCon,                       -- :: $
  24         usOnce, usMany,                                 -- :: $
  25
  26         funTyCon
  27     ) where
  28
  29 #include "HsVersions.h"
  30
  31 -- friends:
  32 import Var        ( TyVar )
  33 import VarEnv     ( TyVarEnv )
  34 import VarSet     ( TyVarSet )
  35 import Name       ( Name )
  36 import BasicTypes ( IPName )
  37 import TyCon      ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
  38 import Class      ( Class )
  39 import Binary
  40
  41 -- others
  42 import PrelNames        ( superKindName, superBoxityName, liftedConName,
  43                           unliftedConName, typeConName, openKindConName,
  44                           usageKindConName, usOnceTyConName, usManyTyConName,
  45                           funTyConName
  46                         )
  47 \end{code}
  48
  49 %************************************************************************
  50 %*                                                                      *
  51 \subsection{Type Classifications}
  52 %*                                                                      *
  53 %************************************************************************
  54
  55 A type is
  56
  57         *unboxed*       iff its representation is other than a pointer
  58                         Unboxed types are also unlifted.
  59
  60         *lifted*        A type is lifted iff it has bottom as an element.
  61                         Closures always have lifted types:  i.e. any
  62                         let-bound identifier in Core must have a lifted
  63                         type.  Operationally, a lifted object is one that
  64                         can be entered.
  65
  66                         Only lifted types may be unified with a type variable.
  67
  68         *algebraic*     A type with one or more constructors, whether declared
  69                         with "data" or "newtype".
  70                         An algebraic type is one that can be deconstructed
  71                         with a case expression.
  72                         *NOT* the same as lifted types,  because we also
  73                         include unboxed tuples in this classification.
  74
  75         *data*          A type declared with "data".  Also boxed tuples.
  76
  77         *primitive*     iff it is a built-in type that can't be expressed
  78                         in Haskell.
  79
  80 Currently, all primitive types are unlifted, but that's not necessarily
  81 the case.  (E.g. Int could be primitive.)
  82
  83 Some primitive types are unboxed, such as Int#, whereas some are boxed
  84 but unlifted (such as ByteArray#).  The only primitive types that we
  85 classify as algebraic are the unboxed tuples.
  86
  87 examples of type classifications:
  88
  89 Type            primitive       boxed           lifted          algebraic
  90 -----------------------------------------------------------------------------
  91 Int#,           Yes             No              No              No
  92 ByteArray#      Yes             Yes             No              No
  93 (# a, b #)      Yes             No              No              Yes
  94 (  a, b  )      No              Yes             Yes             Yes
  95 [a]             No              Yes             Yes             Yes
  96
  97
  98
  99         ----------------------
 100         A note about newtypes
 101         ----------------------
 102
 103 Consider
 104         newtype N = MkN Int
 105
 106 Then we want N to be represented as an Int, and that's what we arrange.
 107 The front end of the compiler [TcType.lhs] treats N as opaque,
 108 the back end treats it as transparent [Type.lhs].
 109
 110 There's a bit of a problem with recursive newtypes
 111         newtype P = MkP P
 112         newtype Q = MkQ (Q->Q)
 113
 114 Here the 'implicit expansion' we get from treating P and Q as transparent
 115 would give rise to infinite types, which in turn makes eqType diverge.
 116 Similarly splitForAllTys and splitFunTys can get into a loop.
 117
 118 Solution: for recursive newtypes use a coerce, and treat the newtype
 119 and its representation as distinct right through the compiler.  That's
 120 what you get if you use recursive newtypes.  (They are rare, so who
 121 cares if they are a tiny bit less efficient.)
 122
 123 So: non-recursive newtypes are represented using a SourceTy (see below)
 124     recursive newtypes are represented using a TyConApp
 125
 126 The TyCon still says "I'm a newtype", but we do not represent the
 127 newtype application as a SourceType; instead as a TyConApp.
 128
 129
 130 %************************************************************************
 131 %*                                                                      *
 132 \subsection{The data type}
 133 %*                                                                      *
 134 %************************************************************************
 135
 136
 137 \begin{code}
 138 type SuperKind = Type
 139 type Kind      = Type
 140
 141 type TyVarSubst = TyVarEnv Type
 142
 143 data Type
 144   = TyVarTy TyVar
 145
 146   | AppTy
 147         Type            -- Function is *not* a TyConApp
 148         Type
 149
 150   | TyConApp            -- Application of a TyCon
 151         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 152                         --      synonyms have their own constructors, below.
 153         [Type]          -- Might not be saturated.
 154
 155   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 156         Type
 157         Type
 158
 159   | ForAllTy            -- A polymorphic type
 160         TyVar
 161         Type
 162
 163   | SourceTy            -- A high level source type
 164         SourceType      -- ...can be expanded to a representation type...
 165
 166   | NoteTy              -- A type with a note attached
 167         TyNote
 168         Type            -- The expanded version
 169
 170 data TyNote
 171   = FTVNote TyVarSet    -- The free type variables of the noted expression
 172
 173   | SynNote Type        -- Used for type synonyms
 174                         -- The Type is always a TyConApp, and is the un-expanded form.
 175                         -- The type to which the note is attached is the expanded form.
 176
 177 \end{code}
 178
 179 -------------------------------------
 180                 Source types
 181
 182 A type of the form
 183         SourceTy sty
 184 represents a value whose type is the Haskell source type sty.
 185 It can be expanded into its representation, but:
 186
 187         * The type checker must treat it as opaque
 188         * The rest of the compiler treats it as transparent
 189
 190 There are two main uses
 191         a) Haskell predicates
 192         b) newtypes
 193
 194 Consider these examples:
 195         f :: (Eq a) => a -> Int
 196         g :: (?x :: Int -> Int) => a -> Int
 197         h :: (r\l) => {r} => {l::Int | r}
 198
 199 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 200 Predicates are represented inside GHC by PredType:
 201
 202 \begin{code}
 203 data SourceType
 204   = ClassP Class [Type]         -- Class predicate
 205   | IParam (IPName Name) Type   -- Implicit parameter
 206   | NType TyCon [Type]          -- A *saturated*, *non-recursive* newtype application
 207                                 -- [See notes at top about newtypes]
 208
 209 type PredType  = SourceType     -- A subtype for predicates
 210 type ThetaType = [PredType]
 211 \end{code}
 212
 213 (We don't support TREX records yet, but the setup is designed
 214 to expand to allow them.)
 215
 216 A Haskell qualified type, such as that for f,g,h above, is
 217 represented using
 218         * a FunTy for the double arrow
 219         * with a PredTy as the function argument
 220
 221 The predicate really does turn into a real extra argument to the
 222 function.  If the argument has type (PredTy p) then the predicate p is
 223 represented by evidence (a dictionary, for example, of type (predRepTy p).
 224
 225
 226 %************************************************************************
 227 %*                                                                      *
 228 \subsection{Kinds}
 229 %*                                                                      *
 230 %************************************************************************
 231
 232 Kinds
 233 ~~~~~
 234 kind :: KX = kind -> kind
 235
 236            | Type liftedness    -- (Type *) is printed as just *
 237                                 -- (Type #) is printed as just #
 238
 239            | UsageKind          -- Printed '$'; used for usage annotations
 240
 241            | OpenKind           -- Can be lifted or unlifted
 242                                 -- Printed '?'
 243
 244            | kv                 -- A kind variable; *only* happens during kind checking
 245
 246 boxity :: BX = *        -- Lifted
 247              | #        -- Unlifted
 248              | bv       -- A boxity variable; *only* happens during kind checking
 249
 250 There's a little subtyping at the kind level:
 251         forall b. Type b <: OpenKind
 252
 253 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 254
 255 OpenKind, written '?', is used as the kind for certain type variables,
 256 in two situations:
 257
 258 1.  The universally quantified type variable(s) for special built-in
 259     things like error :: forall (a::?). String -> a.
 260     Here, the 'a' can be instantiated to a lifted or unlifted type.
 261
 262 2.  Kind '?' is also used when the typechecker needs to create a fresh
 263     type variable, one that may very well later be unified with a type.
 264     For example, suppose f::a, and we see an application (f x).  Then a
 265     must be a function type, so we unify a with (b->c).  But what kind
 266     are b and c?  They can be lifted or unlifted types, or indeed type schemes,
 267     so we give them kind '?'.
 268
 269     When the type checker generalises over a bunch of type variables, it
 270     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 271     present in an inferred type.
 272
 273
 274 ------------------------------------------
 275 Define  KX, the type of a kind
 276         BX, the type of a boxity
 277
 278 \begin{code}
 279 superKind :: SuperKind          -- KX, the type of all kinds
 280 superKind = TyConApp (mkSuperKindCon superKindName) []
 281
 282 superBoxity :: SuperKind                -- BX, the type of all boxities
 283 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 284 \end{code}
 285
 286 ------------------------------------------
 287 Define boxities: @*@ and @#@
 288
 289 \begin{code}
 290 liftedBoxity, unliftedBoxity :: Kind            -- :: BX
 291 liftedBoxity   = TyConApp liftedBoxityCon   []
 292 unliftedBoxity = TyConApp unliftedBoxityCon []
 293
 294 liftedBoxityCon   = mkKindCon liftedConName superBoxity
 295 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
 296 \end{code}
 297
 298 ------------------------------------------
 299 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
 300
 301 \begin{code}
 302 typeCon :: KindCon      -- :: BX -> KX
 303 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 304
 305 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 306
 307 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 308 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 309
 310 openKindCon     = mkKindCon openKindConName superKind
 311 openTypeKind    = TyConApp openKindCon []
 312
 313 usageKindCon     = mkKindCon usageKindConName superKind
 314 usageTypeKind    = TyConApp usageKindCon []
 315 \end{code}
 316
 317 ------------------------------------------
 318 Define arrow kinds
 319
 320 \begin{code}
 321 mkArrowKind :: Kind -> Kind -> Kind
 322 mkArrowKind k1 k2 = k1 `FunTy` k2
 323
 324 mkArrowKinds :: [Kind] -> Kind -> Kind
 325 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 326 \end{code}
 327
 328 -----------------------------------------------------------------------------
 329 Binary kinds for interface files
 330
 331 \begin{code}
 332 instance Binary Kind where
 333   put_ bh k@(TyConApp tc [])
 334         | tc == openKindCon  = putByte bh 0
 335         | tc == usageKindCon = putByte bh 1
 336   put_ bh k@(TyConApp tc [TyConApp bc _])
 337         | tc == typeCon && bc == liftedBoxityCon   = putByte bh 2
 338         | tc == typeCon && bc == unliftedBoxityCon = putByte bh 3
 339   put_ bh (FunTy f a) = do putByte bh 4;        put_ bh f; put_ bh a
 340   put_ bh _ = error "Binary.put(Kind): strange-looking Kind"
 341
 342   get bh = do
 343         b <- getByte bh
 344         case b of
 345           0 -> return openTypeKind
 346           1 -> return usageTypeKind
 347           2 -> return liftedTypeKind
 348           3 -> return unliftedTypeKind
 349           _ -> do f <- get bh; a <- get bh; return (FunTy f a)
 350 \end{code}
 351
 352 %************************************************************************
 353 %*                                                                      *
 354 \subsection{Wired-in type constructors
 355 %*                                                                      *
 356 %************************************************************************
 357
 358 We define a few wired-in type constructors here to avoid module knots
 359
 360 \begin{code}
 361 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 362 \end{code}
 363
 364 ------------------------------------------
 365 Usage tycons @.@ and @!@
 366
 367 The usage tycons are of kind usageTypeKind (`$').  The types contain
 368 no values, and are used purely for usage annotation.
 369
 370 \begin{code}
 371 usOnceTyCon     = mkKindCon usOnceTyConName usageTypeKind
 372 usOnce          = TyConApp usOnceTyCon []
 373
 374 usManyTyCon     = mkKindCon usManyTyConName usageTypeKind
 375 usMany          = TyConApp usManyTyCon []
 376 \end{code}
 377