I only followed the discussion relatively loosely, so apologies if the following is not helpful.

The declaration for `Any2 `can be modified slightly to get it accepted wit the explicit forall. Note that a pattern type signature has some quirks w.r.t quantification of existential and universal type variables.

pattern Any2 :: forall . forall a. a -> Some

If I remember correctly, the first forall in a pattern signature quantifies universal type variables and the second quantifies existentials. If only one is given, it is assumed to be for universals.
If none are given, GHC tries to infer any quantification. This should be described in the "Pattern Synonyms" (Pickering et al) paper.

I guess the printed type when asking GHC could be improved. But it might be that GHC is doing the "correct" thing since `:t Any` asks for the type of `Any` in an expression and not as a pattern signature.

For constraints, there is a similar story w.r.t provided and required constraints.

Cheers,
Kai Prott

> With an implicit forall, the code does type check.

So to recap. Explicit/implicit forall doesn't seem to matter here (both compile, both work):

>    pattern Justy ::  a -> Maybe a
>    pattern Justy x = Just x

>

>    pattern Justy2 :: forall a. a -> Maybe a
>    pattern Justy2 x = Just x

(The docos for Pattern Synonyms don't give any examples with explicit `forall`; neither do they discuss whether it makes a difference. I'm inclined to say don't bother with outermost `forall`.)

But it does matter here:

>    data Some where
>      Some :: a -> Some
>
>    pattern Any :: a -> Some
>    pattern Any x = Some x
>
>    pattern Any2 :: forall a. a -> Some
>    pattern Any2 x = Some x

>

>    pattern Any3 :: (forall a. a) -> Some
>    pattern Any3 x = Some x

`Any` is accepted; `Any2` and `Any3` are rejected with a type mismatch/rigid tyvar message per your o.p. (I'm not surprised `Any3` is rejected.) The message complains about the binding line, not the signature. If you don't give a signature for `Any`, we get (with `-fprint-explicit-foralls`) `Any :: forall {a}. a -> Some`, which is the same as for `Justy, Justy2 :: forall {a}. a -> Maybe a` mutatis mutandis.

As to 'working', I presume your actual code doesn't merely have an existential for `Some`(?) but rather a constraint. Otherwise pattern-matching with `(Any x)` or with `(Some x)` you can't do anything with the `x` on RHS.

Your o.p. asked

> Is there a way around it, or is this a missing feature?

What feature would you like that you think is "missing"? Do you think a pattern's explicit `forall` for an existential data constructor should do something different vs for a regular datatype?

This could just be a stray loose end that nobody anticipated with Pattern Synonyms.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.