DataCon.hs 57.4 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1998

5
\section[DataCon]{@DataCon@: Data Constructors}
Austin Seipp's avatar
Austin Seipp committed
6
-}
7

8
{-# LANGUAGE CPP, DeriveDataTypeable #-}
Ian Lynagh's avatar
Ian Lynagh committed
9

10
module DataCon (
batterseapower's avatar
batterseapower committed
11
        -- * Main data types
Simon Peyton Jones's avatar
Simon Peyton Jones committed
12
        DataCon, DataConRep(..),
13 14
        SrcStrictness(..), SrcUnpackedness(..),
        HsSrcBang(..), HsImplBang(..),
Simon Peyton Jones's avatar
Simon Peyton Jones committed
15
        StrictnessMark(..),
Edward Z. Yang's avatar
Edward Z. Yang committed
16 17
        ConTag,

18 19 20
        -- ** Equality specs
        EqSpec, mkEqSpec, eqSpecTyVar, eqSpecType,
        eqSpecPair, eqSpecPreds,
21
        substEqSpec, filterEqSpec,
22

23 24 25
        -- ** Field labels
        FieldLbl(..), FieldLabel, FieldLabelString,

Edward Z. Yang's avatar
Edward Z. Yang committed
26
        -- ** Type construction
27
        mkDataCon, fIRST_TAG,
Edward Z. Yang's avatar
Edward Z. Yang committed
28 29

        -- ** Type deconstruction
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
30
        dataConRepType, dataConInstSig, dataConFullSig,
31 32 33
        dataConName, dataConIdentity, dataConTag, dataConTagZ,
        dataConTyCon, dataConOrigTyCon,
        dataConUserType,
Ningning Xie's avatar
Ningning Xie committed
34
        dataConUnivTyVars, dataConExTyCoVars, dataConUnivAndExTyCoVars,
35
        dataConUserTyVars, dataConUserTyVarBinders,
36
        dataConEqSpec, dataConTheta,
Edward Z. Yang's avatar
Edward Z. Yang committed
37 38 39
        dataConStupidTheta,
        dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
        dataConInstOrigArgTys, dataConRepArgTys,
40
        dataConFieldLabels, dataConFieldType, dataConFieldType_maybe,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
41
        dataConSrcBangs,
42
        dataConSourceArity, dataConRepArity,
Edward Z. Yang's avatar
Edward Z. Yang committed
43
        dataConIsInfix,
44 45
        dataConWorkId, dataConWrapId, dataConWrapId_maybe,
        dataConImplicitTyThings,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
46
        dataConRepStrictness, dataConImplBangs, dataConBoxer,
Edward Z. Yang's avatar
Edward Z. Yang committed
47 48

        splitDataProductType_maybe,
49

Edward Z. Yang's avatar
Edward Z. Yang committed
50 51
        -- ** Predicates on DataCons
        isNullarySrcDataCon, isNullaryRepDataCon, isTupleDataCon, isUnboxedTupleCon,
52
        isUnboxedSumCon,
Edward Z. Yang's avatar
Edward Z. Yang committed
53
        isVanillaDataCon, classDataCon, dataConCannotMatch,
54
        dataConUserTyVarsArePermuted,
55
        isBanged, isMarkedStrict, eqHsBang, isSrcStrict, isSrcUnpacked,
56
        specialPromotedDc,
57

58
        -- ** Promotion related functions
59
        promoteDataCon
60 61 62 63
    ) where

#include "HsVersions.h"

64 65
import GhcPrelude

66
import {-# SOURCE #-} MkId( DataConBoxer )
Simon Marlow's avatar
Simon Marlow committed
67
import Type
68
import Coercion
69
import Unify
Simon Marlow's avatar
Simon Marlow committed
70
import TyCon
71
import FieldLabel
Simon Marlow's avatar
Simon Marlow committed
72 73
import Class
import Name
74
import PrelNames
75
import Predicate
Simon Marlow's avatar
Simon Marlow committed
76
import Var
77
import Outputable
Simon Marlow's avatar
Simon Marlow committed
78
import Util
batterseapower's avatar
batterseapower committed
79
import BasicTypes
80
import FastString
81
import Module
82
import Binary
83 84
import UniqSet
import Unique( mkAlphaTyVarUnique )
85

86 87 88
import Data.ByteString (ByteString)
import qualified Data.ByteString.Builder as BSB
import qualified Data.ByteString.Lazy    as LBS
89
import qualified Data.Data as Data
90
import Data.Char
Simon Peyton Jones's avatar
Simon Peyton Jones committed
91
import Data.List( find )
92

Austin Seipp's avatar
Austin Seipp committed
93
{-
94 95 96
Data constructor representation
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following Haskell data type declaration
97

Edward Z. Yang's avatar
Edward Z. Yang committed
98
        data T = T !Int ![Int]
99 100 101

Using the strictness annotations, GHC will represent this as

Edward Z. Yang's avatar
Edward Z. Yang committed
102
        data T = T Int# [Int]
103 104 105

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

Edward Z. Yang's avatar
Edward Z. Yang committed
106
        T e1 e2
107 108 109

is translated to

Edward Z. Yang's avatar
Edward Z. Yang committed
110 111 112
        case e1 of { I# x ->
        case e2 of { r ->
        T x r }}
113 114 115 116

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

Edward Z. Yang's avatar
Edward Z. Yang committed
117
        case e of { T a b -> ... }
118 119 120

becomes

Edward Z. Yang's avatar
Edward Z. Yang committed
121
        case e of { T a' b -> let a = I# a' in ... }
122 123 124 125 126 127 128

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


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

Edward Z. Yang's avatar
Edward Z. Yang committed
131
                   OccName   Name space   Name of   Notes
132
 ---------------------------------------------------------------------------
Edward Z. Yang's avatar
Edward Z. Yang committed
133 134 135
 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
136
 The "newtype coercion"  :CoT  TcClsName  TyCon
Edward Z. Yang's avatar
Edward Z. Yang committed
137

138 139 140 141 142
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
143 144 145 146 147 148
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:

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

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

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

Edward Z. Yang's avatar
Edward Z. Yang committed
157
* For a *newtype*, the worker has a compulsory unfolding which
158
  does a cast, e.g.
Edward Z. Yang's avatar
Edward Z. Yang committed
159 160 161
        newtype T = MkT Int
        The worker for MkT has unfolding
                \\(x:Int). x `cast` sym CoT
162
  Here CoT is the type constructor, witnessing the FC axiom
Edward Z. Yang's avatar
Edward Z. Yang committed
163
        axiom CoT : T = Int
164

batterseapower's avatar
batterseapower committed
165
The "wrapper Id", \$WC, goes as follows
166

Edward Z. Yang's avatar
Edward Z. Yang committed
167
* Its type is exactly what it looks like in the source program.
168

Edward Z. Yang's avatar
Edward Z. Yang committed
169
* It is an ordinary function, and it gets a top-level binding
170 171 172 173
  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
Edward Z. Yang's avatar
Edward Z. Yang committed
174
        \$wC = C
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
Note [Data constructor workers and wrappers]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Algebraic data types
  - Always have a worker, with no unfolding
  - May or may not have a wrapper; see Note [The need for a wrapper]

* Newtypes
  - Always have a worker, which has a compulsory unfolding (just a cast)
  - May or may not have a wrapper; see Note [The need for a wrapper]

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

* Neither_ the worker _nor_ the wrapper take the dcStupidTheta dicts as arguments

* The wrapper (if it exists) takes dcOrigArgTys as its arguments
  The worker takes dataConRepArgTys as its arguments
  If the worker is absent, dataConRepArgTys is the same as dcOrigArgTys

* The 'NoDataConRep' case of DataConRep is important. Not only is it
  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.)

204 205
Note [The need for a wrapper]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
206 207
Why might the wrapper have anything to do?  The full story is
in wrapper_reqd in MkId.mkDataConRep.
208 209

* Unboxing strict fields (with -funbox-strict-fields)
Edward Z. Yang's avatar
Edward Z. Yang committed
210 211 212 213
        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
214
  just one.  That is, the worker has type
Edward Z. Yang's avatar
Edward Z. Yang committed
215
                MkT :: Int -> Int -> T
216 217

* Equality constraints for GADTs
Edward Z. Yang's avatar
Edward Z. Yang committed
218
        data T a where { MkT :: a -> T [a] }
219 220 221

  The worker gets a type with explicit equality
  constraints, thus:
Edward Z. Yang's avatar
Edward Z. Yang committed
222
        MkT :: forall a b. (a=[b]) => b -> T a
223 224

  The wrapper has the programmer-specified type:
Edward Z. Yang's avatar
Edward Z. Yang committed
225 226
        \$wMkT :: a -> T [a]
        \$wMkT a x = MkT [a] a [a] x
227
  The third argument is a coercion
Edward Z. Yang's avatar
Edward Z. Yang committed
228
        [a] :: [a]~[a]
229

230
* Data family instances may do a cast on the result
231

232 233
* Type variables may be permuted; see MkId
  Note [Data con wrappers and GADT syntax]
234

235 236 237

Note [The stupid context]
~~~~~~~~~~~~~~~~~~~~~~~~~
238
Data types can have a context:
Edward Z. Yang's avatar
Edward Z. Yang committed
239 240

        data (Eq a, Ord b) => T a b = T1 a b | T2 a
241 242 243 244

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

Edward Z. Yang's avatar
Edward Z. Yang committed
245 246
        T1 :: (Eq a, Ord b) => a -> b -> T a b
        T2 :: (Eq a) => a -> T a b
247 248 249 250 251

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):

Edward Z. Yang's avatar
Edward Z. Yang committed
252
        f (T2 x) = x
253
gets inferred type
Edward Z. Yang's avatar
Edward Z. Yang committed
254
        f :: Eq a => T a b -> a
255 256 257 258 259

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.

Edward Z. Yang's avatar
Edward Z. Yang committed
260 261 262 263 264
        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).
