Order of constraints forced (in pattern synonyms, type classes in comments)

Ever since TypeApplications the order of quantification matters.

It seems there are some places where the user has no control over the order:

data A a where
  X :: A [xxx]

pattern X' :: forall t. () => forall xxx. t ~ [xxx] => A t
pattern X' = X

This quantifies the universal t and the existential xxx.. but in this case t is constrained to equal [xxx] so when we supply our first type (the universal t) it is forced to be of the form [a]. Then the existential is forced to equal a (there is currently no way to express this without quantification + annotation X' @[t] @t :: forall t. A [t], see ticket #11385 (closed) to allow X' @[_t] @_t, for this ticket the equality is inherent in X so it doesn't matter).

This means that the first argument really doesn't give any further information but it seems impossible to reorder the existential type before the universal. This either forces the user to supply a dummy type:

X' @_ @ActualType

or to write [ActualType] explicitly

X' @[ActualType]

X' @[ActualType] @ActualType

X' @[_] @ActualType

This may be a bigger inconvenience than it may seem: the return type can be more complicated A (B (C a)) and it requires the user to look it up. X' @_ @ActualType feels like bad library design, especially as the number of existential variables grows and the user has to remember how many underscores to provide.

See also ticket:10928#comment:108009

Keep in mind that this usage will be common, since the more obvious (see ticket:10928#comment:108139)

pattern X'' :: forall xxx. A [xxx]
pattern X'' = X

cannot match against a type A a

-- Works
foo :: A a -> ...
foo X' = ...

-- Doesn't
bar :: A a -> ...
bar X'' = ...

Thoughts?