never executed always true always false
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1998
4
5 \section[DataCon]{@DataCon@: Data Constructors}
6 -}
7
8 {-# LANGUAGE DeriveDataTypeable #-}
9
10 module GHC.Core.DataCon (
11 -- * Main data types
12 DataCon, DataConRep(..),
13 SrcStrictness(..), SrcUnpackedness(..),
14 HsSrcBang(..), HsImplBang(..),
15 StrictnessMark(..),
16 ConTag,
17
18 -- ** Equality specs
19 EqSpec, mkEqSpec, eqSpecTyVar, eqSpecType,
20 eqSpecPair, eqSpecPreds,
21 substEqSpec, filterEqSpec,
22
23 -- ** Field labels
24 FieldLabel(..), FieldLabelString,
25
26 -- ** Type construction
27 mkDataCon, fIRST_TAG,
28
29 -- ** Type deconstruction
30 dataConRepType, dataConInstSig, dataConFullSig,
31 dataConName, dataConIdentity, dataConTag, dataConTagZ,
32 dataConTyCon, dataConOrigTyCon,
33 dataConWrapperType,
34 dataConNonlinearType,
35 dataConDisplayType,
36 dataConUnivTyVars, dataConExTyCoVars, dataConUnivAndExTyCoVars,
37 dataConUserTyVars, dataConUserTyVarBinders,
38 dataConEqSpec, dataConTheta,
39 dataConStupidTheta,
40 dataConOtherTheta,
41 dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
42 dataConInstOrigArgTys, dataConRepArgTys,
43 dataConFieldLabels, dataConFieldType, dataConFieldType_maybe,
44 dataConSrcBangs,
45 dataConSourceArity, dataConRepArity,
46 dataConIsInfix,
47 dataConWorkId, dataConWrapId, dataConWrapId_maybe,
48 dataConImplicitTyThings,
49 dataConRepStrictness, dataConImplBangs, dataConBoxer,
50
51 splitDataProductType_maybe,
52
53 -- ** Predicates on DataCons
54 isNullarySrcDataCon, isNullaryRepDataCon,
55 isTupleDataCon, isBoxedTupleDataCon, isUnboxedTupleDataCon,
56 isUnboxedSumDataCon,
57 isVanillaDataCon, isNewDataCon, classDataCon, dataConCannotMatch,
58 dataConUserTyVarsArePermuted,
59 isBanged, isMarkedStrict, eqHsBang, isSrcStrict, isSrcUnpacked,
60 specialPromotedDc,
61
62 -- ** Promotion related functions
63 promoteDataCon
64 ) where
65
66 import GHC.Prelude
67
68 import {-# SOURCE #-} GHC.Types.Id.Make ( DataConBoxer )
69 import GHC.Core.Type as Type
70 import GHC.Core.Coercion
71 import GHC.Core.Unify
72 import GHC.Core.TyCon
73 import GHC.Core.Multiplicity
74 import {-# SOURCE #-} GHC.Types.TyThing
75 import GHC.Types.FieldLabel
76 import GHC.Types.SourceText
77 import GHC.Core.Class
78 import GHC.Types.Name
79 import GHC.Builtin.Names
80 import GHC.Core.Predicate
81 import GHC.Types.Var
82 import GHC.Types.Basic
83 import GHC.Data.FastString
84 import GHC.Unit.Types
85 import GHC.Unit.Module.Name
86 import GHC.Utils.Binary
87 import GHC.Types.Unique.Set
88 import GHC.Builtin.Uniques( mkAlphaTyVarUnique )
89
90 import GHC.Utils.Outputable
91 import GHC.Utils.Misc
92 import GHC.Utils.Panic
93 import GHC.Utils.Panic.Plain
94
95 import Data.ByteString (ByteString)
96 import qualified Data.ByteString.Builder as BSB
97 import qualified Data.ByteString.Lazy as LBS
98 import qualified Data.Data as Data
99 import Data.Char
100 import Data.List( find )
101
102 {-
103 Data constructor representation
104 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
105 Consider the following Haskell data type declaration
106
107 data T = T !Int ![Int]
108
109 Using the strictness annotations, GHC will represent this as
110
111 data T = T Int# [Int]
112
113 That is, the Int has been unboxed. Furthermore, the Haskell source construction
114
115 T e1 e2
116
117 is translated to
118
119 case e1 of { I# x ->
120 case e2 of { r ->
121 T x r }}
122
123 That is, the first argument is unboxed, and the second is evaluated. Finally,
124 pattern matching is translated too:
125
126 case e of { T a b -> ... }
127
128 becomes
129
130 case e of { T a' b -> let a = I# a' in ... }
131
132 To keep ourselves sane, we name the different versions of the data constructor
133 differently, as follows.
134
135
136 Note [Data Constructor Naming]
137 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
138 Each data constructor C has two, and possibly up to four, Names associated with it:
139
140 OccName Name space Name of Notes
141 ---------------------------------------------------------------------------
142 The "data con itself" C DataName DataCon In dom( GlobalRdrEnv )
143 The "worker data con" C VarName Id The worker
144 The "wrapper data con" $WC VarName Id The wrapper
145 The "newtype coercion" :CoT TcClsName TyCon
146
147 EVERY data constructor (incl for newtypes) has the former two (the
148 data con itself, and its worker. But only some data constructors have a
149 wrapper (see Note [The need for a wrapper]).
150
151 Each of these three has a distinct Unique. The "data con itself" name
152 appears in the output of the renamer, and names the Haskell-source
153 data constructor. The type checker translates it into either the wrapper Id
154 (if it exists) or worker Id (otherwise).
155
156 The data con has one or two Ids associated with it:
157
158 The "worker Id", is the actual data constructor.
159 * Every data constructor (newtype or data type) has a worker
160
161 * The worker is very like a primop, in that it has no binding.
162
163 * For a *data* type, the worker *is* the data constructor;
164 it has no unfolding
165
166 * For a *newtype*, the worker has a compulsory unfolding which
167 does a cast, e.g.
168 newtype T = MkT Int
169 The worker for MkT has unfolding
170 \\(x:Int). x `cast` sym CoT
171 Here CoT is the type constructor, witnessing the FC axiom
172 axiom CoT : T = Int
173
174 The "wrapper Id", \$WC, goes as follows
175
176 * Its type is exactly what it looks like in the source program.
177
178 * It is an ordinary function, and it gets a top-level binding
179 like any other function.
180
181 * The wrapper Id isn't generated for a data type if there is
182 nothing for the wrapper to do. That is, if its defn would be
183 \$wC = C
184
185 Note [Data constructor workers and wrappers]
186 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
187 * Algebraic data types
188 - Always have a worker, with no unfolding
189 - May or may not have a wrapper; see Note [The need for a wrapper]
190
191 * Newtypes
192 - Always have a worker, which has a compulsory unfolding (just a cast)
193 - May or may not have a wrapper; see Note [The need for a wrapper]
194
195 * INVARIANT: the dictionary constructor for a class
196 never has a wrapper.
197
198 * See Note [Data Constructor Naming] for how the worker and wrapper
199 are named
200
201 * Neither_ the worker _nor_ the wrapper take the dcStupidTheta dicts as arguments
202
203 * The wrapper (if it exists) takes dcOrigArgTys as its arguments.
204 The worker takes dataConRepArgTys as its arguments
205 If the worker is absent, dataConRepArgTys is the same as dcOrigArgTys
206
207 * The 'NoDataConRep' case of DataConRep is important. Not only is it
208 efficient, but it also ensures that the wrapper is replaced by the
209 worker (because it *is* the worker) even when there are no
210 args. E.g. in
211 f (:) x
212 the (:) *is* the worker. This is really important in rule matching,
213 (We could match on the wrappers, but that makes it less likely that
214 rules will match when we bring bits of unfoldings together.)
215
216 Note [The need for a wrapper]
217 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
218 Why might the wrapper have anything to do? The full story is
219 in wrapper_reqd in GHC.Types.Id.Make.mkDataConRep.
220
221 * Unboxing strict fields (with -funbox-strict-fields)
222 data T = MkT !(Int,Int)
223 \$wMkT :: (Int,Int) -> T
224 \$wMkT (x,y) = MkT x y
225 Notice that the worker has two fields where the wapper has
226 just one. That is, the worker has type
227 MkT :: Int -> Int -> T
228
229 * Equality constraints for GADTs
230 data T a where { MkT :: a -> T [a] }
231
232 The worker gets a type with explicit equality
233 constraints, thus:
234 MkT :: forall a b. (a=[b]) => b -> T a
235
236 The wrapper has the programmer-specified type:
237 \$wMkT :: a -> T [a]
238 \$wMkT a x = MkT [a] a [a] x
239 The third argument is a coercion
240 [a] :: [a]~[a]
241
242 * Data family instances may do a cast on the result
243
244 * Type variables may be permuted; see MkId
245 Note [Data con wrappers and GADT syntax]
246
247
248 Note [The stupid context]
249 ~~~~~~~~~~~~~~~~~~~~~~~~~
250 Data types can have a context:
251
252 data (Eq a, Ord b) => T a b = T1 a b | T2 a
253
254 and that makes the constructors have a context too
255 (notice that T2's context is "thinned"):
256
257 T1 :: (Eq a, Ord b) => a -> b -> T a b
258 T2 :: (Eq a) => a -> T a b
259
260 Furthermore, this context pops up when pattern matching
261 (though GHC hasn't implemented this, but it is in H98, and
262 I've fixed GHC so that it now does):
263
264 f (T2 x) = x
265 gets inferred type
266 f :: Eq a => T a b -> a
267
268 I say the context is "stupid" because the dictionaries passed
269 are immediately discarded -- they do nothing and have no benefit.
270 It's a flaw in the language.
271
272 Up to now [March 2002] I have put this stupid context into the
273 type of the "wrapper" constructors functions, T1 and T2, but
274 that turned out to be jolly inconvenient for generics, and
275 record update, and other functions that build values of type T
276 (because they don't have suitable dictionaries available).
277
278 So now I've taken the stupid context out. I simply deal with
279 it separately in the type checker on occurrences of a
280 constructor, either in an expression or in a pattern.
281
282 [May 2003: actually I think this decision could easily be
283 reversed now, and probably should be. Generics could be
284 disabled for types with a stupid context; record updates now
285 (H98) needs the context too; etc. It's an unforced change, so
286 I'm leaving it for now --- but it does seem odd that the
287 wrapper doesn't include the stupid context.]
288
289 [July 04] With the advent of generalised data types, it's less obvious
290 what the "stupid context" is. Consider
291 C :: forall a. Ord a => a -> a -> T (Foo a)
292 Does the C constructor in Core contain the Ord dictionary? Yes, it must:
293
294 f :: T b -> Ordering
295 f = /\b. \x:T b.
296 case x of
297 C a (d:Ord a) (p:a) (q:a) -> compare d p q
298
299 Note that (Foo a) might not be an instance of Ord.
300
301 ************************************************************************
302 * *
303 \subsection{Data constructors}
304 * *
305 ************************************************************************
306 -}
307
308 -- | A data constructor
309 --
310 -- - 'GHC.Parser.Annotation.AnnKeywordId' : 'GHC.Parser.Annotation.AnnOpen',
311 -- 'GHC.Parser.Annotation.AnnClose','GHC.Parser.Annotation.AnnComma'
312
313 -- For details on above see note [exact print annotations] in GHC.Parser.Annotation
314 data DataCon
315 = MkData {
316 dcName :: Name, -- This is the name of the *source data con*
317 -- (see "Note [Data Constructor Naming]" above)
318 dcUnique :: Unique, -- Cached from Name
319 dcTag :: ConTag, -- ^ Tag, used for ordering 'DataCon's
320
321 -- Running example:
322 --
323 -- *** As declared by the user
324 -- data T a b c where
325 -- MkT :: forall c y x b. (x~y,Ord x) => x -> y -> T (x,y) b c
326
327 -- *** As represented internally
328 -- data T a b c where
329 -- MkT :: forall a b c. forall x y. (a~(x,y),x~y,Ord x)
330 -- => x -> y -> T a b c
331 --
332 -- The next six fields express the type of the constructor, in pieces
333 -- e.g.
334 --
335 -- dcUnivTyVars = [a,b,c]
336 -- dcExTyCoVars = [x,y]
337 -- dcUserTyVarBinders = [c,y,x,b]
338 -- dcEqSpec = [a~(x,y)]
339 -- dcOtherTheta = [x~y, Ord x]
340 -- dcOrigArgTys = [x,y]
341 -- dcRepTyCon = T
342
343 -- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE
344 -- TYVARS FOR THE PARENT TyCon. (This is a change (Oct05): previously,
345 -- vanilla datacons guaranteed to have the same type variables as their
346 -- parent TyCon, but that seems ugly.) They can be different in the case
347 -- where a GADT constructor uses different names for the universal
348 -- tyvars than does the tycon. For example:
349 --
350 -- data H a where
351 -- MkH :: b -> H b
352 --
353 -- Here, the tyConTyVars of H will be [a], but the dcUnivTyVars of MkH
354 -- will be [b].
355
356 dcVanilla :: Bool, -- True <=> This is a vanilla Haskell 98 data constructor
357 -- Its type is of form
358 -- forall a1..an . t1 -> ... tm -> T a1..an
359 -- No existentials, no coercions, nothing.
360 -- That is: dcExTyCoVars = dcEqSpec = dcOtherTheta = []
361 -- NB 1: newtypes always have a vanilla data con
362 -- NB 2: a vanilla constructor can still be declared in GADT-style
363 -- syntax, provided its type looks like the above.
364 -- The declaration format is held in the TyCon (algTcGadtSyntax)
365
366 -- Universally-quantified type vars [a,b,c]
367 -- INVARIANT: length matches arity of the dcRepTyCon
368 -- INVARIANT: result type of data con worker is exactly (T a b c)
369 -- COROLLARY: The dcUnivTyVars are always in one-to-one correspondence with
370 -- the tyConTyVars of the parent TyCon
371 dcUnivTyVars :: [TyVar],
372
373 -- Existentially-quantified type and coercion vars [x,y]
374 -- For an example involving coercion variables,
375 -- Why tycovars? See Note [Existential coercion variables]
376 dcExTyCoVars :: [TyCoVar],
377
378 -- INVARIANT: the UnivTyVars and ExTyCoVars all have distinct OccNames
379 -- Reason: less confusing, and easier to generate Iface syntax
380
381 -- The type/coercion vars in the order the user wrote them [c,y,x,b]
382 -- INVARIANT: the set of tyvars in dcUserTyVarBinders is exactly the set
383 -- of tyvars (*not* covars) of dcExTyCoVars unioned with the
384 -- set of dcUnivTyVars whose tyvars do not appear in dcEqSpec
385 -- See Note [DataCon user type variable binders]
386 dcUserTyVarBinders :: [InvisTVBinder],
387
388 dcEqSpec :: [EqSpec], -- Equalities derived from the result type,
389 -- _as written by the programmer_.
390 -- Only non-dependent GADT equalities (dependent
391 -- GADT equalities are in the covars of
392 -- dcExTyCoVars).
393
394 -- This field allows us to move conveniently between the two ways
395 -- of representing a GADT constructor's type:
396 -- MkT :: forall a b. (a ~ [b]) => b -> T a
397 -- MkT :: forall b. b -> T [b]
398 -- Each equality is of the form (a ~ ty), where 'a' is one of
399 -- the universally quantified type variables. Moreover, the
400 -- only place in the DataCon where this 'a' will occur is in
401 -- dcUnivTyVars. See [The dcEqSpec domain invariant].
402
403 -- The next two fields give the type context of the data constructor
404 -- (aside from the GADT constraints,
405 -- which are given by the dcExpSpec)
406 -- In GADT form, this is *exactly* what the programmer writes, even if
407 -- the context constrains only universally quantified variables
408 -- MkT :: forall a b. (a ~ b, Ord b) => a -> T a b
409 dcOtherTheta :: ThetaType, -- The other constraints in the data con's type
410 -- other than those in the dcEqSpec
411
412 dcStupidTheta :: ThetaType, -- The context of the data type declaration
413 -- data Eq a => T a = ...
414 -- or, rather, a "thinned" version thereof
415 -- "Thinned", because the Report says
416 -- to eliminate any constraints that don't mention
417 -- tyvars free in the arg types for this constructor
418 --
419 -- INVARIANT: the free tyvars of dcStupidTheta are a subset of dcUnivTyVars
420 -- Reason: dcStupidTeta is gotten by thinning the stupid theta from the tycon
421 --
422 -- "Stupid", because the dictionaries aren't used for anything.
423 -- Indeed, [as of March 02] they are no longer in the type of
424 -- the wrapper Id, because that makes it harder to use the wrap-id
425 -- to rebuild values after record selection or in generics.
426
427 dcOrigArgTys :: [Scaled Type], -- Original argument types
428 -- (before unboxing and flattening of strict fields)
429 dcOrigResTy :: Type, -- Original result type, as seen by the user
430 -- NB: for a data instance, the original user result type may
431 -- differ from the DataCon's representation TyCon. Example
432 -- data instance T [a] where MkT :: a -> T [a]
433 -- The dcOrigResTy is T [a], but the dcRepTyCon might be R:TList
434
435 -- Now the strictness annotations and field labels of the constructor
436 dcSrcBangs :: [HsSrcBang],
437 -- See Note [Bangs on data constructor arguments]
438 --
439 -- The [HsSrcBang] as written by the programmer.
440 --
441 -- Matches 1-1 with dcOrigArgTys
442 -- Hence length = dataConSourceArity dataCon
443
444 dcFields :: [FieldLabel],
445 -- Field labels for this constructor, in the
446 -- same order as the dcOrigArgTys;
447 -- length = 0 (if not a record) or dataConSourceArity.
448
449 -- The curried worker function that corresponds to the constructor:
450 -- It doesn't have an unfolding; the code generator saturates these Ids
451 -- and allocates a real constructor when it finds one.
452 dcWorkId :: Id,
453
454 -- Constructor representation
455 dcRep :: DataConRep,
456
457 -- Cached; see Note [DataCon arities]
458 -- INVARIANT: dcRepArity == length dataConRepArgTys + count isCoVar (dcExTyCoVars)
459 -- INVARIANT: dcSourceArity == length dcOrigArgTys
460 dcRepArity :: Arity,
461 dcSourceArity :: Arity,
462
463 -- Result type of constructor is T t1..tn
464 dcRepTyCon :: TyCon, -- Result tycon, T
465
466 dcRepType :: Type, -- Type of the constructor
467 -- forall a x y. (a~(x,y), x~y, Ord x) =>
468 -- x -> y -> T a
469 -- (this is *not* of the constructor wrapper Id:
470 -- see Note [Data con representation] below)
471 -- Notice that the existential type parameters come *second*.
472 -- Reason: in a case expression we may find:
473 -- case (e :: T t) of
474 -- MkT x y co1 co2 (d:Ord x) (v:r) (w:F s) -> ...
475 -- It's convenient to apply the rep-type of MkT to 't', to get
476 -- forall x y. (t~(x,y), x~y, Ord x) => x -> y -> T t
477 -- and use that to check the pattern. Mind you, this is really only
478 -- used in GHC.Core.Lint.
479
480
481 dcInfix :: Bool, -- True <=> declared infix
482 -- Used for Template Haskell and 'deriving' only
483 -- The actual fixity is stored elsewhere
484
485 dcPromoted :: TyCon -- The promoted TyCon
486 -- See Note [Promoted data constructors] in GHC.Core.TyCon
487 }
488
489
490 {- Note [TyVarBinders in DataCons]
491 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
492 For the TyVarBinders in a DataCon and PatSyn:
493
494 * Each argument flag is Inferred or Specified.
495 None are Required. (A DataCon is a term-level function; see
496 Note [No Required TyCoBinder in terms] in GHC.Core.TyCo.Rep.)
497
498 Why do we need the TyVarBinders, rather than just the TyVars? So that
499 we can construct the right type for the DataCon with its foralls
500 attributed the correct visibility. That in turn governs whether you
501 can use visible type application at a call of the data constructor.
502
503 See also [DataCon user type variable binders] for an extended discussion on the
504 order in which TyVarBinders appear in a DataCon.
505
506 Note [Existential coercion variables]
507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
508
509 For now (Aug 2018) we can't write coercion quantifications in source Haskell, but
510 we can in Core. Consider having:
511
512 data T :: forall k. k -> k -> Constraint where
513 MkT :: forall k (a::k) (b::k). forall k' (c::k') (co::k'~k). (b~(c|>co))
514 => T k a b
515
516 dcUnivTyVars = [k,a,b]
517 dcExTyCoVars = [k',c,co]
518 dcUserTyVarBinders = [k,a,k',c]
519 dcEqSpec = [b~(c|>co)]
520 dcOtherTheta = []
521 dcOrigArgTys = []
522 dcRepTyCon = T
523
524 Function call 'dataConKindEqSpec' returns [k'~k]
525
526 Note [DataCon arities]
527 ~~~~~~~~~~~~~~~~~~~~~~
528 dcSourceArity does not take constraints into account,
529 but dcRepArity does. For example:
530 MkT :: Ord a => a -> T a
531 dcSourceArity = 1
532 dcRepArity = 2
533
534 Note [DataCon user type variable binders]
535 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
536 In System FC, data constructor type signatures always quantify over all of
537 their universal type variables, followed by their existential type variables.
538 Normally, this isn't a problem, as most datatypes naturally quantify their type
539 variables in this order anyway. For example:
540
541 data T a b = forall c. MkT b c
542
543 Here, we have `MkT :: forall {k} (a :: k) (b :: *) (c :: *). b -> c -> T a b`,
544 where k, a, and b are universal and c is existential. (The inferred variable k
545 isn't available for TypeApplications, hence why it's in braces.) This is a
546 perfectly reasonable order to use, as the syntax of H98-style datatypes
547 (+ ExistentialQuantification) suggests it.
548
549 Things become more complicated when GADT syntax enters the picture. Consider
550 this example:
551
552 data X a where
553 MkX :: forall b a. b -> Proxy a -> X a
554
555 If we adopt the earlier approach of quantifying all the universal variables
556 followed by all the existential ones, GHC would come up with this type
557 signature for MkX:
558
559 MkX :: forall {k} (a :: k) (b :: *). b -> Proxy a -> X a
560
561 But this is not what we want at all! After all, if a user were to use
562 TypeApplications on MkX, they would expect to instantiate `b` before `a`,
563 as that's the order in which they were written in the `forall`. (See #11721.)
564 Instead, we'd like GHC to come up with this type signature:
565
566 MkX :: forall {k} (b :: *) (a :: k). b -> Proxy a -> X a
567
568 In fact, even if we left off the explicit forall:
569
570 data X a where
571 MkX :: b -> Proxy a -> X a
572
573 Then a user should still expect `b` to be quantified before `a`, since
574 according to the rules of TypeApplications, in the absence of `forall` GHC
575 performs a stable topological sort on the type variables in the user-written
576 type signature, which would place `b` before `a`.
577
578 But as noted above, enacting this behavior is not entirely trivial, as System
579 FC demands the variables go in universal-then-existential order under the hood.
580 Our solution is thus to equip DataCon with two different sets of type
581 variables:
582
583 * dcUnivTyVars and dcExTyCoVars, for the universal type variable and existential
584 type/coercion variables, respectively. Their order is irrelevant for the
585 purposes of TypeApplications, and as a consequence, they do not come equipped
586 with visibilities (that is, they are TyVars/TyCoVars instead of
587 TyCoVarBinders).
588
589 * dcUserTyVarBinders, for the type variables binders in the order in which they
590 originally arose in the user-written type signature. Their order *does* matter
591 for TypeApplications, so they are full TyVarBinders, complete with
592 visibilities.
593
594 This encoding has some redundancy. The set of tyvars in dcUserTyVarBinders
595 consists precisely of:
596
597 * The set of tyvars in dcUnivTyVars whose type variables do not appear in
598 dcEqSpec, unioned with:
599 * The set of tyvars (*not* covars) in dcExTyCoVars
600 No covars here because because they're not user-written
601
602 The word "set" is used above because the order in which the tyvars appear in
603 dcUserTyVarBinders can be completely different from the order in dcUnivTyVars or
604 dcExTyCoVars. That is, the tyvars in dcUserTyVarBinders are a permutation of
605 (tyvars of dcExTyCoVars + a subset of dcUnivTyVars). But aside from the
606 ordering, they in fact share the same type variables (with the same Uniques). We
607 sometimes refer to this as "the dcUserTyVarBinders invariant".
608
609 dcUserTyVarBinders, as the name suggests, is the one that users will
610 see most of the time. It's used when computing the type signature of a
611 data constructor wrapper (see dataConWrapperType), and as a result,
612 it's what matters from a TypeApplications perspective.
613
614 Note [The dcEqSpec domain invariant]
615 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
616 Consider this example of a GADT constructor:
617
618 data Y a where
619 MkY :: Bool -> Y Bool
620
621 The user-written type of MkY is `Bool -> Y Bool`, but what is the underlying
622 Core type for MkY? There are two conceivable possibilities:
623
624 1. MkY :: forall a. (a ~# Bool) => Bool -> Y a
625 2. MkY :: forall a. (a ~# Bool) => a -> Y a
626
627 In practice, GHC picks (1) as the Core type for MkY. This is because we
628 maintain an invariant that the type variables in the domain of dcEqSpec will
629 only ever appear in the dcUnivTyVars. As a consequence, the type variables in
630 the domain of dcEqSpec will /never/ appear in the dcExTyCoVars, dcOtherTheta,
631 dcOrigArgTys, or dcOrigResTy; these can only ever mention variables from
632 dcUserTyVarBinders, which excludes things in the domain of dcEqSpec.
633 (See Note [DataCon user type variable binders].) This explains why GHC would
634 not pick (2) as the Core type, since the argument type `a` mentions a type
635 variable in the dcEqSpec.
636
637 There are certain parts of the codebase where it is convenient to apply the
638 substitution arising from the dcEqSpec to the dcUnivTyVars in order to obtain
639 the user-written return type of a GADT constructor. A consequence of the
640 dcEqSpec domain invariant is that you /never/ need to apply the substitution
641 to any other part of the constructor type, as they don't require it.
642 -}
643
644 -- | Data Constructor Representation
645 -- See Note [Data constructor workers and wrappers]
646 data DataConRep
647 = -- NoDataConRep means that the data con has no wrapper
648 NoDataConRep
649
650 -- DCR means that the data con has a wrapper
651 | DCR { dcr_wrap_id :: Id -- Takes src args, unboxes/flattens,
652 -- and constructs the representation
653
654 , dcr_boxer :: DataConBoxer
655
656 , dcr_arg_tys :: [Scaled Type] -- Final, representation argument types,
657 -- after unboxing and flattening,
658 -- and *including* all evidence args
659
660 , dcr_stricts :: [StrictnessMark] -- 1-1 with dcr_arg_tys
661 -- See also Note [Data-con worker strictness]
662
663 , dcr_bangs :: [HsImplBang] -- The actual decisions made (including failures)
664 -- about the original arguments; 1-1 with orig_arg_tys
665 -- See Note [Bangs on data constructor arguments]
666
667 }
668
669 -------------------------
670
671 -- | Haskell Source Bang
672 --
673 -- Bangs on data constructor arguments as the user wrote them in the
674 -- source code.
675 --
676 -- @(HsSrcBang _ SrcUnpack SrcLazy)@ and
677 -- @(HsSrcBang _ SrcUnpack NoSrcStrict)@ (without StrictData) makes no sense, we
678 -- emit a warning (in checkValidDataCon) and treat it like
679 -- @(HsSrcBang _ NoSrcUnpack SrcLazy)@
680 data HsSrcBang =
681 HsSrcBang SourceText -- Note [Pragma source text] in GHC.Types.SourceText
682 SrcUnpackedness
683 SrcStrictness
684 deriving Data.Data
685
686 -- | Haskell Implementation Bang
687 --
688 -- Bangs of data constructor arguments as generated by the compiler
689 -- after consulting HsSrcBang, flags, etc.
690 data HsImplBang
691 = HsLazy -- ^ Lazy field, or one with an unlifted type
692 | HsStrict -- ^ Strict but not unpacked field
693 | HsUnpack (Maybe Coercion)
694 -- ^ Strict and unpacked field
695 -- co :: arg-ty ~ product-ty HsBang
696 deriving Data.Data
697
698 -- | Source Strictness
699 --
700 -- What strictness annotation the user wrote
701 data SrcStrictness = SrcLazy -- ^ Lazy, ie '~'
702 | SrcStrict -- ^ Strict, ie '!'
703 | NoSrcStrict -- ^ no strictness annotation
704 deriving (Eq, Data.Data)
705
706 -- | Source Unpackedness
707 --
708 -- What unpackedness the user requested
709 data SrcUnpackedness = SrcUnpack -- ^ {-# UNPACK #-} specified
710 | SrcNoUnpack -- ^ {-# NOUNPACK #-} specified
711 | NoSrcUnpack -- ^ no unpack pragma
712 deriving (Eq, Data.Data)
713
714
715
716 -------------------------
717 -- StrictnessMark is internal only, used to indicate strictness
718 -- of the DataCon *worker* fields
719 data StrictnessMark = MarkedStrict | NotMarkedStrict
720
721 -- | An 'EqSpec' is a tyvar/type pair representing an equality made in
722 -- rejigging a GADT constructor
723 data EqSpec = EqSpec TyVar
724 Type
725
726 -- | Make a non-dependent 'EqSpec'
727 mkEqSpec :: TyVar -> Type -> EqSpec
728 mkEqSpec tv ty = EqSpec tv ty
729
730 eqSpecTyVar :: EqSpec -> TyVar
731 eqSpecTyVar (EqSpec tv _) = tv
732
733 eqSpecType :: EqSpec -> Type
734 eqSpecType (EqSpec _ ty) = ty
735
736 eqSpecPair :: EqSpec -> (TyVar, Type)
737 eqSpecPair (EqSpec tv ty) = (tv, ty)
738
739 eqSpecPreds :: [EqSpec] -> ThetaType
740 eqSpecPreds spec = [ mkPrimEqPred (mkTyVarTy tv) ty
741 | EqSpec tv ty <- spec ]
742
743 -- | Substitute in an 'EqSpec'. Precondition: if the LHS of the EqSpec
744 -- is mapped in the substitution, it is mapped to a type variable, not
745 -- a full type.
746 substEqSpec :: TCvSubst -> EqSpec -> EqSpec
747 substEqSpec subst (EqSpec tv ty)
748 = EqSpec tv' (substTy subst ty)
749 where
750 tv' = getTyVar "substEqSpec" (substTyVar subst tv)
751
752 -- | Filter out any 'TyVar's mentioned in an 'EqSpec'.
753 filterEqSpec :: [EqSpec] -> [TyVar] -> [TyVar]
754 filterEqSpec eq_spec
755 = filter not_in_eq_spec
756 where
757 not_in_eq_spec var = all (not . (== var) . eqSpecTyVar) eq_spec
758
759 instance Outputable EqSpec where
760 ppr (EqSpec tv ty) = ppr (tv, ty)
761
762 {- Note [Data-con worker strictness]
763 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
764 Notice that we do *not* say the worker Id is strict even if the data
765 constructor is declared strict
766 e.g. data T = MkT !(Int,Int)
767 Why? Because the *wrapper* $WMkT is strict (and its unfolding has case
768 expressions that do the evals) but the *worker* MkT itself is not. If we
769 pretend it is strict then when we see
770 case x of y -> MkT y
771 the simplifier thinks that y is "sure to be evaluated" (because the worker MkT
772 is strict) and drops the case. No, the workerId MkT is not strict.
773
774 However, the worker does have StrictnessMarks. When the simplifier sees a
775 pattern
776 case e of MkT x -> ...
777 it uses the dataConRepStrictness of MkT to mark x as evaluated; but that's
778 fine... dataConRepStrictness comes from the data con not from the worker Id.
779
780 Note [Bangs on data constructor arguments]
781 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
782 Consider
783 data T = MkT !Int {-# UNPACK #-} !Int Bool
784
785 When compiling the module, GHC will decide how to represent
786 MkT, depending on the optimisation level, and settings of
787 flags like -funbox-small-strict-fields.
788
789 Terminology:
790 * HsSrcBang: What the user wrote
791 Constructors: HsSrcBang
792
793 * HsImplBang: What GHC decided
794 Constructors: HsLazy, HsStrict, HsUnpack
795
796 * If T was defined in this module, MkT's dcSrcBangs field
797 records the [HsSrcBang] of what the user wrote; in the example
798 [ HsSrcBang _ NoSrcUnpack SrcStrict
799 , HsSrcBang _ SrcUnpack SrcStrict
800 , HsSrcBang _ NoSrcUnpack NoSrcStrictness]
801
802 * However, if T was defined in an imported module, the importing module
803 must follow the decisions made in the original module, regardless of
804 the flag settings in the importing module.
805 Also see Note [Bangs on imported data constructors] in GHC.Types.Id.Make
806
807 * The dcr_bangs field of the dcRep field records the [HsImplBang]
808 If T was defined in this module, Without -O the dcr_bangs might be
809 [HsStrict, HsStrict, HsLazy]
810 With -O it might be
811 [HsStrict, HsUnpack _, HsLazy]
812 With -funbox-small-strict-fields it might be
813 [HsUnpack, HsUnpack _, HsLazy]
814 With -XStrictData it might be
815 [HsStrict, HsUnpack _, HsStrict]
816
817 Note [Data con representation]
818 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
819 The dcRepType field contains the type of the representation of a constructor
820 This may differ from the type of the constructor *Id* (built
821 by MkId.mkDataConId) for two reasons:
822 a) the constructor Id may be overloaded, but the dictionary isn't stored
823 e.g. data Eq a => T a = MkT a a
824
825 b) the constructor may store an unboxed version of a strict field.
826
827 So whenever this module talks about the representation of a data constructor
828 what it means is the DataCon with all Unpacking having been applied.
829 We can think of this as the Core representation.
830
831 Here's an example illustrating the Core representation:
832 data Ord a => T a = MkT Int! a Void#
833 Here
834 T :: Ord a => Int -> a -> Void# -> T a
835 but the rep type is
836 Trep :: Int# -> a -> Void# -> T a
837 Actually, the unboxed part isn't implemented yet!
838
839 Not that this representation is still *different* from runtime
840 representation. (Which is what STG uses afer unarise).
841
842 This is how T would end up being used in STG post-unarise:
843
844 let x = T 1# y
845 in ...
846 case x of
847 T int a -> ...
848
849 The Void# argument is dropped and the boxed int is replaced by an unboxed
850 one. In essence we only generate binders for runtime relevant values.
851
852 We also flatten out unboxed tuples in this process. See the unarise
853 pass for details on how this is done. But as an example consider
854 `data S = MkS Bool (# Bool | Char #)` which when matched on would
855 result in an alternative with three binders like this
856
857 MkS bool tag tpl_field ->
858
859 See Note [Translating unboxed sums to unboxed tuples] and Note [Unarisation]
860 for the details of this transformation.
861
862
863 ************************************************************************
864 * *
865 \subsection{Instances}
866 * *
867 ************************************************************************
868 -}
869
870 instance Eq DataCon where
871 a == b = getUnique a == getUnique b
872 a /= b = getUnique a /= getUnique b
873
874 instance Uniquable DataCon where
875 getUnique = dcUnique
876
877 instance NamedThing DataCon where
878 getName = dcName
879
880 instance Outputable DataCon where
881 ppr con = ppr (dataConName con)
882
883 instance OutputableBndr DataCon where
884 pprInfixOcc con = pprInfixName (dataConName con)
885 pprPrefixOcc con = pprPrefixName (dataConName con)
886
887 instance Data.Data DataCon where
888 -- don't traverse?
889 toConstr _ = abstractConstr "DataCon"
890 gunfold _ _ = error "gunfold"
891 dataTypeOf _ = mkNoRepType "DataCon"
892
893 instance Outputable HsSrcBang where
894 ppr (HsSrcBang _ prag mark) = ppr prag <+> ppr mark
895
896 instance Outputable HsImplBang where
897 ppr HsLazy = text "Lazy"
898 ppr (HsUnpack Nothing) = text "Unpacked"
899 ppr (HsUnpack (Just co)) = text "Unpacked" <> parens (ppr co)
900 ppr HsStrict = text "StrictNotUnpacked"
901
902 instance Outputable SrcStrictness where
903 ppr SrcLazy = char '~'
904 ppr SrcStrict = char '!'
905 ppr NoSrcStrict = empty
906
907 instance Outputable SrcUnpackedness where
908 ppr SrcUnpack = text "{-# UNPACK #-}"
909 ppr SrcNoUnpack = text "{-# NOUNPACK #-}"
910 ppr NoSrcUnpack = empty
911
912 instance Outputable StrictnessMark where
913 ppr MarkedStrict = text "!"
914 ppr NotMarkedStrict = empty
915
916 instance Binary SrcStrictness where
917 put_ bh SrcLazy = putByte bh 0
918 put_ bh SrcStrict = putByte bh 1
919 put_ bh NoSrcStrict = putByte bh 2
920
921 get bh =
922 do h <- getByte bh
923 case h of
924 0 -> return SrcLazy
925 1 -> return SrcStrict
926 _ -> return NoSrcStrict
927
928 instance Binary SrcUnpackedness where
929 put_ bh SrcNoUnpack = putByte bh 0
930 put_ bh SrcUnpack = putByte bh 1
931 put_ bh NoSrcUnpack = putByte bh 2
932
933 get bh =
934 do h <- getByte bh
935 case h of
936 0 -> return SrcNoUnpack
937 1 -> return SrcUnpack
938 _ -> return NoSrcUnpack
939
940 -- | Compare strictness annotations
941 eqHsBang :: HsImplBang -> HsImplBang -> Bool
942 eqHsBang HsLazy HsLazy = True
943 eqHsBang HsStrict HsStrict = True
944 eqHsBang (HsUnpack Nothing) (HsUnpack Nothing) = True
945 eqHsBang (HsUnpack (Just c1)) (HsUnpack (Just c2))
946 = eqType (coercionType c1) (coercionType c2)
947 eqHsBang _ _ = False
948
949 isBanged :: HsImplBang -> Bool
950 isBanged (HsUnpack {}) = True
951 isBanged (HsStrict {}) = True
952 isBanged HsLazy = False
953
954 isSrcStrict :: SrcStrictness -> Bool
955 isSrcStrict SrcStrict = True
956 isSrcStrict _ = False
957
958 isSrcUnpacked :: SrcUnpackedness -> Bool
959 isSrcUnpacked SrcUnpack = True
960 isSrcUnpacked _ = False
961
962 isMarkedStrict :: StrictnessMark -> Bool
963 isMarkedStrict NotMarkedStrict = False
964 isMarkedStrict _ = True -- All others are strict
965
966 {- *********************************************************************
967 * *
968 \subsection{Construction}
969 * *
970 ********************************************************************* -}
971
972 -- | Build a new data constructor
973 mkDataCon :: Name
974 -> Bool -- ^ Is the constructor declared infix?
975 -> TyConRepName -- ^ TyConRepName for the promoted TyCon
976 -> [HsSrcBang] -- ^ Strictness/unpack annotations, from user
977 -> [FieldLabel] -- ^ Field labels for the constructor,
978 -- if it is a record, otherwise empty
979 -> [TyVar] -- ^ Universals.
980 -> [TyCoVar] -- ^ Existentials.
981 -> [InvisTVBinder] -- ^ User-written 'TyVarBinder's.
982 -- These must be Inferred/Specified.
983 -- See @Note [TyVarBinders in DataCons]@
984 -> [EqSpec] -- ^ GADT equalities
985 -> KnotTied ThetaType -- ^ Theta-type occurring before the arguments proper
986 -> [KnotTied (Scaled Type)] -- ^ Original argument types
987 -> KnotTied Type -- ^ Original result type
988 -> RuntimeRepInfo -- ^ See comments on 'GHC.Core.TyCon.RuntimeRepInfo'
989 -> KnotTied TyCon -- ^ Representation type constructor
990 -> ConTag -- ^ Constructor tag
991 -> ThetaType -- ^ The "stupid theta", context of the data
992 -- declaration e.g. @data Eq a => T a ...@
993 -> Id -- ^ Worker Id
994 -> DataConRep -- ^ Representation
995 -> DataCon
996 -- Can get the tag from the TyCon
997
998 mkDataCon name declared_infix prom_info
999 arg_stricts -- Must match orig_arg_tys 1-1
1000 fields
1001 univ_tvs ex_tvs user_tvbs
1002 eq_spec theta
1003 orig_arg_tys orig_res_ty rep_info rep_tycon tag
1004 stupid_theta work_id rep
1005 -- Warning: mkDataCon is not a good place to check certain invariants.
1006 -- If the programmer writes the wrong result type in the decl, thus:
1007 -- data T a where { MkT :: S }
1008 -- then it's possible that the univ_tvs may hit an assertion failure
1009 -- if you pull on univ_tvs. This case is checked by checkValidDataCon,
1010 -- so the error is detected properly... it's just that assertions here
1011 -- are a little dodgy.
1012
1013 = con
1014 where
1015 is_vanilla = null ex_tvs && null eq_spec && null theta
1016
1017 con = MkData {dcName = name, dcUnique = nameUnique name,
1018 dcVanilla = is_vanilla, dcInfix = declared_infix,
1019 dcUnivTyVars = univ_tvs,
1020 dcExTyCoVars = ex_tvs,
1021 dcUserTyVarBinders = user_tvbs,
1022 dcEqSpec = eq_spec,
1023 dcOtherTheta = theta,
1024 dcStupidTheta = stupid_theta,
1025 dcOrigArgTys = orig_arg_tys, dcOrigResTy = orig_res_ty,
1026 dcRepTyCon = rep_tycon,
1027 dcSrcBangs = arg_stricts,
1028 dcFields = fields, dcTag = tag, dcRepType = rep_ty,
1029 dcWorkId = work_id,
1030 dcRep = rep,
1031 dcSourceArity = length orig_arg_tys,
1032 dcRepArity = length rep_arg_tys + count isCoVar ex_tvs,
1033 dcPromoted = promoted }
1034
1035 -- The 'arg_stricts' passed to mkDataCon are simply those for the
1036 -- source-language arguments. We add extra ones for the
1037 -- dictionary arguments right here.
1038
1039 rep_arg_tys = dataConRepArgTys con
1040
1041 rep_ty =
1042 case rep of
1043 -- If the DataCon has no wrapper, then the worker's type *is* the
1044 -- user-facing type, so we can simply use dataConWrapperType.
1045 NoDataConRep -> dataConWrapperType con
1046 -- If the DataCon has a wrapper, then the worker's type is never seen
1047 -- by the user. The visibilities we pick do not matter here.
1048 DCR{} -> mkInfForAllTys univ_tvs $ mkTyCoInvForAllTys ex_tvs $
1049 mkVisFunTys rep_arg_tys $
1050 mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
1051
1052 -- See Note [Promoted data constructors] in GHC.Core.TyCon
1053 prom_tv_bndrs = [ mkNamedTyConBinder (Invisible spec) tv
1054 | Bndr tv spec <- user_tvbs ]
1055
1056 fresh_names = freshNames (map getName user_tvbs)
1057 -- fresh_names: make sure that the "anonymous" tyvars don't
1058 -- clash in name or unique with the universal/existential ones.
1059 -- Tiresome! And unnecessary because these tyvars are never looked at
1060 prom_theta_bndrs = [ mkAnonTyConBinder InvisArg (mkTyVar n t)
1061 {- Invisible -} | (n,t) <- fresh_names `zip` theta ]
1062 prom_arg_bndrs = [ mkAnonTyConBinder VisArg (mkTyVar n t)
1063 {- Visible -} | (n,t) <- dropList theta fresh_names `zip` map scaledThing orig_arg_tys ]
1064 prom_bndrs = prom_tv_bndrs ++ prom_theta_bndrs ++ prom_arg_bndrs
1065 prom_res_kind = orig_res_ty
1066 promoted = mkPromotedDataCon con name prom_info prom_bndrs
1067 prom_res_kind roles rep_info
1068
1069 roles = map (\tv -> if isTyVar tv then Nominal else Phantom)
1070 (univ_tvs ++ ex_tvs)
1071 ++ map (const Representational) (theta ++ map scaledThing orig_arg_tys)
1072
1073 freshNames :: [Name] -> [Name]
1074 -- Make an infinite list of Names whose Uniques and OccNames
1075 -- differ from those in the 'avoid' list
1076 freshNames avoids
1077 = [ mkSystemName uniq occ
1078 | n <- [0..]
1079 , let uniq = mkAlphaTyVarUnique n
1080 occ = mkTyVarOccFS (mkFastString ('x' : show n))
1081
1082 , not (uniq `elementOfUniqSet` avoid_uniqs)
1083 , not (occ `elemOccSet` avoid_occs) ]
1084
1085 where
1086 avoid_uniqs :: UniqSet Unique
1087 avoid_uniqs = mkUniqSet (map getUnique avoids)
1088
1089 avoid_occs :: OccSet
1090 avoid_occs = mkOccSet (map getOccName avoids)
1091
1092 -- | The 'Name' of the 'DataCon', giving it a unique, rooted identification
1093 dataConName :: DataCon -> Name
1094 dataConName = dcName
1095
1096 -- | The tag used for ordering 'DataCon's
1097 dataConTag :: DataCon -> ConTag
1098 dataConTag = dcTag
1099
1100 dataConTagZ :: DataCon -> ConTagZ
1101 dataConTagZ con = dataConTag con - fIRST_TAG
1102
1103 -- | The type constructor that we are building via this data constructor
1104 dataConTyCon :: DataCon -> TyCon
1105 dataConTyCon = dcRepTyCon
1106
1107 -- | The original type constructor used in the definition of this data
1108 -- constructor. In case of a data family instance, that will be the family
1109 -- type constructor.
1110 dataConOrigTyCon :: DataCon -> TyCon
1111 dataConOrigTyCon dc
1112 | Just (tc, _) <- tyConFamInst_maybe (dcRepTyCon dc) = tc
1113 | otherwise = dcRepTyCon dc
1114
1115 -- | The representation type of the data constructor, i.e. the sort
1116 -- type that will represent values of this type at runtime
1117 dataConRepType :: DataCon -> Type
1118 dataConRepType = dcRepType
1119
1120 -- | Should the 'DataCon' be presented infix?
1121 dataConIsInfix :: DataCon -> Bool
1122 dataConIsInfix = dcInfix
1123
1124 -- | The universally-quantified type variables of the constructor
1125 dataConUnivTyVars :: DataCon -> [TyVar]
1126 dataConUnivTyVars (MkData { dcUnivTyVars = tvbs }) = tvbs
1127
1128 -- | The existentially-quantified type/coercion variables of the constructor
1129 -- including dependent (kind-) GADT equalities
1130 dataConExTyCoVars :: DataCon -> [TyCoVar]
1131 dataConExTyCoVars (MkData { dcExTyCoVars = tvbs }) = tvbs
1132
1133 -- | Both the universal and existential type/coercion variables of the constructor
1134 dataConUnivAndExTyCoVars :: DataCon -> [TyCoVar]
1135 dataConUnivAndExTyCoVars (MkData { dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tvs })
1136 = univ_tvs ++ ex_tvs
1137
1138 -- See Note [DataCon user type variable binders]
1139 -- | The type variables of the constructor, in the order the user wrote them
1140 dataConUserTyVars :: DataCon -> [TyVar]
1141 dataConUserTyVars (MkData { dcUserTyVarBinders = tvbs }) = binderVars tvbs
1142
1143 -- See Note [DataCon user type variable binders]
1144 -- | 'InvisTVBinder's for the type variables of the constructor, in the order the
1145 -- user wrote them
1146 dataConUserTyVarBinders :: DataCon -> [InvisTVBinder]
1147 dataConUserTyVarBinders = dcUserTyVarBinders
1148
1149 -- | Equalities derived from the result type of the data constructor, as written
1150 -- by the programmer in any GADT declaration. This includes *all* GADT-like
1151 -- equalities, including those written in by hand by the programmer.
1152 dataConEqSpec :: DataCon -> [EqSpec]
1153 dataConEqSpec con@(MkData { dcEqSpec = eq_spec, dcOtherTheta = theta })
1154 = dataConKindEqSpec con
1155 ++ eq_spec ++
1156 [ spec -- heterogeneous equality
1157 | Just (tc, [_k1, _k2, ty1, ty2]) <- map splitTyConApp_maybe theta
1158 , tc `hasKey` heqTyConKey
1159 , spec <- case (getTyVar_maybe ty1, getTyVar_maybe ty2) of
1160 (Just tv1, _) -> [mkEqSpec tv1 ty2]
1161 (_, Just tv2) -> [mkEqSpec tv2 ty1]
1162 _ -> []
1163 ] ++
1164 [ spec -- homogeneous equality
1165 | Just (tc, [_k, ty1, ty2]) <- map splitTyConApp_maybe theta
1166 , tc `hasKey` eqTyConKey
1167 , spec <- case (getTyVar_maybe ty1, getTyVar_maybe ty2) of
1168 (Just tv1, _) -> [mkEqSpec tv1 ty2]
1169 (_, Just tv2) -> [mkEqSpec tv2 ty1]
1170 _ -> []
1171 ]
1172
1173 -- | Dependent (kind-level) equalities in a constructor.
1174 -- There are extracted from the existential variables.
1175 -- See Note [Existential coercion variables]
1176 dataConKindEqSpec :: DataCon -> [EqSpec]
1177 dataConKindEqSpec (MkData {dcExTyCoVars = ex_tcvs})
1178 -- It is used in 'dataConEqSpec' (maybe also 'dataConFullSig' in the future),
1179 -- which are frequently used functions.
1180 -- For now (Aug 2018) this function always return empty set as we don't really
1181 -- have coercion variables.
1182 -- In the future when we do, we might want to cache this information in DataCon
1183 -- so it won't be computed every time when aforementioned functions are called.
1184 = [ EqSpec tv ty
1185 | cv <- ex_tcvs
1186 , isCoVar cv
1187 , let (_, _, ty1, ty, _) = coVarKindsTypesRole cv
1188 tv = getTyVar "dataConKindEqSpec" ty1
1189 ]
1190
1191 -- | The *full* constraints on the constructor type, including dependent GADT
1192 -- equalities.
1193 dataConTheta :: DataCon -> ThetaType
1194 dataConTheta con@(MkData { dcEqSpec = eq_spec, dcOtherTheta = theta })
1195 = eqSpecPreds (dataConKindEqSpec con ++ eq_spec) ++ theta
1196
1197 -- | Get the Id of the 'DataCon' worker: a function that is the "actual"
1198 -- constructor and has no top level binding in the program. The type may
1199 -- be different from the obvious one written in the source program. Panics
1200 -- if there is no such 'Id' for this 'DataCon'
1201 dataConWorkId :: DataCon -> Id
1202 dataConWorkId dc = dcWorkId dc
1203
1204 -- | Get the Id of the 'DataCon' wrapper: a function that wraps the "actual"
1205 -- constructor so it has the type visible in the source program: c.f.
1206 -- 'dataConWorkId'.
1207 -- Returns Nothing if there is no wrapper, which occurs for an algebraic data
1208 -- constructor and also for a newtype (whose constructor is inlined
1209 -- compulsorily)
1210 dataConWrapId_maybe :: DataCon -> Maybe Id
1211 dataConWrapId_maybe dc = case dcRep dc of
1212 NoDataConRep -> Nothing
1213 DCR { dcr_wrap_id = wrap_id } -> Just wrap_id
1214
1215 -- | Returns an Id which looks like the Haskell-source constructor by using
1216 -- the wrapper if it exists (see 'dataConWrapId_maybe') and failing over to
1217 -- the worker (see 'dataConWorkId')
1218 dataConWrapId :: DataCon -> Id
1219 dataConWrapId dc = case dcRep dc of
1220 NoDataConRep-> dcWorkId dc -- worker=wrapper
1221 DCR { dcr_wrap_id = wrap_id } -> wrap_id
1222
1223 -- | Find all the 'Id's implicitly brought into scope by the data constructor. Currently,
1224 -- the union of the 'dataConWorkId' and the 'dataConWrapId'
1225 dataConImplicitTyThings :: DataCon -> [TyThing]
1226 dataConImplicitTyThings (MkData { dcWorkId = work, dcRep = rep })
1227 = [mkAnId work] ++ wrap_ids
1228 where
1229 wrap_ids = case rep of
1230 NoDataConRep -> []
1231 DCR { dcr_wrap_id = wrap } -> [mkAnId wrap]
1232
1233 -- | The labels for the fields of this particular 'DataCon'
1234 dataConFieldLabels :: DataCon -> [FieldLabel]
1235 dataConFieldLabels = dcFields
1236
1237 -- | Extract the type for any given labelled field of the 'DataCon'
1238 dataConFieldType :: DataCon -> FieldLabelString -> Type
1239 dataConFieldType con label = case dataConFieldType_maybe con label of
1240 Just (_, ty) -> ty
1241 Nothing -> pprPanic "dataConFieldType" (ppr con <+> ppr label)
1242
1243 -- | Extract the label and type for any given labelled field of the
1244 -- 'DataCon', or return 'Nothing' if the field does not belong to it
1245 dataConFieldType_maybe :: DataCon -> FieldLabelString
1246 -> Maybe (FieldLabel, Type)
1247 dataConFieldType_maybe con label
1248 = find ((== label) . flLabel . fst) (dcFields con `zip` (scaledThing <$> dcOrigArgTys con))
1249
1250 -- | Strictness/unpack annotations, from user; or, for imported
1251 -- DataCons, from the interface file
1252 -- The list is in one-to-one correspondence with the arity of the 'DataCon'
1253
1254 dataConSrcBangs :: DataCon -> [HsSrcBang]
1255 dataConSrcBangs = dcSrcBangs
1256
1257 -- | Source-level arity of the data constructor
1258 dataConSourceArity :: DataCon -> Arity
1259 dataConSourceArity (MkData { dcSourceArity = arity }) = arity
1260
1261 -- | Gives the number of actual fields in the /representation/ of the
1262 -- data constructor. This may be more than appear in the source code;
1263 -- the extra ones are the existentially quantified dictionaries
1264 dataConRepArity :: DataCon -> Arity
1265 dataConRepArity (MkData { dcRepArity = arity }) = arity
1266
1267 -- | Return whether there are any argument types for this 'DataCon's original source type
1268 -- See Note [DataCon arities]
1269 isNullarySrcDataCon :: DataCon -> Bool
1270 isNullarySrcDataCon dc = dataConSourceArity dc == 0
1271
1272 -- | Return whether there are any argument types for this 'DataCon's runtime representation type
1273 -- See Note [DataCon arities]
1274 isNullaryRepDataCon :: DataCon -> Bool
1275 isNullaryRepDataCon dc = dataConRepArity dc == 0
1276
1277 dataConRepStrictness :: DataCon -> [StrictnessMark]
1278 -- ^ Give the demands on the arguments of a
1279 -- Core constructor application (Con dc args)
1280 dataConRepStrictness dc = case dcRep dc of
1281 NoDataConRep -> [NotMarkedStrict | _ <- dataConRepArgTys dc]
1282 DCR { dcr_stricts = strs } -> strs
1283
1284 dataConImplBangs :: DataCon -> [HsImplBang]
1285 -- The implementation decisions about the strictness/unpack of each
1286 -- source program argument to the data constructor
1287 dataConImplBangs dc
1288 = case dcRep dc of
1289 NoDataConRep -> replicate (dcSourceArity dc) HsLazy
1290 DCR { dcr_bangs = bangs } -> bangs
1291
1292 dataConBoxer :: DataCon -> Maybe DataConBoxer
1293 dataConBoxer (MkData { dcRep = DCR { dcr_boxer = boxer } }) = Just boxer
1294 dataConBoxer _ = Nothing
1295
1296 dataConInstSig
1297 :: DataCon
1298 -> [Type] -- Instantiate the *universal* tyvars with these types
1299 -> ([TyCoVar], ThetaType, [Type]) -- Return instantiated existentials
1300 -- theta and arg tys
1301 -- ^ Instantiate the universal tyvars of a data con,
1302 -- returning
1303 -- ( instantiated existentials
1304 -- , instantiated constraints including dependent GADT equalities
1305 -- which are *also* listed in the instantiated existentials
1306 -- , instantiated args)
1307 dataConInstSig con@(MkData { dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tvs
1308 , dcOrigArgTys = arg_tys })
1309 univ_tys
1310 = ( ex_tvs'
1311 , substTheta subst (dataConTheta con)
1312 , substTys subst (map scaledThing arg_tys))
1313 where
1314 univ_subst = zipTvSubst univ_tvs univ_tys
1315 (subst, ex_tvs') = Type.substVarBndrs univ_subst ex_tvs
1316
1317
1318 -- | The \"full signature\" of the 'DataCon' returns, in order:
1319 --
1320 -- 1) The result of 'dataConUnivTyVars'
1321 --
1322 -- 2) The result of 'dataConExTyCoVars'
1323 --
1324 -- 3) The non-dependent GADT equalities.
1325 -- Dependent GADT equalities are implied by coercion variables in
1326 -- return value (2).
1327 --
1328 -- 4) The other constraints of the data constructor type, excluding GADT
1329 -- equalities
1330 --
1331 -- 5) The original argument types to the 'DataCon' (i.e. before
1332 -- any change of the representation of the type) with linearity
1333 -- annotations
1334 --
1335 -- 6) The original result type of the 'DataCon'
1336 dataConFullSig :: DataCon
1337 -> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Scaled Type], Type)
1338 dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tvs,
1339 dcEqSpec = eq_spec, dcOtherTheta = theta,
1340 dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
1341 = (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
1342
1343 dataConOrigResTy :: DataCon -> Type
1344 dataConOrigResTy dc = dcOrigResTy dc
1345
1346 -- | The \"stupid theta\" of the 'DataCon', such as @data Eq a@ in:
1347 --
1348 -- > data Eq a => T a = ...
1349 dataConStupidTheta :: DataCon -> ThetaType
1350 dataConStupidTheta dc = dcStupidTheta dc
1351
1352 {-
1353 Note [Displaying linear fields]
1354 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1355 A constructor with a linear field can be written either as
1356 MkT :: a %1 -> T a (with -XLinearTypes)
1357 or
1358 MkT :: a -> T a (with -XNoLinearTypes)
1359
1360 There are three different methods to retrieve a type of a datacon.
1361 They differ in how linear fields are handled.
1362
1363 1. dataConWrapperType:
1364 The type of the wrapper in Core.
1365 For example, dataConWrapperType for Maybe is a %1 -> Just a.
1366
1367 2. dataConNonlinearType:
1368 The type of the constructor, with linear arrows replaced by unrestricted ones.
1369 Used when we don't want to introduce linear types to user (in holes
1370 and in types in hie used by haddock).
1371
1372 3. dataConDisplayType (takes a boolean indicating if -XLinearTypes is enabled):
1373 The type we'd like to show in error messages, :info and -ddump-types.
1374 Ideally, it should reflect the type written by the user;
1375 the function returns a type with arrows that would be required
1376 to write this constructor under the current setting of -XLinearTypes.
1377 In principle, this type can be different from the user's source code
1378 when the value of -XLinearTypes has changed, but we don't
1379 expect this to cause much trouble.
1380
1381 Due to internal plumbing in checkValidDataCon, we can't just return a Doc.
1382 The multiplicity of arrows returned by dataConDisplayType and
1383 dataConDisplayType is used only for pretty-printing.
1384 -}
1385
1386 dataConWrapperType :: DataCon -> Type
1387 -- ^ The user-declared type of the data constructor
1388 -- in the nice-to-read form:
1389 --
1390 -- > T :: forall a b. a -> b -> T [a]
1391 --
1392 -- rather than:
1393 --
1394 -- > T :: forall a c. forall b. (c~[a]) => a -> b -> T c
1395 --
1396 -- The type variables are quantified in the order that the user wrote them.
1397 -- See @Note [DataCon user type variable binders]@.
1398 --
1399 -- NB: If the constructor is part of a data instance, the result type
1400 -- mentions the family tycon, not the internal one.
1401 dataConWrapperType (MkData { dcUserTyVarBinders = user_tvbs,
1402 dcOtherTheta = theta, dcOrigArgTys = arg_tys,
1403 dcOrigResTy = res_ty })
1404 = mkInvisForAllTys user_tvbs $
1405 mkInvisFunTysMany theta $
1406 mkVisFunTys arg_tys $
1407 res_ty
1408
1409 dataConNonlinearType :: DataCon -> Type
1410 dataConNonlinearType (MkData { dcUserTyVarBinders = user_tvbs,
1411 dcOtherTheta = theta, dcOrigArgTys = arg_tys,
1412 dcOrigResTy = res_ty })
1413 = let arg_tys' = map (\(Scaled w t) -> Scaled (case w of One -> Many; _ -> w) t) arg_tys
1414 in mkInvisForAllTys user_tvbs $
1415 mkInvisFunTysMany theta $
1416 mkVisFunTys arg_tys' $
1417 res_ty
1418
1419 dataConDisplayType :: Bool -> DataCon -> Type
1420 dataConDisplayType show_linear_types dc
1421 = if show_linear_types
1422 then dataConWrapperType dc
1423 else dataConNonlinearType dc
1424
1425 -- | Finds the instantiated types of the arguments required to construct a
1426 -- 'DataCon' representation
1427 -- NB: these INCLUDE any dictionary args
1428 -- but EXCLUDE the data-declaration context, which is discarded
1429 -- It's all post-flattening etc; this is a representation type
1430 dataConInstArgTys :: DataCon -- ^ A datacon with no existentials or equality constraints
1431 -- However, it can have a dcTheta (notably it can be a
1432 -- class dictionary, with superclasses)
1433 -> [Type] -- ^ Instantiated at these types
1434 -> [Scaled Type]
1435 dataConInstArgTys dc@(MkData {dcUnivTyVars = univ_tvs,
1436 dcExTyCoVars = ex_tvs}) inst_tys
1437 = assertPpr (univ_tvs `equalLength` inst_tys)
1438 (text "dataConInstArgTys" <+> ppr dc $$ ppr univ_tvs $$ ppr inst_tys) $
1439 assertPpr (null ex_tvs) (ppr dc) $
1440 map (mapScaledType (substTyWith univ_tvs inst_tys)) (dataConRepArgTys dc)
1441
1442 -- | Returns just the instantiated /value/ argument types of a 'DataCon',
1443 -- (excluding dictionary args)
1444 dataConInstOrigArgTys
1445 :: DataCon -- Works for any DataCon
1446 -> [Type] -- Includes existential tyvar args, but NOT
1447 -- equality constraints or dicts
1448 -> [Scaled Type]
1449 -- For vanilla datacons, it's all quite straightforward
1450 -- But for the call in GHC.HsToCore.Match.Constructor, we really do want just
1451 -- the value args
1452 dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys,
1453 dcUnivTyVars = univ_tvs,
1454 dcExTyCoVars = ex_tvs}) inst_tys
1455 = assertPpr (tyvars `equalLength` inst_tys)
1456 (text "dataConInstOrigArgTys" <+> ppr dc $$ ppr tyvars $$ ppr inst_tys) $
1457 substScaledTys subst arg_tys
1458 where
1459 tyvars = univ_tvs ++ ex_tvs
1460 subst = zipTCvSubst tyvars inst_tys
1461
1462 -- | Returns the argument types of the wrapper, excluding all dictionary arguments
1463 -- and without substituting for any type variables
1464 dataConOrigArgTys :: DataCon -> [Scaled Type]
1465 dataConOrigArgTys dc = dcOrigArgTys dc
1466
1467 -- | Returns constraints in the wrapper type, other than those in the dataConEqSpec
1468 dataConOtherTheta :: DataCon -> ThetaType
1469 dataConOtherTheta dc = dcOtherTheta dc
1470
1471 -- | Returns the arg types of the worker, including *all* non-dependent
1472 -- evidence, after any flattening has been done and without substituting for
1473 -- any type variables
1474 dataConRepArgTys :: DataCon -> [Scaled Type]
1475 dataConRepArgTys (MkData { dcRep = rep
1476 , dcEqSpec = eq_spec
1477 , dcOtherTheta = theta
1478 , dcOrigArgTys = orig_arg_tys })
1479 = case rep of
1480 NoDataConRep -> assert (null eq_spec) $ (map unrestricted theta) ++ orig_arg_tys
1481 DCR { dcr_arg_tys = arg_tys } -> arg_tys
1482
1483 -- | The string @package:module.name@ identifying a constructor, which is attached
1484 -- to its info table and used by the GHCi debugger and the heap profiler
1485 dataConIdentity :: DataCon -> ByteString
1486 -- We want this string to be UTF-8, so we get the bytes directly from the FastStrings.
1487 dataConIdentity dc = LBS.toStrict $ BSB.toLazyByteString $ mconcat
1488 [ BSB.shortByteString $ fastStringToShortByteString $
1489 unitFS $ moduleUnit mod
1490 , BSB.int8 $ fromIntegral (ord ':')
1491 , BSB.shortByteString $ fastStringToShortByteString $
1492 moduleNameFS $ moduleName mod
1493 , BSB.int8 $ fromIntegral (ord '.')
1494 , BSB.shortByteString $ fastStringToShortByteString $
1495 occNameFS $ nameOccName name
1496 ]
1497 where name = dataConName dc
1498 mod = assert (isExternalName name) $ nameModule name
1499
1500 isTupleDataCon :: DataCon -> Bool
1501 isTupleDataCon (MkData {dcRepTyCon = tc}) = isTupleTyCon tc
1502
1503 isBoxedTupleDataCon :: DataCon -> Bool
1504 isBoxedTupleDataCon (MkData {dcRepTyCon = tc}) = isBoxedTupleTyCon tc
1505
1506 isUnboxedTupleDataCon :: DataCon -> Bool
1507 isUnboxedTupleDataCon (MkData {dcRepTyCon = tc}) = isUnboxedTupleTyCon tc
1508
1509 isUnboxedSumDataCon :: DataCon -> Bool
1510 isUnboxedSumDataCon (MkData {dcRepTyCon = tc}) = isUnboxedSumTyCon tc
1511
1512 -- | Vanilla 'DataCon's are those that are nice boring Haskell 98 constructors
1513 isVanillaDataCon :: DataCon -> Bool
1514 isVanillaDataCon dc = dcVanilla dc
1515
1516 -- | Is this the 'DataCon' of a newtype?
1517 isNewDataCon :: DataCon -> Bool
1518 isNewDataCon dc = isNewTyCon (dataConTyCon dc)
1519
1520 -- | Should this DataCon be allowed in a type even without -XDataKinds?
1521 -- Currently, only Lifted & Unlifted
1522 specialPromotedDc :: DataCon -> Bool
1523 specialPromotedDc = isKindTyCon . dataConTyCon
1524
1525 classDataCon :: Class -> DataCon
1526 classDataCon clas = case tyConDataCons (classTyCon clas) of
1527 (dict_constr:no_more) -> assert (null no_more) dict_constr
1528 [] -> panic "classDataCon"
1529
1530 dataConCannotMatch :: [Type] -> DataCon -> Bool
1531 -- Returns True iff the data con *definitely cannot* match a
1532 -- scrutinee of type (T tys)
1533 -- where T is the dcRepTyCon for the data con
1534 dataConCannotMatch tys con
1535 -- See (U6) in Note [Implementing unsafeCoerce]
1536 -- in base:Unsafe.Coerce
1537 | dataConName con == unsafeReflDataConName
1538 = False
1539 | null inst_theta = False -- Common
1540 | all isTyVarTy tys = False -- Also common
1541 | otherwise = typesCantMatch (concatMap predEqs inst_theta)
1542 where
1543 (_, inst_theta, _) = dataConInstSig con tys
1544
1545 -- TODO: could gather equalities from superclasses too
1546 predEqs pred = case classifyPredType pred of
1547 EqPred NomEq ty1 ty2 -> [(ty1, ty2)]
1548 ClassPred eq args
1549 | eq `hasKey` eqTyConKey
1550 , [_, ty1, ty2] <- args -> [(ty1, ty2)]
1551 | eq `hasKey` heqTyConKey
1552 , [_, _, ty1, ty2] <- args -> [(ty1, ty2)]
1553 _ -> []
1554
1555 -- | Were the type variables of the data con written in a different order
1556 -- than the regular order (universal tyvars followed by existential tyvars)?
1557 --
1558 -- This is not a cheap test, so we minimize its use in GHC as much as possible.
1559 -- Currently, its only call site in the GHC codebase is in 'mkDataConRep' in
1560 -- "MkId", and so 'dataConUserTyVarsArePermuted' is only called at most once
1561 -- during a data constructor's lifetime.
1562
1563 -- See Note [DataCon user type variable binders], as well as
1564 -- Note [Data con wrappers and GADT syntax] for an explanation of what
1565 -- mkDataConRep is doing with this function.
1566 dataConUserTyVarsArePermuted :: DataCon -> Bool
1567 dataConUserTyVarsArePermuted (MkData { dcUnivTyVars = univ_tvs
1568 , dcExTyCoVars = ex_tvs, dcEqSpec = eq_spec
1569 , dcUserTyVarBinders = user_tvbs }) =
1570 (filterEqSpec eq_spec univ_tvs ++ ex_tvs) /= binderVars user_tvbs
1571
1572 {-
1573 %************************************************************************
1574 %* *
1575 Promoting of data types to the kind level
1576 * *
1577 ************************************************************************
1578
1579 -}
1580
1581 promoteDataCon :: DataCon -> TyCon
1582 promoteDataCon (MkData { dcPromoted = tc }) = tc
1583
1584 {-
1585 ************************************************************************
1586 * *
1587 \subsection{Splitting products}
1588 * *
1589 ************************************************************************
1590 -}
1591
1592 -- | Extract the type constructor, type argument, data constructor and it's
1593 -- /representation/ argument types from a type if it is a product type.
1594 --
1595 -- Precisely, we return @Just@ for any data type that is all of:
1596 --
1597 -- * Concrete (i.e. constructors visible)
1598 -- * Single-constructor
1599 -- * ... which has no existentials
1600 --
1601 -- Whether the type is a @data@ type or a @newtype@.
1602 splitDataProductType_maybe
1603 :: Type -- ^ A product type, perhaps
1604 -> Maybe (TyCon, -- The type constructor
1605 [Type], -- Type args of the tycon
1606 DataCon, -- The data constructor
1607 [Scaled Type]) -- Its /representation/ arg types
1608
1609 -- Rejecting existentials means we don't have to worry about
1610 -- freshening and substituting type variables
1611 -- (See "GHC.Type.Id.Make.dataConArgUnpack")
1612
1613 splitDataProductType_maybe ty
1614 | Just (tycon, ty_args) <- splitTyConApp_maybe ty
1615 , Just con <- tyConSingleDataCon_maybe tycon
1616 , null (dataConExTyCoVars con) -- no existentials! See above
1617 = Just (tycon, ty_args, con, dataConInstArgTys con ty_args)
1618 | otherwise
1619 = Nothing