TyCon.hs 69.4 KB
Newer Older
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

5 6

The @TyCon@ datatype
7
-}
8

9
{-# LANGUAGE CPP, DeriveDataTypeable #-}
10

11
module TyCon(
batterseapower's avatar
batterseapower committed
12
        -- * Main TyCon data types
13
        TyCon, FieldLabel,
14

15
        AlgTyConRhs(..), visibleDataCons,
16
        TyConParent(..), isNoParent,
17
        FamTyConFlav(..), Role(..),
18

batterseapower's avatar
batterseapower committed
19
        -- ** Constructing TyCons
20 21 22 23 24 25 26
        mkAlgTyCon,
        mkClassTyCon,
        mkFunTyCon,
        mkPrimTyCon,
        mkKindTyCon,
        mkLiftedPrimTyCon,
        mkTupleTyCon,
27 28
        mkSynonymTyCon,
        mkFamilyTyCon,
29
        mkPromotedDataCon,
30
        mkPromotedTyCon,
batterseapower's avatar
batterseapower committed
31 32 33

        -- ** Predicates on TyCons
        isAlgTyCon,
34 35
        isClassTyCon, isFamInstTyCon,
        isFunTyCon,
batterseapower's avatar
batterseapower committed
36
        isPrimTyCon,
37
        isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
38
        isTypeSynonymTyCon,
39
        isDecomposableTyCon,
40
        isPromotedDataCon, isPromotedTyCon,
41
        isPromotedDataCon_maybe, isPromotedTyCon_maybe,
42
        promotableTyCon_maybe, promoteTyCon,
batterseapower's avatar
batterseapower committed
43

44 45
        isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
        isEnumerationTyCon,
46
        isNewTyCon, isAbstractTyCon,
47
        isFamilyTyCon, isOpenFamilyTyCon,
48 49
        isTypeFamilyTyCon, isDataFamilyTyCon,
        isOpenTypeFamilyTyCon, isClosedSynFamilyTyCon_maybe,
50
        isBuiltInSynFamTyCon_maybe,
batterseapower's avatar
batterseapower committed
51
        isUnLiftedTyCon,
52 53 54 55
        isGadtSyntaxTyCon, isDistinctTyCon, isDistinctAlgRhs,
        isTyConAssoc, tyConAssoc_maybe,
        isRecursiveTyCon,
        isImplicitTyCon,
batterseapower's avatar
batterseapower committed
56 57

        -- ** Extracting information out of TyCons
58 59 60 61
        tyConName,
        tyConKind,
        tyConUnique,
        tyConTyVars,
62
        tyConCType, tyConCType_maybe,
Jan Stolarek's avatar
Jan Stolarek committed
63
        tyConDataCons, tyConDataCons_maybe,
64
        tyConSingleDataCon_maybe, tyConSingleAlgDataCon_maybe,
65 66 67
        tyConFamilySize,
        tyConStupidTheta,
        tyConArity,
68
        tyConRoles,
69
        tyConParent,
70
        tyConTuple_maybe, tyConClass_maybe,
71
        tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
72
        synTyConDefn_maybe, synTyConRhs_maybe, famTyConFlav_maybe,
73
        algTyConRhs,
Jan Stolarek's avatar
Jan Stolarek committed
74
        newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
75
        unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
batterseapower's avatar
batterseapower committed
76
        tupleTyConBoxity, tupleTyConSort, tupleTyConArity,
77

batterseapower's avatar
batterseapower committed
78
        -- ** Manipulating TyCons
79
        expandSynTyCon_maybe,
80 81
        makeTyConAbstract,
        newTyConCo, newTyConCo_maybe,
82
        pprPromotionQuote,
83

batterseapower's avatar
batterseapower committed
84
        -- * Primitive representations of Types
85
        PrimRep(..), PrimElemRep(..),
86
        tyConPrimRep, isVoidRep, isGcPtrRep,
87 88 89 90
        primRepSizeW, primElemRepSizeB,

        -- * Recursion breaking
        RecTcChecker, initRecTc, checkRecTc
91

92 93
) where

94
#include "HsVersions.h"
95

96
import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
97
import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon )
98

99 100 101
import Var
import Class
import BasicTypes
102
import DynFlags
103
import ForeignCall
104
import Name
105
import NameSet
106
import CoAxiom
107 108
import PrelNames
import Maybes
109
import Outputable
110
import Constants
111 112
import Util
import qualified Data.Data as Data
113
import Data.Typeable (Typeable)
114

