@@ -40,6 +40,9 @@ module TypeFun.Data.List
40 , ElementIsUniq
40 , ElementIsUniq
41 , UniqElements
41 , UniqElements
42 , UniqElements'
42 , UniqElements'
45import Data.Type.Bool
48import Data.Type.Bool
@@ -48,6 +51,7 @@ import GHC.TypeLits
48import TypeFun.Data.Eq
51import TypeFun.Data.Eq
49import TypeFun.Data.Maybe
52import TypeFun.Data.Maybe
50import TypeFun.Data.Peano
53import TypeFun.Data.Peano
52------------------------------------------------------------------------
56------------------------------------------------------------------------
53-- NOTE: Errors type classes. These type classes are not in separate --
57-- NOTE: Errors type classes. These type classes are not in separate --
@@ -104,6 +108,13 @@ type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
104 '[] :++: b = b
108 '[] :++: b = b
105 (a ': as) :++: b = a ': (as :++: b)
109 (a ': as) :++: b = a ': (as :++: b)
114+ -> (l ~ (l :++: '[]) => r)
116+appendId = unsafeCoerce id
107type IndexOf a s = FromJust (IndexOfMay a s)
118type IndexOf a s = FromJust (IndexOfMay a s)
109type IndexOfMay a s = IndexOfMay' Z a s
120type IndexOfMay a s = IndexOfMay' Z a s
@@ -157,6 +168,12 @@ type family SubList (a :: [k]) (b :: [k]) :: Constraint where
157 SubList '[] bs = ()
168 SubList '[] bs = ()
158 SubList (a ': as) bs = (Elem a bs, SubList as bs)
169 SubList (a ': as) bs = (Elem a bs, SubList as bs)
174+ -> (SubList l l => r) -> r
175+subListId _ = unsafeCoerce id
160type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
177type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
161 NotSubList '[] bs = ()
178 NotSubList '[] bs = ()
162 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
179 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)