Binding existentials in a non-uniform GADT

Learning
1

I learned recently that you can explicitly name the existentials when pattern-matching on a GADT. However, this doesn’t seem to work when the type parameters of the GADT are non-uniform:

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?

2

This will be supported in 5.3 (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

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

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

to all type variables introduced by the GADT equation.

1 Like