115
{-
116
-----------------------------------------------
117
        Notes about type families
118 119
-----------------------------------------------

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
120 121
Note [Type synonym families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
122 123 124
* Type synonym families, also known as "type functions", map directly
  onto the type functions in FC:

125 126 127
        type family F a :: *
        type instance F Int = Bool
        ..etc...
128

129
* Reply "yes" to isTypeFamilyTyCon, and isFamilyTyCon
130

131
* From the user's point of view (F Int) and Bool are simply
132
  equivalent types.
133 134 135 136 137

* A Haskell 98 type synonym is a degenerate form of a type synonym
  family.

* Type functions can't appear in the LHS of a type function:
138
        type instance F (F Int) = ...   -- BAD!
139

140
* Translation of type family decl:
141
        type family F a :: *
142
  translates to
143
    a FamilyTyCon 'F', whose FamTyConFlav is OpenSynFamilyTyCon
144

145 146 147 148
        type family G a :: * where
          G Int = Bool
          G Bool = Char
          G a = ()
149
  translates to
150
    a FamilyTyCon 'G', whose FamTyConFlav is ClosedSynFamilyTyCon, with the
151
    appropriate CoAxiom representing the equations
152

153 154
* In the future we might want to support
    * injective type families (allow decomposition)
155
  but we don't at the moment [2013]
156

157 158
Note [Data type families]
~~~~~~~~~~~~~~~~~~~~~~~~~
159
See also Note [Wrappers for data instance tycons] in MkId.hs
160

161
* Data type families are declared thus
162 163
        data family T a :: *
        data instance T Int = T1 | T2 Bool
164 165

  Here T is the "family TyCon".
166

167 168
* Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon

169 170
* The user does not see any "equivalent types" as he did with type
  synonym families.  He just sees constructors with types
171 172
        T1 :: T Int
        T2 :: Bool -> T Int
173

174
* Here's the FC version of the above declarations:
175

176 177 178
        data T a
        data R:TInt = T1 | T2 Bool
        axiom ax_ti : T Int ~ R:TInt
179 180 181

  The R:TInt is the "representation TyCons".
  It has an AlgTyConParent of
182
        FamInstTyCon T [Int] ax_ti
183

Simon Peyton Jones's avatar
Simon Peyton Jones committed
184 185 186
* The axiom ax_ti may be eta-reduced; see
  Note [Eta reduction for data family axioms] in TcInstDcls

187
* The data contructor T2 has a wrapper (which is what the
188 189
  source-level "T2" invokes):

190 191
        $WT2 :: Bool -> T Int
        $WT2 b = T2 b `cast` sym ax_ti
192 193 194

* A data instance can declare a fully-fledged GADT:

195
        data instance T (a,b) where
196
          X1 :: T (Int,Bool)
197
          X2 :: a -> b -> T (a,b)
198

199 200
  Here's the FC version of the above declaration:

201 202 203 204
        data R:TPair a where
          X1 :: R:TPair Int Bool
          X2 :: a -> b -> R:TPair a b
        axiom ax_pr :: T (a,b) ~ R:TPair a b
205

206 207
        $WX1 :: forall a b. a -> b -> T (a,b)
        $WX1 a b (x::a) (y::b) = X2 a b x y `cast` sym (ax_pr a b)
208 209 210 211 212 213 214 215

  The R:TPair are the "representation TyCons".
  We have a bit of work to do, to unpick the result types of the
  data instance declaration for T (a,b), to get the result type in the
  representation; e.g.  T (a,b) --> R:TPair a b

  The representation TyCon R:TList, has an AlgTyConParent of

216
        FamInstTyCon T [(a,b)] ax_pr
217 218

* Notice that T is NOT translated to a FC type function; it just
219 220 221
  becomes a "data type" with no constructors, which can be coerced inot
  into R:TInt, R:TPair by the axioms.  These axioms
  axioms come into play when (and *only* when) you
222 223
        - use a data constructor
        - do pattern matching
224 225 226
  Rather like newtype, in fact

  As a result
227 228

  - T behaves just like a data type so far as decomposition is concerned
229

230
  - (T Int) is not implicitly converted to R:TInt during type inference.
231 232
    Indeed the latter type is unknown to the programmer.

233
  - There *is* an instance for (T Int) in the type-family instance
234 235
    environment, but it is only used for overlap checking

236
  - It's fine to have T in the LHS of a type function:
237 238 239 240 241 242
    type instance F (T a) = [a]

  It was this last point that confused me!  The big thing is that you
  should not think of a data family T as a *type function* at all, not
  even an injective one!  We can't allow even injective type functions
  on the LHS of a type function:
243 244
        type family injective G a :: *
        type instance F (G Int) = Bool
245
  is no good, even if G is injective, because consider
246 247
        type instance G Int = Bool
        type instance F Bool = Char
248 249

  So a data type family is not an injective type function. It's just a
250
  data type with some axioms that connect it to other data types.
251

252 253 254 255 256 257
Note [Associated families and their parent class]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
*Associated* families are just like *non-associated* families, except
that they have a TyConParent of AssocFamilyTyCon, which identifies the
parent class.

258
However there is an important sharing relationship between
259 260 261 262 263
  * the tyConTyVars of the parent Class
  * the tyConTyvars of the associated TyCon

   class C a b where
     data T p a
264
     type F a q b
265 266 267

Here the 'a' and 'b' are shared with the 'Class'; that is, they have
the same Unique.
268 269

This is important. In an instance declaration we expect
270 271 272 273 274 275 276 277
  * all the shared variables to be instantiated the same way
  * the non-shared variables of the associated type should not
    be instantiated at all

  instance C [x] (Tree y) where
     data T p [x] = T1 x | T2 p
     type F [x] q (Tree y) = (x,y,q)

278 279 280 281 282
Note [TyCon Role signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Every tycon has a role signature, assigning a role to each of the tyConTyVars
(or of equal length to the tyConArity, if there are no tyConTyVars). An
283 284 285 286 287 288
example demonstrates these best: say we have a tycon T, with parameters a at
nominal, b at representational, and c at phantom. Then, to prove
representational equality between T a1 b1 c1 and T a2 b2 c2, we need to have
nominal equality between a1 and a2, representational equality between b1 and
b2, and nothing in particular (i.e., phantom equality) between c1 and c2. This
might happen, say, with the following declaration:
289 290 291 292 293 294 295 296 297 298 299 300

  data T a b c where
    MkT :: b -> T Int b c

Data and class tycons have their roles inferred (see inferRoles in TcTyDecls),
as do vanilla synonym tycons. Family tycons have all parameters at role N,
though it is conceivable that we could relax this restriction. (->)'s and
tuples' parameters are at role R. Each primitive tycon declares its roles;
it's worth noting that (~#)'s parameters are at role N. Promoted data
constructors' type arguments are at role R. All kind arguments are at role
N.

301 302
************************************************************************
*                                                                      *
303
\subsection{The data type}
304 305 306
*                                                                      *
************************************************************************
-}
307

308 309
-- | TyCons represent type constructors. Type constructors are introduced by
-- things such as:
batterseapower's avatar
batterseapower committed
310
--
311 312
-- 1) Data declarations: @data Foo = ...@ creates the @Foo@ type constructor of
--    kind @*@
batterseapower's avatar
batterseapower committed
313 314 315
--
-- 2) Type synonyms: @type Foo = ...@ creates the @Foo@ type constructor
--
316 317
-- 3) Newtypes: @newtype Foo a = MkFoo ...@ creates the @Foo@ type constructor
--    of kind @* -> *@
batterseapower's avatar
batterseapower committed
318
--
319 320
-- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor
--    of kind @*@
batterseapower's avatar
batterseapower committed
321
--
322 323
-- This data type also encodes a number of primitive, built in type constructors
-- such as those for function and tuple types.
324 325

