type family IndexC (n :: Nat) (i :: Nat) (a :: k1) = (r :: k2)

type family GetConstructor1 a where ...

type family GetConstructor2 a where ...

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