@@ -1,13 +1,12 @@
11{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
22 MultiParamTypeClasses, FlexibleInstances, PolyKinds,
33 FlexibleContexts, UndecidableInstances, ConstraintKinds,
4− ScopedTypeVariables, TypeInType #-}
4+ ScopedTypeVariables #-}
55
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, (:\),
10− Member(..), NonMember, MemberP(..)) where
9+ Delete(..), Proxy(..)) where
1110
1211import GHC.TypeLits
1312import Data.Type.Bool
@@ -16,7 +15,7 @@ import Data.Type.Equality
1615data Proxy (p :: k) = Proxy
1716
1817-- Value-level 'Set' representation, essentially a list
19−data Set (n :: [k]) where
18+data Set (n :: [*]) where
2019 {--| Construct an empty set -}
2120 Empty :: Set '[]
2221 {--| Extend a set with an element -}
@@ -74,25 +73,6 @@ append :: Set s -> Set t -> Set (s :++ t)
7473append Empty x = x
7574append (Ext e xs) ys = Ext e (append xs ys)
7675
77−{-| Delete elements from a set -}
78−type family (m :: [k]) :\ (x :: k) :: [k] where
79− '[] :\ x = '[]
80− (x ': xs) :\ x = xs :\ x
81− (y ': xs) :\ x = y ': (xs :\ x)
82−
83−class Remove s t where
84− remove :: Set s -> Proxy t -> Set (s :\ t)
85−
86−instance Remove '[] t where
87− remove Empty Proxy = Empty
88−
89−instance {-# OVERLAPS #-} Remove xs x => Remove (x ': xs) x where
90− remove (Ext _ xs) x@Proxy = remove xs x
91−
92−instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
93− => Remove (y ': xs) x where
94− remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
95−
9676{-| Splitting a union a set, given the sets we want to split it into -}
9777class Split s t st where
9878 -- where st ~ Union s t
@@ -113,6 +93,8 @@ instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
11393 split (Ext x st) = let (s, t) = split st
11494 in (s, Ext x t)
11595
96+
97+
11698{-| Remove duplicates from a sorted list -}
11799type family Nub t where
118100 Nub '[] = '[]
@@ -148,10 +130,10 @@ class Subset s t where
148130instance Subset '[] '[] where
149131 subset xs = Empty
150132
151−instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
133+instance Subset s t => Subset s (x ': t) where
152134 subset (Ext _ xs) = subset xs
153135
154−instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
136+instance Subset s t => Subset (x ': s) (x ': t) where
155137 subset (Ext x xs) = Ext x (subset xs)
156138
157139
@@ -216,21 +198,3 @@ instance Conder False where
216198{-| Open-family for the ordering operation in the sort -}
217199
218200type 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
230−
231−type family MemberP a s :: Bool where
232− MemberP a '[] = False
233− MemberP a (a ': s) = True
234− MemberP a (b ': s) = MemberP a s
235−
236−type NonMember a s = MemberP a s ~ False