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(..), SourceType(..),           -- Representation visible to friends
   9
  10         Kind, TauType, PredType, ThetaType,             -- Synonyms
  11         TyVarSubst,
  12
  13         superKind, superBoxity,                         -- KX and BX respectively
  14         liftedBoxity, unliftedBoxity,                   -- :: BX
  15         openKindCon,                                    -- :: KX
  16         typeCon,                                        -- :: BX -> KX
  17         liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
  18         mkArrowKind, mkArrowKinds,                      -- :: KX -> KX -> KX
  19
  20         usageKindCon,                                   -- :: KX
  21         usageTypeKind,                                  -- :: KX
  22         usOnceTyCon, usManyTyCon,                       -- :: $
  23         usOnce, usMany,                                 -- :: $
  24
  25         funTyCon
  26     ) where
  27
  28 #include "HsVersions.h"
  29
  30 -- friends:
  31 import Var      ( TyVar )
  32 import VarEnv
  33 import VarSet
  34
  35 import Name     ( Name )
  36 import TyCon    ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
  37 import Class    ( Class )
  38
  39 -- others
  40 import PrelNames        ( superKindName, superBoxityName, liftedConName,
  41                           unliftedConName, typeConName, openKindConName,
  42                           usageKindConName, usOnceTyConName, usManyTyConName,
  43                           funTyConName
  44                         )
  45 \end{code}
  46
  47 %************************************************************************
  48 %*                                                                      *
  49 \subsection{Type Classifications}
  50 %*                                                                      *
  51 %************************************************************************
  52
  53 A type is
  54
  55         *unboxed*       iff its representation is other than a pointer
  56                         Unboxed types are also unlifted.
  57
  58         *lifted*        A type is lifted iff it has bottom as an element.
  59                         Closures always have lifted types:  i.e. any
  60                         let-bound identifier in Core must have a lifted
  61                         type.  Operationally, a lifted object is one that
  62                         can be entered.
  63
  64                         Only lifted types may be unified with a type variable.
  65
  66         *algebraic*     A type with one or more constructors, whether declared
  67                         with "data" or "newtype".
  68                         An algebraic type is one that can be deconstructed
  69                         with a case expression.
  70                         *NOT* the same as lifted types,  because we also
  71                         include unboxed tuples in this classification.
  72
  73         *data*          A type declared with "data".  Also boxed tuples.
  74
  75         *primitive*     iff it is a built-in type that can't be expressed
  76                         in Haskell.
  77
  78 Currently, all primitive types are unlifted, but that's not necessarily
  79 the case.  (E.g. Int could be primitive.)
  80
  81 Some primitive types are unboxed, such as Int#, whereas some are boxed
  82 but unlifted (such as ByteArray#).  The only primitive types that we
  83 classify as algebraic are the unboxed tuples.
  84
  85 examples of type classifications:
  86
  87 Type            primitive       boxed           lifted          algebraic
  88 -----------------------------------------------------------------------------
  89 Int#,           Yes             No              No              No
  90 ByteArray#      Yes             Yes             No              No
  91 (# a, b #)      Yes             No              No              Yes
  92 (  a, b  )      No              Yes             Yes             Yes
  93 [a]             No              Yes             Yes             Yes
  94
  95
  96
  97         ----------------------
  98         A note about newtypes
  99         ----------------------
 100
 101 Consider
 102         newtype N = MkN Int
 103
 104 Then we want N to be represented as an Int, and that's what we arrange.
 105 The front end of the compiler [TcType.lhs] treats N as opaque,
 106 the back end treats it as transparent [Type.lhs].
 107
 108 There's a bit of a problem with recursive newtypes
 109         newtype P = MkP P
 110         newtype Q = MkQ (Q->Q)
 111
 112 Here the 'implicit expansion' we get from treating P and Q as transparent
 113 would give rise to infinite types, which in turn makes eqType diverge.
 114 Similarly splitForAllTys and splitFunTys can get into a loop.
 115
 116 Solution: for recursive newtypes use a coerce, and treat the newtype
 117 and its representation as distinct right through the compiler.  That's
 118 what you get if you use recursive newtypes.  (They are rare, so who
 119 cares if they are a tiny bit less efficient.)
 120
 121 So: non-recursive newtypes are represented using a SourceTy (see below)
 122     recursive newtypes are represented using a TyConApp
 123
 124 The TyCon still says "I'm a newtype", but we do not represent the
 125 newtype application as a SourceType; instead as a TyConApp.
 126
 127
 128 %************************************************************************
 129 %*                                                                      *
 130 \subsection{The data type}
 131 %*                                                                      *
 132 %************************************************************************
 133
 134
 135 \begin{code}
 136 type SuperKind = Type
 137 type Kind      = Type
 138 type TauType   = Type
 139
 140 type TyVarSubst = TyVarEnv Type
 141
 142 data Type
 143   = TyVarTy TyVar
 144
 145   | AppTy
 146         Type            -- Function is *not* a TyConApp
 147         Type
 148
 149   | TyConApp            -- Application of a TyCon
 150         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 151                         --      synonyms have their own constructors, below.
 152         [Type]          -- Might not be saturated.
 153
 154   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 155         Type
 156         Type
 157
 158   | ForAllTy            -- A polymorphic type
 159         TyVar
 160         Type
 161
 162   | SourceTy            -- A high level source type
 163         SourceType      -- ...can be expanded to a representation type...
 164
 165   | UsageTy             -- A usage-annotated type
 166         Type            --   - Annotation of kind $ (i.e., usage annotation)
 167         Type            --   - Annotated type
 168
 169   | NoteTy              -- A type with a note attached
 170         TyNote
 171         Type            -- The expanded version
 172
 173 data TyNote
 174   = FTVNote TyVarSet    -- The free type variables of the noted expression
 175
 176   | SynNote Type        -- Used for type synonyms
 177                         -- The Type is always a TyConApp, and is the un-expanded form.
 178                         -- The type to which the note is attached is the expanded form.
 179 \end{code}
 180
 181 INVARIANT: UsageTys are optional, but may *only* appear immediately
 182 under a FunTy (either argument), or at top-level of a Type permitted
 183 to be annotated (such as the type of an Id).  NoteTys are transparent
 184 for the purposes of this rule.
 185
 186 -------------------------------------
 187                 Source types
 188
 189 A type of the form
 190         SourceTy sty
 191 represents a value whose type is the Haskell source type sty.
 192 It can be expanded into its representation, but:
 193
 194         * The type checker must treat it as opaque
 195         * The rest of the compiler treats it as transparent
 196
 197 There are two main uses
 198         a) Haskell predicates
 199         b) newtypes
 200
 201 Consider these examples:
 202         f :: (Eq a) => a -> Int
 203         g :: (?x :: Int -> Int) => a -> Int
 204         h :: (r\l) => {r} => {l::Int | r}
 205
 206 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 207 Predicates are represented inside GHC by PredType:
 208
 209 \begin{code}
 210 data SourceType  = ClassP Class [Type]          -- Class predicate
 211                  | IParam 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, so we give them
 273     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 (mkKindCon liftedConName superBoxity) []
 298
 299 unliftedBoxity  = TyConApp (mkKindCon unliftedConName superBoxity) []
 300 \end{code}
 301
 302 ------------------------------------------
 303 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
 304
 305 \begin{code}
 306 typeCon :: KindCon      -- :: BX -> KX
 307 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 308
 309 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 310
 311 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 312 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 313
 314 openKindCon     = mkKindCon openKindConName superKind
 315 openTypeKind    = TyConApp openKindCon []
 316
 317 usageKindCon     = mkKindCon usageKindConName superKind
 318 usageTypeKind    = TyConApp usageKindCon []
 319 \end{code}
 320
 321 ------------------------------------------
 322 Define arrow kinds
 323
 324 \begin{code}
 325 mkArrowKind :: Kind -> Kind -> Kind
 326 mkArrowKind k1 k2 = k1 `FunTy` k2
 327
 328 mkArrowKinds :: [Kind] -> Kind -> Kind
 329 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 330 \end{code}
 331
 332
 333 %************************************************************************
 334 %*                                                                      *
 335 \subsection{Wired-in type constructors
 336 %*                                                                      *
 337 %************************************************************************
 338
 339 We define a few wired-in type constructors here to avoid module knots
 340
 341 \begin{code}
 342 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 343 \end{code}
 344
 345 ------------------------------------------
 346 Usage tycons @.@ and @!@
 347
 348 The usage tycons are of kind usageTypeKind (`$').  The types contain
 349 no values, and are used purely for usage annotation.
 350
 351 \begin{code}
 352 usOnceTyCon     = mkKindCon usOnceTyConName usageTypeKind
 353 usOnce          = TyConApp usOnceTyCon []
 354
 355 usManyTyCon     = mkKindCon usManyTyConName usageTypeKind
 356 usMany          = TyConApp usManyTyCon []
 357 \end{code}
 358