This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Still worth considering.
Note that nominal types are contractive, so adding them would already be an improvement.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

I am trying to write a library that would benefit from this feature! Is there anything serious that would be blocking a merge of this feature if implemented?

A first step would be to agree on the syntax. My proposal type 'a t : contractive above is not necessarily a good choice, because:

• it looks very different from existing variance-style annotation syntaxes, and
• it does not clearly extend to multi-parameter types (for example type ('a, 'b) t = 'a is contractive in 'b but not in 'a).

It may be a matter of agreeing on a weird new symbol to add to variance-like markers +, -, ! to indicate contractiveness.

Then you have to implement it. I expect that this will be difficult, but easier than agreeing on the syntax :-)

From what I understand, adding the annotation to the type declaration in the module is the only place it's appropriate, so it probably doesn't belong with the variance annotations. Maybe something like type 'a t : contractive 'a? Seems like a good enough choice to prototype with

I'm not sure I follow. My idea is to add this on type declarations (and optionally on type definitions but there it can be inferred), in particular on type declarations in the argument of a functor, and to be able to annotate each parameter. For example the following should work, assuming I use # for contractibility:

module F(X: sig type (#'a, 'b) t end) = struct type u = (u, unit) X.t end

module M = struct type ('a, 'b) = 'b end
module N = F(M)

This seems similar to variance to me:

module F(X: sig type (+'a, -'b) t end) = struct type +'a u = ('a * 'a, 'a -> unit) X.t end

module M = struct type ('a, 'b) t = 'b -> 'a end
module N = F(M)