#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