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(..), PredType(..),             -- Representation visible to friends
   9
  10         Kind, ThetaType, RhoType, TauType, SigmaType,           -- Synonyms
  11         TyVarSubst,
  12
  13         superKind, superBoxity,                         -- KX and BX respectively
  14         boxedBoxity, unboxedBoxity,                     -- :: BX
  15         openKindCon,                                    -- :: KX
  16         typeCon,                                        -- :: BX -> KX
  17         boxedTypeKind, unboxedTypeKind, 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, tcName )
  36 import TyCon    ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
  37 import Class    ( Class )
  38
  39 -- others
  40 import PrelNames        ( superKindName, superBoxityName, boxedConName,
  41                           unboxedConName, typeConName, openKindConName, funTyConName,
  42                           usageKindConName, usOnceTyConName, usManyTyConName
  43                         )
  44 \end{code}
  45
  46 %************************************************************************
  47 %*                                                                      *
  48 \subsection{Type Classifications}
  49 %*                                                                      *
  50 %************************************************************************
  51
  52 A type is
  53
  54         *unboxed*       iff its representation is other than a pointer
  55                         Unboxed types cannot instantiate a type variable.
  56                         Unboxed types are always 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                         (NOTE: previously "pointed").
  64
  65         *algebraic*     A type with one or more constructors, whether declared
  66                         with "data" or "newtype".
  67                         An algebraic type is one that can be deconstructed
  68                         with a case expression.
  69                         *NOT* the same as lifted types,  because we also
  70                         include unboxed tuples in this classification.
  71
  72         *data*          A type declared with "data".  Also boxed tuples.
  73
  74         *primitive*     iff it is a built-in type that can't be expressed
  75                         in Haskell.
  76
  77 Currently, all primitive types are unlifted, but that's not necessarily
  78 the case.  (E.g. Int could be primitive.)
  79
  80 Some primitive types are unboxed, such as Int#, whereas some are boxed
  81 but unlifted (such as ByteArray#).  The only primitive types that we
  82 classify as algebraic are the unboxed tuples.
  83
  84 examples of type classifications:
  85
  86 Type            primitive       boxed           lifted          algebraic
  87 -----------------------------------------------------------------------------
  88 Int#,           Yes             No              No              No
  89 ByteArray#      Yes             Yes             No              No
  90 (# a, b #)      Yes             No              No              Yes
  91 (  a, b  )      No              Yes             Yes             Yes
  92 [a]             No              Yes             Yes             Yes
  93
  94 %************************************************************************
  95 %*                                                                      *
  96 \subsection{The data type}
  97 %*                                                                      *
  98 %************************************************************************
  99
 100
 101 \begin{code}
 102 type SuperKind = Type
 103 type Kind      = Type
 104
 105 type TyVarSubst = TyVarEnv Type
 106
 107 data Type
 108   = TyVarTy TyVar
 109
 110   | AppTy
 111         Type            -- Function is *not* a TyConApp
 112         Type
 113
 114   | TyConApp            -- Application of a TyCon
 115         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 116                         --      synonyms have their own constructors, below.
 117         [Type]          -- Might not be saturated.
 118
 119   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 120         Type
 121         Type
 122
 123   | ForAllTy            -- A polymorphic type
 124         TyVar
 125         Type
 126
 127   | PredTy              -- A Haskell predicate
 128         PredType
 129
 130   | UsageTy             -- A usage-annotated type
 131         Type            --   - Annotation of kind $ (i.e., usage annotation)
 132         Type            --   - Annotated type
 133
 134   | NoteTy              -- A type with a note attached
 135         TyNote
 136         Type            -- The expanded version
 137
 138 data TyNote
 139   = SynNote Type        -- The unexpanded version of the type synonym; always a TyConApp
 140   | FTVNote TyVarSet    -- The free type variables of the noted expression
 141
 142 type ThetaType    = [PredType]
 143 type RhoType      = Type
 144 type TauType      = Type
 145 type SigmaType    = Type
 146 \end{code}
 147
 148 INVARIANT: UsageTys are optional, but may *only* appear immediately
 149 under a FunTy (either argument), or at top-level of a Type permitted
 150 to be annotated (such as the type of an Id).  NoteTys are transparent
 151 for the purposes of this rule.
 152
 153 -------------------------------------
 154                 Predicates
 155
 156 Consider these examples:
 157         f :: (Eq a) => a -> Int
 158         g :: (?x :: Int -> Int) => a -> Int
 159         h :: (r\l) => {r} => {l::Int | r}
 160
 161 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 162 Predicates are represented inside GHC by PredType:
 163
 164 \begin{code}
 165 data PredType  = Class  Class [Type]
 166                | IParam Name  Type
 167 \end{code}
 168
 169 (We don't support TREX records yet, but the setup is designed
 170 to expand to allow them.)
 171
 172 A Haskell qualified type, such as that for f,g,h above, is
 173 represented using
 174         * a FunTy for the double arrow
 175         * with a PredTy as the function argument
 176
 177 The predicate really does turn into a real extra argument to the
 178 function.  If the argument has type (PredTy p) then the predicate p is
 179 represented by evidence (a dictionary, for example, of type (predRepTy p).
 180
 181
 182 %************************************************************************
 183 %*                                                                      *
 184 \subsection{Kinds}
 185 %*                                                                      *
 186 %************************************************************************
 187
 188 Kinds
 189 ~~~~~
 190 kind :: KX = kind -> kind
 191
 192            | Type boxity        -- (Type *) is printed as just *
 193                                 -- (Type #) is printed as just #
 194
 195            | UsageKind          -- Printed '$'; used for usage annotations
 196
 197            | OpenKind           -- Can be boxed or unboxed
 198                                 -- Printed '?'
 199
 200            | kv                 -- A kind variable; *only* happens during kind checking
 201
 202 boxity :: BX = *        -- Boxed
 203              | #        -- Unboxed
 204              | bv       -- A boxity variable; *only* happens during kind checking
 205
 206 There's a little subtyping at the kind level:
 207         forall b. Type b <: OpenKind
 208
 209 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 210
 211 OpenKind, written '?', is used as the kind for certain type variables,
 212 in two situations:
 213
 214 1.  The universally quantified type variable(s) for special built-in
 215     things like error :: forall (a::?). String -> a.
 216     Here, the 'a' can be instantiated to a boxed or unboxed type.
 217
 218 2.  Kind '?' is also used when the typechecker needs to create a fresh
 219     type variable, one that may very well later be unified with a type.
 220     For example, suppose f::a, and we see an application (f x).  Then a
 221     must be a function type, so we unify a with (b->c).  But what kind
 222     are b and c?  They can be boxed or unboxed types, so we give them kind '?'.
 223
 224     When the type checker generalises over a bunch of type variables, it
 225     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 226     present in an inferred type.
 227
 228
 229 ------------------------------------------
 230 Define  KX, the type of a kind
 231         BX, the type of a boxity
 232
 233 \begin{code}
 234 superKind :: SuperKind          -- KX, the type of all kinds
 235 superKind = TyConApp (mkSuperKindCon superKindName) []
 236
 237 superBoxity :: SuperKind                -- BX, the type of all boxities
 238 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 239 \end{code}
 240
 241 ------------------------------------------
 242 Define boxities: @*@ and @#@
 243
 244 \begin{code}
 245 boxedBoxity, unboxedBoxity :: Kind              -- :: BX
 246 boxedBoxity  = TyConApp (mkKindCon boxedConName superBoxity) []
 247
 248 unboxedBoxity  = TyConApp (mkKindCon unboxedConName superBoxity) []
 249 \end{code}
 250
 251 ------------------------------------------
 252 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
 253
 254 \begin{code}
 255 typeCon :: KindCon      -- :: BX -> KX
 256 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 257
 258 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind    -- Of superkind superKind
 259
 260 boxedTypeKind   = TyConApp typeCon [boxedBoxity]
 261 unboxedTypeKind = TyConApp typeCon [unboxedBoxity]
 262
 263 openKindCon     = mkKindCon openKindConName superKind
 264 openTypeKind    = TyConApp openKindCon []
 265
 266 usageKindCon     = mkKindCon usageKindConName superKind
 267 usageTypeKind    = TyConApp usageKindCon []
 268 \end{code}
 269
 270 ------------------------------------------
 271 Define arrow kinds
 272
 273 \begin{code}
 274 mkArrowKind :: Kind -> Kind -> Kind
 275 mkArrowKind k1 k2 = k1 `FunTy` k2
 276
 277 mkArrowKinds :: [Kind] -> Kind -> Kind
 278 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 279 \end{code}
 280
 281
 282 %************************************************************************
 283 %*                                                                      *
 284 \subsection{Wired-in type constructors
 285 %*                                                                      *
 286 %************************************************************************
 287
 288 We define a few wired-in type constructors here to avoid module knots
 289
 290 \begin{code}
 291 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
 292 \end{code}
 293
 294 ------------------------------------------
 295 Usage tycons @.@ and @!@
 296
 297 The usage tycons are of kind usageTypeKind (`$').  The types contain
 298 no values, and are used purely for usage annotation.
 299
 300 \begin{code}
 301 usOnceTyCon     = mkKindCon usOnceTyConName usageTypeKind
 302 usOnce          = TyConApp usOnceTyCon []
 303
 304 usManyTyCon     = mkKindCon usManyTyConName usageTypeKind
 305 usMany          = TyConApp usManyTyCon []
 306 \end{code}
 307