Re: [Caml-list] Problem with universal functions in a module

[Leo White <lpw25@cam.ac.uk>]

> I don't see anything to infere there. Only thing I see is that in the
> case of mono the universal function has to be unified with a single
> type function. But 'a . 'a -> 'a should unify with int -> int
> resulting in int -> int without problems.

'a. 'a -> 'a cannot unify with int -> int. If it did then 'a. 'a -> 'a
wouldn't be polymorphic: it could not be used as both int -> int and
float -> float. Instead 'a. 'a -> 'a must be instantiated to 'b -> 'b
which can then be unified with int -> int. It is the descision whether
or not to perform this instantiation that needs to be infered.

To understand the full range of issues associated with higher-rank and
impredicative polymorphism I suggest reading the relevant literature
(e.g. "MLF: raising ML to the power of system F", "Semi-explicit
first-class polymorphism for ML", "Flexible types: robust type inference
for first-class polymorphism", "Boxy types: inference for higher-rank
types and impredicativity", ...).

Regards,

Leo