<div dir="ltr"><font face="monospace">There was an interesting exchange between the authors of Haskell compilers back in 1999 (i.e. when there were multiple compilers) <a href="http://web.archive.org/web/20151001142647/http://code.haskell.org/~dons/haskell-1990-2000/msg04061.html">http://web.archive.org/web/20151001142647/http://code.haskell.org/~dons/haskell-1990-2000/msg04061.html</a></font><div><font face="monospace"><br></font></div><div><font face="monospace">I was trying to simulate SPJ's point of view, using PatternSynonyms.</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">></font></div><div><font face="monospace">>    {-#  LANGUAGE DatatypeContexts, PatternSynonyms  #-}</font></div><div><font face="monospace">></font></div><div><font face="monospace"><span style="font-size:1em;color:rgb(0,0,0)">>    </span>data Ord a => TSPJ a = MkTSPJ a a<br></font></div><font face="monospace">></font><div><font face="monospace">>    pattern PatTSPJ :: (Ord a) => () => a -> a -> TSPJ a    -- empty Provided<br>>    pattern PatTSPJ x y = MkTSPJ x y<br>></font></div><div><font face="monospace">>    unPatTSPJ :: TSPJ a -> (a, a)                            -- no constraints<br>>    unPatTSPJ (PatTSPJ x y) = (x, y)</font></div><div><font face="monospace">></font></div><div><font face="monospace"><br></font></div><div><font face="monospace">`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)`.</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">Taking the DatatypeContext off the `data` decl doesn't make a difference.</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">The User Guide <a href="https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms">https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms</a> says</font></div><div><font face="monospace"><br></font></div><ul class="gmail-simple" style="color:rgb(0,0,0);font-size:14px"><li style="hyphens: auto;"><p style="margin:0px"><font face="monospace">⟨CProv⟩ are the constraints <em>made available (provided)</em> by a successful pattern match.</font></p></li></ul><div><font face="monospace"><font color="#000000"><span style="font-size:14px">But it doesn't mean that. It's more like "</span></font><span style="color:rgb(0,0,0);font-size:14px">⟨CProv⟩ are the constraints made available *in addition to </span><span style="color:rgb(0,0,0);font-size:14px">⟨CReq⟩* (provided union required) by a successful pattern match."</span></font></div><div><span style="color:rgb(0,0,0);font-size:14px"><font face="monospace"><br></font></span></div><div><span style="color:rgb(0,0,0);font-size:14px"><font face="monospace">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.)</font></span></div><div><span style="color:rgb(0,0,0);font-size:14px"><font face="monospace"><br></font></span></div><div><span style="color:rgb(0,0,0)"><font face="monospace" style="">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</font></span></div><div><span style="color:rgb(0,0,0)"><font face="monospace"><br></font></span></div><div><pre style="color:rgb(0,0,0)"><font face="monospace" size="2"> "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."</font></pre></div><div><span style="color:rgb(0,0,0);font-size:14px"><font face="monospace"><br></font></span></div><div><span style="color:rgb(0,0,0);font-size:14px"><font face="monospace">AntC</font></span></div><div><span style="color:rgb(0,0,0);font-size:14px"><br></span></div></div>