Note: when we discussed this during a meeting, I suggested that you and @lpw25 write a short document that would explain, with examples, the current need for (and uses of) the feature (including the examples from Oleg, and the "injectivity witnesses" that @lpw25 mentioned). I think this would be very useful to follow what's going on -- I understand the general feature and I think agree with @lpw25 it is simple and nice to expose it, but I haven't been able to follow the recent practical interest in it.

I think this means that #5985 can finally be closed.

What's the situation with GADTs? I haven't looked at the implementation, but gave the branch a quick try and was surprised to discover that injectivity annotations for some indexes are rejected:

# type (!_, !_) eql = Refl : ('a, 'a) eql;;
Line 1, characters 0-39:
1 | type (!_, !_) eql = Refl : ('a, 'a) eql;;
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In this definition, expected parameter variances are not satisfied.
       The 1st type parameter was expected to be injective invariant,
       but it is unrestricted.

@yallop There is no point in giving injectivity annotations for "nominal" (i.e. records and sums, including GADTs and extensible ones) types: their parameters are always injective by definition.

Understood. But since the annotations are correct, even if pointless, I think it's best to accept them when they're given.

In particular, I think this behaviour, where a variant definition matches an injective signature, but can't be marked as injective directly, is surprising:

# module M : sig type !_ t end = struct type _ t = X end;;
module M : sig type !_ t end

# module M : sig type !_ t end = struct type !_ t = X end;;
Line 1, characters 38-51:
1 | module M : sig type !_ t end = struct type !_ t = X end;;
                                          ^^^^^^^^^^^^^
Error: In this definition, expected parameter variances are not satisfied.
       The 1st type parameter was expected to be injective invariant,
       but it is unrestricted.

@yallop The last commit ignores injectivity annotations for nominal types, so this fixes your problem.

You can see the injectivity witnesses people use here:

https://ocaml.janestreet.com/ocaml-core/latest/doc/base/Base/Type_equal/module-type-Injective/index.html

I'm not sure whether any uses of it are in our open source code, but I think how you use it is fairly obvious. I'll try and dig up an example of why you might use it when I have some time.

This PR is now ready for reviewing.

It implements injectivity annotations on type parameters, using the suggested syntax !. Injectivity comes after variance, so one can write type +!'a t.

The main motivation is solving the famous #5985, explained in my OCaml 2013 paper. In particular, this allows to define GADTs where parametric abstract types appear as index. See the nominal types RFC or Oleg's recent mail on the caml-list for examples of this problem.

Injectivity annotations do not make sense for nominal types (records or sum types), since all their parameters are injective by definition. For them, annotations are silently ignored.

For type abbreviations (public or private), the injectivity of parameters can be inferred from the body of the type, and annotations are only checked.

For abstract types and private row types, injectivity annotations should be satisfied by the actual implementation. They are kept in the type definition, and checked through module subtyping. Note that for private row types, injectivity can also be inferred in some cases.

For concrete examples, see the file testsuite/tests/typing-misc/injectivity.ml.

The implementation has two parts.

• The first one, about injectivity of normal type parameters is only about adding syntax to express injectivity, and mapping it to the already existing injectivity bit of variances. There was almost nothing to change internally, since injectivity is already inferred. The main points are parsing (we allow both + ! and +!, without introducing a specific lexeme for +!), and printing (i.e. print injectivity annotations, but only where they are useful).
• The second part concerns the injectivity of constrained type parameters in type abbreviations. In order to integrate them smoothly, their injectivity is now inferred (this was not the case before, except when the parameter itself appeared in the type), i.e. such a parameter is deemed injective if it appears at an injective position in the body of the type, or if all its type variables are injective. As a result, one never needs to annotate explicitly a type abbreviation, so that injectivity annotations are only shown when printing abstract types and private row types.

@lpw25 Thank you, this is clear enough indeed.
I suppose everybody would be happy not to have to do this kind of gymnastic.
So adding injectivity annotations seems to be a reasonable first step, all the more as the compiler already tracks it.

This PR is a bit strange, as most of the effort seems to be going into constrained type parameters in type abbreviations, which is a very minor feature.
I have added a bit more code, to get maximal expressiveness: it is possible to write types in a way such that one can infer all the possible injectivity, even with constrained type parameters. On the other hand, writing it in a different way may lose injectivity, but does it really matter when those types a rare enough.

@yallop I wonder if you are satisfied with @garrigue's handling of your points, so that the PR can move further. (This said, it needs a full code review to move further, and I don't know who is volunteering for that, I'm currently not.)

@gasche: I'm happy with @garrigue's response and changes, so I've updated my review to "approve".

@garrigue this can be merged, but you need to fix conflicts first -- in the Changes, and in the generated parser.