Kind classes and associated closed type families

Richard Eisenberg eir at
Fri Dec 18 18:56:06 UTC 2015

On Dec 18, 2015, at 1:37 PM, Ryan Scott < at> wrote:

> 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]

Yes, that's exactly right.

> That leads me to wonder: is there a particular reason why GHC couldn't
> allow closed associated type families?

No. At the time, we thought that associated closed type families are easy enough to build (as you do here) and just one more wrinkle that GHC didn't need. No theoretical trouble at all. Just some routine engineering, I imagine.

> 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.

Why does this interfere with :kind! ? It shouldn't. (Yes, the -XUndecidableInstances is regrettable. We really need a better type-level termination checker. Care to write one? :)  )


> Ryan S.
> -----
> [1]
> [2]
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at

More information about the ghc-devs mailing list