## 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 for`TypeApplications`

(that's why it's in braces), because it is not user-written. - The
`b`

is quantified before the`a`

, because`b`

comes before`a`

in the user-written type signature for`MkX`

.

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.