@@ -1,11 +1,11 @@
11{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
22 MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
3− UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}
3+ UndecidableInstances, ConstraintKinds, ScopedTypeVariables #-}
44
55module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
66 Sort, Sortable, Append(..), Split(..), Cmp,
77 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
8− (:->)(..), Var(..)) where
8+ (:->)(..), Var(..), Delete(..)) where
99
1010import GHC.TypeLits
1111import Data.Type.Bool
@@ -144,6 +144,15 @@ type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
144144 Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs)
145145 Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs)
146146
147+type family DeleteFromList (e :: elem) (list :: [elem]) where
148+ DeleteFromList elem '[] = '[]
149+ DeleteFromList elem (x ': xs) = If (Cmp elem x == EQ)
150+ xs
151+ (x ': DeleteFromList elem xs)
152+
153+type family Delete elem set where
154+ Delete elem (Set xs) = Set (DeleteFromList elem xs)
155+
147156{-| Value-level quick sort that respects the type-level ordering -}
148157class Sortable xs where
149158 quicksort :: Set xs -> Set (Sort xs)