[Haskell-cafe] Type-level list "elem" inference

[amindfv at gmail.com]

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