<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<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" cite="mid:CABU_mxhPYCkiOi7GK+L=-oK3dnuR7KUJXWcxv=D6ofE5ix-t_g@mail.gmail.com">
<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 class="gmail-Apple-interchange-newline">
</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 class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
Only members subscribed via the mailman list are allowed to post.</pre>
</blockquote>
</body>
</html>