TyCon.hs 87.9 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, FlexibleInstances #-}
10

11
module TyCon(
batterseapower's avatar
batterseapower committed
12
        -- * Main TyCon data types
13
        TyCon, AlgTyConRhs(..), visibleDataCons,
14
        AlgTyConFlav(..), isNoParent,
15
        FamTyConFlav(..), Role(..), Injectivity(..),
16
        RuntimeRepInfo(..),
17

18 19 20 21 22 23 24
        -- * TyConBinder
        TyConBinder, TyConBndrVis(..),
        mkNamedTyConBinder, mkNamedTyConBinders,
        mkAnonTyConBinder, mkAnonTyConBinders,
        tyConBinderVisibility, isNamedTyConBinder,
        isVisibleTyConBinder, isInvisibleTyConBinder,

Adam Gundry's avatar
Adam Gundry committed
25
        -- ** Field labels
Matthew Pickering's avatar
Matthew Pickering committed
26
        tyConFieldLabels, tyConFieldLabelEnv,
Adam Gundry's avatar
Adam Gundry committed
27

batterseapower's avatar
batterseapower committed
28
        -- ** Constructing TyCons
29 30 31 32 33 34 35
        mkAlgTyCon,
        mkClassTyCon,
        mkFunTyCon,
        mkPrimTyCon,
        mkKindTyCon,
        mkLiftedPrimTyCon,
        mkTupleTyCon,
36 37
        mkSynonymTyCon,
        mkFamilyTyCon,
38
        mkPromotedDataCon,
39
        mkTcTyCon,
batterseapower's avatar
batterseapower committed
40 41

        -- ** Predicates on TyCons
42
        isAlgTyCon, isVanillaAlgTyCon,
43 44
        isClassTyCon, isFamInstTyCon,
        isFunTyCon,
batterseapower's avatar
batterseapower committed
45
        isPrimTyCon,
46
        isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
47
        isTypeSynonymTyCon,
48
        mightBeUnsaturatedTyCon,
49 50
        isPromotedDataCon, isPromotedDataCon_maybe,
        isKindTyCon, isLiftedTypeKindTyConName,
batterseapower's avatar
batterseapower committed
51

52 53
        isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
        isEnumerationTyCon,
54
        isNewTyCon, isAbstractTyCon,
55
        isFamilyTyCon, isOpenFamilyTyCon,
56
        isTypeFamilyTyCon, isDataFamilyTyCon,
57
        isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
Jan Stolarek's avatar
Jan Stolarek committed
58
        familyTyConInjectivityInfo,
59
        isBuiltInSynFamTyCon_maybe,
60
        isUnliftedTyCon,
61
        isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
62 63 64
        isTyConAssoc, tyConAssoc_maybe,
        isRecursiveTyCon,
        isImplicitTyCon,
65
        isTyConWithSrcDataCons,
66
        isTcTyCon,
batterseapower's avatar
batterseapower committed
67 68

        -- ** Extracting information out of TyCons
69 70 71 72
        tyConName,
        tyConKind,
        tyConUnique,
        tyConTyVars,
73
        tyConCType, tyConCType_maybe,
Jan Stolarek's avatar
Jan Stolarek committed
74
        tyConDataCons, tyConDataCons_maybe,
75 76
        tyConSingleDataCon_maybe, tyConSingleDataCon,
        tyConSingleAlgDataCon_maybe,
77 78 79
        tyConFamilySize,
        tyConStupidTheta,
        tyConArity,
80
        tyConRoles,
81
        tyConFlavour,
82
        tyConTuple_maybe, tyConClass_maybe, tyConATs,
83
        tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
Jan Stolarek's avatar
Jan Stolarek committed
84 85 86
        tyConFamilyResVar_maybe,
        synTyConDefn_maybe, synTyConRhs_maybe,
        famTyConFlav_maybe, famTcResVar,
87
        algTyConRhs,
Jan Stolarek's avatar
Jan Stolarek committed
88
        newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
89
        unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
Adam Gundry's avatar
Adam Gundry committed
90
        algTcFields,
91 92
        tyConRuntimeRepInfo,
        tyConBinders, tyConResKind,
93
        tcTyConScopedTyVars,
94

batterseapower's avatar
batterseapower committed
95
        -- ** Manipulating TyCons
96
        expandSynTyCon_maybe,
97 98
        makeTyConAbstract,
        newTyConCo, newTyConCo_maybe,
99
        pprPromotionQuote, mkTyConKind,
100

101 102
        -- * Runtime type representation
        TyConRepName, tyConRepName_maybe,
103 104
        mkPrelTyConRepName,
        tyConRepModOcc,
105

batterseapower's avatar
batterseapower committed
106
        -- * Primitive representations of Types
107
        PrimRep(..), PrimElemRep(..),
108
        isVoidRep, isGcPtrRep,
109
        primRepSizeW, primElemRepSizeB,
110
        primRepIsFloat,
111 112 113

        -- * Recursion breaking
        RecTcChecker, initRecTc, checkRecTc
114

115 116
) where

