Given a type witness and the description view of the product type, how to convert from a list of index-free type witness to a product type description?

Here are the details. An indexed type witness is given by the GADT:

```
type _ ty = | Int : int ty
| Bool : bool ty
| List : 'a ty -> 'a list ty
```

Index-free type witness is given by the GADT:

```
type ty' = E : 'a ty -> ty'
```

And the type description view of product types is given by the GADT

```
type _ product = | Nil : unit product
| Cons : 'a ty * 'b product -> ('a * 'b) product
```

How to convert from the type `ty' list`

to the type `'b product`

? For example, the list:

```
[E Int ; E Bool ; E (List Int) ]
: ty' list
```

shall be converted to

```
Cons(Int, Cons(Bool, Cons(List Int, Nil)))
: (int * (bool * (int list * unit))) product
```

I wrote the first function

```
let of_list : 'b . ty' list -> 'b product =
function | [] -> Nil
| E h :: t -> Cons(h, of_list t)
```

and the second function

```
let of_list : type b . ty' list -> b product =
function | [] -> Nil
| E h :: t -> Cons(h, of_list t)
```

but in both cases there are type clashes at the return type.

I can see that in the first function `'b product`

is specialized to `unit product`

by the first branch of pattern matching, and it clashed with the inferred type `('a * 'b) product`

of `Cons(h, of_list t)`

in the second branch of pattern matching. In the second function I expect the type checker to learn the type equation `b = unit`

from the first branch of pattern matching but it doesnâ€™t.