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

[Jeremy Yallop <yallop@gmail.com>]

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).

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.

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs