Rejigger roles for kind coercions.

Upshot of this all: a proof of (t1 ~r t2) proves both that t1 and t2
are r-equal *and* that k1 and k2 are r-equal (where k1 and k2 are
the kinds of t1 and t2). This is a change from previously, where all
kind coercions were nominal.... but this seemed wrong because a kind
cast used a nominal coercion instead a representational coercion like
a term cast.

This commit includes some unfinished work in normalise_type and in
ty_co_subst. It seems that we'll need yet another coercion form to
finish these functions. Argh. Waiting to consult with SCW before
deciding how to proceed.