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, and with user-specified
visibilities.
- They are the forall'd binders of the data con /wrapper/, which the user calls.
- With RequiredTypeArguments, some of the foralls may be visible, e.g.
MkT :: forall a b. forall c -> (a, b, c) -> T a b c
so the binders are full TyVarBinders, complete with visibilities.
- Even if we only consider invisible foralls, the order and specificity of
binders matter for TypeApplications.
* 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/
- They do not come equipped with visibilities:
dcUnivTyVars :: [TyVar] -- not [TyVarBinder]
dcExTyCoVars :: [TyCoVar] -- not [ForAllTyBinder]
Instead, we treat them as having the Specified (coreTyLamForAllTyFlag)
visibility. For example:
wrapper type: forall {a} b. forall c -> ...
worker type: forall a b c. ...
This is a design choice. Reasons:
* Workers are never called by the user. They are part of the Core
language where visibilities don't matter as much.
* Consistency with type lambdas in Core. As Note [Required foralls in Core]
in GHC.Core.TyCo.Rep explains, (/\a. e) :: (forall a. e_ty), and we need
a coercion to cast it to (forall a -> e_ty).
As a consequence, we may need to adjust visibilities with a cast in the
wrapper. See Note [Flag cast in data con wrappers].
Often (dcUnivTyVars ++ dcExTyCoVars) = binderVars dcUserTyVarBinders; but they
may differ for two 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.
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.