[GHC] #12025: Order of constraints forced (in pattern synonyms, type classes in comments)

[GHC]

#12025: Order of constraints forced (in pattern synonyms, type classes in comments)
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications PatternSynonyms   |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  11513, 10928
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Ever since `TypeApplications` the order of quantification matters.

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

 {{{#!hs
 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 a type annotation `X' @[t] @t :: A [t]`, see ticket #11385 to
 allow `X' @[_t] @_t`, for this ticket the equality is inherent in `X` so
 it's no big deal).

 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:

 {{{#!hs
 X' @_ @ActualType
 }}}

 or to write `[ActualType]` explicitly


 {{{#!hs
 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:5

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

 {{{#!hs
 pattern X'' :: forall xxx. A [xxx]
 pattern X'' = X
 }}}

 cannot match against a type `A a`

 {{{#!hs
 -- Works
 foo :: A a -> ...
 foo X' = ...

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

 Thoughts?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12025>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler