Hi Tyson, I don't think this is a bug.
> type family F a b :: * -> * -- F's arity is 2, > -- although its overall kind is * -> * -> * -> * > F Char [Int] -- OK! Kind: * -> * Char :: * [Int] :: * So we can "fill" in the first two * in the kind * -> * -> * -> * to get * -> *, as reported. > F Char [Int] Bool -- OK! Kind: * Char :: * [Int] :: * Bool :: * As before, except that we can now fill in another * to get *. > F IO Bool -- WRONG: kind mismatch in the first argument IO :: * -> * Bool :: * Uh-oh! F has kind: * -> (* -> (* -> *)) And we are trying to do the application: F IO But IO :: * -> * /= * (the kind on the left of the arrow)! So we get a kind error. > F Bool -- WRONG: unsaturated application This is disallowed by the rules of type families. If unsaturated applications were allowed it would be well-kinded though, since Bool :: *. > and I'm wondering about the overall kind. Shouldn't that be * -> * -> *, or > am I not understanding something? I'm not sure what you think has gone wrong. * -> * -> * is the kind of something with two type arguments, but F clearly has 3 (two indexed ones, one parametric one). The inference rule you need to think of is something like: t1 :: k1 -> k2 t2 :: k1 -------------- t1 t2 :: k2 With axioms like (glossing over issues of saturation): ------------ Bool :: * --------------- IO :: * -> * -------------------------- F :: * -> * -> * -> * GHC's kind system is actually even more complicated than this due to subkinding, but you usually don't have to worry about that. Cheers, Max _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users