117
#include "HsVersions.h"
118

119
import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType, pprType )
120
import {-# SOURCE #-} TysWiredIn  ( runtimeRepTyCon, constraintKind
121 122
                                  , vecCountTyCon, vecElemTyCon, liftedTypeKind
                                  , mkFunKind, mkForAllKind )
Adam Gundry's avatar
Adam Gundry committed
123
import {-# SOURCE #-} DataCon ( DataCon, dataConExTyVars, dataConFieldLabels )
124

Jan Stolarek's avatar
Jan Stolarek committed
125
import Binary
126 127 128
import Var
import Class
import BasicTypes
129
import DynFlags
130
import ForeignCall
131
import Name
132
import NameEnv
133
import CoAxiom
134 135
import PrelNames
import Maybes
136
import Outputable
Adam Gundry's avatar
Adam Gundry committed
137 138
import FastStringEnv
import FieldLabel
139
import Constants
140
import Util
141
import Unique( tyConRepNameUnique, dataConRepNameUnique )
142
import UniqSet
143
import Module
Adam Gundry's avatar
Adam Gundry committed
144

145
import qualified Data.Data as Data
146

147
{-
148
-----------------------------------------------
149
        Notes about type families
150 151
-----------------------------------------------

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
152 153
Note [Type synonym families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
154 155 156
* Type synonym families, also known as "type functions", map directly
  onto the type functions in FC:

157 158 159
        type family F a :: *
        type instance F Int = Bool
        ..etc...
160

161
* Reply "yes" to isTypeFamilyTyCon, and isFamilyTyCon
162

163
* From the user's point of view (F Int) and Bool are simply
164
  equivalent types.
165 166 167 168 169

* 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:
170
        type instance F (F Int) = ...   -- BAD!
171

172
* Translation of type family decl:
173
        type family F a :: *
174
  translates to
175
    a FamilyTyCon 'F', whose FamTyConFlav is OpenSynFamilyTyCon
176

177 178 179 180
        type family G a :: * where
          G Int = Bool
          G Bool = Char
          G a = ()
181
  translates to
182
    a FamilyTyCon 'G', whose FamTyConFlav is ClosedSynFamilyTyCon, with the
183
    appropriate CoAxiom representing the equations
184

Jan Stolarek's avatar
Jan Stolarek committed
185
We also support injective type families -- see Note [Injective type families]
186

187 188
Note [Data type families]
~~~~~~~~~~~~~~~~~~~~~~~~~
189
See also Note [Wrappers for data instance tycons] in MkId.hs
190

191
* Data type families are declared thus
192 193
        data family T a :: *
        data instance T Int = T1 | T2 Bool
194 195

  Here T is the "family TyCon".
196

197 198
* Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon

199 200
* The user does not see any "equivalent types" as he did with type
  synonym families.  He just sees constructors with types
201 202
        T1 :: T Int
        T2 :: Bool -> T Int
203

204
* Here's the FC version of the above declarations:
205

206 207
        data T a
        data R:TInt = T1 | T2 Bool
208
        axiom ax_ti : T Int ~R R:TInt
209

210
  Note that this is a *representational* coercion
211
  The R:TInt is the "representation TyCons".
212 213
  It has an AlgTyConFlav of
        DataFamInstTyCon T [Int] ax_ti
214

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

Gabor Greif's avatar
Gabor Greif committed
218
* The data constructor T2 has a wrapper (which is what the
219 220
  source-level "T2" invokes):

221 222
        $WT2 :: Bool -> T Int
        $WT2 b = T2 b `cast` sym ax_ti
223 224 225

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

226
        data instance T (a,b) where
227
          X1 :: T (Int,Bool)
228
          X2 :: a -> b -> T (a,b)
229

230 231
  Here's the FC version of the above declaration:

232 233 234
        data R:TPair a where
          X1 :: R:TPair Int Bool
          X2 :: a -> b -> R:TPair a b
235
        axiom ax_pr :: T (a,b)  ~R  R:TPair a b
236

237 238
        $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)
239 240 241 242 243 244

  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

245
  The representation TyCon R:TList, has an AlgTyConFlav of
246

247
        DataFamInstTyCon T [(a,b)] ax_pr
248 249

* Notice that T is NOT translated to a FC type function; it just
250 251 252
  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
253 254
        - use a data constructor
        - do pattern matching
255 256 257
  Rather like newtype, in fact

  As a result
258 259

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

261
  - (T Int) is not implicitly converted to R:TInt during type inference.
262 263
    Indeed the latter type is unknown to the programmer.

264
  - There *is* an instance for (T Int) in the type-family instance
265 266
    environment, but it is only used for overlap checking

267
  - It's fine to have T in the LHS of a type function:
268 269 270 271 272 273
    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:
274 275
        type family injective G a :: *
        type instance F (G Int) = Bool
276
  is no good, even if G is injective, because consider
277 278
        type instance G Int = Bool
        type instance F Bool = Char
279 280

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

283 284 285 286 287
* The tyConTyVars of the representation tycon are the tyvars that the
  user wrote in the patterns. This is important in TcDeriv, where we
  bring these tyvars into scope before type-checking the deriving
  clause. This fact is arranged for in TcInstDecls.tcDataFamInstDecl.

288 289 290
Note [Associated families and their parent class]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
*Associated* families are just like *non-associated* families, except
291
that they have a famTcParent field of (Just cls), which identifies the
292 293
parent class.

294
However there is an important sharing relationship between
295 296 297 298 299
  * the tyConTyVars of the parent Class
  * the tyConTyvars of the associated TyCon

   class C a b where
     data T p a
300
     type F a q b
301 302 303

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

This is important. In an instance declaration we expect
306 307 308 309 310 311 312 313
  * 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)

314 315 316 317
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
318 319 320 321 322 323
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:
324 325 326 327 328 329 330 331 332 333 334 335

  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.

336 337 338 339 340
Note [Unboxed tuple RuntimeRep vars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The contents of an unboxed tuple may have any representation. Accordingly,
the kind of the unboxed tuple constructor is runtime-representation
polymorphic. For example,
341

342
   (#,#) :: forall (q :: RuntimeRep) (r :: RuntimeRep). TYPE q -> TYPE r -> #
343 344 345 346 347

These extra tyvars (v and w) cause some delicate processing around tuples,
where we used to be able to assume that the tycon arity and the
datacon arity were the same.

Jan Stolarek's avatar
Jan Stolarek committed
348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
Note [Injective type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We allow injectivity annotations for type families (both open and closed):

  type family F (a :: k) (b :: k) = r | r -> a
  type family G a b = res | res -> a b where ...

Injectivity information is stored in the `famTcInj` field of `FamilyTyCon`.
`famTcInj` maybe stores a list of Bools, where each entry corresponds to a
single element of `tyConTyVars` (both lists should have identical length). If no
injectivity annotation was provided `famTcInj` is Nothing. From this follows an
invariant that if `famTcInj` is a Just then at least one element in the list
must be True.

See also:
 * [Injectivity annotation] in HsDecls
 * [Renaming injectivity annotation] in RnSource
 * [Verifying injectivity annotation] in FamInstEnv
 * [Type inference for type families with injectivity] in TcInteract

368 369
************************************************************************
*                                                                      *
370
                    TyConBinder
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 407 408 409 410 411 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 437 438 439 440
type TyConBinder = TyVarBndr TyVar TyConBndrVis

data TyConBndrVis
  = NamedTCB VisibilityFlag
  | AnonTCB

mkAnonTyConBinder :: TyVar -> TyConBinder
mkAnonTyConBinder tv = TvBndr tv AnonTCB

mkAnonTyConBinders :: [TyVar] -> [TyConBinder]
mkAnonTyConBinders tvs = map mkAnonTyConBinder tvs

mkNamedTyConBinder :: VisibilityFlag -> TyVar -> TyConBinder
-- The odd argument order supports currying
mkNamedTyConBinder vis tv = TvBndr tv (NamedTCB vis)

mkNamedTyConBinders :: VisibilityFlag -> [TyVar] -> [TyConBinder]
-- The odd argument order supports currying
mkNamedTyConBinders vis tvs = map (mkNamedTyConBinder vis) tvs

tyConBinderVisibility :: TyConBinder -> VisibilityFlag
tyConBinderVisibility (TvBndr _ (NamedTCB vis)) = vis
tyConBinderVisibility (TvBndr _ AnonTCB)        = Visible

isNamedTyConBinder :: TyConBinder -> Bool
isNamedTyConBinder (TvBndr _ (NamedTCB {})) = True
isNamedTyConBinder _                        = False

isVisibleTyConBinder :: TyVarBndr tv TyConBndrVis -> Bool
-- Works for IfaceTyConBinder too
isVisibleTyConBinder (TvBndr _ (NamedTCB vis)) = isVisible vis
isVisibleTyConBinder (TvBndr _ AnonTCB)        = True

isInvisibleTyConBinder :: TyVarBndr tv TyConBndrVis -> Bool
-- Works for IfaceTyConBinder too
isInvisibleTyConBinder tcb = not (isVisibleTyConBinder tcb)

mkTyConKind :: [TyConBinder] -> Kind -> Kind
mkTyConKind bndrs res_kind = foldr mk res_kind bndrs
  where
    mk :: TyConBinder -> Kind -> Kind
    mk (TvBndr tv AnonTCB)        k = mkFunKind (tyVarKind tv) k
    mk (TvBndr tv (NamedTCB vis)) k = mkForAllKind tv vis k

{- Note [The binders/kind/arity fields of a TyCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
All TyCons have this group of fields
  tyConBinders :: [TyConBinder]
  tyConResKind :: Kind
  tyConTyVars  :: [TyVra] -- Cached = binderVars tyConBinders
  tyConKind    :: Kind    -- Cached = mkTyConKind tyConBinders tyConResKind
  tyConArity   :: Arity   -- Cached = length tyConBinders

They fit together like so:

* tyConBinders gives the telescope of type variables on the LHS of the
  type declaration.  For example:

    type App a (b :: k) = a b

  tyConBinders = [ TvBndr (k::*)   (NamedTCB Invisible)
                 , TvBndr (a:k->*) AnonTCB
                 , TvBndr (b:k)    AnonTCB ]

  Note that that are three binders here, including the
  kind variable k.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
441

442 443
  See Note [TyBinders and VisibilityFlags] in TyConRep for what
  the visibility flag means.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
444

445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465
* Each TyConBinder tyConBinders has a TyVar, and that TyVar may
  scope over some other part of the TyCon's definition. Eg
      type T a = a->a
  we have
      tyConBinders = [ TvBndr (a:*) AnonTCB ]
      synTcRhs     = a->a
  So the 'a' scopes over the synTcRhs

* From the tyConBinders and tyConResKind we can get the tyConKind
  E.g for our App example:
      App :: forall k. (k->*) -> k -> *

  We get a 'forall' in the kind for each NamedTCB, and an arrow
  for each AnonTCB

  tyConKind is the full kind of the TyCon, not just the result kind

* tyConArity is the arguments this TyCon must be applied to, to be
  considered saturated.  Here we mean "applied to in the actual Type",
  not surface syntax; i.e. including implicit kind variables.
  So it's just (length tyConBinders)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
466 467
-}

468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491
instance Outputable tv => Outputable (TyVarBndr tv TyConBndrVis) where
  ppr (TvBndr v AnonTCB)              = ppr v
  ppr (TvBndr v (NamedTCB Visible))   = ppr v
  ppr (TvBndr v (NamedTCB Specified)) = char '@' <> ppr v
  ppr (TvBndr v (NamedTCB Invisible)) = braces (ppr v)

instance Binary TyConBndrVis where
  put_ bh AnonTCB        = putByte bh 0
  put_ bh (NamedTCB vis) = do { putByte bh 1; put_ bh vis }

  get bh = do { h <- getByte bh
              ; case h of
                  0 -> return AnonTCB
                  _ -> do { vis <- get bh; return (NamedTCB vis) } }


{- *********************************************************************
*                                                                      *
               The TyCon type
*                                                                      *
************************************************************************
-}


492 493
-- | TyCons represent type constructors. Type constructors are introduced by
-- things such as:
batterseapower's avatar
batterseapower committed
494
--
495 496
-- 1) Data declarations: @data Foo = ...@ creates the @Foo@ type constructor of
--    kind @*@
batterseapower's avatar
batterseapower committed
497 498 499
--
-- 2) Type synonyms: @type Foo = ...@ creates the @Foo@ type constructor
--
500 501
-- 3) Newtypes: @newtype Foo a = MkFoo ...@ creates the @Foo@ type constructor
--    of kind @* -> *@
batterseapower's avatar
batterseapower committed
502
--
503 504
-- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor
--    of kind @*@
batterseapower's avatar
batterseapower committed
505
--
506 507
-- This data type also encodes a number of primitive, built in type constructors
-- such as those for function and tuple types.
508 509

-- If you edit this type, you may need to update the GHC formalism
510
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
511
data TyCon
batterseapower's avatar
batterseapower committed
512 513
  = -- | The function type constructor, @(->)@
    FunTyCon {
514 515 516 517 518 519
        tyConUnique :: Unique,   -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

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

520
        -- See Note [The binders/kind/arity fields of a TyCon]
521 522 523 524
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
525 526

        tcRepName :: TyConRepName
527 528
    }

529 530 531 532 533 534 535 536 537 538 539 540 541
  -- | Algebraic data types, from
  --     - @data@ declararations
  --     - @newtype@ declarations
  --     - data instance declarations
  --     - type instance declarations
  --     - the TyCon generated by a class declaration
  --     - boxed tuples
  --     - unboxed tuples
  --     - constraint tuples
  -- All these constructors are lifted and boxed except unboxed tuples
  -- which should have an 'UnboxedAlgTyCon' parent.
  -- Data/newtype/type /families/ are handled by 'FamilyTyCon'.
  -- See 'AlgTyConRhs' for more information.
542
  | AlgTyCon {
543 544 545 546 547 548
        tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

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

549
        -- See Note [The binders/kind/arity fields of a TyCon]
550 551 552 553 554 555 556 557 558 559 560 561 562 563
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConTyVars  :: [TyVar],          -- ^ TyVar binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity

              -- The tyConTyVars scope 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.
564 565

        tcRoles      :: [Role],  -- ^ The role for each type variable
566
                                 -- This list has length = tyConArity
567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588
                                 -- 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

Adam Gundry's avatar
Adam Gundry committed
589 590 591
        algTcFields :: FieldLabelEnv, -- ^ Maps a label to information
                                      -- about the field

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

595
        algTcParent :: AlgTyConFlav -- ^ Gives the class or family declaration
596 597
                                       -- 'TyCon' for derived 'TyCon's representing
                                       -- class or family instances, respectively.
598

599 600
    }

batterseapower's avatar
batterseapower committed
601
  -- | Represents type synonyms
602 603 604 605 606 607 608
  | SynonymTyCon {
        tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

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

609
        -- See Note [The binders/kind/arity fields of a TyCon]
610 611 612 613 614 615
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConTyVars  :: [TyVar],          -- ^ TyVar binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
             -- tyConTyVars scope over: synTcRhs
616 617

        tcRoles      :: [Role],  -- ^ The role for each type variable
618
                                 -- This list has length = tyConArity
619 620 621 622 623
                                 -- See also Note [TyCon Role signatures]

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

625 626
  -- | Represents families (both type and data)
  -- Argument roles are all Nominal
627 628 629 630
  | FamilyTyCon {
        tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.
631

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

634
        -- See Note [The binders/kind/arity fields of a TyCon]
635 636 637 638 639 640
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConTyVars  :: [TyVar],          -- ^ TyVar binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
            -- tyConTyVars connect an associated family TyCon
641
            -- with its parent class; see TcValidity.checkConsistentFamInst
642

Jan Stolarek's avatar
Jan Stolarek committed
643 644 645 646 647
        famTcResVar  :: Maybe Name,   -- ^ Name of result type variable, used
                                      -- for pretty-printing with --show-iface
                                      -- and for reifying TyCon in Template
                                      -- Haskell

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

652 653 654
        famTcParent  :: Maybe Class,  -- ^ For *associated* type/data families
                                      -- The class in whose declaration the family is declared
                                      -- See Note [Associated families and their parent class]
655

Jan Stolarek's avatar
Jan Stolarek committed
656 657 658
        famTcInj     :: Injectivity   -- ^ is this a type family injective in
                                      -- its type variables? Nothing if no
                                      -- injectivity annotation was given
659 660
    }

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
661 662
  -- | Primitive types; cannot be defined in Haskell. This includes
  -- the usual suspects (such as @Int#@) as well as foreign-imported
663
  -- types and kinds (@*@, @#@, and @?@)
664
  | PrimTyCon {
665 666 667 668 669 670
        tyConUnique   :: Unique, -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

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

671
        -- See Note [The binders/kind/arity fields of a TyCon]
672 673 674 675
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
676 677

        tcRoles       :: [Role], -- ^ The role for each type variable
678
                                 -- This list has length = tyConArity
679 680
                                 -- See also Note [TyCon Role signatures]

681
        isUnlifted   :: Bool,    -- ^ Most primitive tycons are unlifted (may
682 683
                                 -- not contain bottom) but other are lifted,
                                 -- e.g. @RealWorld@
684 685 686 687
                                 -- Only relevant if tyConKind = *

        primRepName :: Maybe TyConRepName   -- Only relevant for kind TyCons
                                            -- i.e, *, #, ?
688 689
    }

dreixel's avatar
dreixel committed
690
  -- | Represents promoted data constructor.
691
  | PromotedDataCon {          -- See Note [Promoted data constructors]
692 693 694 695
        tyConUnique  :: Unique,     -- ^ Same Unique as the data constructor
        tyConName    :: Name,       -- ^ Same Name as the data constructor

        -- See Note [The binders/kind/arity fields of a TyCon]
696 697 698 699
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
700 701 702

        tcRoles       :: [Role],    -- ^ Roles: N for kind vars, R for type vars
        dataCon       :: DataCon,   -- ^ Corresponding data constructor
703 704
        tcRepName     :: TyConRepName,
        promDcRepInfo :: RuntimeRepInfo  -- ^ See comments with 'RuntimeRepInfo'
dreixel's avatar
dreixel committed
705 706
    }

707 708
  -- | These exist only during a recursive type/class type-checking knot.
  | TcTyCon {
709 710 711 712 713
        tyConUnique :: Unique,
        tyConName   :: Name,
        tyConUnsat  :: Bool,  -- ^ can this tycon be unsaturated?

        -- See Note [The binders/kind/arity fields of a TyCon]
714 715 716 717 718
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConTyVars  :: [TyVar],          -- ^ TyVar binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
719 720 721

        tcTyConScopedTyVars :: [TyVar] -- ^ Scoped tyvars over the
                                       -- tycon's body. See Note [TcTyCon]
722
      }
723

724

batterseapower's avatar
batterseapower committed
725
-- | Represents right-hand-sides of 'TyCon's for algebraic types
726
data AlgTyConRhs
727

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
728 729 730
    -- | 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.
731
  = AbstractTyCon
732 733 734
      Bool      -- True  <=> It's definitely a distinct data type,
                --           equal only to itself; ie not a newtype
                -- False <=> Not sure
735

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
736 737 738
    -- | Information about those 'TyCon's derived from a @data@
    -- declaration. This includes data types with no constructors at
    -- all.
739
  | DataTyCon {
740
        data_cons :: [DataCon],
741 742
                          -- ^ The data type constructors; can be empty if the
                          --   user declares the type to have no constructors
743
                          --
744 745
                          -- INVARIANT: Kept in order of increasing 'DataCon'
                          -- tag (see the tag assignment in DataCon.mkDataCon)
746 747

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

751 752 753 754 755 756
  | TupleTyCon {                   -- A boxed, unboxed, or constraint tuple
        data_con :: DataCon,       -- NB: it can be an *unboxed* tuple
        tup_sort :: TupleSort      -- ^ Is this a boxed, unboxed or constraint
                                   -- tuple?
    }

batterseapower's avatar
batterseapower committed
757
  -- | Information about those 'TyCon's derived from a @newtype@ declaration
758
  | NewTyCon {
759
        data_con :: DataCon,    -- ^ The unique constructor for the @newtype@.
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
760
                                --   It has no existentials
batterseapower's avatar
batterseapower committed
761

762 763 764 765 766
        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).
767
                                --
768 769
                                -- The free 'TyVar's of this type are the
                                -- 'tyConTyVars' from the corresponding 'TyCon'
batterseapower's avatar
batterseapower committed
770

771 772 773 774 775 776
        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]
777
        nt_co :: CoAxiom Unbranched
778 779
                             -- The axiom coercion that creates the @newtype@
                             -- from the representation 'Type'.
780

781 782
                             -- See Note [Newtype coercions]
                             -- Invariant: arity = #tvs in nt_etad_rhs;
783
                             -- See Note [Newtype eta]
784 785
                             -- Watch out!  If any newtypes become transparent
                             -- again check Trac #1072.
786
    }
787

788 789 790 791 792 793 794 795 796 797 798 799 800
-- | Some promoted datacons signify extra info relevant to GHC. For example,
-- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep'
-- constructor of 'PrimRep'. This data structure allows us to store this
-- information right in the 'TyCon'. The other approach would be to look
-- up things like @RuntimeRep@'s @PrimRep@ by known-key every time.
data RuntimeRepInfo
  = NoRRI       -- ^ an ordinary promoted data con
  | RuntimeRep ([Type] -> PrimRep)
      -- ^ A constructor of @RuntimeRep@. The argument to the function should
      -- be the list of arguments to the promoted datacon.
  | VecCount Int         -- ^ A constructor of @VecCount@
  | VecElem PrimElemRep  -- ^ A constructor of @VecElem@

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
801 802 803
-- | 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!
804
visibleDataCons :: AlgTyConRhs -> [DataCon]
805
visibleDataCons (AbstractTyCon {})            = []
806 807
visibleDataCons (DataTyCon{ data_cons = cs }) = cs
visibleDataCons (NewTyCon{ data_con = c })    = [c]
808
visibleDataCons (TupleTyCon{ data_con = c })  = [c]
809

batterseapower's avatar
batterseapower committed
810
-- ^ Both type classes as well as family instances imply implicit
811
-- type constructors.  These implicit type constructors refer to their parent
812
-- structure (ie, the class or family from which they derive) using a type of
813 814
-- the following form.
data AlgTyConFlav
batterseapower's avatar
batterseapower committed
815
  = -- | An ordinary type constructor has no parent.
816 817 818 819 820 821
    VanillaAlgTyCon
       TyConRepName

    -- | An unboxed type constructor. Note that this carries no TyConRepName
    -- as it is not representable.
  | UnboxedAlgTyCon
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
822

batterseapower's avatar
batterseapower committed
823
  -- | Type constructors representing a class dictionary.
824
  -- See Note [ATyCon for classes] in TyCoRep
825
  | ClassTyCon
826 827
        Class           -- INVARIANT: the classTyCon of this Class is the
                        -- current tycon
828 829 830 831 832 833 834 835 836 837 838 839 840 841
        TyConRepName

  -- | Type constructors representing an *instance* of a *data* family.
  -- Parameters:
  --
  --  1) The type family in question
  --
  --  2) Instance types; free variables are the 'tyConTyVars'
  --  of the current 'TyCon' (not the family one). INVARIANT:
  --  the number of types matches the arity of the family 'TyCon'
  --
  --  3) A 'CoTyCon' identifying the representation
  --  type with the type instance family
  | DataFamInstTyCon          -- See Note [Data type families]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
842
        (CoAxiom Unbranched)  -- The coercion axiom.
843 844
               -- A *Representational* coercion,
               -- of kind   T ty1 ty2   ~R   R:T a b c
Simon Peyton Jones's avatar
Simon Peyton Jones committed
845 846 847 848 849 850
               -- 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]
