Re: [Caml-list] Why doesn't relaxed value restriction apply here?

[Romain Bardou <romain@bardou.fr>]

On 04/21/2018 11:04 AM, Jeremy Yallop wrote:
> On 21 April 2018 at 09:41, Romain Bardou <romain@bardou.fr> wrote:
>> According to the manual
>> (http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html) and to the
>> paper "Relaxing the Value Restriction"
>> (http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf),
>> the relaxed value restriction allows to generalize type variables which only
>> appear in covariant positions.
>>
>> The following code :
>>
>>      let f = let _ = ref 0 in fun f -> f []
>>
>> returns the following in the toplevel:
>>
>>      val f : ('_a list -> '_b) -> '_b = <fun>
>>
>> In this type, '_a only appears in covariant position. So, why is it not
>> generalized?
> 
> I think the current implementation only generalizes variables that
> only occur in *strictly* positive positions -- that is, that do not
> appear to the left of any arrow.  In your example, "'a" occurs in a
> positive position (to the left of an even number of arrows) that is
> not strictly positive (to the left of zero arrows).

Interesting. I wonder what the reason is behind this choice: is it about 
soundness, or about simplicity. Your example below seems to indicate 
that this is not about soundness as one can hide the depth of a type 
variable using an abstract type.

> This choice can lead to some slightly surprising situations, where
> exposing valid type equalities can cause previously-valid programs to
> be rejected.  For example, the following program, which is based on
> your example, is accepted:
> 
>     module M :
>     sig
>       type (+'a,'b) t
>       val g : unit -> ('a,'b) t
>     end =
>     struct
>       type (+'a,'b) t = ('a list -> 'b) -> 'b
>       let g () = let _ = ref 0 in fun f -> f []
>     end;;
> 
>     let f = M.g () in ((f : (int, unit) M.t), (f : (float, unit) M.t));;
> 
> but if the signature for 'M' is removed then the program is rejected.

That's very interesting actually.

Thanks a lot for your quick answer and your example :)

Cheers,

-- Romain Bardou