GHC and Kinds

[Steffen Mazanek]

Hello again,

I have browsed the GHC commentary and I could not find
a lot of information about kinds. But kinds are very
important for my implementation! The parser seems to
call liftedTypeKind from TypeRep. But in TypeRep we
have 

type Kind = Type

What does this mean? 

I briefly explain the basics of my algorithm, so that
you see how much it depends on the notion of Kinds.
I have the following declaration:

data Kind = KVar Kindvar --kind variables
    | KVarInv Kindvar --inversion of kind variables
    | Star --corresponds to *
    | Cov --corresponds to +
    | Contr --corresponds to - 
    | Inv  --corresponds to x
    | Kind :-> Kind --function kind
		   deriving Eq

The new atomic kinds Cov, Contr and Inv can be explained
by some examples. In my system, the list type constructor,
that is covariant in its argument, i.e., ([] a)<([] b) 
whenever a<b, is represented by (Tycon "[]" (Cov:->Star)).
In contrast, the arrow type constructor's kind is given
by (Contr:->(Cov:->Star)) due to its contravariance.
If one tries to establish a subtype relationship, kinds
are taken into consideration.

How can I gently integrate this behavior in the GHC?
Till now I have worked with "Typing Haskell in Haskell"
and I really expected a declaration like

data Kind = Star | Kfun Kind Kind

Any help is greatly appreciated.

Regards,
Steffen Mazanek