summaryrefslogtreecommitdiff
path: root/compiler/basicTypes/DataCon.lhs
blob: d56aaac4ba381329071c8f7f3af47039d7aeb0d5 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1998
%
\section[DataCon]{@DataCon@: Data Constructors}

\begin{code}
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

module DataCon (
        -- * Main data types
	DataCon, DataConIds(..),
	ConTag,
	
	-- ** Type construction
	mkDataCon, fIRST_TAG,
	
	-- ** Type deconstruction
	dataConRepType, dataConSig, dataConFullSig,
	dataConName, dataConIdentity, dataConTag, dataConTyCon, 
        dataConOrigTyCon, dataConUserType,
	dataConUnivTyVars, dataConExTyVars, dataConAllTyVars, 
	dataConEqSpec, eqSpecPreds, dataConTheta,
	dataConStupidTheta,  
	dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
	dataConInstOrigArgTys, dataConRepArgTys, 
	dataConFieldLabels, dataConFieldType,
	dataConStrictMarks, dataConExStricts,
	dataConSourceArity, dataConRepArity, dataConRepRepArity,
	dataConIsInfix,
	dataConWorkId, dataConWrapId, dataConWrapId_maybe, dataConImplicitIds,
	dataConRepStrictness,
	
	-- ** Predicates on DataCons
	isNullarySrcDataCon, isNullaryRepDataCon, isTupleCon, isUnboxedTupleCon,
	isVanillaDataCon, classDataCon, dataConCannotMatch,

        -- * Splitting product types
	splitProductType_maybe, splitProductType, deepSplitProductType,
        deepSplitProductType_maybe,

        -- ** Promotion related functions
        promoteType, isPromotableType, isPromotableTyCon,
        buildPromotedTyCon, buildPromotedDataCon,
    ) where

#include "HsVersions.h"

import Type
import TypeRep( Type(..) )  -- Used in promoteType
import PrelNames( liftedTypeKindTyConKey )
import Kind
import Unify
import Coercion
import TyCon
import Class
import Name
import Var
import Outputable
import Unique
import ListSetOps
import Util
import BasicTypes
import FastString
import Module
import VarEnv

import qualified Data.Data as Data
import qualified Data.Typeable
import Data.Char
import Data.Word
\end{code}


Data constructor representation
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following Haskell data type declaration

	data T = T !Int ![Int]

Using the strictness annotations, GHC will represent this as

	data T = T Int# [Int]

That is, the Int has been unboxed.  Furthermore, the Haskell source construction

	T e1 e2

is translated to

	case e1 of { I# x -> 
	case e2 of { r ->
	T x r }}

That is, the first argument is unboxed, and the second is evaluated.  Finally,
pattern matching is translated too:

	case e of { T a b -> ... }

becomes

	case e of { T a' b -> let a = I# a' in ... }

To keep ourselves sane, we name the different versions of the data constructor
differently, as follows.


Note [Data Constructor Naming]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Each data constructor C has two, and possibly up to four, Names associated with it:

		   OccName   Name space	  Name of   Notes
 ---------------------------------------------------------------------------
 The "data con itself" 	 C     DataName	  DataCon   In dom( GlobalRdrEnv )
 The "worker data con"	 C     VarName	  Id        The worker
 The "wrapper data con"	 $WC   VarName	  Id        The wrapper
 The "newtype coercion"  :CoT  TcClsName  TyCon
 
