I must be slow on the uptake. I've just grokked this equivalence -- or is it? Consider

>    data Eq a => Set a = NilSet | ConsSet a (Set a)     -- from the Language report
>
>    -- ConsSet :: forall a. Eq a => a -> Set a => Set a   -- inferred/per report
>
>    --  equiv with Pattern syn 'Required' constraint
>    data Set' a = NilSet' | ConsSet' a (Set' a)     -- no DT context
>
>    pattern ConsSetP :: (Eq a) => () => a -> (Set' a) -> (Set' a)
>    pattern ConsSetP x xs = ConsSet' x xs
>
>    ffP ((ConsSet x xs), (ConsSetP y ys)) = (x, y)
>
>    -- ffP :: forall {a} {b}. (Eq a, Eq b) => (Set a, Set' b) -> (a, b)   -- inferred

The signature decl for `ConsSetP` explicitly gives both the Required `(Eq a) =>` and Provided `() =>` constraints, but the Provided could be omitted, because it's empty. I get the same signature for both `ConsSetP` as `ConsSet` with the DT Context. Or is there some subtle difference?

This typing effect is what got DT Contexts called 'stupid theta' and deprecated/removed from the language standard. ("widely considered a mis-feature", as GHC is keen to tell me.) If there's no difference, why re-introduce the feature for Patterns? That is, why go to the bother of the double-context business, which looks weird, and behaves counter to usual signatures:

>    foo :: (Eq a) => (Show a) => a -> a
>    --   foo :: forall {a}. (Eq a, Show a) => a -> a     -- inferred

There is a slight difference possible with Pattern synonyms, compare:

>    pattern NilSetP :: (Eq a) => () => (Set' a)
>    pattern NilSetP = NilSet'
>
>    -- NilSetP :: forall {a}. Eq a => Set' a             -- inferred
>    -- NilSet   :: forall {a}.      => Set a                   -- inferred/per report

Using `NilSetP` somewhere needs giving an explicit signature/otherwise your types are ambiguous; but arguably that's a better discipline than using `NilSet` and allowing a Set with non-comparable element types.

AntC