
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/hask... 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... 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