-- If you edit this type, you may need to update the GHC formalism
326
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
327
data TyCon
batterseapower's avatar
batterseapower committed
328 329
  = -- | The function type constructor, @(->)@
    FunTyCon {
330 331 332 333 334 335 336 337 338 339 340 341
        tyConUnique :: Unique,   -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

        tyConName   :: Name,     -- ^ Name of the constructor

        tyConKind   :: Kind,     -- ^ Kind of this TyCon (full kind, not just
                                 -- the return kind)

        tyConArity  :: Arity     -- ^ Number of arguments this TyCon must
                                 -- receive to be considered saturated
                                 -- (including implicit kind variables)
342 343
    }

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
344 345 346 347
  -- | Algebraic type constructors, which are defined to be those
  -- arising @data@ type and @newtype@ declarations.  All these
  -- constructors are lifted and boxed. See 'AlgTyConRhs' for more
  -- information.
348
  | AlgTyCon {
349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406
        tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

        tyConName    :: Name,    -- ^ Name of the constructor

        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
                                 -- the return kind)

        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
                                 -- receive to be considered saturated
                                 -- (including implicit kind variables)

        tyConTyVars  :: [TyVar], -- ^ The kind and type variables used in the
                                 -- type constructor.
                                 -- Invariant: length tyvars = arity
                                 -- Precisely, this list scopes over:
                                 --
                                 -- 1. The 'algTcStupidTheta'
                                 -- 2. The cached types in algTyConRhs.NewTyCon
                                 -- 3. The family instance types if present
                                 --
                                 -- Note that it does /not/ scope over the data
                                 -- constructors.

        tcRoles      :: [Role],  -- ^ The role for each type variable
                                 -- This list has the same length as tyConTyVars
                                 -- See also Note [TyCon Role signatures]

        tyConCType   :: Maybe CType,-- ^ The C type that should be used
                                    -- for this type when using the FFI
                                    -- and CAPI

        algTcGadtSyntax  :: Bool,   -- ^ Was the data type declared with GADT
                                    -- syntax?  If so, that doesn't mean it's a
                                    -- true GADT; only that the "where" form
                                    -- was used.  This field is used only to
                                    -- guide pretty-printing

        algTcStupidTheta :: [PredType], -- ^ The \"stupid theta\" for the data
                                        -- type (always empty for GADTs).  A
                                        -- \"stupid theta\" is the context to
                                        -- the left of an algebraic type
                                        -- declaration, e.g. @Eq a@ in the
                                        -- declaration @data Eq a => T a ...@.

        algTcRhs    :: AlgTyConRhs, -- ^ Contains information about the
                                    -- data constructors of the algebraic type

        algTcRec    :: RecFlag,     -- ^ Tells us whether the data type is part
                                    -- of a mutually-recursive group or not

        algTcParent :: TyConParent, -- ^ Gives the class or family declaration
                                    -- 'TyCon' for derived 'TyCon's representing
                                    -- class or family instances, respectively.
                                    -- See also 'synTcParent'

        tcPromoted  :: Maybe TyCon  -- ^ Promoted TyCon, if any
407 408
    }

