seemingly inconsistent behavior for "kind-indexed" type constraints in GHC 7.6

[Nicolas Frisby]

Just in case anyone is following along at home, here's what I'm going with.

> type TakeN n ts = TakeNDropM n Z ts
>
> type family TakeNDropM (n :: Nat) (which :: Nat) (ts :: [k]) :: [k]
> type instance TakeNDropM Z     which ts = '[]
> type instance TakeNDropM (S n) which ts = Nth which ts ': TakeNDropM n (S which) ts
>
> class (ts ~ TakeN n ts) => NLong (n :: Nat) (ts :: [k])

(Turns out the coercion method itself is unnecessary in this case.)

Now I just have to "prove" it (by using the requisite ~ constraints on
ts) via instances… in the morning. I think this solution will work out
nicely, based on my previous experiences.

It may turn out to be interesting to compare this convention (of
sprinkling NLong constraints everywhere) to the intended behavior of
using a promoted vector GADT for the kind of ts — eg (ts :: Vec n k).

Thanks for the help, Richard and Gábor. To everyone else, sorry for
the noise/HTH in the future.

On Mon, Oct 8, 2012 at 1:52 AM, Nicolas Frisby <nicolas.frisby at gmail.com> wrote:
> On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> For similar reasons, GHC does not bring the constraints on an instance into the context when an instance matches. So, even if GHC did select the instance you want, it would not bring ('[] ~ ps) into the context.
>
> Ah, of course. I was naively letting myself regarding NLong by its
> semantics and not by its instances. Silly mistake.
>
> Part of the reason I made that mistake is that NLong is having the
> desired effect on my program in other situations (as my second gist
> demonstrates). I still need to characterize how that's working for me
> there, but I'm sure your clarification here will surely guide me when
> doing so. Thank you.
>
> In past situations like this one, I have effected the desired
> implication (to the instance context as instead of to the superclass)
> via a coercion, which I make into a rank2 method of the class. It's
> just rather tricky to express the type of the coercion in this case,
> because of the involved Nat. I'm working on it now.