TyCon.hs 110 KB
Newer Older
1 2 3 4
{-# LANGUAGE CPP               #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase        #-}

5 6 7 8
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

9 10

The @TyCon@ datatype
11
-}
12

Sylvain Henry's avatar
Sylvain Henry committed
13
module GHC.Core.TyCon(
batterseapower's avatar
batterseapower committed
14
        -- * Main TyCon data types
15 16
        TyCon,
        AlgTyConRhs(..), visibleDataCons,
17
        AlgTyConFlav(..), isNoParent,
18
        FamTyConFlav(..), Role(..), Injectivity(..),
19
        RuntimeRepInfo(..), TyConFlavour(..),
20

21
        -- * TyConBinder
Ningning Xie's avatar
Ningning Xie committed
22
        TyConBinder, TyConBndrVis(..), TyConTyCoBinder,
23
        mkNamedTyConBinder, mkNamedTyConBinders,
Tobias Dammers's avatar
Tobias Dammers committed
24
        mkRequiredTyConBinder,
25
        mkAnonTyConBinder, mkAnonTyConBinders,
26
        tyConBinderArgFlag, tyConBndrVisArgFlag, isNamedTyConBinder,
27 28
        isVisibleTyConBinder, isInvisibleTyConBinder,

Adam Gundry's avatar
Adam Gundry committed
29
        -- ** Field labels
30
        tyConFieldLabels, lookupTyConFieldLabel,
Adam Gundry's avatar
Adam Gundry committed
31

batterseapower's avatar
batterseapower committed
32
        -- ** Constructing TyCons
33 34 35 36 37 38 39
        mkAlgTyCon,
        mkClassTyCon,
        mkFunTyCon,
        mkPrimTyCon,
        mkKindTyCon,
        mkLiftedPrimTyCon,
        mkTupleTyCon,
40
        mkSumTyCon,
41
        mkDataTyConRhs,
42 43
        mkSynonymTyCon,
        mkFamilyTyCon,
44
        mkPromotedDataCon,
45
        mkTcTyCon,
46
        noTcTyConScopedTyVars,
batterseapower's avatar
batterseapower committed
47 48

        -- ** Predicates on TyCons
49
        isAlgTyCon, isVanillaAlgTyCon, isConstraintKindCon,
50 51
        isClassTyCon, isFamInstTyCon,
        isFunTyCon,
batterseapower's avatar
batterseapower committed
52
        isPrimTyCon,
53
        isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
54
        isUnboxedSumTyCon, isPromotedTupleTyCon,
55
        isTypeSynonymTyCon,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
56
        mustBeSaturated,
57 58
        isPromotedDataCon, isPromotedDataCon_maybe,
        isKindTyCon, isLiftedTypeKindTyConName,
59
        isTauTyCon, isFamFreeTyCon, isForgetfulSynTyCon,
batterseapower's avatar
batterseapower committed
60

61
        isDataTyCon,
62
        isEnumerationTyCon,
63
        isNewTyCon, isAbstractTyCon,
64
        isFamilyTyCon, isOpenFamilyTyCon,
65
        isTypeFamilyTyCon, isDataFamilyTyCon,
66
        isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
67
        tyConInjectivityInfo,
68
        isBuiltInSynFamTyCon_maybe,
69
        isUnliftedTyCon,
70
        isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
Tobias Dammers's avatar
Tobias Dammers committed
71
        isTyConAssoc, tyConAssoc_maybe, tyConFlavourAssoc_maybe,
72
        isImplicitTyCon,
73
        isTyConWithSrcDataCons,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
74 75
        isTcTyCon, setTcTyConKind,
        isTcLevPoly,
batterseapower's avatar
batterseapower committed
76 77

        -- ** Extracting information out of TyCons
78
        tyConName,
79
        tyConSkolem,
80 81
        tyConKind,
        tyConUnique,
82
        tyConTyVars, tyConVisibleTyVars,
83
        tyConCType, tyConCType_maybe,
Jan Stolarek's avatar
Jan Stolarek committed
84
        tyConDataCons, tyConDataCons_maybe,
85
        tyConSingleDataCon_maybe, tyConSingleDataCon,
86
        tyConAlgDataCons_maybe,
87
        tyConSingleAlgDataCon_maybe,
88
        tyConFamilySize,
89 90
        tyConStupidTheta,
        tyConArity,
91
        tyConNullaryTy,
92
        tyConRoles,
93
        tyConFlavour,
94
        tyConTuple_maybe, tyConClass_maybe, tyConATs,
95
        tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
Jan Stolarek's avatar
Jan Stolarek committed
96 97 98
        tyConFamilyResVar_maybe,
        synTyConDefn_maybe, synTyConRhs_maybe,
        famTyConFlav_maybe, famTcResVar,
99
        algTyConRhs,
Jan Stolarek's avatar
Jan Stolarek committed
100
        newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
101
        unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
102
        newTyConDataCon_maybe,
Adam Gundry's avatar
Adam Gundry committed
103
        algTcFields,
104
        tyConRuntimeRepInfo,
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
105
        tyConBinders, tyConResKind, tyConInvisTVBinders,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
106
        tcTyConScopedTyVars, tcTyConIsPoly,
107
        mkTyConTagMap,
108

batterseapower's avatar
batterseapower committed
109
        -- ** Manipulating TyCons
110
        expandSynTyCon_maybe,
111
        newTyConCo, newTyConCo_maybe,
112
        pprPromotionQuote, mkTyConKind,
113

114
        -- ** Predicated on TyConFlavours
Simon Peyton Jones's avatar
Simon Peyton Jones committed
115
        tcFlavourIsOpen,
116

117 118
        -- * Runtime type representation
        TyConRepName, tyConRepName_maybe,
119 120
        mkPrelTyConRepName,
        tyConRepModOcc,
121

batterseapower's avatar
batterseapower committed
122
        -- * Primitive representations of Types
123
        PrimRep(..), PrimElemRep(..),
124
        isVoidRep, isGcPtrRep,
125 126
        primRepSizeB,
        primElemRepSizeB,
127
        primRepIsFloat,
128 129
        primRepsCompatible,
        primRepCompatible,
130

131 132
) where