EVERY data constructor (incl for newtypes) has the former two (the
data con itself, and its worker.  But only some data constructors have a
wrapper (see Note [The need for a wrapper]).

Each of these three has a distinct Unique.  The "data con itself" name
appears in the output of the renamer, and names the Haskell-source
data constructor.  The type checker translates it into either the wrapper Id
(if it exists) or worker Id (otherwise).

The data con has one or two Ids associated with it:

The "worker Id", is the actual data constructor.
* Every data constructor (newtype or data type) has a worker

* The worker is very like a primop, in that it has no binding.

* For a *data* type, the worker *is* the data constructor;
  it has no unfolding

* For a *newtype*, the worker has a compulsory unfolding which 
  does a cast, e.g.
	newtype T = MkT Int
	The worker for MkT has unfolding
		\\(x:Int). x `cast` sym CoT
  Here CoT is the type constructor, witnessing the FC axiom
	axiom CoT : T = Int

The "wrapper Id", \$WC, goes as follows

* Its type is exactly what it looks like in the source program. 

* It is an ordinary function, and it gets a top-level binding 
  like any other function.

* The wrapper Id isn't generated for a data type if there is
  nothing for the wrapper to do.  That is, if its defn would be
	\$wC = C

Note [The need for a wrapper]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Why might the wrapper have anything to do?  Two reasons:

* Unboxing strict fields (with -funbox-strict-fields)
	data T = MkT !(Int,Int)
	\$wMkT :: (Int,Int) -> T
	\$wMkT (x,y) = MkT x y
  Notice that the worker has two fields where the wapper has 
  just one.  That is, the worker has type
		MkT :: Int -> Int -> T

* Equality constraints for GADTs
	data T a where { MkT :: a -> T [a] }

  The worker gets a type with explicit equality
  constraints, thus:
	MkT :: forall a b. (a=[b]) => b -> T a

  The wrapper has the programmer-specified type:
	\$wMkT :: a -> T [a]
	\$wMkT a x = MkT [a] a [a] x
  The third argument is a coerion
	[a] :: [a]~[a]

INVARIANT: the dictionary constructor for a class
	   never has a wrapper.


A note about the stupid context
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Data types can have a context:
	
	data (Eq a, Ord b) => T a b = T1 a b | T2 a

and that makes the constructors have a context too
(notice that T2's context is "thinned"):

	T1 :: (Eq a, Ord b) => a -> b -> T a b
	T2 :: (Eq a) => a -> T a b

Furthermore, this context pops up when pattern matching
(though GHC hasn't implemented this, but it is in H98, and
I've fixed GHC so that it now does):

	f (T2 x) = x
gets inferred type
	f :: Eq a => T a b -> a

I say the context is "stupid" because the dictionaries passed
are immediately discarded -- they do nothing and have no benefit.
It's a flaw in the language.

	Up to now [March 2002] I have put this stupid context into the
	type of the "wrapper" constructors functions, T1 and T2, but
	that turned out to be jolly inconvenient for generics, and
	record update, and other functions that build values of type T
	(because they don't have suitable dictionaries available).

	So now I've taken the stupid context out.  I simply deal with
	it separately in the type checker on occurrences of a
	constructor, either in an expression or in a pattern.

	[May 2003: actually I think this decision could evasily be
	reversed now, and probably should be.  Generics could be
	disabled for types with a stupid context; record updates now
	(H98) needs the context too; etc.  It's an unforced change, so
	I'm leaving it for now --- but it does seem odd that the
	wrapper doesn't include the stupid context.]

[July 04] With the advent of generalised data types, it's less obvious
what the "stupid context" is.  Consider
	C :: forall a. Ord a => a -> a -> T (Foo a)
Does the C constructor in Core contain the Ord dictionary?  Yes, it must:

	f :: T b -> Ordering
	f = /\b. \x:T b. 
	    case x of
		C a (d:Ord a) (p:a) (q:a) -> compare d p q

Note that (Foo a) might not be an instance of Ord.

%************************************************************************
%*									*
\subsection{Data constructors}
%*									*
%************************************************************************

\begin{code}
-- | A data constructor
data DataCon
  = MkData {
	dcName    :: Name,	-- This is the name of the *source data con*
				-- (see "Note [Data Constructor Naming]" above)
	dcUnique :: Unique, 	-- Cached from Name
	dcTag    :: ConTag,     -- ^ Tag, used for ordering 'DataCon's

	-- Running example:
	--
	-- 	*** As declared by the user
	--  data T a where
	--    MkT :: forall x y. (x~y,Ord x) => x -> y -> T (x,y)

	-- 	*** As represented internally
	--  data T a where
	--    MkT :: forall a. forall x y. (a~(x,y),x~y,Ord x) => x -> y -> T a
	-- 
	-- The next six fields express the type of the constructor, in pieces
	-- e.g.
	--
	--	dcUnivTyVars  = [a]
	--	dcExTyVars    = [x,y]
	--	dcEqSpec      = [a~(x,y)]
	--	dcOtherTheta  = [x~y, Ord x]	
	--	dcOrigArgTys  = [a,List b]
	--	dcRepTyCon       = T

	dcVanilla :: Bool,	-- True <=> This is a vanilla Haskell 98 data constructor
				--	    Its type is of form
				--	        forall a1..an . t1 -> ... tm -> T a1..an
				-- 	    No existentials, no coercions, nothing.
				-- That is: dcExTyVars = dcEqSpec = dcOtherTheta = []
		-- NB 1: newtypes always have a vanilla data con
		-- NB 2: a vanilla constructor can still be declared in GADT-style 
		--	 syntax, provided its type looks like the above.
		--       The declaration format is held in the TyCon (algTcGadtSyntax)

	dcUnivTyVars :: [TyVar],	-- Universally-quantified type vars [a,b,c]
					-- INVARIANT: length matches arity of the dcRepTyCon
					---           result type of (rep) data con is exactly (T a b c)

	dcExTyVars   :: [TyVar],	-- Existentially-quantified type vars 
		-- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE TYVARS
		-- FOR THE PARENT TyCon. With GADTs the data con might not even have 
		-- the same number of type variables.
		-- [This is a change (Oct05): previously, vanilla datacons guaranteed to
		--  have the same type variables as their parent TyCon, but that seems ugly.]

	-- INVARIANT: the UnivTyVars and ExTyVars all have distinct OccNames
	-- Reason: less confusing, and easier to generate IfaceSyn

	dcEqSpec :: [(TyVar,Type)],	-- Equalities derived from the result type, 
					-- _as written by the programmer_
		-- This field allows us to move conveniently between the two ways
		-- of representing a GADT constructor's type:
		--	MkT :: forall a b. (a ~ [b]) => b -> T a
		--	MkT :: forall b. b -> T [b]
		-- Each equality is of the form (a ~ ty), where 'a' is one of 
		-- the universally quantified type variables
					
		-- The next two fields give the type context of the data constructor
		-- 	(aside from the GADT constraints, 
		--	 which are given by the dcExpSpec)
		-- In GADT form, this is *exactly* what the programmer writes, even if
		-- the context constrains only universally quantified variables
		--	MkT :: forall a b. (a ~ b, Ord b) => a -> T a b
	dcOtherTheta :: ThetaType,  -- The other constraints in the data con's type
		                    -- other than those in the dcEqSpec

	dcStupidTheta :: ThetaType,	-- The context of the data type declaration 
					--	data Eq a => T a = ...
					-- or, rather, a "thinned" version thereof
		-- "Thinned", because the Report says
		-- to eliminate any constraints that don't mention
		-- tyvars free in the arg types for this constructor
		--
		-- INVARIANT: the free tyvars of dcStupidTheta are a subset of dcUnivTyVars
		-- Reason: dcStupidTeta is gotten by thinning the stupid theta from the tycon
		-- 
		-- "Stupid", because the dictionaries aren't used for anything.  
		-- Indeed, [as of March 02] they are no longer in the type of 
		-- the wrapper Id, because that makes it harder to use the wrap-id 
		-- to rebuild values after record selection or in generics.

	dcOrigArgTys :: [Type],		-- Original argument types
					-- (before unboxing and flattening of strict fields)
	dcOrigResTy :: Type,		-- Original result type, as seen by the user
		-- NB: for a data instance, the original user result type may 
		-- differ from the DataCon's representation TyCon.  Example
		--	data instance T [a] where MkT :: a -> T [a]
		-- The OrigResTy is T [a], but the dcRepTyCon might be :T123

	-- Now the strictness annotations and field labels of the constructor
	dcStrictMarks :: [HsBang],
		-- Strictness annotations as decided by the compiler.  
		-- Does *not* include the existential dictionaries
		-- length = dataConSourceArity dataCon

	dcFields  :: [FieldLabel],
		-- Field labels for this constructor, in the
		-- same order as the dcOrigArgTys; 
		-- length = 0 (if not a record) or dataConSourceArity.

	-- Constructor representation
	dcRepArgTys :: [Type],	-- Final, representation argument types, 
				-- after unboxing and flattening,
				-- and *including* all existential evidence args

	dcRepStrictness :: [StrictnessMark],
                -- One for each *representation* *value* argument
		-- See also Note [Data-con worker strictness] in MkId.lhs

	-- Result type of constructor is T t1..tn
	dcRepTyCon  :: TyCon,		-- Result tycon, T

	dcRepType   :: Type,	-- Type of the constructor
				-- 	forall a x y. (a~(x,y), x~y, Ord x) =>
                                --        x -> y -> T a
				-- (this is *not* of the constructor wrapper Id:
				--  see Note [Data con representation] below)
	-- Notice that the existential type parameters come *second*.  
	-- Reason: in a case expression we may find:
	--	case (e :: T t) of
        --        MkT x y co1 co2 (d:Ord x) (v:r) (w:F s) -> ...
	-- It's convenient to apply the rep-type of MkT to 't', to get
	--	forall x y. (t~(x,y), x~y, Ord x) => x -> y -> T t
	-- and use that to check the pattern.  Mind you, this is really only
	-- used in CoreLint.


	-- The curried worker function that corresponds to the constructor:
	-- It doesn't have an unfolding; the code generator saturates these Ids
	-- and allocates a real constructor when it finds one.
	--
	-- An entirely separate wrapper function is built in TcTyDecls
	dcIds :: DataConIds,

	dcInfix :: Bool		-- True <=> declared infix
				-- Used for Template Haskell and 'deriving' only
				-- The actual fixity is stored elsewhere
  }
  deriving Data.Typeable.Typeable

-- | Contains the Ids of the data constructor functions
data DataConIds
  = DCIds (Maybe Id) Id 	-- Algebraic data types always have a worker, and
				-- may or may not have a wrapper, depending on whether
				-- the wrapper does anything.  Newtypes just have a worker

	-- _Neither_ the worker _nor_ the wrapper take the dcStupidTheta dicts as arguments

	-- The wrapper takes dcOrigArgTys as its arguments
	-- The worker takes dcRepArgTys as its arguments
	-- If the worker is absent, dcRepArgTys is the same as dcOrigArgTys

	-- The 'Nothing' case of DCIds is important
	-- Not only is this efficient,
	-- but it also ensures that the wrapper is replaced
	-- by the worker (because it *is* the worker)
	-- even when there are no args. E.g. in
	-- 		f (:) x
	-- the (:) *is* the worker.
	-- This is really important in rule matching,
	-- (We could match on the wrappers,
	-- but that makes it less likely that rules will match
	-- when we bring bits of unfoldings together.)

-- | Type of the tags associated with each constructor possibility
type ConTag = Int

fIRST_TAG :: ConTag
-- ^ Tags are allocated from here for real constructors
fIRST_TAG =  1
\end{code}

Note [Data con representation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The dcRepType field contains the type of the representation of a contructor
This may differ from the type of the contructor *Id* (built
by MkId.mkDataConId) for two reasons:
	a) the constructor Id may be overloaded, but the dictionary isn't stored
	   e.g.    data Eq a => T a = MkT a a

	b) the constructor may store an unboxed version of a strict field.

Here's an example illustrating both:
	data Ord a => T a = MkT Int! a
Here
	T :: Ord a => Int -> a -> T a
but the rep type is
	Trep :: Int# -> a -> T a
Actually, the unboxed part isn't implemented yet!


%************************************************************************
%*									*
\subsection{Instances}
%*									*
%************************************************************************

\begin{code}
instance Eq DataCon where
    a == b = getUnique a == getUnique b
    a /= b = getUnique a /= getUnique b

instance Ord DataCon where
    a <= b = getUnique a <= getUnique b
    a <	 b = getUnique a <  getUnique b
    a >= b = getUnique a >= getUnique b
    a >	 b = getUnique a > getUnique b
    compare a b = getUnique a `compare` getUnique b

instance Uniquable DataCon where
    getUnique = dcUnique

instance NamedThing DataCon where
    getName = dcName

instance Outputable DataCon where
    ppr con = ppr (dataConName con)

instance Show DataCon where
    showsPrec p con = showsPrecSDoc p (ppr con)

instance Data.Data DataCon where
    -- don't traverse?
    toConstr _   = abstractConstr "DataCon"
    gunfold _ _  = error "gunfold"
    dataTypeOf _ = mkNoRepType "DataCon"
\end{code}


%************************************************************************
%*									*
\subsection{Construction}
%*									*
%************************************************************************

\begin{code}
-- | Build a new data constructor
mkDataCon :: Name 
	  -> Bool	        -- ^ Is the constructor declared infix?
	  -> [HsBang]           -- ^ Strictness annotations written in the source file
	  -> [FieldLabel]       -- ^ Field labels for the constructor, if it is a record, 
				--   otherwise empty
	  -> [TyVar]            -- ^ Universally quantified type variables
	  -> [TyVar]            -- ^ Existentially quantified type variables
	  -> [(TyVar,Type)]     -- ^ GADT equalities
	  -> ThetaType          -- ^ Theta-type occuring before the arguments proper
	  -> [Type]             -- ^ Original argument types
	  -> Type		-- ^ Original result type
	  -> TyCon              -- ^ Representation type constructor
	  -> ThetaType          -- ^ The "stupid theta", context of the data declaration 
				--   e.g. @data Eq a => T a ...@
	  -> DataConIds         -- ^ The Ids of the actual builder functions
	  -> DataCon
  -- Can get the tag from the TyCon

mkDataCon name declared_infix
	  arg_stricts	-- Must match orig_arg_tys 1-1
	  fields
	  univ_tvs ex_tvs 
	  eq_spec theta
	  orig_arg_tys orig_res_ty rep_tycon
	  stupid_theta ids
-- Warning: mkDataCon is not a good place to check invariants. 
-- If the programmer writes the wrong result type in the decl, thus:
--	data T a where { MkT :: S }
-- then it's possible that the univ_tvs may hit an assertion failure
-- if you pull on univ_tvs.  This case is checked by checkValidDataCon,
-- so the error is detected properly... it's just that asaertions here
-- are a little dodgy.

  = -- ASSERT( not (any isEqPred theta) )
	-- We don't currently allow any equality predicates on
	-- a data constructor (apart from the GADT ones in eq_spec)
    con
  where
    is_vanilla = null ex_tvs && null eq_spec && null theta
    con = MkData {dcName = name, dcUnique = nameUnique name, 
		  dcVanilla = is_vanilla, dcInfix = declared_infix,
	  	  dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, 
		  dcEqSpec = eq_spec, 
		  dcOtherTheta = theta,
		  dcStupidTheta = stupid_theta, 
		  dcOrigArgTys = orig_arg_tys, dcOrigResTy = orig_res_ty,
		  dcRepTyCon = rep_tycon, 
		  dcRepArgTys = rep_arg_tys,
		  dcStrictMarks = arg_stricts, 
		  dcRepStrictness = rep_arg_stricts,
		  dcFields = fields, dcTag = tag, dcRepType = ty,
		  dcIds = ids }

	-- Strictness marks for source-args
	--	*after unboxing choices*, 
	-- but  *including existential dictionaries*
	-- 
	-- The 'arg_stricts' passed to mkDataCon are simply those for the
	-- source-language arguments.  We add extra ones for the
	-- dictionary arguments right here.
    full_theta   = eqSpecPreds eq_spec ++ theta
    real_arg_tys = full_theta                         ++ orig_arg_tys
    real_stricts = map mk_pred_strict_mark full_theta ++ arg_stricts

	-- Representation arguments and demands
	-- To do: eliminate duplication with MkId
    (rep_arg_stricts, rep_arg_tys) = computeRep real_stricts real_arg_tys

    tag = assoc "mkDataCon" (tyConDataCons rep_tycon `zip` [fIRST_TAG..]) con
    ty  = mkForAllTys univ_tvs $ mkForAllTys ex_tvs $ 
	  mkFunTys rep_arg_tys $
	  mkTyConApp rep_tycon (mkTyVarTys univ_tvs)

eqSpecPreds :: [(TyVar,Type)] -> ThetaType
eqSpecPreds spec = [ mkEqPred (mkTyVarTy tv) ty | (tv,ty) <- spec ]

mk_pred_strict_mark :: PredType -> HsBang
mk_pred_strict_mark pred 
  | isEqPred pred = HsUnpack	-- Note [Unpack equality predicates]
  | otherwise     = HsNoBang
\end{code}

Note [Unpack equality predicates]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we have a GADT with a contructor C :: (a~[b]) => b -> T a
we definitely want that equality predicate *unboxed* so that it
takes no space at all.  This is easily done: just give it
an UNPACK pragma. The rest of the unpack/repack code does the
heavy lifting.  This one line makes every GADT take a word less
space for each equality predicate, so it's pretty important!

\begin{code}
-- | The 'Name' of the 'DataCon', giving it a unique, rooted identification
dataConName :: DataCon -> Name
dataConName = dcName

-- | The tag used for ordering 'DataCon's
dataConTag :: DataCon -> ConTag
dataConTag  = dcTag

-- | The type constructor that we are building via this data constructor
dataConTyCon :: DataCon -> TyCon
dataConTyCon = dcRepTyCon

-- | The original type constructor used in the definition of this data
-- constructor.  In case of a data family instance, that will be the family
-- type constructor.
dataConOrigTyCon :: DataCon -> TyCon
dataConOrigTyCon dc 
  | Just (tc, _) <- tyConFamInst_maybe (dcRepTyCon dc) = tc
  | otherwise                                          = dcRepTyCon dc

-- | The representation type of the data constructor, i.e. the sort
-- type that will represent values of this type at runtime
dataConRepType :: DataCon -> Type
dataConRepType = dcRepType

-- | Should the 'DataCon' be presented infix?
dataConIsInfix :: DataCon -> Bool
dataConIsInfix = dcInfix

-- | The universally-quantified type variables of the constructor
dataConUnivTyVars :: DataCon -> [TyVar]
dataConUnivTyVars = dcUnivTyVars

-- | The existentially-quantified type variables of the constructor
dataConExTyVars :: DataCon -> [TyVar]
dataConExTyVars = dcExTyVars

-- | Both the universal and existentiatial type variables of the constructor
dataConAllTyVars :: DataCon -> [TyVar]
dataConAllTyVars (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs })
  = univ_tvs ++ ex_tvs

-- | Equalities derived from the result type of the data constructor, as written
-- by the programmer in any GADT declaration
dataConEqSpec :: DataCon -> [(TyVar,Type)]
dataConEqSpec = dcEqSpec

-- | The *full* constraints on the constructor type
dataConTheta :: DataCon -> ThetaType
dataConTheta (MkData { dcEqSpec = eq_spec, dcOtherTheta = theta }) 
  = eqSpecPreds eq_spec ++ theta

-- | Get the Id of the 'DataCon' worker: a function that is the "actual"
-- constructor and has no top level binding in the program. The type may
-- be different from the obvious one written in the source program. Panics
-- if there is no such 'Id' for this 'DataCon'
dataConWorkId :: DataCon -> Id
dataConWorkId dc = case dcIds dc of
			DCIds _ wrk_id -> wrk_id

-- | Get the Id of the 'DataCon' wrapper: a function that wraps the "actual"
-- constructor so it has the type visible in the source program: c.f. 'dataConWorkId'.
-- Returns Nothing if there is no wrapper, which occurs for an algebraic data constructor 
-- and also for a newtype (whose constructor is inlined compulsorily)
dataConWrapId_maybe :: DataCon -> Maybe Id
dataConWrapId_maybe dc = case dcIds dc of
				DCIds mb_wrap _ -> mb_wrap

-- | Returns an Id which looks like the Haskell-source constructor by using
-- the wrapper if it exists (see 'dataConWrapId_maybe') and failing over to
-- the worker (see 'dataConWorkId')
dataConWrapId :: DataCon -> Id
dataConWrapId dc = case dcIds dc of
			DCIds (Just wrap) _   -> wrap
			DCIds Nothing     wrk -> wrk	    -- worker=wrapper

-- | Find all the 'Id's implicitly brought into scope by the data constructor. Currently,
-- the union of the 'dataConWorkId' and the 'dataConWrapId'
dataConImplicitIds :: DataCon -> [Id]
dataConImplicitIds dc = case dcIds dc of
			  DCIds (Just wrap) work -> [wrap,work]
			  DCIds Nothing     work -> [work]

-- | The labels for the fields of this particular 'DataCon'
dataConFieldLabels :: DataCon -> [FieldLabel]
dataConFieldLabels = dcFields

-- | Extract the type for any given labelled field of the 'DataCon'
dataConFieldType :: DataCon -> FieldLabel -> Type
dataConFieldType con label
  = case lookup label (dcFields con `zip` dcOrigArgTys con) of
      Just ty -> ty
      Nothing -> pprPanic "dataConFieldType" (ppr con <+> ppr label)

-- | The strictness markings decided on by the compiler.  Does not include those for
-- existential dictionaries.  The list is in one-to-one correspondence with the arity of the 'DataCon'
dataConStrictMarks :: DataCon -> [HsBang]
dataConStrictMarks = dcStrictMarks

-- | Strictness of evidence arguments to the wrapper function
dataConExStricts :: DataCon -> [HsBang]
-- Usually empty, so we don't bother to cache this
dataConExStricts dc = map mk_pred_strict_mark (dataConTheta dc)

-- | Source-level arity of the data constructor
dataConSourceArity :: DataCon -> Arity
dataConSourceArity dc = length (dcOrigArgTys dc)

-- | Gives the number of actual fields in the /representation/ of the 
-- data constructor. This may be more than appear in the source code;
-- the extra ones are the existentially quantified dictionaries
dataConRepArity :: DataCon -> Arity
dataConRepArity (MkData {dcRepArgTys = arg_tys}) = length arg_tys

-- | The number of fields in the /representation/ of the constructor
-- AFTER taking into account the unpacking of any unboxed tuple fields
dataConRepRepArity :: DataCon -> RepArity
dataConRepRepArity dc = typeRepArity (dataConRepArity dc) (dataConRepType dc)

-- | Return whether there are any argument types for this 'DataCon's original source type
isNullarySrcDataCon :: DataCon -> Bool
isNullarySrcDataCon dc = null (dcOrigArgTys dc)

-- | Return whether there are any argument types for this 'DataCon's runtime representation type
isNullaryRepDataCon :: DataCon -> Bool
isNullaryRepDataCon dc = null (dcRepArgTys dc)

dataConRepStrictness :: DataCon -> [StrictnessMark]
-- ^ Give the demands on the arguments of a
-- Core constructor application (Con dc args)
dataConRepStrictness dc = dcRepStrictness dc

-- | The \"signature\" of the 'DataCon' returns, in order:
--
-- 1) The result of 'dataConAllTyVars',
--
-- 2) All the 'ThetaType's relating to the 'DataCon' (coercion, dictionary, implicit
--    parameter - whatever)
--
-- 3) The type arguments to the constructor
--
-- 4) The /original/ result type of the 'DataCon'
dataConSig :: DataCon -> ([TyVar], ThetaType, [Type], Type)
dataConSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, 
		    dcEqSpec = eq_spec, dcOtherTheta  = theta, 
		    dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
  = (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ theta, arg_tys, res_ty)

