Hi everyone,

I’ve started making use of GADT in my code and I’ve been loving the elegance of it so far. I understand that a typical use case of GADTs is when you’ve got a parameterized type `'a t`

and want the output type of a function to depend on parameter `'a`

, while providing different implementations for different values of `'a`

using polymorphism.

I had no problem building functions whose signatures looked like `type a. a t -> a`

, but now I’d like to do something a little different. My GADT `_ t`

has several constructors :

```
type x
type y
type z
type _ t =
| X : x -> x t
| Y : y -> y t
| Z : z -> z t
```

For some reasons, the function I’d like to write would return a `y t`

when passed a `x t`

as an argument, and would return a `z t`

when passed a `y t`

.

```
let f : type a. a t -> (* what should I write here ? *) = function
| X _ as x -> y_of_x x (* output of type y t *)
| Y _ as y -> z_of_y y (* output of type z t *)
| Z _ -> raise InvalidArgument
```

Having such a function seems doable in theory (static typability could be achieved just by examining the constructors), but I can’t get to express its type right. OCaml seems to only allow the output type to depend on the local type that is provided by the input GADT parameter.

Does OCaml provide a proper way to achieve this or is it not currently possible ?

I’ve found a clumsy workaround using polymorphic variants, but I dislike the facts that they require the variables to be `match`

ed upon to know of which type they actually are, which is not necessary in my case : if `var`

is of type `x t`

, the compiler can be sure that `f var`

is of type `y t`

.

Thanks in advance for your answers or advices