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