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 OccName  ( mkOccFS, tcName )
  34 import TyCon    ( TyCon, KindCon,
  35                   mkFunTyCon, mkKindCon, mkSuperKindCon,
  36                 )
  37 import Class    ( Class )
  38
  39 -- others
  40 import SrcLoc           ( mkBuiltinSrcLoc )
  41 import PrelNames        ( pREL_GHC, kindConKey, boxityConKey, boxedConKey, unboxedConKey,
  42                           typeConKey, anyBoxConKey, funTyConKey
  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   | NoteTy              -- A type with a note attached
 131         TyNote
 132         Type            -- The expanded version
 133
 134 data TyNote
 135   = SynNote Type        -- The unexpanded version of the type synonym; always a TyConApp
 136   | FTVNote TyVarSet    -- The free type variables of the noted expression
 137   | UsgNote UsageAnn    -- The usage annotation at this node
 138   | UsgForAll UVar      -- Annotation variable binder
 139
 140 data UsageAnn
 141   = UsOnce              -- Used at most once
 142   | UsMany              -- Used possibly many times (no info; this annotation can be omitted)
 143   | UsVar    UVar       -- Annotation is variable (unbound OK only inside analysis)
 144
 145
 146 type ThetaType    = [PredType]
 147 type RhoType      = Type
 148 type TauType      = Type
 149 type SigmaType    = Type
 150 \end{code}
 151
 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            | Type boxity        -- (Type *) is printed as just *
 192                                 -- (Type #) is printed as just #
 193
 194            | OpenKind           -- Can be boxed or unboxed
 195                                 -- Printed '?'
 196
 197            | kv                 -- A kind variable; *only* happens during kind checking
 198
 199 boxity :: BX = *        -- Boxed
 200              | #        -- Unboxed
 201              | bv       -- A boxity variable; *only* happens during kind checking
 202
 203 There's a little subtyping at the kind level:
 204         forall b. Type b <: OpenKind
 205
 206 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 207
 208 OpenKind, written '?', is used as the kind for certain type variables,
 209 in two situations:
 210
 211 1.  The universally quantified type variable(s) for special built-in
 212     things like error :: forall (a::?). String -> a.
 213     Here, the 'a' can be instantiated to a boxed or unboxed type.
 214
 215 2.  Kind '?' is also used when the typechecker needs to create a fresh
 216     type variable, one that may very well later be unified with a type.
 217     For example, suppose f::a, and we see an application (f x).  Then a
 218     must be a function type, so we unify a with (b->c).  But what kind
 219     are b and c?  They can be boxed or unboxed types, so we give them kind '?'.
 220
 221     When the type checker generalises over a bunch of type variables, it
 222     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 223     present in an inferred type.
 224
 225
 226 \begin{code}
 227 mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str)
 228                                     (LocalDef mkBuiltinSrcLoc NotExported)
 229         -- mk_kind_name is a bit of a hack
 230         -- The LocalDef means that we print the name without
 231         -- a qualifier, which is what we want for these kinds.
 232         -- It's used for both Kinds and Boxities
 233 \end{code}
 234
 235 ------------------------------------------
 236 Define  KX, the type of a kind
 237         BX, the type of a boxity
 238
 239 \begin{code}
 240 superKind :: SuperKind          -- KX, the type of all kinds
 241 superKindName = mk_kind_name kindConKey SLIT("KX")
 242 superKind = TyConApp (mkSuperKindCon superKindName) []
 243
 244 superBoxity :: SuperKind                -- BX, the type of all boxities
 245 superBoxityName = mk_kind_name boxityConKey SLIT("BX")
 246 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 247 \end{code}
 248
 249 ------------------------------------------
 250 Define boxities: @*@ and @#@
 251
 252 \begin{code}
 253 boxedBoxity, unboxedBoxity :: Kind              -- :: BX
 254
 255 boxedConName = mk_kind_name boxedConKey SLIT("*")
 256 boxedBoxity  = TyConApp (mkKindCon boxedConName superBoxity) []
 257
 258 unboxedConName = mk_kind_name unboxedConKey SLIT("#")
 259 unboxedBoxity  = TyConApp (mkKindCon unboxedConName superBoxity) []
 260 \end{code}
 261
 262 ------------------------------------------
 263 Define kinds: Type, Type *, Type #, and OpenKind
 264
 265 \begin{code}
 266 typeCon :: KindCon      -- :: BX -> KX
 267 typeConName = mk_kind_name typeConKey SLIT("Type")
 268 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 269
 270 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind    -- Of superkind superKind
 271
 272 boxedTypeKind   = TyConApp typeCon [boxedBoxity]
 273 unboxedTypeKind = TyConApp typeCon [unboxedBoxity]
 274
 275 openKindConName = mk_kind_name anyBoxConKey SLIT("?")
 276 openKindCon     = mkKindCon openKindConName superKind
 277 openTypeKind    = TyConApp openKindCon []
 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 funTyConName = mkWiredInTyConName funTyConKey pREL_GHC (mkOccFS tcName SLIT("(->)")) funTyCon
 302 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
 303 \end{code}
 304
 305