[GHC] #11224: Program doesn't preserve semantics after pattern synonym inlining.

[GHC]

#11224: Program doesn't preserve semantics after pattern synonym inlining.
-------------------------------------+-------------------------------------
        Reporter:  anton.dubovik     |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Windows           |         Architecture:  x86_64
 Type of failure:  Incorrect result  |  (amd64)
  at runtime                         |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11225            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 OK. So here's my current stream of thought:
 * The universals are those variables that appear in either the result or
 in the required context.

 Except that's not quite right in pathological cases, like this:

 {{{
 data Ex = forall a. Ex a
 magic :: Ex -> a
 magic _ = undefined

 pattern Silly x <- (magic -> x)
 }}}

 As I understand it, the signature for `Silly` should be

 {{{
 pattern type Silly :: a -> Ex
 }}}

 Here, `a` is universal. But `a` is mentioned neither in the result nor in
 the required context. Compare to

 {{{
 pattern type Sensible :: a -> Ex
 pattern Sensible x = Ex x
 }}}

 Here, `a` is existential. But the pattern signature is otherwise
 identical! So we can't infer the universal/existential decision from the
 signature.

 I thus propose the following revision to pattern signatures:
  * Allow explicit quantification in two places, according to this schema:
 {{{
 pattern type Syn :: forall <<univs>>. <<req>> => forall <<exs>>. <<prov>>
 => <<args>> -> <<result>>
 }}}

  * In the absence of explicit quantification, universals are inferred to
 be the variables mentioned in either the result or the required context.
 Existentials are the remaining variables.

  * It is against the rules for existentials to shadow universals.

 According to these rules, the signature given for `Silly` above would be
 rejected, as `a` is inferred to be existential, but in the pattern
 synonym, it really is universal. Instead, the user would have to write

 {{{
 pattern type Silly :: forall a. a -> Ex
 }}}

 What's terribly unfortunate here is that this new, revised signature for
 `Silly` seems to add simply a redundant `forall`... the sort of thing
 Haskell infers all the time. Except here it says "`a` is universal".
 Contrast to the explicit form of `Sensible`'s signature:

 {{{
 pattern type Sensible :: () => forall a. a -> Ex
 }}}

 which is quite ugly.

 This all makes me want the incredibly verbose syntax in
 comment:5:ticket:10928, repeated here for convenience:
 {{{
 pattern type P :: { universals = ...
                   , existentials = ...
                   , provided = ...
                   , required = ...
                   , arguments = ...
                   , result = ... }
 }}}
 A worked out example appears in that comment. We would allow a short-hand
 in common cases (yet to be worked out). This syntax is annoying to write,
 but surely a pleasure to read. And it reminds readers that the thing to
 the right of `pattern type Blah ::` is '''not''' a type.

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