> 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 <[email protected]> wrote: > > On Dec 18, 2015, at 1:37 PM, Ryan Scott <[email protected]> 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#synonym-families >> _______________________________________________ >> ghc-devs mailing list >> [email protected] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