409
  -- | Represents the infinite family of tuple type constructors,
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
410
  --   @()@, @(a,b)@, @(# a, b #)@ etc.
411
  | TupleTyCon {
412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436
        tyConUnique    :: Unique,   -- ^ A Unique of this TyCon. Invariant:
                                    -- identical to Unique of Name stored in
                                    -- tyConName field.

        tyConName      :: Name,     -- ^ Name of the constructor

        tyConKind      :: Kind,     -- ^ Kind of this TyCon (full kind, not just
                                    -- the return kind)

        tyConArity     :: Arity,    -- ^ Number of arguments this TyCon must
                                    -- receive to be considered saturated
                                    -- (including implicit kind variables)

        tyConTupleSort :: TupleSort,-- ^ Is this a boxed, unboxed or constraint
                                    -- tuple?

        tyConTyVars    :: [TyVar],  -- ^ List of type and kind variables in this
                                    -- TyCon. Includes implicit kind variables.
                                    -- Invariant:
                                    -- length tyConTyVars = tyConArity

        dataCon        :: DataCon,  -- ^ Corresponding tuple data constructor

        tcPromoted     :: Maybe TyCon
                                    -- ^ Nothing for unboxed tuples
437 438
    }

batterseapower's avatar
batterseapower committed
439
  -- | Represents type synonyms
440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464
  | SynonymTyCon {
        tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

        tyConName    :: Name,    -- ^ Name of the constructor

        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
                                 -- the return kind)

        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
                                 -- receive to be considered saturated
                                 -- (including implicit kind variables)

        tyConTyVars  :: [TyVar], -- ^ List of type and kind variables in this
                                 -- TyCon. Includes implicit kind variables.
                                 -- Invariant: length tyConTyVars = tyConArity

        tcRoles      :: [Role],  -- ^ The role for each type variable
                                 -- This list has the same length as tyConTyVars
                                 -- See also Note [TyCon Role signatures]

        synTcRhs     :: Type     -- ^ Contains information about the expansion
                                 -- of the synonym
    }
465

466 467 468 469 470
  -- | Represents type families
  | FamilyTyCon {
        tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.
471

472
        tyConName    :: Name,    -- ^ Name of the constructor
473

474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498
        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
                                 -- the return kind)

        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
                                 -- receive to be considered saturated
                                 -- (including implicit kind variables)

        tyConTyVars  :: [TyVar], -- ^ The kind and type variables used in the
                                 -- type constructor.
                                 -- Invariant: length tyvars = arity
                                 -- Precisely, this list scopes over:
                                 --
                                 -- 1. The 'algTcStupidTheta'
                                 -- 2. The cached types in 'algTyConRhs.NewTyCon'
                                 -- 3. The family instance types if present
                                 --
                                 -- Note that it does /not/ scope over the data
                                 -- constructors.

        famTcFlav    :: FamTyConFlav, -- ^ Type family flavour: open, closed,
                                      -- abstract, built-in. See comments for
                                      -- FamTyConFlav

        famTcParent  :: TyConParent   -- ^ TyCon of enclosing class for
                                      -- associated type families
499

