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