Re: [Caml-list] typechecking

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

On 2014/03/23 13:41, oleg@okmij.org wrote:

> The complete solution is to update the function
>        generalize_expansive in typing/ctype.ml
> which is responsible for implementing the relaxed value restriction.
> The type 'a should not be considered co-variant in 'a. Alas, such a
> modification is a bit cumbersome since generalize_expansive is called
> recursively. One have to split cases. It is not clear how much benefit
> can be gained -- complicating type checker for the sake of a rare
> error.

I don't think it would make sense anyway.
I suppose your rationale is that since 'a is empty in the sound part
of the language, if you actually get a value of this type it must be
unsound, and should not be generalized.
However, this would just be a hack, and would not catch all such
errors. For instance 'a list contains the empty list, so we have no reason
not to generalize it, but an unsound function might still return a
non empty list with this type.
Moreover, there are also useful applications of the generalization of 'a.
For instance, the following idiom allows you to give an arbitrary polymorphic
type to a non-value, which you cannot under the strict value restriction.

	let y = Obj.magic (f x)
	let z : ('a -> 'a) t = y

So well, unsound functions are unsound, and you have to live with that.
In particular _always_ annotate with ground types.

Jacques Garrigue