I think I get it with the "unusual form" of constraints. Just checking ...
The examples in that section for Provided constraints (the second one) all seem to involve GADTs/existentials inside the data constructor(?) With the answer here, I'm not sure if an existential is involved (in the Vinyl library), but the type for rhead
has a more specific type than the argument that f
is passing to it. And tbh the PatternSynonym
seems to be a red herring: the arguments to OnlyRecord
don't appear on f
's rhs.
Required constraints (the first one of two, or the only one if there's one) seem to give the same functionality as the now-deprecated DatatypeContexts
(?) For example
data NoCSet a where -- no constraints on the datatype
NilSet_ :: NoCSet a
ConsSet_ :: a -> NoCSet a -> NoCSet a
deriving (Eq, Show, Read)
pattern ConsSet :: (Eq a) => () => a -> NoCSet a -> NoCSet a
-- Req'd => Prov'd => type; Prov'd is empty, so omittable
pattern ConsSet x xs = ConsSet_ x xs
pattern NilSet :: (Eq a) => () => NoCSet a
pattern NilSet = NilSet_
ccUnit = ConsSet () NilSet -- accepted
-- ccid = ConsSet id NilSet -- rejected no instance Eq (a -> a)
-- ncid = NilSet :: NoCSet (a -> a) -- ditto
with the extra advantage I can put a Required constraint on a pattern NilSet
without an argument, disallowing building even an empty set with an unacceptable type. DatatypeContexts
for constructors like that just ignore the constraint.
Edit/focussed question: (response to @Noughtmare comment)
Is there an observable difference between pattern ConsSet
defined above vs constructor DCConsSet
here:
data (Eq a) => DCSet a = -- constraint on the datatype
DCNilSet
| DCConsSet a (DCSet a)
deriving (Eq, Show, Read)
I mean "difference" other than one's a pattern, one's a constructor. I've tried using them in both building and matching values; I get same behaviour.