Comment author: @Drup

Additional note: if I annotate this type to be covariant, it generalizes properly, but since my real type is not covariant, that doesn't help me much.

Comment author: @Drup

Is it related to #5985 and the need for injectivity annotation ?

Comment author: @gasche

This is the value restriction. Covariance works because of the relaxed value restriction. For reference, see
Relaxing the value restriction
Jacques Garrigue
2004
http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf

(This is not related to injectivity.)

There is no general solution to this problem, except an effect system that can guarantee that some functions are pure (and doing that in a usable way is a research problem).

Comment author: @lpw25

There is no general solution to this problem, except an effect system that can guarantee that some functions are pure (and doing that in a usable way is a research problem).

I think higher-rank types would also solve it in this case:

let add (x : 'a. 'a t) : 'b. 'b t = Add x
(* val add : 'a. 'a t -> 'b. 'b t *)

Of course then add will only work with an argument that is also generalised.

Comment author: @xavierleroy

"Real World OCaml" contains a tutorial on the value restriction and why it is there in the first place:
https://realworldocaml.org/v1/en/html/imperative-programming-1.html#side-effects-and-weak-polymorphism
A good read before delving in Garrigue's 2004 paper.

Comment author: @Drup

@gasche: I know about the value restriction and the relaxation with covariance, but it's not helping, since my type is not covariant, but I still would like to instruct the type system that it can generalize.

If it's really unsound to generalize in this case, why ?

As you said in #6653:

• you desire covariance because of the relaxed value restriction, but the types you want to express are fundamentally not covariant (and you should instead long for ways to mark terms as non-expansive to allow generalization in absence of covariance

Comment author: @gasche

It is unsound to generalize expressions which may allocate and share fresh mutable memory. The value restriction approximates "safe" terms by the set of values (which do not compute and thus do not allocate), and everything that is not syntactically value-like is considered unsafe and not generalized.

In "this case" it's of course sound to generalize, as inlining the Add function immediately shows. The problem is that this is not a general criterion as inlining is anti-modular and opens a can of worm of never-ending non-trivial refinements. The proper solution is effect-typing, which gives a modular interface to the "safe to generalize" idea.

I think the history of the value restriction is very well explained in the first two sections of Jacques' article. (In particular, Leo's suggestion to use rank-1 polymorphism is mentioned page 3.)