Question regarding the GHC users manual

[Max Bolingbroke]

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