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