500 501
    }

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
502 503 504
  -- | Primitive types; cannot be defined in Haskell. This includes
  -- the usual suspects (such as @Int#@) as well as foreign-imported
  -- types and kinds
505
  | PrimTyCon {
506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530
        tyConUnique   :: Unique, -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

        tyConName     :: Name,   -- ^ Name of the constructor

        tyConKind     :: Kind,   -- ^ Kind of this TyCon (full kind, not just
                                 -- the return kind)

        tyConArity    :: Arity,  -- ^ Number of arguments this TyCon must
                                 -- receive to be considered saturated
                                 -- (including implicit kind variables)

        tcRoles       :: [Role], -- ^ The role for each type variable
                                 -- This list has the same length as tyConTyVars
                                 -- See also Note [TyCon Role signatures]

        primTyConRep  :: PrimRep,-- ^ Many primitive tycons are unboxed, but
                                 -- some are boxed (represented by
                                 -- pointers). This 'PrimRep' holds that
                                 -- information.  Only relevant if tyConKind = *

        isUnLifted   :: Bool     -- ^ Most primitive tycons are unlifted (may
                                 -- not contain bottom) but other are lifted,
                                 -- e.g. @RealWorld@
531 532
    }

dreixel's avatar
dreixel committed
533
  -- | Represents promoted data constructor.
534
  | PromotedDataCon {          -- See Note [Promoted data constructors]
535 536 537
        tyConUnique :: Unique, -- ^ Same Unique as the data constructor
        tyConName   :: Name,   -- ^ Same Name as the data constructor
        tyConArity  :: Arity,
538 539
        tyConKind   :: Kind,   -- ^ Translated type of the data constructor
        tcRoles     :: [Role], -- ^ Roles: N for kind vars, R for type vars
dreixel's avatar
dreixel committed
540 541 542 543
        dataCon     :: DataCon -- ^ Corresponding data constructor
    }

  -- | Represents promoted type constructor.
544
  | PromotedTyCon {
545 546 547
        tyConUnique :: Unique, -- ^ Same Unique as the type constructor
        tyConName   :: Name,   -- ^ Same Name as the type constructor
        tyConArity  :: Arity,  -- ^ n if ty_con :: * -> ... -> *  n times
548
        tyConKind   :: Kind,   -- ^ Always TysPrim.superKind
dreixel's avatar
dreixel committed
549 550 551
        ty_con      :: TyCon   -- ^ Corresponding type constructor
    }

552
  deriving Typeable
553

batterseapower's avatar
batterseapower committed
554
-- | Names of the fields in an algebraic record type
555 556
type FieldLabel = Name

batterseapower's avatar
batterseapower committed
557
-- | Represents right-hand-sides of 'TyCon's for algebraic types
558
data AlgTyConRhs
559

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
560 561 562
    -- | Says that we know nothing about this data type, except that
    -- it's represented by a pointer.  Used when we export a data type
    -- abstractly into an .hi file.
563
  = AbstractTyCon
564 565 566 567
      Bool      -- True  <=> It's definitely a distinct data type,
                --           equal only to itself; ie not a newtype
                -- False <=> Not sure
                -- See Note [AbstractTyCon and type equality]
568

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
569 570
    -- | Represents an open type family without a fixed right hand
    -- side.  Additional instances can appear at any time.
571
    --
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
572 573 574 575
    -- These are introduced by either a top level declaration:
    --
    -- > data T a :: *
    --
576
    -- Or an associated data type declaration, within a class declaration:
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
577 578 579
    --
    -- > class C a b where
    -- >   data T b :: *
580
  | DataFamilyTyCon
581

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
582 583 584
    -- | Information about those 'TyCon's derived from a @data@
    -- declaration. This includes data types with no constructors at
    -- all.
585
  | DataTyCon {
586
        data_cons :: [DataCon],
587 588
                          -- ^ The data type constructors; can be empty if the
                          --   user declares the type to have no constructors
589
                          --
590 591
                          -- INVARIANT: Kept in order of increasing 'DataCon'
                          -- tag (see the tag assignment in DataCon.mkDataCon)
592 593

        is_enum :: Bool   -- ^ Cached value: is this an enumeration type?
594
                          --   See Note [Enumeration types]
batterseapower's avatar
batterseapower committed
595
    }
596

batterseapower's avatar
batterseapower committed
597
  -- | Information about those 'TyCon's derived from a @newtype@ declaration
598
  | NewTyCon {
599
        data_con :: DataCon,    -- ^ The unique constructor for the @newtype@.
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
600
                                --   It has no existentials
batterseapower's avatar
batterseapower committed
601

602 603 604 605 606
        nt_rhs :: Type,         -- ^ Cached value: the argument type of the
                                -- constructor, which is just the representation
                                -- type of the 'TyCon' (remember that @newtype@s
                                -- do not exist at runtime so need a different
                                -- representation type).
607
                                --
608 609
                                -- The free 'TyVar's of this type are the
                                -- 'tyConTyVars' from the corresponding 'TyCon'
batterseapower's avatar
batterseapower committed
610

611 612 613 614 615 616
        nt_etad_rhs :: ([TyVar], Type),
                        -- ^ Same as the 'nt_rhs', but this time eta-reduced.
                        -- Hence the list of 'TyVar's in this field may be
                        -- shorter than the declared arity of the 'TyCon'.

                        -- See Note [Newtype eta]
617
        nt_co :: CoAxiom Unbranched
618 619
                             -- The axiom coercion that creates the @newtype@
                             -- from the representation 'Type'.
620

621 622
                             -- See Note [Newtype coercions]
                             -- Invariant: arity = #tvs in nt_etad_rhs;
623
                             -- See Note [Newtype eta]
624 625
                             -- Watch out!  If any newtypes become transparent
                             -- again check Trac #1072.
626
    }
627

628
{-
629 630 631
Note [AbstractTyCon and type equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
TODO
632
-}
633

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
634 635 636
-- | Extract those 'DataCon's that we are able to learn about.  Note
-- that visibility in this sense does not correspond to visibility in
-- the context of any particular user program!
637
visibleDataCons :: AlgTyConRhs -> [DataCon]
638 639
visibleDataCons (AbstractTyCon {})            = []
visibleDataCons DataFamilyTyCon {}            = []
640 641
visibleDataCons (DataTyCon{ data_cons = cs }) = cs
visibleDataCons (NewTyCon{ data_con = c })    = [c]
642

batterseapower's avatar
batterseapower committed
643
-- ^ Both type classes as well as family instances imply implicit
644
-- type constructors.  These implicit type constructors refer to their parent
645
-- structure (ie, the class or family from which they derive) using a type of
646
-- the following form.  We use 'TyConParent' for both algebraic and synonym
batterseapower's avatar
batterseapower committed
647
-- types, but the variant 'ClassTyCon' will only be used by algebraic 'TyCon's.
648
data TyConParent
batterseapower's avatar
batterseapower committed
649 650
  = -- | An ordinary type constructor has no parent.
    NoParentTyCon
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
651

batterseapower's avatar
batterseapower committed
652
  -- | Type constructors representing a class dictionary.
dreixel's avatar
dreixel committed
653
  -- See Note [ATyCon for classes] in TypeRep
654
  | ClassTyCon
655 656
        Class           -- INVARIANT: the classTyCon of this Class is the
                        -- current tycon
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
657

658 659 660 661
  -- | An *associated* type of a class.
  | AssocFamilyTyCon
        Class           -- The class in whose declaration the family is declared
                        -- See Note [Associated families and their parent class]
662

663 664
  -- | Type constructors representing an instance of a *data* family.
  -- Parameters:
batterseapower's avatar
batterseapower committed
665 666 667 668
  --
  --  1) The type family in question
  --
  --  2) Instance types; free variables are the 'tyConTyVars'
