Injective type families
[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, DeriveDataTypeable #-}
10
11 module TyCon(
12 -- * Main TyCon data types
13 TyCon, FieldLabel,
14
15 AlgTyConRhs(..), visibleDataCons,
16 TyConParent(..), isNoParent,
17 FamTyConFlav(..), Role(..), Injectivity(..),
18
19 -- ** Constructing TyCons
20 mkAlgTyCon,
21 mkClassTyCon,
22 mkFunTyCon,
23 mkPrimTyCon,
24 mkKindTyCon,
25 mkLiftedPrimTyCon,
26 mkTupleTyCon,
27 mkSynonymTyCon,
28 mkFamilyTyCon,
29 mkPromotedDataCon,
30 mkPromotedTyCon,
31
32 -- ** Predicates on TyCons
33 isAlgTyCon,
34 isClassTyCon, isFamInstTyCon,
35 isFunTyCon,
36 isPrimTyCon,
37 isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
38 isTypeSynonymTyCon,
39 mightBeUnsaturatedTyCon,
40 isPromotedDataCon, isPromotedTyCon,
41 isPromotedDataCon_maybe, isPromotedTyCon_maybe,
42 promotableTyCon_maybe, promoteTyCon,
43
44 isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
45 isEnumerationTyCon,
46 isNewTyCon, isAbstractTyCon,
47 isFamilyTyCon, isOpenFamilyTyCon,
48 isTypeFamilyTyCon, isDataFamilyTyCon,
49 isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
50 familyTyConInjectivityInfo,
51 isBuiltInSynFamTyCon_maybe,
52 isUnLiftedTyCon,
53 isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
54 isTyConAssoc, tyConAssoc_maybe,
55 isRecursiveTyCon,
56 isImplicitTyCon,
57
58 -- ** Extracting information out of TyCons
59 tyConName,
60 tyConKind,
61 tyConUnique,
62 tyConTyVars,
63 tyConCType, tyConCType_maybe,
64 tyConDataCons, tyConDataCons_maybe,
65 tyConSingleDataCon_maybe, tyConSingleDataCon,
66 tyConSingleAlgDataCon_maybe,
67 tyConFamilySize,
68 tyConStupidTheta,
69 tyConArity,
70 tyConRoles,
71 tyConParent,
72 tyConFlavour,
73 tyConTuple_maybe, tyConClass_maybe,
74 tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
75 tyConFamilyResVar_maybe,
76 synTyConDefn_maybe, synTyConRhs_maybe,
77 famTyConFlav_maybe, famTcResVar,
78 algTyConRhs,
79 newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
80 unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
81
82 -- ** Manipulating TyCons
83 expandSynTyCon_maybe,
84 makeTyConAbstract,
85 newTyConCo, newTyConCo_maybe,
86 pprPromotionQuote,
87
88 -- * Primitive representations of Types
89 PrimRep(..), PrimElemRep(..),
90 tyConPrimRep, isVoidRep, isGcPtrRep,
91 primRepSizeW, primElemRepSizeB,
92 primRepIsFloat,
93
94 -- * Recursion breaking
95 RecTcChecker, initRecTc, checkRecTc
96
97 ) where
98
99 #include "HsVersions.h"
100
101 import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
102 import {-# SOURCE #-} DataCon ( DataCon, dataConExTyVars )
103
104 import Binary
105 import Var
106 import Class
107 import BasicTypes
108 import DynFlags
109 import ForeignCall
110 import Name
111 import NameEnv
112 import CoAxiom
113 import PrelNames
114 import Maybes
115 import Outputable
116 import Constants
117 import Util
118 import qualified Data.Data as Data
119 import Data.Typeable (Typeable)
120
121 {-
122 -----------------------------------------------
123 Notes about type families
124 -----------------------------------------------
125
126 Note [Type synonym families]
127 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
128 * Type synonym families, also known as "type functions", map directly
129 onto the type functions in FC:
130
131 type family F a :: *
132 type instance F Int = Bool
133 ..etc...
134
135 * Reply "yes" to isTypeFamilyTyCon, and isFamilyTyCon
136
137 * From the user's point of view (F Int) and Bool are simply
138 equivalent types.
139
140 * A Haskell 98 type synonym is a degenerate form of a type synonym
141 family.
142
143 * Type functions can't appear in the LHS of a type function:
144 type instance F (F Int) = ... -- BAD!
145
146 * Translation of type family decl:
147 type family F a :: *
148 translates to
149 a FamilyTyCon 'F', whose FamTyConFlav is OpenSynFamilyTyCon
150
151 type family G a :: * where
152 G Int = Bool
153 G Bool = Char
154 G a = ()
155 translates to
156 a FamilyTyCon 'G', whose FamTyConFlav is ClosedSynFamilyTyCon, with the
157 appropriate CoAxiom representing the equations
158
159 We also support injective type families -- see Note [Injective type families]
160
161 Note [Data type families]
162 ~~~~~~~~~~~~~~~~~~~~~~~~~
163 See also Note [Wrappers for data instance tycons] in MkId.hs
164
165 * Data type families are declared thus
166 data family T a :: *
167 data instance T Int = T1 | T2 Bool
168
169 Here T is the "family TyCon".
170
171 * Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon
172
173 * The user does not see any "equivalent types" as he did with type
174 synonym families. He just sees constructors with types
175 T1 :: T Int
176 T2 :: Bool -> T Int
177
178 * Here's the FC version of the above declarations:
179
180 data T a
181 data R:TInt = T1 | T2 Bool
182 axiom ax_ti : T Int ~R R:TInt
183
184 Note that this is a *representational* coercion
185 The R:TInt is the "representation TyCons".
186 It has an AlgTyConParent of
187 FamInstTyCon T [Int] ax_ti
188
189 * The axiom ax_ti may be eta-reduced; see
190 Note [Eta reduction for data family axioms] in TcInstDcls
191
192 * The data contructor T2 has a wrapper (which is what the
193 source-level "T2" invokes):
194
195 $WT2 :: Bool -> T Int
196 $WT2 b = T2 b `cast` sym ax_ti
197
198 * A data instance can declare a fully-fledged GADT:
199
200 data instance T (a,b) where
201 X1 :: T (Int,Bool)
202 X2 :: a -> b -> T (a,b)
203
204 Here's the FC version of the above declaration:
205
206 data R:TPair a where
207 X1 :: R:TPair Int Bool
208 X2 :: a -> b -> R:TPair a b
209 axiom ax_pr :: T (a,b) ~R R:TPair a b
210
211 $WX1 :: forall a b. a -> b -> T (a,b)
212 $WX1 a b (x::a) (y::b) = X2 a b x y `cast` sym (ax_pr a b)
213
214 The R:TPair are the "representation TyCons".
215 We have a bit of work to do, to unpick the result types of the
216 data instance declaration for T (a,b), to get the result type in the
217 representation; e.g. T (a,b) --> R:TPair a b
218
219 The representation TyCon R:TList, has an AlgTyConParent of
220
221 FamInstTyCon T [(a,b)] ax_pr
222
223 * Notice that T is NOT translated to a FC type function; it just
224 becomes a "data type" with no constructors, which can be coerced inot
225 into R:TInt, R:TPair by the axioms. These axioms
226 axioms come into play when (and *only* when) you
227 - use a data constructor
228 - do pattern matching
229 Rather like newtype, in fact
230
231 As a result
232
233 - T behaves just like a data type so far as decomposition is concerned
234
235 - (T Int) is not implicitly converted to R:TInt during type inference.
236 Indeed the latter type is unknown to the programmer.
237
238 - There *is* an instance for (T Int) in the type-family instance
239 environment, but it is only used for overlap checking
240
241 - It's fine to have T in the LHS of a type function:
242 type instance F (T a) = [a]
243
244 It was this last point that confused me! The big thing is that you
245 should not think of a data family T as a *type function* at all, not
246 even an injective one! We can't allow even injective type functions
247 on the LHS of a type function:
248 type family injective G a :: *
249 type instance F (G Int) = Bool
250 is no good, even if G is injective, because consider
251 type instance G Int = Bool
252 type instance F Bool = Char
253
254 So a data type family is not an injective type function. It's just a
255 data type with some axioms that connect it to other data types.
256
257 Note [Associated families and their parent class]
258 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
259 *Associated* families are just like *non-associated* families, except
260 that they have a TyConParent of AssocFamilyTyCon, which identifies the
261 parent class.
262
263 However there is an important sharing relationship between
264 * the tyConTyVars of the parent Class
265 * the tyConTyvars of the associated TyCon
266
267 class C a b where
268 data T p a
269 type F a q b
270
271 Here the 'a' and 'b' are shared with the 'Class'; that is, they have
272 the same Unique.
273
274 This is important. In an instance declaration we expect
275 * all the shared variables to be instantiated the same way
276 * the non-shared variables of the associated type should not
277 be instantiated at all
278
279 instance C [x] (Tree y) where
280 data T p [x] = T1 x | T2 p
281 type F [x] q (Tree y) = (x,y,q)
282
283 Note [TyCon Role signatures]
284 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
285
286 Every tycon has a role signature, assigning a role to each of the tyConTyVars
287 (or of equal length to the tyConArity, if there are no tyConTyVars). An
288 example demonstrates these best: say we have a tycon T, with parameters a at
289 nominal, b at representational, and c at phantom. Then, to prove
290 representational equality between T a1 b1 c1 and T a2 b2 c2, we need to have
291 nominal equality between a1 and a2, representational equality between b1 and
292 b2, and nothing in particular (i.e., phantom equality) between c1 and c2. This
293 might happen, say, with the following declaration:
294
295 data T a b c where
296 MkT :: b -> T Int b c
297
298 Data and class tycons have their roles inferred (see inferRoles in TcTyDecls),
299 as do vanilla synonym tycons. Family tycons have all parameters at role N,
300 though it is conceivable that we could relax this restriction. (->)'s and
301 tuples' parameters are at role R. Each primitive tycon declares its roles;
302 it's worth noting that (~#)'s parameters are at role N. Promoted data
303 constructors' type arguments are at role R. All kind arguments are at role
304 N.
305
306 Note [Injective type families]
307 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
308
309 We allow injectivity annotations for type families (both open and closed):
310
311 type family F (a :: k) (b :: k) = r | r -> a
312 type family G a b = res | res -> a b where ...
313
314 Injectivity information is stored in the `famTcInj` field of `FamilyTyCon`.
315 `famTcInj` maybe stores a list of Bools, where each entry corresponds to a
316 single element of `tyConTyVars` (both lists should have identical length). If no
317 injectivity annotation was provided `famTcInj` is Nothing. From this follows an
318 invariant that if `famTcInj` is a Just then at least one element in the list
319 must be True.
320
321 See also:
322 * [Injectivity annotation] in HsDecls
323 * [Renaming injectivity annotation] in RnSource
324 * [Verifying injectivity annotation] in FamInstEnv
325 * [Type inference for type families with injectivity] in TcInteract
326
327
328 ************************************************************************
329 * *
330 \subsection{The data type}
331 * *
332 ************************************************************************
333 -}
334
335 -- | TyCons represent type constructors. Type constructors are introduced by
336 -- things such as:
337 --
338 -- 1) Data declarations: @data Foo = ...@ creates the @Foo@ type constructor of
339 -- kind @*@
340 --
341 -- 2) Type synonyms: @type Foo = ...@ creates the @Foo@ type constructor
342 --
343 -- 3) Newtypes: @newtype Foo a = MkFoo ...@ creates the @Foo@ type constructor
344 -- of kind @* -> *@
345 --
346 -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor
347 -- of kind @*@
348 --
349 -- This data type also encodes a number of primitive, built in type constructors
350 -- such as those for function and tuple types.
351
352 -- If you edit this type, you may need to update the GHC formalism
353 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
354 data TyCon
355 = -- | The function type constructor, @(->)@
356 FunTyCon {
357 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
358 -- identical to Unique of Name stored in
359 -- tyConName field.
360
361 tyConName :: Name, -- ^ Name of the constructor
362
363 tyConKind :: Kind, -- ^ Kind of this TyCon (full kind, not just
364 -- the return kind)
365
366 tyConArity :: Arity -- ^ Number of arguments this TyCon must
367 -- receive to be considered saturated
368 -- (including implicit kind variables)
369 }
370
371 -- | Algebraic type constructors, which are defined to be those
372 -- arising @data@ type and @newtype@ declarations. All these
373 -- constructors are lifted and boxed. See 'AlgTyConRhs' for more
374 -- information.
375 | AlgTyCon {
376 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
377 -- identical to Unique of Name stored in
378 -- tyConName field.
379
380 tyConName :: Name, -- ^ Name of the constructor
381
382 tyConKind :: Kind, -- ^ Kind of this TyCon (full kind, not just
383 -- the return kind)
384
385 tyConArity :: Arity, -- ^ Number of arguments this TyCon must
386 -- receive to be considered saturated
387 -- (including implicit kind variables)
388
389 tyConTyVars :: [TyVar], -- ^ The kind and type variables used in the
390 -- type constructor.
391 -- Invariant: length tyvars = arity
392 -- Precisely, this list scopes over:
393 --
394 -- 1. The 'algTcStupidTheta'
395 -- 2. The cached types in algTyConRhs.NewTyCon
396 -- 3. The family instance types if present
397 --
398 -- Note that it does /not/ scope over the data
399 -- constructors.
400
401 tcRoles :: [Role], -- ^ The role for each type variable
402 -- This list has the same length as tyConTyVars
403 -- See also Note [TyCon Role signatures]
404
405 tyConCType :: Maybe CType,-- ^ The C type that should be used
406 -- for this type when using the FFI
407 -- and CAPI
408
409 algTcGadtSyntax :: Bool, -- ^ Was the data type declared with GADT
410 -- syntax? If so, that doesn't mean it's a
411 -- true GADT; only that the "where" form
412 -- was used. This field is used only to
413 -- guide pretty-printing
414
415 algTcStupidTheta :: [PredType], -- ^ The \"stupid theta\" for the data
416 -- type (always empty for GADTs). A
417 -- \"stupid theta\" is the context to
418 -- the left of an algebraic type
419 -- declaration, e.g. @Eq a@ in the
420 -- declaration @data Eq a => T a ...@.
421
422 algTcRhs :: AlgTyConRhs, -- ^ Contains information about the
423 -- data constructors of the algebraic type
424
425 algTcRec :: RecFlag, -- ^ Tells us whether the data type is part
426 -- of a mutually-recursive group or not
427
428 algTcParent :: TyConParent, -- ^ Gives the class or family declaration
429 -- 'TyCon' for derived 'TyCon's representing
430 -- class or family instances, respectively.
431 -- See also 'synTcParent'
432
433 tcPromoted :: Maybe TyCon -- ^ Promoted TyCon, if any
434 }
435
436 -- | Represents type synonyms
437 | SynonymTyCon {
438 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
439 -- identical to Unique of Name stored in
440 -- tyConName field.
441
442 tyConName :: Name, -- ^ Name of the constructor
443
444 tyConKind :: Kind, -- ^ Kind of this TyCon (full kind, not just
445 -- the return kind)
446
447 tyConArity :: Arity, -- ^ Number of arguments this TyCon must
448 -- receive to be considered saturated
449 -- (including implicit kind variables)
450
451 tyConTyVars :: [TyVar], -- ^ List of type and kind variables in this
452 -- TyCon. Includes implicit kind variables.
453 -- Invariant: length tyConTyVars = tyConArity
454
455 tcRoles :: [Role], -- ^ The role for each type variable
456 -- This list has the same length as tyConTyVars
457 -- See also Note [TyCon Role signatures]
458
459 synTcRhs :: Type -- ^ Contains information about the expansion
460 -- of the synonym
461 }
462
463 -- | Represents type families
464 | FamilyTyCon {
465 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
466 -- identical to Unique of Name stored in
467 -- tyConName field.
468
469 tyConName :: Name, -- ^ Name of the constructor
470
471 tyConKind :: Kind, -- ^ Kind of this TyCon (full kind, not just
472 -- the return kind)
473
474 tyConArity :: Arity, -- ^ Number of arguments this TyCon must
475 -- receive to be considered saturated
476 -- (including implicit kind variables)
477
478 tyConTyVars :: [TyVar], -- ^ The kind and type variables used in the
479 -- type constructor.
480 -- Invariant: length tyvars = arity
481 -- Precisely, this list scopes over:
482 --
483 -- 1. The 'algTcStupidTheta'
484 -- 2. The cached types in algTyConRhs.NewTyCon
485 -- 3. The family instance types if present
486 --
487 -- Note that it does /not/ scope over the data
488 -- constructors.
489
490 famTcResVar :: Maybe Name, -- ^ Name of result type variable, used
491 -- for pretty-printing with --show-iface
492 -- and for reifying TyCon in Template
493 -- Haskell
494
495 famTcFlav :: FamTyConFlav, -- ^ Type family flavour: open, closed,
496 -- abstract, built-in. See comments for
497 -- FamTyConFlav
498
499 famTcParent :: TyConParent, -- ^ TyCon of enclosing class for
500 -- associated type families
501
502 famTcInj :: Injectivity -- ^ is this a type family injective in
503 -- its type variables? Nothing if no
504 -- injectivity annotation was given
505 }
506
507 -- | Primitive types; cannot be defined in Haskell. This includes
508 -- the usual suspects (such as @Int#@) as well as foreign-imported
509 -- types and kinds
510 | PrimTyCon {
511 tyConUnique :: Unique, -- ^ A Unique of this TyCon. Invariant:
512 -- identical to Unique of Name stored in
513 -- tyConName field.
514
515 tyConName :: Name, -- ^ Name of the constructor
516
517 tyConKind :: Kind, -- ^ Kind of this TyCon (full kind, not just
518 -- the return kind)
519
520 tyConArity :: Arity, -- ^ Number of arguments this TyCon must
521 -- receive to be considered saturated
522 -- (including implicit kind variables)
523
524 tcRoles :: [Role], -- ^ The role for each type variable
525 -- This list has the same length as tyConTyVars
526 -- See also Note [TyCon Role signatures]
527
528 primTyConRep :: PrimRep,-- ^ Many primitive tycons are unboxed, but
529 -- some are boxed (represented by
530 -- pointers). This 'PrimRep' holds that
531 -- information. Only relevant if tyConKind = *
532
533 isUnLifted :: Bool -- ^ Most primitive tycons are unlifted (may
534 -- not contain bottom) but other are lifted,
535 -- e.g. @RealWorld@
536 }
537
538 -- | Represents promoted data constructor.
539 | PromotedDataCon { -- See Note [Promoted data constructors]
540 tyConUnique :: Unique, -- ^ Same Unique as the data constructor
541 tyConName :: Name, -- ^ Same Name as the data constructor
542 tyConArity :: Arity,
543 tyConKind :: Kind, -- ^ Translated type of the data constructor
544 tcRoles :: [Role], -- ^ Roles: N for kind vars, R for type vars
545 dataCon :: DataCon -- ^ Corresponding data constructor
546 }
547
548 -- | Represents promoted type constructor.
549 | PromotedTyCon {
550 tyConUnique :: Unique, -- ^ Same Unique as the type constructor
551 tyConName :: Name, -- ^ Same Name as the type constructor
552 tyConArity :: Arity, -- ^ n if ty_con :: * -> ... -> * n times
553 tyConKind :: Kind, -- ^ Always TysPrim.superKind
554 ty_con :: TyCon -- ^ Corresponding type constructor
555 }
556
557 deriving Typeable
558
559 -- | Names of the fields in an algebraic record type
560 type FieldLabel = Name
561
562 -- | Represents right-hand-sides of 'TyCon's for algebraic types
563 data AlgTyConRhs
564
565 -- | Says that we know nothing about this data type, except that
566 -- it's represented by a pointer. Used when we export a data type
567 -- abstractly into an .hi file.
568 = AbstractTyCon
569 Bool -- True <=> It's definitely a distinct data type,
570 -- equal only to itself; ie not a newtype
571 -- False <=> Not sure
572 -- See Note [AbstractTyCon and type equality]
573
574 -- | Represents an open type family without a fixed right hand
575 -- side. Additional instances can appear at any time.
576 --
577 -- These are introduced by either a top level declaration:
578 --
579 -- > data T a :: *
580 --
581 -- Or an associated data type declaration, within a class declaration:
582 --
583 -- > class C a b where
584 -- > data T b :: *
585 | DataFamilyTyCon
586
587 -- | Information about those 'TyCon's derived from a @data@
588 -- declaration. This includes data types with no constructors at
589 -- all.
590 | DataTyCon {
591 data_cons :: [DataCon],
592 -- ^ The data type constructors; can be empty if the
593 -- user declares the type to have no constructors
594 --
595 -- INVARIANT: Kept in order of increasing 'DataCon'
596 -- tag (see the tag assignment in DataCon.mkDataCon)
597
598 is_enum :: Bool -- ^ Cached value: is this an enumeration type?
599 -- See Note [Enumeration types]
600 }
601
602 | TupleTyCon { -- A boxed, unboxed, or constraint tuple
603 data_con :: DataCon, -- NB: it can be an *unboxed* tuple
604 tup_sort :: TupleSort -- ^ Is this a boxed, unboxed or constraint
605 -- tuple?
606 }
607
608 -- | Information about those 'TyCon's derived from a @newtype@ declaration
609 | NewTyCon {
610 data_con :: DataCon, -- ^ The unique constructor for the @newtype@.
611 -- It has no existentials
612
613 nt_rhs :: Type, -- ^ Cached value: the argument type of the
614 -- constructor, which is just the representation
615 -- type of the 'TyCon' (remember that @newtype@s
616 -- do not exist at runtime so need a different
617 -- representation type).
618 --
619 -- The free 'TyVar's of this type are the
620 -- 'tyConTyVars' from the corresponding 'TyCon'
621
622 nt_etad_rhs :: ([TyVar], Type),
623 -- ^ Same as the 'nt_rhs', but this time eta-reduced.
624 -- Hence the list of 'TyVar's in this field may be
625 -- shorter than the declared arity of the 'TyCon'.
626
627 -- See Note [Newtype eta]
628 nt_co :: CoAxiom Unbranched
629 -- The axiom coercion that creates the @newtype@
630 -- from the representation 'Type'.
631
632 -- See Note [Newtype coercions]
633 -- Invariant: arity = #tvs in nt_etad_rhs;
634 -- See Note [Newtype eta]
635 -- Watch out! If any newtypes become transparent
636 -- again check Trac #1072.
637 }
638
639 {-
640 Note [AbstractTyCon and type equality]
641 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
642 TODO
643 -}
644
645 -- | Extract those 'DataCon's that we are able to learn about. Note
646 -- that visibility in this sense does not correspond to visibility in
647 -- the context of any particular user program!
648 visibleDataCons :: AlgTyConRhs -> [DataCon]
649 visibleDataCons (AbstractTyCon {}) = []
650 visibleDataCons DataFamilyTyCon {} = []
651 visibleDataCons (DataTyCon{ data_cons = cs }) = cs
652 visibleDataCons (NewTyCon{ data_con = c }) = [c]
653 visibleDataCons (TupleTyCon{ data_con = c }) = [c]
654
655 -- ^ Both type classes as well as family instances imply implicit
656 -- type constructors. These implicit type constructors refer to their parent
657 -- structure (ie, the class or family from which they derive) using a type of
658 -- the following form. We use 'TyConParent' for both algebraic and synonym
659 -- types, but the variant 'ClassTyCon' will only be used by algebraic 'TyCon's.
660 data TyConParent
661 = -- | An ordinary type constructor has no parent.
662 NoParentTyCon
663
664 -- | Type constructors representing a class dictionary.
665 -- See Note [ATyCon for classes] in TypeRep
666 | ClassTyCon
667 Class -- INVARIANT: the classTyCon of this Class is the
668 -- current tycon
669
670 -- | An *associated* type of a class.
671 | AssocFamilyTyCon
672 Class -- The class in whose declaration the family is declared
673 -- See Note [Associated families and their parent class]
674
675 -- | Type constructors representing an instance of a *data* family.
676 -- Parameters:
677 --
678 -- 1) The type family in question
679 --
680 -- 2) Instance types; free variables are the 'tyConTyVars'
681 -- of the current 'TyCon' (not the family one). INVARIANT:
682 -- the number of types matches the arity of the family 'TyCon'
683 --
684 -- 3) A 'CoTyCon' identifying the representation
685 -- type with the type instance family
686 | FamInstTyCon -- See Note [Data type families]
687 (CoAxiom Unbranched) -- The coercion axiom.
688 -- A *Representational* coercion,
689 -- of kind T ty1 ty2 ~R R:T a b c
690 -- where T is the family TyCon,
691 -- and R:T is the representation TyCon (ie this one)
692 -- and a,b,c are the tyConTyVars of this TyCon
693 --
694 -- BUT may be eta-reduced; see TcInstDcls
695 -- Note [Eta reduction for data family axioms]
696
697 -- Cached fields of the CoAxiom, but adjusted to
698 -- use the tyConTyVars of this TyCon
699 TyCon -- The family TyCon
700 [Type] -- Argument types (mentions the tyConTyVars of this TyCon)
701 -- Match in length the tyConTyVars of the family TyCon
702
703 -- E.g. data intance T [a] = ...
704 -- gives a representation tycon:
705 -- data R:TList a = ...
706 -- axiom co a :: T [a] ~ R:TList a
707 -- with R:TList's algTcParent = FamInstTyCon T [a] co
708
709 instance Outputable TyConParent where
710 ppr NoParentTyCon = text "No parent"
711 ppr (ClassTyCon cls) = text "Class parent" <+> ppr cls
712 ppr (AssocFamilyTyCon cls) =
713 text "Class parent (assoc. family)" <+> ppr cls
714 ppr (FamInstTyCon _ tc tys) =
715 text "Family parent (family instance)" <+> ppr tc <+> sep (map ppr tys)
716
717 -- | Checks the invariants of a 'TyConParent' given the appropriate type class
718 -- name, if any
719 okParent :: Name -> TyConParent -> Bool
720 okParent _ NoParentTyCon = True
721 okParent tc_name (AssocFamilyTyCon cls) = tc_name `elem` map tyConName (classATs cls)
722 okParent tc_name (ClassTyCon cls) = tc_name == tyConName (classTyCon cls)
723 okParent _ (FamInstTyCon _ fam_tc tys) = tyConArity fam_tc == length tys
724
725 isNoParent :: TyConParent -> Bool
726 isNoParent NoParentTyCon = True
727 isNoParent _ = False
728
729 --------------------
730
731 data Injectivity
732 = NotInjective
733 | Injective [Bool] -- Length is 1-1 with tyConTyVars (incl kind vars)
734 deriving( Eq )
735
736 -- | Information pertaining to the expansion of a type synonym (@type@)
737 data FamTyConFlav
738 = -- | An open type synonym family e.g. @type family F x y :: * -> *@
739 OpenSynFamilyTyCon
740
741 -- | A closed type synonym family e.g.
742 -- @type family F x where { F Int = Bool }@
743 | ClosedSynFamilyTyCon (Maybe (CoAxiom Branched))
744 -- See Note [Closed type families]
745
746 -- | A closed type synonym family declared in an hs-boot file with
747 -- type family F a where ..
748 | AbstractClosedSynFamilyTyCon
749
750 -- | Built-in type family used by the TypeNats solver
751 | BuiltInSynFamTyCon BuiltInSynFamily
752
753 {-
754 Note [Closed type families]
755 ~~~~~~~~~~~~~~~~~~~~~~~~~
756 * In an open type family you can add new instances later. This is the
757 usual case.
758
759 * In a closed type family you can only put equations where the family
760 is defined.
761
762 A non-empty closed type family has a single axiom with multiple
763 branches, stored in the 'ClosedSynFamilyTyCon' constructor. A closed
764 type family with no equations does not have an axiom, because there is
765 nothing for the axiom to prove!
766
767
768 Note [Promoted data constructors]
769 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
770 A data constructor can be promoted to become a type constructor,
771 via the PromotedTyCon alternative in TyCon.
772
773 * Only data constructors with
774 (a) no kind polymorphism
775 (b) no constraints in its type (eg GADTs)
776 are promoted. Existentials are ok; see Trac #7347.
777
778 * The TyCon promoted from a DataCon has the *same* Name and Unique as
779 the DataCon. Eg. If the data constructor Data.Maybe.Just(unique 78,
780 say) is promoted to a TyCon whose name is Data.Maybe.Just(unique 78)
781
782 * The *kind* of a promoted DataCon may be polymorphic. Example:
783 type of DataCon Just :: forall (a:*). a -> Maybe a
784 kind of (promoted) tycon Just :: forall (a:box). a -> Maybe a
785 The kind is not identical to the type, because of the */box
786 kind signature on the forall'd variable; so the tyConKind field of
787 PromotedTyCon is not identical to the dataConUserType of the
788 DataCon. But it's the same modulo changing the variable kinds,
789 done by DataCon.promoteType.
790
791 * Small note: We promote the *user* type of the DataCon. Eg
792 data T = MkT {-# UNPACK #-} !(Bool, Bool)
793 The promoted kind is
794 MkT :: (Bool,Bool) -> T
795 *not*
796 MkT :: Bool -> Bool -> T
797
798 Note [Enumeration types]
799 ~~~~~~~~~~~~~~~~~~~~~~~~
800 We define datatypes with no constructors to *not* be
801 enumerations; this fixes trac #2578, Otherwise we
802 end up generating an empty table for
803 <mod>_<type>_closure_tbl
804 which is used by tagToEnum# to map Int# to constructors
805 in an enumeration. The empty table apparently upset
806 the linker.
807
808 Moreover, all the data constructor must be enumerations, meaning
809 they have type (forall abc. T a b c). GADTs are not enumerations.
810 For example consider
811 data T a where
812 T1 :: T Int
813 T2 :: T Bool
814 T3 :: T a
815 What would [T1 ..] be? [T1,T3] :: T Int? Easiest thing is to exclude them.
816 See Trac #4528.
817
818 Note [Newtype coercions]
819 ~~~~~~~~~~~~~~~~~~~~~~~~
820 The NewTyCon field nt_co is a CoAxiom which is used for coercing from
821 the representation type of the newtype, to the newtype itself. For
822 example,
823
824 newtype T a = MkT (a -> a)
825
826 the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> t.
827
828 In the case that the right hand side is a type application
829 ending with the same type variables as the left hand side, we
830 "eta-contract" the coercion. So if we had
831
832 newtype S a = MkT [a]
833
834 then we would generate the arity 0 axiom CoS : S ~ []. The
835 primary reason we do this is to make newtype deriving cleaner.
836
837 In the paper we'd write
838 axiom CoT : (forall t. T t) ~ (forall t. [t])
839 and then when we used CoT at a particular type, s, we'd say
840 CoT @ s
841 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
842
843 Note [Newtype eta]
844 ~~~~~~~~~~~~~~~~~~
845 Consider
846 newtype Parser a = MkParser (IO a) deriving Monad
847 Are these two types equal (to Core)?
848 Monad Parser
849 Monad IO
850 which we need to make the derived instance for Monad Parser.
851
852 Well, yes. But to see that easily we eta-reduce the RHS type of
853 Parser, in this case to ([], Froogle), so that even unsaturated applications
854 of Parser will work right. This eta reduction is done when the type
855 constructor is built, and cached in NewTyCon.
856
857 Here's an example that I think showed up in practice
858 Source code:
859 newtype T a = MkT [a]
860 newtype Foo m = MkFoo (forall a. m a -> Int)
861
862 w1 :: Foo []
863 w1 = ...
864
865 w2 :: Foo T
866 w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
867
868 After desugaring, and discarding the data constructors for the newtypes,
869 we get:
870 w2 = w1 `cast` Foo CoT
871 so the coercion tycon CoT must have
872 kind: T ~ []
873 and arity: 0
874
875 ************************************************************************
876 * *
877 \subsection{PrimRep}
878 * *
879 ************************************************************************
880
881 Note [rep swamp]
882
883 GHC has a rich selection of types that represent "primitive types" of
884 one kind or another. Each of them makes a different set of
885 distinctions, and mostly the differences are for good reasons,
886 although it's probably true that we could merge some of these.
887
888 Roughly in order of "includes more information":
889
890 - A Width (cmm/CmmType) is simply a binary value with the specified
891 number of bits. It may represent a signed or unsigned integer, a
892 floating-point value, or an address.
893
894 data Width = W8 | W16 | W32 | W64 | W80 | W128
895
896 - Size, which is used in the native code generator, is Width +
897 floating point information.
898
899 data Size = II8 | II16 | II32 | II64 | FF32 | FF64 | FF80
900
901 it is necessary because e.g. the instruction to move a 64-bit float
902 on x86 (movsd) is different from the instruction to move a 64-bit
903 integer (movq), so the mov instruction is parameterised by Size.
904
905 - CmmType wraps Width with more information: GC ptr, float, or
906 other value.
907
908 data CmmType = CmmType CmmCat Width
909
910 data CmmCat -- "Category" (not exported)
911 = GcPtrCat -- GC pointer
912 | BitsCat -- Non-pointer
913 | FloatCat -- Float
914
915 It is important to have GcPtr information in Cmm, since we generate
916 info tables containing pointerhood for the GC from this. As for
917 why we have float (and not signed/unsigned) here, see Note [Signed
918 vs unsigned].
919
920 - ArgRep makes only the distinctions necessary for the call and
921 return conventions of the STG machine. It is essentially CmmType
922 + void.
923
924 - PrimRep makes a few more distinctions than ArgRep: it divides
925 non-GC-pointers into signed/unsigned and addresses, information
926 that is necessary for passing these values to foreign functions.
927
928 There's another tension here: whether the type encodes its size in
929 bytes, or whether its size depends on the machine word size. Width
930 and CmmType have the size built-in, whereas ArgRep and PrimRep do not.
931
932 This means to turn an ArgRep/PrimRep into a CmmType requires DynFlags.
933
934 On the other hand, CmmType includes some "nonsense" values, such as
935 CmmType GcPtrCat W32 on a 64-bit machine.
936 -}
937
938 -- | A 'PrimRep' is an abstraction of a type. It contains information that
939 -- the code generator needs in order to pass arguments, return results,
940 -- and store values of this type.
941 data PrimRep
942 = VoidRep
943 | PtrRep
944 | IntRep -- ^ Signed, word-sized value
945 | WordRep -- ^ Unsigned, word-sized value
946 | Int64Rep -- ^ Signed, 64 bit value (with 32-bit words only)
947 | Word64Rep -- ^ Unsigned, 64 bit value (with 32-bit words only)
948 | AddrRep -- ^ A pointer, but /not/ to a Haskell value (use 'PtrRep')
949 | FloatRep
950 | DoubleRep
951 | VecRep Int PrimElemRep -- ^ A vector
952 deriving( Eq, Show )
953
954 data PrimElemRep
955 = Int8ElemRep
956 | Int16ElemRep
957 | Int32ElemRep
958 | Int64ElemRep
959 | Word8ElemRep
960 | Word16ElemRep
961 | Word32ElemRep
962 | Word64ElemRep
963 | FloatElemRep
964 | DoubleElemRep
965 deriving( Eq, Show )
966
967 instance Outputable PrimRep where
968 ppr r = text (show r)
969
970 instance Outputable PrimElemRep where
971 ppr r = text (show r)
972
973 isVoidRep :: PrimRep -> Bool
974 isVoidRep VoidRep = True
975 isVoidRep _other = False
976
977 isGcPtrRep :: PrimRep -> Bool
978 isGcPtrRep PtrRep = True
979 isGcPtrRep _ = False
980
981 -- | Find the size of a 'PrimRep', in words
982 primRepSizeW :: DynFlags -> PrimRep -> Int
983 primRepSizeW _ IntRep = 1
984 primRepSizeW _ WordRep = 1
985 primRepSizeW dflags Int64Rep = wORD64_SIZE `quot` wORD_SIZE dflags
986 primRepSizeW dflags Word64Rep = wORD64_SIZE `quot` wORD_SIZE dflags
987 primRepSizeW _ FloatRep = 1 -- NB. might not take a full word
988 primRepSizeW dflags DoubleRep = dOUBLE_SIZE dflags `quot` wORD_SIZE dflags
989 primRepSizeW _ AddrRep = 1
990 primRepSizeW _ PtrRep = 1
991 primRepSizeW _ VoidRep = 0
992 primRepSizeW dflags (VecRep len rep) = len * primElemRepSizeB rep `quot` wORD_SIZE dflags
993
994 primElemRepSizeB :: PrimElemRep -> Int
995 primElemRepSizeB Int8ElemRep = 1
996 primElemRepSizeB Int16ElemRep = 2
997 primElemRepSizeB Int32ElemRep = 4
998 primElemRepSizeB Int64ElemRep = 8
999 primElemRepSizeB Word8ElemRep = 1
1000 primElemRepSizeB Word16ElemRep = 2
1001 primElemRepSizeB Word32ElemRep = 4
1002 primElemRepSizeB Word64ElemRep = 8
1003 primElemRepSizeB FloatElemRep = 4
1004 primElemRepSizeB DoubleElemRep = 8
1005
1006 -- | Return if Rep stands for floating type,
1007 -- returns Nothing for vector types.
1008 primRepIsFloat :: PrimRep -> Maybe Bool
1009 primRepIsFloat FloatRep = Just True
1010 primRepIsFloat DoubleRep = Just True
1011 primRepIsFloat (VecRep _ _) = Nothing
1012 primRepIsFloat _ = Just False
1013
1014 {-
1015 ************************************************************************
1016 * *
1017 \subsection{TyCon Construction}
1018 * *
1019 ************************************************************************
1020
1021 Note: the TyCon constructors all take a Kind as one argument, even though
1022 they could, in principle, work out their Kind from their other arguments.
1023 But to do so they need functions from Types, and that makes a nasty
1024 module mutual-recursion. And they aren't called from many places.
1025 So we compromise, and move their Kind calculation to the call site.
1026 -}
1027
1028 -- | Given the name of the function type constructor and it's kind, create the
1029 -- corresponding 'TyCon'. It is reccomended to use 'TypeRep.funTyCon' if you want
1030 -- this functionality
1031 mkFunTyCon :: Name -> Kind -> TyCon
1032 mkFunTyCon name kind
1033 = FunTyCon {
1034 tyConUnique = nameUnique name,
1035 tyConName = name,
1036 tyConKind = kind,
1037 tyConArity = 2
1038 }
1039
1040 -- | This is the making of an algebraic 'TyCon'. Notably, you have to
1041 -- pass in the generic (in the -XGenerics sense) information about the
1042 -- type constructor - you can get hold of it easily (see Generics
1043 -- module)
1044 mkAlgTyCon :: Name
1045 -> Kind -- ^ Kind of the resulting 'TyCon'
1046 -> [TyVar] -- ^ 'TyVar's scoped over: see 'tyConTyVars'.
1047 -- Arity is inferred from the length of this
1048 -- list
1049 -> [Role] -- ^ The roles for each TyVar
1050 -> Maybe CType -- ^ The C type this type corresponds to
1051 -- when using the CAPI FFI
1052 -> [PredType] -- ^ Stupid theta: see 'algTcStupidTheta'
1053 -> AlgTyConRhs -- ^ Information about dat aconstructors
1054 -> TyConParent
1055 -> RecFlag -- ^ Is the 'TyCon' recursive?
1056 -> Bool -- ^ Was the 'TyCon' declared with GADT syntax?
1057 -> Maybe TyCon -- ^ Promoted version
1058 -> TyCon
1059 mkAlgTyCon name kind tyvars roles cType stupid rhs parent is_rec gadt_syn prom_tc
1060 = AlgTyCon {
1061 tyConName = name,
1062 tyConUnique = nameUnique name,
1063 tyConKind = kind,
1064 tyConArity = length tyvars,
1065 tyConTyVars = tyvars,
1066 tcRoles = roles,
1067 tyConCType = cType,
1068 algTcStupidTheta = stupid,
1069 algTcRhs = rhs,
1070 algTcParent = ASSERT2( okParent name parent, ppr name $$ ppr parent ) parent,
1071 algTcRec = is_rec,
1072 algTcGadtSyntax = gadt_syn,
1073 tcPromoted = prom_tc
1074 }
1075
1076 -- | Simpler specialization of 'mkAlgTyCon' for classes
1077 mkClassTyCon :: Name -> Kind -> [TyVar] -> [Role] -> AlgTyConRhs -> Class
1078 -> RecFlag -> TyCon
1079 mkClassTyCon name kind tyvars roles rhs clas is_rec
1080 = mkAlgTyCon name kind tyvars roles Nothing [] rhs (ClassTyCon clas)
1081 is_rec False
1082 Nothing -- Class TyCons are not promoted
1083
1084 mkTupleTyCon :: Name
1085 -> Kind -- ^ Kind of the resulting 'TyCon'
1086 -> Arity -- ^ Arity of the tuple
1087 -> [TyVar] -- ^ 'TyVar's scoped over: see 'tyConTyVars'
1088 -> DataCon
1089 -> TupleSort -- ^ Whether the tuple is boxed or unboxed
1090 -> Maybe TyCon -- ^ Promoted version
1091 -> TyConParent
1092 -> TyCon
1093 mkTupleTyCon name kind arity tyvars con sort prom_tc parent
1094 = AlgTyCon {
1095 tyConName = name,
1096 tyConUnique = nameUnique name,
1097 tyConKind = kind,
1098 tyConArity = arity,
1099 tyConTyVars = tyvars,
1100 tcRoles = replicate arity Representational,
1101 tyConCType = Nothing,
1102 algTcStupidTheta = [],
1103 algTcRhs = TupleTyCon { data_con = con, tup_sort = sort },
1104 algTcParent = parent,
1105 algTcRec = NonRecursive,
1106 algTcGadtSyntax = False,
1107 tcPromoted = prom_tc
1108 }
1109
1110 -- | Create an unlifted primitive 'TyCon', such as @Int#@
1111 mkPrimTyCon :: Name -> Kind -> [Role] -> PrimRep -> TyCon
1112 mkPrimTyCon name kind roles rep
1113 = mkPrimTyCon' name kind roles rep True
1114
1115 -- | Kind constructors
1116 mkKindTyCon :: Name -> Kind -> TyCon
1117 mkKindTyCon name kind
1118 = mkPrimTyCon' name kind [] VoidRep True
1119
1120 -- | Create a lifted primitive 'TyCon' such as @RealWorld@
1121 mkLiftedPrimTyCon :: Name -> Kind -> [Role] -> PrimRep -> TyCon
1122 mkLiftedPrimTyCon name kind roles rep
1123 = mkPrimTyCon' name kind roles rep False
1124
1125 mkPrimTyCon' :: Name -> Kind -> [Role] -> PrimRep -> Bool -> TyCon
1126 mkPrimTyCon' name kind roles rep is_unlifted
1127 = PrimTyCon {
1128 tyConName = name,
1129 tyConUnique = nameUnique name,
1130 tyConKind = kind,
1131 tyConArity = length roles,
1132 tcRoles = roles,
1133 primTyConRep = rep,
1134 isUnLifted = is_unlifted
1135 }
1136
1137 -- | Create a type synonym 'TyCon'
1138 mkSynonymTyCon :: Name -> Kind -> [TyVar] -> [Role] -> Type -> TyCon
1139 mkSynonymTyCon name kind tyvars roles rhs
1140 = SynonymTyCon {
1141 tyConName = name,
1142 tyConUnique = nameUnique name,
1143 tyConKind = kind,
1144 tyConArity = length tyvars,
1145 tyConTyVars = tyvars,
1146 tcRoles = roles,
1147 synTcRhs = rhs
1148 }
1149
1150 -- | Create a type family 'TyCon'
1151 mkFamilyTyCon:: Name -> Kind -> [TyVar] -> Maybe Name -> FamTyConFlav
1152 -> TyConParent -> Injectivity -> TyCon
1153 mkFamilyTyCon name kind tyvars resVar flav parent inj
1154 = FamilyTyCon
1155 { tyConUnique = nameUnique name
1156 , tyConName = name
1157 , tyConKind = kind
1158 , tyConArity = length tyvars
1159 , tyConTyVars = tyvars
1160 , famTcResVar = resVar
1161 , famTcFlav = flav
1162 , famTcParent = parent
1163 , famTcInj = inj
1164 }
1165
1166
1167 -- | Create a promoted data constructor 'TyCon'
1168 -- Somewhat dodgily, we give it the same Name
1169 -- as the data constructor itself; when we pretty-print
1170 -- the TyCon we add a quote; see the Outputable TyCon instance
1171 mkPromotedDataCon :: DataCon -> Name -> Unique -> Kind -> [Role] -> TyCon
1172 mkPromotedDataCon con name unique kind roles
1173 = PromotedDataCon {
1174 tyConName = name,
1175 tyConUnique = unique,
1176 tyConArity = arity,
1177 tcRoles = roles,
1178 tyConKind = kind,
1179 dataCon = con
1180 }
1181 where
1182 arity = length roles
1183
1184 -- | Create a promoted type constructor 'TyCon'
1185 -- Somewhat dodgily, we give it the same Name
1186 -- as the type constructor itself
1187 mkPromotedTyCon :: TyCon -> Kind -> TyCon
1188 mkPromotedTyCon tc kind
1189 = PromotedTyCon {
1190 tyConName = getName tc,
1191 tyConUnique = getUnique tc,
1192 tyConArity = tyConArity tc,
1193 tyConKind = kind,
1194 ty_con = tc
1195 }
1196
1197 isFunTyCon :: TyCon -> Bool
1198 isFunTyCon (FunTyCon {}) = True
1199 isFunTyCon _ = False
1200
1201 -- | Test if the 'TyCon' is algebraic but abstract (invisible data constructors)
1202 isAbstractTyCon :: TyCon -> Bool
1203 isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon {} }) = True
1204 isAbstractTyCon _ = False
1205
1206 -- | Make an algebraic 'TyCon' abstract. Panics if the supplied 'TyCon' is not
1207 -- algebraic
1208 makeTyConAbstract :: TyCon -> TyCon
1209 makeTyConAbstract tc@(AlgTyCon { algTcRhs = rhs })
1210 = tc { algTcRhs = AbstractTyCon (isGenInjAlgRhs rhs) }
1211 makeTyConAbstract tc = pprPanic "makeTyConAbstract" (ppr tc)
1212
1213 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
1214 isPrimTyCon :: TyCon -> Bool
1215 isPrimTyCon (PrimTyCon {}) = True
1216 isPrimTyCon _ = False
1217
1218 -- | Is this 'TyCon' unlifted (i.e. cannot contain bottom)? Note that this can
1219 -- only be true for primitive and unboxed-tuple 'TyCon's
1220 isUnLiftedTyCon :: TyCon -> Bool
1221 isUnLiftedTyCon (PrimTyCon {isUnLifted = is_unlifted})
1222 = is_unlifted
1223 isUnLiftedTyCon (AlgTyCon { algTcRhs = rhs } )
1224 | TupleTyCon { tup_sort = sort } <- rhs
1225 = not (isBoxed (tupleSortBoxity sort))
1226 isUnLiftedTyCon _ = False
1227
1228 -- | Returns @True@ if the supplied 'TyCon' resulted from either a
1229 -- @data@ or @newtype@ declaration
1230 isAlgTyCon :: TyCon -> Bool
1231 isAlgTyCon (AlgTyCon {}) = True
1232 isAlgTyCon _ = False
1233
1234 isDataTyCon :: TyCon -> Bool
1235 -- ^ Returns @True@ for data types that are /definitely/ represented by
1236 -- heap-allocated constructors. These are scrutinised by Core-level
1237 -- @case@ expressions, and they get info tables allocated for them.
1238 --
1239 -- Generally, the function will be true for all @data@ types and false
1240 -- for @newtype@s, unboxed tuples and type family 'TyCon's. But it is
1241 -- not guaranteed to return @True@ in all cases that it could.
1242 --
1243 -- NB: for a data type family, only the /instance/ 'TyCon's
1244 -- get an info table. The family declaration 'TyCon' does not
1245 isDataTyCon (AlgTyCon {algTcRhs = rhs})
1246 = case rhs of
1247 TupleTyCon { tup_sort = sort }
1248 -> isBoxed (tupleSortBoxity sort)
1249 DataTyCon {} -> True
1250 NewTyCon {} -> False
1251 DataFamilyTyCon {} -> False
1252 AbstractTyCon {} -> False -- We don't know, so return False
1253 isDataTyCon _ = False
1254
1255 -- | 'isInjectiveTyCon' is true of 'TyCon's for which this property holds
1256 -- (where X is the role passed in):
1257 -- If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
1258 -- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
1259 -- See also Note [Decomposing equalities] in TcCanonical
1260 isInjectiveTyCon :: TyCon -> Role -> Bool
1261 isInjectiveTyCon _ Phantom = False
1262 isInjectiveTyCon (FunTyCon {}) _ = True
1263 isInjectiveTyCon (AlgTyCon {}) Nominal = True
1264 isInjectiveTyCon (AlgTyCon {algTcRhs = rhs}) Representational
1265 = isGenInjAlgRhs rhs
1266 isInjectiveTyCon (SynonymTyCon {}) _ = False
1267 isInjectiveTyCon (FamilyTyCon {}) _ = False
1268 isInjectiveTyCon (PrimTyCon {}) _ = True
1269 isInjectiveTyCon (PromotedDataCon {}) _ = True
1270 isInjectiveTyCon (PromotedTyCon {ty_con = tc}) r
1271 = isInjectiveTyCon tc r
1272
1273 -- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
1274 -- (where X is the role passed in):
1275 -- If (T tys ~X t), then (t's head ~X T).
1276 -- See also Note [Decomposing equalities] in TcCanonical
1277 isGenerativeTyCon :: TyCon -> Role -> Bool
1278 isGenerativeTyCon = isInjectiveTyCon
1279 -- as it happens, generativity and injectivity coincide, but there's
1280 -- no a priori reason this must be the case
1281
1282 -- | Is this an 'AlgTyConRhs' of a 'TyCon' that is generative and injective
1283 -- with respect to representational equality?
1284 isGenInjAlgRhs :: AlgTyConRhs -> Bool
1285 isGenInjAlgRhs (TupleTyCon {}) = True
1286 isGenInjAlgRhs (DataTyCon {}) = True
1287 isGenInjAlgRhs (DataFamilyTyCon {}) = False
1288 isGenInjAlgRhs (AbstractTyCon distinct) = distinct
1289 isGenInjAlgRhs (NewTyCon {}) = False
1290
1291 -- | Is this 'TyCon' that for a @newtype@
1292 isNewTyCon :: TyCon -> Bool
1293 isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True
1294 isNewTyCon _ = False
1295
1296 -- | Take a 'TyCon' apart into the 'TyVar's it scopes over, the 'Type' it expands
1297 -- into, and (possibly) a coercion from the representation type to the @newtype@.
1298 -- Returns @Nothing@ if this is not possible.
1299 unwrapNewTyCon_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched)
1300 unwrapNewTyCon_maybe (AlgTyCon { tyConTyVars = tvs,
1301 algTcRhs = NewTyCon { nt_co = co,
1302 nt_rhs = rhs }})
1303 = Just (tvs, rhs, co)
1304 unwrapNewTyCon_maybe _ = Nothing
1305
1306 unwrapNewTyConEtad_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched)
1307 unwrapNewTyConEtad_maybe (AlgTyCon { algTcRhs = NewTyCon { nt_co = co,
1308 nt_etad_rhs = (tvs,rhs) }})
1309 = Just (tvs, rhs, co)
1310 unwrapNewTyConEtad_maybe _ = Nothing
1311
1312 isProductTyCon :: TyCon -> Bool
1313 -- True of datatypes or newtypes that have
1314 -- one, non-existential, data constructor
1315 -- See Note [Product types]
1316 isProductTyCon tc@(AlgTyCon {})
1317 = case algTcRhs tc of
1318 TupleTyCon {} -> True
1319 DataTyCon{ data_cons = [data_con] }
1320 -> null (dataConExTyVars data_con)
1321 NewTyCon {} -> True
1322 _ -> False
1323 isProductTyCon _ = False
1324
1325 isDataProductTyCon_maybe :: TyCon -> Maybe DataCon
1326 -- True of datatypes (not newtypes) with
1327 -- one, vanilla, data constructor
1328 -- See Note [Product types]
1329 isDataProductTyCon_maybe (AlgTyCon { algTcRhs = rhs })
1330 = case rhs of
1331 DataTyCon { data_cons = [con] }
1332 | null (dataConExTyVars con) -- non-existential
1333 -> Just con
1334 TupleTyCon { data_con = con }
1335 -> Just con
1336 _ -> Nothing
1337 isDataProductTyCon_maybe _ = Nothing
1338
1339 {- Note [Product types]
1340 ~~~~~~~~~~~~~~~~~~~~~~~
1341 A product type is
1342 * A data type (not a newtype)
1343 * With one, boxed data constructor
1344 * That binds no existential type variables
1345
1346 The main point is that product types are amenable to unboxing for
1347 * Strict function calls; we can transform
1348 f (D a b) = e
1349 to
1350 fw a b = e
1351 via the worker/wrapper transformation. (Question: couldn't this
1352 work for existentials too?)
1353
1354 * CPR for function results; we can transform
1355 f x y = let ... in D a b
1356 to
1357 fw x y = let ... in (# a, b #)
1358
1359 Note that the data constructor /can/ have evidence arguments: equality
1360 constraints, type classes etc. So it can be GADT. These evidence
1361 arguments are simply value arguments, and should not get in the way.
1362 -}
1363
1364
1365 -- | Is this a 'TyCon' representing a regular H98 type synonym (@type@)?
1366 isTypeSynonymTyCon :: TyCon -> Bool
1367 isTypeSynonymTyCon (SynonymTyCon {}) = True
1368 isTypeSynonymTyCon _ = False
1369
1370
1371 -- As for newtypes, it is in some contexts important to distinguish between
1372 -- closed synonyms and synonym families, as synonym families have no unique
1373 -- right hand side to which a synonym family application can expand.
1374 --
1375
1376 mightBeUnsaturatedTyCon :: TyCon -> Bool
1377 -- True iff we can decompose (T a b c) into ((T a b) c)
1378 -- I.e. is it injective and generative w.r.t nominal equality?
1379 -- That is, if (T a b) ~N d e f, is it always the case that
1380 -- (T ~N d), (a ~N e) and (b ~N f)?
1381 -- Specifically NOT true of synonyms (open and otherwise)
1382 --
1383 -- It'd be unusual to call mightBeUnsaturatedTyCon on a regular H98
1384 -- type synonym, because you should probably have expanded it first
1385 -- But regardless, it's not decomposable
1386 mightBeUnsaturatedTyCon (SynonymTyCon {}) = False
1387 mightBeUnsaturatedTyCon (FamilyTyCon {}) = False
1388 mightBeUnsaturatedTyCon _other = True
1389
1390 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
1391 isGadtSyntaxTyCon :: TyCon -> Bool
1392 isGadtSyntaxTyCon (AlgTyCon { algTcGadtSyntax = res }) = res
1393 isGadtSyntaxTyCon _ = False
1394
1395 -- | Is this an algebraic 'TyCon' which is just an enumeration of values?
1396 isEnumerationTyCon :: TyCon -> Bool
1397 -- See Note [Enumeration types] in TyCon
1398 isEnumerationTyCon (AlgTyCon { tyConArity = arity, algTcRhs = rhs })
1399 = case rhs of
1400 DataTyCon { is_enum = res } -> res
1401 TupleTyCon {} -> arity == 0
1402 _ -> False
1403 isEnumerationTyCon _ = False
1404
1405 -- | Is this a 'TyCon', synonym or otherwise, that defines a family?
1406 isFamilyTyCon :: TyCon -> Bool
1407 isFamilyTyCon (FamilyTyCon {}) = True
1408 isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
1409 isFamilyTyCon _ = False
1410
1411 -- | Is this a 'TyCon', synonym or otherwise, that defines a family with
1412 -- instances?
1413 isOpenFamilyTyCon :: TyCon -> Bool
1414 isOpenFamilyTyCon (FamilyTyCon {famTcFlav = OpenSynFamilyTyCon }) = True
1415 isOpenFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon }) = True
1416 isOpenFamilyTyCon _ = False
1417
1418 -- | Is this a synonym 'TyCon' that can have may have further instances appear?
1419 isTypeFamilyTyCon :: TyCon -> Bool
1420 isTypeFamilyTyCon (FamilyTyCon {}) = True
1421 isTypeFamilyTyCon _ = False
1422
1423 -- | Is this an open type family TyCon?
1424 isOpenTypeFamilyTyCon :: TyCon -> Bool
1425 isOpenTypeFamilyTyCon (FamilyTyCon {famTcFlav = OpenSynFamilyTyCon }) = True
1426 isOpenTypeFamilyTyCon _ = False
1427
1428 -- | Is this a non-empty closed type family? Returns 'Nothing' for
1429 -- abstract or empty closed families.
1430 isClosedSynFamilyTyConWithAxiom_maybe :: TyCon -> Maybe (CoAxiom Branched)
1431 isClosedSynFamilyTyConWithAxiom_maybe
1432 (FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb}) = mb
1433 isClosedSynFamilyTyConWithAxiom_maybe _ = Nothing
1434
1435 -- | Try to read the injectivity information from a FamilyTyCon. Only
1436 -- FamilyTyCons can be injective so for every other TyCon this function panics.
1437 familyTyConInjectivityInfo :: TyCon -> Injectivity
1438 familyTyConInjectivityInfo (FamilyTyCon { famTcInj = inj }) = inj
1439 familyTyConInjectivityInfo _ = panic "familyTyConInjectivityInfo"
1440
1441 isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe BuiltInSynFamily
1442 isBuiltInSynFamTyCon_maybe
1443 (FamilyTyCon {famTcFlav = BuiltInSynFamTyCon ops }) = Just ops
1444 isBuiltInSynFamTyCon_maybe _ = Nothing
1445
1446 -- | Is this a synonym 'TyCon' that can have may have further instances appear?
1447 isDataFamilyTyCon :: TyCon -> Bool
1448 isDataFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
1449 isDataFamilyTyCon _ = False
1450
1451 -- | Are we able to extract information 'TyVar' to class argument list
1452 -- mapping from a given 'TyCon'?
1453 isTyConAssoc :: TyCon -> Bool
1454 isTyConAssoc tc = isJust (tyConAssoc_maybe tc)
1455
1456 tyConAssoc_maybe :: TyCon -> Maybe Class
1457 tyConAssoc_maybe tc = case tyConParent tc of
1458 AssocFamilyTyCon cls -> Just cls
1459 _ -> Nothing
1460
1461 -- The unit tycon didn't used to be classed as a tuple tycon
1462 -- but I thought that was silly so I've undone it
1463 -- If it can't be for some reason, it should be a AlgTyCon
1464 isTupleTyCon :: TyCon -> Bool
1465 -- ^ Does this 'TyCon' represent a tuple?
1466 --
1467 -- NB: when compiling @Data.Tuple@, the tycons won't reply @True@ to
1468 -- 'isTupleTyCon', because they are built as 'AlgTyCons'. However they
1469 -- get spat into the interface file as tuple tycons, so I don't think
1470 -- it matters.
1471 isTupleTyCon (AlgTyCon { algTcRhs = TupleTyCon {} }) = True
1472 isTupleTyCon _ = False
1473
1474 tyConTuple_maybe :: TyCon -> Maybe TupleSort
1475 tyConTuple_maybe (AlgTyCon { algTcRhs = rhs })
1476 | TupleTyCon { tup_sort = sort} <- rhs = Just sort
1477 tyConTuple_maybe _ = Nothing
1478
1479 -- | Is this the 'TyCon' for an unboxed tuple?
1480 isUnboxedTupleTyCon :: TyCon -> Bool
1481 isUnboxedTupleTyCon (AlgTyCon { algTcRhs = rhs })
1482 | TupleTyCon { tup_sort = sort } <- rhs
1483 = not (isBoxed (tupleSortBoxity sort))
1484 isUnboxedTupleTyCon _ = False
1485
1486 -- | Is this the 'TyCon' for a boxed tuple?
1487 isBoxedTupleTyCon :: TyCon -> Bool
1488 isBoxedTupleTyCon (AlgTyCon { algTcRhs = rhs })
1489 | TupleTyCon { tup_sort = sort } <- rhs
1490 = isBoxed (tupleSortBoxity sort)
1491 isBoxedTupleTyCon _ = False
1492
1493 -- | Is this a recursive 'TyCon'?
1494 isRecursiveTyCon :: TyCon -> Bool
1495 isRecursiveTyCon (AlgTyCon {algTcRec = Recursive}) = True
1496 isRecursiveTyCon _ = False
1497
1498 promotableTyCon_maybe :: TyCon -> Maybe TyCon
1499 promotableTyCon_maybe (AlgTyCon { tcPromoted = prom }) = prom
1500 promotableTyCon_maybe _ = Nothing
1501
1502 promoteTyCon :: TyCon -> TyCon
1503 promoteTyCon tc = case promotableTyCon_maybe tc of
1504 Just prom_tc -> prom_tc
1505 Nothing -> pprPanic "promoteTyCon" (ppr tc)
1506
1507 -- | Is this a PromotedTyCon?
1508 isPromotedTyCon :: TyCon -> Bool
1509 isPromotedTyCon (PromotedTyCon {}) = True
1510 isPromotedTyCon _ = False
1511
1512 -- | Retrieves the promoted TyCon if this is a PromotedTyCon;
1513 isPromotedTyCon_maybe :: TyCon -> Maybe TyCon
1514 isPromotedTyCon_maybe (PromotedTyCon { ty_con = tc }) = Just tc
1515 isPromotedTyCon_maybe _ = Nothing
1516
1517 -- | Is this a PromotedDataCon?
1518 isPromotedDataCon :: TyCon -> Bool
1519 isPromotedDataCon (PromotedDataCon {}) = True
1520 isPromotedDataCon _ = False
1521
1522 -- | Retrieves the promoted DataCon if this is a PromotedDataCon;
1523 isPromotedDataCon_maybe :: TyCon -> Maybe DataCon
1524 isPromotedDataCon_maybe (PromotedDataCon { dataCon = dc }) = Just dc
1525 isPromotedDataCon_maybe _ = Nothing
1526
1527 -- | Identifies implicit tycons that, in particular, do not go into interface
1528 -- files (because they are implicitly reconstructed when the interface is
1529 -- read).
1530 --
1531 -- Note that:
1532 --
1533 -- * Associated families are implicit, as they are re-constructed from
1534 -- the class declaration in which they reside, and
1535 --
1536 -- * Family instances are /not/ implicit as they represent the instance body
1537 -- (similar to a @dfun@ does that for a class instance).
1538 --
1539 -- * Tuples are implicit iff they have a wired-in name
1540 -- (namely: boxed and unboxed tupeles are wired-in and implicit,
1541 -- but constraint tuples are not)
1542 isImplicitTyCon :: TyCon -> Bool
1543 isImplicitTyCon (FunTyCon {}) = True
1544 isImplicitTyCon (PrimTyCon {}) = True
1545 isImplicitTyCon (PromotedDataCon {}) = True
1546 isImplicitTyCon (PromotedTyCon {}) = True
1547 isImplicitTyCon (AlgTyCon { algTcRhs = rhs, algTcParent = parent, tyConName = name })
1548 | TupleTyCon {} <- rhs = isWiredInName name
1549 | AssocFamilyTyCon {} <- parent = True
1550 | otherwise = False
1551 isImplicitTyCon (FamilyTyCon { famTcParent = parent })
1552 | AssocFamilyTyCon {} <- parent = True
1553 | otherwise = False
1554 isImplicitTyCon (SynonymTyCon {}) = False
1555
1556 tyConCType_maybe :: TyCon -> Maybe CType
1557 tyConCType_maybe tc@(AlgTyCon {}) = tyConCType tc
1558 tyConCType_maybe _ = Nothing
1559
1560 {-
1561 -----------------------------------------------
1562 -- Expand type-constructor applications
1563 -----------------------------------------------
1564 -}
1565
1566 expandSynTyCon_maybe
1567 :: TyCon
1568 -> [tyco] -- ^ Arguments to 'TyCon'
1569 -> Maybe ([(TyVar,tyco)],
1570 Type,
1571 [tyco]) -- ^ Returns a 'TyVar' substitution, the body
1572 -- type of the synonym (not yet substituted)
1573 -- and any arguments remaining from the
1574 -- application
1575
1576 -- ^ Expand a type synonym application, if any
1577 expandSynTyCon_maybe tc tys
1578 | SynonymTyCon { tyConTyVars = tvs, synTcRhs = rhs } <- tc
1579 , let n_tvs = length tvs
1580 = case n_tvs `compare` length tys of
1581 LT -> Just (tvs `zip` tys, rhs, drop n_tvs tys)
1582 EQ -> Just (tvs `zip` tys, rhs, [])
1583 GT -> Nothing
1584 | otherwise
1585 = Nothing
1586
1587 ----------------
1588
1589 -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no
1590 -- constructors could be found
1591 tyConDataCons :: TyCon -> [DataCon]
1592 -- It's convenient for tyConDataCons to return the
1593 -- empty list for type synonyms etc
1594 tyConDataCons tycon = tyConDataCons_maybe tycon `orElse` []
1595
1596 -- | Determine the 'DataCon's originating from the given 'TyCon', if the 'TyCon'
1597 -- is the sort that can have any constructors (note: this does not include
1598 -- abstract algebraic types)
1599 tyConDataCons_maybe :: TyCon -> Maybe [DataCon]
1600 tyConDataCons_maybe (AlgTyCon {algTcRhs = rhs})
1601 = case rhs of
1602 DataTyCon { data_cons = cons } -> Just cons
1603 NewTyCon { data_con = con } -> Just [con]
1604 TupleTyCon { data_con = con } -> Just [con]
1605 _ -> Nothing
1606 tyConDataCons_maybe _ = Nothing
1607
1608 -- | If the given 'TyCon' has a /single/ data constructor, i.e. it is a @data@
1609 -- type with one alternative, a tuple type or a @newtype@ then that constructor
1610 -- is returned. If the 'TyCon' has more than one constructor, or represents a
1611 -- primitive or function type constructor then @Nothing@ is returned. In any
1612 -- other case, the function panics
1613 tyConSingleDataCon_maybe :: TyCon -> Maybe DataCon
1614 tyConSingleDataCon_maybe (AlgTyCon { algTcRhs = rhs })
1615 = case rhs of
1616 DataTyCon { data_cons = [c] } -> Just c
1617 TupleTyCon { data_con = c } -> Just c
1618 NewTyCon { data_con = c } -> Just c
1619 _ -> Nothing
1620 tyConSingleDataCon_maybe _ = Nothing
1621
1622 tyConSingleDataCon :: TyCon -> DataCon
1623 tyConSingleDataCon tc
1624 = case tyConSingleDataCon_maybe tc of
1625 Just c -> c
1626 Nothing -> pprPanic "tyConDataCon" (ppr tc)
1627
1628 tyConSingleAlgDataCon_maybe :: TyCon -> Maybe DataCon
1629 -- Returns (Just con) for single-constructor
1630 -- *algebraic* data types *not* newtypes
1631 tyConSingleAlgDataCon_maybe (AlgTyCon { algTcRhs = rhs })
1632 = case rhs of
1633 DataTyCon { data_cons = [c] } -> Just c
1634 TupleTyCon { data_con = c } -> Just c
1635 _ -> Nothing
1636 tyConSingleAlgDataCon_maybe _ = Nothing
1637
1638 -- | Determine the number of value constructors a 'TyCon' has. Panics if the
1639 -- 'TyCon' is not algebraic or a tuple
1640 tyConFamilySize :: TyCon -> Int
1641 tyConFamilySize tc@(AlgTyCon { algTcRhs = rhs })
1642 = case rhs of
1643 DataTyCon { data_cons = cons } -> length cons
1644 NewTyCon {} -> 1
1645 TupleTyCon {} -> 1
1646 DataFamilyTyCon {} -> 0
1647 _ -> pprPanic "tyConFamilySize 1" (ppr tc)
1648 tyConFamilySize tc = pprPanic "tyConFamilySize 2" (ppr tc)
1649
1650 -- | Extract an 'AlgTyConRhs' with information about data constructors from an
1651 -- algebraic or tuple 'TyCon'. Panics for any other sort of 'TyCon'
1652 algTyConRhs :: TyCon -> AlgTyConRhs
1653 algTyConRhs (AlgTyCon {algTcRhs = rhs}) = rhs
1654 algTyConRhs other = pprPanic "algTyConRhs" (ppr other)
1655
1656 -- | Extract type variable naming the result of injective type family
1657 tyConFamilyResVar_maybe :: TyCon -> Maybe Name
1658 tyConFamilyResVar_maybe (FamilyTyCon {famTcResVar = res}) = res
1659 tyConFamilyResVar_maybe _ = Nothing
1660
1661 -- | Get the list of roles for the type parameters of a TyCon
1662 tyConRoles :: TyCon -> [Role]
1663 -- See also Note [TyCon Role signatures]
1664 tyConRoles tc
1665 = case tc of
1666 { FunTyCon {} -> const_role Representational
1667 ; AlgTyCon { tcRoles = roles } -> roles
1668 ; SynonymTyCon { tcRoles = roles } -> roles
1669 ; FamilyTyCon {} -> const_role Nominal
1670 ; PrimTyCon { tcRoles = roles } -> roles
1671 ; PromotedDataCon { tcRoles = roles } -> roles
1672 ; PromotedTyCon {} -> const_role Nominal
1673 }
1674 where
1675 const_role r = replicate (tyConArity tc) r
1676
1677 -- | Extract the bound type variables and type expansion of a type synonym
1678 -- 'TyCon'. Panics if the 'TyCon' is not a synonym
1679 newTyConRhs :: TyCon -> ([TyVar], Type)
1680 newTyConRhs (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon { nt_rhs = rhs }})
1681 = (tvs, rhs)
1682 newTyConRhs tycon = pprPanic "newTyConRhs" (ppr tycon)
1683
1684 -- | The number of type parameters that need to be passed to a newtype to
1685 -- resolve it. May be less than in the definition if it can be eta-contracted.
1686 newTyConEtadArity :: TyCon -> Int
1687 newTyConEtadArity (AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }})
1688 = length (fst tvs_rhs)
1689 newTyConEtadArity tycon = pprPanic "newTyConEtadArity" (ppr tycon)
1690
1691 -- | Extract the bound type variables and type expansion of an eta-contracted
1692 -- type synonym 'TyCon'. Panics if the 'TyCon' is not a synonym
1693 newTyConEtadRhs :: TyCon -> ([TyVar], Type)
1694 newTyConEtadRhs (AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }}) = tvs_rhs
1695 newTyConEtadRhs tycon = pprPanic "newTyConEtadRhs" (ppr tycon)
1696
1697 -- | Extracts the @newtype@ coercion from such a 'TyCon', which can be used to
1698 -- construct something with the @newtype@s type from its representation type
1699 -- (right hand side). If the supplied 'TyCon' is not a @newtype@, returns
1700 -- @Nothing@
1701 newTyConCo_maybe :: TyCon -> Maybe (CoAxiom Unbranched)
1702 newTyConCo_maybe (AlgTyCon {algTcRhs = NewTyCon { nt_co = co }}) = Just co
1703 newTyConCo_maybe _ = Nothing
1704
1705 newTyConCo :: TyCon -> CoAxiom Unbranched
1706 newTyConCo tc = case newTyConCo_maybe tc of
1707 Just co -> co
1708 Nothing -> pprPanic "newTyConCo" (ppr tc)
1709
1710 -- | Find the primitive representation of a 'TyCon'
1711 tyConPrimRep :: TyCon -> PrimRep
1712 tyConPrimRep (PrimTyCon {primTyConRep = rep}) = rep
1713 tyConPrimRep tc = ASSERT(not (isUnboxedTupleTyCon tc)) PtrRep
1714
1715 -- | Find the \"stupid theta\" of the 'TyCon'. A \"stupid theta\" is the context
1716 -- to the left of an algebraic type declaration, e.g. @Eq a@ in the declaration
1717 -- @data Eq a => T a ...@
1718 tyConStupidTheta :: TyCon -> [PredType]
1719 tyConStupidTheta (AlgTyCon {algTcStupidTheta = stupid}) = stupid
1720 tyConStupidTheta tycon = pprPanic "tyConStupidTheta" (ppr tycon)
1721
1722 -- | Extract the 'TyVar's bound by a vanilla type synonym
1723 -- and the corresponding (unsubstituted) right hand side.
1724 synTyConDefn_maybe :: TyCon -> Maybe ([TyVar], Type)
1725 synTyConDefn_maybe (SynonymTyCon {tyConTyVars = tyvars, synTcRhs = ty})
1726 = Just (tyvars, ty)
1727 synTyConDefn_maybe _ = Nothing
1728
1729 -- | Extract the information pertaining to the right hand side of a type synonym
1730 -- (@type@) declaration.
1731 synTyConRhs_maybe :: TyCon -> Maybe Type
1732 synTyConRhs_maybe (SynonymTyCon {synTcRhs = rhs}) = Just rhs
1733 synTyConRhs_maybe _ = Nothing
1734
1735 -- | Extract the flavour of a type family (with all the extra information that
1736 -- it carries)
1737 famTyConFlav_maybe :: TyCon -> Maybe FamTyConFlav
1738 famTyConFlav_maybe (FamilyTyCon {famTcFlav = flav}) = Just flav
1739 famTyConFlav_maybe _ = Nothing
1740
1741 -- | Is this 'TyCon' that for a class instance?
1742 isClassTyCon :: TyCon -> Bool
1743 isClassTyCon (AlgTyCon {algTcParent = ClassTyCon _}) = True
1744 isClassTyCon _ = False
1745
1746 -- | If this 'TyCon' is that for a class instance, return the class it is for.
1747 -- Otherwise returns @Nothing@
1748 tyConClass_maybe :: TyCon -> Maybe Class
1749 tyConClass_maybe (AlgTyCon {algTcParent = ClassTyCon clas}) = Just clas
1750 tyConClass_maybe _ = Nothing
1751
1752 ----------------------------------------------------------------------------
1753 tyConParent :: TyCon -> TyConParent
1754 tyConParent (AlgTyCon {algTcParent = parent}) = parent
1755 tyConParent (FamilyTyCon {famTcParent = parent}) = parent
1756 tyConParent _ = NoParentTyCon
1757
1758 ----------------------------------------------------------------------------
1759 -- | Is this 'TyCon' that for a data family instance?
1760 isFamInstTyCon :: TyCon -> Bool
1761 isFamInstTyCon tc = case tyConParent tc of
1762 FamInstTyCon {} -> True
1763 _ -> False
1764
1765 tyConFamInstSig_maybe :: TyCon -> Maybe (TyCon, [Type], CoAxiom Unbranched)
1766 tyConFamInstSig_maybe tc
1767 = case tyConParent tc of
1768 FamInstTyCon ax f ts -> Just (f, ts, ax)
1769 _ -> Nothing
1770
1771 -- | If this 'TyCon' is that of a family instance, return the family in question
1772 -- and the instance types. Otherwise, return @Nothing@
1773 tyConFamInst_maybe :: TyCon -> Maybe (TyCon, [Type])
1774 tyConFamInst_maybe tc
1775 = case tyConParent tc of
1776 FamInstTyCon _ f ts -> Just (f, ts)
1777 _ -> Nothing
1778
1779 -- | If this 'TyCon' is that of a family instance, return a 'TyCon' which
1780 -- represents a coercion identifying the representation type with the type
1781 -- instance family. Otherwise, return @Nothing@
1782 tyConFamilyCoercion_maybe :: TyCon -> Maybe (CoAxiom Unbranched)
1783 tyConFamilyCoercion_maybe tc
1784 = case tyConParent tc of
1785 FamInstTyCon co _ _ -> Just co
1786 _ -> Nothing
1787
1788 {-
1789 ************************************************************************
1790 * *
1791 \subsection[TyCon-instances]{Instance declarations for @TyCon@}
1792 * *
1793 ************************************************************************
1794
1795 @TyCon@s are compared by comparing their @Unique@s.
1796
1797 The strictness analyser needs @Ord@. It is a lexicographic order with
1798 the property @(a<=b) || (b<=a)@.
1799 -}
1800
1801 instance Eq TyCon where
1802 a == b = case (a `compare` b) of { EQ -> True; _ -> False }
1803 a /= b = case (a `compare` b) of { EQ -> False; _ -> True }
1804
1805 instance Ord TyCon where
1806 a <= b = case (a `compare` b) of { LT -> True; EQ -> True; GT -> False }
1807 a < b = case (a `compare` b) of { LT -> True; EQ -> False; GT -> False }
1808 a >= b = case (a `compare` b) of { LT -> False; EQ -> True; GT -> True }
1809 a > b = case (a `compare` b) of { LT -> False; EQ -> False; GT -> True }
1810 compare a b = getUnique a `compare` getUnique b
1811
1812 instance Uniquable TyCon where
1813 getUnique tc = tyConUnique tc
1814
1815 instance Outputable TyCon where
1816 -- At the moment a promoted TyCon has the same Name as its
1817 -- corresponding TyCon, so we add the quote to distinguish it here
1818 ppr tc = pprPromotionQuote tc <> ppr (tyConName tc)
1819
1820 tyConFlavour :: TyCon -> String
1821 tyConFlavour (AlgTyCon { algTcParent = parent, algTcRhs = rhs })
1822 | ClassTyCon _ <- parent = "class"
1823 | otherwise = case rhs of
1824 TupleTyCon { tup_sort = sort }
1825 | isBoxed (tupleSortBoxity sort) -> "tuple"
1826 | otherwise -> "unboxed tuple"
1827 DataTyCon {} -> "data type"
1828 NewTyCon {} -> "newtype"
1829 DataFamilyTyCon {} -> "data family"
1830 AbstractTyCon {} -> "abstract type"
1831 tyConFlavour (FamilyTyCon {}) = "type family"
1832 tyConFlavour (SynonymTyCon {}) = "type synonym"
1833 tyConFlavour (FunTyCon {}) = "built-in type"
1834 tyConFlavour (PrimTyCon {}) = "built-in type"
1835 tyConFlavour (PromotedDataCon {}) = "promoted data constructor"
1836 tyConFlavour (PromotedTyCon {}) = "promoted type constructor"
1837
1838 pprPromotionQuote :: TyCon -> SDoc
1839 pprPromotionQuote (PromotedDataCon {}) = char '\'' -- Quote promoted DataCons
1840 -- in types
1841 pprPromotionQuote (PromotedTyCon {}) = ifPprDebug (char '\'')
1842 pprPromotionQuote _ = empty -- However, we don't quote TyCons
1843 -- in kinds e.g.
1844 -- type family T a :: Bool -> *
1845 -- cf Trac #5952.
1846 -- Except with -dppr-debug
1847
1848 instance NamedThing TyCon where
1849 getName = tyConName
1850
1851 instance Data.Data TyCon where
1852 -- don't traverse?
1853 toConstr _ = abstractConstr "TyCon"
1854 gunfold _ _ = error "gunfold"
1855 dataTypeOf _ = mkNoRepType "TyCon"
1856
1857 instance Binary Injectivity where
1858 put_ bh NotInjective = putByte bh 0
1859 put_ bh (Injective xs) = putByte bh 1 >> put_ bh xs
1860
1861 get bh = do { h <- getByte bh
1862 ; case h of
1863 0 -> return NotInjective
1864 _ -> do { xs <- get bh
1865 ; return (Injective xs) } }
1866
1867 {-
1868 ************************************************************************
1869 * *
1870 Walking over recursive TyCons
1871 * *
1872 ************************************************************************
1873
1874 Note [Expanding newtypes and products]
1875 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1876 When expanding a type to expose a data-type constructor, we need to be
1877 careful about newtypes, lest we fall into an infinite loop. Here are
1878 the key examples:
1879
1880 newtype Id x = MkId x
1881 newtype Fix f = MkFix (f (Fix f))
1882 newtype T = MkT (T -> T)
1883
1884 Type Expansion
1885 --------------------------
1886 T T -> T
1887 Fix Maybe Maybe (Fix Maybe)
1888 Id (Id Int) Int
1889 Fix Id NO NO NO
1890
1891 Notice that
1892 * We can expand T, even though it's recursive.
1893 * We can expand Id (Id Int), even though the Id shows up
1894 twice at the outer level, because Id is non-recursive
1895
1896 So, when expanding, we keep track of when we've seen a recursive
1897 newtype at outermost level; and bale out if we see it again.
1898
1899 We sometimes want to do the same for product types, so that the
1900 strictness analyser doesn't unbox infinitely deeply.
1901
1902 More precisely, we keep a *count* of how many times we've seen it.
1903 This is to account for
1904 data instance T (a,b) = MkT (T a) (T b)
1905 Then (Trac #10482) if we have a type like
1906 T (Int,(Int,(Int,(Int,Int))))
1907 we can still unbox deeply enough during strictness analysis.
1908 We have to treat T as potentially recursive, but it's still
1909 good to be able to unwrap multiple layers.
1910
1911 The function that manages all this is checkRecTc.
1912 -}
1913
1914 data RecTcChecker = RC !Int (NameEnv Int)
1915 -- The upper bound, and the number of times
1916 -- we have encountered each TyCon
1917
1918 initRecTc :: RecTcChecker
1919 -- Intialise with a fixed max bound of 100
1920 -- We should probably have a flag for this
1921 initRecTc = RC 100 emptyNameEnv
1922
1923 checkRecTc :: RecTcChecker -> TyCon -> Maybe RecTcChecker
1924 -- Nothing => Recursion detected
1925 -- Just rec_tcs => Keep going
1926 checkRecTc rc@(RC bound rec_nts) tc
1927 | not (isRecursiveTyCon tc)
1928 = Just rc -- Tuples are a common example here
1929 | otherwise
1930 = case lookupNameEnv rec_nts tc_name of
1931 Just n | n >= bound -> Nothing
1932 | otherwise -> Just (RC bound (extendNameEnv rec_nts tc_name (n+1)))
1933 Nothing -> Just (RC bound (extendNameEnv rec_nts tc_name 1))
1934 where
1935 tc_name = tyConName tc