[Haskell-cafe] Pattern synonyms and explicit forall.

[Kai-Oliver Prott]

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/b0da4a7e/attachment.html>