851 852 853

          -- Cached fields of the CoAxiom, but adjusted to
          -- use the tyConTyVars of this TyCon
854 855 856
        TyCon   -- The family TyCon
        [Type]  -- Argument types (mentions the tyConTyVars of this TyCon)
                -- Match in length the tyConTyVars of the family TyCon
857

858 859 860 861
        -- E.g.  data intance T [a] = ...
        -- gives a representation tycon:
        --      data R:TList a = ...
        --      axiom co a :: T [a] ~ R:TList a
862 863 864 865 866 867
        -- with R:TList's algTcParent = DataFamInstTyCon T [a] co

instance Outputable AlgTyConFlav where
    ppr (VanillaAlgTyCon {})        = text "Vanilla ADT"
    ppr (UnboxedAlgTyCon {})        = text "Unboxed ADT"
    ppr (ClassTyCon cls _)          = text "Class parent" <+> ppr cls
868 869
    ppr (DataFamInstTyCon _ tc tys) = text "Family parent (family instance)"
                                      <+> ppr tc <+> sep (map pprType tys)
batterseapower's avatar
batterseapower committed
870

871
-- | Checks the invariants of a 'AlgTyConFlav' given the appropriate type class
872
-- name, if any
873 874 875 876 877
okParent :: Name -> AlgTyConFlav -> Bool
okParent _       (VanillaAlgTyCon {})            = True
okParent _       (UnboxedAlgTyCon)               = True
okParent tc_name (ClassTyCon cls _)              = tc_name == tyConName (classTyCon cls)
okParent _       (DataFamInstTyCon _ fam_tc tys) = tyConArity fam_tc == length tys
878

