Typing of Pattern Synonyms: Required vs Provided constraints

[Gergő Érdi]

Fwiw, a less contrived, and much more relatable, version of Richard's
example would be


pattern Is3 :: (Num a, Eq a) => a   -- only a Required constraint
pattern Is3 = 3 -- a polymorphic literal!

I think it can be quite instructive for people new to patsyn typing to work
out why this is exactly the same as the one in Richard's email!


On Thu, Jan 6, 2022, 21:11 Richard Eisenberg <lists at richarde.dev> wrote:

>
>
> On Jan 5, 2022, at 9:19 PM, Anthony Clayden <anthony.d.clayden at gmail.com>
> wrote:
>
> So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.
>
>
> In your example, yes: the Required context is "stupid" in the way that
> "stupid theta" is. The reason to have a Required context is if your pattern
> synonym does computation that requires a constraint. For example:
>
> pattern Is3 :: (Num a, Eq a) => a   -- only a Required constraint
> pattern Is3 = ((==) 3 -> True)   -- that's a view pattern
>
> In your case, there is no computation (your pattern synonym just stands
> for a constructor), so the Required context is unhelpful (and does indeed
> act just like a datatype context).
>
>
> The User Guide
> https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms
>  says
>
>
>    - ⟨CProv⟩ are the constraints *made available (provided)* by a
>    successful pattern match.
>
> But it doesn't mean that. It's more like "⟨CProv⟩ are the constraints
> made available *in addition to ⟨CReq⟩* (provided union required) by a
> successful pattern match."
>
>
> I agree with the user guide here: the Provided constraints are made
> available. The Required constraint must *already* be available before the
> pattern match, so they are not made available *by* the match. It is true,
> though, that in the context of the match, both the Provided and the
> Required constraints must be satisfiable.
>
> To get the pre-1999 behavior, you would need a different type for a
> pattern synonym used as a pattern than for one used as an expression. This
> is the subject of the accepted-but-not-implemented
> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst
>
> Richard
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20220106/b7b56f66/attachment.html>