module Data.HSet.TypeLevel where

data Nat = Z | S Nat

-- | Calculates to 'True if first type argument contained in second
-- list element
type family Elem (typ :: k) (typs :: [k]) :: Bool where
    Elem typ '[]             = 'False
    Elem typ (typ ': typs)   = 'True
    Elem typ1 (typ2 ': typs) = Elem typ1 typs

-- | Calculates to Nat kinded type describing the index of first argument in second argument
type family Index (typ :: k) (typs :: [k]) :: Nat where
  Index t (t ': ts) = 'Z
  Index t (tt ': ts) = 'S (Index t ts)