669
  --  of the current 'TyCon' (not the family one). INVARIANT:
batterseapower's avatar
batterseapower committed
670 671
  --  the number of types matches the arity of the family 'TyCon'
  --
672
  --  3) A 'CoTyCon' identifying the representation
batterseapower's avatar
batterseapower committed
673
  --  type with the type instance family
674
  | FamInstTyCon          -- See Note [Data type families]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
675 676 677 678 679 680 681 682
        (CoAxiom Unbranched)  -- The coercion axiom.
               -- Generally of kind   T ty1 ty2 ~ R:T a b c
               -- where T is the family TyCon,
               -- and R:T is the representation TyCon (ie this one)
               -- and a,b,c are the tyConTyVars of this TyCon
               --
               -- BUT may be eta-reduced; see TcInstDcls
               --     Note [Eta reduction for data family axioms]
683 684 685

          -- Cached fields of the CoAxiom, but adjusted to
          -- use the tyConTyVars of this TyCon
686 687 688
        TyCon   -- The family TyCon
        [Type]  -- Argument types (mentions the tyConTyVars of this TyCon)
                -- Match in length the tyConTyVars of the family TyCon
689

690 691 692 693 694
        -- E.g.  data intance T [a] = ...
        -- gives a representation tycon:
        --      data R:TList a = ...
        --      axiom co a :: T [a] ~ R:TList a
        -- with R:TList's algTcParent = FamInstTyCon T [a] co
695

batterseapower's avatar
batterseapower committed
696 697 698
instance Outputable TyConParent where
    ppr NoParentTyCon           = text "No parent"
    ppr (ClassTyCon cls)        = text "Class parent" <+> ppr cls
699 700 701 702
    ppr (AssocFamilyTyCon cls)  =
        text "Class parent (assoc. family)" <+> ppr cls
    ppr (FamInstTyCon _ tc tys) =
        text "Family parent (family instance)" <+> ppr tc <+> sep (map ppr tys)
batterseapower's avatar
batterseapower committed
703

704 705
-- | Checks the invariants of a 'TyConParent' given the appropriate type class
-- name, if any
batterseapower's avatar
batterseapower committed
706
okParent :: Name -> TyConParent -> Bool
707 708 709 710
okParent _       NoParentTyCon               = True
okParent tc_name (AssocFamilyTyCon cls)      = tc_name `elem` map tyConName (classATs cls)
okParent tc_name (ClassTyCon cls)            = tc_name == tyConName (classTyCon cls)
okParent _       (FamInstTyCon _ fam_tc tys) = tyConArity fam_tc == length tys
711 712 713 714

isNoParent :: TyConParent -> Bool
isNoParent NoParentTyCon = True
isNoParent _             = False
715 716

--------------------
batterseapower's avatar
batterseapower committed
717 718

-- | Information pertaining to the expansion of a type synonym (@type@)
719 720 721
data FamTyConFlav
  = -- | An open type synonym family  e.g. @type family F x y :: * -> *@
     OpenSynFamilyTyCon
722

723 724
   -- | A closed type synonym family  e.g.
   -- @type family F x where { F Int = Bool }@
725 726
   | ClosedSynFamilyTyCon
       (CoAxiom Branched) -- The one axiom for this family
727 728 729 730

   -- | A closed type synonym family declared in an hs-boot file with
   -- type family F a where ..
   | AbstractClosedSynFamilyTyCon
731

732
   -- | Built-in type family used by the TypeNats solver
733
   | BuiltInSynFamTyCon BuiltInSynFamily
734

