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 NOTE: currently [March 02] we regard a newtype as 'recursive' if it's in a
 131 mutually recursive group.  That's a bit conservative: only if there's a loop
 132 consisting only of newtypes do we need consider it as recursive.  But it's
 133 not so easy to discover that, and the situation isn't that common.
 134
 135
 136 %************************************************************************
 137 %*                                                                      *
 138 \subsection{The data type}
 139 %*                                                                      *
 140 %************************************************************************
 141
 142
 143 \begin{code}
 144 type SuperKind = Type
 145 type Kind      = Type
 146
 147 type TyVarSubst = TyVarEnv Type
 148
 149 data Type
 150   = TyVarTy TyVar
 151
 152   | AppTy
 153         Type            -- Function is *not* a TyConApp
 154         Type
 155
 156   | TyConApp            -- Application of a TyCon
 157         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 158                         --      synonyms have their own constructors, below.
 159         [Type]          -- Might not be saturated.
 160
 161   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 162         Type
 163         Type
 164
 165   | ForAllTy            -- A polymorphic type
 166         TyVar
 167         Type
 168
 169   | SourceTy            -- A high level source type
 170         SourceType      -- ...can be expanded to a representation type...
 171
 172   | NoteTy              -- A type with a note attached
 173         TyNote
 174         Type            -- The expanded version
 175
 176 data TyNote
 177   = FTVNote TyVarSet    -- The free type variables of the noted expression
 178
 179   | SynNote Type        -- Used for type synonyms
 180                         -- The Type is always a TyConApp, and is the un-expanded form.
 181                         -- The type to which the note is attached is the expanded form.
 182
 183 \end{code}
 184
 185 -------------------------------------
 186                 Source types
 187
 188 A type of the form
 189         SourceTy sty
 190 represents a value whose type is the Haskell source type sty.
 191 It can be expanded into its representation, but:
 192
 193         * The type checker must treat it as opaque
 194         * The rest of the compiler treats it as transparent
 195
 196 There are two main uses
 197         a) Haskell predicates
 198         b) newtypes
 199
 200 Consider these examples:
 201         f :: (Eq a) => a -> Int
 202         g :: (?x :: Int -> Int) => a -> Int
 203         h :: (r\l) => {r} => {l::Int | r}
 204
 205 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 206 Predicates are represented inside GHC by PredType:
 207
 208 \begin{code}
 209 data SourceType
 210   = ClassP Class [Type]         -- Class predicate
 211   | IParam (IPName Name) Type   -- Implicit parameter
 212   | NType TyCon [Type]          -- A *saturated*, *non-recursive* newtype application
 213                                 -- [See notes at top about newtypes]
 214
 215 type PredType  = SourceType     -- A subtype for predicates
 216 type ThetaType = [PredType]
 217 \end{code}
 218
 219 (We don't support TREX records yet, but the setup is designed
 220 to expand to allow them.)
 221
 222 A Haskell qualified type, such as that for f,g,h above, is
 223 represented using
 224         * a FunTy for the double arrow
 225         * with a PredTy as the function argument
 226
 227 The predicate really does turn into a real extra argument to the
 228 function.  If the argument has type (PredTy p) then the predicate p is
 229 represented by evidence (a dictionary, for example, of type (predRepTy p).
 230
 231
 232 %************************************************************************
 233 %*                                                                      *
 234 \subsection{Kinds}
 235 %*                                                                      *
 236 %************************************************************************
 237
 238 Kinds
 239 ~~~~~
 240 kind :: KX = kind -> kind
 241
 242            | Type liftedness    -- (Type *) is printed as just *
 243                                 -- (Type #) is printed as just #
 244
 245            | UsageKind          -- Printed '$'; used for usage annotations
 246
 247            | OpenKind           -- Can be lifted or unlifted
 248                                 -- Printed '?'
 249
 250            | kv                 -- A kind variable; *only* happens during kind checking
 251
 252 boxity :: BX = *        -- Lifted
 253              | #        -- Unlifted
 254              | bv       -- A boxity variable; *only* happens during kind checking
 255
 256 There's a little subtyping at the kind level:
 257         forall b. Type b <: OpenKind
 258
 259 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 260
 261 OpenKind, written '?', is used as the kind for certain type variables,
 262 in two situations:
 263
 264 1.  The universally quantified type variable(s) for special built-in
 265     things like error :: forall (a::?). String -> a.
 266     Here, the 'a' can be instantiated to a lifted or unlifted type.
 267
 268 2.  Kind '?' is also used when the typechecker needs to create a fresh
 269     type variable, one that may very well later be unified with a type.
 270     For example, suppose f::a, and we see an application (f x).  Then a
 271     must be a function type, so we unify a with (b->c).  But what kind
 272     are b and c?  They can be lifted or unlifted types, or indeed type schemes,
 273     so we give them kind '?'.
 274
 275     When the type checker generalises over a bunch of type variables, it
 276     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 277     present in an inferred type.
 278
 279
 280 ------------------------------------------
 281 Define  KX, the type of a kind
 282         BX, the type of a boxity
 283
 284 \begin{code}
 285 superKind :: SuperKind          -- KX, the type of all kinds
 286 superKind = TyConApp (mkSuperKindCon superKindName) []
 287
 288 superBoxity :: SuperKind                -- BX, the type of all boxities
 289 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 290 \end{code}
 291
 292 ------------------------------------------
 293 Define boxities: @*@ and @#@
 294
 295 \begin{code}
 296 liftedBoxity, unliftedBoxity :: Kind            -- :: BX
 297 liftedBoxity   = TyConApp liftedBoxityCon   []
 298 unliftedBoxity = TyConApp unliftedBoxityCon []
 299
 300 liftedBoxityCon   = mkKindCon liftedConName superBoxity
 301 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
 302 \end{code}
 303
 304 ------------------------------------------
 305 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
 306
 307 \begin{code}
 308 typeCon :: KindCon      -- :: BX -> KX
 309 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 310
 311 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 312
 313 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 314 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 315
 316 openKindCon     = mkKindCon openKindConName superKind
 317 openTypeKind    = TyConApp openKindCon []
 318
 319 usageKindCon     = mkKindCon usageKindConName superKind
 320 usageTypeKind    = TyConApp usageKindCon []
 321 \end{code}
 322
 323 ------------------------------------------
 324 Define arrow kinds
 325
 326 \begin{code}
 327 mkArrowKind :: Kind -> Kind -> Kind
 328 mkArrowKind k1 k2 = k1 `FunTy` k2
 329
 330 mkArrowKinds :: [Kind] -> Kind -> Kind
 331 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 332 \end{code}
 333
 334 -----------------------------------------------------------------------------
 335 Binary kinds for interface files
 336
 337 \begin{code}
 338 instance Binary Kind where
 339   put_ bh k@(TyConApp tc [])
 340         | tc == openKindCon  = putByte bh 0
 341         | tc == usageKindCon = putByte bh 1
 342   put_ bh k@(TyConApp tc [TyConApp bc _])
 343         | tc == typeCon && bc == liftedBoxityCon   = putByte bh 2
 344         | tc == typeCon && bc == unliftedBoxityCon = putByte bh 3
 345   put_ bh (FunTy f a) = do putByte bh 4;        put_ bh f; put_ bh a
 346   put_ bh _ = error "Binary.put(Kind): strange-looking Kind"
 347
 348   get bh = do
 349         b <- getByte bh
 350         case b of
 351           0 -> return openTypeKind
 352           1 -> return usageTypeKind
 353           2 -> return liftedTypeKind
 354           3 -> return unliftedTypeKind
 355           _ -> do f <- get bh; a <- get bh; return (FunTy f a)
 356 \end{code}
 357
 358 %************************************************************************
 359 %*                                                                      *
 360 \subsection{Wired-in type constructors
 361 %*                                                                      *
 362 %************************************************************************
 363
 364 We define a few wired-in type constructors here to avoid module knots
 365
 366 \begin{code}
 367 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 368         -- You might think that (->) should have type (? -> ? -> *), and you'd be right
 369         -- But if we do that we get kind errors when saying
 370         --      instance Control.Arrow (->)
 371         -- becuase the expected kind is (*->*->*).  The trouble is that the
 372         -- expected/actual stuff in the unifier does not go contra-variant, whereas
 373         -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
 374         -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
 375 \end{code}
 376
 377 ------------------------------------------
 378 Usage tycons @.@ and @!@
 379
 380 The usage tycons are of kind usageTypeKind (`$').  The types contain
 381 no values, and are used purely for usage annotation.
 382
 383 \begin{code}
 384 usOnceTyCon     = mkKindCon usOnceTyConName usageTypeKind
 385 usOnce          = TyConApp usOnceTyCon []
 386
 387 usManyTyCon     = mkKindCon usManyTyConName usageTypeKind
 388 usMany          = TyConApp usManyTyCon []
 389 \end{code}
 390