#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