kind inference question

[Bernard James POPE]

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.