Add some injectivity annotations to the standard library.

[yallop]

This is a follow-up to @garrigue's #9500, which added support for injectivity annotations to the language. This PR adds injectivity annotations to abstract types in the standard library.

Before this PR, user code could not make use of the fact that most¹ standard library abstract types are injective:

# type !'a t = 'a Map.Make(Int).t -> int;;
Line 1, characters 0-38:
1 | type !'a t = 'a Map.Make(Int).t -> int;;
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In this definition, expected parameter variances are not satisfied.
       The 1st type parameter was expected to be injective invariant,
       but it is contravariant.

After this PR the code above passes typechecking:

# type !'a t = 'a Map.Make(Int).t -> int;;
type 'a t = 'a Map.Make(Int).t -> int

---

¹ Ephemeron.K1.t is an exception

[nojb]

I'm not yet very familiar with the concept of injectivity and did not follow #9500, but I tried reviewing this one as it seemed rather trivial. For my own understanding, do the following hold?

• Is it the case that when we add an injectivity annotation to the interface of a module only, the compiler checks in the implementation that the type is actually injective?

• If the above holds, then for those types which are defined by sums or records in the implementation an injectivity annotation is not needed in the implementation (or in any case, it is ignored)

• For types which are defined as abstract in the implementation (eg Genarray.t), the annotation needs to be put in both interface and implementation sides. Is it right to say that an annotation in this case can never be "wrong", ie that such an abstract type can never be "not injective"?

[garrigue]

@nojb:
The answer to all those questions is positive.
The type checker already ensures that all injectivity annotations in interfaces are correct, and adding an injectivity annotation to a purely abstract is sound too (there is no way to build an incoherent equation).

The only way to obtain a contradiction using injectivity is to intentionally build a wrong equality witness, using Obj.magic. Note that you can also use this technique to prove bool = float, so there is nothing new there, just never use Obj.magic when building a GADT.

type (_,_) eq = Refl : ('a,'a) eq
type !'a t
let w0 : (bool, float) eq = Obj.magic Refl
let w : (bool t, float t) eq = Obj.magic Refl
let w' : (bool, float) eq = (fun (type a b) (Refl : (a t, b t) eq) -> (Refl : (a, b) eq)) w

[garrigue]

By the way, it would be in theory sound to have purely abstract types (i.e. abstract types defined in implementations) be always injective. However, this would change the inferred types.
Currently, in the absence of injectivity annotation they only behave invectively inside the current module.

[nojb]

Thanks for the explanation @garrigue, that clears it up for me.

[nojb]

LGTM. For those wondering, the injectivity of 'a Lazy.t seems to be deduced automatically from that of the built-in type 'a lazy_t and does not require an annotation.

[nojb]

Looks good to go. As this touches the stdlib, let's wait a bit in case someone wants to comment further. Otherwise I'll merge by end of day today or tomorrow morning at most.

[nojb]

Merged, thanks!