(This issue is extracted from a suggestion by 'kantian' in this Discuss thread)

Consider the following example (OCaml 5.0):

type _ th =
  | Thunk : 'a * ('a -> 'b) -> 'b th

(* this works *)
let f (type a) : a th -> a = function
  | Thunk (type b) (x, f : b * (b -> _)) -> f x

(* this does not work *)
let f (type a) : a th -> a = function
  | Thunk (type b c) (x, f : b * (b -> c)) -> f x
(*                           ^^^^^^^^^^^^
This pattern matches values of type b * (b -> c)
but a pattern was expected which matches values of type b * (b -> a)
Type c is not compatible with type a
*)

I think that the second example should also work: users should be able to "name explicitly" all the variables that are local to the constructor declaration.

Things get even more confusing when the variable that we would want to name is not exactly one of the rigid type variables refined by the constructor, but only a part of it:

type _ tho =
  | Thunk_opt : 'b * ('b -> 'c option) -> 'c option tho

let f (type a) : a tho -> a = function
  | Thunk_opt (type b c) (x, f : b * (b -> c option)) -> f x
(*                               ^^^^^^^^^^^^^^^^^^^
This pattern matches values of type b * (b -> c option)
but a pattern was expected which matches values of type b * (b -> $0 option)
Type c is not compatible with type $0
*)

(The error message in this example is also very unclear. Explicit names in annotations are supposed to improve the clarify of error messages, but here they are making things worse)

Currently the "named existentials" features seems to only support "pure existentials" and nothing else. But we cannot really expect users to know the internal distinctions we make between the various kind of GADT variables, so this is probably very confusing to them. Could we support the examples above?

Note: see the current manual on named existentials:

Even in this example in the manual, I don't think it is clear to users that "all existential variables of the constructor" mean just ['a] and not ['a; 'b].

cc @garrigue