So it's the same type `a` all the way down, and therefore the same instance for the constraint(s). Consider (adapted from the H98 Report for DatatypeContexts):
{-# LANGUAGE GADTs #-}
data SetG a where
NilSetG :: Eq a => SetG a
ConsSetG :: Eq a => a -> SetG a -> SetG a
elemSG x NilSetG = False
elemSG x (ConsSetG y ys) | x == y = True
| otherwise = elemSG x ys
-- ===> elemSG :: a -> SetG a -> Bool -- no Eq a inferred
The elem pattern matching test makes use of ConsSetG's Eq instance, but doesn't expose that in the inferred type. Whereas:
headS (ConsSetG x _) = x -- hide the pattern match
tailS (ConsSetG _ xs) = xs
elemSh x NilSetG = False
elemSh x yss | x == headS yss = True
| otherwise = elemSG x $ tailS yss
-- ==> elemSh :: Eq a => a -> SetG a -> Bool -- Eq a inferred
It seems you can get there with PatternSynonyms, using an explicit signature with 'required' constraints:
pattern ConsSetPS x yss = ConsSetG x yss
-- inferred pattern ConsSetPS :: () => Eq a => a -> SetP a -> SetP a -- that is, if no sig given
Using `ConsSetPS` as the pattern in `elemSG` with that default/inferred signature gives the same typing as using the GADT constructor. But with explicit signature
pattern ConsSetPS :: Eq a => a -> SetG a -> SetG a
-- longhand :: Eq a => () => a -> SetG a -> SetG a
The 'required' `Eq a` is exposed, so `elemSG` gets the same signature as `elemSh` above.
After all, if you're trying to maintain an invariant, you'd be using a PatternSynonym as 'smart constructor' to validate uniqueness; so giving it a signature (and hiding the GADT constructor) is easy enough.
Would be nice to be able to give pattern-style signatures for GADT constructors. Unfortunately, the sigs for `ConsSetG` and `ConsSetPS` look the same but mean the opposite way round.
AntC