Allow existential types introduced in a constructor pattern to be bound without tuple type constraints patterns

[ebresafegaga]

Currently, if we have this:

module type Printable = sig
  type t
  val print : t -> unit
end

type printable = Printable : 'a * (module Printable with type t = 'a) -> printable

let print_list ps =
  ps
  |> List.iter (fun (Printable (type a) ((item : a), (module P))) -> P.print item)

We will get an error:

 Existential types introduced in a constructor pattern
   must be bound by a type constraint on the argument.

This is the only correct way:

let print_list ps =
  ps
  |> List.iter (fun (Printable (type a) ((item, (module P)) : a * _)) -> P.print item)

It would be nice if we could do this both ways.

[hyphenrf]

When I needed a locally abstract type like this, I found myself naturally reaching out for the ((a : t), b) syntax before the (a, b : t * _) one. +1 here.

[gasche]

Not really an answer to this issue, but it may help to consider the history of this fairly-recent feature, that prominently features syntax discussions. (Basically: this syntax is a bit annoying on users but also very predictable and simple to implement, so it managed to gather consensus when more convenient and complex proposals did not.)

• When GADTs were introduced in OCaml 4.00 (July 2012) there was no way to name existentials in patterns, and the error messages were rather bad. Pretty much from the start we discussed the fact that it would be nice to name existentials in patterns, but there was no clear syntax proposal.
  Strange type variable names in error messages (GADTs) #5780 (comment)
  This issue was eventually closed without allowing to provide explicit names for existentials in patterns, but with a better automatic naming scheme ($Foo_'a instead of ex#0, telling you which constructor bound the existential and what its name was in the type declaration).

• Naming existentials in pattern continued to be discussed in There is no easy way to give names to existential variables introduced by GADT pattern-matching #7074

• @garrigue proposed a first PR in 2020, Introduce local type variables in patterns #9579, but many people disliked the syntax and it did not fly. (let f = function <'a> Dyn (w,(x:'a)) -> ...)

• @garrigue proposed a second PR in 2020, Allow to name existentials in pattern-matching #9584, that eventually was merged and contains the current syntax. People mentioned again that relaxing the syntax to allow to annotate only some arguments would be nice.

• A variation Name existentials : new approach #10180 was briefly discussed where instead of (p, q, r : ty1 * ty2 * ty3), the annotation was of the form ((p : ty1), (q : ty2), (r : ty3)), but this one was dropped.

Some examples of syntaxes that have been considered in the process:

let f = function type b. D ((x:b), f) -> f x

function D (type a) (x, f) -> f x (* using definition order for existential variables *)

let f (type b) (D ((x: b), f)) = ...

fun (C : type a b. a * (a -> b list) -> t. (x, f)) -> ...
fun (C (type a b) ((x : a), (f : a -> b list))) -> ...

function 'a. C ((x : 'a), f) -> ...

function <'a> Dyn (w,(x:'a)) -> ...

function Dyn (type a) (w, x : a ty * a) -> ...
function Dyn (type a) ((w : a ty), (x : a)) ->

Generally:

• Suggestions to not require any annotation on the pattern arguments and use the type-declaration variable order to give meaning to the names have been abandoned.
• People recognized the lack of flexibility of the current syntax from the start, but no more flexible syntax gathered consensus.
• Currently only "toplevel" annotations are easy to implement; we currently require (type a) (w, x : a ty * a), we could instead allow (type a) ((w : a ty), (x : a)) for GADTs with two constructors, and we could even possibly allow say (type a) ((w : a ty), x) (making some toplevel annotation optionals), but we cannot allow (type a) (Some (x : a)), with an annotation in-depth in the pattern -- not without a significant change to the implementation strategy.
• Due to this "toplevel" restriction, there is a feeling that syntaxes that look like they allow for in-depth annotations are not great as they suggest something that the programmer cannot do -- they are not obviously restrictive, they are sneakily restrictive.

[github-actions]

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.

[Octachron]

I am moving this feature wish to a discussion, since this is not really planned (and as far as I remember possibly much harder to implement that it looks).