[Haskell-cafe] Pattern synonyms and explicit forall.

[Anthony Clayden]

> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210919/2d154f1a/attachment.html>