Thanks to Richard's hard work, I can now define kind classes! class Extractable k where type Extract (n :: Nat) (x :: k) :: y (For context, Extract is something roughly resembling the X type family in the paper Generic Programming for Indexed Datatypes. [1]) This is really, really cool. Except that when I tried using this class, I quickly ran into issues: instance Extractable (a, b) where type Extract 0 '(l, _) = l type Extract 1 '(_, r) = r type Extract _ _ = TypeError ('Text "out of bounds") This yields the error: Extractable.hs:16:8: error: Conflicting family instance declarations: forall a b (r :: b) (_ :: a). Extract 1 '(_, r) = r -- Defined at Extractable.hs:16:8 forall a b (_ :: Nat) (_1 :: (a, b)) y. Extract _ _1 = (TypeError ...) -- Defined at Extractable.hs:17:8 It hit me as to why: GHC is interpreting each Extract type instance as being separate from each other, not as a part of a single, closed type family over kind (a, b). And as it turns out, GHC does not allow closed associated type families. [2] That leads me to wonder: is there a particular reason why GHC couldn't allow closed associated type families? Because of this restriction, I have to define the Extractable (a, b) instance like this: instance Extractable (a, b) where type Extract n p = ExtractPair n p type family ExtractPair (n :: Nat) (x :: (a, b)) :: y where ExtractPair 0 '(a, _) = a ExtractPair 1 '(_, b) = b ExtractPair _ _ = TypeError ('Text "out of bounds") But that requires -XUndecidableInstances, and makes it much more difficult to examine type family reductions with GHCi's :kind! command. Ryan S. ----- [1] http://dreixel.net/research/pdf/gpid.pdf [2] https://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#syno...