The new Haskell report 1.3 (preliminary) allows type variables of
other kinds than *, e.g. it gives the example (page 51)
data App f a = A (f a)
where the type variable f has kind *->*, and App has (*->*)->*->*.
My problem is that I haven't seen (in the report) any mention
about the interaction of this with type inference.
Take for instance the declaration:
something = A ()
what is the type of something ?
It could be App (\x->x) (), but it could also be
App (\x->()) a, for any type a, and a few others.
But these are different types and it matters for type inference which
one we choose, there is no longer a most general type, a principal type.
Basically, these are the usual problems with higher-order unification
(including that it's undecidable).
I'm not arguing against this feature, I'm just complaining that the
report doesn't say anything about the problem of what do with
non-determined higher-order types during type inference.
--
Stefan Kahrs
