Lets say I have some GADT
type _ t = | Str : string t | Int : int t
and I want to write a function that takes some identifier (we’ll use an
int) and returns a corresponding value of
let f = function | 0 -> Some Str | 1 -> Some Int | _ -> None
The above function doesn’t compile for obvious reasons; the first branch concretizes the return type as
string t. Fair enough, but using locally abstract types doesn’t work either:
let f (type a) : int -> a t option = function ...
This time the compiler complains that
int are not equal to
type a, which also makes sense.
This also doesn’t work with explicit polymorphism. The one case that I’ve found does work is when using first class modules:
module type Flat_t = sig type arg val v : arg t end let f = function | 0 -> Some (module struct type t = string let v = Str end) ...
This seems redundant to me as no extra information is added in the module.
I understand why this is the case – I’m just wondering if there’s a more elegant solution to this that doesn’t require the extra indirection of wrapping the values with modules.