[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 request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |             Keywords:
      Resolution:                    |  TypeApplications PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  11513, 10928      |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

@@ -18,3 +18,3 @@
- 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 without quantification + annotation `X' @[t] @t :: forall t. A [t]`,
+ see ticket #11385 to allow `X' @[_t] @_t`, for this ticket the equality is
+ inherent in `X` so it doesn't matter).

New description:

 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 quantification + annotation `X' @[t] @t :: forall t. A [t]`,
 see ticket #11385 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:

 {{{#!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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler