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