<div><div>Thank's Kai-Oliver, it worked in the real setting as well, though the errors could be somewhat improved.<br></div><div><br></div><div>For example both of these type signatures are accepted:<br></div><div>```<br></div><div>pattern Any :: forall . forall a. () => () => a -> Some<br></div></div><div><br></div><div></div><div>pattern Any :: forall . () => forall a. () => a -> Some<br></div><div><div>```<br></div><div>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: <br></div><div><a href="https://github.com/input-output-hk/ouroboros-network/blob/coot/typed-protocols-rewrite/typed-protocols/src/Network/TypedProtocol/Peer/Client.hs#L97">https://github.com/input-output-hk/ouroboros-network/blob/coot/typed-protocols-rewrite/typed-protocols/src/Network/TypedProtocol/Peer/Client.hs#L97</a><br></div></div><div class="protonmail_signature_block"><div class="protonmail_signature_block-user protonmail_signature_block-empty"></div><div class="protonmail_signature_block-proton"><br>Thanks again both of you Kai & Anthony.<br>Have a nice Sunday,<br>Marcin<br><br>Sent with <a href="https://protonmail.com/" target="_blank">ProtonMail</a> Secure Email.</div></div><div><br></div><div class="protonmail_quote">
‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐<br>
On Sunday, September 19th, 2021 at 04:12, Kai-Oliver Prott <kai.prott@hotmail.de> wrote:<br>
<blockquote class="protonmail_quote" type="cite">
<p>I only followed the discussion relatively loosely, so apologies
if the following is not helpful.</p>
<p>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. <br>
</p>
<p>pattern Any2 :: forall . forall a. a -> Some<br>
</p>
<p>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.<br>
If none are given, GHC tries to infer any quantification. This
should be described in the "Pattern Synonyms" (Pickering et al)
paper.</p>
<p>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. <br>
</p>
<p>For constraints, there is a similar story w.r.t provided and
required constraints.<br>
<br>
Cheers,<br>
Kai Prott<br>
</p>
<div class="moz-cite-prefix">On 19.09.21 02:24, Anthony Clayden
wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr"><font face="arial, sans-serif">> <span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">With an implicit forall, the code does type check.</span><br>
<br>
</font>
<div><font face="arial, sans-serif">So to recap.
Explicit/implicit forall doesn't seem to matter here (both
compile, both work):</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif">> pattern Justy :: a
-> Maybe a<br>
> pattern Justy x = Just x<br>
</font></div>
<div><font face="arial, sans-serif">></font></div>
<div><font face="arial, sans-serif">> pattern Justy2 ::
forall a. a -> Maybe a<br>
> pattern Justy2 x = Just x<br>
</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif">(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`.)</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif">But it does matter here:</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif">> data Some where<br>
> Some :: a -> Some<br>
><br>
> pattern Any :: a -> Some<br>
> pattern Any x = Some x<br>
><br>
> pattern Any2 :: forall a. a -> Some<br>
> pattern Any2 x = Some x<br>
</font></div>
<div><font face="arial, sans-serif">></font></div>
<div><font face="arial, sans-serif">> pattern Any3 ::
(forall a. a) -> Some<br>
> pattern Any3 x = Some x<br>
</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif">`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.</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif">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.</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif">Your o.p. asked</font></div>
<div><font face="arial, sans-serif"><br>
</font></div>
<div><font face="arial, sans-serif">> <span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">Is there a way around it, or is this a missing feature?</span></font></div>
<div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="arial, sans-serif">
</font></span></div>
<div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="arial, sans-serif">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?</font></span></div>
<div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="arial, sans-serif">
</font></span></div>
<div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="arial, sans-serif">This could just be a stray loose end that nobody anticipated with Pattern Synonyms.</font></span></div>
<div><span style="color:rgb(0,0,0);font-size:1em;white-space:pre-wrap"><font face="arial, sans-serif">
</font></span></div>
<div><span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap">
</span></div>
</div>
<br>
<fieldset></fieldset>
<pre wrap="">_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank" rel="noreferrer nofollow noopener">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
Only members subscribed via the mailman list are allowed to post.</pre>
</blockquote>
</blockquote><br>
</div>