# Binding existentials in a non-uniform GADT

**URL:** <https://discuss.ocaml.org/t/binding-existentials-in-a-non-uniform-gadt/14809>\
**Category:** Learning\
**Tags:** gadt\
**Created:** [June 18, 2024, 3:52am UTC](https://discuss.ocaml.org/t/binding-existentials-in-a-non-uniform-gadt/14809 "2024-06-18T03:52:51Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [June 18, 2024, 3:52am UTC](https://discuss.ocaml.org/t/binding-existentials-in-a-non-uniform-gadt/14809/1 "2024-06-18T03:52:52Z")

</div>

I learned recently that you can [explicitly name the existentials](https://ocaml.org/manual/5.2/gadts-tutorial.html#s:explicit-existential-name) when pattern-matching on a GADT. However, this doesn’t seem to work when the type parameters of the GADT are non-uniform:

```ocaml
type _ foo = Foo : 'a * 'b -> ('a * 'b) foo

let extract : type c. c foo -> c = function (Foo (type a b) (x, y : a * b)) -> (x, y);;

Error: This pattern matches values of type a * b
       but a pattern was expected which matches values of type $0 * $1
       Type a is not compatible with type $0

```

Is there a way to do this?

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [June 18, 2024, 8:38am UTC](https://discuss.ocaml.org/t/binding-existentials-in-a-non-uniform-gadt/14809/2 "2024-06-18T08:38:51Z")

</div>

This will be supported in [5.3](https://github.com/ocaml/ocaml/pull/12507) (if there are no complications). The reason why the feature has only been introduced in 5.3 is that the type variables `'a` and `'b` are not existentially quantified in

```ocaml
type _ foo = Foo : 'a * 'b -> ('a * 'b) foo

```

since they appear in the type of the variant. The recent PR is 5.3 acknowledge that it is nice to name all type variables introduced by matching other a GADT constructor and extend the support for

```ocaml
function (Foo (type a b) (x, y : a * b)) -> (x, y)

```

to all type variables introduced by the GADT equation.