-- | The \"full signature\" of the 'DataCon' returns, in order:
--
-- 1) The result of 'dataConUnivTyVars'
--
-- 2) The result of 'dataConExTyVars'
--
-- 3) The result of 'dataConEqSpec'
--
-- 4) The result of 'dataConDictTheta'
--
-- 5) The original argument types to the 'DataCon' (i.e. before 
--    any change of the representation of the type)
--
-- 6) The original result type of the 'DataCon'
dataConFullSig :: DataCon 
	       -> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, [Type], Type)
dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, 
			dcEqSpec = eq_spec, dcOtherTheta = theta,
			dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
  = (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)

dataConOrigResTy :: DataCon -> Type
dataConOrigResTy dc = dcOrigResTy dc

-- | The \"stupid theta\" of the 'DataCon', such as @data Eq a@ in:
--
-- > data Eq a => T a = ...
dataConStupidTheta :: DataCon -> ThetaType
dataConStupidTheta dc = dcStupidTheta dc

dataConUserType :: DataCon -> Type
-- ^ The user-declared type of the data constructor
-- in the nice-to-read form:
--
-- > T :: forall a b. a -> b -> T [a]
--
-- rather than:
--
-- > T :: forall a c. forall b. (c~[a]) => a -> b -> T c
--
-- NB: If the constructor is part of a data instance, the result type
-- mentions the family tycon, not the internal one.
dataConUserType  (MkData { dcUnivTyVars = univ_tvs, 
			   dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
			   dcOtherTheta = theta, dcOrigArgTys = arg_tys,
			   dcOrigResTy = res_ty })
  = mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
    mkFunTys theta $
    mkFunTys arg_tys $
    res_ty