133
#include "HsVersions.h"
134

135
import GHC.Prelude
Sylvain Henry's avatar
Sylvain Henry committed
136
import GHC.Platform
137

Sylvain Henry's avatar
Sylvain Henry committed
138
import {-# SOURCE #-} GHC.Core.TyCo.Rep
139
   ( Kind, Type, PredType, mkForAllTy, mkFunTyMany, mkTyConTy_ )
Sylvain Henry's avatar
Sylvain Henry committed
140 141
import {-# SOURCE #-} GHC.Core.TyCo.Ppr
   ( pprType )
Sylvain Henry's avatar
Sylvain Henry committed
142
import {-# SOURCE #-} GHC.Builtin.Types
143
   ( runtimeRepTyCon, constraintKind
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
144
   , multiplicityTyCon
Sylvain Henry's avatar
Sylvain Henry committed
145 146
   , vecCountTyCon, vecElemTyCon, liftedTypeKind )
import {-# SOURCE #-} GHC.Core.DataCon
147
   ( DataCon, dataConFieldLabels
Sylvain Henry's avatar
Sylvain Henry committed
148
   , dataConTyCon, dataConFullSig
149
   , isUnboxedSumDataCon )
Aditya Gupta's avatar
Aditya Gupta committed
150 151 152
import GHC.Builtin.Uniques
  ( tyConRepNameUnique
  , dataConTyRepNameUnique )
153

154
import GHC.Utils.Binary
Sylvain Henry's avatar
Sylvain Henry committed
155 156
import GHC.Types.Var
import GHC.Types.Var.Set
Sylvain Henry's avatar
Sylvain Henry committed
157
import GHC.Core.Class
Sylvain Henry's avatar
Sylvain Henry committed
158 159 160 161
import GHC.Types.Basic
import GHC.Types.ForeignCall
import GHC.Types.Name
import GHC.Types.Name.Env
Sylvain Henry's avatar
Sylvain Henry committed
162
import GHC.Core.Coercion.Axiom
Sylvain Henry's avatar
Sylvain Henry committed
163
import GHC.Builtin.Names
164 165
import GHC.Data.Maybe
import GHC.Utils.Outputable
166
import GHC.Utils.Panic
167
import GHC.Data.FastString.Env
Sylvain Henry's avatar
Sylvain Henry committed
168
import GHC.Types.FieldLabel
Sylvain Henry's avatar
Sylvain Henry committed
169
import GHC.Settings.Constants
170
import GHC.Utils.Misc
Sylvain Henry's avatar
Sylvain Henry committed
171
import GHC.Types.Unique.Set
Sylvain Henry's avatar
Sylvain Henry committed
172
import GHC.Unit.Module
Adam Gundry's avatar
Adam Gundry committed
173

174
import qualified Data.Data as Data
175

176
{-
177
-----------------------------------------------
178
        Notes about type families
179 180
-----------------------------------------------

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
181 182
Note [Type synonym families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
183 184 185
* Type synonym families, also known as "type functions", map directly
  onto the type functions in FC:

186 187 188
        type family F a :: *
        type instance F Int = Bool
        ..etc...
189

190
* Reply "yes" to isTypeFamilyTyCon, and isFamilyTyCon
191

192
* From the user's point of view (F Int) and Bool are simply
193
  equivalent types.
194 195 196 197 198

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

201
* Translation of type family decl:
202
        type family F a :: *
203
  translates to
204
    a FamilyTyCon 'F', whose FamTyConFlav is OpenSynFamilyTyCon
205

206 207 208 209
        type family G a :: * where
          G Int = Bool
          G Bool = Char
          G a = ()
210
  translates to
211
    a FamilyTyCon 'G', whose FamTyConFlav is ClosedSynFamilyTyCon, with the
212
    appropriate CoAxiom representing the equations
213

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

216 217
Note [Data type families]
~~~~~~~~~~~~~~~~~~~~~~~~~
Sylvain Henry's avatar
Sylvain Henry committed
218
See also Note [Wrappers for data instance tycons] in GHC.Types.Id.Make
219

220
* Data type families are declared thus
221 222
        data family T a :: *
        data instance T Int = T1 | T2 Bool
223 224

  Here T is the "family TyCon".
225

226 227
* Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon

228 229
* The user does not see any "equivalent types" as they did with type
  synonym families.  They just see constructors with types
230 231
        T1 :: T Int
        T2 :: Bool -> T Int
232

233
* Here's the FC version of the above declarations:
234

235 236
        data T a
        data R:TInt = T1 | T2 Bool
237
        axiom ax_ti : T Int ~R R:TInt
238

239
  Note that this is a *representational* coercion
240
  The R:TInt is the "representation TyCons".
241 242
  It has an AlgTyConFlav of
        DataFamInstTyCon T [Int] ax_ti
243

Simon Peyton Jones's avatar
Simon Peyton Jones committed
244
* The axiom ax_ti may be eta-reduced; see
245
  Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
246 247

* Data family instances may have a different arity than the data family.
Sylvain Henry's avatar
Sylvain Henry committed
248
  See Note [Arity of data families] in GHC.Core.FamInstEnv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
249

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

253 254
        $WT2 :: Bool -> T Int
        $WT2 b = T2 b `cast` sym ax_ti
255 256 257

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

258
        data instance T (a,b) where
259
          X1 :: T (Int,Bool)
260
          X2 :: a -> b -> T (a,b)
261

262 263
  Here's the FC version of the above declaration:

Ningning Xie's avatar
Ningning Xie committed
264
        data R:TPair a b where
265 266
          X1 :: R:TPair Int Bool
          X2 :: a -> b -> R:TPair a b
267
        axiom ax_pr :: T (a,b)  ~R  R:TPair a b
268

269 270
        $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)
271 272 273 274 275 276

  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

277
  The representation TyCon R:TList, has an AlgTyConFlav of
278

279
        DataFamInstTyCon T [(a,b)] ax_pr
280 281

* Notice that T is NOT translated to a FC type function; it just
Ningning Xie's avatar
Ningning Xie committed
282
  becomes a "data type" with no constructors, which can be coerced
283 284
  into R:TInt, R:TPair by the axioms.  These axioms
  axioms come into play when (and *only* when) you
285 286
        - use a data constructor
        - do pattern matching
287 288 289
  Rather like newtype, in fact

  As a result
290 291

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

293
  - (T Int) is not implicitly converted to R:TInt during type inference.
294 295
    Indeed the latter type is unknown to the programmer.

296
  - There *is* an instance for (T Int) in the type-family instance
297 298 299 300 301 302 303 304
    environment, but it is looked up (via tcLookupDataFamilyInst)
    in can_eq_nc (via tcTopNormaliseNewTypeTF_maybe) when trying to
    solve representational equalities like
         T Int ~R# Bool
    Here we look up (T Int), convert it to R:TInt, and then unwrap the
    newtype R:TInt.

    It is also looked up in reduceTyFamApp_maybe.
305

306
  - It's fine to have T in the LHS of a type function:
307 308 309 310 311 312
    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:
313 314
        type family injective G a :: *
        type instance F (G Int) = Bool
315
  is no good, even if G is injective, because consider
316 317
        type instance G Int = Bool
        type instance F Bool = Char
318 319

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

322
* The tyConTyVars of the representation tycon are the tyvars that the
Sylvain Henry's avatar
Sylvain Henry committed
323
  user wrote in the patterns. This is important in GHC.Tc.Deriv, where we
324 325 326
  bring these tyvars into scope before type-checking the deriving
  clause. This fact is arranged for in TcInstDecls.tcDataFamInstDecl.

327 328 329
Note [Associated families and their parent class]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
*Associated* families are just like *non-associated* families, except
Tobias Dammers's avatar
Tobias Dammers committed
330
that they have a famTcParent field of (Just cls_tc), which identifies the
331 332
parent class.

333
However there is an important sharing relationship between
334
  * the tyConTyVars of the parent Class
Ningning Xie's avatar
Ningning Xie committed
335
  * the tyConTyVars of the associated TyCon
336 337 338

   class C a b where
     data T p a
339
     type F a q b
340 341 342

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

This is important. In an instance declaration we expect
345 346 347 348 349 350 351 352
  * 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)

353 354 355 356
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
357 358 359 360 361 362
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:
363 364 365 366

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

Sylvain Henry's avatar
Sylvain Henry committed
367
Data and class tycons have their roles inferred (see inferRoles in GHC.Tc.TyCl.Utils),
368 369 370 371 372 373 374
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.

375 376 377 378
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
379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398
polymorphic.

Type constructor (2 kind arguments)
   (#,#) :: forall (q :: RuntimeRep) (r :: RuntimeRep).
                   TYPE q -> TYPE r -> TYPE (TupleRep [q, r])
Data constructor (4 type arguments)
   (#,#) :: forall (q :: RuntimeRep) (r :: RuntimeRep)
                   (a :: TYPE q) (b :: TYPE r). a -> b -> (# a, b #)

These extra tyvars (q and r) cause some delicate processing around tuples,
where we need to manually insert RuntimeRep arguments.
The same situation happens with unboxed sums: each alternative
has its own RuntimeRep.
For boxed tuples, there is no levity polymorphism, and therefore
we add RuntimeReps only for the unboxed version.

Type constructor (no kind arguments)
   (,) :: Type -> Type -> Type
Data constructor (2 type arguments)
   (,) :: forall a b. a -> b -> (a, b)
399 400


Jan Stolarek's avatar
Jan Stolarek committed
401 402 403 404 405 406 407 408 409 410 411 412 413 414 415
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:
Sylvain Henry's avatar
Sylvain Henry committed
416
 * [Injectivity annotation] in GHC.Hs.Decls
Sylvain Henry's avatar
Sylvain Henry committed
417
 * [Renaming injectivity annotation] in GHC.Rename.Module
Sylvain Henry's avatar
Sylvain Henry committed
418
 * [Verifying injectivity annotation] in GHC.Core.FamInstEnv
Sylvain Henry's avatar
Sylvain Henry committed
419
 * [Type inference for type families with injectivity] in GHC.Tc.Solver.Interact
Jan Stolarek's avatar
Jan Stolarek committed
420

421 422 423 424 425 426 427 428 429 430 431 432 433 434
Note [Sharing nullary TyConApps]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Nullary type constructor applications are extremely common. For this reason
each TyCon carries with it a @TyConApp tycon []@. This ensures that
'mkTyConTy' does not need to allocate and eliminates quite a bit of heap
residency. Furthermore, we use 'mkTyConTy' in the nullary case of 'mkTyConApp',
ensuring that this function also benefits from sharing.

This optimisation improves allocations in the Cabal test by around 0.3% and
decreased cache misses measurably.

See #19367.


435 436
************************************************************************
*                                                                      *
Ningning Xie's avatar
Ningning Xie committed
437
                    TyConBinder, TyConTyCoBinder
438 439 440
*                                                                      *
************************************************************************
-}
441

442
type TyConBinder     = VarBndr TyVar   TyConBndrVis
Ningning Xie's avatar
Ningning Xie committed
443
type TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis
444 445
     -- Only PromotedDataCon has TyConTyCoBinders
     -- See Note [Promoted GADT data construtors]
446 447

data TyConBndrVis
448
  = NamedTCB ArgFlag
Simon Peyton Jones's avatar
Simon Peyton Jones committed
449
  | AnonTCB  AnonArgFlag
450

451
instance Outputable TyConBndrVis where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
452 453
  ppr (NamedTCB flag) = text "NamedTCB" <> ppr flag
  ppr (AnonTCB af)    = text "AnonTCB"  <> ppr af
454

Simon Peyton Jones's avatar
Simon Peyton Jones committed
455 456 457
mkAnonTyConBinder :: AnonArgFlag -> TyVar -> TyConBinder
mkAnonTyConBinder af tv = ASSERT( isTyVar tv)
                          Bndr tv (AnonTCB af)
458

Simon Peyton Jones's avatar
Simon Peyton Jones committed
459 460
mkAnonTyConBinders :: AnonArgFlag -> [TyVar] -> [TyConBinder]
mkAnonTyConBinders af tvs = map (mkAnonTyConBinder af) tvs
461

462
mkNamedTyConBinder :: ArgFlag -> TyVar -> TyConBinder
463
-- The odd argument order supports currying
Ningning Xie's avatar
Ningning Xie committed
464 465
mkNamedTyConBinder vis tv = ASSERT( isTyVar tv )
                            Bndr tv (NamedTCB vis)
466

467
mkNamedTyConBinders :: ArgFlag -> [TyVar] -> [TyConBinder]
468 469 470
-- The odd argument order supports currying
mkNamedTyConBinders vis tvs = map (mkNamedTyConBinder vis) tvs

Tobias Dammers's avatar
Tobias Dammers committed
471 472 473 474 475 476 477
-- | Make a Required TyConBinder. It chooses between NamedTCB and
-- AnonTCB based on whether the tv is mentioned in the dependent set
mkRequiredTyConBinder :: TyCoVarSet  -- these are used dependently
                      -> TyVar
                      -> TyConBinder
mkRequiredTyConBinder dep_set tv
  | tv `elemVarSet` dep_set = mkNamedTyConBinder Required tv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
478
  | otherwise               = mkAnonTyConBinder  VisArg   tv
Tobias Dammers's avatar
Tobias Dammers committed
479

480
tyConBinderArgFlag :: TyConBinder -> ArgFlag
Ningning Xie's avatar
Ningning Xie committed
481
tyConBinderArgFlag (Bndr _ vis) = tyConBndrVisArgFlag vis
482 483

tyConBndrVisArgFlag :: TyConBndrVis -> ArgFlag
Simon Peyton Jones's avatar
Simon Peyton Jones committed
484 485 486
tyConBndrVisArgFlag (NamedTCB vis)     = vis
tyConBndrVisArgFlag (AnonTCB VisArg)   = Required
tyConBndrVisArgFlag (AnonTCB InvisArg) = Inferred    -- See Note [AnonTCB InvisArg]
487 488

isNamedTyConBinder :: TyConBinder -> Bool
489 490 491
-- Identifies kind variables
-- E.g. data T k (a:k) = blah
-- Here 'k' is a NamedTCB, a variable used in the kind of other binders
Ningning Xie's avatar
Ningning Xie committed
492 493
isNamedTyConBinder (Bndr _ (NamedTCB {})) = True
isNamedTyConBinder _                      = False
494

Ningning Xie's avatar
Ningning Xie committed
495
isVisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
496
-- Works for IfaceTyConBinder too
Ningning Xie's avatar
Ningning Xie committed
497
isVisibleTyConBinder (Bndr _ tcb_vis) = isVisibleTcbVis tcb_vis
498 499

isVisibleTcbVis :: TyConBndrVis -> Bool
Simon Peyton Jones's avatar
Simon Peyton Jones committed
500 501 502
isVisibleTcbVis (NamedTCB vis)     = isVisibleArgFlag vis
isVisibleTcbVis (AnonTCB VisArg)   = True
isVisibleTcbVis (AnonTCB InvisArg) = False
503

Ningning Xie's avatar
Ningning Xie committed
504
isInvisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
505 506 507
-- Works for IfaceTyConBinder too
isInvisibleTyConBinder tcb = not (isVisibleTyConBinder tcb)

508
-- Build the 'tyConKind' from the binders and the result kind.
509
-- Keep in sync with 'mkTyConKind' in GHC.Iface.Type.
510 511 512 513
mkTyConKind :: [TyConBinder] -> Kind -> Kind
mkTyConKind bndrs res_kind = foldr mk res_kind bndrs
  where
    mk :: TyConBinder -> Kind -> Kind
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
514
    mk (Bndr tv (AnonTCB af))   k = mkFunTyMany af (varType tv) k
Simon Peyton Jones's avatar
Simon Peyton Jones committed
515
    mk (Bndr tv (NamedTCB vis)) k = mkForAllTy tv vis k
516

Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
517 518
tyConInvisTVBinders :: [TyConBinder]   -- From the TyCon
                    -> [InvisTVBinder] -- Suitable for the foralls of a term function
519
-- See Note [Building TyVarBinders from TyConBinders]
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
520
tyConInvisTVBinders tc_bndrs
521 522
 = map mk_binder tc_bndrs
 where
Ningning Xie's avatar
Ningning Xie committed
523
   mk_binder (Bndr tv tc_vis) = mkTyVarBinder vis tv
524 525
      where
        vis = case tc_vis of
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
526 527 528 529
                AnonTCB VisArg           -> SpecifiedSpec
                AnonTCB InvisArg         -> InferredSpec   -- See Note [AnonTCB InvisArg]
                NamedTCB Required        -> SpecifiedSpec
                NamedTCB (Invisible vis) -> vis
530

Ningning Xie's avatar
Ningning Xie committed
531
-- Returns only tyvars, as covars are always inferred
532 533
tyConVisibleTyVars :: TyCon -> [TyVar]
tyConVisibleTyVars tc
Ningning Xie's avatar
Ningning Xie committed
534
  = [ tv | Bndr tv vis <- tyConBinders tc
535 536
         , isVisibleTcbVis vis ]

537
{- Note [AnonTCB InvisArg]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
538 539
~~~~~~~~~~~~~~~~~~~~~~~~~~
It's pretty rare to have an (AnonTCB InvisArg) binder.  The
540 541 542 543 544 545 546
only way it can occur is through equality constraints in kinds. These
can arise in one of two ways:

* In a PromotedDataCon whose kind has an equality constraint:

    'MkT :: forall a b. (a~b) => blah

Sylvain Henry's avatar
Sylvain Henry committed
547
  See Note [Constraints in kinds] in GHC.Core.TyCo.Rep, and
548 549 550 551 552
  Note [Promoted data constructors] in this module.
* In a data type whose kind has an equality constraint, as in the
  following example from #12102:

    data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type
Simon Peyton Jones's avatar
Simon Peyton Jones committed
553 554 555 556 557 558 559 560 561 562 563 564

When mapping an (AnonTCB InvisArg) to an ArgFlag, in
tyConBndrVisArgFlag, we use "Inferred" to mean "the user cannot
specify this arguments, even with visible type/kind application;
instead the type checker must fill it in.

We map (AnonTCB VisArg) to Required, of course: the user must
provide it. It would be utterly wrong to do this for constraint
arguments, which is why AnonTCB must have the AnonArgFlag in
the first place.

Note [Building TyVarBinders from TyConBinders]
565 566 567 568 569 570 571 572
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We sometimes need to build the quantified type of a value from
the TyConBinders of a type or class.  For that we need not
TyConBinders but TyVarBinders (used in forall-type)  E.g:

 *  From   data T a = MkT (Maybe a)
    we are going to make a data constructor with type
           MkT :: forall a. Maybe a -> T a
Ningning Xie's avatar
Ningning Xie committed
573
    See the TyCoVarBinders passed to buildDataCon
574 575 576 577

 * From    class C a where { op :: a -> Maybe a }
   we are going to make a default method
           $dmop :: forall a. C a => a -> Maybe a
Ningning Xie's avatar
Ningning Xie committed
578
   See the TyCoVarBinders passed to mkSigmaTy in mkDefaultMethodType
579 580 581 582 583 584 585 586 587 588 589 590 591

Both of these are user-callable.  (NB: default methods are not callable
directly by the user but rather via the code generated by 'deriving',
which uses visible type application; see mkDefMethBind.)

Since they are user-callable we must get their type-argument visibility
information right; and that info is in the TyConBinders.
Here is an example:

  data App a b = MkApp (a b) -- App :: forall {k}. (k->*) -> k -> *

The TyCon has

Ningning Xie's avatar
Ningning Xie committed
592
  tyConTyBinders = [ Named (Bndr (k :: *) Inferred), Anon (k->*), Anon k ]
593 594 595 596 597 598

The TyConBinders for App line up with App's kind, given above.

But the DataCon MkApp has the type
  MkApp :: forall {k} (a:k->*) (b:k). a b -> App k a b

Ningning Xie's avatar
Ningning Xie committed
599
That is, its TyCoVarBinders should be
600

Ningning Xie's avatar
Ningning Xie committed
601 602 603
  dataConUnivTyVarBinders = [ Bndr (k:*)    Inferred
                            , Bndr (a:k->*) Specified
                            , Bndr (b:k)    Specified ]
604

Gabor Greif's avatar
Gabor Greif committed
605
So tyConTyVarBinders converts TyCon's TyConBinders into TyVarBinders:
606 607 608 609 610 611
  - variable names from the TyConBinders
  - but changing Anon/Required to Specified

The last part about Required->Specified comes from this:
  data T k (a:k) b = MkT (a b)
Here k is Required in T's kind, but we don't have Required binders in
Ningning Xie's avatar
Ningning Xie committed
612
the TyCoBinders for a term (see Note [No Required TyCoBinder in terms]
Sylvain Henry's avatar
Sylvain Henry committed
613
in GHC.Core.TyCo.Rep), so we change it to Specified when making MkT's TyCoBinders
614 615 616
-}


617 618 619
{- Note [The binders/kind/arity fields of a TyCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
All TyCons have this group of fields
Ningning Xie's avatar
Ningning Xie committed
620 621 622 623 624 625 626 627
  tyConBinders   :: [TyConBinder/TyConTyCoBinder]
  tyConResKind   :: Kind
  tyConTyVars    :: [TyVar]   -- Cached = binderVars tyConBinders
                              --   NB: Currently (Aug 2018), TyCons that own this
                              --   field really only contain TyVars. So it is
                              --   [TyVar] instead of [TyCoVar].
  tyConKind      :: Kind      -- Cached = mkTyConKind tyConBinders tyConResKind
  tyConArity     :: Arity     -- Cached = length tyConBinders
628 629 630

They fit together like so:

Ningning Xie's avatar
Ningning Xie committed
631
* tyConBinders gives the telescope of type/coercion variables on the LHS of the
632 633 634 635
  type declaration.  For example:

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

Ningning Xie's avatar
Ningning Xie committed
636 637 638
  tyConBinders = [ Bndr (k::*)   (NamedTCB Inferred)
                 , Bndr (a:k->*) AnonTCB
                 , Bndr (b:k)    AnonTCB ]
639

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

Sylvain Henry's avatar
Sylvain Henry committed
643
* See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep
644
  for what the visibility flag means.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
645

Ningning Xie's avatar
Ningning Xie committed
646 647 648
* Each TyConBinder tyConBinders has a TyVar (sometimes it is TyCoVar), and
  that TyVar may scope over some other part of the TyCon's definition. Eg
      type T a = a -> a
649
  we have
Ningning Xie's avatar
Ningning Xie committed
650 651
      tyConBinders = [ Bndr (a:*) AnonTCB ]
      synTcRhs     = a -> a
652 653 654 655 656 657 658 659 660 661 662
  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

663 664 665 666 667 668 669 670 671
* For type families, 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)

* For an algebraic data type, or data instance, the tyConResKind is
  always (TYPE r); that is, the tyConBinders are enough to saturate
  the type constructor.  I'm not quite sure why we have this invariant,
  but it's enforced by etaExpandAlgTyCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
672 673
-}

674 675
instance OutputableBndr tv => Outputable (VarBndr tv TyConBndrVis) where
  ppr (Bndr v bi) = ppr_bi bi <+> parens (pprBndr LetBind v)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
676 677 678 679
    where
      ppr_bi (AnonTCB VisArg)     = text "anon-vis"
      ppr_bi (AnonTCB InvisArg)   = text "anon-invis"
      ppr_bi (NamedTCB Required)  = text "req"
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
680 681 682 683
      -- See Note [Explicit Case Statement for Specificity]
      ppr_bi (NamedTCB (Invisible spec)) = case spec of
        SpecifiedSpec -> text "spec"
        InferredSpec  -> text "inf"
684 685

instance Binary TyConBndrVis where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
686
  put_ bh (AnonTCB af)   = do { putByte bh 0; put_ bh af }
687 688 689 690
  put_ bh (NamedTCB vis) = do { putByte bh 1; put_ bh vis }

  get bh = do { h <- getByte bh
              ; case h of
Simon Peyton Jones's avatar
Simon Peyton Jones committed
691
                  0 -> do { af  <- get bh; return (AnonTCB af) }
692 693 694 695 696 697 698 699 700 701 702
                  _ -> do { vis <- get bh; return (NamedTCB vis) } }


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


703 704
-- | TyCons represent type constructors. Type constructors are introduced by
-- things such as:
batterseapower's avatar
batterseapower committed
705
--
706 707
-- 1) Data declarations: @data Foo = ...@ creates the @Foo@ type constructor of
--    kind @*@
batterseapower's avatar
batterseapower committed
708 709 710
--
-- 2) Type synonyms: @type Foo = ...@ creates the @Foo@ type constructor
--
711 712
-- 3) Newtypes: @newtype Foo a = MkFoo ...@ creates the @Foo@ type constructor
--    of kind @* -> *@
batterseapower's avatar
batterseapower committed
713
--
714 715
-- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor
--    of kind @*@
batterseapower's avatar
batterseapower committed
716
--
717 718
-- This data type also encodes a number of primitive, built in type constructors
-- such as those for function and tuple types.
719 720

-- If you edit this type, you may need to update the GHC formalism
Sylvain Henry's avatar
Sylvain Henry committed
721
-- See Note [GHC Formalism] in GHC.Core.Lint
722
data TyCon
batterseapower's avatar
batterseapower committed
723 724
  = -- | The function type constructor, @(->)@
    FunTyCon {
725 726 727 728 729 730
        tyConUnique :: Unique,   -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

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

731
        -- See Note [The binders/kind/arity fields of a TyCon]
732 733 734 735
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
736
        tyConNullaryTy :: Type,
737 738

        tcRepName :: TyConRepName
739 740
    }

741
  -- | Algebraic data types, from
742
  --     - @data@ declarations
743 744 745 746 747 748 749 750 751 752 753
  --     - @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.
754
  | AlgTyCon {
755 756 757 758 759 760
        tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

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

761
        -- See Note [The binders/kind/arity fields of a TyCon]
762 763 764 765 766
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConTyVars  :: [TyVar],          -- ^ TyVar binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
767
        tyConNullaryTy :: Type,           -- ^ A pre-allocated @TyConApp tycon []@
768 769 770 771 772 773 774 775 776

              -- 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.
777 778

        tcRoles      :: [Role],  -- ^ The role for each type variable
779
                                 -- This list has length = tyConArity
780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801
                                 -- 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
802 803 804
        algTcFields :: FieldLabelEnv, -- ^ Maps a label to information
                                      -- about the field

805
        algTcParent :: AlgTyConFlav -- ^ Gives the class or family declaration
806 807
                                       -- 'TyCon' for derived 'TyCon's representing
                                       -- class or family instances, respectively.
808

809 810
    }

batterseapower's avatar
batterseapower committed
811
  -- | Represents type synonyms
812 813 814 815 816 817 818
  | SynonymTyCon {
        tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                 -- identical to Unique of Name stored in
                                 -- tyConName field.

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

819
        -- See Note [The binders/kind/arity fields of a TyCon]
820 821 822 823 824
        tyConBinders :: [TyConBinder], -- ^ Full binders
        tyConTyVars  :: [TyVar],          -- ^ TyVar binders
        tyConResKind :: Kind,             -- ^ Result kind
        tyConKind    :: Kind,             -- ^ Kind of this TyCon
        tyConArity   :: Arity,            -- ^ Arity
825
        tyConNullaryTy :: Type,           -- ^ A pre-allocated @TyConApp tycon []@
826
             -- tyConTyVars scope over: synTcRhs
827 828

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

832
        synTcRhs     :: Type,    -- ^ Contains information about the expansion
833
                                 -- of the synonym
834 835 836 837

        synIsTau     :: Bool,   -- True <=> the RHS of this synonym does not
                                 --          have any foralls, after expanding any
                                 --          nested synonyms
838
        synIsFamFree  :: Bool,   -- True <=> the RHS of this synonym does not mention
839 840 841
                                 --          any type synonym families (data families
                                 --          are fine), again after expanding any
                                 --          nested synonyms
842 843 844 845 846
        synIsForgetful :: Bool   -- True <=  at least one argument is not mentioned
                                 --          in the RHS (or is mentioned only under
                                 --          forgetful synonyms)
                                 -- Test is conservative, so True does not guarantee
                                 -- forgetfulness.
847
    }
848

849 850
  -- | Represents families (both type and data)
  -- Argument roles are all Nominal
851 852 853