Fix missing unboxed tuple RuntimeReps (#16565)
[ghc.git] / compiler / types / TyCon.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 The @TyCon@ datatype
7 -}
8
9 {-# LANGUAGE CPP, FlexibleInstances #-}
10
11 module TyCon(
12 -- * Main TyCon data types
13 TyCon,
14 AlgTyConRhs(..), visibleDataCons,
15 AlgTyConFlav(..), isNoParent,
16 FamTyConFlav(..), Role(..), Injectivity(..),
17 RuntimeRepInfo(..), TyConFlavour(..),
18
19 -- * TyConBinder
20 TyConBinder, TyConBndrVis(..), TyConTyCoBinder,
21 mkNamedTyConBinder, mkNamedTyConBinders,
22 mkRequiredTyConBinder,
23 mkAnonTyConBinder, mkAnonTyConBinders,
24 tyConBinderArgFlag, tyConBndrVisArgFlag, isNamedTyConBinder,
25 isVisibleTyConBinder, isInvisibleTyConBinder,
26
27 -- ** Field labels
28 tyConFieldLabels, lookupTyConFieldLabel,
29
30 -- ** Constructing TyCons
31 mkAlgTyCon,
32 mkClassTyCon,
33 mkFunTyCon,
34 mkPrimTyCon,
35 mkKindTyCon,
36 mkLiftedPrimTyCon,
37 mkTupleTyCon,
38 mkSumTyCon,
39 mkDataTyConRhs,
40 mkSynonymTyCon,
41 mkFamilyTyCon,
42 mkPromotedDataCon,
43 mkTcTyCon,
44
45 -- ** Predicates on TyCons
46 isAlgTyCon, isVanillaAlgTyCon,
47 isClassTyCon, isFamInstTyCon,
48 isFunTyCon,
49 isPrimTyCon,
50 isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
51 isUnboxedSumTyCon, isPromotedTupleTyCon,
52 isTypeSynonymTyCon,
53 mustBeSaturated,
54 isPromotedDataCon, isPromotedDataCon_maybe,
55 isKindTyCon, isLiftedTypeKindTyConName,
56 isTauTyCon, isFamFreeTyCon,
57
58 isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
59 isDataSumTyCon_maybe,
60 isEnumerationTyCon,
61 isNewTyCon, isAbstractTyCon,
62 isFamilyTyCon, isOpenFamilyTyCon,
63 isTypeFamilyTyCon, isDataFamilyTyCon,
64 isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
65 tyConInjectivityInfo,
66 isBuiltInSynFamTyCon_maybe,
67 isUnliftedTyCon,
68 isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
69 isTyConAssoc, tyConAssoc_maybe, tyConFlavourAssoc_maybe,
70 isImplicitTyCon,
71 isTyConWithSrcDataCons,
72 isTcTyCon, setTcTyConKind,
73 isTcLevPoly,
74
75 -- ** Extracting information out of TyCons
76 tyConName,
77 tyConSkolem,
78 tyConKind,
79 tyConUnique,
80 tyConTyVars, tyConVisibleTyVars,
81 tyConCType, tyConCType_maybe,
82 tyConDataCons, tyConDataCons_maybe,
83 tyConSingleDataCon_maybe, tyConSingleDataCon,
84 tyConSingleAlgDataCon_maybe,
85 tyConFamilySize,
86 tyConStupidTheta,
87 tyConArity,
88 tyConRoles,
89 tyConFlavour,
90 tyConTuple_maybe, tyConClass_maybe, tyConATs,
91 tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
92 tyConFamilyResVar_maybe,
93 synTyConDefn_maybe, synTyConRhs_maybe,
94 famTyConFlav_maybe, famTcResVar,
95 algTyConRhs,
96 newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
97 unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
98 newTyConDataCon_maybe,
99 algTcFields,
100 tyConRuntimeRepInfo,
101 tyConBinders, tyConResKind, tyConTyVarBinders,
102 tcTyConScopedTyVars, tcTyConIsPoly,
103 mkTyConTagMap,
104
105 -- ** Manipulating TyCons
106 expandSynTyCon_maybe,
107 newTyConCo, newTyConCo_maybe,
108 pprPromotionQuote, mkTyConKind,
109
110 -- ** Predicated on TyConFlavours
111 tcFlavourIsOpen,
112
113 -- * Runtime type representation
114 TyConRepName, tyConRepName_maybe,
115 mkPrelTyConRepName,
116 tyConRepModOcc,
117
118 -- * Primitive representations of Types
119 PrimRep(..), PrimElemRep(..),
120 isVoidRep, isGcPtrRep,
121 primRepSizeB,
122 primElemRepSizeB,
123 primRepIsFloat,
124
125 -- * Recursion breaking
126 RecTcChecker, initRecTc, defaultRecTcMaxBound,
127 setRecTcMaxBound, checkRecTc
128
129 ) where
130
131 #include "HsVersions.h"
132
133 import GhcPrelude
134
135 import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType, pprType, mkForAllTy, mkFunTy )
136 import {-# SOURCE #-} TysWiredIn ( runtimeRepTyCon, constraintKind
137 , vecCountTyCon, vecElemTyCon, liftedTypeKind )
138 import {-# SOURCE #-} DataCon ( DataCon, dataConExTyCoVars, dataConFieldLabels
139 , dataConTyCon, dataConFullSig
140 , isUnboxedSumCon )
141
142 import Binary
143 import Var
144 import VarSet
145 import Class
146 import BasicTypes
147 import DynFlags
148 import ForeignCall
149 import Name
150 import NameEnv
151 import CoAxiom
152 import PrelNames
153 import Maybes
154 import Outputable
155 import FastStringEnv
156 import FieldLabel
157 import Constants
158 import Util
159 import Unique( tyConRepNameUnique, dataConTyRepNameUnique )
160 import UniqSet
161 import Module
162
163 import qualified Data.Data as Data
164
165 {-
166 -----------------------------------------------
167 Notes about type families
168 -----------------------------------------------
169
170 Note [Type synonym families]
171 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
172 * Type synonym families, also known as "type functions", map directly
173 onto the type functions in FC:
174
175 type family F a :: *
176 type instance F Int = Bool
177 ..etc...
178
179 * Reply "yes" to isTypeFamilyTyCon, and isFamilyTyCon
180
181 * From the user's point of view (F Int) and Bool are simply
182 equivalent types.
183
184 * A Haskell 98 type synonym is a degenerate form of a type synonym
185 family.
186
187 * Type functions can't appear in the LHS of a type function:
188 type instance F (F Int) = ... -- BAD!
189
190 * Translation of type family decl:
191 type family F a :: *
192 translates to
193 a FamilyTyCon 'F', whose FamTyConFlav is OpenSynFamilyTyCon
194
195 type family G a :: * where
196 G Int = Bool
197 G Bool = Char
198 G a = ()
199 translates to
200 a FamilyTyCon 'G', whose FamTyConFlav is ClosedSynFamilyTyCon, with the
201 appropriate CoAxiom representing the equations
202
203 We also support injective type families -- see Note [Injective type families]
204
205 Note [Data type families]
206 ~~~~~~~~~~~~~~~~~~~~~~~~~
207 See also Note [Wrappers for data instance tycons] in MkId.hs
208
209 * Data type families are declared thus
210 data family T a :: *
211 data instance T Int = T1 | T2 Bool
212
213 Here T is the "family TyCon".
214
215 * Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon
216
217 * The user does not see any "equivalent types" as he did with type
218 synonym families. He just sees constructors with types
219 T1 :: T Int
220 T2 :: Bool -> T Int
221
222 * Here's the FC version of the above declarations:
223
224 data T a
225 data R:TInt = T1 | T2 Bool
226 axiom ax_ti : T Int ~R R:TInt
227
228 Note that this is a *representational* coercion
229 The R:TInt is the "representation TyCons".
230 It has an AlgTyConFlav of
231 DataFamInstTyCon T [Int] ax_ti
232
233 * The axiom ax_ti may be eta-reduced; see
234 Note [Eta reduction for data families] in FamInstEnv
235
236 * Data family instances may have a different arity than the data family.
237 See Note [Arity of data families] in FamInstEnv
238
239 * The data constructor T2 has a wrapper (which is what the
240 source-level "T2" invokes):
241
242 $WT2 :: Bool -> T Int
243 $WT2 b = T2 b `cast` sym ax_ti
244
245 * A data instance can declare a fully-fledged GADT:
246
247 data instance T (a,b) where
248 X1 :: T (Int,Bool)
249 X2 :: a -> b -> T (a,b)
250
251 Here's the FC version of the above declaration:
252
253 data R:TPair a b where
254 X1 :: R:TPair Int Bool
255 X2 :: a -> b -> R:TPair a b
256 axiom ax_pr :: T (a,b) ~R R:TPair a b
257
258 $WX1 :: forall a b. a -> b -> T (a,b)
259 $WX1 a b (x::a) (y::b) = X2 a b x y `cast` sym (ax_pr a b)
260
261 The R:TPair are the "representation TyCons".
262 We have a bit of work to do, to unpick the result types of the
263 data instance declaration for T (a,b), to get the result type in the
264 representation; e.g. T (a,b) --> R:TPair a b
265
266 The representation TyCon R:TList, has an AlgTyConFlav of
267
268 DataFamInstTyCon T [(a,b)] ax_pr
269
270 * Notice that T is NOT translated to a FC type function; it just
271 becomes a "data type" with no constructors, which can be coerced
272 into R:TInt, R:TPair by the axioms. These axioms
273 axioms come into play when (and *only* when) you
274 - use a data constructor
275 - do pattern matching
276 Rather like newtype, in fact
277
278 As a result
279
280 - T behaves just like a data type so far as decomposition is concerned
281
282 - (T Int) is not implicitly converted to R:TInt during type inference.
283 Indeed the latter type is unknown to the programmer.
284
285 - There *is* an instance for (T Int) in the type-family instance
286 environment, but it is only used for overlap checking
287
288 - It's fine to have T in the LHS of a type function:
289 type instance F (T a) = [a]
290
291 It was this last point that confused me! The big thing is that you
292 should not think of a data family T as a *type function* at all, not
293 even an injective one! We can't allow even injective type functions
294 on the LHS of a type function:
295 type family injective G a :: *
296 type instance F (G Int) = Bool
297 is no good, even if G is injective, because consider
298 type instance G Int = Bool
299 type instance F Bool = Char
300
301 So a data type family is not an injective type function. It's just a
302 data type with some axioms that connect it to other data types.
303
304 * The tyConTyVars of the representation tycon are the tyvars that the
305 user wrote in the patterns. This is important in TcDeriv, where we
306 bring these tyvars into scope before type-checking the deriving
307 clause. This fact is arranged for in TcInstDecls.tcDataFamInstDecl.
308
309 Note [Associated families and their parent class]
310 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
311 *Associated* families are just like *non-associated* families, except
312 that they have a famTcParent field of (Just cls_tc), which identifies the
313 parent class.
314
315 However there is an important sharing relationship between
316 * the tyConTyVars of the parent Class
317 * the tyConTyVars of the associated TyCon
318
319 class C a b where
320 data T p a
321 type F a q b
322
323 Here the 'a' and 'b' are shared with the 'Class'; that is, they have
324 the same Unique.
325
326 This is important. In an instance declaration we expect
327 * all the shared variables to be instantiated the same way
328 * the non-shared variables of the associated type should not
329 be instantiated at all
330
331 instance C [x] (Tree y) where
332 data T p [x] = T1 x | T2 p
333 type F [x] q (Tree y) = (x,y,q)
334
335 Note [TyCon Role signatures]
336 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
337 Every tycon has a role signature, assigning a role to each of the tyConTyVars
338 (or of equal length to the tyConArity, if there are no tyConTyVars). An
339 example demonstrates these best: say we have a tycon T, with parameters a at
340 nominal, b at representational, and c at phantom. Then, to prove
341 representational equality between T a1 b1 c1 and T a2 b2 c2, we need to have
342 nominal equality between a1 and a2, representational equality between b1 and
343 b2, and nothing in particular (i.e., phantom equality) between c1 and c2. This
344 might happen, say, with the following declaration:
345
346 data T a b c where
347 MkT :: b -> T Int b c
348
349 Data and class tycons have their roles inferred (see inferRoles in TcTyDecls),
350 as do vanilla synonym tycons. Family tycons have all parameters at role N,
351 though it is conceivable that we could relax this restriction. (->)'s and
352 tuples' parameters are at role R. Each primitive tycon declares its roles;
353 it's worth noting that (~#)'s parameters are at role N. Promoted data
354 constructors' type arguments are at role R. All kind arguments are at role
355 N.
356
357 Note [Unboxed tuple RuntimeRep vars]
358 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
359 The contents of an unboxed tuple may have any representation. Accordingly,
360 the kind of the unboxed tuple constructor is runtime-representation
361 polymorphic.
362
363 Type constructor (2 kind arguments)
364 (#,#) :: forall (q :: RuntimeRep) (r :: RuntimeRep).
365 TYPE q -> TYPE r -> TYPE (TupleRep [q, r])
366 Data constructor (4 type arguments)
367 (#,#) :: forall (q :: RuntimeRep) (r :: RuntimeRep)
368 (a :: TYPE q) (b :: TYPE r). a -> b -> (# a, b #)
369
370 These extra tyvars (q and r) cause some delicate processing around tuples,
371 where we need to manually insert RuntimeRep arguments.
372 The same situation happens with unboxed sums: each alternative
373 has its own RuntimeRep.
374 For boxed tuples, there is no levity polymorphism, and therefore
375 we add RuntimeReps only for the unboxed version.
376
377 Type constructor (no kind arguments)
378 (,) :: Type -> Type -> Type
379 Data constructor (2 type arguments)
380 (,) :: forall a b. a -> b -> (a, b)
381
382
383 Note [Injective type families]
384 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
385 We allow injectivity annotations for type families (both open and closed):
386
387 type family F (a :: k) (b :: k) = r | r -> a
388 type family G a b = res | res -> a b where ...
389
390 Injectivity information is stored in the `famTcInj` field of `FamilyTyCon`.
391 `famTcInj` maybe stores a list of Bools, where each entry corresponds to a
392 single element of `tyConTyVars` (both lists should have identical length). If no
393 injectivity annotation was provided `famTcInj` is Nothing. From this follows an
394 invariant that if `famTcInj` is a Just then at least one element in the list
395 must be True.
396
397 See also:
398 * [Injectivity annotation] in HsDecls
399 * [Renaming injectivity annotation] in RnSource
400 * [Verifying injectivity annotation] in FamInstEnv
401 * [Type inference for type families with injectivity] in TcInteract
402
403 ************************************************************************
404 * *
405 TyConBinder, TyConTyCoBinder
406 * *
407 ************************************************************************
408 -}
409
410 type TyConBinder = VarBndr TyVar TyConBndrVis
411
412 -- In the whole definition of @data TyCon@, only @PromotedDataCon@ will really
413 -- contain CoVar.
414 type TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis
415
416 data TyConBndrVis
417 = NamedTCB ArgFlag
418 | AnonTCB AnonArgFlag
419
420 instance Outputable TyConBndrVis where
421 ppr (NamedTCB flag) = text "NamedTCB" <> ppr flag
422 ppr (AnonTCB af) = text "AnonTCB" <> ppr af
423
424 mkAnonTyConBinder :: AnonArgFlag -> TyVar -> TyConBinder
425 mkAnonTyConBinder af tv = ASSERT( isTyVar tv)
426 Bndr tv (AnonTCB af)
427
428 mkAnonTyConBinders :: AnonArgFlag -> [TyVar] -> [TyConBinder]
429 mkAnonTyConBinders af tvs = map (mkAnonTyConBinder af) tvs
430
431 mkNamedTyConBinder :: ArgFlag -> TyVar -> TyConBinder
432 -- The odd argument order supports currying
433 mkNamedTyConBinder vis tv = ASSERT( isTyVar tv )
434 Bndr tv (NamedTCB vis)
435
436 mkNamedTyConBinders :: ArgFlag -> [TyVar] -> [TyConBinder]
437 -- The odd argument order supports currying
438 mkNamedTyConBinders vis tvs = map (mkNamedTyConBinder vis) tvs
439
440 -- | Make a Required TyConBinder. It chooses between NamedTCB and
441 -- AnonTCB based on whether the tv is mentioned in the dependent set
442 mkRequiredTyConBinder :: TyCoVarSet -- these are used dependently
443 -> TyVar
444 -> TyConBinder
445 mkRequiredTyConBinder dep_set tv
446 | tv `elemVarSet` dep_set = mkNamedTyConBinder Required tv
447 | otherwise = mkAnonTyConBinder VisArg tv
448
449 tyConBinderArgFlag :: TyConBinder -> ArgFlag
450 tyConBinderArgFlag (Bndr _ vis) = tyConBndrVisArgFlag vis
451
452 tyConBndrVisArgFlag :: TyConBndrVis -> ArgFlag
453 tyConBndrVisArgFlag (NamedTCB vis) = vis
454 tyConBndrVisArgFlag (AnonTCB VisArg) = Required
455 tyConBndrVisArgFlag (AnonTCB InvisArg) = Inferred -- See Note [AnonTCB InvisArg]
456
457 isNamedTyConBinder :: TyConBinder -> Bool
458 -- Identifies kind variables
459 -- E.g. data T k (a:k) = blah
460 -- Here 'k' is a NamedTCB, a variable used in the kind of other binders
461 isNamedTyConBinder (Bndr _ (NamedTCB {})) = True
462 isNamedTyConBinder _ = False
463
464 isVisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
465 -- Works for IfaceTyConBinder too
466 isVisibleTyConBinder (Bndr _ tcb_vis) = isVisibleTcbVis tcb_vis
467
468 isVisibleTcbVis :: TyConBndrVis -> Bool
469 isVisibleTcbVis (NamedTCB vis) = isVisibleArgFlag vis
470 isVisibleTcbVis (AnonTCB VisArg) = True
471 isVisibleTcbVis (AnonTCB InvisArg) = False
472
473 isInvisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
474 -- Works for IfaceTyConBinder too
475 isInvisibleTyConBinder tcb = not (isVisibleTyConBinder tcb)
476
477 mkTyConKind :: [TyConBinder] -> Kind -> Kind
478 mkTyConKind bndrs res_kind = foldr mk res_kind bndrs
479 where
480 mk :: TyConBinder -> Kind -> Kind
481 mk (Bndr tv (AnonTCB af)) k = mkFunTy af (varType tv) k
482 mk (Bndr tv (NamedTCB vis)) k = mkForAllTy tv vis k
483
484 tyConTyVarBinders :: [TyConBinder] -- From the TyCon
485 -> [TyVarBinder] -- Suitable for the foralls of a term function
486 -- See Note [Building TyVarBinders from TyConBinders]
487 tyConTyVarBinders tc_bndrs
488 = map mk_binder tc_bndrs
489 where
490 mk_binder (Bndr tv tc_vis) = mkTyVarBinder vis tv
491 where
492 vis = case tc_vis of
493 AnonTCB VisArg -> Specified
494 AnonTCB InvisArg -> Inferred -- See Note [AnonTCB InvisArg]
495 NamedTCB Required -> Specified
496 NamedTCB vis -> vis
497
498 -- Returns only tyvars, as covars are always inferred
499 tyConVisibleTyVars :: TyCon -> [TyVar]
500 tyConVisibleTyVars tc
501 = [ tv | Bndr tv vis <- tyConBinders tc
502 , isVisibleTcbVis vis ]
503
504 {- Note [AnonTCB InvisArg]
505 ~~~~~~~~~~~~~~~~~~~~~~~~~~
506 It's pretty rare to have an (AnonTCB InvisArg) binder. The
507 only way it can occur is through equality constraints in kinds. These
508 can arise in one of two ways:
509
510 * In a PromotedDataCon whose kind has an equality constraint:
511
512 'MkT :: forall a b. (a~b) => blah
513
514 See Note [Constraints in kinds] in TyCoRep, and
515 Note [Promoted data constructors] in this module.
516 * In a data type whose kind has an equality constraint, as in the
517 following example from #12102:
518
519 data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type
520
521 When mapping an (AnonTCB InvisArg) to an ArgFlag, in
522 tyConBndrVisArgFlag, we use "Inferred" to mean "the user cannot
523 specify this arguments, even with visible type/kind application;
524 instead the type checker must fill it in.
525
526 We map (AnonTCB VisArg) to Required, of course: the user must
527 provide it. It would be utterly wrong to do this for constraint
528 arguments, which is why AnonTCB must have the AnonArgFlag in
529 the first place.
530
531 Note [Building TyVarBinders from TyConBinders]
532 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
533 We sometimes need to build the quantified type of a value from
534 the TyConBinders of a type or class. For that we need not
535 TyConBinders but TyVarBinders (used in forall-type) E.g:
536
537 * From data T a = MkT (Maybe a)
538 we are going to make a data constructor with type
539 MkT :: forall a. Maybe a -> T a
540 See the TyCoVarBinders passed to buildDataCon
541
542 * From class C a where { op :: a -> Maybe a }
543 we are going to make a default method
544 $dmop :: forall a. C a => a -> Maybe a
545 See the TyCoVarBinders passed to mkSigmaTy in mkDefaultMethodType
546
547 Both of these are user-callable. (NB: default methods are not callable
548 directly by the user but rather via the code generated by 'deriving',
549 which uses visible type application; see mkDefMethBind.)
550
551 Since they are user-callable we must get their type-argument visibility
552 information right; and that info is in the TyConBinders.
553 Here is an example:
554
555 data App a b = MkApp (a b) -- App :: forall {k}. (k->*) -> k -> *
556
557 The TyCon has
558
559 tyConTyBinders = [ Named (Bndr (k :: *) Inferred), Anon (k->*), Anon k ]
560
561 The TyConBinders for App line up with App's kind, given above.
562
563 But the DataCon MkApp has the type
564 MkApp :: forall {k} (a:k->*) (b:k). a b -> App k a b
565
566 That is, its TyCoVarBinders should be
567
568 dataConUnivTyVarBinders = [ Bndr (k:*) Inferred
569 , Bndr (a:k->*) Specified
570 , Bndr (b:k) Specified ]
571
572 So tyConTyVarBinders converts TyCon's TyConBinders into TyVarBinders:
573 - variable names from the TyConBinders
574 - but changing Anon/Required to Specified
575
576 The last part about Required->Specified comes from this:
577 data T k (a:k) b = MkT (a b)
578 Here k is Required in T's kind, but we don't have Required binders in
579 the TyCoBinders for a term (see Note [No Required TyCoBinder in terms]
580 in TyCoRep), so we change it to Specified when making MkT's TyCoBinders
581 -}
582
583
584 {- Note [The binders/kind/arity fields of a TyCon]
585 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
586 All TyCons have this group of fields
587 tyConBinders :: [TyConBinder/TyConTyCoBinder]
588 tyConResKind :: Kind
589 tyConTyVars :: [TyVar] -- Cached = binderVars tyConBinders
590 -- NB: Currently (Aug 2018), TyCons that own this
591 -- field really only contain TyVars. So it is
592 -- [TyVar] instead of [TyCoVar].
593 tyConKind :: Kind -- Cached = mkTyConKind tyConBinders tyConResKind
594 tyConArity :: Arity -- Cached = length tyConBinders
595
596 They fit together like so:
597
598 * tyConBinders gives the telescope of type/coercion variables on the LHS of the
599 type declaration. For example:
600
601 type App a (b :: k) = a b
602
603 tyConBinders = [ Bndr (k::*) (NamedTCB Inferred)
604 , Bndr (a:k->*) AnonTCB
605 , Bndr (b:k) AnonTCB ]
606
607 Note that that are three binders here, including the
608 kind variable k.
609
610 * See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep
611 for what the visibility flag means.
612
613 * Each TyConBinder tyConBinders has a TyVar (sometimes it is TyCoVar), and
614 that TyVar may scope over some other part of the TyCon's definition. Eg
615 type T a = a -> a
616 we have
617 tyConBinders = [ Bndr (a:*) AnonTCB ]
618 synTcRhs = a -> a
619 So the 'a' scopes over the synTcRhs
620
621 * From the tyConBinders and tyConResKind we can get the tyConKind
622 E.g for our App example:
623 App :: forall k. (k->*) -> k -> *
624
625 We get a 'forall' in the kind for each NamedTCB, and an arrow
626 for each AnonTCB
627
628 tyConKind is the full kind of the TyCon, not just the result kind
629
630 * For type families, tyConArity is the arguments this TyCon must be
631 applied to, to be considered saturated. Here we mean "applied to in
632 the actual Type", not surface syntax; i.e. including implicit kind
633 variables. So it's just (length tyConBinders)
634
635 * For an algebraic data type, or data instance, the tyConResKind is
636 always (TYPE r); that is, the tyConBinders are enough to saturate
637 the type constructor. I'm not quite sure why we have this invariant,
638 but it's enforced by etaExpandAlgTyCon
639 -}
640
641 instance Outputable tv => Outputable (VarBndr tv TyConBndrVis) where
642 ppr (Bndr v bi) = ppr_bi bi <+> parens (ppr v)
643 where
644 ppr_bi (AnonTCB VisArg) = text "anon-vis"
645 ppr_bi (AnonTCB InvisArg) = text "anon-invis"
646 ppr_bi (NamedTCB Required) = text "req"
647 ppr_bi (NamedTCB Specified) = text "spec"
648 ppr_bi (NamedTCB Inferred) = text "inf"
649
650 instance Binary TyConBndrVis where
651 put_ bh (AnonTCB af) = do { putByte bh 0; put_ bh af }
652 put_ bh (NamedTCB vis) = do { putByte bh 1; put_ bh vis }
653
654 get bh = do { h <- getByte bh
655 ; case h of
656 0 -> do { af <- get bh; return (AnonTCB af) }
657 _ -> do { vis <- get bh; return (NamedTCB vis) } }
658
659
660 {- *********************************************************************
661 * *
662 The TyCon type
663 * *
664 ************************************************************************
665 -}
666
667
668 -- | TyCons represent type constructors. Type constructors are introduced by
669 -- things such as:
670 --
671 -- 1) Data declarations: @data Foo = ...@ creates the @Foo@ type constructor of
672 -- kind @*@
673 --
674 -- 2) Type synonyms: @type Foo = ...@ creates the @Foo@ type constructor
675 --
676 -- 3) Newtypes: @newtype Foo a = MkFoo ...@ creates the @Foo@ type constructor
677 -- of kind @* -> *@
678 --
679 -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor
680 -- of kind @*@
681 --
682 -- This data type also encodes a number of primitive, built in type constructors
683 -- such as those for function and tuple types.
684
685 -- If you edit this type, you may need to update the GHC formalism
686 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
687 data TyCon
688 = -- | The function type constructor, @(->)@
689 FunTyCon {
690 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
691 -- identical to Unique of Name stored in
692 -- tyConName field.
693
694 tyConName :: Name, -- ^ Name of the constructor
695
696 -- See Note [The binders/kind/arity fields of a TyCon]
697 tyConBinders :: [TyConBinder], -- ^ Full binders
698 tyConResKind :: Kind, -- ^ Result kind
699 tyConKind :: Kind, -- ^ Kind of this TyCon
700 tyConArity :: Arity, -- ^ Arity
701
702 tcRepName :: TyConRepName
703 }
704
705 -- | Algebraic data types, from
706 -- - @data@ declarations
707 -- - @newtype@ declarations
708 -- - data instance declarations
709 -- - type instance declarations
710 -- - the TyCon generated by a class declaration
711 -- - boxed tuples
712 -- - unboxed tuples
713 -- - constraint tuples
714 -- All these constructors are lifted and boxed except unboxed tuples
715 -- which should have an 'UnboxedAlgTyCon' parent.
716 -- Data/newtype/type /families/ are handled by 'FamilyTyCon'.
717 -- See 'AlgTyConRhs' for more information.
718 | AlgTyCon {
719 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
720 -- identical to Unique of Name stored in
721 -- tyConName field.
722
723 tyConName :: Name, -- ^ Name of the constructor
724
725 -- See Note [The binders/kind/arity fields of a TyCon]
726 tyConBinders :: [TyConBinder], -- ^ Full binders
727 tyConTyVars :: [TyVar], -- ^ TyVar binders
728 tyConResKind :: Kind, -- ^ Result kind
729 tyConKind :: Kind, -- ^ Kind of this TyCon
730 tyConArity :: Arity, -- ^ Arity
731
732 -- The tyConTyVars scope over:
733 --
734 -- 1. The 'algTcStupidTheta'
735 -- 2. The cached types in algTyConRhs.NewTyCon
736 -- 3. The family instance types if present
737 --
738 -- Note that it does /not/ scope over the data
739 -- constructors.
740
741 tcRoles :: [Role], -- ^ The role for each type variable
742 -- This list has length = tyConArity
743 -- See also Note [TyCon Role signatures]
744
745 tyConCType :: Maybe CType,-- ^ The C type that should be used
746 -- for this type when using the FFI
747 -- and CAPI
748
749 algTcGadtSyntax :: Bool, -- ^ Was the data type declared with GADT
750 -- syntax? If so, that doesn't mean it's a
751 -- true GADT; only that the "where" form
752 -- was used. This field is used only to
753 -- guide pretty-printing
754
755 algTcStupidTheta :: [PredType], -- ^ The \"stupid theta\" for the data
756 -- type (always empty for GADTs). A
757 -- \"stupid theta\" is the context to
758 -- the left of an algebraic type
759 -- declaration, e.g. @Eq a@ in the
760 -- declaration @data Eq a => T a ...@.
761
762 algTcRhs :: AlgTyConRhs, -- ^ Contains information about the
763 -- data constructors of the algebraic type
764
765 algTcFields :: FieldLabelEnv, -- ^ Maps a label to information
766 -- about the field
767
768 algTcParent :: AlgTyConFlav -- ^ Gives the class or family declaration
769 -- 'TyCon' for derived 'TyCon's representing
770 -- class or family instances, respectively.
771
772 }
773
774 -- | Represents type synonyms
775 | SynonymTyCon {
776 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
777 -- identical to Unique of Name stored in
778 -- tyConName field.
779
780 tyConName :: Name, -- ^ Name of the constructor
781
782 -- See Note [The binders/kind/arity fields of a TyCon]
783 tyConBinders :: [TyConBinder], -- ^ Full binders
784 tyConTyVars :: [TyVar], -- ^ TyVar binders
785 tyConResKind :: Kind, -- ^ Result kind
786 tyConKind :: Kind, -- ^ Kind of this TyCon
787 tyConArity :: Arity, -- ^ Arity
788 -- tyConTyVars scope over: synTcRhs
789
790 tcRoles :: [Role], -- ^ The role for each type variable
791 -- This list has length = tyConArity
792 -- See also Note [TyCon Role signatures]
793
794 synTcRhs :: Type, -- ^ Contains information about the expansion
795 -- of the synonym
796
797 synIsTau :: Bool, -- True <=> the RHS of this synonym does not
798 -- have any foralls, after expanding any
799 -- nested synonyms
800 synIsFamFree :: Bool -- True <=> the RHS of this synonym does not mention
801 -- any type synonym families (data families
802 -- are fine), again after expanding any
803 -- nested synonyms
804 }
805
806 -- | Represents families (both type and data)
807 -- Argument roles are all Nominal
808 | FamilyTyCon {
809 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
810 -- identical to Unique of Name stored in
811 -- tyConName field.
812
813 tyConName :: Name, -- ^ Name of the constructor
814
815 -- See Note [The binders/kind/arity fields of a TyCon]
816 tyConBinders :: [TyConBinder], -- ^ Full binders
817 tyConTyVars :: [TyVar], -- ^ TyVar binders
818 tyConResKind :: Kind, -- ^ Result kind
819 tyConKind :: Kind, -- ^ Kind of this TyCon
820 tyConArity :: Arity, -- ^ Arity
821 -- tyConTyVars connect an associated family TyCon
822 -- with its parent class; see TcValidity.checkConsistentFamInst
823
824 famTcResVar :: Maybe Name, -- ^ Name of result type variable, used
825 -- for pretty-printing with --show-iface
826 -- and for reifying TyCon in Template
827 -- Haskell
828
829 famTcFlav :: FamTyConFlav, -- ^ Type family flavour: open, closed,
830 -- abstract, built-in. See comments for
831 -- FamTyConFlav
832
833 famTcParent :: Maybe TyCon, -- ^ For *associated* type/data families
834 -- The class tycon in which the family is declared
835 -- See Note [Associated families and their parent class]
836
837 famTcInj :: Injectivity -- ^ is this a type family injective in
838 -- its type variables? Nothing if no
839 -- injectivity annotation was given
840 }
841
842 -- | Primitive types; cannot be defined in Haskell. This includes
843 -- the usual suspects (such as @Int#@) as well as foreign-imported
844 -- types and kinds (@*@, @#@, and @?@)
845 | PrimTyCon {
846 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
847 -- identical to Unique of Name stored in
848 -- tyConName field.
849
850 tyConName :: Name, -- ^ Name of the constructor
851
852 -- See Note [The binders/kind/arity fields of a TyCon]
853 tyConBinders :: [TyConBinder], -- ^ Full binders
854 tyConResKind :: Kind, -- ^ Result kind
855 tyConKind :: Kind, -- ^ Kind of this TyCon
856 tyConArity :: Arity, -- ^ Arity
857
858 tcRoles :: [Role], -- ^ The role for each type variable
859 -- This list has length = tyConArity
860 -- See also Note [TyCon Role signatures]
861
862 isUnlifted :: Bool, -- ^ Most primitive tycons are unlifted (may
863 -- not contain bottom) but other are lifted,
864 -- e.g. @RealWorld@
865 -- Only relevant if tyConKind = *
866
867 primRepName :: Maybe TyConRepName -- Only relevant for kind TyCons
868 -- i.e, *, #, ?
869 }
870
871 -- | Represents promoted data constructor.
872 | PromotedDataCon { -- See Note [Promoted data constructors]
873 tyConUnique :: Unique, -- ^ Same Unique as the data constructor
874 tyConName :: Name, -- ^ Same Name as the data constructor
875
876 -- See Note [The binders/kind/arity fields of a TyCon]
877 tyConBinders :: [TyConTyCoBinder], -- ^ Full binders
878 tyConResKind :: Kind, -- ^ Result kind
879 tyConKind :: Kind, -- ^ Kind of this TyCon
880 tyConArity :: Arity, -- ^ Arity
881
882 tcRoles :: [Role], -- ^ Roles: N for kind vars, R for type vars
883 dataCon :: DataCon, -- ^ Corresponding data constructor
884 tcRepName :: TyConRepName,
885 promDcRepInfo :: RuntimeRepInfo -- ^ See comments with 'RuntimeRepInfo'
886 }
887
888 -- | These exist only during type-checking. See Note [How TcTyCons work]
889 -- in TcTyClsDecls
890 | TcTyCon {
891 tyConUnique :: Unique,
892 tyConName :: Name,
893
894 -- See Note [The binders/kind/arity fields of a TyCon]
895 tyConBinders :: [TyConBinder], -- ^ Full binders
896 tyConTyVars :: [TyVar], -- ^ TyVar binders
897 tyConResKind :: Kind, -- ^ Result kind
898 tyConKind :: Kind, -- ^ Kind of this TyCon
899 tyConArity :: Arity, -- ^ Arity
900
901 -- NB: the TyConArity of a TcTyCon must match
902 -- the number of Required (positional, user-specified)
903 -- arguments to the type constructor; see the use
904 -- of tyConArity in generaliseTcTyCon
905
906 tcTyConScopedTyVars :: [(Name,TyVar)],
907 -- ^ Scoped tyvars over the tycon's body
908 -- See Note [Scoped tyvars in a TcTyCon]
909
910 tcTyConIsPoly :: Bool, -- ^ Is this TcTyCon already generalized?
911
912 tcTyConFlavour :: TyConFlavour
913 -- ^ What sort of 'TyCon' this represents.
914 }
915 {- Note [Scoped tyvars in a TcTyCon]
916
917 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
918 The tcTyConScopedTyVars field records the lexicial-binding connection
919 between the original, user-specified Name (i.e. thing in scope) and
920 the TcTyVar that the Name is bound to.
921
922 Order *does* matter; the tcTyConScopedTyvars list consists of
923 specified_tvs ++ required_tvs
924
925 where
926 * specified ones first
927 * required_tvs the same as tyConTyVars
928 * tyConArity = length required_tvs
929
930 See also Note [How TcTyCons work] in TcTyClsDecls
931 -}
932
933 -- | Represents right-hand-sides of 'TyCon's for algebraic types
934 data AlgTyConRhs
935
936 -- | Says that we know nothing about this data type, except that
937 -- it's represented by a pointer. Used when we export a data type
938 -- abstractly into an .hi file.
939 = AbstractTyCon
940
941 -- | Information about those 'TyCon's derived from a @data@
942 -- declaration. This includes data types with no constructors at
943 -- all.
944 | DataTyCon {
945 data_cons :: [DataCon],
946 -- ^ The data type constructors; can be empty if the
947 -- user declares the type to have no constructors
948 --
949 -- INVARIANT: Kept in order of increasing 'DataCon'
950 -- tag (see the tag assignment in mkTyConTagMap)
951 data_cons_size :: Int,
952 -- ^ Cached value: length data_cons
953 is_enum :: Bool -- ^ Cached value: is this an enumeration type?
954 -- See Note [Enumeration types]
955 }
956
957 | TupleTyCon { -- A boxed, unboxed, or constraint tuple
958 data_con :: DataCon, -- NB: it can be an *unboxed* tuple
959 tup_sort :: TupleSort -- ^ Is this a boxed, unboxed or constraint
960 -- tuple?
961 }
962
963 -- | An unboxed sum type.
964 | SumTyCon {
965 data_cons :: [DataCon],
966 data_cons_size :: Int -- ^ Cached value: length data_cons
967 }
968
969 -- | Information about those 'TyCon's derived from a @newtype@ declaration
970 | NewTyCon {
971 data_con :: DataCon, -- ^ The unique constructor for the @newtype@.
972 -- It has no existentials
973
974 nt_rhs :: Type, -- ^ Cached value: the argument type of the
975 -- constructor, which is just the representation
976 -- type of the 'TyCon' (remember that @newtype@s
977 -- do not exist at runtime so need a different
978 -- representation type).
979 --
980 -- The free 'TyVar's of this type are the
981 -- 'tyConTyVars' from the corresponding 'TyCon'
982
983 nt_etad_rhs :: ([TyVar], Type),
984 -- ^ Same as the 'nt_rhs', but this time eta-reduced.
985 -- Hence the list of 'TyVar's in this field may be
986 -- shorter than the declared arity of the 'TyCon'.
987
988 -- See Note [Newtype eta]
989 nt_co :: CoAxiom Unbranched
990 -- The axiom coercion that creates the @newtype@
991 -- from the representation 'Type'.
992
993 -- See Note [Newtype coercions]
994 -- Invariant: arity = #tvs in nt_etad_rhs;
995 -- See Note [Newtype eta]
996 -- Watch out! If any newtypes become transparent
997 -- again check #1072.
998 }
999
1000 mkSumTyConRhs :: [DataCon] -> AlgTyConRhs
1001 mkSumTyConRhs data_cons = SumTyCon data_cons (length data_cons)
1002
1003 mkDataTyConRhs :: [DataCon] -> AlgTyConRhs
1004 mkDataTyConRhs cons
1005 = DataTyCon {
1006 data_cons = cons,
1007 data_cons_size = length cons,
1008 is_enum = not (null cons) && all is_enum_con cons
1009 -- See Note [Enumeration types] in TyCon
1010 }
1011 where
1012 is_enum_con con
1013 | (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res)
1014 <- dataConFullSig con
1015 = null ex_tvs && null eq_spec && null theta && null arg_tys
1016
1017 -- | Some promoted datacons signify extra info relevant to GHC. For example,
1018 -- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep'
1019 -- constructor of 'PrimRep'. This data structure allows us to store this
1020 -- information right in the 'TyCon'. The other approach would be to look
1021 -- up things like @RuntimeRep@'s @PrimRep@ by known-key every time.
1022 data RuntimeRepInfo
1023 = NoRRI -- ^ an ordinary promoted data con
1024 | RuntimeRep ([Type] -> [PrimRep])
1025 -- ^ A constructor of @RuntimeRep@. The argument to the function should
1026 -- be the list of arguments to the promoted datacon.
1027 | VecCount Int -- ^ A constructor of @VecCount@
1028 | VecElem PrimElemRep -- ^ A constructor of @VecElem@
1029
1030 -- | Extract those 'DataCon's that we are able to learn about. Note
1031 -- that visibility in this sense does not correspond to visibility in
1032 -- the context of any particular user program!
1033 visibleDataCons :: AlgTyConRhs -> [DataCon]
1034 visibleDataCons (AbstractTyCon {}) = []
1035 visibleDataCons (DataTyCon{ data_cons = cs }) = cs
1036 visibleDataCons (NewTyCon{ data_con = c }) = [c]
1037 visibleDataCons (TupleTyCon{ data_con = c }) = [c]
1038 visibleDataCons (SumTyCon{ data_cons = cs }) = cs
1039
1040 -- ^ Both type classes as well as family instances imply implicit
1041 -- type constructors. These implicit type constructors refer to their parent
1042 -- structure (ie, the class or family from which they derive) using a type of
1043 -- the following form.
1044 data AlgTyConFlav
1045 = -- | An ordinary type constructor has no parent.
1046 VanillaAlgTyCon
1047 TyConRepName
1048
1049 -- | An unboxed type constructor. The TyConRepName is a Maybe since we
1050 -- currently don't allow unboxed sums to be Typeable since there are too
1051 -- many of them. See #13276.
1052 | UnboxedAlgTyCon
1053 (Maybe TyConRepName)
1054
1055 -- | Type constructors representing a class dictionary.
1056 -- See Note [ATyCon for classes] in TyCoRep
1057 | ClassTyCon
1058 Class -- INVARIANT: the classTyCon of this Class is the
1059 -- current tycon
1060 TyConRepName
1061
1062 -- | Type constructors representing an *instance* of a *data* family.
1063 -- Parameters:
1064 --
1065 -- 1) The type family in question
1066 --
1067 -- 2) Instance types; free variables are the 'tyConTyVars'
1068 -- of the current 'TyCon' (not the family one). INVARIANT:
1069 -- the number of types matches the arity of the family 'TyCon'
1070 --
1071 -- 3) A 'CoTyCon' identifying the representation
1072 -- type with the type instance family
1073 | DataFamInstTyCon -- See Note [Data type families]
1074 (CoAxiom Unbranched) -- The coercion axiom.
1075 -- A *Representational* coercion,
1076 -- of kind T ty1 ty2 ~R R:T a b c
1077 -- where T is the family TyCon,
1078 -- and R:T is the representation TyCon (ie this one)
1079 -- and a,b,c are the tyConTyVars of this TyCon
1080 --
1081 -- BUT may be eta-reduced; see FamInstEnv
1082 -- Note [Eta reduction for data families]
1083
1084 -- Cached fields of the CoAxiom, but adjusted to
1085 -- use the tyConTyVars of this TyCon
1086 TyCon -- The family TyCon
1087 [Type] -- Argument types (mentions the tyConTyVars of this TyCon)
1088 -- No shorter in length than the tyConTyVars of the family TyCon
1089 -- How could it be longer? See [Arity of data families] in FamInstEnv
1090
1091 -- E.g. data instance T [a] = ...
1092 -- gives a representation tycon:
1093 -- data R:TList a = ...
1094 -- axiom co a :: T [a] ~ R:TList a
1095 -- with R:TList's algTcParent = DataFamInstTyCon T [a] co
1096
1097 instance Outputable AlgTyConFlav where
1098 ppr (VanillaAlgTyCon {}) = text "Vanilla ADT"
1099 ppr (UnboxedAlgTyCon {}) = text "Unboxed ADT"
1100 ppr (ClassTyCon cls _) = text "Class parent" <+> ppr cls
1101 ppr (DataFamInstTyCon _ tc tys) = text "Family parent (family instance)"
1102 <+> ppr tc <+> sep (map pprType tys)
1103
1104 -- | Checks the invariants of a 'AlgTyConFlav' given the appropriate type class
1105 -- name, if any
1106 okParent :: Name -> AlgTyConFlav -> Bool
1107 okParent _ (VanillaAlgTyCon {}) = True
1108 okParent _ (UnboxedAlgTyCon {}) = True
1109 okParent tc_name (ClassTyCon cls _) = tc_name == tyConName (classTyCon cls)
1110 okParent _ (DataFamInstTyCon _ fam_tc tys) = tys `lengthAtLeast` tyConArity fam_tc
1111
1112 isNoParent :: AlgTyConFlav -> Bool
1113 isNoParent (VanillaAlgTyCon {}) = True
1114 isNoParent _ = False
1115
1116 --------------------
1117
1118 data Injectivity
1119 = NotInjective
1120 | Injective [Bool] -- 1-1 with tyConTyVars (incl kind vars)
1121 deriving( Eq )
1122
1123 -- | Information pertaining to the expansion of a type synonym (@type@)
1124 data FamTyConFlav
1125 = -- | Represents an open type family without a fixed right hand
1126 -- side. Additional instances can appear at any time.
1127 --
1128 -- These are introduced by either a top level declaration:
1129 --
1130 -- > data family T a :: *
1131 --
1132 -- Or an associated data type declaration, within a class declaration:
1133 --
1134 -- > class C a b where
1135 -- > data T b :: *
1136 DataFamilyTyCon
1137 TyConRepName
1138
1139 -- | An open type synonym family e.g. @type family F x y :: * -> *@
1140 | OpenSynFamilyTyCon
1141
1142 -- | A closed type synonym family e.g.
1143 -- @type family F x where { F Int = Bool }@
1144 | ClosedSynFamilyTyCon (Maybe (CoAxiom Branched))
1145 -- See Note [Closed type families]
1146
1147 -- | A closed type synonym family declared in an hs-boot file with
1148 -- type family F a where ..
1149 | AbstractClosedSynFamilyTyCon
1150
1151 -- | Built-in type family used by the TypeNats solver
1152 | BuiltInSynFamTyCon BuiltInSynFamily
1153
1154 instance Outputable FamTyConFlav where
1155 ppr (DataFamilyTyCon n) = text "data family" <+> ppr n
1156 ppr OpenSynFamilyTyCon = text "open type family"
1157 ppr (ClosedSynFamilyTyCon Nothing) = text "closed type family"
1158 ppr (ClosedSynFamilyTyCon (Just coax)) = text "closed type family" <+> ppr coax
1159 ppr AbstractClosedSynFamilyTyCon = text "abstract closed type family"
1160 ppr (BuiltInSynFamTyCon _) = text "built-in type family"
1161
1162 {- Note [Closed type families]
1163 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1164 * In an open type family you can add new instances later. This is the
1165 usual case.
1166
1167 * In a closed type family you can only put equations where the family
1168 is defined.
1169
1170 A non-empty closed type family has a single axiom with multiple
1171 branches, stored in the 'ClosedSynFamilyTyCon' constructor. A closed
1172 type family with no equations does not have an axiom, because there is
1173 nothing for the axiom to prove!
1174
1175
1176 Note [Promoted data constructors]
1177 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1178 All data constructors can be promoted to become a type constructor,
1179 via the PromotedDataCon alternative in TyCon.
1180
1181 * The TyCon promoted from a DataCon has the *same* Name and Unique as
1182 the DataCon. Eg. If the data constructor Data.Maybe.Just(unique 78,
1183 say) is promoted to a TyCon whose name is Data.Maybe.Just(unique 78)
1184
1185 * We promote the *user* type of the DataCon. Eg
1186 data T = MkT {-# UNPACK #-} !(Bool, Bool)
1187 The promoted kind is
1188 'MkT :: (Bool,Bool) -> T
1189 *not*
1190 'MkT :: Bool -> Bool -> T
1191
1192 * Similarly for GADTs:
1193 data G a where
1194 MkG :: forall b. b -> G [b]
1195 The promoted data constructor has kind
1196 'MkG :: forall b. b -> G [b]
1197 *not*
1198 'MkG :: forall a b. (a ~# [b]) => b -> G a
1199
1200 Note [Enumeration types]
1201 ~~~~~~~~~~~~~~~~~~~~~~~~
1202 We define datatypes with no constructors to *not* be
1203 enumerations; this fixes trac #2578, Otherwise we
1204 end up generating an empty table for
1205 <mod>_<type>_closure_tbl
1206 which is used by tagToEnum# to map Int# to constructors
1207 in an enumeration. The empty table apparently upset
1208 the linker.
1209
1210 Moreover, all the data constructor must be enumerations, meaning
1211 they have type (forall abc. T a b c). GADTs are not enumerations.
1212 For example consider
1213 data T a where
1214 T1 :: T Int
1215 T2 :: T Bool
1216 T3 :: T a
1217 What would [T1 ..] be? [T1,T3] :: T Int? Easiest thing is to exclude them.
1218 See #4528.
1219
1220 Note [Newtype coercions]
1221 ~~~~~~~~~~~~~~~~~~~~~~~~
1222 The NewTyCon field nt_co is a CoAxiom which is used for coercing from
1223 the representation type of the newtype, to the newtype itself. For
1224 example,
1225
1226 newtype T a = MkT (a -> a)
1227
1228 the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> t.
1229
1230 In the case that the right hand side is a type application
1231 ending with the same type variables as the left hand side, we
1232 "eta-contract" the coercion. So if we had
1233
1234 newtype S a = MkT [a]
1235
1236 then we would generate the arity 0 axiom CoS : S ~ []. The
1237 primary reason we do this is to make newtype deriving cleaner.
1238
1239 In the paper we'd write
1240 axiom CoT : (forall t. T t) ~ (forall t. [t])
1241 and then when we used CoT at a particular type, s, we'd say
1242 CoT @ s
1243 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
1244
1245 Note [Newtype eta]
1246 ~~~~~~~~~~~~~~~~~~
1247 Consider
1248 newtype Parser a = MkParser (IO a) deriving Monad
1249 Are these two types equal (to Core)?
1250 Monad Parser
1251 Monad IO
1252 which we need to make the derived instance for Monad Parser.
1253
1254 Well, yes. But to see that easily we eta-reduce the RHS type of
1255 Parser, in this case to ([], Froogle), so that even unsaturated applications
1256 of Parser will work right. This eta reduction is done when the type
1257 constructor is built, and cached in NewTyCon.
1258
1259 Here's an example that I think showed up in practice
1260 Source code:
1261 newtype T a = MkT [a]
1262 newtype Foo m = MkFoo (forall a. m a -> Int)
1263
1264 w1 :: Foo []
1265 w1 = ...
1266
1267 w2 :: Foo T
1268 w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
1269
1270 After desugaring, and discarding the data constructors for the newtypes,
1271 we get:
1272 w2 = w1 `cast` Foo CoT
1273 so the coercion tycon CoT must have
1274 kind: T ~ []
1275 and arity: 0
1276
1277 This eta-reduction is implemented in BuildTyCl.mkNewTyConRhs.
1278
1279
1280 ************************************************************************
1281 * *
1282 TyConRepName
1283 * *
1284 ********************************************************************* -}
1285
1286 type TyConRepName = Name -- The Name of the top-level declaration
1287 -- $tcMaybe :: Data.Typeable.Internal.TyCon
1288 -- $tcMaybe = TyCon { tyConName = "Maybe", ... }
1289
1290 tyConRepName_maybe :: TyCon -> Maybe TyConRepName
1291 tyConRepName_maybe (FunTyCon { tcRepName = rep_nm })
1292 = Just rep_nm
1293 tyConRepName_maybe (PrimTyCon { primRepName = mb_rep_nm })
1294 = mb_rep_nm
1295 tyConRepName_maybe (AlgTyCon { algTcParent = parent })
1296 | VanillaAlgTyCon rep_nm <- parent = Just rep_nm
1297 | ClassTyCon _ rep_nm <- parent = Just rep_nm
1298 | UnboxedAlgTyCon rep_nm <- parent = rep_nm
1299 tyConRepName_maybe (FamilyTyCon { famTcFlav = DataFamilyTyCon rep_nm })
1300 = Just rep_nm
1301 tyConRepName_maybe (PromotedDataCon { dataCon = dc, tcRepName = rep_nm })
1302 | isUnboxedSumCon dc -- see #13276
1303 = Nothing
1304 | otherwise
1305 = Just rep_nm
1306 tyConRepName_maybe _ = Nothing
1307
1308 -- | Make a 'Name' for the 'Typeable' representation of the given wired-in type
1309 mkPrelTyConRepName :: Name -> TyConRepName
1310 -- See Note [Grand plan for Typeable] in 'TcTypeable' in TcTypeable.
1311 mkPrelTyConRepName tc_name -- Prelude tc_name is always External,
1312 -- so nameModule will work
1313 = mkExternalName rep_uniq rep_mod rep_occ (nameSrcSpan tc_name)
1314 where
1315 name_occ = nameOccName tc_name
1316 name_mod = nameModule tc_name
1317 name_uniq = nameUnique tc_name
1318 rep_uniq | isTcOcc name_occ = tyConRepNameUnique name_uniq
1319 | otherwise = dataConTyRepNameUnique name_uniq
1320 (rep_mod, rep_occ) = tyConRepModOcc name_mod name_occ
1321
1322 -- | The name (and defining module) for the Typeable representation (TyCon) of a
1323 -- type constructor.
1324 --
1325 -- See Note [Grand plan for Typeable] in 'TcTypeable' in TcTypeable.
1326 tyConRepModOcc :: Module -> OccName -> (Module, OccName)
1327 tyConRepModOcc tc_module tc_occ = (rep_module, mkTyConRepOcc tc_occ)
1328 where
1329 rep_module
1330 | tc_module == gHC_PRIM = gHC_TYPES
1331 | otherwise = tc_module
1332
1333
1334 {- *********************************************************************
1335 * *
1336 PrimRep
1337 * *
1338 ************************************************************************
1339
1340 Note [rep swamp]
1341
1342 GHC has a rich selection of types that represent "primitive types" of
1343 one kind or another. Each of them makes a different set of
1344 distinctions, and mostly the differences are for good reasons,
1345 although it's probably true that we could merge some of these.
1346
1347 Roughly in order of "includes more information":
1348
1349 - A Width (cmm/CmmType) is simply a binary value with the specified
1350 number of bits. It may represent a signed or unsigned integer, a
1351 floating-point value, or an address.
1352
1353 data Width = W8 | W16 | W32 | W64 | W128
1354
1355 - Size, which is used in the native code generator, is Width +
1356 floating point information.
1357
1358 data Size = II8 | II16 | II32 | II64 | FF32 | FF64
1359
1360 it is necessary because e.g. the instruction to move a 64-bit float
1361 on x86 (movsd) is different from the instruction to move a 64-bit
1362 integer (movq), so the mov instruction is parameterised by Size.
1363
1364 - CmmType wraps Width with more information: GC ptr, float, or
1365 other value.
1366
1367 data CmmType = CmmType CmmCat Width
1368
1369 data CmmCat -- "Category" (not exported)
1370 = GcPtrCat -- GC pointer
1371 | BitsCat -- Non-pointer
1372 | FloatCat -- Float
1373
1374 It is important to have GcPtr information in Cmm, since we generate
1375 info tables containing pointerhood for the GC from this. As for
1376 why we have float (and not signed/unsigned) here, see Note [Signed
1377 vs unsigned].
1378
1379 - ArgRep makes only the distinctions necessary for the call and
1380 return conventions of the STG machine. It is essentially CmmType
1381 + void.
1382
1383 - PrimRep makes a few more distinctions than ArgRep: it divides
1384 non-GC-pointers into signed/unsigned and addresses, information
1385 that is necessary for passing these values to foreign functions.
1386
1387 There's another tension here: whether the type encodes its size in
1388 bytes, or whether its size depends on the machine word size. Width
1389 and CmmType have the size built-in, whereas ArgRep and PrimRep do not.
1390
1391 This means to turn an ArgRep/PrimRep into a CmmType requires DynFlags.
1392
1393 On the other hand, CmmType includes some "nonsense" values, such as
1394 CmmType GcPtrCat W32 on a 64-bit machine.
1395 -}
1396
1397 -- | A 'PrimRep' is an abstraction of a type. It contains information that
1398 -- the code generator needs in order to pass arguments, return results,
1399 -- and store values of this type.
1400 data PrimRep
1401 = VoidRep
1402 | LiftedRep
1403 | UnliftedRep -- ^ Unlifted pointer
1404 | Int8Rep -- ^ Signed, 8-bit value
1405 | Int16Rep -- ^ Signed, 16-bit value
1406 | IntRep -- ^ Signed, word-sized value
1407 | WordRep -- ^ Unsigned, word-sized value
1408 | Int64Rep -- ^ Signed, 64 bit value (with 32-bit words only)
1409 | Word8Rep -- ^ Unsigned, 8 bit value
1410 | Word16Rep -- ^ Unsigned, 16 bit value
1411 | Word64Rep -- ^ Unsigned, 64 bit value (with 32-bit words only)
1412 | AddrRep -- ^ A pointer, but /not/ to a Haskell value (use '(Un)liftedRep')
1413 | FloatRep
1414 | DoubleRep
1415 | VecRep Int PrimElemRep -- ^ A vector
1416 deriving( Eq, Show )
1417
1418 data PrimElemRep
1419 = Int8ElemRep
1420 | Int16ElemRep
1421 | Int32ElemRep
1422 | Int64ElemRep
1423 | Word8ElemRep
1424 | Word16ElemRep
1425 | Word32ElemRep
1426 | Word64ElemRep
1427 | FloatElemRep
1428 | DoubleElemRep
1429 deriving( Eq, Show )
1430
1431 instance Outputable PrimRep where
1432 ppr r = text (show r)
1433
1434 instance Outputable PrimElemRep where
1435 ppr r = text (show r)
1436
1437 isVoidRep :: PrimRep -> Bool
1438 isVoidRep VoidRep = True
1439 isVoidRep _other = False
1440
1441 isGcPtrRep :: PrimRep -> Bool
1442 isGcPtrRep LiftedRep = True
1443 isGcPtrRep UnliftedRep = True
1444 isGcPtrRep _ = False
1445
1446 -- | The size of a 'PrimRep' in bytes.
1447 --
1448 -- This applies also when used in a constructor, where we allow packing the
1449 -- fields. For instance, in @data Foo = Foo Float# Float#@ the two fields will
1450 -- take only 8 bytes, which for 64-bit arch will be equal to 1 word.
1451 -- See also mkVirtHeapOffsetsWithPadding for details of how data fields are
1452 -- layed out.
1453 primRepSizeB :: DynFlags -> PrimRep -> Int
1454 primRepSizeB dflags IntRep = wORD_SIZE dflags
1455 primRepSizeB dflags WordRep = wORD_SIZE dflags
1456 primRepSizeB _ Int8Rep = 1
1457 primRepSizeB _ Int16Rep = 2
1458 primRepSizeB _ Int64Rep = wORD64_SIZE
1459 primRepSizeB _ Word8Rep = 1
1460 primRepSizeB _ Word16Rep = 2
1461 primRepSizeB _ Word64Rep = wORD64_SIZE
1462 primRepSizeB _ FloatRep = fLOAT_SIZE
1463 primRepSizeB dflags DoubleRep = dOUBLE_SIZE dflags
1464 primRepSizeB dflags AddrRep = wORD_SIZE dflags
1465 primRepSizeB dflags LiftedRep = wORD_SIZE dflags
1466 primRepSizeB dflags UnliftedRep = wORD_SIZE dflags
1467 primRepSizeB _ VoidRep = 0
1468 primRepSizeB _ (VecRep len rep) = len * primElemRepSizeB rep
1469
1470 primElemRepSizeB :: PrimElemRep -> Int
1471 primElemRepSizeB Int8ElemRep = 1
1472 primElemRepSizeB Int16ElemRep = 2
1473 primElemRepSizeB Int32ElemRep = 4
1474 primElemRepSizeB Int64ElemRep = 8
1475 primElemRepSizeB Word8ElemRep = 1
1476 primElemRepSizeB Word16ElemRep = 2
1477 primElemRepSizeB Word32ElemRep = 4
1478 primElemRepSizeB Word64ElemRep = 8
1479 primElemRepSizeB FloatElemRep = 4
1480 primElemRepSizeB DoubleElemRep = 8
1481
1482 -- | Return if Rep stands for floating type,
1483 -- returns Nothing for vector types.
1484 primRepIsFloat :: PrimRep -> Maybe Bool
1485 primRepIsFloat FloatRep = Just True
1486 primRepIsFloat DoubleRep = Just True
1487 primRepIsFloat (VecRep _ _) = Nothing
1488 primRepIsFloat _ = Just False
1489
1490
1491 {-
1492 ************************************************************************
1493 * *
1494 Field labels
1495 * *
1496 ************************************************************************
1497 -}
1498
1499 -- | The labels for the fields of this particular 'TyCon'
1500 tyConFieldLabels :: TyCon -> [FieldLabel]
1501 tyConFieldLabels tc = dFsEnvElts $ tyConFieldLabelEnv tc
1502
1503 -- | The labels for the fields of this particular 'TyCon'
1504 tyConFieldLabelEnv :: TyCon -> FieldLabelEnv
1505 tyConFieldLabelEnv tc
1506 | isAlgTyCon tc = algTcFields tc
1507 | otherwise = emptyDFsEnv
1508
1509 -- | Look up a field label belonging to this 'TyCon'
1510 lookupTyConFieldLabel :: FieldLabelString -> TyCon -> Maybe FieldLabel
1511 lookupTyConFieldLabel lbl tc = lookupDFsEnv (tyConFieldLabelEnv tc) lbl
1512
1513 -- | Make a map from strings to FieldLabels from all the data
1514 -- constructors of this algebraic tycon
1515 fieldsOfAlgTcRhs :: AlgTyConRhs -> FieldLabelEnv
1516 fieldsOfAlgTcRhs rhs = mkDFsEnv [ (flLabel fl, fl)
1517 | fl <- dataConsFields (visibleDataCons rhs) ]
1518 where
1519 -- Duplicates in this list will be removed by 'mkFsEnv'
1520 dataConsFields dcs = concatMap dataConFieldLabels dcs
1521
1522
1523 {-
1524 ************************************************************************
1525 * *
1526 \subsection{TyCon Construction}
1527 * *
1528 ************************************************************************
1529
1530 Note: the TyCon constructors all take a Kind as one argument, even though
1531 they could, in principle, work out their Kind from their other arguments.
1532 But to do so they need functions from Types, and that makes a nasty
1533 module mutual-recursion. And they aren't called from many places.
1534 So we compromise, and move their Kind calculation to the call site.
1535 -}
1536
1537 -- | Given the name of the function type constructor and it's kind, create the
1538 -- corresponding 'TyCon'. It is recommended to use 'TyCoRep.funTyCon' if you want
1539 -- this functionality
1540 mkFunTyCon :: Name -> [TyConBinder] -> Name -> TyCon
1541 mkFunTyCon name binders rep_nm
1542 = FunTyCon {
1543 tyConUnique = nameUnique name,
1544 tyConName = name,
1545 tyConBinders = binders,
1546 tyConResKind = liftedTypeKind,
1547 tyConKind = mkTyConKind binders liftedTypeKind,
1548 tyConArity = length binders,
1549 tcRepName = rep_nm
1550 }
1551
1552 -- | This is the making of an algebraic 'TyCon'. Notably, you have to
1553 -- pass in the generic (in the -XGenerics sense) information about the
1554 -- type constructor - you can get hold of it easily (see Generics
1555 -- module)
1556 mkAlgTyCon :: Name
1557 -> [TyConBinder] -- ^ Binders of the 'TyCon'
1558 -> Kind -- ^ Result kind
1559 -> [Role] -- ^ The roles for each TyVar
1560 -> Maybe CType -- ^ The C type this type corresponds to
1561 -- when using the CAPI FFI
1562 -> [PredType] -- ^ Stupid theta: see 'algTcStupidTheta'
1563 -> AlgTyConRhs -- ^ Information about data constructors
1564 -> AlgTyConFlav -- ^ What flavour is it?
1565 -- (e.g. vanilla, type family)
1566 -> Bool -- ^ Was the 'TyCon' declared with GADT syntax?
1567 -> TyCon
1568 mkAlgTyCon name binders res_kind roles cType stupid rhs parent gadt_syn
1569 = AlgTyCon {
1570 tyConName = name,
1571 tyConUnique = nameUnique name,
1572 tyConBinders = binders,
1573 tyConResKind = res_kind,
1574 tyConKind = mkTyConKind binders res_kind,
1575 tyConArity = length binders,
1576 tyConTyVars = binderVars binders,
1577 tcRoles = roles,
1578 tyConCType = cType,
1579 algTcStupidTheta = stupid,
1580 algTcRhs = rhs,
1581 algTcFields = fieldsOfAlgTcRhs rhs,
1582 algTcParent = ASSERT2( okParent name parent, ppr name $$ ppr parent ) parent,
1583 algTcGadtSyntax = gadt_syn
1584 }
1585
1586 -- | Simpler specialization of 'mkAlgTyCon' for classes
1587 mkClassTyCon :: Name -> [TyConBinder]
1588 -> [Role] -> AlgTyConRhs -> Class
1589 -> Name -> TyCon
1590 mkClassTyCon name binders roles rhs clas tc_rep_name
1591 = mkAlgTyCon name binders constraintKind roles Nothing [] rhs
1592 (ClassTyCon clas tc_rep_name)
1593 False
1594
1595 mkTupleTyCon :: Name
1596 -> [TyConBinder]
1597 -> Kind -- ^ Result kind of the 'TyCon'
1598 -> Arity -- ^ Arity of the tuple 'TyCon'
1599 -> DataCon
1600 -> TupleSort -- ^ Whether the tuple is boxed or unboxed
1601 -> AlgTyConFlav
1602 -> TyCon
1603 mkTupleTyCon name binders res_kind arity con sort parent
1604 = AlgTyCon {
1605 tyConUnique = nameUnique name,
1606 tyConName = name,
1607 tyConBinders = binders,
1608 tyConTyVars = binderVars binders,
1609 tyConResKind = res_kind,
1610 tyConKind = mkTyConKind binders res_kind,
1611 tyConArity = arity,
1612 tcRoles = replicate arity Representational,
1613 tyConCType = Nothing,
1614 algTcGadtSyntax = False,
1615 algTcStupidTheta = [],
1616 algTcRhs = TupleTyCon { data_con = con,
1617 tup_sort = sort },
1618 algTcFields = emptyDFsEnv,
1619 algTcParent = parent
1620 }
1621
1622 mkSumTyCon :: Name
1623 -> [TyConBinder]
1624 -> Kind -- ^ Kind of the resulting 'TyCon'
1625 -> Arity -- ^ Arity of the sum
1626 -> [TyVar] -- ^ 'TyVar's scoped over: see 'tyConTyVars'
1627 -> [DataCon]
1628 -> AlgTyConFlav
1629 -> TyCon
1630 mkSumTyCon name binders res_kind arity tyvars cons parent
1631 = AlgTyCon {
1632 tyConUnique = nameUnique name,
1633 tyConName = name,
1634 tyConBinders = binders,
1635 tyConTyVars = tyvars,
1636 tyConResKind = res_kind,
1637 tyConKind = mkTyConKind binders res_kind,
1638 tyConArity = arity,
1639 tcRoles = replicate arity Representational,
1640 tyConCType = Nothing,
1641 algTcGadtSyntax = False,
1642 algTcStupidTheta = [],
1643 algTcRhs = mkSumTyConRhs cons,
1644 algTcFields = emptyDFsEnv,
1645 algTcParent = parent
1646 }
1647
1648 -- | Makes a tycon suitable for use during type-checking. It stores
1649 -- a variety of details about the definition of the TyCon, but no
1650 -- right-hand side. It lives only during the type-checking of a
1651 -- mutually-recursive group of tycons; it is then zonked to a proper
1652 -- TyCon in zonkTcTyCon.
1653 -- See also Note [Kind checking recursive type and class declarations]
1654 -- in TcTyClsDecls.
1655 mkTcTyCon :: Name
1656 -> [TyConBinder]
1657 -> Kind -- ^ /result/ kind only
1658 -> [(Name,TcTyVar)] -- ^ Scoped type variables;
1659 -- see Note [How TcTyCons work] in TcTyClsDecls
1660 -> Bool -- ^ Is this TcTyCon generalised already?
1661 -> TyConFlavour -- ^ What sort of 'TyCon' this represents
1662 -> TyCon
1663 mkTcTyCon name binders res_kind scoped_tvs poly flav
1664 = TcTyCon { tyConUnique = getUnique name
1665 , tyConName = name
1666 , tyConTyVars = binderVars binders
1667 , tyConBinders = binders
1668 , tyConResKind = res_kind
1669 , tyConKind = mkTyConKind binders res_kind
1670 , tyConArity = length binders
1671 , tcTyConScopedTyVars = scoped_tvs
1672 , tcTyConIsPoly = poly
1673 , tcTyConFlavour = flav }
1674
1675 -- | Create an unlifted primitive 'TyCon', such as @Int#@.
1676 mkPrimTyCon :: Name -> [TyConBinder]
1677 -> Kind -- ^ /result/ kind, never levity-polymorphic
1678 -> [Role] -> TyCon
1679 mkPrimTyCon name binders res_kind roles
1680 = mkPrimTyCon' name binders res_kind roles True (Just $ mkPrelTyConRepName name)
1681
1682 -- | Kind constructors
1683 mkKindTyCon :: Name -> [TyConBinder]
1684 -> Kind -- ^ /result/ kind
1685 -> [Role] -> Name -> TyCon
1686 mkKindTyCon name binders res_kind roles rep_nm
1687 = tc
1688 where
1689 tc = mkPrimTyCon' name binders res_kind roles False (Just rep_nm)
1690
1691 -- | Create a lifted primitive 'TyCon' such as @RealWorld@
1692 mkLiftedPrimTyCon :: Name -> [TyConBinder]
1693 -> Kind -- ^ /result/ kind
1694 -> [Role] -> TyCon
1695 mkLiftedPrimTyCon name binders res_kind roles
1696 = mkPrimTyCon' name binders res_kind roles False (Just rep_nm)
1697 where rep_nm = mkPrelTyConRepName name
1698
1699 mkPrimTyCon' :: Name -> [TyConBinder]
1700 -> Kind -- ^ /result/ kind, never levity-polymorphic
1701 -- (If you need a levity-polymorphic PrimTyCon, change
1702 -- isTcLevPoly.)
1703 -> [Role]
1704 -> Bool -> Maybe TyConRepName -> TyCon
1705 mkPrimTyCon' name binders res_kind roles is_unlifted rep_nm
1706 = PrimTyCon {
1707 tyConName = name,
1708 tyConUnique = nameUnique name,
1709 tyConBinders = binders,
1710 tyConResKind = res_kind,
1711 tyConKind = mkTyConKind binders res_kind,
1712 tyConArity = length roles,
1713 tcRoles = roles,
1714 isUnlifted = is_unlifted,
1715 primRepName = rep_nm
1716 }
1717
1718 -- | Create a type synonym 'TyCon'
1719 mkSynonymTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind
1720 -> [Role] -> Type -> Bool -> Bool -> TyCon
1721 mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
1722 = SynonymTyCon {
1723 tyConName = name,
1724 tyConUnique = nameUnique name,
1725 tyConBinders = binders,
1726 tyConResKind = res_kind,
1727 tyConKind = mkTyConKind binders res_kind,
1728 tyConArity = length binders,
1729 tyConTyVars = binderVars binders,
1730 tcRoles = roles,
1731 synTcRhs = rhs,
1732 synIsTau = is_tau,
1733 synIsFamFree = is_fam_free
1734 }
1735
1736 -- | Create a type family 'TyCon'
1737 mkFamilyTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind
1738 -> Maybe Name -> FamTyConFlav
1739 -> Maybe Class -> Injectivity -> TyCon
1740 mkFamilyTyCon name binders res_kind resVar flav parent inj
1741 = FamilyTyCon
1742 { tyConUnique = nameUnique name
1743 , tyConName = name
1744 , tyConBinders = binders
1745 , tyConResKind = res_kind
1746 , tyConKind = mkTyConKind binders res_kind
1747 , tyConArity = length binders
1748 , tyConTyVars = binderVars binders
1749 , famTcResVar = resVar
1750 , famTcFlav = flav
1751 , famTcParent = classTyCon <$> parent
1752 , famTcInj = inj
1753 }
1754
1755
1756 -- | Create a promoted data constructor 'TyCon'
1757 -- Somewhat dodgily, we give it the same Name
1758 -- as the data constructor itself; when we pretty-print
1759 -- the TyCon we add a quote; see the Outputable TyCon instance
1760 mkPromotedDataCon :: DataCon -> Name -> TyConRepName
1761 -> [TyConTyCoBinder] -> Kind -> [Role]
1762 -> RuntimeRepInfo -> TyCon
1763 mkPromotedDataCon con name rep_name binders res_kind roles rep_info
1764 = PromotedDataCon {
1765 tyConUnique = nameUnique name,
1766 tyConName = name,
1767 tyConArity = length roles,
1768 tcRoles = roles,
1769 tyConBinders = binders,
1770 tyConResKind = res_kind,
1771 tyConKind = mkTyConKind binders res_kind,
1772 dataCon = con,
1773 tcRepName = rep_name,
1774 promDcRepInfo = rep_info
1775 }
1776
1777 isFunTyCon :: TyCon -> Bool
1778 isFunTyCon (FunTyCon {}) = True
1779 isFunTyCon _ = False
1780
1781 -- | Test if the 'TyCon' is algebraic but abstract (invisible data constructors)
1782 isAbstractTyCon :: TyCon -> Bool
1783 isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon }) = True
1784 isAbstractTyCon _ = False
1785
1786 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
1787 isPrimTyCon :: TyCon -> Bool
1788 isPrimTyCon (PrimTyCon {}) = True
1789 isPrimTyCon _ = False
1790
1791 -- | Is this 'TyCon' unlifted (i.e. cannot contain bottom)? Note that this can
1792 -- only be true for primitive and unboxed-tuple 'TyCon's
1793 isUnliftedTyCon :: TyCon -> Bool
1794 isUnliftedTyCon (PrimTyCon {isUnlifted = is_unlifted})
1795 = is_unlifted
1796 isUnliftedTyCon (AlgTyCon { algTcRhs = rhs } )
1797 | TupleTyCon { tup_sort = sort } <- rhs
1798 = not (isBoxed (tupleSortBoxity sort))
1799 isUnliftedTyCon (AlgTyCon { algTcRhs = rhs } )
1800 | SumTyCon {} <- rhs
1801 = True
1802 isUnliftedTyCon _ = False
1803
1804 -- | Returns @True@ if the supplied 'TyCon' resulted from either a
1805 -- @data@ or @newtype@ declaration
1806 isAlgTyCon :: TyCon -> Bool
1807 isAlgTyCon (AlgTyCon {}) = True
1808 isAlgTyCon _ = False
1809
1810 -- | Returns @True@ for vanilla AlgTyCons -- that is, those created
1811 -- with a @data@ or @newtype@ declaration.
1812 isVanillaAlgTyCon :: TyCon -> Bool
1813 isVanillaAlgTyCon (AlgTyCon { algTcParent = VanillaAlgTyCon _ }) = True
1814 isVanillaAlgTyCon _ = False
1815
1816 isDataTyCon :: TyCon -> Bool
1817 -- ^ Returns @True@ for data types that are /definitely/ represented by
1818 -- heap-allocated constructors. These are scrutinised by Core-level
1819 -- @case@ expressions, and they get info tables allocated for them.
1820 --
1821 -- Generally, the function will be true for all @data@ types and false
1822 -- for @newtype@s, unboxed tuples, unboxed sums and type family
1823 -- 'TyCon's. But it is not guaranteed to return @True@ in all cases
1824 -- that it could.
1825 --
1826 -- NB: for a data type family, only the /instance/ 'TyCon's
1827 -- get an info table. The family declaration 'TyCon' does not
1828 isDataTyCon (AlgTyCon {algTcRhs = rhs})
1829 = case rhs of
1830 TupleTyCon { tup_sort = sort }
1831 -> isBoxed (tupleSortBoxity sort)
1832 SumTyCon {} -> False
1833 DataTyCon {} -> True
1834 NewTyCon {} -> False
1835 AbstractTyCon {} -> False -- We don't know, so return False
1836 isDataTyCon _ = False
1837
1838 -- | 'isInjectiveTyCon' is true of 'TyCon's for which this property holds
1839 -- (where X is the role passed in):
1840 -- If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
1841 -- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
1842 -- See also Note [Decomposing equality] in TcCanonical
1843 isInjectiveTyCon :: TyCon -> Role -> Bool
1844 isInjectiveTyCon _ Phantom = False
1845 isInjectiveTyCon (FunTyCon {}) _ = True
1846 isInjectiveTyCon (AlgTyCon {}) Nominal = True
1847 isInjectiveTyCon (AlgTyCon {algTcRhs = rhs}) Representational
1848 = isGenInjAlgRhs rhs
1849 isInjectiveTyCon (SynonymTyCon {}) _ = False
1850 isInjectiveTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ })
1851 Nominal = True
1852 isInjectiveTyCon (FamilyTyCon { famTcInj = Injective inj }) Nominal = and inj
1853 isInjectiveTyCon (FamilyTyCon {}) _ = False
1854 isInjectiveTyCon (PrimTyCon {}) _ = True
1855 isInjectiveTyCon (PromotedDataCon {}) _ = True
1856 isInjectiveTyCon (TcTyCon {}) _ = True
1857 -- Reply True for TcTyCon to minimise knock on type errors
1858 -- See Note [How TcTyCons work] item (1) in TcTyClsDecls
1859
1860 -- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
1861 -- (where X is the role passed in):
1862 -- If (T tys ~X t), then (t's head ~X T).
1863 -- See also Note [Decomposing equality] in TcCanonical
1864 isGenerativeTyCon :: TyCon -> Role -> Bool
1865 isGenerativeTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) Nominal = True
1866 isGenerativeTyCon (FamilyTyCon {}) _ = False
1867 -- in all other cases, injectivity implies generativity
1868 isGenerativeTyCon tc r = isInjectiveTyCon tc r
1869
1870 -- | Is this an 'AlgTyConRhs' of a 'TyCon' that is generative and injective
1871 -- with respect to representational equality?
1872 isGenInjAlgRhs :: AlgTyConRhs -> Bool
1873 isGenInjAlgRhs (TupleTyCon {}) = True
1874 isGenInjAlgRhs (SumTyCon {}) = True
1875 isGenInjAlgRhs (DataTyCon {}) = True
1876 isGenInjAlgRhs (AbstractTyCon {}) = False
1877 isGenInjAlgRhs (NewTyCon {}) = False
1878
1879 -- | Is this 'TyCon' that for a @newtype@
1880 isNewTyCon :: TyCon -> Bool
1881 isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True
1882 isNewTyCon _ = False
1883
1884 -- | Take a 'TyCon' apart into the 'TyVar's it scopes over, the 'Type' it
1885 -- expands into, and (possibly) a coercion from the representation type to the
1886 -- @newtype@.
1887 -- Returns @Nothing@ if this is not possible.
1888 unwrapNewTyCon_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched)
1889 unwrapNewTyCon_maybe (AlgTyCon { tyConTyVars = tvs,
1890 algTcRhs = NewTyCon { nt_co = co,
1891 nt_rhs = rhs }})
1892 = Just (tvs, rhs, co)
1893 unwrapNewTyCon_maybe _ = Nothing
1894
1895 unwrapNewTyConEtad_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched)
1896 unwrapNewTyConEtad_maybe (AlgTyCon { algTcRhs = NewTyCon { nt_co = co,
1897 nt_etad_rhs = (tvs,rhs) }})
1898 = Just (tvs, rhs, co)
1899 unwrapNewTyConEtad_maybe _ = Nothing
1900
1901 isProductTyCon :: TyCon -> Bool
1902 -- True of datatypes or newtypes that have
1903 -- one, non-existential, data constructor
1904 -- See Note [Product types]
1905 isProductTyCon tc@(AlgTyCon {})
1906 = case algTcRhs tc of
1907 TupleTyCon {} -> True
1908 DataTyCon{ data_cons = [data_con] }
1909 -> null (dataConExTyCoVars data_con)
1910 NewTyCon {} -> True
1911 _ -> False
1912 isProductTyCon _ = False
1913
1914 isDataProductTyCon_maybe :: TyCon -> Maybe DataCon
1915 -- True of datatypes (not newtypes) with
1916 -- one, vanilla, data constructor
1917 -- See Note [Product types]
1918 isDataProductTyCon_maybe (AlgTyCon { algTcRhs = rhs })
1919 = case rhs of
1920 DataTyCon { data_cons = [con] }
1921 | null (dataConExTyCoVars con) -- non-existential
1922 -> Just con
1923 TupleTyCon { data_con = con }
1924 -> Just con
1925 _ -> Nothing
1926 isDataProductTyCon_maybe _ = Nothing
1927
1928 isDataSumTyCon_maybe :: TyCon -> Maybe [DataCon]
1929 isDataSumTyCon_maybe (AlgTyCon { algTcRhs = rhs })
1930 = case rhs of
1931 DataTyCon { data_cons = cons }
1932 | cons `lengthExceeds` 1
1933 , all (null . dataConExTyCoVars) cons -- FIXME(osa): Why do we need this?
1934 -> Just cons
1935 SumTyCon { data_cons = cons }
1936 | all (null . dataConExTyCoVars) cons -- FIXME(osa): Why do we need this?
1937 -> Just cons
1938 _ -> Nothing
1939 isDataSumTyCon_maybe _ = Nothing
1940
1941 {- Note [Product types]
1942 ~~~~~~~~~~~~~~~~~~~~~~~
1943 A product type is
1944 * A data type (not a newtype)
1945 * With one, boxed data constructor
1946 * That binds no existential type variables
1947
1948 The main point is that product types are amenable to unboxing for
1949 * Strict function calls; we can transform
1950 f (D a b) = e
1951 to
1952 fw a b = e
1953 via the worker/wrapper transformation. (Question: couldn't this
1954 work for existentials too?)
1955
1956 * CPR for function results; we can transform
1957 f x y = let ... in D a b
1958 to
1959 fw x y = let ... in (# a, b #)
1960
1961 Note that the data constructor /can/ have evidence arguments: equality
1962 constraints, type classes etc. So it can be GADT. These evidence
1963 arguments are simply value arguments, and should not get in the way.
1964 -}
1965
1966
1967 -- | Is this a 'TyCon' representing a regular H98 type synonym (@type@)?
1968 isTypeSynonymTyCon :: TyCon -> Bool
1969 isTypeSynonymTyCon (SynonymTyCon {}) = True
1970 isTypeSynonymTyCon _ = False
1971
1972 isTauTyCon :: TyCon -> Bool
1973 isTauTyCon (SynonymTyCon { synIsTau = is_tau }) = is_tau
1974 isTauTyCon _ = True
1975
1976 isFamFreeTyCon :: TyCon -> Bool
1977 isFamFreeTyCon (SynonymTyCon { synIsFamFree = fam_free }) = fam_free
1978 isFamFreeTyCon (FamilyTyCon { famTcFlav = flav }) = isDataFamFlav flav
1979 isFamFreeTyCon _ = True
1980
1981 -- As for newtypes, it is in some contexts important to distinguish between
1982 -- closed synonyms and synonym families, as synonym families have no unique
1983 -- right hand side to which a synonym family application can expand.
1984 --
1985
1986 -- | True iff we can decompose (T a b c) into ((T a b) c)
1987 -- I.e. is it injective and generative w.r.t nominal equality?
1988 -- That is, if (T a b) ~N d e f, is it always the case that
1989 -- (T ~N d), (a ~N e) and (b ~N f)?
1990 -- Specifically NOT true of synonyms (open and otherwise)
1991 --
1992 -- It'd be unusual to call mustBeSaturated on a regular H98
1993 -- type synonym, because you should probably have expanded it first
1994 -- But regardless, it's not decomposable
1995 mustBeSaturated :: TyCon -> Bool
1996 mustBeSaturated = tcFlavourMustBeSaturated . tyConFlavour
1997
1998 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
1999 isGadtSyntaxTyCon :: TyCon -> Bool
2000 isGadtSyntaxTyCon (AlgTyCon { algTcGadtSyntax = res }) = res
2001 isGadtSyntaxTyCon _ = False
2002
2003 -- | Is this an algebraic 'TyCon' which is just an enumeration of values?
2004 isEnumerationTyCon :: TyCon -> Bool
2005 -- See Note [Enumeration types] in TyCon
2006 isEnumerationTyCon (AlgTyCon { tyConArity = arity, algTcRhs = rhs })
2007 = case rhs of
2008 DataTyCon { is_enum = res } -> res
2009 TupleTyCon {} -> arity == 0
2010 _ -> False
2011 isEnumerationTyCon _ = False
2012
2013 -- | Is this a 'TyCon', synonym or otherwise, that defines a family?
2014 isFamilyTyCon :: TyCon -> Bool
2015 isFamilyTyCon (FamilyTyCon {}) = True
2016 isFamilyTyCon _ = False
2017
2018 -- | Is this a 'TyCon', synonym or otherwise, that defines a family with
2019 -- instances?
2020 isOpenFamilyTyCon :: TyCon -> Bool
2021 isOpenFamilyTyCon (FamilyTyCon {famTcFlav = flav })
2022 | OpenSynFamilyTyCon <- flav = True
2023 | DataFamilyTyCon {} <- flav = True
2024 isOpenFamilyTyCon _ = False
2025
2026 -- | Is this a synonym 'TyCon' that can have may have further instances appear?
2027 isTypeFamilyTyCon :: TyCon -> Bool
2028 isTypeFamilyTyCon (FamilyTyCon { famTcFlav = flav }) = not (isDataFamFlav flav)
2029 isTypeFamilyTyCon _ = False
2030
2031 -- | Is this a synonym 'TyCon' that can have may have further instances appear?
2032 isDataFamilyTyCon :: TyCon -> Bool
2033 isDataFamilyTyCon (FamilyTyCon { famTcFlav = flav }) = isDataFamFlav flav
2034 isDataFamilyTyCon _ = False
2035
2036 -- | Is this an open type family TyCon?
2037 isOpenTypeFamilyTyCon :: TyCon -> Bool
2038 isOpenTypeFamilyTyCon (FamilyTyCon {famTcFlav = OpenSynFamilyTyCon }) = True
2039 isOpenTypeFamilyTyCon _ = False
2040
2041 -- | Is this a non-empty closed type family? Returns 'Nothing' for
2042 -- abstract or empty closed families.
2043 isClosedSynFamilyTyConWithAxiom_maybe :: TyCon -> Maybe (CoAxiom Branched)
2044 isClosedSynFamilyTyConWithAxiom_maybe
2045 (FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb}) = mb
2046 isClosedSynFamilyTyConWithAxiom_maybe _ = Nothing
2047
2048 -- | @'tyConInjectivityInfo' tc@ returns @'Injective' is@ is @tc@ is an
2049 -- injective tycon (where @is@ states for which 'tyConBinders' @tc@ is
2050 -- injective), or 'NotInjective' otherwise.
2051 tyConInjectivityInfo :: TyCon -> Injectivity
2052 tyConInjectivityInfo tc
2053 | FamilyTyCon { famTcInj = inj } <- tc
2054 = inj
2055 | isInjectiveTyCon tc Nominal
2056 = Injective (replicate (tyConArity tc) True)
2057 | otherwise
2058 = NotInjective
2059
2060 isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe BuiltInSynFamily
2061 isBuiltInSynFamTyCon_maybe
2062 (FamilyTyCon {famTcFlav = BuiltInSynFamTyCon ops }) = Just ops
2063 isBuiltInSynFamTyCon_maybe _ = Nothing
2064
2065 isDataFamFlav :: FamTyConFlav -> Bool
2066 isDataFamFlav (DataFamilyTyCon {}) = True -- Data family
2067 isDataFamFlav _ = False -- Type synonym family
2068
2069 -- | Is this TyCon for an associated type?
2070 isTyConAssoc :: TyCon -> Bool
2071 isTyConAssoc = isJust . tyConAssoc_maybe
2072
2073 -- | Get the enclosing class TyCon (if there is one) for the given TyCon.
2074 tyConAssoc_maybe :: TyCon -> Maybe TyCon
2075 tyConAssoc_maybe = tyConFlavourAssoc_maybe . tyConFlavour
2076
2077 -- | Get the enclosing class TyCon (if there is one) for the given TyConFlavour
2078 tyConFlavourAssoc_maybe :: TyConFlavour -> Maybe TyCon
2079 tyConFlavourAssoc_maybe (DataFamilyFlavour mb_parent) = mb_parent
2080 tyConFlavourAssoc_maybe (OpenTypeFamilyFlavour mb_parent) = mb_parent
2081 tyConFlavourAssoc_maybe _ = Nothing
2082
2083 -- The unit tycon didn't used to be classed as a tuple tycon
2084 -- but I thought that was silly so I've undone it
2085 -- If it can't be for some reason, it should be a AlgTyCon
2086 isTupleTyCon :: TyCon -> Bool
2087 -- ^ Does this 'TyCon' represent a tuple?
2088 --
2089 -- NB: when compiling @Data.Tuple@, the tycons won't reply @True@ to
2090 -- 'isTupleTyCon', because they are built as 'AlgTyCons'. However they
2091 -- get spat into the interface file as tuple tycons, so I don't think
2092 -- it matters.
2093 isTupleTyCon (AlgTyCon { algTcRhs = TupleTyCon {} }) = True
2094 isTupleTyCon _ = False
2095
2096 tyConTuple_maybe :: TyCon -> Maybe TupleSort
2097 tyConTuple_maybe (AlgTyCon { algTcRhs = rhs })
2098 | TupleTyCon { tup_sort = sort} <- rhs = Just sort
2099 tyConTuple_maybe _ = Nothing
2100
2101 -- | Is this the 'TyCon' for an unboxed tuple?
2102 isUnboxedTupleTyCon :: TyCon -> Bool
2103 isUnboxedTupleTyCon (AlgTyCon { algTcRhs = rhs })
2104 | TupleTyCon { tup_sort = sort } <- rhs
2105 = not (isBoxed (tupleSortBoxity sort))
2106 isUnboxedTupleTyCon _ = False
2107
2108 -- | Is this the 'TyCon' for a boxed tuple?
2109 isBoxedTupleTyCon :: TyCon -> Bool
2110 isBoxedTupleTyCon (AlgTyCon { algTcRhs = rhs })
2111 | TupleTyCon { tup_sort = sort } <- rhs
2112 = isBoxed (tupleSortBoxity sort)
2113 isBoxedTupleTyCon _ = False
2114
2115 -- | Is this the 'TyCon' for an unboxed sum?
2116 isUnboxedSumTyCon :: TyCon -> Bool
2117 isUnboxedSumTyCon (AlgTyCon { algTcRhs = rhs })
2118 | SumTyCon {} <- rhs
2119 = True
2120 isUnboxedSumTyCon _ = False
2121
2122 -- | Is this the 'TyCon' for a /promoted/ tuple?
2123 isPromotedTupleTyCon :: TyCon -> Bool
2124 isPromotedTupleTyCon tyCon
2125 | Just dataCon <- isPromotedDataCon_maybe tyCon
2126 , isTupleTyCon (dataConTyCon dataCon) = True
2127 | otherwise = False
2128
2129 -- | Is this a PromotedDataCon?
2130 isPromotedDataCon :: TyCon -> Bool
2131 isPromotedDataCon (PromotedDataCon {}) = True
2132 isPromotedDataCon _ = False
2133
2134 -- | Retrieves the promoted DataCon if this is a PromotedDataCon;
2135 isPromotedDataCon_maybe :: TyCon -> Maybe DataCon
2136 isPromotedDataCon_maybe (PromotedDataCon { dataCon = dc }) = Just dc
2137 isPromotedDataCon_maybe _ = Nothing
2138
2139 -- | Is this tycon really meant for use at the kind level? That is,
2140 -- should it be permitted without -XDataKinds?
2141 isKindTyCon :: TyCon -> Bool
2142 isKindTyCon tc = getUnique tc `elementOfUniqSet` kindTyConKeys
2143
2144 -- | These TyCons should be allowed at the kind level, even without
2145 -- -XDataKinds.
2146 kindTyConKeys :: UniqSet Unique
2147 kindTyConKeys = unionManyUniqSets
2148 ( mkUniqSet [ liftedTypeKindTyConKey, constraintKindTyConKey, tYPETyConKey ]
2149 : map (mkUniqSet . tycon_with_datacons) [ runtimeRepTyCon
2150 , vecCountTyCon, vecElemTyCon ] )
2151 where
2152 tycon_with_datacons tc = getUnique tc : map getUnique (tyConDataCons tc)
2153
2154 isLiftedTypeKindTyConName :: Name -> Bool
2155 isLiftedTypeKindTyConName = (`hasKey` liftedTypeKindTyConKey)
2156
2157 -- | Identifies implicit tycons that, in particular, do not go into interface
2158 -- files (because they are implicitly reconstructed when the interface is
2159 -- read).
2160 --
2161 -- Note that:
2162 --
2163 -- * Associated families are implicit, as they are re-constructed from
2164 -- the class declaration in which they reside, and
2165 --
2166 -- * Family instances are /not/ implicit as they represent the instance body
2167 -- (similar to a @dfun@ does that for a class instance).
2168 --
2169 -- * Tuples are implicit iff they have a wired-in name
2170 -- (namely: boxed and unboxed tupeles are wired-in and implicit,
2171 -- but constraint tuples are not)
2172 isImplicitTyCon :: TyCon -> Bool
2173 isImplicitTyCon (FunTyCon {}) = True
2174 isImplicitTyCon (PrimTyCon {}) = True
2175 isImplicitTyCon (PromotedDataCon {}) = True
2176 isImplicitTyCon (AlgTyCon { algTcRhs = rhs, tyConName = name })
2177 | TupleTyCon {} <- rhs = isWiredInName name
2178 | SumTyCon {} <- rhs = True
2179 | otherwise = False
2180 isImplicitTyCon (FamilyTyCon { famTcParent = parent }) = isJust parent
2181 isImplicitTyCon (SynonymTyCon {}) = False
2182 isImplicitTyCon (TcTyCon {}) = False
2183
2184 tyConCType_maybe :: TyCon -> Maybe CType
2185 tyConCType_maybe tc@(AlgTyCon {}) = tyConCType tc
2186 tyConCType_maybe _ = Nothing
2187
2188 -- | Is this a TcTyCon? (That is, one only used during type-checking?)
2189 isTcTyCon :: TyCon -> Bool
2190 isTcTyCon (TcTyCon {}) = True
2191 isTcTyCon _ = False
2192
2193 setTcTyConKind :: TyCon -> Kind -> TyCon
2194 -- Update the Kind of a TcTyCon
2195 -- The new kind is always a zonked version of its previous
2196 -- kind, so we don't need to update any other fields.
2197 -- See Note [The Purely Kinded Invariant] in TcHsType
2198 setTcTyConKind tc@(TcTyCon {}) kind = tc { tyConKind = kind }
2199 setTcTyConKind tc _ = pprPanic "setTcTyConKind" (ppr tc)
2200
2201 -- | Could this TyCon ever be levity-polymorphic when fully applied?
2202 -- True is safe. False means we're sure. Does only a quick check
2203 -- based on the TyCon's category.
2204 -- Precondition: The fully-applied TyCon has kind (TYPE blah)
2205 isTcLevPoly :: TyCon -> Bool
2206 isTcLevPoly FunTyCon{} = False
2207 isTcLevPoly (AlgTyCon { algTcParent = UnboxedAlgTyCon _ }) = True
2208 isTcLevPoly AlgTyCon{} = False
2209 isTcLevPoly SynonymTyCon{} = True
2210 isTcLevPoly FamilyTyCon{} = True
2211 isTcLevPoly PrimTyCon{} = False
2212 isTcLevPoly TcTyCon{} = False
2213 isTcLevPoly tc@PromotedDataCon{} = pprPanic "isTcLevPoly datacon" (ppr tc)
2214
2215 {-
2216 -----------------------------------------------
2217 -- Expand type-constructor applications
2218 -----------------------------------------------
2219 -}
2220
2221 expandSynTyCon_maybe
2222 :: TyCon
2223 -> [tyco] -- ^ Arguments to 'TyCon'
2224 -> Maybe ([(TyVar,tyco)],
2225 Type,
2226 [tyco]) -- ^ Returns a 'TyVar' substitution, the body
2227 -- type of the synonym (not yet substituted)
2228 -- and any arguments remaining from the
2229 -- application
2230
2231 -- ^ Expand a type synonym application, if any
2232 expandSynTyCon_maybe tc tys
2233 | SynonymTyCon { tyConTyVars = tvs, synTcRhs = rhs, tyConArity = arity } <- tc
2234 = case tys `listLengthCmp` arity of
2235 GT -> Just (tvs `zip` tys, rhs, drop arity tys)
2236 EQ -> Just (tvs `zip` tys, rhs, [])
2237 LT -> Nothing
2238 | otherwise
2239 = Nothing
2240
2241 ----------------
2242
2243 -- | Check if the tycon actually refers to a proper `data` or `newtype`
2244 -- with user defined constructors rather than one from a class or other
2245 -- construction.
2246
2247 -- NB: This is only used in TcRnExports.checkPatSynParent to determine if an
2248 -- exported tycon can have a pattern synonym bundled with it, e.g.,
2249 -- module Foo (TyCon(.., PatSyn)) where
2250 isTyConWithSrcDataCons :: TyCon -> Bool
2251 isTyConWithSrcDataCons (AlgTyCon { algTcRhs = rhs, algTcParent = parent }) =
2252 case rhs of
2253 DataTyCon {} -> isSrcParent
2254 NewTyCon {} -> isSrcParent
2255 TupleTyCon {} -> isSrcParent
2256 _ -> False
2257 where
2258 isSrcParent = isNoParent parent
2259 isTyConWithSrcDataCons (FamilyTyCon { famTcFlav = DataFamilyTyCon {} })
2260 = True -- #14058
2261 isTyConWithSrcDataCons _ = False
2262
2263
2264 -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no
2265 -- constructors could be found
2266 tyConDataCons :: TyCon -> [DataCon]
2267 -- It's convenient for tyConDataCons to return the
2268 -- empty list for type synonyms etc
2269 tyConDataCons tycon = tyConDataCons_maybe tycon `orElse` []
2270
2271 -- | Determine the 'DataCon's originating from the given 'TyCon', if the 'TyCon'
2272 -- is the sort that can have any constructors (note: this does not include
2273 -- abstract algebraic types)
2274 tyConDataCons_maybe :: TyCon -> Maybe [DataCon]
2275 tyConDataCons_maybe (AlgTyCon {algTcRhs = rhs})
2276 = case rhs of
2277 DataTyCon { data_cons = cons } -> Just cons
2278 NewTyCon { data_con = con } -> Just [con]
2279 TupleTyCon { data_con = con } -> Just [con]
2280 SumTyCon { data_cons = cons } -> Just cons
2281 _ -> Nothing
2282 tyConDataCons_maybe _ = Nothing
2283
2284 -- | If the given 'TyCon' has a /single/ data constructor, i.e. it is a @data@
2285 -- type with one alternative, a tuple type or a @newtype@ then that constructor
2286 -- is returned. If the 'TyCon' has more than one constructor, or represents a
2287 -- primitive or function type constructor then @Nothing@ is returned. In any
2288 -- other case, the function panics
2289 tyConSingleDataCon_maybe :: TyCon -> Maybe DataCon
2290 tyConSingleDataCon_maybe (AlgTyCon { algTcRhs = rhs })
2291 = case rhs of
2292 DataTyCon { data_cons = [c] } -> Just c
2293 TupleTyCon { data_con = c } -> Just c
2294 NewTyCon { data_con = c } -> Just c
2295 _ -> Nothing
2296 tyConSingleDataCon_maybe _ = Nothing
2297
2298 tyConSingleDataCon :: TyCon -> DataCon
2299 tyConSingleDataCon tc
2300 = case tyConSingleDataCon_maybe tc of
2301 Just c -> c
2302 Nothing -> pprPanic "tyConDataCon" (ppr tc)
2303
2304 tyConSingleAlgDataCon_maybe :: TyCon -> Maybe DataCon
2305 -- Returns (Just con) for single-constructor
2306 -- *algebraic* data types *not* newtypes
2307 tyConSingleAlgDataCon_maybe (AlgTyCon { algTcRhs = rhs })
2308 = case rhs of
2309 DataTyCon { data_cons = [c] } -> Just c
2310 TupleTyCon { data_con = c } -> Just c
2311 _ -> Nothing
2312 tyConSingleAlgDataCon_maybe _ = Nothing
2313
2314 -- | Determine the number of value constructors a 'TyCon' has. Panics if the
2315 -- 'TyCon' is not algebraic or a tuple
2316 tyConFamilySize :: TyCon -> Int
2317 tyConFamilySize tc@(AlgTyCon { algTcRhs = rhs })
2318 = case rhs of
2319 DataTyCon { data_cons_size = size } -> size
2320 NewTyCon {} -> 1
2321 TupleTyCon {} -> 1
2322 SumTyCon { data_cons_size = size } -> size
2323 _ -> pprPanic "tyConFamilySize 1" (ppr tc)
2324 tyConFamilySize tc = pprPanic "tyConFamilySize 2" (ppr tc)
2325
2326 -- | Extract an 'AlgTyConRhs' with information about data constructors from an
2327 -- algebraic or tuple 'TyCon'. Panics for any other sort of 'TyCon'
2328 algTyConRhs :: TyCon -> AlgTyConRhs
2329 algTyConRhs (AlgTyCon {algTcRhs = rhs}) = rhs
2330 algTyConRhs other = pprPanic "algTyConRhs" (ppr other)
2331
2332 -- | Extract type variable naming the result of injective type family
2333 tyConFamilyResVar_maybe :: TyCon -> Maybe Name
2334 tyConFamilyResVar_maybe (FamilyTyCon {famTcResVar = res}) = res
2335 tyConFamilyResVar_maybe _ = Nothing
2336
2337 -- | Get the list of roles for the type parameters of a TyCon
2338 tyConRoles :: TyCon -> [Role]
2339 -- See also Note [TyCon Role signatures]
2340 tyConRoles tc
2341 = case tc of
2342 { FunTyCon {} -> [Nominal, Nominal, Representational, Representational]
2343 ; AlgTyCon { tcRoles = roles } -> roles
2344 ; SynonymTyCon { tcRoles = roles } -> roles
2345 ; FamilyTyCon {} -> const_role Nominal
2346 ; PrimTyCon { tcRoles = roles } -> roles
2347 ; PromotedDataCon { tcRoles = roles } -> roles
2348 ; TcTyCon {} -> const_role Nominal
2349 }
2350 where
2351 const_role r = replicate (tyConArity tc) r
2352
2353 -- | Extract the bound type variables and type expansion of a type synonym
2354 -- 'TyCon'. Panics if the 'TyCon' is not a synonym
2355 newTyConRhs :: TyCon -> ([TyVar], Type)
2356 newTyConRhs (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon { nt_rhs = rhs }})
2357 = (tvs, rhs)
2358 newTyConRhs tycon = pprPanic "newTyConRhs" (ppr tycon)
2359
2360 -- | The number of type parameters that need to be passed to a newtype to
2361 -- resolve it. May be less than in the definition if it can be eta-contracted.
2362 newTyConEtadArity :: TyCon -> Int
2363 newTyConEtadArity (AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }})
2364 = length (fst tvs_rhs)
2365 newTyConEtadArity tycon = pprPanic "newTyConEtadArity" (ppr tycon)
2366
2367 -- | Extract the bound type variables and type expansion of an eta-contracted
2368 -- type synonym 'TyCon'. Panics if the 'TyCon' is not a synonym
2369 newTyConEtadRhs :: TyCon -> ([TyVar], Type)
2370 newTyConEtadRhs (AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }}) = tvs_rhs
2371 newTyConEtadRhs tycon = pprPanic "newTyConEtadRhs" (ppr tycon)
2372
2373 -- | Extracts the @newtype@ coercion from such a 'TyCon', which can be used to
2374 -- construct something with the @newtype@s type from its representation type
2375 -- (right hand side). If the supplied 'TyCon' is not a @newtype@, returns
2376 -- @Nothing@
2377 newTyConCo_maybe :: TyCon -> Maybe (CoAxiom Unbranched)
2378 newTyConCo_maybe (AlgTyCon {algTcRhs = NewTyCon { nt_co = co }}) = Just co
2379 newTyConCo_maybe _ = Nothing
2380
2381 newTyConCo :: TyCon -> CoAxiom Unbranched
2382 newTyConCo tc = case newTyConCo_maybe tc of
2383 Just co -> co
2384 Nothing -> pprPanic "newTyConCo" (ppr tc)
2385
2386 newTyConDataCon_maybe :: TyCon -> Maybe DataCon
2387 newTyConDataCon_maybe (AlgTyCon {algTcRhs = NewTyCon { data_con = con }}) = Just con
2388 newTyConDataCon_maybe _ = Nothing
2389
2390 -- | Find the \"stupid theta\" of the 'TyCon'. A \"stupid theta\" is the context
2391 -- to the left of an algebraic type declaration, e.g. @Eq a@ in the declaration
2392 -- @data Eq a => T a ...@
2393 tyConStupidTheta :: TyCon -> [PredType]
2394 tyConStupidTheta (AlgTyCon {algTcStupidTheta = stupid}) = stupid
2395 tyConStupidTheta (FunTyCon {}) = []
2396 tyConStupidTheta tycon = pprPanic "tyConStupidTheta" (ppr tycon)
2397
2398 -- | Extract the 'TyVar's bound by a vanilla type synonym
2399 -- and the corresponding (unsubstituted) right hand side.
2400 synTyConDefn_maybe :: TyCon -> Maybe ([TyVar], Type)
2401 synTyConDefn_maybe (SynonymTyCon {tyConTyVars = tyvars, synTcRhs = ty})
2402 = Just (tyvars, ty)
2403 synTyConDefn_maybe _ = Nothing
2404
2405 -- | Extract the information pertaining to the right hand side of a type synonym
2406 -- (@type@) declaration.
2407 synTyConRhs_maybe :: TyCon -> Maybe Type
2408 synTyConRhs_maybe (SynonymTyCon {synTcRhs = rhs}) = Just rhs
2409 synTyConRhs_maybe _ = Nothing
2410
2411 -- | Extract the flavour of a type family (with all the extra information that
2412 -- it carries)
2413 famTyConFlav_maybe :: TyCon -> Maybe FamTyConFlav
2414 famTyConFlav_maybe (FamilyTyCon {famTcFlav = flav}) = Just flav
2415 famTyConFlav_maybe _ = Nothing
2416
2417 -- | Is this 'TyCon' that for a class instance?
2418 isClassTyCon :: TyCon -> Bool
2419 isClassTyCon (AlgTyCon {algTcParent = ClassTyCon {}}) = True
2420 isClassTyCon _ = False
2421
2422 -- | If this 'TyCon' is that for a class instance, return the class it is for.
2423 -- Otherwise returns @Nothing@
2424 tyConClass_maybe :: TyCon -> Maybe Class
2425 tyConClass_maybe (AlgTyCon {algTcParent = ClassTyCon clas _}) = Just clas
2426 tyConClass_maybe _ = Nothing
2427
2428 -- | Return the associated types of the 'TyCon', if any
2429 tyConATs :: TyCon -> [TyCon]
2430 tyConATs (AlgTyCon {algTcParent = ClassTyCon clas _}) = classATs clas
2431 tyConATs _ = []
2432
2433 ----------------------------------------------------------------------------
2434 -- | Is this 'TyCon' that for a data family instance?
2435 isFamInstTyCon :: TyCon -> Bool
2436 isFamInstTyCon (AlgTyCon {algTcParent = DataFamInstTyCon {} })
2437 = True
2438 isFamInstTyCon _ = False
2439
2440 tyConFamInstSig_maybe :: TyCon -> Maybe (TyCon, [Type], CoAxiom Unbranched)
2441 tyConFamInstSig_maybe (AlgTyCon {algTcParent = DataFamInstTyCon ax f ts })
2442 = Just (f, ts, ax)
2443 tyConFamInstSig_maybe _ = Nothing
2444
2445 -- | If this 'TyCon' is that of a data family instance, return the family in question
2446 -- and the instance types. Otherwise, return @Nothing@
2447 tyConFamInst_maybe :: TyCon -> Maybe (TyCon, [Type])
2448 tyConFamInst_maybe (AlgTyCon {algTcParent = DataFamInstTyCon _ f ts })
2449 = Just (f, ts)
2450 tyConFamInst_maybe _ = Nothing
2451
2452 -- | If this 'TyCon' is that of a data family instance, return a 'TyCon' which
2453 -- represents a coercion identifying the representation type with the type
2454 -- instance family. Otherwise, return @Nothing@
2455 tyConFamilyCoercion_maybe :: TyCon -> Maybe (CoAxiom Unbranched)
2456 tyConFamilyCoercion_maybe (AlgTyCon {algTcParent = DataFamInstTyCon ax _ _ })
2457 = Just ax
2458 tyConFamilyCoercion_maybe _ = Nothing
2459
2460 -- | Extract any 'RuntimeRepInfo' from this TyCon
2461 tyConRuntimeRepInfo :: TyCon -> RuntimeRepInfo
2462 tyConRuntimeRepInfo (PromotedDataCon { promDcRepInfo = rri }) = rri
2463 tyConRuntimeRepInfo _ = NoRRI
2464 -- could panic in that second case. But Douglas Adams told me not to.
2465
2466 {-
2467 Note [Constructor tag allocation]
2468 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2469 When typechecking we need to allocate constructor tags to constructors.
2470 They are allocated based on the position in the data_cons field of TyCon,
2471 with the first constructor getting fIRST_TAG.
2472
2473 We used to pay linear cost per constructor, with each constructor looking up
2474 its relative index in the constructor list. That was quadratic and prohibitive
2475 for large data types with more than 10k constructors.
2476
2477 The current strategy is to build a NameEnv with a mapping from costructor's
2478 Name to ConTag and pass it down to buildDataCon for efficient lookup.
2479
2480 Relevant ticket: #14657
2481 -}
2482
2483 mkTyConTagMap :: TyCon -> NameEnv ConTag
2484 mkTyConTagMap tycon =
2485 mkNameEnv $ map getName (tyConDataCons tycon) `zip` [fIRST_TAG..]
2486 -- See Note [Constructor tag allocation]
2487
2488 {-
2489 ************************************************************************
2490 * *
2491 \subsection[TyCon-instances]{Instance declarations for @TyCon@}
2492 * *
2493 ************************************************************************
2494
2495 @TyCon@s are compared by comparing their @Unique@s.
2496 -}
2497
2498 instance Eq TyCon where
2499 a == b = getUnique a == getUnique b
2500 a /= b = getUnique a /= getUnique b
2501
2502 instance Uniquable TyCon where
2503 getUnique tc = tyConUnique tc
2504
2505 instance Outputable TyCon where
2506 -- At the moment a promoted TyCon has the same Name as its
2507 -- corresponding TyCon, so we add the quote to distinguish it here
2508 ppr tc = pprPromotionQuote tc <> ppr (tyConName tc) <> pp_tc
2509 where
2510 pp_tc = getPprStyle $ \sty -> if ((debugStyle sty || dumpStyle sty) && isTcTyCon tc)
2511 then text "[tc]"
2512 else empty
2513
2514 -- | Paints a picture of what a 'TyCon' represents, in broad strokes.
2515 -- This is used towards more informative error messages.
2516 data TyConFlavour
2517 = ClassFlavour
2518 | TupleFlavour Boxity
2519 | SumFlavour
2520 | DataTypeFlavour
2521 | NewtypeFlavour
2522 | AbstractTypeFlavour
2523 | DataFamilyFlavour (Maybe TyCon) -- Just tc <=> (tc == associated class)
2524 | OpenTypeFamilyFlavour (Maybe TyCon) -- Just tc <=> (tc == associated class)
2525 | ClosedTypeFamilyFlavour
2526 | TypeSynonymFlavour
2527 | BuiltInTypeFlavour -- ^ e.g., the @(->)@ 'TyCon'.
2528 | PromotedDataConFlavour
2529 deriving Eq
2530
2531 instance Outputable TyConFlavour where
2532 ppr = text . go
2533 where
2534 go ClassFlavour = "class"
2535 go (TupleFlavour boxed) | isBoxed boxed = "tuple"
2536 | otherwise = "unboxed tuple"
2537 go SumFlavour = "unboxed sum"
2538 go DataTypeFlavour = "data type"
2539 go NewtypeFlavour = "newtype"
2540 go AbstractTypeFlavour = "abstract type"
2541 go (DataFamilyFlavour (Just _)) = "associated data family"
2542 go (DataFamilyFlavour Nothing) = "data family"
2543 go (OpenTypeFamilyFlavour (Just _)) = "associated type family"
2544 go (OpenTypeFamilyFlavour Nothing) = "type family"
2545 go ClosedTypeFamilyFlavour = "type family"
2546 go TypeSynonymFlavour = "type synonym"
2547 go BuiltInTypeFlavour = "built-in type"
2548 go PromotedDataConFlavour = "promoted data constructor"
2549
2550 tyConFlavour :: TyCon -> TyConFlavour
2551 tyConFlavour (AlgTyCon { algTcParent = parent, algTcRhs = rhs })
2552 | ClassTyCon _ _ <- parent = ClassFlavour
2553 | otherwise = case rhs of
2554 TupleTyCon { tup_sort = sort }
2555 -> TupleFlavour (tupleSortBoxity sort)
2556 SumTyCon {} -> SumFlavour
2557 DataTyCon {} -> DataTypeFlavour
2558 NewTyCon {} -> NewtypeFlavour
2559 AbstractTyCon {} -> AbstractTypeFlavour
2560 tyConFlavour (FamilyTyCon { famTcFlav = flav, famTcParent = parent })
2561 = case flav of
2562 DataFamilyTyCon{} -> DataFamilyFlavour parent
2563 OpenSynFamilyTyCon -> OpenTypeFamilyFlavour parent
2564 ClosedSynFamilyTyCon{} -> ClosedTypeFamilyFlavour
2565 AbstractClosedSynFamilyTyCon -> ClosedTypeFamilyFlavour
2566 BuiltInSynFamTyCon{} -> ClosedTypeFamilyFlavour
2567 tyConFlavour (SynonymTyCon {}) = TypeSynonymFlavour
2568 tyConFlavour (FunTyCon {}) = BuiltInTypeFlavour
2569 tyConFlavour (PrimTyCon {}) = BuiltInTypeFlavour
2570 tyConFlavour (PromotedDataCon {}) = PromotedDataConFlavour
2571 tyConFlavour (TcTyCon { tcTyConFlavour = flav }) = flav
2572
2573 -- | Can this flavour of 'TyCon' appear unsaturated?
2574 tcFlavourMustBeSaturated :: TyConFlavour -> Bool
2575 tcFlavourMustBeSaturated ClassFlavour = False
2576 tcFlavourMustBeSaturated DataTypeFlavour = False
2577 tcFlavourMustBeSaturated NewtypeFlavour = False
2578 tcFlavourMustBeSaturated DataFamilyFlavour{} = False
2579 tcFlavourMustBeSaturated TupleFlavour{} = False
2580 tcFlavourMustBeSaturated SumFlavour = False
2581 tcFlavourMustBeSaturated AbstractTypeFlavour = False
2582 tcFlavourMustBeSaturated BuiltInTypeFlavour = False
2583 tcFlavourMustBeSaturated PromotedDataConFlavour = False
2584 tcFlavourMustBeSaturated TypeSynonymFlavour = True
2585 tcFlavourMustBeSaturated OpenTypeFamilyFlavour{} = True
2586 tcFlavourMustBeSaturated ClosedTypeFamilyFlavour = True
2587
2588 -- | Is this flavour of 'TyCon' an open type family or a data family?
2589 tcFlavourIsOpen :: TyConFlavour -> Bool
2590 tcFlavourIsOpen DataFamilyFlavour{} = True
2591 tcFlavourIsOpen OpenTypeFamilyFlavour{} = True
2592 tcFlavourIsOpen ClosedTypeFamilyFlavour = False
2593 tcFlavourIsOpen ClassFlavour = False
2594 tcFlavourIsOpen DataTypeFlavour = False
2595 tcFlavourIsOpen NewtypeFlavour = False
2596 tcFlavourIsOpen TupleFlavour{} = False
2597 tcFlavourIsOpen SumFlavour = False
2598 tcFlavourIsOpen AbstractTypeFlavour = False
2599 tcFlavourIsOpen BuiltInTypeFlavour = False
2600 tcFlavourIsOpen PromotedDataConFlavour = False
2601 tcFlavourIsOpen TypeSynonymFlavour = False
2602
2603 pprPromotionQuote :: TyCon -> SDoc
2604 -- Promoted data constructors already have a tick in their OccName
2605 pprPromotionQuote tc
2606 = case tc of
2607 PromotedDataCon {} -> char '\'' -- Always quote promoted DataCons in types
2608 _ -> empty
2609
2610 instance NamedThing TyCon where
2611 getName = tyConName
2612
2613 instance Data.Data TyCon where
2614 -- don't traverse?
2615 toConstr _ = abstractConstr "TyCon"
2616 gunfold _ _ = error "gunfold"
2617 dataTypeOf _ = mkNoRepType "TyCon"
2618
2619 instance Binary Injectivity where
2620 put_ bh NotInjective = putByte bh 0
2621 put_ bh (Injective xs) = putByte bh 1 >> put_ bh xs
2622
2623 get bh = do { h <- getByte bh
2624 ; case h of
2625 0 -> return NotInjective
2626 _ -> do { xs <- get bh
2627 ; return (Injective xs) } }
2628
2629 {-
2630 ************************************************************************
2631 * *
2632 Walking over recursive TyCons
2633 * *
2634 ************************************************************************
2635
2636 Note [Expanding newtypes and products]
2637 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2638 When expanding a type to expose a data-type constructor, we need to be
2639 careful about newtypes, lest we fall into an infinite loop. Here are
2640 the key examples:
2641
2642 newtype Id x = MkId x
2643 newtype Fix f = MkFix (f (Fix f))
2644 newtype T = MkT (T -> T)
2645
2646 Type Expansion
2647 --------------------------
2648 T T -> T
2649 Fix Maybe Maybe (Fix Maybe)
2650 Id (Id Int) Int
2651 Fix Id NO NO NO
2652
2653 Notice that
2654 * We can expand T, even though it's recursive.
2655 * We can expand Id (Id Int), even though the Id shows up
2656 twice at the outer level, because Id is non-recursive
2657
2658 So, when expanding, we keep track of when we've seen a recursive
2659 newtype at outermost level; and bail out if we see it again.
2660
2661 We sometimes want to do the same for product types, so that the
2662 strictness analyser doesn't unbox infinitely deeply.
2663
2664 More precisely, we keep a *count* of how many times we've seen it.
2665 This is to account for
2666 data instance T (a,b) = MkT (T a) (T b)
2667 Then (#10482) if we have a type like
2668 T (Int,(Int,(Int,(Int,Int))))
2669 we can still unbox deeply enough during strictness analysis.
2670 We have to treat T as potentially recursive, but it's still
2671 good to be able to unwrap multiple layers.
2672
2673 The function that manages all this is checkRecTc.
2674 -}
2675
2676 data RecTcChecker = RC !Int (NameEnv Int)
2677 -- The upper bound, and the number of times
2678 -- we have encountered each TyCon
2679
2680 -- | Initialise a 'RecTcChecker' with 'defaultRecTcMaxBound'.
2681 initRecTc :: RecTcChecker
2682 initRecTc = RC defaultRecTcMaxBound emptyNameEnv
2683
2684 -- | The default upper bound (100) for the number of times a 'RecTcChecker' is
2685 -- allowed to encounter each 'TyCon'.
2686 defaultRecTcMaxBound :: Int
2687 defaultRecTcMaxBound = 100
2688 -- Should we have a flag for this?
2689
2690 -- | Change the upper bound for the number of times a 'RecTcChecker' is allowed
2691 -- to encounter each 'TyCon'.
2692 setRecTcMaxBound :: Int -> RecTcChecker -> RecTcChecker
2693 setRecTcMaxBound new_bound (RC _old_bound rec_nts) = RC new_bound rec_nts
2694
2695 checkRecTc :: RecTcChecker -> TyCon -> Maybe RecTcChecker
2696 -- Nothing => Recursion detected
2697 -- Just rec_tcs => Keep going
2698 checkRecTc (RC bound rec_nts) tc
2699 = case lookupNameEnv rec_nts tc_name of
2700 Just n | n >= bound -> Nothing
2701 | otherwise -> Just (RC bound (extendNameEnv rec_nts tc_name (n+1)))
2702 Nothing -> Just (RC bound (extendNameEnv rec_nts tc_name 1))
2703 where
2704 tc_name = tyConName tc
2705
2706 -- | Returns whether or not this 'TyCon' is definite, or a hole
2707 -- that may be filled in at some later point. See Note [Skolem abstract data]
2708 tyConSkolem :: TyCon -> Bool
2709 tyConSkolem = isHoleName . tyConName
2710
2711 -- Note [Skolem abstract data]
2712 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2713 -- Skolem abstract data arises from data declarations in an hsig file.
2714 --
2715 -- The best analogy is to interpret the types declared in signature files as
2716 -- elaborating to universally quantified type variables; e.g.,
2717 --
2718 -- unit p where
2719 -- signature H where
2720 -- data T
2721 -- data S
2722 -- module M where
2723 -- import H
2724 -- f :: (T ~ S) => a -> b
2725 -- f x = x
2726 --
2727 -- elaborates as (with some fake structural types):
2728 --
2729 -- p :: forall t s. { f :: forall a b. t ~ s => a -> b }
2730 -- p = { f = \x -> x } -- ill-typed
2731 --
2732 -- It is clear that inside p, t ~ s is not provable (and
2733 -- if we tried to write a function to cast t to s, that
2734 -- would not work), but if we call p @Int @Int, clearly Int ~ Int
2735 -- is provable. The skolem variables are all distinct from
2736 -- one another, but we can't make assumptions like "f is
2737 -- inaccessible", because the skolem variables will get
2738 -- instantiated eventually!
2739 --
2740 -- Skolem abstractness can apply to "non-abstract" data as well):
2741 --
2742 -- unit p where
2743 -- signature H1 where
2744 -- data T = MkT
2745 -- signature H2 where
2746 -- data T = MkT
2747 -- module M where
2748 -- import qualified H1
2749 -- import qualified H2
2750 -- f :: (H1.T ~ H2.T) => a -> b
2751 -- f x = x
2752 --
2753 -- This is why the test is on the original name of the TyCon,
2754 -- not whether it is abstract or not.