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