Type of function returning GADT

Learning
#1

I am attempting to serialize and deserialize a GADT, however, the problem is, I cannot make the type system understand that my deserializer function will return a general GADT.

If the GADT is

type 'a t =
  | A : a t
  | B : b t

I need a way of expressing that my deserializer function will return any t depending on the case it falls in

This is all I have tried:

In these cases it complains that the GADT type is inferred as a t however I am also returning b t in some cases

let f : ... -> _ t =
  | ... -> A
  | ... -> B

let f : ... -> 'a t =
  | ... -> A
  | ... -> B

let f : 'a. ... -> 'a t =
  | ... -> A
  | ... -> B

In these cases it complains that it expects any t however I provide it with a t

let f : type any. ... -> any t =
  | ... -> A
  | ... -> B

let f (type any) ... : any t =
  | ... -> A
  | ... -> B

I am quite inexperienced with GADTs, and was wondering whether there is a way to express I am returning a GADT of an unknown type yet. Or maybe Iā€™m not understanding how GADTs work.

#2

When you write f (type any) ... : any t this means "I can produce a t at every type any", but what you want is "there exists some type any for which I can produce a t".

You need to use an auxiliary GADT to have existential types:

type any_t = AnyT : 'any t -> any_t

let f : _ -> any_t = 
  | ... -> AnyT A
  | ... -> AnyT B
2 Likes
#3

"there exists some type any for which I can produce a t "

Yes, indeed, this is what I wanted, thanks for the help!