Re: Kind classes and associated closed type families

Why does this interfere with :kind! ? It shouldn't.

Well, it seems to interfere in my usage of it, at least:

:kind! Extract 0 '(Int, Char) Extract 0 '(Int, Char) :: y = ExtractPair 0 '(Int, Char)

I presumed this was because :kind! didn't do any type family reduction whenever something was undecidable in general (to ensure :kind! always terminates, I suppose). Ryan S. On Fri, Dec 18, 2015 at 10:56 AM, Richard Eisenberg wrote:

On Dec 18, 2015, at 1:37 PM, Ryan Scott 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? :) )

Richard

...

Ryan S. ----- [1] http://dreixel.net/research/pdf/gpid.pdf [2] https://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#syno... _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs