Re: [GHC] #12166: Pattern synonym existential variable confusion

8 Jun 2016

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

Comment (by simonpj):

 I'm not sure I agree.  Over-existentialising is just a way of making the
 pattern more restricted than it could be.  Here's another example:
 {{{
 data T where
   MkT :: [a] -> ([a] -> Int) -> T

 pattern P :: () => forall b. b -> (b->Int) -> T
 pattern P x y <- MkT x y
 }}}
 Now `P` is less useful than `MkT` because a match against `P` binds a
 first argument of type `b` rather than `[a]`.  It's the dual of
 restricting polymorphism in an ordinary type signature.

 I think that what you show is just an extreme version.  Here's another one
 {{{
 data S where
   MkS :: Show a => a -> (a->Int) -> S

 pattern Q :: () => forall a. a -> (a->Int) -> S
 pattern Q x y = MkS x y
 }}}
 So there's a continuum here, isn't there?

 All of these compile -- and should do so, I think.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12166#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler