[Haskell-cafe] Pattern synonyms and explicit forall.
coot at coot.me
coot at coot.me
Sun Sep 19 07:49:38 UTC 2021
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>
More information about the Haskell-Cafe
mailing list