265

Edward Z. Yang's avatar
Edward Z. Yang committed
266 267 268
        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.
269

Gabor Greif's avatar
Gabor Greif committed
270
        [May 2003: actually I think this decision could easily be
Edward Z. Yang's avatar
Edward Z. Yang committed
271 272 273 274 275
        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.]
276

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

Edward Z. Yang's avatar
Edward Z. Yang committed
282 283 284 285
        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
286

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

Austin Seipp's avatar
Austin Seipp committed
289 290
************************************************************************
*                                                                      *
291
\subsection{Data constructors}
Austin Seipp's avatar
Austin Seipp committed
292 293 294
*                                                                      *
************************************************************************
-}
295

batterseapower's avatar
batterseapower committed
296
-- | A data constructor
Alan Zimmerman's avatar
Alan Zimmerman committed
297 298 299
--
-- - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnOpen',
--             'ApiAnnotation.AnnClose','ApiAnnotation.AnnComma'
300 301

-- For details on above see note [Api annotations] in ApiAnnotation
302
data DataCon
303
  = MkData {
Edward Z. Yang's avatar
Edward Z. Yang committed
304 305 306 307 308 309 310 311
        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
312 313
        --  data T a b c where
        --    MkT :: forall c y x b. (x~y,Ord x) => x -> y -> T (x,y) b c
Edward Z. Yang's avatar
Edward Z. Yang committed
314 315

        --      *** As represented internally
316 317 318
        --  data T a b c where
        --    MkT :: forall a b c. forall x y. (a~(x,y),x~y,Ord x)
        --        => x -> y -> T a b c
Edward Z. Yang's avatar
Edward Z. Yang committed
319 320 321 322
        --
        -- The next six fields express the type of the constructor, in pieces
        -- e.g.
        --
323
        --      dcUnivTyVars       = [a,b,c]
Ningning Xie's avatar
Ningning Xie committed
324
        --      dcExTyCoVars       = [x,y]
325
        --      dcUserTyVarBinders = [c,y,x,b]
326 327 328 329
        --      dcEqSpec           = [a~(x,y)]
        --      dcOtherTheta       = [x~y, Ord x]
        --      dcOrigArgTys       = [x,y]
        --      dcRepTyCon         = T
Edward Z. Yang's avatar
Edward Z. Yang committed
330

Ningning Xie's avatar
Ningning Xie committed
331 332 333 334 335 336
        -- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE
        -- TYVARS FOR THE PARENT TyCon. (This is a change (Oct05): previously,
        -- vanilla datacons guaranteed to have the same type variables as their
        -- parent TyCon, but that seems ugly.) They can be different in the case
        -- where a GADT constructor uses different names for the universal
        -- tyvars than does the tycon. For example:
337 338 339 340 341 342
        --
        --   data H a where
        --     MkH :: b -> H b
        --
        -- Here, the tyConTyVars of H will be [a], but the dcUnivTyVars of MkH
        -- will be [b].
343

Edward Z. Yang's avatar
Edward Z. Yang committed
344 345 346 347
        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.
Ningning Xie's avatar
Ningning Xie committed
348
                                -- That is: dcExTyCoVars = dcEqSpec = dcOtherTheta = []
Edward Z. Yang's avatar
Edward Z. Yang committed
349 350 351 352 353
                -- 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)

