#12166 closed bug (invalid)

Pattern synonym existential variable confusion

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown 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.)

Change History (2)

comment:1 Changed 13 months ago 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.

comment:2 Changed 13 months ago by goldfire

Resolution: invalid
Status: newclosed

Perhaps you're right. The big difference between your examples and mine is that yours indeed bring some existential into scope. Your pattern signature restricts the usefulness of these existentials. In my example, though, there is no existential at all brought into scope in the pattern, even though there is in the signature.

That said, my case is contrived (and I think all examples like mine would be) and there's no lint error, so I'll stand down.

Note: See TracTickets for help on using tickets.