Jacques Garrigue

Thanks for putting back the feedback here. A short answer, because I'm on holidays. * I have got feedback from Nomadic labs, confirming that the inability to distinguish (non-external) abstract...

Concerning the syntax, my feeling is that the attribute syntax is closer to what we need here, as this information strengthens the type checker, but does not change the semantics...

Sorry, going to Japan and back and all that delayed me a lot. I thought a bit about one of the main applications, which is allowing to define witnesses for...

Here is another version using Oleg's workaround of reifying the equation. I think this is weaker, but I must look for another example. ```ocaml type (_,_) eq = Refl :...

Following @gasche 's suggestion, I'm going to use `!` for injective type parameters, in an independent prototype. Except if @Drup has a problem with this...

[PR#9500](https://github.com/ocaml/ocaml/pull/9500) proposes an alternative solution to this RFC, through injectivity annotations on type parameters. Its implementation is simpler, and it is finer grain, but this does not allow to distinguish...

Thank you for your feedback. This is indeed the alternative approach I had in mind. I am a bit concerned that providing each feature independently would be both painful to...

> @garrigue, @trefis, do you have some idea of what "global opening of GADTs" would entail? Sorry for the very slow answer. In theory there is nothing wrong with global...

Actually, this is the other way round: this PR tracks the part or purity relevant to polymorphism, in order to get more polymorphism. The types are unchanged. Purity is a...

Planned extensions after discussion with @diremy : * allow purity annotations for recursive polymorphism and polymorphic record fields * maybe also for polymorphic methods * there should be a way...