-- | Finds the instantiated types of the arguments required to construct a 'DataCon' representation
-- NB: these INCLUDE any dictionary args
--     but EXCLUDE the data-declaration context, which is discarded
-- It's all post-flattening etc; this is a representation type
dataConInstArgTys :: DataCon	-- ^ A datacon with no existentials or equality constraints
				-- However, it can have a dcTheta (notably it can be a 
				-- class dictionary, with superclasses)
	      	  -> [Type] 	-- ^ Instantiated at these types
	      	  -> [Type]
dataConInstArgTys dc@(MkData {dcRepArgTys = rep_arg_tys, 
			      dcUnivTyVars = univ_tvs, dcEqSpec = eq_spec,
			      dcExTyVars = ex_tvs}) inst_tys
 = ASSERT2 ( length univ_tvs == length inst_tys 
           , ptext (sLit "dataConInstArgTys") <+> ppr dc $$ ppr univ_tvs $$ ppr inst_tys)
   ASSERT2 ( null ex_tvs && null eq_spec, ppr dc )        
   map (substTyWith univ_tvs inst_tys) rep_arg_tys

-- | Returns just the instantiated /value/ argument types of a 'DataCon',
-- (excluding dictionary args)
dataConInstOrigArgTys 
	:: DataCon	-- Works for any DataCon
	-> [Type]	-- Includes existential tyvar args, but NOT
			-- equality constraints or dicts
	-> [Type]
