Re: [Haskell-cafe] Pattern synonyms and explicit forall.
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.
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.
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-protoco...
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
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.
participants (3)
-
Anthony Clayden -
coot＠coot.me -
Kai-Oliver Prott