{-# LANGUAGE DataKinds, TypeFamilies #-}

module In where

data L = L1 | L2

data Foo (xs :: [L]) where
  T1 :: L1 `In` xs => Foo xs
  T2 :: L2 `In` xs => Foo xs

type x `In` xs = x `Elem` xs ~ True

type Elem :: k -> [k] -> Bool
type family x `Elem` xs where
  x `Elem` '[    ] = False
  x `Elem`  (x:ys) = True
  x `Elem`  (y:xs) = x `Elem` xs

test :: Foo '[L1] -> ()
test T1 = ()