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(..), IPName(..),     -- 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
  34 import VarSet
  35
  36 import Name     ( Name )
  37 import TyCon    ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
  38 import Class    ( Class )
  39
  40 -- others
  41 import PrelNames        ( superKindName, superBoxityName, liftedConName,
  42                           unliftedConName, typeConName, openKindConName,
  43                           usageKindConName, usOnceTyConName, usManyTyConName,
  44                           funTyConName
  45                         )
  46 \end{code}
  47
  48 %************************************************************************
  49 %*                                                                      *
  50 \subsection{Type Classifications}
  51 %*                                                                      *
  52 %************************************************************************
  53
  54 A type is
  55
  56         *unboxed*       iff its representation is other than a pointer
  57                         Unboxed types are also unlifted.
  58
  59         *lifted*        A type is lifted iff it has bottom as an element.
  60                         Closures always have lifted types:  i.e. any
  61                         let-bound identifier in Core must have a lifted
  62                         type.  Operationally, a lifted object is one that
  63                         can be entered.
  64
  65                         Only lifted types may be unified with a type variable.
  66
  67         *algebraic*     A type with one or more constructors, whether declared
  68                         with "data" or "newtype".
  69                         An algebraic type is one that can be deconstructed
  70                         with a case expression.
  71                         *NOT* the same as lifted types,  because we also
  72                         include unboxed tuples in this classification.
  73
  74         *data*          A type declared with "data".  Also boxed tuples.
  75
  76         *primitive*     iff it is a built-in type that can't be expressed
  77                         in Haskell.
  78
  79 Currently, all primitive types are unlifted, but that's not necessarily
  80 the case.  (E.g. Int could be primitive.)
  81
  82 Some primitive types are unboxed, such as Int#, whereas some are boxed
  83 but unlifted (such as ByteArray#).  The only primitive types that we
  84 classify as algebraic are the unboxed tuples.
  85
  86 examples of type classifications:
  87
  88 Type            primitive       boxed           lifted          algebraic
  89 -----------------------------------------------------------------------------
  90 Int#,           Yes             No              No              No
  91 ByteArray#      Yes             Yes             No              No
  92 (# a, b #)      Yes             No              No              Yes
  93 (  a, b  )      No              Yes             Yes             Yes
  94 [a]             No              Yes             Yes             Yes
  95
  96
  97
  98         ----------------------
  99         A note about newtypes
 100         ----------------------
 101
 102 Consider
 103         newtype N = MkN Int
 104
 105 Then we want N to be represented as an Int, and that's what we arrange.
 106 The front end of the compiler [TcType.lhs] treats N as opaque,
 107 the back end treats it as transparent [Type.lhs].
 108
 109 There's a bit of a problem with recursive newtypes
 110         newtype P = MkP P
 111         newtype Q = MkQ (Q->Q)
 112
 113 Here the 'implicit expansion' we get from treating P and Q as transparent
 114 would give rise to infinite types, which in turn makes eqType diverge.
 115 Similarly splitForAllTys and splitFunTys can get into a loop.
 116
 117 Solution: for recursive newtypes use a coerce, and treat the newtype
 118 and its representation as distinct right through the compiler.  That's
 119 what you get if you use recursive newtypes.  (They are rare, so who
 120 cares if they are a tiny bit less efficient.)
 121
 122 So: non-recursive newtypes are represented using a SourceTy (see below)
 123     recursive newtypes are represented using a TyConApp
 124
 125 The TyCon still says "I'm a newtype", but we do not represent the
 126 newtype application as a SourceType; instead as a TyConApp.
 127
 128
 129 %************************************************************************
 130 %*                                                                      *
 131 \subsection{The data type}
 132 %*                                                                      *
 133 %************************************************************************
 134
 135
 136 \begin{code}
 137 type SuperKind = Type
 138 type Kind      = 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
 211   = ClassP Class [Type]         -- Class predicate
 212   | IParam (IPName Name) Type   -- Implicit parameter
 213   | NType TyCon [Type]          -- A *saturated*, *non-recursive* newtype application
 214                                 -- [See notes at top about newtypes]
 215
 216 data IPName name
 217   = Dupable   name      -- ?x: you can freely duplicate this implicit parameter
 218   | MustSplit name      -- %x: you must use the splitting function to duplicate it
 219   deriving( Eq, Ord )   -- Ord is used in the IP name cache finite map
 220                         --      (used in HscTypes.OrigIParamCache)
 221         -- I sometimes thisnk this type should be in BasicTypes
 222
 223 type PredType  = SourceType     -- A subtype for predicates
 224 type ThetaType = [PredType]
 225 \end{code}
 226
 227 (We don't support TREX records yet, but the setup is designed
 228 to expand to allow them.)
 229
 230 A Haskell qualified type, such as that for f,g,h above, is
 231 represented using
 232         * a FunTy for the double arrow
 233         * with a PredTy as the function argument
 234
 235 The predicate really does turn into a real extra argument to the
 236 function.  If the argument has type (PredTy p) then the predicate p is
 237 represented by evidence (a dictionary, for example, of type (predRepTy p).
 238
 239
 240 %************************************************************************
 241 %*                                                                      *
 242 \subsection{Kinds}
 243 %*                                                                      *
 244 %************************************************************************
 245
 246 Kinds
 247 ~~~~~
 248 kind :: KX = kind -> kind
 249
 250            | Type liftedness    -- (Type *) is printed as just *
 251                                 -- (Type #) is printed as just #
 252
 253            | UsageKind          -- Printed '$'; used for usage annotations
 254
 255            | OpenKind           -- Can be lifted or unlifted
 256                                 -- Printed '?'
 257
 258            | kv                 -- A kind variable; *only* happens during kind checking
 259
 260 boxity :: BX = *        -- Lifted
 261              | #        -- Unlifted
 262              | bv       -- A boxity variable; *only* happens during kind checking
 263
 264 There's a little subtyping at the kind level:
 265         forall b. Type b <: OpenKind
 266
 267 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 268
 269 OpenKind, written '?', is used as the kind for certain type variables,
 270 in two situations:
 271
 272 1.  The universally quantified type variable(s) for special built-in
 273     things like error :: forall (a::?). String -> a.
 274     Here, the 'a' can be instantiated to a lifted or unlifted type.
 275
 276 2.  Kind '?' is also used when the typechecker needs to create a fresh
 277     type variable, one that may very well later be unified with a type.
 278     For example, suppose f::a, and we see an application (f x).  Then a
 279     must be a function type, so we unify a with (b->c).  But what kind
 280     are b and c?  They can be lifted or unlifted types, or indeed type schemes,
 281     so we give them kind '?'.
 282
 283     When the type checker generalises over a bunch of type variables, it
 284     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 285     present in an inferred type.
 286
 287
 288 ------------------------------------------
 289 Define  KX, the type of a kind
 290         BX, the type of a boxity
 291
 292 \begin{code}
 293 superKind :: SuperKind          -- KX, the type of all kinds
 294 superKind = TyConApp (mkSuperKindCon superKindName) []
 295
 296 superBoxity :: SuperKind                -- BX, the type of all boxities
 297 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 298 \end{code}
 299
 300 ------------------------------------------
 301 Define boxities: @*@ and @#@
 302
 303 \begin{code}
 304 liftedBoxity, unliftedBoxity :: Kind            -- :: BX
 305 liftedBoxity  = TyConApp (mkKindCon liftedConName superBoxity) []
 306
 307 unliftedBoxity  = TyConApp (mkKindCon unliftedConName superBoxity) []
 308 \end{code}
 309
 310 ------------------------------------------
 311 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
 312
 313 \begin{code}
 314 typeCon :: KindCon      -- :: BX -> KX
 315 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 316
 317 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 318
 319 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 320 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 321
 322 openKindCon     = mkKindCon openKindConName superKind
 323 openTypeKind    = TyConApp openKindCon []
 324
 325 usageKindCon     = mkKindCon usageKindConName superKind
 326 usageTypeKind    = TyConApp usageKindCon []
 327 \end{code}
 328
 329 ------------------------------------------
 330 Define arrow kinds
 331
 332 \begin{code}
 333 mkArrowKind :: Kind -> Kind -> Kind
 334 mkArrowKind k1 k2 = k1 `FunTy` k2
 335
 336 mkArrowKinds :: [Kind] -> Kind -> Kind
 337 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 338 \end{code}
 339
 340
 341 %************************************************************************
 342 %*                                                                      *
 343 \subsection{Wired-in type constructors
 344 %*                                                                      *
 345 %************************************************************************
 346
 347 We define a few wired-in type constructors here to avoid module knots
 348
 349 \begin{code}
 350 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 351 \end{code}
 352
 353 ------------------------------------------
 354 Usage tycons @.@ and @!@
 355
 356 The usage tycons are of kind usageTypeKind (`$').  The types contain
 357 no values, and are used purely for usage annotation.
 358
 359 \begin{code}
 360 usOnceTyCon     = mkKindCon usOnceTyConName usageTypeKind
 361 usOnce          = TyConApp usOnceTyCon []
 362
 363 usManyTyCon     = mkKindCon usManyTyConName usageTypeKind
 364 usMany          = TyConApp usManyTyCon []
 365 \end{code}
 366