GADT-syntax data constructors don't work well with TypeApplications
Consider
data X a where
MkX :: b -> Proxy a -> X a
According to the rules around specified vs. generalized variables around TypeApplications
, the type of MkX
should be
MkX :: forall {k} (b :: *) (a :: k). b -> Proxy a -> X a
A few things to note:
- The
k
isn't available forTypeApplications
(that's why it's in braces), because it is not user-written. - The
b
is quantified before thea
, becauseb
comes beforea
in the user-written type signature forMkX
.
Both of these bullets are currently violated. GHCi reports MkX
's type as
MkX :: forall k (a :: k) b. b -> Proxy a -> X a
It turns out that this is a hard to fix. The problem is that GHC expects data constructors to have their universal variables followed by their existential variables, always. And yet that's violated in the desired type for MkX
. Furthermore, given the way that GHC deals with GADT return types ("rejigging", in technical parlance), it's inconvenient to get the specified/generalized distinction correct.
Given time constraints, I'm afraid fixing this all won't make it for 8.0.
Happily, there is are easy-to-articulate rules governing GHC's current (wrong) behavior. In a GADT-syntax data constructor:
- All kind and type variables are considered specified and available for visible type application.
- Universal variables always come first, in precisely the order they appear in the tycon. Note that universals that are constrained by a GADT return type are missing from the datacon.
- Existential variables come next. Their order is determined by a user-written
forall
; or, if there is none, by taking the left-to-right order in the datacon's type and doing a stable topological sort. (This stable topological sort step is the same as for other user-written type signatures.)
Despite the existence of these rules, it would still be better not to have special rules for GADT-syntax data constructors. This ticket is intended to capture that eventual goal.