354
        -- Universally-quantified type vars [a,b,c]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
355 356
        -- INVARIANT: length matches arity of the dcRepTyCon
        -- INVARIANT: result type of data con worker is exactly (T a b c)
357 358
        -- COROLLARY: The dcUnivTyVars are always in one-to-one correspondence with
        --            the tyConTyVars of the parent TyCon
Ningning Xie's avatar
Ningning Xie committed
359
        dcUnivTyVars     :: [TyVar],
360

Ningning Xie's avatar
Ningning Xie committed
361 362 363 364
        -- Existentially-quantified type and coercion vars [x,y]
        -- For an example involving coercion variables,
        -- Why tycovars? See Note [Existential coercion variables]
        dcExTyCoVars     :: [TyCoVar],
365

Ningning Xie's avatar
Ningning Xie committed
366
        -- INVARIANT: the UnivTyVars and ExTyCoVars all have distinct OccNames
367
        -- Reason: less confusing, and easier to generate Iface syntax
Edward Z. Yang's avatar
Edward Z. Yang committed
368

Ningning Xie's avatar
Ningning Xie committed
369 370 371 372
        -- The type/coercion vars in the order the user wrote them [c,y,x,b]
        -- INVARIANT: the set of tyvars in dcUserTyVarBinders is exactly the set
        --            of tyvars (*not* covars) of dcExTyCoVars unioned with the
        --            set of dcUnivTyVars whose tyvars do not appear in dcEqSpec
373 374 375
        -- See Note [DataCon user type variable binders]
        dcUserTyVarBinders :: [TyVarBinder],

376
        dcEqSpec :: [EqSpec],   -- Equalities derived from the result type,
Ningning Xie's avatar
Ningning Xie committed
377 378 379 380
                                -- _as written by the programmer_.
                                -- Only non-dependent GADT equalities (dependent
                                -- GADT equalities are in the covars of
                                -- dcExTyCoVars).
381

Edward Z. Yang's avatar
Edward Z. Yang committed
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
                -- 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
422
        dcSrcBangs :: [HsSrcBang],
Simon Peyton Jones's avatar
Simon Peyton Jones committed
423
                -- See Note [Bangs on data constructor arguments]
424 425
                --
                -- The [HsSrcBang] as written by the programmer.
426
                --
Edward Z. Yang's avatar
Edward Z. Yang committed
427 428 429 430 431 432 433 434 435 436 437 438 439 440
                -- Matches 1-1 with dcOrigArgTys
                -- Hence 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.

        -- 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.
        dcWorkId :: Id,

        -- Constructor representation
441
        dcRep      :: DataConRep,
442

443
        -- Cached; see Note [DataCon arities]
Ningning Xie's avatar
Ningning Xie committed
444
        -- INVARIANT: dcRepArity    == length dataConRepArgTys + count isCoVar (dcExTyCoVars)
445
        -- INVARIANT: dcSourceArity == length dcOrigArgTys
446 447
        dcRepArity    :: Arity,
        dcSourceArity :: Arity,
448

Edward Z. Yang's avatar
Edward Z. Yang committed
449 450
        -- Result type of constructor is T t1..tn
        dcRepTyCon  :: TyCon,           -- Result tycon, T
451

Edward Z. Yang's avatar
Edward Z. Yang committed
452 453
        dcRepType   :: Type,    -- Type of the constructor
                                --      forall a x y. (a~(x,y), x~y, Ord x) =>
454
                                --        x -> y -> T a
Edward Z. Yang's avatar
Edward Z. Yang committed
455 456 457 458 459
                                -- (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
460
        --        MkT x y co1 co2 (d:Ord x) (v:r) (w:F s) -> ...
Edward Z. Yang's avatar
Edward Z. Yang committed
461 462 463 464
        -- 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.
465 466


Edward Z. Yang's avatar
Edward Z. Yang committed
467 468 469
        dcInfix :: Bool,        -- True <=> declared infix
                                -- Used for Template Haskell and 'deriving' only
                                -- The actual fixity is stored elsewhere
470

471 472
        dcPromoted :: TyCon    -- The promoted TyCon
                               -- See Note [Promoted data constructors] in TyCon
473 474
  }

475

