Why does relaxed value restriction treat function types differently?

Learning
1

Hello everyone! I find it kind of confusing when playing with relaxed value restriction. Given the following code:

type (+'a, -'b, +'c) t = ('a -> 'b) -> 'c
let f1 = (fun () () -> (assert false : _ t)) ()
(* val f1 : unit -> ('_weak1, '_weak2, 'a) t = <fun> *)

Even though f1 is not a syntactic value, relaxed value restriction generalized the third covariant type variable. The first type variable, covariant though, cannot be generalized, otherwise the following function

let f1' : unit -> _ t = (fun () -> let r = ref None in fun () f -> r := Some f) ()
(* val f1' : unit -> ('_weak3, '_weak4, unit) t = <fun> *)

would be unsound.

However, if we use ADT or abstract type instead of type alias:

type (+'a,-'b,+'c) u = A of (('a -> 'b) -> 'c)
module M : sig
  type (+'a,-'b,+'c) v
end = struct
  type (+'a,-'b,+'c) v = ('a -> 'b) -> 'c
end
open M
let f2 = (fun () () -> (assert false : _ u)) ()
(* val f2 : unit -> ('a, '_weak5, 'b) u = <fun> *)
let f3 = (fun () () -> (assert false : _ v)) ()
(* val f3 : unit -> ('a, '_weak6, 'b) M.v = <fun> *)

Now the first type variable is generalized. What’s happening?

2

I think that the issue is that type variables in contravariant positions are not generalized under (the OCaml implementation of) the relaxed value restriction, so that a binding like this

let f = (fun _ _ -> ()) ()

is given a weak type _'a -> unit. If type variables in positive-but-not-strictly-positive positions were generalized then f could also be given a generalized type such as ('b -> unit) -> unit, which would violate principality.

3

Thanks! I spent some time reading the paper, and was surprised that my question was already answered in it:

We deem dangerous all occurrences appearing in a contravariant branch of a type. While this is not necessary to ensure type soundness, we need it to keep principality of type inference.

Datatype definitions being generative, they are not expanded during type inference, and all covariant variables can be considered as safe.

Also, it seems that I made a mistake in the example I gave. I said that if all covariant variables were generalized, the function

let f1' : unit -> _ t = (fun () -> let r = ref None in fun () f -> r := Some f) ()
(* val f1' : unit -> ('_weak3, '_weak4, unit) t = <fun> *)

would be unsound. However, even though r could save functions of different input types, they are not actually invoked so no runtime error happens.