879 880 881
isNoParent :: AlgTyConFlav -> Bool
isNoParent (VanillaAlgTyCon {}) = True
isNoParent _                   = False
882 883

--------------------
batterseapower's avatar
batterseapower committed
884

Jan Stolarek's avatar
Jan Stolarek committed
885 886
data Injectivity
  = NotInjective
887
  | Injective [Bool]   -- 1-1 with tyConTyVars (incl kind vars)
Jan Stolarek's avatar
Jan Stolarek committed
888 889
  deriving( Eq )

batterseapower's avatar
batterseapower committed
890
-- | Information pertaining to the expansion of a type synonym (@type@)
891
data FamTyConFlav
892 893 894 895 896
  = -- | Represents an open type family without a fixed right hand
    -- side.  Additional instances can appear at any time.
    --
    -- These are introduced by either a top level declaration:
    --
897
    -- > data family T a :: *
898 899 900 901 902 903 904 905 906 907
    --
    -- Or an associated data type declaration, within a class declaration:
    --
    -- > class C a b where
    -- >   data T b :: *
     DataFamilyTyCon
       TyConRepName

     -- | An open type synonym family  e.g. @type family F x y :: * -> *@
   | OpenSynFamilyTyCon
908

909 910
   -- | A closed type synonym family  e.g.
   -- @type family F x where { F Int = Bool }@
911 912
   | ClosedSynFamilyTyCon (Maybe (CoAxiom Branched))
     -- See Note [Closed type families]
913 914 915 916

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

918
   -- | Built-in type family used by the TypeNats solver
919
   | BuiltInSynFamTyCon BuiltInSynFamily
920

921 922
{- Note [Closed type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Jan Stolarek's avatar
Jan Stolarek committed
923 924
* In an open type family you can add new instances later.  This is the
  usual case.
925

926 927 928
* In a closed type family you can only put equations where the family
  is defined.

929 930 931 932 933