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.