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