type IndexC n i a

type family IndexCK k (n :: Nat) (i :: Nat) a = (r :: k)

type family GetConstructor1 a where ...

type family GetConstructor2 a where ...

type family IsData (n :: Nat) a :: Constraint