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