Hi all, I'm in the middle of writing kind inference for haskell, as part of a type checker/inferer. After reading the section in the haskell report about kind inference (section 4.6), I began to wonder why kind inference must be done in dependency order. Some friends and I came up with the following example which raises an issue: data C x = Foo (B x) (x Int) data B y = Bar According to the report (and ghc and hugs) this is ill-kinded. The reason is that kinds must be inferred in dependency order, and when parts of a kind are not fully determined they default to * (star). So: inferring the kind of B first gives: kind (B) = * -> * this results in a kind error because in the definition of C, B must have kind (* -> *) -> *, which differs from the inference made above However, an alternative kind inference algorithm might allow the above declarations, by performing kind inference of C and B together (effectively unifying the kind of x and the kind of y). This would result in: kind (C) = (* -> *) -> * kind (B) = (* -> *) -> * I'm not suggesting that allowing this inference would be a good idea, but I am wondering why haskell requires the dependency ordering. Perhaps there are better examples that elucidate the motivation for dependency ordering. Basically I'm just curious. Regards Bernie.