Hello,

It means that Kinds are represented by Types.

Admittedly, Kinds only use a small fragment of what Types can represent, namely Arrow, and type constructor applications. So * is represented by a TyConApp with a TyCon that is called typeCon.

The really annoying thing about Kinds is that there's occasionally a bit of sub-kinding. In particular

error :: forall a. String -> a

We want to allow error "foo" :: Int#

I have subkinding in my calculus as well, but in a completely different context. For instance, the kind of Either is + -> + -> * because Either is covariant in its arguments. But the kind of Either is also x -> x -> * (x=invariance). So we have + -> + -> * as the most specific kind of Either. Note, that the kind arrow in my system is contravariant as well. I think, that is a nice analogy to the type system. For example, let tau_1:(x -> *) -> *, tau_2:(+ -> *) -> *. Then tau_1 is usable whenever tau_2 is in operation. So from (+ -> *) <: (x -> *) it follows in my system, that (x -> *) -> * <: (+ -> *) -> *. Unfortunately I have to decide two contexts of the kind arrow. To understand this, consider my definition of kinds: Def.: Kinds are inductively defined as follows: * is a kind if kappa1 and kappa2 are kinds, then kappa1 -> kappa2 is a kind if kappa is a kind, then + -> kappa, - -> kappa, x -> kappa and alpha -> kappa alpha is a so-called kind variable, that can be instantiated by +, - or x (not by arbitrary kinds!). Further on, we have the convention, that * -> kappa has to be seen as x -> kappa. What do we mean by the term kind variable? A type tau may have the kind (alpha->beta->*)->alpha->beta->*. If one applies this type, e.g., to the arrow type constructor one gaines (tau (->)): - -> + -> *. So information about variances is propagated. This allows for subtyping in a convenient manner.

so the kind of 'a' can't be *, nor # (the kind of unboxed types). It's an "open" kind, written "?"; both * and # are sub-kinds of ?.

I have read about this issue in the sources of the GHC. I try to understand...

You should nevertheless be able to encode your kind system in the same way as GHC does.

This is a pity, because my kind system allows for a really nice type inference algorithm, that can deal with higher-kinded types properly. I hope, that I can transfer it to the GHC. I will write a short section for the commentary as soon as I completely understand the GHC kind system.

But I have been thinking that it's over-kill to use Types for Kinds, and leads to no real saving.

I think so, too, because the system from "Typing Haskell in Haskell" is very easy to understand and extend. Another advantage is, that it is closer to the Haskell report.

I may well split the two types in the future.

This would be great. Thank you for the informations, Steffen Mazanek