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