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(..),           -- Representation visible
   9         SourceType(..),                 -- to friends
  10
  11         Kind, PredType, ThetaType,              -- Synonyms
  12         TyVarSubst,
  13
  14         superKind, superBoxity,                         -- KX and BX respectively
  15         liftedBoxity, unliftedBoxity,                   -- :: BX
  16         openKindCon,                                    -- :: KX
  17         typeCon,                                        -- :: BX -> KX
  18         liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
  19         mkArrowKind, mkArrowKinds,                      -- :: KX -> KX -> KX
  20
  21         funTyCon
  22     ) where
  23
  24 #include "HsVersions.h"
  25
  26 -- friends:
  27 import Var        ( TyVar )
  28 import VarEnv     ( TyVarEnv )
  29 import VarSet     ( TyVarSet )
  30 import Name       ( Name )
  31 import BasicTypes ( IPName )
  32 import TyCon      ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
  33 import Class      ( Class )
  34 import Binary
  35
  36 -- others
  37 import PrelNames        ( superKindName, superBoxityName, liftedConName,
  38                           unliftedConName, typeConName, openKindConName,
  39                           funTyConName
  40                         )
  41 \end{code}
  42
  43 %************************************************************************
  44 %*                                                                      *
  45 \subsection{Type Classifications}
  46 %*                                                                      *
  47 %************************************************************************
  48
  49 A type is
  50
  51         *unboxed*       iff its representation is other than a pointer
  52                         Unboxed types are also unlifted.
  53
  54         *lifted*        A type is lifted iff it has bottom as an element.
  55                         Closures always have lifted types:  i.e. any
  56                         let-bound identifier in Core must have a lifted
  57                         type.  Operationally, a lifted object is one that
  58                         can be entered.
  59
  60                         Only lifted types may be unified with a type variable.
  61
  62         *algebraic*     A type with one or more constructors, whether declared
  63                         with "data" or "newtype".
  64                         An algebraic type is one that can be deconstructed
  65                         with a case expression.
  66                         *NOT* the same as lifted types,  because we also
  67                         include unboxed tuples in this classification.
  68
  69         *data*          A type declared with "data".  Also boxed tuples.
  70
  71         *primitive*     iff it is a built-in type that can't be expressed
  72                         in Haskell.
  73
  74 Currently, all primitive types are unlifted, but that's not necessarily
  75 the case.  (E.g. Int could be primitive.)
  76
  77 Some primitive types are unboxed, such as Int#, whereas some are boxed
  78 but unlifted (such as ByteArray#).  The only primitive types that we
  79 classify as algebraic are the unboxed tuples.
  80
  81 examples of type classifications:
  82
  83 Type            primitive       boxed           lifted          algebraic
  84 -----------------------------------------------------------------------------
  85 Int#,           Yes             No              No              No
  86 ByteArray#      Yes             Yes             No              No
  87 (# a, b #)      Yes             No              No              Yes
  88 (  a, b  )      No              Yes             Yes             Yes
  89 [a]             No              Yes             Yes             Yes
  90
  91
  92
  93         ----------------------
  94         A note about newtypes
  95         ----------------------
  96
  97 Consider
  98         newtype N = MkN Int
  99
 100 Then we want N to be represented as an Int, and that's what we arrange.
 101 The front end of the compiler [TcType.lhs] treats N as opaque,
 102 the back end treats it as transparent [Type.lhs].
 103
 104 There's a bit of a problem with recursive newtypes
 105         newtype P = MkP P
 106         newtype Q = MkQ (Q->Q)
 107
 108 Here the 'implicit expansion' we get from treating P and Q as transparent
 109 would give rise to infinite types, which in turn makes eqType diverge.
 110 Similarly splitForAllTys and splitFunTys can get into a loop.
 111
 112 Solution: for recursive newtypes use a coerce, and treat the newtype
 113 and its representation as distinct right through the compiler.  That's
 114 what you get if you use recursive newtypes.  (They are rare, so who
 115 cares if they are a tiny bit less efficient.)
 116
 117 So: non-recursive newtypes are represented using a SourceTy (see below)
 118     recursive newtypes are represented using a TyConApp
 119
 120 The TyCon still says "I'm a newtype", but we do not represent the
 121 newtype application as a SourceType; instead as a TyConApp.
 122
 123
 124 NOTE: currently [March 02] we regard a newtype as 'recursive' if it's in a
 125 mutually recursive group.  That's a bit conservative: only if there's a loop
 126 consisting only of newtypes do we need consider it as recursive.  But it's
 127 not so easy to discover that, and the situation isn't that common.
 128
 129
 130 %************************************************************************
 131 %*                                                                      *
 132 \subsection{The data type}
 133 %*                                                                      *
 134 %************************************************************************
 135
 136
 137 \begin{code}
 138 type SuperKind = Type
 139 type Kind      = Type
 140
 141 type TyVarSubst = TyVarEnv Type
 142
 143 data Type
 144   = TyVarTy TyVar
 145
 146   | AppTy
 147         Type            -- Function is *not* a TyConApp
 148         Type
 149
 150   | TyConApp            -- Application of a TyCon
 151         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 152                         --      synonyms have their own constructors, below.
 153         [Type]          -- Might not be saturated.
 154
 155   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 156         Type
 157         Type
 158
 159   | ForAllTy            -- A polymorphic type
 160         TyVar
 161         Type
 162
 163   | SourceTy            -- A high level source type
 164         SourceType      -- ...can be expanded to a representation type...
 165
 166   | NoteTy              -- A type with a note attached
 167         TyNote
 168         Type            -- The expanded version
 169
 170 data TyNote
 171   = FTVNote TyVarSet    -- The free type variables of the noted expression
 172
 173   | SynNote Type        -- Used for type synonyms
 174                         -- The Type is always a TyConApp, and is the un-expanded form.
 175                         -- The type to which the note is attached is the expanded form.
 176
 177 \end{code}
 178
 179 -------------------------------------
 180                 Source types
 181
 182 A type of the form
 183         SourceTy sty
 184 represents a value whose type is the Haskell source type sty.
 185 It can be expanded into its representation, but:
 186
 187         * The type checker must treat it as opaque
 188         * The rest of the compiler treats it as transparent
 189
 190 There are two main uses
 191         a) Haskell predicates
 192         b) newtypes
 193
 194 Consider these examples:
 195         f :: (Eq a) => a -> Int
 196         g :: (?x :: Int -> Int) => a -> Int
 197         h :: (r\l) => {r} => {l::Int | r}
 198
 199 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 200 Predicates are represented inside GHC by PredType:
 201
 202 \begin{code}
 203 data SourceType
 204   = ClassP Class [Type]         -- Class predicate
 205   | IParam (IPName Name) Type   -- Implicit parameter
 206   | NType TyCon [Type]          -- A *saturated*, *non-recursive* newtype application
 207                                 -- [See notes at top about newtypes]
 208
 209 type PredType  = SourceType     -- A subtype for predicates
 210 type ThetaType = [PredType]
 211 \end{code}
 212
 213 (We don't support TREX records yet, but the setup is designed
 214 to expand to allow them.)
 215
 216 A Haskell qualified type, such as that for f,g,h above, is
 217 represented using
 218         * a FunTy for the double arrow
 219         * with a PredTy as the function argument
 220
 221 The predicate really does turn into a real extra argument to the
 222 function.  If the argument has type (PredTy p) then the predicate p is
 223 represented by evidence (a dictionary, for example, of type (predRepTy p).
 224
 225
 226 %************************************************************************
 227 %*                                                                      *
 228 \subsection{Kinds}
 229 %*                                                                      *
 230 %************************************************************************
 231
 232 Kinds
 233 ~~~~~
 234 kind :: KX = kind -> kind
 235
 236            | Type liftedness    -- (Type *) is printed as just *
 237                                 -- (Type #) is printed as just #
 238
 239            | OpenKind           -- Can be lifted or unlifted
 240                                 -- Printed '?'
 241
 242            | kv                 -- A kind variable; *only* happens during kind checking
 243
 244 boxity :: BX = *        -- Lifted
 245              | #        -- Unlifted
 246              | bv       -- A boxity variable; *only* happens during kind checking
 247
 248 There's a little subtyping at the kind level:
 249         forall b. Type b <: OpenKind
 250
 251 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 252
 253 OpenKind, written '?', is used as the kind for certain type variables,
 254 in two situations:
 255
 256 1.  The universally quantified type variable(s) for special built-in
 257     things like error :: forall (a::?). String -> a.
 258     Here, the 'a' can be instantiated to a lifted or unlifted type.
 259
 260 2.  Kind '?' is also used when the typechecker needs to create a fresh
 261     type variable, one that may very well later be unified with a type.
 262     For example, suppose f::a, and we see an application (f x).  Then a
 263     must be a function type, so we unify a with (b->c).  But what kind
 264     are b and c?  They can be lifted or unlifted types, or indeed type schemes,
 265     so we give them kind '?'.
 266
 267     When the type checker generalises over a bunch of type variables, it
 268     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 269     present in an inferred type.
 270
 271
 272 ------------------------------------------
 273 Define  KX, the type of a kind
 274         BX, the type of a boxity
 275
 276 \begin{code}
 277 superKind :: SuperKind          -- KX, the type of all kinds
 278 superKind = TyConApp (mkSuperKindCon superKindName) []
 279
 280 superBoxity :: SuperKind                -- BX, the type of all boxities
 281 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 282 \end{code}
 283
 284 ------------------------------------------
 285 Define boxities: @*@ and @#@
 286
 287 \begin{code}
 288 liftedBoxity, unliftedBoxity :: Kind            -- :: BX
 289 liftedBoxity   = TyConApp liftedBoxityCon   []
 290 unliftedBoxity = TyConApp unliftedBoxityCon []
 291
 292 liftedBoxityCon   = mkKindCon liftedConName superBoxity
 293 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
 294 \end{code}
 295
 296 ------------------------------------------
 297 Define kinds: Type, Type *, Type #, OpenKind
 298
 299 \begin{code}
 300 typeCon :: KindCon      -- :: BX -> KX
 301 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 302
 303 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 304
 305 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 306 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 307
 308 openKindCon     = mkKindCon openKindConName superKind
 309 openTypeKind    = TyConApp openKindCon []
 310 \end{code}
 311
 312 ------------------------------------------
 313 Define arrow kinds
 314
 315 \begin{code}
 316 mkArrowKind :: Kind -> Kind -> Kind
 317 mkArrowKind k1 k2 = k1 `FunTy` k2
 318
 319 mkArrowKinds :: [Kind] -> Kind -> Kind
 320 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 321 \end{code}
 322
 323 -----------------------------------------------------------------------------
 324 Binary kinds for interface files
 325
 326 \begin{code}
 327 instance Binary Kind where
 328   put_ bh k@(TyConApp tc [])
 329         | tc == openKindCon  = putByte bh 0
 330   put_ bh k@(TyConApp tc [TyConApp bc _])
 331         | tc == typeCon && bc == liftedBoxityCon   = putByte bh 2
 332         | tc == typeCon && bc == unliftedBoxityCon = putByte bh 3
 333   put_ bh (FunTy f a) = do putByte bh 4;        put_ bh f; put_ bh a
 334   put_ bh _ = error "Binary.put(Kind): strange-looking Kind"
 335
 336   get bh = do
 337         b <- getByte bh
 338         case b of
 339           0 -> return openTypeKind
 340           2 -> return liftedTypeKind
 341           3 -> return unliftedTypeKind
 342           _ -> do f <- get bh; a <- get bh; return (FunTy f a)
 343 \end{code}
 344
 345 %************************************************************************
 346 %*                                                                      *
 347 \subsection{Wired-in type constructors
 348 %*                                                                      *
 349 %************************************************************************
 350
 351 We define a few wired-in type constructors here to avoid module knots
 352
 353 \begin{code}
 354 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 355         -- You might think that (->) should have type (? -> ? -> *), and you'd be right
 356         -- But if we do that we get kind errors when saying
 357         --      instance Control.Arrow (->)
 358         -- becuase the expected kind is (*->*->*).  The trouble is that the
 359         -- expected/actual stuff in the unifier does not go contra-variant, whereas
 360         -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
 361         -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
 362 \end{code}
 363
 364