[Haskell-cafe] Pattern synonyms and explicit forall.

[coot at coot.me]

Thank's Kai-Oliver,  it worked in the real setting as well, though the errors could be somewhat improved.

For example both of these type signatures are accepted:
```
pattern Any :: forall . forall a. () => () => a -> Some

pattern Any :: forall . () => forall a. () => a -> Some
```
But in my real scenario the first one is giving a puzzling error about the pattern match number of arguments not agreeing with the number of arrows in the type. I  needed to realized that the second type makes more sense, and it worked.  Btw the real thing I was trying to type with explicit quantification / existentials is this one:
https://github.com/input-output-hk/ouroboros-network/blob/coot/typed-protocols-rewrite/typed-protocols/src/Network/TypedProtocol/Peer/Client.hs#L97

Thanks again both of you Kai & Anthony.

Have a nice Sunday,

Marcin

Sent with ProtonMail Secure Email.

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐

On Sunday, September 19th, 2021 at 04:12, Kai-Oliver Prott <kai.prott at hotmail.de> wrote:

> 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
> 

> On 19.09.21 02:24, Anthony Clayden wrote:
> 

> > > 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210919/02bfd09d/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 509 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210919/02bfd09d/attachment-0001.sig>