-- For vanilla datacons, it's all quite straightforward
-- But for the call in MatchCon, we really do want just the value args
dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys,
			          dcUnivTyVars = univ_tvs, 
			          dcExTyVars = ex_tvs}) inst_tys
  = ASSERT2( length tyvars == length inst_tys
          , ptext (sLit "dataConInstOrigArgTys") <+> ppr dc $$ ppr tyvars $$ ppr inst_tys )
    map (substTyWith tyvars inst_tys) arg_tys
  where
    tyvars = univ_tvs ++ ex_tvs
\end{code}

\begin{code}
-- | Returns the argument types of the wrapper, excluding all dictionary arguments
-- and without substituting for any type variables
dataConOrigArgTys :: DataCon -> [Type]
dataConOrigArgTys dc = dcOrigArgTys dc

-- | Returns the arg types of the worker, including all dictionaries, after any 
-- flattening has been done and without substituting for any type variables
dataConRepArgTys :: DataCon -> [Type]
dataConRepArgTys dc = dcRepArgTys dc
\end{code}

\begin{code}
-- | The string @package:module.name@ identifying a constructor, which is attached
-- to its info table and used by the GHCi debugger and the heap profiler
dataConIdentity :: DataCon -> [Word8]
-- We want this string to be UTF-8, so we get the bytes directly from the FastStrings.
dataConIdentity dc = bytesFS (packageIdFS (modulePackageId mod)) ++ 
                  fromIntegral (ord ':') : bytesFS (moduleNameFS (moduleName mod)) ++
                  fromIntegral (ord '.') : bytesFS (occNameFS (nameOccName name))
  where name = dataConName dc
        mod  = ASSERT( isExternalName name ) nameModule name
