Typing of Pattern Synonyms: Required vs Provided constraints

[Anthony Clayden]

There was an interesting exchange between the authors of Haskell compilers
back in 1999 (i.e. when there were multiple compilers)
http://web.archive.org/web/20151001142647/http://code.haskell.org/~dons/haskell-1990-2000/msg04061.html

I was trying to simulate SPJ's point of view, using PatternSynonyms.

>
>    {-#  LANGUAGE DatatypeContexts, PatternSynonyms  #-}
>
>    data Ord a => TSPJ a = MkTSPJ a a
>
>    pattern PatTSPJ :: (Ord a) => () => a -> a -> TSPJ a    -- empty
Provided
>    pattern PatTSPJ x y = MkTSPJ x y
>
>    unPatTSPJ :: TSPJ a -> (a, a)                            -- no
constraints
>    unPatTSPJ (PatTSPJ x y) = (x, y)
>

`unPatSPJ`'s binding rejected `No instance for (Ord a) arising from a
pattern`. If I don't give a signature, inferred `unPatTSPJ :: Ord b => TSPJ
b -> (b, b)`.

Taking the DatatypeContext off the `data` decl doesn't make a difference.

So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.

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."

Or ... is there some way to simulate the up-to-1999 GHC behaviour? (I
happen to agree with SPJ; Wadler wasn't thinking it through; consider for
example constructor classes over type constructors with constraints:
there's nothing in the instance head for the constraint to attach to. Now
that we have GADTs -- which are appropriate for a different job -- that DT
Contexts perhaps were being (ab-)used for -- I agree more strongly with
SPJ.)

With GADTs I could get a `unGSPJ` that doesn't expose/provide the
constraint, but it does that by packing the constraint/dictionary
(polluting) inside the data constructor. Not  what I want. As SPJ says
down-thread

 "when you take a constructor *apart*, the invariant must hold
	by construction: you couldn't have built the thing you are taking
	apart unless invariant held.  So enforcing the invariant again is
	redundant; and in addition it pollutes the type of selectors."


AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20220106/24b56d7a/attachment.html>