735
{-
736 737
Note [Closed type families]
~~~~~~~~~~~~~~~~~~~~~~~~~
Jan Stolarek's avatar
Jan Stolarek committed
738 739
* In an open type family you can add new instances later.  This is the
  usual case.
740

741 742 743
* In a closed type family you can only put equations where the family
  is defined.

744

dreixel's avatar
dreixel committed
745 746 747
Note [Promoted data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A data constructor can be promoted to become a type constructor,
748
via the PromotedTyCon alternative in TyCon.
dreixel's avatar
dreixel committed
749

Jan Stolarek's avatar
Jan Stolarek committed
750
* Only data constructors with
751 752 753
     (a) no kind polymorphism
     (b) no constraints in its type (eg GADTs)
  are promoted.  Existentials are ok; see Trac #7347.
dreixel's avatar
dreixel committed
754 755 756 757 758 759 760 761

* The TyCon promoted from a DataCon has the *same* Name and Unique as
  the DataCon.  Eg. If the data constructor Data.Maybe.Just(unique 78,
  say) is promoted to a TyCon whose name is Data.Maybe.Just(unique 78)

* The *kind* of a promoted DataCon may be polymorphic.  Example:
    type of DataCon           Just :: forall (a:*). a -> Maybe a
    kind of (promoted) tycon  Just :: forall (a:box). a -> Maybe a
762
  The kind is not identical to the type, because of the */box
763
  kind signature on the forall'd variable; so the tyConKind field of
764
  PromotedTyCon is not identical to the dataConUserType of the
dreixel's avatar
dreixel committed
765
  DataCon.  But it's the same modulo changing the variable kinds,
766
  done by DataCon.promoteType.
dreixel's avatar
dreixel committed
767 768 769 770 771

* Small note: We promote the *user* type of the DataCon.  Eg
     data T = MkT {-# UNPACK #-} !(Bool, Bool)
  The promoted kind is
     MkT :: (Bool,Bool) -> T
772
  *not*
dreixel's avatar
dreixel committed
773 774
     MkT :: Bool -> Bool -> T

775 776
Note [Enumeration types]
~~~~~~~~~~~~~~~~~~~~~~~~
777
We define datatypes with no constructors to *not* be
778 779 780 781 782 783 784
enumerations; this fixes trac #2578,  Otherwise we
end up generating an empty table for
  <mod>_<type>_closure_tbl
which is used by tagToEnum# to map Int# to constructors
in an enumeration. The empty table apparently upset
the linker.

785 786 787 788 789 790 791 792 793 794
Moreover, all the data constructor must be enumerations, meaning
they have type  (forall abc. T a b c).  GADTs are not enumerations.
For example consider
    data T a where
      T1 :: T Int
      T2 :: T Bool
      T3 :: T a
What would [T1 ..] be?  [T1,T3] :: T Int? Easiest thing is to exclude them.
See Trac #4528.

795 796
Note [Newtype coercions]
~~~~~~~~~~~~~~~~~~~~~~~~
797 798 799
The NewTyCon field nt_co is a CoAxiom which is used for coercing from
the representation type of the newtype, to the newtype itself. For
example,
800

801
   newtype T a = MkT (a -> a)
802

803
the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> t.
804 805

In the case that the right hand side is a type application
806 807 808 809 810
ending with the same type variables as the left hand side, we
"eta-contract" the coercion.  So if we had

   newtype S a = MkT [a]

811
then we would generate the arity 0 axiom CoS : S ~ [].  The
812
primary reason we do this is to make newtype deriving cleaner.
813

814
In the paper we'd write
815
        axiom CoT : (forall t. T t) ~ (forall t. [t])
816
and then when we used CoT at a particular type, s, we'd say
817
        CoT @ s
818 819
which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])

820 821 822
Note [Newtype eta]
~~~~~~~~~~~~~~~~~~
Consider
Gabor Greif's avatar
Gabor Greif committed
823
        newtype Parser a = MkParser (IO a) deriving Monad
824
Are these two types equal (to Core)?
825 826 827 828
        Monad Parser
        Monad IO
which we need to make the derived instance for Monad Parser.

829 830
Well, yes.  But to see that easily we eta-reduce the RHS type of
Parser, in this case to ([], Froogle), so that even unsaturated applications
831
of Parser will work right.  This eta reduction is done when the type
832
constructor is built, and cached in NewTyCon.
833

834 835
Here's an example that I think showed up in practice
Source code:
836 837
        newtype T a = MkT [a]
        newtype Foo m = MkFoo (forall a. m a -> Int)
838

839 840 841 842 843
        w1 :: Foo []
        w1 = ...

        w2 :: Foo T
        w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
844

845
After desugaring, and discarding the data constructors for the newtypes,
846
we get:
847 848 849 850
        w2 = w1 `cast` Foo CoT
so the coercion tycon CoT must have
        kind:    T ~ []
 and    arity:   0
851

852 853
************************************************************************
*                                                                      *
854
\subsection{PrimRep}
855 856
*                                                                      *
************************************************************************
857

858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885
Note [rep swamp]

GHC has a rich selection of types that represent "primitive types" of
one kind or another.  Each of them makes a different set of
distinctions, and mostly the differences are for good reasons,
although it's probably true that we could merge some of these.

Roughly in order of "includes more information":

 - A Width (cmm/CmmType) is simply a binary value with the specified
   number of bits.  It may represent a signed or unsigned integer, a
   floating-point value, or an address.

    data Width = W8 | W16 | W32 | W64 | W80 | W128

 - Size, which is used in the native code generator, is Width +
   floating point information.

   data Size = II8 | II16 | II32 | II64 | FF32 | FF64 | FF80

   it is necessary because e.g. the instruction to move a 64-bit float
   on x86 (movsd) is different from the instruction to move a 64-bit
   integer (movq), so the mov instruction is parameterised by Size.

 - CmmType wraps Width with more information: GC ptr, float, or
   other value.

    data CmmType = CmmType CmmCat Width
Jan Stolarek's avatar
Jan Stolarek committed
886

887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912
    data CmmCat     -- "Category" (not exported)
       = GcPtrCat   -- GC pointer
       | BitsCat    -- Non-pointer
       | FloatCat   -- Float

   It is important to have GcPtr information in Cmm, since we generate
   info tables containing pointerhood for the GC from this.  As for
   why we have float (and not signed/unsigned) here, see Note [Signed
   vs unsigned].

 - ArgRep makes only the distinctions necessary for the call and
   return conventions of the STG machine.  It is essentially CmmType
   + void.

 - PrimRep makes a few more distinctions than ArgRep: it divides
   non-GC-pointers into signed/unsigned and addresses, information
   that is necessary for passing these values to foreign functions.

There's another tension here: whether the type encodes its size in
bytes, or whether its size depends on the machine word size.  Width
and CmmType have the size built-in, whereas ArgRep and PrimRep do not.

This means to turn an ArgRep/PrimRep into a CmmType requires DynFlags.

On the other hand, CmmType includes some "nonsense" values, such as
CmmType GcPtrCat W32 on a 64-bit machine.
913
-}
914

