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