[GHC] #13735: RankNTypes don't work with PatternSynonyms

[GHC]

#13735: RankNTypes don't work with PatternSynonyms
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:  invalid           |             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:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 > But re the original Description, I agree that the bidirectional
 definition should go through

 I was wrong.  Actually what is happening is quite reasonable.

 GHC is rejecting a unidirectional pattern with a signature (bidirectional
 is red herring):
 {{{
 pattern LLam :: (forall a. a -> PLambda a) -> Lam
 pattern LLam x <- L (Lam x)
 }}}
 Why rejected?  Well, if `LLam` had the type claimed by the signature, this
 would be ok
 {{{
 f1 (LLam x) = (x 'c', x True)
 }}}
 since `x :: forall a. a -> PLambda a`.  But if you expand the syononym,
 thus
 {{{
 f2 (L (Lam x)) = (x 'c', x True)
 }}}
 it's clear that `f2` should be rejected.  (And it is; try it.)
 If you doubt that it should be, try to desugar it:
 {{{
 f2 = \(v:Lam). case v of L (w :: forall b. PLambda b) ->
                case (w @ty) of Lam (x :: ty -> PLambda ty) ->
                (x 'c', x True)
 }}}
 We pattern match on `f2`'s argument to extract a polymorphic `w`. Then we
 must apply `w` to some type `ty` before we can do any more; but now the
 `x` we get from pattern matching is not polymorphic.

 Conclusion: it's working fine.

 I'll close, but re-open if you disagree

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