@@ -6,7 +6,8 @@
66module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
77 Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
88 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9− Delete(..), Proxy(..), remove, Remove, (:\)) where
9+ Delete(..), Proxy(..), remove, Remove, (:\),
10+ Member) where
1011
1112import GHC.TypeLits
1213import Data.Type.Bool
@@ -15,7 +16,7 @@ import Data.Type.Equality
1516data Proxy (p :: k) = Proxy
1617
1718-- Value-level 'Set' representation, essentially a list
18−data Set (n :: [*]) where
19+data Set (n :: [k]) :: * where
1920 {--| Construct an empty set -}
2021 Empty :: Set '[]
2122 {--| Extend a set with an element -}
@@ -215,3 +216,14 @@ instance Conder False where
215216{-| Open-family for the ordering operation in the sort -}
216217
217218type family Cmp (a :: k) (b :: k) :: Ordering
219+
220+{-| Membership of an element in a set, with an acommanying
221+ value-level function that returns a bool -}
222+class Member a s where
223+ member :: Proxy a -> Set s -> Bool
224+
225+instance {-# OVERLAPS #-} Member a (a ': s) where
226+ member _ (Ext x _) = True
227+
228+instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where
229+ member a (Ext _ xs) = member a xs