batterseapower's avatar
batterseapower committed
915 916 917
-- | A 'PrimRep' is an abstraction of a type.  It contains information that
-- the code generator needs in order to pass arguments, return results,
-- and store values of this type.
918 919 920
data PrimRep
  = VoidRep
  | PtrRep
921 922 923 924 925
  | IntRep        -- ^ Signed, word-sized value
  | WordRep       -- ^ Unsigned, word-sized value
  | Int64Rep      -- ^ Signed, 64 bit value (with 32-bit words only)
  | Word64Rep     -- ^ Unsigned, 64 bit value (with 32-bit words only)
  | AddrRep       -- ^ A pointer, but /not/ to a Haskell value (use 'PtrRep')
926 927
  | FloatRep
  | DoubleRep
928
  | VecRep Int PrimElemRep  -- ^ A vector
929 930
  deriving( Eq, Show )

931 932 933 934 935 936 937 938 939 940 941 942 943
data PrimElemRep
  = Int8ElemRep
  | Int16ElemRep
  | Int32ElemRep
  | Int64ElemRep
  | Word8ElemRep
  | Word16ElemRep
  | Word32ElemRep
  | Word64ElemRep
  | FloatElemRep
  | DoubleElemRep
   deriving( Eq, Show )

944 945 946
instance Outputable PrimRep where
  ppr r = text (show r)

947 948 949
instance Outputable PrimElemRep where
  ppr r = text (show r)

950 951 952 953 954 955 956 957
isVoidRep :: PrimRep -> Bool
isVoidRep VoidRep = True
isVoidRep _other  = False

isGcPtrRep :: PrimRep -> Bool
isGcPtrRep PtrRep = True
isGcPtrRep _      = False

batterseapower's avatar
batterseapower committed
958
-- | Find the size of a 'PrimRep', in words
959
primRepSizeW :: DynFlags -> PrimRep -> Int
960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981
primRepSizeW _      IntRep           = 1
primRepSizeW _      WordRep          = 1
primRepSizeW dflags Int64Rep         = wORD64_SIZE `quot` wORD_SIZE dflags
primRepSizeW dflags Word64Rep        = wORD64_SIZE `quot` wORD_SIZE dflags
primRepSizeW _      FloatRep         = 1    -- NB. might not take a full word
primRepSizeW dflags DoubleRep        = dOUBLE_SIZE dflags `quot` wORD_SIZE dflags
primRepSizeW _      AddrRep          = 1
primRepSizeW _      PtrRep           = 1
primRepSizeW _      VoidRep          = 0
primRepSizeW dflags (VecRep len rep) = len * primElemRepSizeB rep `quot` wORD_SIZE dflags

primElemRepSizeB :: PrimElemRep -> Int
primElemRepSizeB Int8ElemRep   = 1
primElemRepSizeB Int16ElemRep  = 2
primElemRepSizeB Int32ElemRep  = 4
primElemRepSizeB Int64ElemRep  = 8
primElemRepSizeB Word8ElemRep  = 1
primElemRepSizeB Word16ElemRep = 2
primElemRepSizeB Word32ElemRep = 4
primElemRepSizeB Word64ElemRep = 8
primElemRepSizeB FloatElemRep  = 4
primElemRepSizeB DoubleElemRep = 8
982

983 984 985
{-
************************************************************************
*                                                                      *
986
\subsection{TyCon Construction}
987 988
*                                                                      *
************************************************************************
989

990 991 992 993 994
Note: the TyCon constructors all take a Kind as one argument, even though
they could, in principle, work out their Kind from their other arguments.
But to do so they need functions from Types, and that makes a nasty
module mutual-recursion.  And they aren't called from many places.
So we compromise, and move their Kind calculation to the call site.
995
-}
996

batterseapower's avatar
batterseapower committed
997
-- | Given the name of the function type constructor and it's kind, create the
998
-- corresponding 'TyCon'. It is reccomended to use 'TypeRep.funTyCon' if you want
batterseapower's avatar
batterseapower committed
999
-- this functionality
1000
mkFunTyCon :: Name -> Kind -> TyCon
1001 1002 1003 1004
mkFunTyCon name kind
  = FunTyCon {
        tyConUnique = nameUnique name,
        tyConName   = name,