module Data.HSet.TypeLevel where

data Nat = Z | S Nat

type family Elem (typ :: *) (typs :: [*]) :: Bool where
    Elem typ '[]             = 'False
    Elem typ (typ ': typs)   = 'True
    Elem typ1 (typ2 ': typs) = Elem typ1 typs

type family Index (typ :: *) (typs :: [*]) :: Nat where
  Index t (t ': ts) = 'Z
  Index t (tt ': ts) = 'S (Index t ts)