kind inference question
Bernard James POPE
Wed, 7 Feb 2001 18:22:18 +1100 (EST)
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).
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.