Re: [Caml-list] Type system infering 'a and '_a

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Tom <tom.primozic@gmail.com>

> But now...
> 
>   type ('a, 'b) t5 =
>       Empty_a5 of 'a option ref
>     | Empty_b5 of 'b option ref
>     | Full5 of 'a * 'b
> 
>   # let a5 = Empty_a5 (ref None);;
>   val a5 : ('_a, '_b) t5 = Empty_a5 {contents = None}
> 
> Stupid. Value a5 should be polymorphic in 'b!

The main role of a type system is not to be smart, just to be correct :-)
So the above sentence should use "could", not "should".
Let's just explain why you get this result.
The decision on how to generalize is made at the level of the let. 
If the right hand side contains mutable values creations and/or
function applications, the generalization is made in "safe" mode,
generalizing only covariant type variables in the result type.
This "safe" generalization is done without looking at the definition
itself, so it doesn't know what caused the switch to safe mode.

One can always imagine more clever approaches, like memorizing
variables that cannot be generalized just where the mutable value is
created, rather than decide on a whole-expression basis. In some cases
this would give better types. But this also adds complexity to the
type-checker, which still should be able to generalize this variable
if it is covariant in the final type.  And complexity can be the enemy
of correctness, so this is not done currently.

Do you have a concrete example where the above polymorphism is required,
and there is no workaround?
In general there is an (easy) workaround: separate definition of
mutable parts from immutable ones.

# let r = ref None;;
val r : '_a option ref = {contents = None}
# let a5' = Empty_a5 r;;
val a5' : ('_a, 'b) t5 = Empty_a5 {contents = None}

Jacques Garrigue