Kind classes and associated closed type families

[Ryan Scott]

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#synonym-families