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         TyThing(..),
   9         Type(..), TyNote(..),           -- Representation visible
  10         PredType(..),                   -- to friends
  11
  12         Kind, ThetaType,                -- Synonyms
  13         TyVarSubst,
  14
  15         superKind, superBoxity,                         -- KX and BX respectively
  16         liftedBoxity, unliftedBoxity,                   -- :: BX
  17         openKindCon,                                    -- :: KX
  18         typeCon,                                        -- :: BX -> KX
  19         liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
  20         mkArrowKind, mkArrowKinds,                      -- :: KX -> KX -> KX
  21
  22         funTyCon
  23 #ifdef DEBUG
  24         , crudePprType
  25 #endif
  26     ) where
  27
  28 #include "HsVersions.h"
  29
  30 import {-# SOURCE #-} DataCon( DataCon )
  31
  32 -- friends:
  33 import Var        ( Id, TyVar, tyVarKind )
  34 import VarEnv     ( TyVarEnv )
  35 import VarSet     ( TyVarSet )
  36 import Name       ( Name, mkWiredInName, mkInternalName )
  37 import OccName    ( mkOccFS, mkKindOccFS, tcName )
  38 import BasicTypes ( IPName )
  39 import TyCon      ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon, isNewTyCon )
  40 import Class      ( Class )
  41
  42 -- others
  43 import PrelNames        ( gHC_PRIM, kindConKey, boxityConKey, liftedConKey,
  44                           unliftedConKey, typeConKey, anyBoxConKey,
  45                           funTyConKey
  46                         )
  47 import SrcLoc           ( noSrcLoc )
  48 import Outputable
  49 \end{code}
  50
  51 %************************************************************************
  52 %*                                                                      *
  53 \subsection{Type Classifications}
  54 %*                                                                      *
  55 %************************************************************************
  56
  57 A type is
  58
  59         *unboxed*       iff its representation is other than a pointer
  60                         Unboxed types are also unlifted.
  61
  62         *lifted*        A type is lifted iff it has bottom as an element.
  63                         Closures always have lifted types:  i.e. any
  64                         let-bound identifier in Core must have a lifted
  65                         type.  Operationally, a lifted object is one that
  66                         can be entered.
  67
  68                         Only lifted types may be unified with a type variable.
  69
  70         *algebraic*     A type with one or more constructors, whether declared
  71                         with "data" or "newtype".
  72                         An algebraic type is one that can be deconstructed
  73                         with a case expression.
  74                         *NOT* the same as lifted types,  because we also
  75                         include unboxed tuples in this classification.
  76
  77         *data*          A type declared with "data".  Also boxed tuples.
  78
  79         *primitive*     iff it is a built-in type that can't be expressed
  80                         in Haskell.
  81
  82 Currently, all primitive types are unlifted, but that's not necessarily
  83 the case.  (E.g. Int could be primitive.)
  84
  85 Some primitive types are unboxed, such as Int#, whereas some are boxed
  86 but unlifted (such as ByteArray#).  The only primitive types that we
  87 classify as algebraic are the unboxed tuples.
  88
  89 examples of type classifications:
  90
  91 Type            primitive       boxed           lifted          algebraic
  92 -----------------------------------------------------------------------------
  93 Int#,           Yes             No              No              No
  94 ByteArray#      Yes             Yes             No              No
  95 (# a, b #)      Yes             No              No              Yes
  96 (  a, b  )      No              Yes             Yes             Yes
  97 [a]             No              Yes             Yes             Yes
  98
  99
 100
 101         ----------------------
 102         A note about newtypes
 103         ----------------------
 104
 105 Consider
 106         newtype N = MkN Int
 107
 108 Then we want N to be represented as an Int, and that's what we arrange.
 109 The front end of the compiler [TcType.lhs] treats N as opaque,
 110 the back end treats it as transparent [Type.lhs].
 111
 112 There's a bit of a problem with recursive newtypes
 113         newtype P = MkP P
 114         newtype Q = MkQ (Q->Q)
 115
 116 Here the 'implicit expansion' we get from treating P and Q as transparent
 117 would give rise to infinite types, which in turn makes eqType diverge.
 118 Similarly splitForAllTys and splitFunTys can get into a loop.
 119
 120 Solution:
 121
 122 * Newtypes are always represented using NewTcApp, never as TyConApp.
 123
 124 * For non-recursive newtypes, P, treat P just like a type synonym after
 125   type-checking is done; i.e. it's opaque during type checking (functions
 126   from TcType) but transparent afterwards (functions from Type).
 127   "Treat P as a type synonym" means "all functions expand NewTcApps
 128   on the fly".
 129
 130   Applications of the data constructor P simply vanish:
 131         P x = x
 132
 133
 134 * For recursive newtypes Q, treat the Q and its representation as
 135   distinct right through the compiler.  Applications of the data consructor
 136   use a coerce:
 137         Q = \(x::Q->Q). coerce Q x
 138   They are rare, so who cares if they are a tiny bit less efficient.
 139
 140 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
 141 to cut all loops.  The other members of the loop may be marked 'non-recursive'.
 142
 143
 144 %************************************************************************
 145 %*                                                                      *
 146 \subsection{The data type}
 147 %*                                                                      *
 148 %************************************************************************
 149
 150
 151 \begin{code}
 152 type SuperKind = Type
 153 type Kind      = Type
 154
 155 type TyVarSubst = TyVarEnv Type
 156
 157 data Type
 158   = TyVarTy TyVar
 159
 160   | AppTy
 161         Type            -- Function is *not* a TyConApp
 162         Type
 163
 164   | TyConApp            -- Application of a TyCon
 165         TyCon           -- *Invariant* saturated appliations of FunTyCon and
 166                         --      synonyms have their own constructors, below.
 167         [Type]          -- Might not be saturated.
 168
 169   | NewTcApp            -- Application of a NewType TyCon.   All newtype applications
 170         TyCon           -- show up like this until they are fed through newTypeRep,
 171                         -- which returns
 172                         --      * an ordinary TyConApp for non-saturated,
 173                         --       or recursive newtypes
 174                         --
 175                         --      * the representation type of the newtype for satuarted,
 176                         --        non-recursive ones
 177                         -- [But the result of a call to newTypeRep is always consumed
 178                         --  immediately; it never lives on in another type.  So in any
 179                         --  type, newtypes are always represented with NewTcApp.]
 180         [Type]          -- Might not be saturated.
 181
 182   | FunTy               -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
 183         Type
 184         Type
 185
 186   | ForAllTy            -- A polymorphic type
 187         TyVar
 188         Type
 189
 190   | PredTy              -- A high level source type
 191         PredType        -- ...can be expanded to a representation type...
 192
 193   | NoteTy              -- A type with a note attached
 194         TyNote
 195         Type            -- The expanded version
 196
 197 data TyNote
 198   = FTVNote TyVarSet    -- The free type variables of the noted expression
 199
 200   | SynNote Type        -- Used for type synonyms
 201                         -- The Type is always a TyConApp, and is the un-expanded form.
 202                         -- The type to which the note is attached is the expanded form.
 203 \end{code}
 204
 205 -------------------------------------
 206                 Source types
 207
 208 A type of the form
 209         PredTy p
 210 represents a value whose type is the Haskell predicate p,
 211 where a predicate is what occurs before the '=>' in a Haskell type.
 212 It can be expanded into its representation, but:
 213
 214         * The type checker must treat it as opaque
 215         * The rest of the compiler treats it as transparent
 216
 217 Consider these examples:
 218         f :: (Eq a) => a -> Int
 219         g :: (?x :: Int -> Int) => a -> Int
 220         h :: (r\l) => {r} => {l::Int | r}
 221
 222 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
 223 Predicates are represented inside GHC by PredType:
 224
 225 \begin{code}
 226 data PredType
 227   = ClassP Class [Type]         -- Class predicate
 228   | IParam (IPName Name) Type   -- Implicit parameter
 229
 230 type ThetaType = [PredType]
 231 \end{code}
 232
 233 (We don't support TREX records yet, but the setup is designed
 234 to expand to allow them.)
 235
 236 A Haskell qualified type, such as that for f,g,h above, is
 237 represented using
 238         * a FunTy for the double arrow
 239         * with a PredTy as the function argument
 240
 241 The predicate really does turn into a real extra argument to the
 242 function.  If the argument has type (PredTy p) then the predicate p is
 243 represented by evidence (a dictionary, for example, of type (predRepTy p).
 244
 245
 246 %************************************************************************
 247 %*                                                                      *
 248 \subsection{Kinds}
 249 %*                                                                      *
 250 %************************************************************************
 251
 252 Kinds
 253 ~~~~~
 254 kind :: KX = kind -> kind
 255
 256            | Type liftedness    -- (Type *) is printed as just *
 257                                 -- (Type #) is printed as just #
 258
 259            | OpenKind           -- Can be lifted or unlifted
 260                                 -- Printed '?'
 261
 262            | kv                 -- A kind variable; *only* happens during kind checking
 263
 264 boxity :: BX = *        -- Lifted
 265              | #        -- Unlifted
 266              | bv       -- A boxity variable; *only* happens during kind checking
 267
 268 There's a little subtyping at the kind level:
 269         forall b. Type b <: OpenKind
 270
 271 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
 272
 273 OpenKind, written '?', is used as the kind for certain type variables,
 274 in two situations:
 275
 276 1.  The universally quantified type variable(s) for special built-in
 277     things like error :: forall (a::?). String -> a.
 278     Here, the 'a' can be instantiated to a lifted or unlifted type.
 279
 280 2.  Kind '?' is also used when the typechecker needs to create a fresh
 281     type variable, one that may very well later be unified with a type.
 282     For example, suppose f::a, and we see an application (f x).  Then a
 283     must be a function type, so we unify a with (b->c).  But what kind
 284     are b and c?  They can be lifted or unlifted types, or indeed type schemes,
 285     so we give them kind '?'.
 286
 287     When the type checker generalises over a bunch of type variables, it
 288     makes any that still have kind '?' into kind '*'.  So kind '?' is never
 289     present in an inferred type.
 290
 291
 292 ------------------------------------------
 293 Define  KX, the type of a kind
 294         BX, the type of a boxity
 295
 296 \begin{code}
 297 superKindName    = kindQual FSLIT("KX") kindConKey
 298 superBoxityName  = kindQual FSLIT("BX") boxityConKey
 299 liftedConName    = kindQual FSLIT("*") liftedConKey
 300 unliftedConName  = kindQual FSLIT("#") unliftedConKey
 301 openKindConName  = kindQual FSLIT("?") anyBoxConKey
 302 typeConName      = kindQual FSLIT("Type") typeConKey
 303
 304 kindQual str uq = mkInternalName uq (mkKindOccFS tcName str) noSrcLoc
 305         -- Kinds are not z-encoded in interface file, hence mkKindOccFS
 306         -- And they don't come from any particular module; indeed we always
 307         -- want to print them unqualified.  Hence the InternalName.
 308 \end{code}
 309
 310 \begin{code}
 311 superKind :: SuperKind          -- KX, the type of all kinds
 312 superKind = TyConApp (mkSuperKindCon superKindName) []
 313
 314 superBoxity :: SuperKind                -- BX, the type of all boxities
 315 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
 316 \end{code}
 317
 318 ------------------------------------------
 319 Define boxities: @*@ and @#@
 320
 321 \begin{code}
 322 liftedBoxity, unliftedBoxity :: Kind            -- :: BX
 323 liftedBoxity   = TyConApp liftedBoxityCon   []
 324 unliftedBoxity = TyConApp unliftedBoxityCon []
 325
 326 liftedBoxityCon   = mkKindCon liftedConName superBoxity
 327 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
 328 \end{code}
 329
 330 ------------------------------------------
 331 Define kinds: Type, Type *, Type #, OpenKind
 332
 333 \begin{code}
 334 typeCon :: KindCon      -- :: BX -> KX
 335 typeCon     = mkKindCon typeConName (superBoxity `FunTy` superKind)
 336
 337 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind  -- Of superkind superKind
 338
 339 liftedTypeKind   = TyConApp typeCon [liftedBoxity]
 340 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
 341
 342 openKindCon     = mkKindCon openKindConName superKind
 343 openTypeKind    = TyConApp openKindCon []
 344 \end{code}
 345
 346 ------------------------------------------
 347 Define arrow kinds
 348
 349 \begin{code}
 350 mkArrowKind :: Kind -> Kind -> Kind
 351 mkArrowKind k1 k2 = k1 `FunTy` k2
 352
 353 mkArrowKinds :: [Kind] -> Kind -> Kind
 354 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 355 \end{code}
 356
 357
 358 %************************************************************************
 359 %*                                                                      *
 360                         TyThing
 361 %*                                                                      *
 362 %************************************************************************
 363
 364 Despite the fact that DataCon has to be imported via a hi-boot route,
 365 this module seems the right place for TyThing, because it's needed for
 366 funTyCon and all the types in TysPrim.
 367
 368 \begin{code}
 369 data TyThing = AnId     Id
 370              | ADataCon DataCon
 371              | ATyCon   TyCon
 372              | AClass   Class
 373 \end{code}
 374
 375
 376 %************************************************************************
 377 %*                                                                      *
 378 \subsection{Wired-in type constructors
 379 %*                                                                      *
 380 %************************************************************************
 381
 382 We define a few wired-in type constructors here to avoid module knots
 383
 384 \begin{code}
 385 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
 386         -- You might think that (->) should have type (? -> ? -> *), and you'd be right
 387         -- But if we do that we get kind errors when saying
 388         --      instance Control.Arrow (->)
 389         -- becuase the expected kind is (*->*->*).  The trouble is that the
 390         -- expected/actual stuff in the unifier does not go contra-variant, whereas
 391         -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
 392         -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
 393
 394 funTyConName = mkWiredInName gHC_PRIM
 395                         (mkOccFS tcName FSLIT("(->)"))
 396                         funTyConKey
 397                         Nothing                 -- No parent object
 398                         (ATyCon funTyCon)       -- Relevant TyCon
 399 \end{code}
 400
 401
 402
 403 %************************************************************************
 404 %*                                                                      *
 405                 Crude printing
 406         For debug purposes, we may want to print a type directly
 407 %*                                                                      *
 408 %************************************************************************
 409
 410 \begin{code}
 411 #ifdef DEBUG
 412 crudePprType :: Type -> SDoc
 413 crudePprType (TyVarTy tv)      = ppr tv
 414 crudePprType (AppTy t1 t2)     = crudePprType t1 <+> (parens (crudePprType t2))
 415 crudePprType (FunTy t1 t2)     = crudePprType t1 <+> (parens (crudePprType t2))
 416 crudePprType (TyConApp tc tys) = ppr_tc_app (ppr tc <> pp_nt tc) tys
 417 crudePprType (NewTcApp tc tys) = ptext SLIT("<nt>") <+> ppr_tc_app (ppr tc <> pp_nt tc) tys
 418 crudePprType (ForAllTy tv ty)  = sep [ptext SLIT("forall") <+>
 419                                         parens (ppr tv <+> crudePprType (tyVarKind tv)) <> dot,
 420                                       crudePprType ty]
 421 crudePprType (PredTy st)                = braces (crudePprPredTy st)
 422 crudePprType (NoteTy (SynNote ty1) ty2) = crudePprType ty1
 423 crudePprType (NoteTy other ty)          = crudePprType ty
 424
 425 crudePprPredTy (ClassP cls tys) = ppr_tc_app (ppr cls) tys
 426 crudePprPredTy (IParam ip ty)   = ppr ip <> dcolon <> crudePprType ty
 427
 428 ppr_tc_app :: SDoc -> [Type] -> SDoc
 429 ppr_tc_app tc tys = tc <+> sep (map (parens . crudePprType) tys)
 430
 431 pp_nt tc | isNewTyCon tc = ptext SLIT("(nt)")
 432          | otherwise     = empty
 433 #endif
 434 \end{code}