\end{code}

\begin{code}
isTupleCon :: DataCon -> Bool
isTupleCon (MkData {dcRepTyCon = tc}) = isTupleTyCon tc
	
isUnboxedTupleCon :: DataCon -> Bool
isUnboxedTupleCon (MkData {dcRepTyCon = tc}) = isUnboxedTupleTyCon tc

-- | Vanilla 'DataCon's are those that are nice boring Haskell 98 constructors
isVanillaDataCon :: DataCon -> Bool
isVanillaDataCon dc = dcVanilla dc
\end{code}

\begin{code}
classDataCon :: Class -> DataCon
classDataCon clas = case tyConDataCons (classTyCon clas) of
		      (dict_constr:no_more) -> ASSERT( null no_more ) dict_constr 
		      [] -> panic "classDataCon"
\end{code}

\begin{code}
dataConCannotMatch :: [Type] -> DataCon -> Bool
-- Returns True iff the data con *definitely cannot* match a 
--		    scrutinee of type (T tys)
--		    where T is the type constructor for the data con
-- NB: look at *all* equality constraints, not only those
--     in dataConEqSpec; see Trac #5168
dataConCannotMatch tys con
  | null theta        = False	-- Common
  | all isTyVarTy tys = False	-- Also common
  | otherwise
  = typesCantMatch [(Type.substTy subst ty1, Type.substTy subst ty2)
                   | (ty1, ty2) <- concatMap predEqs theta ]
  where
    dc_tvs  = dataConUnivTyVars con
    theta   = dataConTheta con
    subst   = zipTopTvSubst dc_tvs tys

    -- TODO: could gather equalities from superclasses too
    predEqs pred = case classifyPredType pred of
                     EqPred ty1 ty2 -> [(ty1, ty2)]
                     TuplePred ts   -> concatMap predEqs ts
                     _              -> []
