@@ -40,6 +40,9 @@ module TypeFun.Data.List
4040 , ElementIsUniq
4141 , UniqElements
4242 , UniqElements'
43+ -- * Helpers
44+ , appendId
45+ , subListId
4346 ) where
4447
4548import Data.Type.Bool
@@ -48,6 +51,7 @@ import GHC.TypeLits
4851import TypeFun.Data.Eq
4952import TypeFun.Data.Maybe
5053import TypeFun.Data.Peano
54+import Unsafe.Coerce
5155
5256------------------------------------------------------------------------
5357-- NOTE: Errors type classes. These type classes are not in separate --
@@ -104,6 +108,13 @@ type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
104108 '[] :++: b = b
105109 (a ': as) :++: b = a ': (as :++: b)
106110
111+appendId
112+ :: forall proxy l r
113+ . proxy l
114+ -> (l ~ (l :++: '[]) => r)
115+ -> r
116+appendId = unsafeCoerce id
117+
107118type IndexOf a s = FromJust (IndexOfMay a s)
108119
109120type IndexOfMay a s = IndexOfMay' Z a s
@@ -157,6 +168,12 @@ type family SubList (a :: [k]) (b :: [k]) :: Constraint where
157168 SubList '[] bs = ()
158169 SubList (a ': as) bs = (Elem a bs, SubList as bs)
159170
171+subListId
172+ :: forall proxy l r
173+ . proxy l
174+ -> (SubList l l => r) -> r
175+subListId _ = unsafeCoerce id
176+
160177type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
161178 NotSubList '[] bs = ()
162179 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)