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 The TyCon still says "I'm a newtype", but we do not represent the
 122 newtype application as a SourceType; instead as a TyConApp.
 123
 124
 125 %************************************************************************
 126 %*                                                                      *
 127 \subsection{The data type}
 128 %*                                                                      *
 129 %************************************************************************
 130
 131
 132 \begin{code}
 133 type SuperKind = Type
 134 type Kind      = Type
 135 type TauType   = Type
 136
 137 type TyVarSubst = TyVarEnv Type
 138
 139 data Type
 140   = TyVarTy TyVar
 141
 142   | AppTy
 143         Type            -- Function is *not* a TyConApp
 144         Type
 145
 146   | TyConApp            -- Application of a TyCon
 147         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 148                         --      synonyms have their own constructors, below.
 149         [Type]          -- Might not be saturated.
 150
 151   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 152         Type
 153         Type
 154
 155   | ForAllTy            -- A polymorphic type
 156         TyVar
 157         Type
 158
 159   | SourceTy            -- A high level source type
 160         SourceType      -- ...can be expanded to a representation type...
 161
 162   | UsageTy             -- A usage-annotated type
 163         Type            --   - Annotation of kind $ (i.e., usage annotation)
 164         Type            --   - Annotated 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 \end{code}
 177
 178 INVARIANT: UsageTys are optional, but may *only* appear immediately
 179 under a FunTy (either argument), or at top-level of a Type permitted
 180 to be annotated (such as the type of an Id).  NoteTys are transparent
 181 for the purposes of this rule.
 182
 183 -------------------------------------
 184                 Source types
 185
 186 A type of the form
 187         SourceTy sty
 188 represents a value whose type is the Haskell source type sty.
 189 It can be expanded into its representation, but:
 190
 191         * The type checker must treat it as opaque
 192         * The rest of the compiler treats it as transparent
 193
 194 There are two main uses
 195         a) Haskell predicates
 196         b) newtypes
 197
 198 Consider these examples:
 199         f :: (Eq a) => a -> Int
 200         g :: (?x :: Int -> Int) => a -> Int
 201         h :: (r\l) => {r} => {l::Int | r}
 202
 203 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 204 Predicates are represented inside GHC by PredType:
 205
 206 \begin{code}
 207 data SourceType  = ClassP Class [Type]          -- Class predicate
 208                  | IParam Name  Type            -- Implicit parameter
 209                  | NType TyCon [Type]           -- A *saturated*, *non-recursive* newtype application
 210                                                 -- [See notes at top about newtypes]
 211
 212 type PredType  = SourceType     -- A subtype for predicates
 213 type ThetaType = [PredType]
 214 \end{code}
 215
 216 (We don't support TREX records yet, but the setup is designed
 217 to expand to allow them.)
 218
 219 A Haskell qualified type, such as that for f,g,h above, is
 220 represented using
 221         * a FunTy for the double arrow
 222         * with a PredTy as the function argument
 223
 224 The predicate really does turn into a real extra argument to the
 225 function.  If the argument has type (PredTy p) then the predicate p is
 226 represented by evidence (a dictionary, for example, of type (predRepTy p).
 227
 228
 229 %************************************************************************
 230 %*                                                                      *
 231 \subsection{Kinds}
 232 %*                                                                      *
 233 %************************************************************************
 234
 235 Kinds
 236 ~~~~~
 237 kind :: KX = kind -> kind
 238
 239            | Type liftedness    -- (Type *) is printed as just *
 240                                 -- (Type #) is printed as just #
 241
 242            | UsageKind          -- Printed '$'; used for usage annotations
 243
 244            | OpenKind           -- Can be lifted or unlifted
 245                                 -- Printed '?'
 246
 247            | kv                 -- A kind variable; *only* happens during kind checking
 248
 249 boxity :: BX = *        -- Lifted
 250              | #        -- Unlifted
 251              | bv       -- A boxity variable; *only* happens during kind checking
 252
 253 There's a little subtyping at the kind level:
 254         forall b. Type b <: OpenKind
 255
 256 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 257
 258 OpenKind, written '?', is used as the kind for certain type variables,
 259 in two situations:
 260
 261 1.  The universally quantified type variable(s) for special built-in
 262     things like error :: forall (a::?). String -> a.
 263     Here, the 'a' can be instantiated to a lifted or unlifted type.
 264
 265 2.  Kind '?' is also used when the typechecker needs to create a fresh
 266     type variable, one that may very well later be unified with a type.
 267     For example, suppose f::a, and we see an application (f x).  Then a
 268     must be a function type, so we unify a with (b->c).  But what kind
 269     are b and c?  They can be lifted or unlifted types, so we give them
 270     kind '?'.
 271
 272     When the type checker generalises over a bunch of type variables, it
 273     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 274     present in an inferred type.
 275
 276
 277 ------------------------------------------
 278 Define  KX, the type of a kind
 279         BX, the type of a boxity
 280
 281 \begin{code}
 282 superKind :: SuperKind          -- KX, the type of all kinds
 283 superKind = TyConApp (mkSuperKindCon superKindName) []
 284
 285 superBoxity :: SuperKind                -- BX, the type of all boxities
 286 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 287 \end{code}
 288
 289 ------------------------------------------
 290 Define boxities: @*@ and @#@
 291
 292 \begin{code}
 293 liftedBoxity, unliftedBoxity :: Kind            -- :: BX
 294 liftedBoxity  = TyConApp (mkKindCon liftedConName superBoxity) []
 295
 296 unliftedBoxity  = TyConApp (mkKindCon unliftedConName superBoxity) []
 297 \end{code}
 298
 299 ------------------------------------------
 300 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
 301
 302 \begin{code}
 303 typeCon :: KindCon      -- :: BX -> KX
 304 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 305
 306 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 307
 308 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 309 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 310
 311 openKindCon     = mkKindCon openKindConName superKind
 312 openTypeKind    = TyConApp openKindCon []
 313
 314 usageKindCon     = mkKindCon usageKindConName superKind
 315 usageTypeKind    = TyConApp usageKindCon []
 316 \end{code}
 317
 318 ------------------------------------------
 319 Define arrow kinds
 320
 321 \begin{code}
 322 mkArrowKind :: Kind -> Kind -> Kind
 323 mkArrowKind k1 k2 = k1 `FunTy` k2
 324
 325 mkArrowKinds :: [Kind] -> Kind -> Kind
 326 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 327 \end{code}
 328
 329
 330 %************************************************************************
 331 %*                                                                      *
 332 \subsection{Wired-in type constructors
 333 %*                                                                      *
 334 %************************************************************************
 335
 336 We define a few wired-in type constructors here to avoid module knots
 337
 338 \begin{code}
 339 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 340 \end{code}
 341
 342 ------------------------------------------
 343 Usage tycons @.@ and @!@
 344
 345 The usage tycons are of kind usageTypeKind (`$').  The types contain
 346 no values, and are used purely for usage annotation.
 347
 348 \begin{code}
 349 usOnceTyCon     = mkKindCon usOnceTyConName usageTypeKind
 350 usOnce          = TyConApp usOnceTyCon []
 351
 352 usManyTyCon     = mkKindCon usManyTyConName usageTypeKind
 353 usMany          = TyConApp usManyTyCon []
 354 \end{code}
 355