\end{code}

%************************************************************************
%*									*
\subsection{Splitting products}
%*									*
%************************************************************************

\begin{code}
-- | Extract the type constructor, type argument, data constructor and it's
-- /representation/ argument types from a type if it is a product type.
--
-- Precisely, we return @Just@ for any type that is all of:
--
--  * Concrete (i.e. constructors visible)
--
--  * Single-constructor
--
--  * Not existentially quantified
--
-- Whether the type is a @data@ type or a @newtype@
splitProductType_maybe
	:: Type 			-- ^ A product type, perhaps
	-> Maybe (TyCon, 		-- The type constructor
		  [Type],		-- Type args of the tycon
		  DataCon,		-- The data constructor
		  [Type])		-- Its /representation/ arg types

	-- Rejecing existentials is conservative.  Maybe some things
	-- could be made to work with them, but I'm not going to sweat
	-- it through till someone finds it's important.

splitProductType_maybe ty
  = case splitTyConApp_maybe ty of
	Just (tycon,ty_args)
	   | isProductTyCon tycon  	-- Includes check for non-existential,
					-- and for constructors visible
	   -> Just (tycon, ty_args, data_con, dataConInstArgTys data_con ty_args)
	   where
	      data_con = ASSERT( not (null (tyConDataCons tycon)) ) 
			 head (tyConDataCons tycon)
	_other -> Nothing

-- | As 'splitProductType_maybe', but panics if the 'Type' is not a product type
splitProductType :: String -> Type -> (TyCon, [Type], DataCon, [Type])
splitProductType str ty
  = case splitProductType_maybe ty of
	Just stuff -> stuff
	Nothing    -> pprPanic (str ++ ": not a product") (pprType ty)


