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