476
{- Note [TyVarBinders in DataCons]
477
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
478
For the TyVarBinders in a DataCon and PatSyn:
479

480 481
 * Each argument flag is Inferred or Specified.
   None are Required. (A DataCon is a term-level function; see
Ningning Xie's avatar
Ningning Xie committed
482
   Note [No Required TyCoBinder in terms] in TyCoRep.)
483

484 485
Why do we need the TyVarBinders, rather than just the TyVars?  So that
we can construct the right type for the DataCon with its foralls
Ryan Scott's avatar
Ryan Scott committed
486
attributed the correct visibility.  That in turn governs whether you
487
can use visible type application at a call of the data constructor.
488

489 490 491
See also [DataCon user type variable binders] for an extended discussion on the
order in which TyVarBinders appear in a DataCon.

Ningning Xie's avatar
Ningning Xie committed
492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511
Note [Existential coercion variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

For now (Aug 2018) we can't write coercion quantifications in source Haskell, but
we can in Core. Consider having:

  data T :: forall k. k -> k -> Constraint where
    MkT :: forall k (a::k) (b::k). forall k' (c::k') (co::k'~k). (b~(c|>co))
        => T k a b

  dcUnivTyVars       = [k,a,b]
  dcExTyCoVars       = [k',c,co]
  dcUserTyVarBinders = [k,a,k',c]
  dcEqSpec           = [b~(c|>co)]
  dcOtherTheta       = []
  dcOrigArgTys       = []
  dcRepTyCon         = T

  Function call 'dataConKindEqSpec' returns [k'~k]

512 513 514 515 516 517 518
Note [DataCon arities]
~~~~~~~~~~~~~~~~~~~~~~
dcSourceArity does not take constraints into account,
but dcRepArity does.  For example:
   MkT :: Ord a => a -> T a
    dcSourceArity = 1
    dcRepArity    = 2
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

Note [DataCon user type variable binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In System FC, data constructor type signatures always quantify over all of
their universal type variables, followed by their existential type variables.
Normally, this isn't a problem, as most datatypes naturally quantify their type
variables in this order anyway. For example:

  data T a b = forall c. MkT b c

Here, we have `MkT :: forall {k} (a :: k) (b :: *) (c :: *). b -> c -> T a b`,
where k, a, and b are universal and c is existential. (The inferred variable k
isn't available for TypeApplications, hence why it's in braces.) This is a
perfectly reasonable order to use, as the syntax of H98-style datatypes
(+ ExistentialQuantification) suggests it.

Things become more complicated when GADT syntax enters the picture. Consider
this example:

  data X a where
    MkX :: forall b a. b -> Proxy a -> X a

If we adopt the earlier approach of quantifying all the universal variables
followed by all the existential ones, GHC would come up with this type
signature for MkX:

  MkX :: forall {k} (a :: k) (b :: *). b -> Proxy a -> X a

But this is not what we want at all! After all, if a user were to use
TypeApplications on MkX, they would expect to instantiate `b` before `a`,
as that's the order in which they were written in the `forall`. (See #11721.)
Instead, we'd like GHC to come up with this type signature:

  MkX :: forall {k} (b :: *) (a :: k). b -> Proxy a -> X a

In fact, even if we left off the explicit forall:

  data X a where
    MkX :: b -> Proxy a -> X a

Then a user should still expect `b` to be quantified before `a`, since
according to the rules of TypeApplications, in the absence of `forall` GHC
performs a stable topological sort on the type variables in the user-written
type signature, which would place `b` before `a`.

But as noted above, enacting this behavior is not entirely trivial, as System
FC demands the variables go in universal-then-existential order under the hood.
Our solution is thus to equip DataCon with two different sets of type
variables:

Ningning Xie's avatar
Ningning Xie committed
569 570 571 572 573
* dcUnivTyVars and dcExTyCoVars, for the universal type variable and existential
  type/coercion variables, respectively. Their order is irrelevant for the
  purposes of TypeApplications, and as a consequence, they do not come equipped
  with visibilities (that is, they are TyVars/TyCoVars instead of
  TyCoVarBinders).
574
* dcUserTyVarBinders, for the type variables binders in the order in which they
Ningning Xie's avatar
Ningning Xie committed
575 576 577
  originally arose in the user-written type signature. Their order *does* matter
  for TypeApplications, so they are full TyVarBinders, complete with
  visibilities.
578 579 580 581 582 583

This encoding has some redundancy. The set of tyvars in dcUserTyVarBinders
consists precisely of:

* The set of tyvars in dcUnivTyVars whose type variables do not appear in
  dcEqSpec, unioned with:
Ningning Xie's avatar
Ningning Xie committed
584 585 586 587 588 589 590 591 592 593 594 595 596 597
* The set of tyvars (*not* covars) in dcExTyCoVars
  No covars here because because they're not user-written

The word "set" is used above because the order in which the tyvars appear in
dcUserTyVarBinders can be completely different from the order in dcUnivTyVars or
dcExTyCoVars. That is, the tyvars in dcUserTyVarBinders are a permutation of
(tyvars of dcExTyCoVars + a subset of dcUnivTyVars). But aside from the
ordering, they in fact share the same type variables (with the same Uniques). We
sometimes refer to this as "the dcUserTyVarBinders invariant".

dcUserTyVarBinders, as the name suggests, is the one that users will see most of
the time. It's used when computing the type signature of a data constructor (see
dataConUserType), and as a result, it's what matters from a TypeApplications
perspective.
598 599
-}

600
-- | Data Constructor Representation
601
-- See Note [Data constructor workers and wrappers]
Edward Z. Yang's avatar
Edward Z. Yang committed
602
data DataConRep
603 604
  = -- NoDataConRep means that the data con has no wrapper
    NoDataConRep
605

606
    -- DCR means that the data con has a wrapper
Edward Z. Yang's avatar
Edward Z. Yang committed
607
  | DCR { dcr_wrap_id :: Id   -- Takes src args, unboxes/flattens,
608 609 610 611
                              -- and constructs the representation

        , dcr_boxer   :: DataConBoxer

Edward Z. Yang's avatar
Edward Z. Yang committed
612
        , dcr_arg_tys :: [Type]  -- Final, representation argument types,
613 614 615 616
                                 -- after unboxing and flattening,
                                 -- and *including* all evidence args

        , dcr_stricts :: [StrictnessMark]  -- 1-1 with dcr_arg_tys
617
                -- See also Note [Data-con worker strictness] in MkId.hs
618

Simon Peyton Jones's avatar
Simon Peyton Jones committed
619 620 621
        , dcr_bangs :: [HsImplBang]  -- The actual decisions made (including failures)
                                     -- about the original arguments; 1-1 with orig_arg_tys
                                     -- See Note [Bangs on data constructor arguments]
622

623 624
    }

625 626
-------------------------

627 628 629
-- | Haskell Source Bang
--
-- Bangs on data constructor arguments as the user wrote them in the
630 631
-- source code.
--
632 633
-- @(HsSrcBang _ SrcUnpack SrcLazy)@ and
-- @(HsSrcBang _ SrcUnpack NoSrcStrict)@ (without StrictData) makes no sense, we
634
-- emit a warning (in checkValidDataCon) and treat it like
635
-- @(HsSrcBang _ NoSrcUnpack SrcLazy)@
636
data HsSrcBang =
637
  HsSrcBang SourceText -- Note [Pragma source text] in BasicTypes
638 639
            SrcUnpackedness
            SrcStrictness
640
  deriving Data.Data
641

642 643 644
-- | Haskell Implementation Bang
--
-- Bangs of data constructor arguments as generated by the compiler
645 646
-- after consulting HsSrcBang, flags, etc.
data HsImplBang
647
  = HsLazy    -- ^ Lazy field, or one with an unlifted type
648 649 650 651
  | HsStrict  -- ^ Strict but not unpacked field
  | HsUnpack (Maybe Coercion)
    -- ^ Strict and unpacked field
    -- co :: arg-ty ~ product-ty HsBang
652
  deriving Data.Data
653

654 655 656
-- | Source Strictness
--
-- What strictness annotation the user wrote
657 658
data SrcStrictness = SrcLazy -- ^ Lazy, ie '~'
                   | SrcStrict -- ^ Strict, ie '!'
659
                   | NoSrcStrict -- ^ no strictness annotation
660
     deriving (Eq, Data.Data)
661

662 663 664
-- | Source Unpackedness
--
-- What unpackedness the user requested
665 666 667
data SrcUnpackedness = SrcUnpack -- ^ {-# UNPACK #-} specified
                     | SrcNoUnpack -- ^ {-# NOUNPACK #-} specified
                     | NoSrcUnpack -- ^ no unpack pragma
668
     deriving (Eq, Data.Data)
669 670


Simon Peyton Jones's avatar
Simon Peyton Jones committed
671

672
-------------------------
Edward Z. Yang's avatar
Edward Z. Yang committed
673
-- StrictnessMark is internal only, used to indicate strictness
674
-- of the DataCon *worker* fields
Edward Z. Yang's avatar
Edward Z. Yang committed
675
data StrictnessMark = MarkedStrict | NotMarkedStrict
676

677 678 679 680 681
-- | An 'EqSpec' is a tyvar/type pair representing an equality made in
-- rejigging a GADT constructor
data EqSpec = EqSpec TyVar
                     Type

Ningning Xie's avatar
Ningning Xie committed
682
-- | Make a non-dependent 'EqSpec'
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
mkEqSpec :: TyVar -> Type -> EqSpec
mkEqSpec tv ty = EqSpec tv ty

eqSpecTyVar :: EqSpec -> TyVar
eqSpecTyVar (EqSpec tv _) = tv

eqSpecType :: EqSpec -> Type
eqSpecType (EqSpec _ ty) = ty

eqSpecPair :: EqSpec -> (TyVar, Type)
eqSpecPair (EqSpec tv ty) = (tv, ty)

eqSpecPreds :: [EqSpec] -> ThetaType
eqSpecPreds spec = [ mkPrimEqPred (mkTyVarTy tv) ty
                   | EqSpec tv ty <- spec ]

-- | Substitute in an 'EqSpec'. Precondition: if the LHS of the EqSpec
-- is mapped in the substitution, it is mapped to a type variable, not
-- a full type.
substEqSpec :: TCvSubst -> EqSpec -> EqSpec
substEqSpec subst (EqSpec tv ty)
  = EqSpec tv' (substTy subst ty)
  where
    tv' = getTyVar "substEqSpec" (substTyVar subst tv)

708 709
-- | Filter out any 'TyVar's mentioned in an 'EqSpec'.
filterEqSpec :: [EqSpec] -> [TyVar] -> [TyVar]
710 711 712
filterEqSpec eq_spec
  = filter not_in_eq_spec
  where
713
    not_in_eq_spec var = all (not . (== var) . eqSpecTyVar) eq_spec
714

715 716 717
instance Outputable EqSpec where
  ppr (EqSpec tv ty) = ppr (tv, ty)

Simon Peyton Jones's avatar
Simon Peyton Jones committed
718 719 720 721 722 723 724
{- Note [Bangs on data constructor arguments]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
  data T = MkT !Int {-# UNPACK #-} !Int Bool

When compiling the module, GHC will decide how to represent
MkT, depending on the optimisation level, and settings of
725
flags like -funbox-small-strict-fields.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
726 727 728

Terminology:
  * HsSrcBang:  What the user wrote
729
                Constructors: HsSrcBang
Simon Peyton Jones's avatar
Simon Peyton Jones committed
730 731

  * HsImplBang: What GHC decided
732
                Constructors: HsLazy, HsStrict, HsUnpack
Simon Peyton Jones's avatar
Simon Peyton Jones committed
733

734
* If T was defined in this module, MkT's dcSrcBangs field
Simon Peyton Jones's avatar
Simon Peyton Jones committed
735
  records the [HsSrcBang] of what the user wrote; in the example
736 737 738
    [ HsSrcBang _ NoSrcUnpack SrcStrict
    , HsSrcBang _ SrcUnpack SrcStrict
    , HsSrcBang _ NoSrcUnpack NoSrcStrictness]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
739

740 741 742 743
* However, if T was defined in an imported module, the importing module
  must follow the decisions made in the original module, regardless of
  the flag settings in the importing module.
  Also see Note [Bangs on imported data constructors] in MkId
Simon Peyton Jones's avatar
Simon Peyton Jones committed
744 745 746

* The dcr_bangs field of the dcRep field records the [HsImplBang]
  If T was defined in this module, Without -O the dcr_bangs might be
747
    [HsStrict, HsStrict, HsLazy]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
748
  With -O it might be
749
    [HsStrict, HsUnpack _, HsLazy]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
750
  With -funbox-small-strict-fields it might be
751 752 753
    [HsUnpack, HsUnpack _, HsLazy]
  With -XStrictData it might be
    [HsStrict, HsUnpack _, HsStrict]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
754

755 756
Note [Data con representation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
757
The dcRepType field contains the type of the representation of a constructor
758
This may differ from the type of the constructor *Id* (built
759
by MkId.mkDataConId) for two reasons:
Edward Z. Yang's avatar
Edward Z. Yang committed
760 761
        a) the constructor Id may be overloaded, but the dictionary isn't stored
           e.g.    data Eq a => T a = MkT a a
762

Edward Z. Yang's avatar
Edward Z. Yang committed
763
        b) the constructor may store an unboxed version of a strict field.
764 765

Here's an example illustrating both:
Edward Z. Yang's avatar
Edward Z. Yang committed
766
        data Ord a => T a = MkT Int! a
767
Here
Edward Z. Yang's avatar
Edward Z. Yang committed
768
        T :: Ord a => Int -> a -> T a
769
but the rep type is
Edward Z. Yang's avatar
Edward Z. Yang committed
770
        Trep :: Int# -> a -> T a
771 772
Actually, the unboxed part isn't implemented yet!

773

774

Austin Seipp's avatar
Austin Seipp committed
775 776
************************************************************************
*                                                                      *
777
\subsection{Instances}
Austin Seipp's avatar
Austin Seipp committed
778 779 780
*                                                                      *
************************************************************************
-}
781

782 783 784 785 786 787 788 789 790 791 792 793 794
instance Eq DataCon where
    a == b = getUnique a == getUnique b
    a /= b = getUnique a /= getUnique b

instance Uniquable DataCon where
    getUnique = dcUnique

instance NamedThing DataCon where
    getName = dcName

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

795 796 797 798
instance OutputableBndr DataCon where
    pprInfixOcc con = pprInfixName (dataConName con)
    pprPrefixOcc con = pprPrefixName (dataConName con)

799 800 801 802 803
instance Data.Data DataCon where
    -- don't traverse?
    toConstr _   = abstractConstr "DataCon"
    gunfold _ _  = error "gunfold"
    dataTypeOf _ = mkNoRepType "DataCon"
804

805
instance Outputable HsSrcBang where
806
    ppr (HsSrcBang _ prag mark) = ppr prag <+> ppr mark
807 808

instance Outputable HsImplBang where
809 810 811 812
    ppr HsLazy                  = text "Lazy"
    ppr (HsUnpack Nothing)      = text "Unpacked"
    ppr (HsUnpack (Just co))    = text "Unpacked" <> parens (ppr co)
    ppr HsStrict                = text "StrictNotUnpacked"
813 814

instance Outputable SrcStrictness where
815 816 817
    ppr SrcLazy     = char '~'
    ppr SrcStrict   = char '!'
    ppr NoSrcStrict = empty
818 819

instance Outputable SrcUnpackedness where
820 821
    ppr SrcUnpack   = text "{-# UNPACK #-}"
    ppr SrcNoUnpack = text "{-# NOUNPACK #-}"
822
    ppr NoSrcUnpack = empty
823 824

instance Outputable StrictnessMark where
825
    ppr MarkedStrict    = text "!"
826 827 828 829 830 831 832 833 834 835 836
    ppr NotMarkedStrict = empty

instance Binary SrcStrictness where
    put_ bh SrcLazy     = putByte bh 0
    put_ bh SrcStrict   = putByte bh 1
    put_ bh NoSrcStrict = putByte bh 2

    get bh =
      do h <- getByte bh
         case h of
           0 -> return SrcLazy
837
           1 -> return SrcStrict
838 839 840 841 842 843 844 845 846 847 848 849 850
           _ -> return NoSrcStrict

instance Binary SrcUnpackedness where
    put_ bh SrcNoUnpack = putByte bh 0
    put_ bh SrcUnpack   = putByte bh 1
    put_ bh NoSrcUnpack = putByte bh 2

    get bh =
      do h <- getByte bh
         case h of
           0 -> return SrcNoUnpack
           1 -> return SrcUnpack
           _ -> return NoSrcUnpack
851

852
-- | Compare strictness annotations
853
eqHsBang :: HsImplBang -> HsImplBang -> Bool
854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872
eqHsBang HsLazy               HsLazy              = True
eqHsBang HsStrict             HsStrict            = True
eqHsBang (HsUnpack Nothing)   (HsUnpack Nothing)  = True
eqHsBang (HsUnpack (Just c1)) (HsUnpack (Just c2))
  = eqType (coercionType c1) (coercionType c2)
eqHsBang _ _                                       = False

isBanged :: HsImplBang -> Bool
isBanged (HsUnpack {}) = True
isBanged (HsStrict {}) = True
isBanged HsLazy        = False

isSrcStrict :: SrcStrictness -> Bool
isSrcStrict SrcStrict = True
isSrcStrict _ = False

isSrcUnpacked :: SrcUnpackedness -> Bool
isSrcUnpacked SrcUnpack = True
isSrcUnpacked _ = False
873 874 875 876

isMarkedStrict :: StrictnessMark -> Bool
isMarkedStrict NotMarkedStrict = False
isMarkedStrict _               = True   -- All others are strict
877

878
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
879
*                                                                      *
880
\subsection{Construction}
Austin Seipp's avatar
Austin Seipp committed
881
*                                                                      *
882
********************************************************************* -}
883

batterseapower's avatar
batterseapower committed
884
-- | Build a new data constructor
Edward Z. Yang's avatar
Edward Z. Yang committed
885
mkDataCon :: Name
Ningning Xie's avatar
Ningning Xie committed
886 887 888 889 890 891 892 893 894 895 896 897
          -> Bool           -- ^ Is the constructor declared infix?
          -> TyConRepName   -- ^  TyConRepName for the promoted TyCon
          -> [HsSrcBang]    -- ^ Strictness/unpack annotations, from user
          -> [FieldLabel]   -- ^ Field labels for the constructor,
                            -- if it is a record, otherwise empty
          -> [TyVar]        -- ^ Universals.
          -> [TyCoVar]      -- ^ Existentials.
          -> [TyVarBinder]  -- ^ User-written 'TyVarBinder's.
                            --   These must be Inferred/Specified.
                            --   See @Note [TyVarBinders in DataCons]@
          -> [EqSpec]       -- ^ GADT equalities
          -> KnotTied ThetaType -- ^ Theta-type occurring before the arguments proper
898 899 900 901 902 903 904 905 906
          -> [KnotTied Type]    -- ^ Original argument types
          -> KnotTied Type      -- ^ Original result type
          -> RuntimeRepInfo     -- ^ See comments on 'TyCon.RuntimeRepInfo'
          -> KnotTied TyCon     -- ^ Representation type constructor
          -> ConTag             -- ^ Constructor tag
          -> ThetaType          -- ^ The "stupid theta", context of the data
                                -- declaration e.g. @data Eq a => T a ...@
          -> Id                 -- ^ Worker Id
          -> DataConRep         -- ^ Representation
Edward Z. Yang's avatar
Edward Z. Yang committed
907
          -> DataCon
908 909
  -- Can get the tag from the TyCon

910
mkDataCon name declared_infix prom_info
Edward Z. Yang's avatar
Edward Z. Yang committed
911 912
          arg_stricts   -- Must match orig_arg_tys 1-1
          fields
913
          univ_tvs ex_tvs user_tvbs
Edward Z. Yang's avatar
Edward Z. Yang committed
914
          eq_spec theta
915
          orig_arg_tys orig_res_ty rep_info rep_tycon tag
Edward Z. Yang's avatar
Edward Z. Yang committed
916
          stupid_theta work_id rep
917
-- Warning: mkDataCon is not a good place to check certain invariants.
918
-- If the programmer writes the wrong result type in the decl, thus:
Edward Z. Yang's avatar
Edward Z. Yang committed
919
--      data T a where { MkT :: S }
920 921
-- 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,
Gabor Greif's avatar
Gabor Greif committed
922
-- so the error is detected properly... it's just that assertions here
923 924
-- are a little dodgy.

925
  = con
926
  where
927
    is_vanilla = null ex_tvs && null eq_spec && null theta
928

Edward Z. Yang's avatar
Edward Z. Yang committed
929 930
    con = MkData {dcName = name, dcUnique = nameUnique name,
                  dcVanilla = is_vanilla, dcInfix = declared_infix,
931
                  dcUnivTyVars = univ_tvs,
Ningning Xie's avatar
Ningning Xie committed
932
                  dcExTyCoVars = ex_tvs,
933
                  dcUserTyVarBinders = user_tvbs,
Edward Z. Yang's avatar
Edward Z. Yang committed
934 935 936 937 938
                  dcEqSpec = eq_spec,
                  dcOtherTheta = theta,
                  dcStupidTheta = stupid_theta,
                  dcOrigArgTys = orig_arg_tys, dcOrigResTy = orig_res_ty,
                  dcRepTyCon = rep_tycon,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
939
                  dcSrcBangs = arg_stricts,
Edward Z. Yang's avatar
Edward Z. Yang committed
940 941 942
                  dcFields = fields, dcTag = tag, dcRepType = rep_ty,
                  dcWorkId = work_id,
                  dcRep = rep,
943
                  dcSourceArity = length orig_arg_tys,
Ningning Xie's avatar
Ningning Xie committed
944
                  dcRepArity = length rep_arg_tys + count isCoVar ex_tvs,
945
                  dcPromoted = promoted }
946

Edward Z. Yang's avatar
Edward Z. Yang committed
947 948 949
        -- The 'arg_stricts' passed to mkDataCon are simply those for the
        -- source-language arguments.  We add extra ones for the
        -- dictionary arguments right here.
950

951
    rep_arg_tys = dataConRepArgTys con
952

953
    rep_ty =
954 955
      case rep of
        -- If the DataCon has no wrapper, then the worker's type *is* the
956 957
        -- user-facing type, so we can simply use dataConUserType.
        NoDataConRep -> dataConUserType con
958 959
        -- If the DataCon has a wrapper, then the worker's type is never seen
        -- by the user. The visibilities we pick do not matter here.
Ningning Xie's avatar
Ningning Xie committed
960
        DCR{} -> mkInvForAllTys univ_tvs $ mkTyCoInvForAllTys ex_tvs $
961
                 mkVisFunTys rep_arg_tys $
962
                 mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
963

964
      -- See Note [Promoted data constructors] in TyCon
965
    prom_tv_bndrs = [ mkNamedTyConBinder vis tv
Ningning Xie's avatar
Ningning Xie committed
966
                    | Bndr tv vis <- user_tvbs ]
967

968 969 970 971 972 973 974 975 976 977 978 979
    fresh_names = freshNames (map getName user_tvbs)
      -- fresh_names: make sure that the "anonymous" tyvars don't
      -- clash in name or unique with the universal/existential ones.
      -- Tiresome!  And unnecessary because these tyvars are never looked at
    prom_theta_bndrs = [ mkAnonTyConBinder InvisArg (mkTyVar n t)
     {- Invisible -}   | (n,t) <- fresh_names `zip` theta ]
    prom_arg_bndrs   = [ mkAnonTyConBinder VisArg (mkTyVar n t)
     {- Visible -}     | (n,t) <- dropList theta fresh_names `zip` orig_arg_tys ]
    prom_bndrs       = prom_tv_bndrs ++ prom_theta_bndrs ++ prom_arg_bndrs
    prom_res_kind    = orig_res_ty
    promoted         = mkPromotedDataCon con name prom_info prom_bndrs
                                         prom_res_kind roles rep_info
980

Ningning Xie's avatar
Ningning Xie committed
981 982
    roles = map (\tv -> if isTyVar tv then Nominal else Phantom)
                (univ_tvs ++ ex_tvs)
983
            ++ map (const Representational) (theta ++ orig_arg_tys)
984 985

freshNames :: [Name] -> [Name]
986 987
-- Make an infinite list of Names whose Uniques and OccNames
-- differ from those in the 'avoid' list
988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003
freshNames avoids
  = [ mkSystemName uniq occ
    | n <- [0..]
    , let uniq = mkAlphaTyVarUnique n
          occ = mkTyVarOccFS (mkFastString ('x' : show n))

    , not (uniq `elementOfUniqSet` avoid_uniqs)
    , not (occ `elemOccSet` avoid_occs) ]

  where
    avoid_uniqs :: UniqSet Unique
    avoid_uniqs = mkUniqSet (map getUnique avoids)

    avoid_occs :: OccSet
    avoid_occs = mkOccSet (map getOccName avoids)

batterseapower's avatar
batterseapower committed
1004
-- | The 'Name' of the 'DataCon', giving it a unique, rooted identification
1005 1006 1007
dataConName :: DataCon -> Name
dataConName = dcName

batterseapower's avatar
batterseapower committed
1008
-- | The tag used for ordering 'DataCon's
1009 1010 1011
dataConTag :: DataCon -> ConTag
dataConTag  = dcTag

1012 1013 1014
dataConTagZ :: DataCon -> ConTagZ
dataConTagZ con = dataConTag con - fIRST_TAG

batterseapower's avatar
batterseapower committed
1015
-- | The type constructor that we are building via this data constructor
1016
dataConTyCon :: DataCon -> TyCon
1017
dataConTyCon = dcRepTyCon
1018

1019 1020 1021 1022
-- | 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
Edward Z. Yang's avatar
Edward Z. Yang committed
1023
dataConOrigTyCon dc
1024 1025 1026
  | Just (tc, _) <- tyConFamInst_maybe (dcRepTyCon dc) = tc
  | otherwise                                          = dcRepTyCon dc

batterseapower's avatar
batterseapower committed
1027 1028
-- | The representation type of the data constructor, i.e. the sort
-- type that will represent values of this type at runtime
1029 1030
dataConRepType :: DataCon -> Type
dataConRepType = dcRepType
1031

batterseapower's avatar
batterseapower committed
1032
-- | Should the 'DataCon' be presented infix?
1033 1034 1035
dataConIsInfix :: DataCon -> Bool
dataConIsInfix = dcInfix

batterseapower's avatar
batterseapower committed
1036
-- | The universally-quantified type variables of the constructor
1037
dataConUnivTyVars :: DataCon -> [TyVar]
1038
dataConUnivTyVars (MkData { dcUnivTyVars = tvbs }) = tvbs
1039

Ningning Xie's avatar
Ningning Xie committed
1040 1041 1042 1043
-- | The existentially-quantified type/coercion variables of the constructor
-- including dependent (kind-) GADT equalities
dataConExTyCoVars :: DataCon -> [TyCoVar]
dataConExTyCoVars (MkData { dcExTyCoVars = tvbs }) = tvbs
1044

Ningning Xie's avatar
Ningning Xie committed
1045 1046 1047
-- | Both the universal and existential type/coercion variables of the constructor
dataConUnivAndExTyCoVars :: DataCon -> [TyCoVar]
dataConUnivAndExTyCoVars (MkData { dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tvs })
1048 1049 1050 1051 1052 1053 1054 1055
  = univ_tvs ++ ex_tvs

-- See Note [DataCon user type variable binders]
-- | The type variables of the constructor, in the order the user wrote them
dataConUserTyVars :: DataCon -> [TyVar]
dataConUserTyVars (MkData { dcUserTyVarBinders = tvbs }) = binderVars tvbs

-- See Note [DataCon user type variable binders]
Ningning Xie's avatar
Ningning Xie committed
1056
-- | 'TyCoVarBinder's for the type variables of the constructor, in the order the
1057 1058 1059
-- user wrote them
dataConUserTyVarBinders :: DataCon -> [TyVarBinder]
dataConUserTyVarBinders = dcUserTyVarBinders
1060

batterseapower's avatar
batterseapower committed
1061
-- | Equalities derived from the result type of the data constructor, as written
1062 1063 1064
-- by the programmer in any GADT declaration. This includes *all* GADT-like
-- equalities, including those written in by hand by the programmer.
dataConEqSpec :: DataCon -> [EqSpec]
Ningning Xie's avatar
Ningning Xie committed
1065 1066 1067
dataConEqSpec con@(MkData { dcEqSpec = eq_spec, dcOtherTheta = theta })
  = dataConKindEqSpec con
    ++ eq_spec ++
1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084
    [ spec   -- heterogeneous equality
    | Just (tc, [_k1, _k2, ty1, ty2]) <- map splitTyConApp_maybe theta
    , tc `hasKey` heqTyConKey
    , spec <- case (getTyVar_maybe ty1, getTyVar_maybe ty2) of
                    (Just tv1, _) -> [mkEqSpec tv1 ty2]
                    (_, Just tv2) -> [mkEqSpec tv2 ty1]
                    _             -> []
    ] ++
    [ spec   -- homogeneous equality
    | Just (tc, [_k, ty1, ty2]) <- map splitTyConApp_maybe theta
    , tc `hasKey` eqTyConKey
    , spec <- case (getTyVar_maybe ty1, getTyVar_maybe ty2) of
                    (Just tv1, _) -> [mkEqSpec tv1 ty2]
                    (_, Just tv2) -> [mkEqSpec tv2 ty1]
                    _             -> []
    ]

Ningning Xie's avatar
Ningning Xie committed
1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101
-- | Dependent (kind-level) equalities in a constructor.
-- There are extracted from the existential variables.
-- See Note [Existential coercion variables]
dataConKindEqSpec :: DataCon -> [EqSpec]
dataConKindEqSpec (MkData {dcExTyCoVars = ex_tcvs})
  -- It is used in 'dataConEqSpec' (maybe also 'dataConFullSig' in the future),
  -- which are frequently used functions.
  -- For now (Aug 2018) this function always return empty set as we don't really
  -- have coercion variables.
  -- In the future when we do, we might want to cache this information in DataCon
  -- so it won't be computed every time when aforementioned functions are called.
  = [ EqSpec tv ty
    | cv <- ex_tcvs
    , isCoVar cv
    , let (_, _, ty1, ty, _) = coVarKindsTypesRole cv
          tv = getTyVar "dataConKindEqSpec" ty1
    ]
1102

Ningning Xie's avatar
Ningning Xie committed
1103 1104
-- | The *full* constraints on the constructor type, including dependent GADT
-- equalities.
1105
dataConTheta :: DataCon -> ThetaType
Ningning Xie's avatar
Ningning Xie committed
1106 1107
dataConTheta con@(MkData { dcEqSpec = eq_spec, dcOtherTheta = theta })
  = eqSpecPreds (dataConKindEqSpec con ++ eq_spec) ++ theta
1108

batterseapower's avatar
batterseapower committed
1109 1110 1111 1112
-- | 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'
1113
dataConWorkId :: DataCon -> Id
1114
dataConWorkId dc = dcWorkId dc
1115

batterseapower's avatar
batterseapower committed
1116
-- | Get the Id of the 'DataCon' wrapper: a function that wraps the "actual"
Ningning Xie's avatar
Ningning Xie committed
1117 1118 1119 1120 1121
-- 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)
1122
dataConWrapId_maybe :: DataCon -> Maybe Id
1123 1124 1125
dataConWrapId_maybe dc = case dcRep dc of
                           NoDataConRep -> Nothing
                           DCR { dcr_wrap_id = wrap_id } -> Just wrap_id
1126