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 aStar)). 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