{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1998

\section[DataCon]{@DataCon@: Data Constructors}
-}

{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -Wno-orphans #-} -- Outputable, Binary

module GHC.Core.DataCon (
        -- * Main data types
        DataCon, DataConRep(..),
        SrcStrictness(..), SrcUnpackedness(..),
        HsSrcBang(..), HsImplBang(..),
        StrictnessMark(..),
        ConTag,
        DataConEnv,

        -- ** Equality specs
        EqSpec, mkEqSpec, eqSpecTyVar, eqSpecType,
        eqSpecPair, eqSpecPreds,

        -- ** Field labels
        FieldLabel(..), FieldLabelString,

        -- ** Type construction
        mkDataCon, fIRST_TAG,

        -- ** Type deconstruction
        dataConRepType, dataConInstSig, dataConFullSig,
        dataConName, dataConIdentity, dataConTag, dataConTagZ,
        dataConTyCon, dataConOrigTyCon,
        dataConWrapperType,
        dataConNonlinearType,
        dataConDisplayType,
        dataConUnivTyVars, dataConExTyCoVars, dataConUnivAndExTyCoVars,
        dataConUserTyVars, dataConUserTyVarBinders,
        dataConTheta,
        dataConStupidTheta,
        dataConOtherTheta,
        dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
        dataConInstOrigArgTys, dataConRepArgTys, dataConResRepTyArgs,
        dataConInstUnivs,
        dataConFieldLabels, dataConFieldType, dataConFieldType_maybe,
        dataConSrcBangs,
        dataConSourceArity, dataConRepArity,
        dataConIsInfix,
        dataConWorkId, dataConWrapId, dataConWrapId_maybe,
        dataConImplicitTyThings,
        dataConRepStrictness, dataConImplBangs, dataConBoxer,

        splitDataProductType_maybe,

        -- ** Predicates on DataCons
        isNullarySrcDataCon, isNullaryRepDataCon,
        isTupleDataCon, isBoxedTupleDataCon, isUnboxedTupleDataCon,
        isUnboxedSumDataCon, isCovertGadtDataCon,
        isVanillaDataCon, isNewDataCon, isTypeDataCon,
        classDataCon, dataConCannotMatch,
        dataConUserTyVarsNeedWrapper, checkDataConTyVars,
        isBanged, isMarkedStrict, cbvFromStrictMark, eqHsBang, isSrcStrict, isSrcUnpacked,
        specialPromotedDc,

        -- ** Promotion related functions
        promoteDataCon
    ) where

import GHC.Prelude

import Language.Haskell.Syntax.Basic

import {-# SOURCE #-} GHC.Types.Id.Make ( DataConBoxer )
import GHC.Core.Type as Type
import GHC.Core.Coercion
import GHC.Core.Unify
import GHC.Core.TyCon
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Compare( eqType )
import GHC.Core.Multiplicity
import {-# SOURCE #-} GHC.Types.TyThing
import GHC.Types.FieldLabel
import GHC.Types.SourceText
import GHC.Core.Class
import GHC.Types.Name
import GHC.Builtin.Names
import GHC.Core.Predicate
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Basic
import GHC.Data.FastString
import GHC.Unit.Types
import GHC.Utils.Binary
import GHC.Types.Unique.FM ( UniqFM )
import GHC.Types.Unique.Set
import GHC.Builtin.Uniques( mkAlphaTyVarUnique )
import GHC.Data.Graph.UnVar  -- UnVarSet and operations

import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain

import Data.ByteString (ByteString)
import qualified Data.ByteString.Builder as BSB
import qualified Data.ByteString.Lazy    as LBS
import qualified Data.Data as Data
import Data.Char
import Data.List( find )

import Language.Haskell.Syntax.Module.Name

{-
Note [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 [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.

* See Note [Data Constructor Naming] for how the worker and wrapper
  are named

* 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 wrapper 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.)

Note [The need for a wrapper]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Why might the wrapper have anything to do?  The full story is
in wrapper_reqd in GHC.Types.Id.Make.mkDataConRep.

* 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 wrapper 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 coercion
        [a] :: [a]~[a]

* Data family instances may do a cast on the result

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

* Datatype contexts require dropping some dictionary arguments.
  See Note [Instantiating stupid theta].

Note [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. A constructor's context
isn't necessarily the same as the data type's context, however. Per the
Haskell98 Report, the part of the datatype context that is used in a data
constructor is the largest subset of the datatype context that constrains
only the type variables free in the data constructor's field types. For
example, here are the types of T1 and T2:

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

Notice that T2's context is "thinned". Since its field is of type `a`, only
the part of the datatype context that mentions `a`—that is, `Eq a`—is
included in T2's context. On the other hand, T1's fields mention both `a`
and `b`, so T1's context includes all of the datatype context.

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.
(See Note [Instantiating stupid theta].)
It's a flaw in the language.

GHC has made some efforts to correct this flaw. In GHC, datatype contexts
are not available by default. Instead, one must explicitly opt in to them by
using the DatatypeContexts extension. To discourage their use, GHC has
deprecated DatatypeContexts.

Some other notes about stupid contexts:

* Stupid contexts can interact badly with `deriving`. For instance, it's
  unclear how to make this derived Functor instance typecheck:

    data Eq a => T a = MkT a
      deriving Functor

  This is because the derived instance would need to look something like
  `instance Functor T where ...`, but there is nowhere to mention the
  requisite `Eq a` constraint. For this reason, GHC will throw an error if a
  user attempts to derive an instance for Functor (or a Functor-like class)
  where the last type variable is used in a datatype context. For Generic(1),
  the requirements are even harsher, as stupid contexts are not allowed at all
  in derived Generic(1) instances. (We could consider relaxing this requirement
  somewhat, although no one has asked for this yet.)

  Stupid contexts are permitted when deriving instances of non-Functor-like
  classes, or when deriving instances of Functor-like classes where the last
  type variable isn't mentioned in the stupid context. For example, the
  following is permitted:

    data Show a => T a = MkT deriving Eq

  Note that because of the "thinning" behavior mentioned above, the generated
  Eq instance should not mention `Show a`, as the type of MkT doesn't require
  it. That is, the following should be generated (#20501):

    instance Eq (T a) where
      (MkT == MkT) = True

* It's not obvious how stupid contexts should interact with GADTs. For this
  reason, GHC disallows combining datatype contexts with GADT syntax. As a
  result, dcStupidTheta is always empty for data types defined using GADT
  syntax.

Note [Instantiating stupid theta]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider a data type with a "stupid theta" (see
Note [The stupid context]):

  data Ord a => T a = MkT (Maybe a)

We want to generate an Ord constraint for every use of MkT; but
we also want to allow visible type application, such as

   MkT @Int

To achieve this, the wrapper for a data (or newtype) constructor
with a datatype context contains a lambda which drops the dictionary
argments corresponding to the datatype context:

   /\a \(_d:Ord a). MkT @a

Notice that the wrapper discards the dictionary argument d.
We don't need it; it was only there to generate a Wanted constraint.
(That is why it is stupid.)

This all happens in GHC.Types.Id.Make.mkDataConRep.

************************************************************************
*                                                                      *
\subsection{Data constructors}
*                                                                      *
************************************************************************
-}

-- | A data constructor
--
-- - 'GHC.Parser.Annotation.AnnKeywordId' : 'GHC.Parser.Annotation.AnnOpen',
--             'GHC.Parser.Annotation.AnnClose','GHC.Parser.Annotation.AnnComma'

-- For details on above see Note [exact print annotations] in GHC.Parser.Annotation
data DataCon
  = MkData {
        DataCon -> Name
dcName    :: Name,      -- This is the name of the *source data con*
                                -- (see "Note [Data Constructor Naming]" above)
        DataCon -> Unique
dcUnique :: Unique,     -- Cached from Name
        DataCon -> Arity
dcTag    :: ConTag,     -- ^ Tag, used for ordering 'DataCon's

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

        --      *** As represented internally
        --  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
        --
        -- The next six fields express the type of the constructor, in pieces
        -- e.g.
        --
        --      dcUnivTyVars       = [a,b,c]
        --      dcExTyCoVars       = [x,y]
        --      dcUserTyVarBinders = [c,y,x,b]
        --      dcEqSpec           = [a~(x,y)]
        --      dcOtherTheta       = [x~y, Ord x]
        --      dcOrigArgTys       = [x,y]
        --      dcRepTyCon         = T

        -- 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:
        --
        --   data H a where
        --     MkH :: b -> H b
        --
        -- Here, the tyConTyVars of H will be [a], but the dcUnivTyVars of MkH
        -- will be [b].

        DataCon -> Bool
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: dcExTyCoVars = 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: Universally-quantified type vars [a,b,c]
        -- INVARIANT: length matches arity of the dcRepTyCon
        -- INVARIANT: result type of data con worker is exactly (T a b c)
        -- COROLLARY: The dcUnivTyVars are always in one-to-one correspondence with
        --            the tyConTyVars of the parent TyCon
        DataCon -> [TyVar]
dcUnivTyVars     :: [TyVar],

        -- Existentially-quantified type and coercion vars [x,y]
        -- For an example involving coercion variables,
        -- Why TyCoVars? See Note [Existential coercion variables]
        DataCon -> [TyVar]
dcExTyCoVars     :: [TyCoVar],

        -- INVARIANT: the UnivTyVars and ExTyCoVars all have distinct OccNames
        -- Reason: less confusing, and easier to generate Iface syntax

        -- The type/coercion vars in the order the user wrote them [c,y,x,b]
        -- INVARIANT(dataConTyVars): 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
        -- So dcUserTyVarBinders is a subset of (dcUnivTyVars ++ dcExTyCoVars)
        -- See Note [DataCon user type variable binders]
        DataCon -> [InvisTVBinder]
dcUserTyVarBinders :: [InvisTVBinder],

        DataCon -> [EqSpec]
dcEqSpec :: [EqSpec],   -- Equalities derived from the result type,
                                -- _as written by the programmer_.
                                -- Only non-dependent GADT equalities (dependent
                                -- GADT equalities are in the covars of
                                -- dcExTyCoVars).

                -- 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. Moreover, the
                -- only place in the DataCon where this 'a' will occur is in
                -- dcUnivTyVars. See [The dcEqSpec domain invariant].

                -- 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
        DataCon -> [Type]
dcOtherTheta :: ThetaType,  -- The other constraints in the data con's type
                                    -- other than those in the dcEqSpec

        DataCon -> [Type]
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.
                -- See Note [The stupid context].
                --
                -- 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.

        DataCon -> [Scaled Type]
dcOrigArgTys :: [Scaled Type],  -- Original argument types
                                        -- (before unboxing and flattening of strict fields)
        DataCon -> Type
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 dcOrigResTy is T [a], but the dcRepTyCon might be R:TList

        -- Now the strictness annotations and field labels of the constructor
        DataCon -> [HsSrcBang]
dcSrcBangs :: [HsSrcBang],
                -- See Note [Bangs on data constructor arguments]
                --
                -- The [HsSrcBang] as written by the programmer.
                --
                -- Matches 1-1 with dcOrigArgTys
                -- Hence length = dataConSourceArity dataCon

        DataCon -> [FieldLabel]
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.
        DataCon -> TyVar
dcWorkId :: Id,

        -- Constructor representation
        DataCon -> DataConRep
dcRep      :: DataConRep,

        -- Cached; see Note [DataCon arities]
        -- INVARIANT: dcRepArity    == length dataConRepArgTys + count isCoVar (dcExTyCoVars)
        -- INVARIANT: dcSourceArity == length dcOrigArgTys
        DataCon -> Arity
dcRepArity    :: Arity,
        DataCon -> Arity
dcSourceArity :: Arity,

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

        DataCon -> Type
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 GHC.Core.Lint.


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

        DataCon -> TyCon
dcPromoted :: TyCon    -- The promoted TyCon
                               -- See Note [Promoted data constructors] in GHC.Core.TyCon
  }


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

 * Each argument flag is Inferred or Specified.
   None are Required. (A DataCon is a term-level function; see
   Note [No Required PiTyBinder in terms] in GHC.Core.TyCo.Rep.)

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
attributed the correct visibility.  That in turn governs whether you
can use visible type application at a call of the data constructor.

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

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]

Note [DataCon arities]
~~~~~~~~~~~~~~~~~~~~~~
A `DataCon`'s source arity and core representation arity may differ:
`dcSourceArity` does not take constraints into account, but `dcRepArity` does.

The additional arguments taken into account by `dcRepArity` include quantified
dictionaries and coercion arguments, lifted and unlifted (despite the unlifted
coercion arguments having a zero-width runtime representation).
For example:
   MkT :: Ord a => a -> T a
    dcSourceArity = 1
    dcRepArity    = 2

   MkU :: (b ~ '[]) => U b
    dcSourceArity = 0
    dcRepArity    = 1


Note [DataCon user type variable binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A DataCon has two different sets of type variables:

* dcUserTyVarBinders, for the type variables binders in the order in which they
  originally arose in the user-written type signature.

  - They are the forall'd binders of the data con /wrapper/, which the user calls.

  - Their order *does* matter for TypeApplications, so they are full TyVarBinders,
    complete with visibilities.

* dcUnivTyVars and dcExTyCoVars, for the "true underlying" (i.e. of the data
  con worker) universal type variable and existential type/coercion variables,
  respectively.

  - They (i.e. univ ++ ex) are the forall'd variables of the data con /worker/

  - 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 ForAllTyBinders).

Often (dcUnivTyVars ++ dcExTyCoVars) = dcUserTyVarBinders; but they may differ
for three reasons, coming next:

--- Reason (R1): Order of quantification in GADT syntax ---

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`.

--- Reason (R2): GADT constructors quantify over different variables ---

GADT constructors may quantify over different variables than the worker
would.  Consider
   data T a b where
      MkT :: forall c d. c -> T [c] d

The dcUserTyVarBinders must be [c, d] -- that's what the user quantified over.
But c is actually existential, as it is not equal to either of the two
universal variables.

Here is what we'll get:

  dcUserTyVarBinders = [c, d]
  dcUnivTyVars = [a, d]
  dcExTyCoVars = [c]

Note that dcUnivTyVars contains `a` from the type header (the `data T a b`)
and `d` from the signature for MkT. This is done because d is used in place
of b in the result of MkT, and so we use the name d for the universal, as that
might improve error messages. On the other hand, we need to use a fresh name
for the first universal (recalling that the result of a worker must be the
type constructor applied to a sequence of plain variables), so we use `a`, from
the header. This choice of universals is made in GHC.Tc.TyCl.mkGADTVars.

Because c is not a universal, it is an existential. Here, we see that (even
ignoring order) dcUserTyVarBinders is not dcUnivTyVars ⋃ dcExTyCoVars, because
the latter has `a` while the former does not. To understand this better, let's
look at this type for the "true underlying" worker data con:

      MkT :: forall a d. forall c. (a ~# [c]) => c -> T a d

We see here that the `a` universal is connected with the `c` existential via
an equality constraint. It will always be the case (see the code in mkGADTVars)
that the universals not mentioned in dcUserTyVarBinders will be used in a
GADT equality -- that is, used on the left-hand side of an element of dcEqSpec:

  dcEqSpec = [a ~# [c]]

Putting this all together, all variables used on the left-hand side of an
equation in the dcEqSpec will be in dcUnivTyVars but *not* in
dcUserTyVarBinders.

--- Reason (R3): Kind equalities may have been solved ---

Consider now this case:

  type family F a where
    F Type = False
    F _    = True
  type T :: forall k. (F k ~ True) => k -> k -> Type
  data T a b where
    MkT :: T Maybe List

The constraint F k ~ True tells us that T does not want to be indexed by, say,
Int. Now let's consider the Core types involved:

  axiom for F: axF[0] :: F Type ~ False
               axF[1] :: forall a. F a ~ True   (a must be apart from Type)
  tycon: T :: forall k. (F k ~ True) -> k -> k -> Type
  wrapper: MkT :: T @(Type -> Type) @(Eq# (axF[1] (Type -> Type)) Maybe List
  worker:  MkT :: forall k (c :: F k ~ True) (a :: k) (b :: k).
                  (k ~# (Type -> Type), a ~# Maybe, b ~# List) =>
                  T @k @c a b

The key observation here is that the worker quantifies over c, while the wrapper
does not. The worker *must* quantify over c, because c is a universal variable,
and the result of the worker must be the type constructor applied to a sequence
of plain type variables. But the wrapper certainly does not need to quantify over
any evidence that F (Type -> Type) ~ True, as no variables are needed there.

(Aside: the c here is a regular type variable, *not* a coercion variable. This
is because F k ~ True is a *lifted* equality, not the unlifted ~#. This is why
we see Eq# in the type of the wrapper: Eq# boxes the unlifted ~# to become a
lifted ~. See also Note [The equality types story] in GHC.Builtin.Types.Prim about
Eq# and Note [Constraints in kinds] in GHC.Core.TyCo.Rep about having this constraint
in the first place.)

In this case, we'll have these fields of the DataCon:

  dcUserTyVarBinders = []    -- the wrapper quantifies over nothing
  dcUnivTyVars = [k, c, a, b]
  dcExTyCoVars = []  -- no existentials here, but a different constructor might have
  dcEqSpec = [k ~# (Type -> Type), a ~# Maybe, b ~# List]

Note that c is in the dcUserTyVars, but mentioned neither in the dcUserTyVarBinders nor
in the dcEqSpec. We thus have Reason (R3): a variable might be missing from the
dcUserTyVarBinders if its type's kind is Constraint.

(At one point, we thought that the dcEqSpec would have to be non-empty. But that
wouldn't account for silly cases like type T :: (True ~ True) => Type.)

--- End of Reasons ---

INVARIANT(dataConTyVars): the set of tyvars in dcUserTyVarBinders
consists of:

* The set of tyvars in dcUnivTyVars whose type variables do not appear in
  dcEqSpec, unioned with:

* The set of tyvars (*not* covars) in dcExTyCoVars
  No covars here because because they're not user-written

When comparing for equality, we ignore differences concerning type variables
whose kinds have kind Constraint.

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". It is checked
in checkDataConTyVars.

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 wrapper (see dataConWrapperType), and as a result,
it's what matters from a TypeApplications perspective.

Note [The dcEqSpec domain invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this example of a GADT constructor:

  data Y a where
    MkY :: Bool -> Y Bool

The user-written type of MkY is `Bool -> Y Bool`, but what is the underlying
Core type for MkY? There are two conceivable possibilities:

1. MkY :: forall a. (a ~# Bool) => Bool -> Y a
2. MkY :: forall a. (a ~# Bool) => a    -> Y a

In practice, GHC picks (1) as the Core type for MkY. This is because we
maintain an invariant that the type variables in the domain of dcEqSpec will
only ever appear in the dcUnivTyVars. As a consequence, the type variables in
the domain of dcEqSpec will /never/ appear in the dcExTyCoVars, dcOtherTheta,
dcOrigArgTys, or dcOrigResTy; these can only ever mention variables from
dcUserTyVarBinders, which excludes things in the domain of dcEqSpec.
(See Note [DataCon user type variable binders].) This explains why GHC would
not pick (2) as the Core type, since the argument type `a` mentions a type
variable in the dcEqSpec.

There are certain parts of the codebase where it is convenient to apply the
substitution arising from the dcEqSpec to the dcUnivTyVars in order to obtain
the user-written return type of a GADT constructor. A consequence of the
dcEqSpec domain invariant is that you /never/ need to apply the substitution
to any other part of the constructor type, as they don't require it.
-}

-- | Data Constructor Representation
-- See Note [Data constructor workers and wrappers]
data DataConRep
  = -- NoDataConRep means that the data con has no wrapper
    NoDataConRep

    -- DCR means that the data con has a wrapper
  | DCR { DataConRep -> TyVar
dcr_wrap_id :: Id   -- Takes src args, unboxes/flattens,
                              -- and constructs the representation

        , DataConRep -> DataConBoxer
dcr_boxer   :: DataConBoxer

        , DataConRep -> [Scaled Type]
dcr_arg_tys :: [Scaled Type]    -- Final, representation argument types,
                                          -- after unboxing and flattening,
                                          -- and *including* all evidence args

        , DataConRep -> [StrictnessMark]
dcr_stricts :: [StrictnessMark]  -- 1-1 with dcr_arg_tys
                -- See also Note [Data-con worker strictness]

        , DataConRep -> [HsImplBang]
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]

    }

type DataConEnv a = UniqFM DataCon a     -- Keyed by DataCon

-------------------------

-- | Haskell Source Bang
--
-- Bangs on data constructor arguments as the user wrote them in the
-- source code.
--
-- @(HsSrcBang _ SrcUnpack SrcLazy)@ and
-- @(HsSrcBang _ SrcUnpack NoSrcStrict)@ (without StrictData) makes no sense, we
-- emit a warning (in checkValidDataCon) and treat it like
-- @(HsSrcBang _ NoSrcUnpack SrcLazy)@
data HsSrcBang =
  HsSrcBang SourceText -- Note [Pragma source text] in GHC.Types.SourceText
            SrcUnpackedness
            SrcStrictness
  deriving Typeable HsSrcBang
Typeable HsSrcBang =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> HsSrcBang -> c HsSrcBang)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HsSrcBang)
-> (HsSrcBang -> Constr)
-> (HsSrcBang -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HsSrcBang))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsSrcBang))
-> ((forall b. Data b => b -> b) -> HsSrcBang -> HsSrcBang)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HsSrcBang -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HsSrcBang -> r)
-> (forall u. (forall d. Data d => d -> u) -> HsSrcBang -> [u])
-> (forall u.
    Arity -> (forall d. Data d => d -> u) -> HsSrcBang -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang)
-> Data HsSrcBang
HsSrcBang -> Constr
HsSrcBang -> DataType
(forall b. Data b => b -> b) -> HsSrcBang -> HsSrcBang
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Arity -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Arity -> (forall d. Data d => d -> u) -> HsSrcBang -> u
forall u. (forall d. Data d => d -> u) -> HsSrcBang -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsSrcBang -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsSrcBang -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsSrcBang
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsSrcBang -> c HsSrcBang
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsSrcBang)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsSrcBang)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsSrcBang -> c HsSrcBang
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsSrcBang -> c HsSrcBang
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsSrcBang
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsSrcBang
$ctoConstr :: HsSrcBang -> Constr
toConstr :: HsSrcBang -> Constr
$cdataTypeOf :: HsSrcBang -> DataType
dataTypeOf :: HsSrcBang -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsSrcBang)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsSrcBang)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsSrcBang)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsSrcBang)
$cgmapT :: (forall b. Data b => b -> b) -> HsSrcBang -> HsSrcBang
gmapT :: (forall b. Data b => b -> b) -> HsSrcBang -> HsSrcBang
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsSrcBang -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsSrcBang -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsSrcBang -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsSrcBang -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HsSrcBang -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> HsSrcBang -> [u]
$cgmapQi :: forall u. Arity -> (forall d. Data d => d -> u) -> HsSrcBang -> u
gmapQi :: forall u. Arity -> (forall d. Data d => d -> u) -> HsSrcBang -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsSrcBang -> m HsSrcBang
Data.Data

-- | Haskell Implementation Bang
--
-- Bangs of data constructor arguments as generated by the compiler
-- after consulting HsSrcBang, flags, etc.
data HsImplBang
  = HsLazy    -- ^ Lazy field, or one with an unlifted type
  | HsStrict Bool -- ^ Strict but not unpacked field
                  -- True <=> we could have unpacked, but opted not to
                  -- because of -O0.
                  -- See Note [Detecting useless UNPACK pragmas]
  | HsUnpack (Maybe Coercion)
    -- ^ Strict and unpacked field
    -- co :: arg-ty ~ product-ty HsBang
  deriving Typeable HsImplBang
Typeable HsImplBang =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> HsImplBang -> c HsImplBang)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HsImplBang)
-> (HsImplBang -> Constr)
-> (HsImplBang -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HsImplBang))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c HsImplBang))
-> ((forall b. Data b => b -> b) -> HsImplBang -> HsImplBang)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HsImplBang -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HsImplBang -> r)
-> (forall u. (forall d. Data d => d -> u) -> HsImplBang -> [u])
-> (forall u.
    Arity -> (forall d. Data d => d -> u) -> HsImplBang -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang)
-> Data HsImplBang
HsImplBang -> Constr
HsImplBang -> DataType
(forall b. Data b => b -> b) -> HsImplBang -> HsImplBang
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Arity -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Arity -> (forall d. Data d => d -> u) -> HsImplBang -> u
forall u. (forall d. Data d => d -> u) -> HsImplBang -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsImplBang -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsImplBang -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsImplBang
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsImplBang -> c HsImplBang
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsImplBang)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsImplBang)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsImplBang -> c HsImplBang
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HsImplBang -> c HsImplBang
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsImplBang
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HsImplBang
$ctoConstr :: HsImplBang -> Constr
toConstr :: HsImplBang -> Constr
$cdataTypeOf :: HsImplBang -> DataType
dataTypeOf :: HsImplBang -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsImplBang)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HsImplBang)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsImplBang)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsImplBang)
$cgmapT :: (forall b. Data b => b -> b) -> HsImplBang -> HsImplBang
gmapT :: (forall b. Data b => b -> b) -> HsImplBang -> HsImplBang
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsImplBang -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HsImplBang -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsImplBang -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HsImplBang -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HsImplBang -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> HsImplBang -> [u]
$cgmapQi :: forall u. Arity -> (forall d. Data d => d -> u) -> HsImplBang -> u
gmapQi :: forall u. Arity -> (forall d. Data d => d -> u) -> HsImplBang -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HsImplBang -> m HsImplBang
Data.Data



-------------------------
-- StrictnessMark is used to indicate strictness
-- of the DataCon *worker* fields
data StrictnessMark = MarkedStrict | NotMarkedStrict
    deriving StrictnessMark -> StrictnessMark -> Bool
(StrictnessMark -> StrictnessMark -> Bool)
-> (StrictnessMark -> StrictnessMark -> Bool) -> Eq StrictnessMark
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StrictnessMark -> StrictnessMark -> Bool
== :: StrictnessMark -> StrictnessMark -> Bool
$c/= :: StrictnessMark -> StrictnessMark -> Bool
/= :: StrictnessMark -> StrictnessMark -> Bool
Eq

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

-- | Make a non-dependent 'EqSpec'
mkEqSpec :: TyVar -> Type -> EqSpec
mkEqSpec :: TyVar -> Type -> EqSpec
mkEqSpec TyVar
tv Type
ty = TyVar -> Type -> EqSpec
EqSpec TyVar
tv Type
ty

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

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

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

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

instance Outputable EqSpec where
  ppr :: EqSpec -> SDoc
ppr (EqSpec TyVar
tv Type
ty) = (TyVar, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyVar
tv, Type
ty)

{- Note [Data-con worker strictness]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Notice that we do *not* say the worker Id is strict even if the data
constructor is declared strict
     e.g.    data T = MkT ![Int] Bool
Even though most often the evals are done by the *wrapper* $WMkT, there are
situations in which tag inference will re-insert evals around the worker.
So for all intents and purposes the *worker* MkT is strict, too!

Unfortunately, if we exposed accurate strictness of DataCon workers, we'd
see the following transformation:

  f xs = case xs of xs' { __DEFAULT -> ... case MkT xs b of x { __DEFAULT -> [x] } } -- DmdAnal: Strict in xs
  ==> { drop-seq, binder swap on xs' }
  f xs = case MkT xs b of x { __DEFAULT -> [x] } -- DmdAnal: Still strict in xs
  ==> { case-to-let }
  f xs = let x = MkT xs' b in [x] -- DmdAnal: No longer strict in xs!

I.e., we are ironically losing strictness in `xs` by dropping the eval on `xs`
and then doing case-to-let. The issue is that `exprIsHNF` currently says that
every DataCon worker app is a value. The implicit assumption is that surrounding
evals will have evaluated strict fields like `xs` before! But now that we had
just dropped the eval on `xs`, that assumption is no longer valid.

Long story short: By keeping the demand signature lazy, the Simplifier will not
drop the eval on `xs` and using `exprIsHNF` to decide case-to-let and others
remains sound.

Similarly, during demand analysis in dmdTransformDataConSig, we bump up the
field demand with `C_01`, *not* `C_11`, because the latter exposes too much
strictness that will drop the eval on `xs` above.

This issue is discussed at length in
"Failed idea: no wrappers for strict data constructors" in #21497 and #22475.

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
flags like -funbox-small-strict-fields.

Terminology:
  * HsSrcBang:  What the user wrote
                Constructors: HsSrcBang

  * HsImplBang: What GHC decided
                Constructors: HsLazy, HsStrict, HsUnpack

* If T was defined in this module, MkT's dcSrcBangs field
  records the [HsSrcBang] of what the user wrote; in the example
    [ HsSrcBang _ NoSrcUnpack SrcStrict
    , HsSrcBang _ SrcUnpack SrcStrict
    , HsSrcBang _ NoSrcUnpack NoSrcStrictness]

* 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 GHC.Types.Id.Make

* 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
    [HsStrict _, HsStrict _, HsLazy]
  With -O it might be
    [HsStrict _, HsUnpack _, HsLazy]
  With -funbox-small-strict-fields it might be
    [HsUnpack, HsUnpack _, HsLazy]
  With -XStrictData it might be
    [HsStrict _, HsUnpack _, HsStrict _]

Note [Detecting useless UNPACK pragmas]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We want to issue a warning when there's an UNPACK pragma in the source code,
but we decided not to unpack.
However, when compiling with -O0, we never unpack, and that'd generate
spurious warnings.
Therefore, we remember in HsStrict a boolean flag, whether we _could_
have unpacked. This flag is set in GHC.Types.Id.Make.dataConSrcToImplBang.
Then, in GHC.Tc.TyCl.checkValidDataCon (sub-function check_bang),
if the user wrote an `{-# UNPACK #-}` pragma (i.e. HsSrcBang contains SrcUnpack)
we consult HsImplBang:

  HsUnpack _     => field unpacked, no warning
                    Example: data T = MkT {-# UNPACK #-} !Int   [with -O]
  HsStrict True  => field not unpacked because -O0, no warning
                    Example: data T = MkT {-# UNPACK #-} !Int   [with -O0]
  HsStrict False => field not unpacked, warning
                    Example: data T = MkT {-# UNPACK #-} !(Int -> Int)
  HsLazy         => field not unpacked, warning
                    This can happen in two scenarios:

                    1) UNPACK without a bang
                    Example: data T = MkT {-# UNPACK #-} Int
                    This will produce a warning about missing ! before UNPACK.

                    2) UNPACK of an unlifted datatype
                    Because of bug #20204, we currently do not unpack type T,
                    and therefore issue a warning:
                    type IntU :: UnliftedType
                    data IntU = IntU Int#
                    data T = Test {-# UNPACK #-} IntU

The boolean flag is used only for this warning.
See #11270 for motivation.

Note [Data con representation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The dcRepType field contains the type of the representation of a constructor
This may differ from the type of the constructor *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.

So whenever this module talks about the representation of a data constructor
what it means is the DataCon with all Unpacking having been applied.
We can think of this as the Core representation.

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

Note that this representation is still *different* from runtime
representation. (Which is what STG uses after unarise).

This is how T would end up being used in STG post-unarise:

  let x = T 1# y
  in ...
      case x of
        T int a -> ...

The Void# argument is dropped and the boxed int is replaced by an unboxed
one. In essence we only generate binders for runtime relevant values.

We also flatten out unboxed tuples in this process. See the unarise
pass for details on how this is done. But as an example consider
`data S = MkS Bool (# Bool | Char #)` which when matched on would
result in an alternative with three binders like this

    MkS bool tag tpl_field ->

See Note [Translating unboxed sums to unboxed tuples] and Note [Unarisation]
for the details of this transformation.


************************************************************************
*                                                                      *
\subsection{Instances}
*                                                                      *
************************************************************************
-}

instance Eq DataCon where
    DataCon
a == :: DataCon -> DataCon -> Bool
== DataCon
b = DataCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique DataCon
a Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique DataCon
b
    DataCon
a /= :: DataCon -> DataCon -> Bool
/= DataCon
b = DataCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique DataCon
a Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
/= DataCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique DataCon
b

instance Uniquable DataCon where
    getUnique :: DataCon -> Unique
getUnique = DataCon -> Unique
dcUnique

instance NamedThing DataCon where
    getName :: DataCon -> Name
getName = DataCon -> Name
dcName

instance Outputable DataCon where
    ppr :: DataCon -> SDoc
ppr DataCon
con = Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (DataCon -> Name
dataConName DataCon
con)

instance OutputableBndr DataCon where
    pprInfixOcc :: DataCon -> SDoc
pprInfixOcc DataCon
con = Name -> SDoc
forall a. (Outputable a, NamedThing a) => a -> SDoc
pprInfixName (DataCon -> Name
dataConName DataCon
con)
    pprPrefixOcc :: DataCon -> SDoc
pprPrefixOcc DataCon
con = Name -> SDoc
forall a. NamedThing a => a -> SDoc
pprPrefixName (DataCon -> Name
dataConName DataCon
con)

instance Data.Data DataCon where
    -- don't traverse?
    toConstr :: DataCon -> Constr
toConstr DataCon
_   = String -> Constr
abstractConstr String
"DataCon"
    gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DataCon
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_  = String -> Constr -> c DataCon
forall a. HasCallStack => String -> a
error String
"gunfold"
    dataTypeOf :: DataCon -> DataType
dataTypeOf DataCon
_ = String -> DataType
mkNoRepType String
"DataCon"

instance Outputable HsSrcBang where
    ppr :: HsSrcBang -> SDoc
ppr (HsSrcBang SourceText
_ SrcUnpackedness
prag SrcStrictness
mark) = SrcUnpackedness -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcUnpackedness
prag SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SrcStrictness -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcStrictness
mark

instance Outputable HsImplBang where
    ppr :: HsImplBang -> SDoc
ppr HsImplBang
HsLazy                  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Lazy"
    ppr (HsUnpack Maybe Coercion
Nothing)      = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Unpacked"
    ppr (HsUnpack (Just Coercion
co))    = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Unpacked" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
    ppr (HsStrict Bool
b)            = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"StrictNotUnpacked" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
b)

instance Outputable SrcStrictness where
    ppr :: SrcStrictness -> SDoc
ppr SrcStrictness
SrcLazy     = Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'~'
    ppr SrcStrictness
SrcStrict   = Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'!'
    ppr SrcStrictness
NoSrcStrict = SDoc
forall doc. IsOutput doc => doc
empty

instance Outputable SrcUnpackedness where
    ppr :: SrcUnpackedness -> SDoc
ppr SrcUnpackedness
SrcUnpack   = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"{-# UNPACK #-}"
    ppr SrcUnpackedness
SrcNoUnpack = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"{-# NOUNPACK #-}"
    ppr SrcUnpackedness
NoSrcUnpack = SDoc
forall doc. IsOutput doc => doc
empty

instance Outputable StrictnessMark where
    ppr :: StrictnessMark -> SDoc
ppr StrictnessMark
MarkedStrict    = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"!"
    ppr StrictnessMark
NotMarkedStrict = SDoc
forall doc. IsOutput doc => doc
empty

instance Binary StrictnessMark where
    put_ :: BinHandle -> StrictnessMark -> IO ()
put_ BinHandle
bh StrictnessMark
NotMarkedStrict = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
0
    put_ BinHandle
bh StrictnessMark
MarkedStrict    = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1
    get :: BinHandle -> IO StrictnessMark
get BinHandle
bh =
      do Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
         case Word8
h of
           Word8
0 -> StrictnessMark -> IO StrictnessMark
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return StrictnessMark
NotMarkedStrict
           Word8
1 -> StrictnessMark -> IO StrictnessMark
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return StrictnessMark
MarkedStrict
           Word8
_ -> String -> IO StrictnessMark
forall a. HasCallStack => String -> a
panic String
"Invalid binary format"

instance Binary SrcStrictness where
    put_ :: BinHandle -> SrcStrictness -> IO ()
put_ BinHandle
bh SrcStrictness
SrcLazy     = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
0
    put_ BinHandle
bh SrcStrictness
SrcStrict   = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1
    put_ BinHandle
bh SrcStrictness
NoSrcStrict = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
2

    get :: BinHandle -> IO SrcStrictness
get BinHandle
bh =
      do Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
         case Word8
h of
           Word8
0 -> SrcStrictness -> IO SrcStrictness
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SrcStrictness
SrcLazy
           Word8
1 -> SrcStrictness -> IO SrcStrictness
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SrcStrictness
SrcStrict
           Word8
_ -> SrcStrictness -> IO SrcStrictness
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SrcStrictness
NoSrcStrict

instance Binary SrcUnpackedness where
    put_ :: BinHandle -> SrcUnpackedness -> IO ()
put_ BinHandle
bh SrcUnpackedness
SrcNoUnpack = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
0
    put_ BinHandle
bh SrcUnpackedness
SrcUnpack   = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1
    put_ BinHandle
bh SrcUnpackedness
NoSrcUnpack = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
2

    get :: BinHandle -> IO SrcUnpackedness
get BinHandle
bh =
      do Word8
h <- BinHandle -> IO Word8
getByte BinHandle
bh
         case Word8
h of
           Word8
0 -> SrcUnpackedness -> IO SrcUnpackedness
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SrcUnpackedness
SrcNoUnpack
           Word8
1 -> SrcUnpackedness -> IO SrcUnpackedness
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SrcUnpackedness
SrcUnpack
           Word8
_ -> SrcUnpackedness -> IO SrcUnpackedness
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SrcUnpackedness
NoSrcUnpack

-- | Compare strictness annotations
eqHsBang :: HsImplBang -> HsImplBang -> Bool
eqHsBang :: HsImplBang -> HsImplBang -> Bool
eqHsBang HsImplBang
HsLazy               HsImplBang
HsLazy              = Bool
True
eqHsBang (HsStrict Bool
_)         (HsStrict Bool
_)        = Bool
True
eqHsBang (HsUnpack Maybe Coercion
Nothing)   (HsUnpack Maybe Coercion
Nothing)  = Bool
True
eqHsBang (HsUnpack (Just Coercion
c1)) (HsUnpack (Just Coercion
c2))
  = Type -> Type -> Bool
eqType (Coercion -> Type
coercionType Coercion
c1) (Coercion -> Type
coercionType Coercion
c2)
eqHsBang HsImplBang
_ HsImplBang
_                                       = Bool
False

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

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

isSrcUnpacked :: SrcUnpackedness -> Bool
isSrcUnpacked :: SrcUnpackedness -> Bool
isSrcUnpacked SrcUnpackedness
SrcUnpack = Bool
True
isSrcUnpacked SrcUnpackedness
_ = Bool
False

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

cbvFromStrictMark :: StrictnessMark -> CbvMark
cbvFromStrictMark :: StrictnessMark -> CbvMark
cbvFromStrictMark StrictnessMark
NotMarkedStrict = CbvMark
NotMarkedCbv
cbvFromStrictMark StrictnessMark
MarkedStrict = CbvMark
MarkedCbv


{- *********************************************************************
*                                                                      *
\subsection{Construction}
*                                                                      *
********************************************************************* -}

-- | Build a new data constructor
mkDataCon :: Name
          -> 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.
          -> [InvisTVBinder]    -- ^ 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
          -> [KnotTied (Scaled Type)]    -- ^ Original argument types
          -> KnotTied Type      -- ^ Original result type
          -> PromDataConInfo    -- ^ See comments on 'GHC.Core.TyCon.PromDataConInfo'
          -> 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
          -> DataCon
  -- Can get the tag from the TyCon

mkDataCon :: Name
-> Bool
-> Name
-> [HsSrcBang]
-> [FieldLabel]
-> [TyVar]
-> [TyVar]
-> [InvisTVBinder]
-> [EqSpec]
-> [Type]
-> [Scaled Type]
-> Type
-> PromDataConInfo
-> TyCon
-> Arity
-> [Type]
-> TyVar
-> DataConRep
-> DataCon
mkDataCon Name
name Bool
declared_infix Name
prom_info
          [HsSrcBang]
arg_stricts   -- Must match orig_arg_tys 1-1
          [FieldLabel]
fields
          [TyVar]
univ_tvs [TyVar]
ex_tvs [InvisTVBinder]
user_tvbs
          [EqSpec]
eq_spec [Type]
theta
          [Scaled Type]
orig_arg_tys Type
orig_res_ty PromDataConInfo
rep_info TyCon
rep_tycon Arity
tag
          [Type]
stupid_theta TyVar
work_id DataConRep
rep
-- Warning: mkDataCon is not a good place to check certain 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 assertions here
-- are a little dodgy.

  = DataCon
con
  where
    is_vanilla :: Bool
is_vanilla = [TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
ex_tvs Bool -> Bool -> Bool
&& [EqSpec] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EqSpec]
eq_spec Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta

    con :: DataCon
con = MkData {dcName :: Name
dcName = Name
name, dcUnique :: Unique
dcUnique = Name -> Unique
nameUnique Name
name,
                  dcVanilla :: Bool
dcVanilla = Bool
is_vanilla, dcInfix :: Bool
dcInfix = Bool
declared_infix,
                  dcUnivTyVars :: [TyVar]
dcUnivTyVars = [TyVar]
univ_tvs,
                  dcExTyCoVars :: [TyVar]
dcExTyCoVars = [TyVar]
ex_tvs,
                  dcUserTyVarBinders :: [InvisTVBinder]
dcUserTyVarBinders = [InvisTVBinder]
user_tvbs,
                  dcEqSpec :: [EqSpec]
dcEqSpec = [EqSpec]
eq_spec,
                  dcOtherTheta :: [Type]
dcOtherTheta = [Type]
theta,
                  dcStupidTheta :: [Type]
dcStupidTheta = [Type]
stupid_theta,
                  dcOrigArgTys :: [Scaled Type]
dcOrigArgTys = [Scaled Type]
orig_arg_tys, dcOrigResTy :: Type
dcOrigResTy = Type
orig_res_ty,
                  dcRepTyCon :: TyCon
dcRepTyCon = TyCon
rep_tycon,
                  dcSrcBangs :: [HsSrcBang]
dcSrcBangs = [HsSrcBang]
arg_stricts,
                  dcFields :: [FieldLabel]
dcFields = [FieldLabel]
fields, dcTag :: Arity
dcTag = Arity
tag, dcRepType :: Type
dcRepType = Type
rep_ty,
                  dcWorkId :: TyVar
dcWorkId = TyVar
work_id,
                  dcRep :: DataConRep
dcRep = DataConRep
rep,
                  dcSourceArity :: Arity
dcSourceArity = [Scaled Type] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Scaled Type]
orig_arg_tys,
                  dcRepArity :: Arity
dcRepArity = [Scaled Type] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Scaled Type]
rep_arg_tys Arity -> Arity -> Arity
forall a. Num a => a -> a -> a
+ (TyVar -> Bool) -> [TyVar] -> Arity
forall a. (a -> Bool) -> [a] -> Arity
count TyVar -> Bool
isCoVar [TyVar]
ex_tvs,
                  dcPromoted :: TyCon
dcPromoted = TyCon
promoted }

        -- The 'arg_stricts' passed to mkDataCon are simply those for the
        -- source-language arguments.  We add extra ones for the
        -- dictionary arguments right here.

    rep_arg_tys :: [Scaled Type]
rep_arg_tys = DataCon -> [Scaled Type]
dataConRepArgTys DataCon
con

    rep_ty :: Type
rep_ty =
      case DataConRep
rep of
        -- If the DataCon has no wrapper, then the worker's type *is* the
        -- user-facing type, so we can simply use dataConWrapperType.
        DataConRep
NoDataConRep -> DataCon -> Type
dataConWrapperType DataCon
con
        -- 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.
        DCR{} -> [TyVar] -> Type -> Type
mkInfForAllTys [TyVar]
univ_tvs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Type -> Type
mkTyCoInvForAllTys [TyVar]
ex_tvs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                 [Scaled Type] -> Type -> Type
mkScaledFunctionTys [Scaled Type]
rep_arg_tys (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                 TyCon -> [Type] -> Type
mkTyConApp TyCon
rep_tycon ([TyVar] -> [Type]
mkTyVarTys [TyVar]
univ_tvs)
                 -- res_arg_tys is a mixture of TypeLike and ConstraintLike,
                 -- so we don't know which FunTyFlag to use
                 -- Hence using mkScaledFunctionTys.

      -- See Note [Promoted data constructors] in GHC.Core.TyCon
    prom_tv_bndrs :: [TyConBinder]
prom_tv_bndrs = [ ForAllTyFlag -> TyVar -> TyConBinder
mkNamedTyConBinder (Specificity -> ForAllTyFlag
Invisible Specificity
spec) TyVar
tv
                    | Bndr TyVar
tv Specificity
spec <- [InvisTVBinder]
user_tvbs ]

    fresh_names :: [Name]
fresh_names = [Name] -> [Name]
freshNames ((InvisTVBinder -> Name) -> [InvisTVBinder] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map InvisTVBinder -> Name
forall a. NamedThing a => a -> Name
getName [InvisTVBinder]
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 :: [TyConBinder]
prom_theta_bndrs = [ TyVar -> TyConBinder
mkInvisAnonTyConBinder (Name -> Type -> TyVar
mkTyVar Name
n Type
t)
     {- Invisible -}   | (Name
n,Type
t) <- [Name]
fresh_names [Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Type]
theta ]
    prom_arg_bndrs :: [TyConBinder]
prom_arg_bndrs   = [ TyVar -> TyConBinder
mkAnonTyConBinder (Name -> Type -> TyVar
mkTyVar Name
n Type
t)
     {- Visible -}     | (Name
n,Type
t) <- [Type] -> [Name] -> [Name]
forall b a. [b] -> [a] -> [a]
dropList [Type]
theta [Name]
fresh_names [Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
orig_arg_tys ]
    prom_bndrs :: [TyConBinder]
prom_bndrs       = [TyConBinder]
prom_tv_bndrs [TyConBinder] -> [TyConBinder] -> [TyConBinder]
forall a. [a] -> [a] -> [a]
++ [TyConBinder]
prom_theta_bndrs [TyConBinder] -> [TyConBinder] -> [TyConBinder]
forall a. [a] -> [a] -> [a]
++ [TyConBinder]
prom_arg_bndrs
    prom_res_kind :: Type
prom_res_kind    = Type
orig_res_ty
    promoted :: TyCon
promoted         = DataCon
-> Name
-> Name
-> [TyConBinder]
-> Type
-> [Role]
-> PromDataConInfo
-> TyCon
mkPromotedDataCon DataCon
con Name
name Name
prom_info [TyConBinder]
prom_bndrs
                                         Type
prom_res_kind [Role]
roles PromDataConInfo
rep_info

    roles :: [Role]
roles = (TyVar -> Role) -> [TyVar] -> [Role]
forall a b. (a -> b) -> [a] -> [b]
map (\TyVar
tv -> if TyVar -> Bool
isTyVar TyVar
tv then Role
Nominal else Role
Phantom)
                ([TyVar]
univ_tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
ex_tvs)
            [Role] -> [Role] -> [Role]
forall a. [a] -> [a] -> [a]
++ (Type -> Role) -> [Type] -> [Role]
forall a b. (a -> b) -> [a] -> [b]
map (Role -> Type -> Role
forall a b. a -> b -> a
const Role
Representational) ([Type]
theta [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
orig_arg_tys)

freshNames :: [Name] -> [Name]
-- Make an infinite list of Names whose Uniques and OccNames
-- differ from those in the 'avoid' list
freshNames :: [Name] -> [Name]
freshNames [Name]
avoids
  = [ Unique -> OccName -> Name
mkSystemName Unique
uniq OccName
occ
    | Arity
n <- [Arity
0..]
    , let uniq :: Unique
uniq = Arity -> Unique
mkAlphaTyVarUnique Arity
n
          occ :: OccName
occ = FastString -> OccName
mkTyVarOccFS (String -> FastString
mkFastString (Char
'x' Char -> String -> String
forall a. a -> [a] -> [a]
: Arity -> String
forall a. Show a => a -> String
show Arity
n))

    , Bool -> Bool
not (Unique
uniq Unique -> UniqSet Unique -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
`elementOfUniqSet` UniqSet Unique
avoid_uniqs)
    , Bool -> Bool
not (OccName
occ OccName -> OccSet -> Bool
`elemOccSet` OccSet
avoid_occs) ]

  where
    avoid_uniqs :: UniqSet Unique
    avoid_uniqs :: UniqSet Unique
avoid_uniqs = [Unique] -> UniqSet Unique
forall a. Uniquable a => [a] -> UniqSet a
mkUniqSet ((Name -> Unique) -> [Name] -> [Unique]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Unique
forall a. Uniquable a => a -> Unique
getUnique [Name]
avoids)

    avoid_occs :: OccSet
    avoid_occs :: OccSet
avoid_occs = [OccName] -> OccSet
mkOccSet ((Name -> OccName) -> [Name] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> OccName
forall a. NamedThing a => a -> OccName
getOccName [Name]
avoids)

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

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

dataConTagZ :: DataCon -> ConTagZ
dataConTagZ :: DataCon -> Arity
dataConTagZ DataCon
con = DataCon -> Arity
dataConTag DataCon
con Arity -> Arity -> Arity
forall a. Num a => a -> a -> a
- Arity
fIRST_TAG

-- | The type constructor that we are building via this data constructor
dataConTyCon :: DataCon -> TyCon
dataConTyCon :: DataCon -> TyCon
dataConTyCon = DataCon -> TyCon
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 :: DataCon -> TyCon
dataConOrigTyCon DataCon
dc
  | Just (TyCon
tc, [Type]
_) <- TyCon -> Maybe (TyCon, [Type])
tyConFamInst_maybe (DataCon -> TyCon
dcRepTyCon DataCon
dc) = TyCon
tc
  | Bool
otherwise                                          = DataCon -> TyCon
dcRepTyCon DataCon
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 :: DataCon -> Type
dataConRepType = DataCon -> Type
dcRepType

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

-- | The universally-quantified type variables of the constructor
dataConUnivTyVars :: DataCon -> [TyVar]
dataConUnivTyVars :: DataCon -> [TyVar]
dataConUnivTyVars (MkData { dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars = [TyVar]
tvbs }) = [TyVar]
tvbs

-- | The existentially-quantified type/coercion variables of the constructor
-- including dependent (kind-) GADT equalities
dataConExTyCoVars :: DataCon -> [TyCoVar]
dataConExTyCoVars :: DataCon -> [TyVar]
dataConExTyCoVars (MkData { dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
tvbs }) = [TyVar]
tvbs

-- | Both the universal and existential type/coercion variables of the constructor
dataConUnivAndExTyCoVars :: DataCon -> [TyCoVar]
dataConUnivAndExTyCoVars :: DataCon -> [TyVar]
dataConUnivAndExTyCoVars (MkData { dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars = [TyVar]
univ_tvs, dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
ex_tvs })
  = [TyVar]
univ_tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
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 :: DataCon -> [TyVar]
dataConUserTyVars (MkData { dcUserTyVarBinders :: DataCon -> [InvisTVBinder]
dcUserTyVarBinders = [InvisTVBinder]
tvbs }) = [InvisTVBinder] -> [TyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [InvisTVBinder]
tvbs

-- See Note [DataCon user type variable binders]
-- | 'InvisTVBinder's for the type variables of the constructor, in the order the
-- user wrote them
dataConUserTyVarBinders :: DataCon -> [InvisTVBinder]
dataConUserTyVarBinders :: DataCon -> [InvisTVBinder]
dataConUserTyVarBinders = DataCon -> [InvisTVBinder]
dcUserTyVarBinders

-- | Dependent (kind-level) equalities in a constructor.
-- There are extracted from the existential variables.
-- See Note [Existential coercion variables]
dataConKindEqSpec :: DataCon -> [EqSpec]
dataConKindEqSpec :: DataCon -> [EqSpec]
dataConKindEqSpec (MkData {dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
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.
  = [ TyVar -> Type -> EqSpec
EqSpec TyVar
tv Type
ty
    | TyVar
cv <- [TyVar]
ex_tcvs
    , TyVar -> Bool
isCoVar TyVar
cv
    , let (Type
_, Type
_, Type
ty1, Type
ty, Role
_) = (() :: Constraint) => TyVar -> (Type, Type, Type, Type, Role)
TyVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole TyVar
cv
          tv :: TyVar
tv = (() :: Constraint) => Type -> TyVar
Type -> TyVar
getTyVar Type
ty1
    ]

-- | The *full* constraints on the constructor type, including dependent GADT
-- equalities.
dataConTheta :: DataCon -> ThetaType
dataConTheta :: DataCon -> [Type]
dataConTheta con :: DataCon
con@(MkData { dcEqSpec :: DataCon -> [EqSpec]
dcEqSpec = [EqSpec]
eq_spec, dcOtherTheta :: DataCon -> [Type]
dcOtherTheta = [Type]
theta })
  = [EqSpec] -> [Type]
eqSpecPreds (DataCon -> [EqSpec]
dataConKindEqSpec DataCon
con [EqSpec] -> [EqSpec] -> [EqSpec]
forall a. [a] -> [a] -> [a]
++ [EqSpec]
eq_spec) [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
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 :: DataCon -> TyVar
dataConWorkId DataCon
dc = DataCon -> TyVar
dcWorkId DataCon
dc

-- | 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 :: DataCon -> Maybe TyVar
dataConWrapId_maybe DataCon
dc = case DataCon -> DataConRep
dcRep DataCon
dc of
                           DataConRep
NoDataConRep -> Maybe TyVar
forall a. Maybe a
Nothing
                           DCR { dcr_wrap_id :: DataConRep -> TyVar
dcr_wrap_id = TyVar
wrap_id } -> TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just TyVar
wrap_id

-- | 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 :: DataCon -> TyVar
dataConWrapId DataCon
dc = case DataCon -> DataConRep
dcRep DataCon
dc of
                     DataConRep
NoDataConRep-> DataCon -> TyVar
dcWorkId DataCon
dc    -- worker=wrapper
                     DCR { dcr_wrap_id :: DataConRep -> TyVar
dcr_wrap_id = TyVar
wrap_id } -> TyVar
wrap_id

-- | Find all the 'Id's implicitly brought into scope by the data constructor. Currently,
-- the union of the 'dataConWorkId' and the 'dataConWrapId'
dataConImplicitTyThings :: DataCon -> [TyThing]
dataConImplicitTyThings :: DataCon -> [TyThing]
dataConImplicitTyThings (MkData { dcWorkId :: DataCon -> TyVar
dcWorkId = TyVar
work, dcRep :: DataCon -> DataConRep
dcRep = DataConRep
rep })
  = [TyVar -> TyThing
mkAnId TyVar
work] [TyThing] -> [TyThing] -> [TyThing]
forall a. [a] -> [a] -> [a]
++ [TyThing]
wrap_ids
  where
    wrap_ids :: [TyThing]
wrap_ids = case DataConRep
rep of
                 DataConRep
NoDataConRep               -> []
                 DCR { dcr_wrap_id :: DataConRep -> TyVar
dcr_wrap_id = TyVar
wrap } -> [TyVar -> TyThing
mkAnId TyVar
wrap]

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

-- | Extract the type for any given labelled field of the 'DataCon'
dataConFieldType :: DataCon -> FieldLabelString -> Type
dataConFieldType :: DataCon -> FieldLabelString -> Type
dataConFieldType DataCon
con FieldLabelString
label = case DataCon -> FieldLabelString -> Maybe (FieldLabel, Type)
dataConFieldType_maybe DataCon
con FieldLabelString
label of
      Just (FieldLabel
_, Type
ty) -> Type
ty
      Maybe (FieldLabel, Type)
Nothing      -> String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"dataConFieldType" (DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
con SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> FieldLabelString -> SDoc
forall a. Outputable a => a -> SDoc
ppr FieldLabelString
label)

-- | Extract the label and type for any given labelled field of the
-- 'DataCon', or return 'Nothing' if the field does not belong to it
dataConFieldType_maybe :: DataCon -> FieldLabelString
                       -> Maybe (FieldLabel, Type)
dataConFieldType_maybe :: DataCon -> FieldLabelString -> Maybe (FieldLabel, Type)
dataConFieldType_maybe DataCon
con FieldLabelString
label
  = ((FieldLabel, Type) -> Bool)
-> [(FieldLabel, Type)] -> Maybe (FieldLabel, Type)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((FieldLabelString -> FieldLabelString -> Bool
forall a. Eq a => a -> a -> Bool
== FieldLabelString
label) (FieldLabelString -> Bool)
-> ((FieldLabel, Type) -> FieldLabelString)
-> (FieldLabel, Type)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldLabel -> FieldLabelString
flLabel (FieldLabel -> FieldLabelString)
-> ((FieldLabel, Type) -> FieldLabel)
-> (FieldLabel, Type)
-> FieldLabelString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FieldLabel, Type) -> FieldLabel
forall a b. (a, b) -> a
fst) (DataCon -> [FieldLabel]
dcFields DataCon
con [FieldLabel] -> [Type] -> [(FieldLabel, Type)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCon -> [Scaled Type]
dcOrigArgTys DataCon
con))

-- | Strictness/unpack annotations, from user; or, for imported
-- DataCons, from the interface file
-- The list is in one-to-one correspondence with the arity of the 'DataCon'

dataConSrcBangs :: DataCon -> [HsSrcBang]
dataConSrcBangs :: DataCon -> [HsSrcBang]
dataConSrcBangs = DataCon -> [HsSrcBang]
dcSrcBangs

-- | Source-level arity of the data constructor
dataConSourceArity :: DataCon -> Arity
dataConSourceArity :: DataCon -> Arity
dataConSourceArity (MkData { dcSourceArity :: DataCon -> Arity
dcSourceArity = Arity
arity }) = Arity
arity

-- | Gives the number of value arguments (including zero-width coercions)
-- stored by the given `DataCon`'s worker in its Core representation. This may
-- differ from the number of arguments that appear in the source code; see also
-- Note [DataCon arities]
dataConRepArity :: DataCon -> Arity
dataConRepArity :: DataCon -> Arity
dataConRepArity (MkData { dcRepArity :: DataCon -> Arity
dcRepArity = Arity
arity }) = Arity
arity

-- | Return whether there are any argument types for this 'DataCon's original source type
-- See Note [DataCon arities]
isNullarySrcDataCon :: DataCon -> Bool
isNullarySrcDataCon :: DataCon -> Bool
isNullarySrcDataCon DataCon
dc = DataCon -> Arity
dataConSourceArity DataCon
dc Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
0

-- | Return whether this `DataCon`'s worker, in its Core representation, takes
-- any value arguments.
--
-- In particular, remember that we include coercion arguments in the arity of
-- the Core representation of the `DataCon` -- both lifted and unlifted
-- coercions, despite the latter having zero-width runtime representation.
--
-- See also Note [DataCon arities].
isNullaryRepDataCon :: DataCon -> Bool
isNullaryRepDataCon :: DataCon -> Bool
isNullaryRepDataCon DataCon
dc = DataCon -> Arity
dataConRepArity DataCon
dc Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
0

dataConRepStrictness :: DataCon -> [StrictnessMark]
-- ^ Give the demands on the arguments of a
-- Core constructor application (Con dc args)
dataConRepStrictness :: DataCon -> [StrictnessMark]
dataConRepStrictness DataCon
dc = case DataCon -> DataConRep
dcRep DataCon
dc of
                            DataConRep
NoDataConRep -> [StrictnessMark
NotMarkedStrict | Scaled Type
_ <- DataCon -> [Scaled Type]
dataConRepArgTys DataCon
dc]
                            DCR { dcr_stricts :: DataConRep -> [StrictnessMark]
dcr_stricts = [StrictnessMark]
strs } -> [StrictnessMark]
strs

dataConImplBangs :: DataCon -> [HsImplBang]
-- The implementation decisions about the strictness/unpack of each
-- source program argument to the data constructor
dataConImplBangs :: DataCon -> [HsImplBang]
dataConImplBangs DataCon
dc
  = case DataCon -> DataConRep
dcRep DataCon
dc of
      DataConRep
NoDataConRep              -> Arity -> HsImplBang -> [HsImplBang]
forall a. Arity -> a -> [a]
replicate (DataCon -> Arity
dcSourceArity DataCon
dc) HsImplBang
HsLazy
      DCR { dcr_bangs :: DataConRep -> [HsImplBang]
dcr_bangs = [HsImplBang]
bangs } -> [HsImplBang]
bangs

dataConBoxer :: DataCon -> Maybe DataConBoxer
dataConBoxer :: DataCon -> Maybe DataConBoxer
dataConBoxer (MkData { dcRep :: DataCon -> DataConRep
dcRep = DCR { dcr_boxer :: DataConRep -> DataConBoxer
dcr_boxer = DataConBoxer
boxer } }) = DataConBoxer -> Maybe DataConBoxer
forall a. a -> Maybe a
Just DataConBoxer
boxer
dataConBoxer DataCon
_ = Maybe DataConBoxer
forall a. Maybe a
Nothing

dataConInstSig
  :: DataCon
  -> [Type]    -- Instantiate the *universal* tyvars with these types
  -> ([TyCoVar], ThetaType, [Type])  -- Return instantiated existentials
                                     -- theta and arg tys
-- ^ Instantiate the universal tyvars of a data con,
--   returning
--     ( instantiated existentials
--     , instantiated constraints including dependent GADT equalities
--         which are *also* listed in the instantiated existentials
--     , instantiated args)
dataConInstSig :: DataCon -> [Type] -> ([TyVar], [Type], [Type])
dataConInstSig con :: DataCon
con@(MkData { dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars = [TyVar]
univ_tvs, dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
ex_tvs
                           , dcOrigArgTys :: DataCon -> [Scaled Type]
dcOrigArgTys = [Scaled Type]
arg_tys })
               [Type]
univ_tys
  = ( [TyVar]
ex_tvs'
    , (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTheta Subst
subst (DataCon -> [Type]
dataConTheta DataCon
con)
    , (() :: Constraint) => Subst -> [Type] -> [Type]
Subst -> [Type] -> [Type]
substTys Subst
subst ((Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
arg_tys))
  where
    univ_subst :: Subst
univ_subst = [TyVar] -> [Type] -> Subst
(() :: Constraint) => [TyVar] -> [Type] -> Subst
zipTvSubst [TyVar]
univ_tvs [Type]
univ_tys
    (Subst
subst, [TyVar]
ex_tvs') = (() :: Constraint) => Subst -> [TyVar] -> (Subst, [TyVar])
Subst -> [TyVar] -> (Subst, [TyVar])
Type.substVarBndrs Subst
univ_subst [TyVar]
ex_tvs


-- | The \"full signature\" of the 'DataCon' returns, in order:
--
-- 1) The result of 'dataConUnivTyVars'
--
-- 2) The result of 'dataConExTyCoVars'
--
-- 3) The non-dependent GADT equalities.
--    Dependent GADT equalities are implied by coercion variables in
--    return value (2).
--
-- 4) The other constraints of the data constructor type, excluding GADT
-- equalities
--
-- 5) The original argument types to the 'DataCon' (i.e. before
--    any change of the representation of the type) with linearity
--    annotations
--
-- 6) The original result type of the 'DataCon'
dataConFullSig :: DataCon
               -> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Scaled Type], Type)
dataConFullSig :: DataCon
-> ([TyVar], [TyVar], [EqSpec], [Type], [Scaled Type], Type)
dataConFullSig (MkData {dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars = [TyVar]
univ_tvs, dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
ex_tvs,
                        dcEqSpec :: DataCon -> [EqSpec]
dcEqSpec = [EqSpec]
eq_spec, dcOtherTheta :: DataCon -> [Type]
dcOtherTheta = [Type]
theta,
                        dcOrigArgTys :: DataCon -> [Scaled Type]
dcOrigArgTys = [Scaled Type]
arg_tys, dcOrigResTy :: DataCon -> Type
dcOrigResTy = Type
res_ty})
  = ([TyVar]
univ_tvs, [TyVar]
ex_tvs, [EqSpec]
eq_spec, [Type]
theta, [Scaled Type]
arg_tys, Type
res_ty)

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

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

{-
Note [Displaying linear fields]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A constructor with a linear field can be written either as
MkT :: a %1 -> T a (with -XLinearTypes)
or
MkT :: a  -> T a (with -XNoLinearTypes)

There are three different methods to retrieve a type of a datacon.
They differ in how linear fields are handled.

1. dataConWrapperType:
The type of the wrapper in Core.
For example, dataConWrapperType for Maybe is a %1 -> Just a.

2. dataConNonlinearType:
The type of the constructor, with linear arrows replaced by unrestricted ones.
Used when we don't want to introduce linear types to user (in holes
and in types in hie used by haddock).

3. dataConDisplayType (takes a boolean indicating if -XLinearTypes is enabled):
The type we'd like to show in error messages, :info and -ddump-types.
Ideally, it should reflect the type written by the user;
the function returns a type with arrows that would be required
to write this constructor under the current setting of -XLinearTypes.
In principle, this type can be different from the user's source code
when the value of -XLinearTypes has changed, but we don't
expect this to cause much trouble.

Due to internal plumbing in checkValidDataCon, we can't just return a Doc.
The multiplicity of arrows returned by dataConDisplayType and
dataConDisplayType is used only for pretty-printing.
-}

dataConWrapperType :: 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
--
-- The type variables are quantified in the order that the user wrote them.
-- See @Note [DataCon user type variable binders]@.
--
-- NB: If the constructor is part of a data instance, the result type
-- mentions the family tycon, not the internal one.
dataConWrapperType :: DataCon -> Type
dataConWrapperType (MkData { dcUserTyVarBinders :: DataCon -> [InvisTVBinder]
dcUserTyVarBinders = [InvisTVBinder]
user_tvbs,
                             dcOtherTheta :: DataCon -> [Type]
dcOtherTheta = [Type]
theta, dcOrigArgTys :: DataCon -> [Scaled Type]
dcOrigArgTys = [Scaled Type]
arg_tys,
                             dcOrigResTy :: DataCon -> Type
dcOrigResTy = Type
res_ty,
                             dcStupidTheta :: DataCon -> [Type]
dcStupidTheta = [Type]
stupid_theta })
  = [InvisTVBinder] -> Type -> Type
mkInvisForAllTys [InvisTVBinder]
user_tvbs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Type] -> Type -> Type
(() :: Constraint) => [Type] -> Type -> Type
mkInvisFunTys ([Type]
stupid_theta [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
theta) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Scaled Type] -> Type -> Type
(() :: Constraint) => [Scaled Type] -> Type -> Type
mkScaledFunTys [Scaled Type]
arg_tys (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    Type
res_ty

dataConNonlinearType :: DataCon -> Type
-- Just like dataConWrapperType, but with the
-- linearity on the arguments all zapped to Many
dataConNonlinearType :: DataCon -> Type
dataConNonlinearType (MkData { dcUserTyVarBinders :: DataCon -> [InvisTVBinder]
dcUserTyVarBinders = [InvisTVBinder]
user_tvbs,
                               dcOtherTheta :: DataCon -> [Type]
dcOtherTheta = [Type]
theta, dcOrigArgTys :: DataCon -> [Scaled Type]
dcOrigArgTys = [Scaled Type]
arg_tys,
                               dcOrigResTy :: DataCon -> Type
dcOrigResTy = Type
res_ty,
                               dcStupidTheta :: DataCon -> [Type]
dcStupidTheta = [Type]
stupid_theta })
  = [InvisTVBinder] -> Type -> Type
mkInvisForAllTys [InvisTVBinder]
user_tvbs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Type] -> Type -> Type
(() :: Constraint) => [Type] -> Type -> Type
mkInvisFunTys ([Type]
stupid_theta [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
theta) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Scaled Type] -> Type -> Type
(() :: Constraint) => [Scaled Type] -> Type -> Type
mkScaledFunTys [Scaled Type]
arg_tys' (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    Type
res_ty
  where
    arg_tys' :: [Scaled Type]
arg_tys' = (Scaled Type -> Scaled Type) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(Scaled Type
w Type
t) -> Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled (case Type
w of Type
OneTy -> Type
ManyTy; Type
_ -> Type
w) Type
t) [Scaled Type]
arg_tys

dataConDisplayType :: Bool -> DataCon -> Type
dataConDisplayType :: Bool -> DataCon -> Type
dataConDisplayType Bool
show_linear_types DataCon
dc
  = if Bool
show_linear_types
    then DataCon -> Type
dataConWrapperType DataCon
dc
    else DataCon -> Type
dataConNonlinearType DataCon
dc

-- | 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
                  -> [Scaled Type]
dataConInstArgTys :: DataCon -> [Type] -> [Scaled Type]
dataConInstArgTys dc :: DataCon
dc@(MkData {dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars = [TyVar]
univ_tvs,
                              dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
ex_tvs}) [Type]
inst_tys
 = Bool -> SDoc -> [Scaled Type] -> [Scaled Type]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TyVar]
univ_tvs [TyVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
inst_tys)
             (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"dataConInstArgTys" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
dc SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
univ_tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
inst_tys) ([Scaled Type] -> [Scaled Type]) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> a -> b
$
   Bool -> SDoc -> [Scaled Type] -> [Scaled Type]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
ex_tvs) (DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
dc) ([Scaled Type] -> [Scaled Type]) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> a -> b
$
   (Scaled Type -> Scaled Type) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> Scaled Type -> Scaled Type
mapScaledType ([TyVar] -> [Type] -> Type -> Type
(() :: Constraint) => [TyVar] -> [Type] -> Type -> Type
substTyWith [TyVar]
univ_tvs [Type]
inst_tys)) (DataCon -> [Scaled Type]
dataConRepArgTys DataCon
dc)

-- | 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
        -> [Scaled Type]
-- For vanilla datacons, it's all quite straightforward
-- But for the call in GHC.HsToCore.Match.Constructor, we really do want just
-- the value args
dataConInstOrigArgTys :: DataCon -> [Type] -> [Scaled Type]
dataConInstOrigArgTys dc :: DataCon
dc@(MkData {dcOrigArgTys :: DataCon -> [Scaled Type]
dcOrigArgTys = [Scaled Type]
arg_tys,
                                  dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars = [TyVar]
univ_tvs,
                                  dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
ex_tvs}) [Type]
inst_tys
  = Bool -> SDoc -> [Scaled Type] -> [Scaled Type]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([TyVar]
tyvars [TyVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
inst_tys)
              (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"dataConInstOrigArgTys" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
dc SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tyvars SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
inst_tys) ([Scaled Type] -> [Scaled Type]) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> a -> b
$
    (() :: Constraint) => Subst -> [Scaled Type] -> [Scaled Type]
Subst -> [Scaled Type] -> [Scaled Type]
substScaledTys Subst
subst [Scaled Type]
arg_tys
  where
    tyvars :: [TyVar]
tyvars = [TyVar]
univ_tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
ex_tvs
    subst :: Subst
subst  = [TyVar] -> [Type] -> Subst
(() :: Constraint) => [TyVar] -> [Type] -> Subst
zipTCvSubst [TyVar]
tyvars [Type]
inst_tys

-- | Given a data constructor @dc@ with /n/ universally quantified type
-- variables @a_{1}@, @a_{2}@, ..., @a_{n}@, and given a list of argument
-- types @dc_args@ of length /m/ where /m/ <= /n/, then:
--
-- @
-- dataConInstUnivs dc dc_args
-- @
--
-- Will return:
--
-- @
-- [dc_arg_{1}, dc_arg_{2}, ..., dc_arg_{m}, a_{m+1}, ..., a_{n}]
-- @
--
-- That is, return the list of universal type variables with
-- @a_{1}@, @a_{2}@, ..., @a_{m}@ instantiated with
-- @dc_arg_{1}@, @dc_arg_{2}@, ..., @dc_arg_{m}@. It is possible for @m@ to
-- be less than @n@, in which case the remaining @n - m@ elements will simply
-- be universal type variables (with their kinds possibly instantiated).
--
-- Examples:
--
-- * Given the data constructor @D :: forall a b. Foo a b@ and
--   @dc_args@ @[Int, Bool]@, then @dataConInstUnivs D dc_args@ will return
--   @[Int, Bool]@.
--
-- * Given the data constructor @D :: forall a b. Foo a b@ and
--   @dc_args@ @[Int]@, then @@dataConInstUnivs D dc_args@ will return
--   @[Int, b]@.
--
-- * Given the data constructor @E :: forall k (a :: k). Bar k a@ and
--   @dc_args@ @[Type]@, then @@dataConInstUnivs D dc_args@ will return
--   @[Type, (a :: Type)]@.
--
-- This is primarily used in @GHC.Tc.Deriv.*@ in service of instantiating data
-- constructors' field types.
-- See @Note [Instantiating field types in stock deriving]@ for a notable
-- example of this.
dataConInstUnivs :: DataCon -> [Type] -> [Type]
dataConInstUnivs :: DataCon -> [Type] -> [Type]
dataConInstUnivs DataCon
dc [Type]
dc_args = [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
chkAppend [Type]
dc_args ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (TyVar -> Type) -> [TyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Type
mkTyVarTy [TyVar]
dc_args_suffix
  where
    ([TyVar]
dc_univs_prefix, [TyVar]
dc_univs_suffix)
                        = -- Assert that m <= n
                          Bool -> SDoc -> ([TyVar], [TyVar]) -> ([TyVar], [TyVar])
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type]
dc_args [Type] -> [TyVar] -> Bool
forall a b. [a] -> [b] -> Bool
`leLength` DataCon -> [TyVar]
dataConUnivTyVars DataCon
dc)
                                    (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"dataConInstUnivs"
                                      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
dc_args
                                      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (DataCon -> [TyVar]
dataConUnivTyVars DataCon
dc)) (([TyVar], [TyVar]) -> ([TyVar], [TyVar]))
-> ([TyVar], [TyVar]) -> ([TyVar], [TyVar])
forall a b. (a -> b) -> a -> b
$
                          [Type] -> [TyVar] -> ([TyVar], [TyVar])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [Type]
dc_args ([TyVar] -> ([TyVar], [TyVar])) -> [TyVar] -> ([TyVar], [TyVar])
forall a b. (a -> b) -> a -> b
$ DataCon -> [TyVar]
dataConUnivTyVars DataCon
dc
    (Subst
_, [TyVar]
dc_args_suffix) = (() :: Constraint) => Subst -> [TyVar] -> (Subst, [TyVar])
Subst -> [TyVar] -> (Subst, [TyVar])
substTyVarBndrs Subst
prefix_subst [TyVar]
dc_univs_suffix
    prefix_subst :: Subst
prefix_subst        = InScopeSet -> TvSubstEnv -> Subst
mkTvSubst InScopeSet
prefix_in_scope TvSubstEnv
prefix_env
    prefix_in_scope :: InScopeSet
prefix_in_scope     = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
tyCoVarsOfTypes [Type]
dc_args
    prefix_env :: TvSubstEnv
prefix_env          = [TyVar] -> [Type] -> TvSubstEnv
(() :: Constraint) => [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv [TyVar]
dc_univs_prefix [Type]
dc_args

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

-- | Returns constraints in the wrapper type, other than those in the dataConEqSpec
dataConOtherTheta :: DataCon -> ThetaType
dataConOtherTheta :: DataCon -> [Type]
dataConOtherTheta DataCon
dc = DataCon -> [Type]
dcOtherTheta DataCon
dc

-- | Returns the arg types of the worker, including *all* non-dependent
-- evidence, after any flattening has been done and without substituting for
-- any type variables
dataConRepArgTys :: DataCon -> [Scaled Type]
dataConRepArgTys :: DataCon -> [Scaled Type]
dataConRepArgTys (MkData { dcRep :: DataCon -> DataConRep
dcRep = DataConRep
rep
                         , dcEqSpec :: DataCon -> [EqSpec]
dcEqSpec = [EqSpec]
eq_spec
                         , dcOtherTheta :: DataCon -> [Type]
dcOtherTheta = [Type]
theta
                         , dcOrigArgTys :: DataCon -> [Scaled Type]
dcOrigArgTys = [Scaled Type]
orig_arg_tys })
  = case DataConRep
rep of
      DataConRep
NoDataConRep -> Bool -> [Scaled Type] -> [Scaled Type]
forall a. HasCallStack => Bool -> a -> a
assert ([EqSpec] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EqSpec]
eq_spec) ([Scaled Type] -> [Scaled Type]) -> [Scaled Type] -> [Scaled Type]
forall a b. (a -> b) -> a -> b
$ (Type -> Scaled Type) -> [Type] -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Scaled Type
forall a. a -> Scaled a
unrestricted [Type]
theta [Scaled Type] -> [Scaled Type] -> [Scaled Type]
forall a. [a] -> [a] -> [a]
++ [Scaled Type]
orig_arg_tys
      DCR { dcr_arg_tys :: DataConRep -> [Scaled Type]
dcr_arg_tys = [Scaled Type]
arg_tys } -> [Scaled Type]
arg_tys

-- | 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 -> ByteString
-- We want this string to be UTF-8, so we get the bytes directly from the FastStrings.
dataConIdentity :: DataCon -> ByteString
dataConIdentity DataCon
dc = ByteString -> ByteString
LBS.toStrict (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
BSB.toLazyByteString (Builder -> ByteString) -> Builder -> ByteString
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
   [ ShortByteString -> Builder
BSB.shortByteString (ShortByteString -> Builder) -> ShortByteString -> Builder
forall a b. (a -> b) -> a -> b
$ FastString -> ShortByteString
fastStringToShortByteString (FastString -> ShortByteString) -> FastString -> ShortByteString
forall a b. (a -> b) -> a -> b
$
       Unit -> FastString
forall u. IsUnitId u => u -> FastString
unitFS (Unit -> FastString) -> Unit -> FastString
forall a b. (a -> b) -> a -> b
$ GenModule Unit -> Unit
forall unit. GenModule unit -> unit
moduleUnit GenModule Unit
mod
   , Int8 -> Builder
BSB.int8 (Int8 -> Builder) -> Int8 -> Builder
forall a b. (a -> b) -> a -> b
$ Arity -> Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Arity
ord Char
':')
   , ShortByteString -> Builder
BSB.shortByteString (ShortByteString -> Builder) -> ShortByteString -> Builder
forall a b. (a -> b) -> a -> b
$ FastString -> ShortByteString
fastStringToShortByteString (FastString -> ShortByteString) -> FastString -> ShortByteString
forall a b. (a -> b) -> a -> b
$
       ModuleName -> FastString
moduleNameFS (ModuleName -> FastString) -> ModuleName -> FastString
forall a b. (a -> b) -> a -> b
$ GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
moduleName GenModule Unit
mod
   , Int8 -> Builder
BSB.int8 (Int8 -> Builder) -> Int8 -> Builder
forall a b. (a -> b) -> a -> b
$ Arity -> Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Arity
ord Char
'.')
   , ShortByteString -> Builder
BSB.shortByteString (ShortByteString -> Builder) -> ShortByteString -> Builder
forall a b. (a -> b) -> a -> b
$ FastString -> ShortByteString
fastStringToShortByteString (FastString -> ShortByteString) -> FastString -> ShortByteString
forall a b. (a -> b) -> a -> b
$
       OccName -> FastString
occNameFS (OccName -> FastString) -> OccName -> FastString
forall a b. (a -> b) -> a -> b
$ Name -> OccName
nameOccName Name
name
   ]
  where name :: Name
name = DataCon -> Name
dataConName DataCon
dc
        mod :: GenModule Unit
mod  = Bool -> GenModule Unit -> GenModule Unit
forall a. HasCallStack => Bool -> a -> a
assert (Name -> Bool
isExternalName Name
name) (GenModule Unit -> GenModule Unit)
-> GenModule Unit -> GenModule Unit
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Name -> GenModule Unit
Name -> GenModule Unit
nameModule Name
name

isTupleDataCon :: DataCon -> Bool
isTupleDataCon :: DataCon -> Bool
isTupleDataCon (MkData {dcRepTyCon :: DataCon -> TyCon
dcRepTyCon = TyCon
tc}) = TyCon -> Bool
isTupleTyCon TyCon
tc

isBoxedTupleDataCon :: DataCon -> Bool
isBoxedTupleDataCon :: DataCon -> Bool
isBoxedTupleDataCon (MkData {dcRepTyCon :: DataCon -> TyCon
dcRepTyCon = TyCon
tc}) = TyCon -> Bool
isBoxedTupleTyCon TyCon
tc

isUnboxedTupleDataCon :: DataCon -> Bool
isUnboxedTupleDataCon :: DataCon -> Bool
isUnboxedTupleDataCon (MkData {dcRepTyCon :: DataCon -> TyCon
dcRepTyCon = TyCon
tc}) = TyCon -> Bool
isUnboxedTupleTyCon TyCon
tc

isUnboxedSumDataCon :: DataCon -> Bool
isUnboxedSumDataCon :: DataCon -> Bool
isUnboxedSumDataCon (MkData {dcRepTyCon :: DataCon -> TyCon
dcRepTyCon = TyCon
tc}) = TyCon -> Bool
isUnboxedSumTyCon TyCon
tc

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

-- | Is this the 'DataCon' of a newtype?
isNewDataCon :: DataCon -> Bool
isNewDataCon :: DataCon -> Bool
isNewDataCon DataCon
dc = TyCon -> Bool
isNewTyCon (DataCon -> TyCon
dataConTyCon DataCon
dc)

-- | Is this data constructor in a "type data" declaration?
-- See Note [Type data declarations] in GHC.Rename.Module.
isTypeDataCon :: DataCon -> Bool
isTypeDataCon :: DataCon -> Bool
isTypeDataCon DataCon
dc = TyCon -> Bool
isTypeDataTyCon (DataCon -> TyCon
dataConTyCon DataCon
dc)

isCovertGadtDataCon :: DataCon -> Bool
-- See Note [isCovertGadtDataCon]
isCovertGadtDataCon :: DataCon -> Bool
isCovertGadtDataCon (MkData { dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars  = [TyVar]
univ_tvs
                            , dcEqSpec :: DataCon -> [EqSpec]
dcEqSpec     = [EqSpec]
eq_spec
                            , dcRepTyCon :: DataCon -> TyCon
dcRepTyCon   = TyCon
rep_tc })
  =  Bool -> Bool
not ([EqSpec] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EqSpec]
eq_spec)                -- There are some constraints
  Bool -> Bool -> Bool
&& Bool -> Bool
not ((EqSpec -> Bool) -> [EqSpec] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any EqSpec -> Bool
is_visible_spec [EqSpec]
eq_spec) -- But none of them are visible
  where
    visible_univ_tvs :: [TyVar]  -- Visible arguments in result type
    visible_univ_tvs :: [TyVar]
visible_univ_tvs
      = [ TyVar
univ_tv | (TyVar
univ_tv, TyConBinder
tcb) <- [TyVar]
univ_tvs [TyVar] -> [TyConBinder] -> [(TyVar, TyConBinder)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` TyCon -> [TyConBinder]
tyConBinders TyCon
rep_tc
                  , TyConBinder -> Bool
forall tv. VarBndr tv TyConBndrVis -> Bool
isVisibleTyConBinder TyConBinder
tcb ]

    is_visible_spec :: EqSpec -> Bool
    is_visible_spec :: EqSpec -> Bool
is_visible_spec (EqSpec TyVar
univ_tv Type
ty)
       = TyVar
univ_tv TyVar -> [TyVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyVar]
visible_univ_tvs
         Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isTyVarTy Type
ty)  -- See Note [isCovertGadtDataCon] for
                                -- an example where 'ty' is a tyvar

{- Note [isCovertGadtDataCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(isCovertGadtDataCon K) returns True if K is a GADT data constructor, but
does not /look/ like it. Consider (#21447)
    type T :: TYPE r -> Type
    data T a where { MkT :: b -> T b }
Here MkT doesn't look GADT-like, but it is. If we make the kind applications
explicit we'd see:
    data T a where { MkT :: b -> T @LiftedRep b }

The test for covert-ness is bit tricky, because we want to see if
  - dcEqSpec is non-empty
  - dcEqSpec does not constrain any of the /required/ (i.e. visible)
    arguments of the TyCon to a non-tyvar

In the example above, the DataCon for MkT will have
    dcUnivTyVars: [(r::RuntimeRep), (a :: TYPE r)]
    dcExTyVars:   [(b :: Type)]
    dcEqSpec:     [(r, LiftedRep), (a, b)]
Here
  * `r :: RuntimeRep` is constrained by dcEqSpec to LiftedRep
  * `a :: TYPE r` is constrained by dcEqSpec to `b :: Type`
But the constraint on `a` is not visible to the user, so this counts
as a covert GADT data con.  The declaration
     MkT :: forall (b :: Type). b -> T b
looks entirely non-GADT-ish.

Wrinkles:
* The visibility or otherwise is a property of the /TyCon/ binders
* The dcUnivTyVars may or may not be the same as the TyCon binders
* So we have to zip them together.
* For a data family the TyCon in question is the /representation/ TyCon
  hence dcRepTyCon
-}


-- | Should this DataCon be allowed in a type even without -XDataKinds?
-- Currently, only Lifted & Unlifted
specialPromotedDc :: DataCon -> Bool
specialPromotedDc :: DataCon -> Bool
specialPromotedDc = TyCon -> Bool
isKindTyCon (TyCon -> Bool) -> (DataCon -> TyCon) -> DataCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> TyCon
dataConTyCon

classDataCon :: Class -> DataCon
classDataCon :: Class -> DataCon
classDataCon Class
clas = case TyCon -> [DataCon]
tyConDataCons (Class -> TyCon
classTyCon Class
clas) of
                      (DataCon
dict_constr:[DataCon]
no_more) -> Bool -> DataCon -> DataCon
forall a. HasCallStack => Bool -> a -> a
assert ([DataCon] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DataCon]
no_more) DataCon
dict_constr
                      [] -> String -> DataCon
forall a. HasCallStack => String -> a
panic String
"classDataCon"

dataConCannotMatch :: [Type] -> DataCon -> Bool
-- Returns True iff the data con *definitely cannot* match a
--                  scrutinee of type (T tys)
--                  where T is the dcRepTyCon for the data con
dataConCannotMatch :: [Type] -> DataCon -> Bool
dataConCannotMatch [Type]
tys DataCon
con
  -- See (U6) in Note [Implementing unsafeCoerce]
  -- in base:Unsafe.Coerce
  | DataCon -> Name
dataConName DataCon
con Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
unsafeReflDataConName
                      = Bool
False
  | [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
inst_theta   = Bool
False   -- Common
  | (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isTyVarTy [Type]
tys = Bool
False   -- Also common
  | Bool
otherwise         = [(Type, Type)] -> Bool
typesCantMatch ((Type -> [(Type, Type)]) -> [Type] -> [(Type, Type)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [(Type, Type)]
predEqs [Type]
inst_theta)
  where
    ([TyVar]
_, [Type]
inst_theta, [Type]
_) = DataCon -> [Type] -> ([TyVar], [Type], [Type])
dataConInstSig DataCon
con [Type]
tys

    -- TODO: could gather equalities from superclasses too
    predEqs :: Type -> [(Type, Type)]
predEqs Type
pred = case Type -> Pred
classifyPredType Type
pred of
                     EqPred EqRel
NomEq Type
ty1 Type
ty2         -> [(Type
ty1, Type
ty2)]
                     ClassPred Class
eq [Type]
args
                       | Class
eq Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
                       , [Type
_, Type
ty1, Type
ty2] <- [Type]
args    -> [(Type
ty1, Type
ty2)]
                       | Class
eq Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
                       , [Type
_, Type
_, Type
ty1, Type
ty2] <- [Type]
args -> [(Type
ty1, Type
ty2)]
                     Pred
_                            -> []

-- | Were the type variables of the data con written in a different order
-- than the regular order (universal tyvars followed by existential tyvars)?
--
-- This is not a cheap test, so we minimize its use in GHC as much as possible.
-- Currently, its only call site in the GHC codebase is in 'mkDataConRep' in
-- "MkId", and so 'dataConUserTyVarsNeedWrapper' is only called at most once
-- during a data constructor's lifetime.

dataConResRepTyArgs :: DataCon -> [Type]
-- Returns the arguments of a GADT version of the /representation/ TyCon
-- Thus   data instance T [(x,y)] z where
--           MkT :: forall p q. Int -> T [(Int,p)] (Maybe q)
-- The "GADT version of the representation type" is
--        data R:T x y z where
--           MkT :: forall p q. Int -> R:T Int p (Maybe q)
-- so dataConResRepTyArgs for MkT returns [Int, p, Maybe q]
-- This is almost the same as (subst eq_spec univ_tvs); but not quite,
--   because eq_spec omits constraint-kinded equalities
dataConResRepTyArgs :: DataCon -> [Type]
dataConResRepTyArgs dc :: DataCon
dc@(MkData { dcRepTyCon :: DataCon -> TyCon
dcRepTyCon = TyCon
rep_tc, dcOrigResTy :: DataCon -> Type
dcOrigResTy = Type
orig_res_ty })
  | Just (TyCon
fam_tc, [Type]
fam_args) <- TyCon -> Maybe (TyCon, [Type])
tyConFamInst_maybe TyCon
rep_tc
  = -- fvs(fam_args) = tyConTyVars rep_tc
    -- These tyvars are the domain of subst
    -- Fvs(range(subst)) = tvars of the datacon
    case  Type -> Type -> Maybe Subst
tcMatchTy (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
fam_args) Type
orig_res_ty of
       Just Subst
subst -> (TyVar -> Type) -> [TyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> TyVar -> Type
substTyVar Subst
subst) (TyCon -> [TyVar]
tyConTyVars TyCon
rep_tc)
       Maybe Subst
Nothing    -> String -> SDoc -> [Type]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"datacOnResRepTyArgs" (SDoc -> [Type]) -> SDoc -> [Type]
forall a b. (a -> b) -> a -> b
$
                     [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
dc, TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
fam_args
                          , Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
orig_res_ty ]
  | Bool
otherwise
  = HasCallStack => Type -> [Type]
Type -> [Type]
tyConAppArgs Type
orig_res_ty

checkDataConTyVars :: DataCon -> Bool
-- Check that the worker and wrapper have the same set of type variables
-- See Note [DataCon user type variable binders]
-- Also ensures that no user tyvar is in the eq_spec (the eq_spec should
-- only relate fresh universals from (R2) of the note)
checkDataConTyVars :: DataCon -> Bool
checkDataConTyVars dc :: DataCon
dc@(MkData { dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars = [TyVar]
univ_tvs
                              , dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
ex_tvs
                              , dcEqSpec :: DataCon -> [EqSpec]
dcEqSpec = [EqSpec]
eq_spec })
     -- use of sets here: (R1) from the Note
  = [TyVar] -> UnVarSet
mkUnVarSet [TyVar]
depleted_worker_vars UnVarSet -> UnVarSet -> Bool
forall a. Eq a => a -> a -> Bool
== [TyVar] -> UnVarSet
mkUnVarSet [TyVar]
depleted_wrapper_vars Bool -> Bool -> Bool
&&
    (TyVar -> Bool) -> [TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (TyVar -> Bool) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Bool
is_eq_spec_var) [TyVar]
wrapper_vars
  where
    is_constraint_var :: TyVar -> Bool
is_constraint_var TyVar
v = (() :: Constraint) => Type -> TypeOrConstraint
Type -> TypeOrConstraint
typeTypeOrConstraint (TyVar -> Type
tyVarKind TyVar
v) TypeOrConstraint -> TypeOrConstraint -> Bool
forall a. Eq a => a -> a -> Bool
== TypeOrConstraint
ConstraintLike
      -- implements (R3) from the Note

    worker_vars :: [TyVar]
worker_vars = [TyVar]
univ_tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
ex_tvs
    eq_spec_tvs :: UnVarSet
eq_spec_tvs = [TyVar] -> UnVarSet
mkUnVarSet ((EqSpec -> TyVar) -> [EqSpec] -> [TyVar]
forall a b. (a -> b) -> [a] -> [b]
map EqSpec -> TyVar
eqSpecTyVar [EqSpec]
eq_spec)
    is_eq_spec_var :: TyVar -> Bool
is_eq_spec_var = (TyVar -> UnVarSet -> Bool
`elemUnVarSet` UnVarSet
eq_spec_tvs)  -- (R2) from the Note
    depleted_worker_vars :: [TyVar]
depleted_worker_vars = (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (TyVar -> Bool
is_eq_spec_var (TyVar -> Bool) -> (TyVar -> Bool) -> TyVar -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> TyVar -> Bool
is_constraint_var)
                                     [TyVar]
worker_vars

    wrapper_vars :: [TyVar]
wrapper_vars = DataCon -> [TyVar]
dataConUserTyVars DataCon
dc
    depleted_wrapper_vars :: [TyVar]
depleted_wrapper_vars = (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut TyVar -> Bool
is_constraint_var [TyVar]
wrapper_vars

dataConUserTyVarsNeedWrapper :: DataCon -> Bool
-- Check whether the worker and wapper have the same type variables
-- in the same order. If not, we need a wrapper to swizzle them.
-- See Note [DataCon user type variable binders], as well as
-- Note [Data con wrappers and GADT syntax] for an explanation of what
-- mkDataConRep is doing with this function.
dataConUserTyVarsNeedWrapper :: DataCon -> Bool
dataConUserTyVarsNeedWrapper dc :: DataCon
dc@(MkData { dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars = [TyVar]
univ_tvs
                                        , dcExTyCoVars :: DataCon -> [TyVar]
dcExTyCoVars = [TyVar]
ex_tvs
                                        , dcEqSpec :: DataCon -> [EqSpec]
dcEqSpec = [EqSpec]
eq_spec })
  = Bool -> Bool -> Bool
forall a. HasCallStack => Bool -> a -> a
assert ([EqSpec] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EqSpec]
eq_spec Bool -> Bool -> Bool
|| Bool
answer)  -- all GADTs should say "yes" here
    Bool
answer
  where
    answer :: Bool
answer = ([TyVar]
univ_tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
ex_tvs) [TyVar] -> [TyVar] -> Bool
forall a. Eq a => a -> a -> Bool
/= DataCon -> [TyVar]
dataConUserTyVars DataCon
dc
              -- Worker tyvars         Wrapper tyvars


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

-}

promoteDataCon :: DataCon -> TyCon
promoteDataCon :: DataCon -> TyCon
promoteDataCon (MkData { dcPromoted :: DataCon -> TyCon
dcPromoted = TyCon
tc }) = TyCon
tc

{-
************************************************************************
*                                                                      *
\subsection{Splitting products}
*                                                                      *
************************************************************************
-}

-- | 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 data type that is all of:
--
--  * Concrete (i.e. constructors visible)
--  * Single-constructor
--  * ... which has no existentials
--
-- Whether the type is a @data@ type or a @newtype@.
splitDataProductType_maybe
        :: Type                         -- ^ A product type, perhaps
        -> Maybe (TyCon,                -- The type constructor
                  [Type],               -- Type args of the tycon
                  DataCon,              -- The data constructor
                  [Scaled Type])        -- Its /representation/ arg types

        -- Rejecting existentials means we don't have to worry about
        -- freshening and substituting type variables
        -- (See "GHC.Type.Id.Make.dataConArgUnpack")

splitDataProductType_maybe :: Type -> Maybe (TyCon, [Type], DataCon, [Scaled Type])
splitDataProductType_maybe Type
ty
  | Just (TyCon
tycon, [Type]
ty_args) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
  , Just DataCon
con <- TyCon -> Maybe DataCon
tyConSingleDataCon_maybe TyCon
tycon
  , [TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [TyVar]
dataConExTyCoVars DataCon
con) -- no existentials! See above
  = (TyCon, [Type], DataCon, [Scaled Type])
-> Maybe (TyCon, [Type], DataCon, [Scaled Type])
forall a. a -> Maybe a
Just (TyCon
tycon, [Type]
ty_args, DataCon
con, DataCon -> [Type] -> [Scaled Type]
dataConInstArgTys DataCon
con [Type]
ty_args)
  | Bool
otherwise
  = Maybe (TyCon, [Type], DataCon, [Scaled Type])
forall a. Maybe a
Nothing