So I've got some code that looks like: {-# LANGUAGE DataKinds, UndecidableInstances, TypeFamilies, KindSignatures, TypeOperators #-} import Data.Proxy import GHC.TypeLits type family IsSubset (as :: [Symbol]) (bs :: [Symbol]) where IsSubset as bs = IsSubsetPrime as bs bs type family IsSubsetPrime (as :: [Symbol]) bs bs' where IsSubsetPrime as '[] bs' = 'False IsSubsetPrime '[] bs bs' = 'True IsSubsetPrime (a ': as) (a ': bs) bs' = IsSubsetPrime as bs' bs' IsSubsetPrime (a ': as) (b ': bs) bs' = IsSubsetPrime (a ': as) bs bs' This lets me write functions like: foo :: (IsSubset '["foo", "bar"] args ~ 'True) => Proxy args -> Int foo args = undefined I've also got a type family: type family IsElem (a :: Symbol) (bs :: [Symbol]) where IsElem a (a ': bs) = 'True IsElem a (b ': bs) = IsElem a bs IsElem a '[] = 'False This lets me write functions like: bar :: (IsElem "foo" args ~ 'True) => Proxy args -> Int bar args = undefined The problem comes when I want to use "bar args" in the definition of "foo args" -- even though it's clear to me that ["foo","bar"] being a subset of args implies that "foo" is an element of args, I haven't written "IsElem" or "IsSubset" in a way that it's clear to the compiler. Is there a way to write IsElem and IsSubset so they "compose"? Thanks! Tom