-- | As 'splitProductType_maybe', but in turn instantiates the 'TyCon' returned
-- and hence recursively tries to unpack it as far as it able to
deepSplitProductType_maybe :: Type -> Maybe (TyCon, [Type], DataCon, [Type])
deepSplitProductType_maybe ty
  = do { (res@(tycon, tycon_args, _, _)) <- splitProductType_maybe ty
       ; let {result 
             | Just (ty', _co) <- instNewTyCon_maybe tycon tycon_args
	     , not (isRecursiveTyCon tycon)
             = deepSplitProductType_maybe ty'	-- Ignore the coercion?
             | isNewTyCon tycon = Nothing  -- cannot unbox through recursive
					   -- newtypes nor through families
             | otherwise = Just res}
       ; result
       }

-- | As 'deepSplitProductType_maybe', but panics if the 'Type' is not a product type
deepSplitProductType :: String -> Type -> (TyCon, [Type], DataCon, [Type])
deepSplitProductType str ty 
  = case deepSplitProductType_maybe ty of
      Just stuff -> stuff
      Nothing -> pprPanic (str ++ ": not a product") (pprType ty)

-- | Compute the representation type strictness and type suitable for a 'DataCon'
computeRep :: [HsBang]			-- ^ Original argument strictness
	   -> [Type]			-- ^ Original argument types
	   -> ([StrictnessMark],	-- Representation arg strictness
	       [Type])			-- And type

computeRep stricts tys
  = unzip $ concat $ zipWithEqual "computeRep" unbox stricts tys
  where
    unbox HsNoBang       ty = [(NotMarkedStrict, ty)]
    unbox HsStrict       ty = [(MarkedStrict,    ty)]
    unbox HsNoUnpack     ty = [(MarkedStrict,    ty)]
    unbox HsUnpackFailed ty = [(MarkedStrict,    ty)]
    unbox HsUnpack ty = zipEqual "computeRep" (dataConRepStrictness arg_dc) arg_tys
                      where
                        (_tycon, _tycon_args, arg_dc, arg_tys) 
                           = deepSplitProductType "unbox_strict_arg_ty" ty
\end{code}


%************************************************************************
%*                                                                      *
        Promoting of data types to the kind level
%*                                                                      *
%************************************************************************

These two 'buildPromoted..' functions are here because
 * They belong together
 * 'buildPromotedTyCon' is used by promoteType
 * 'buildPromotedTyCon' depends on DataCon stuff

\begin{code}
buildPromotedTyCon :: TyCon -> TyCon
buildPromotedTyCon tc
  = mkPromotedTyCon tc (promoteKind (tyConKind tc))

buildPromotedDataCon :: DataCon -> TyCon
buildPromotedDataCon dc 
  = ASSERT ( isPromotableType ty )
    mkPromotedDataCon dc (getName dc) (getUnique dc) kind arity
  where 
    ty    = dataConUserType dc
    kind  = promoteType ty
    arity = dataConSourceArity dc
\end{code}

Note [Promoting a Type to a Kind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppsoe we have a data constructor D
     D :: forall (a:*). Maybe a -> T a
We promote this to be a type constructor 'D:
     'D :: forall (k:BOX). 'Maybe k -> 'T k

The transformation from type to kind is done by promoteType

  * Convert forall (a:*) to forall (k:BOX), and substitute

  * Ensure all foralls are at the top (no higher rank stuff)

  * Ensure that all type constructors mentioned (Maybe and T
    in the example) are promotable; that is, they have kind 
          * -> ... -> * -> *

\begin{code}
isPromotableType :: Type -> Bool
isPromotableType ty
  = all (isLiftedTypeKind . tyVarKind) tvs
    && go rho
  where
    (tvs, rho) = splitForAllTys ty
    go (TyConApp tc tys) | Just n <- isPromotableTyCon tc
                         = tys `lengthIs` n && all go tys
    go (FunTy arg res)   = go arg && go res
    go (TyVarTy tvar)    = tvar `elem` tvs
    go _                 = False

-- If tc's kind is [ *^n -> * ] returns [ Just n ], else returns [ Nothing ]
isPromotableTyCon :: TyCon -> Maybe Int
isPromotableTyCon tc
  | all isLiftedTypeKind (res:args) = Just $ length args
  | otherwise                       = Nothing
  where
    (args, res) = splitKindFunTys (tyConKind tc)

-- | Promotes a type to a kind. 
-- Assumes the argument satisfies 'isPromotableType'
promoteType :: Type -> Kind
promoteType ty
  = mkForAllTys kvs (go rho)
  where
    (tvs, rho) = splitForAllTys ty
    kvs = [ mkKindVar (tyVarName tv) superKind | tv <- tvs ]
    env = zipVarEnv tvs kvs

    go (TyConApp tc tys) = mkTyConApp (buildPromotedTyCon tc) (map go tys)
    go (FunTy arg res)   = mkArrowKind (go arg) (go res)
    go (TyVarTy tv)      | Just kv <- lookupVarEnv env tv 
                         = TyVarTy kv
    go _ = panic "promoteType"  -- Argument did not satisfy isPromotableType

promoteKind :: Kind -> SuperKind
-- Promote the kind of a type constructor
-- from (* -> * -> *) to (BOX -> BOX -> BOX) 
promoteKind (TyConApp tc []) 
  | tc `hasKey` liftedTypeKindTyConKey = superKind
promoteKind (FunTy arg res) = FunTy (promoteKind arg) (promoteKind res)
promoteKind k = pprPanic "promoteKind" (ppr k)
\end{code}