[GHC] #12166: Pattern synonym existential variable confusion

[GHC]

#12166: Pattern synonym existential variable confusion
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Ponder this:

 {{{
 magic :: Int -> a
 magic = undefined

 pattern Silly :: a -> Int
 pattern Silly a <- (magic -> a)
 }}}

 According to the rules for implicit quantification in pattern signatures,
 the `a` in `Silly`'s type is labeled as existential. That's sensible
 enough. But what surprised me is that the code is accepted, even though
 the pattern `(magic -> a)` doesn't bring any existentials into scope.

 Apparently, GHC is clever enough not to produce a core-lint error, and it
 actually treats the variable as existential, as witnessed by
 {{{
 foo (Silly x) = x
 }}}
 which fails to compile because of skolem-escape.

 If you change the pattern signature to
 {{{
 pattern Silly :: forall a. a -> Int
 }}}
 that changes `a` to be universal, and then `foo` is accepted.

 I think the original program, with `a` inferred to be existential, should
 be rejected.

 (The inference around universal/existential is not at issue. With a
 signature `pattern Silly :: () => forall a. a -> Int`, the program is
 still accepted when it shouldn't be.)

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