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