[Caml-list] Mixing two GADTs

["David Allsopp" <dra-news@metastack.com>]

Suppose I have the following two GADTs:

type _ foo = A : int foo
           | B : string foo
           | C : bool foo

type _ bar = X : int bar
           | Y : float bar
           | Z : string bar

In my actual use case, these two GADTs cannot be altered. Suppose I then
define the following two functions:

let g : type s . s bar -> s = function
  X -> 42
| Y -> 42.0
| Z -> "42"

let get1 : type s . s foo -> s = function
  A -> int_of_string (g Z)
| B -> string_of_float (g Y)
| C -> (=) 1 (g X)

So far, so good. Now what I'd like to try to do is alter get1 to be of the
form:

let get2 : type s . s foo -> s = fun attr ->
  let (f, retr) =
    match attr with
      A -> (int_of_string, Z)
    | B -> (string_of_float, Y)
    | C -> ((=) 1, X)
  in
    f (g retr)

Obviously, I need type annotations for f and retr. I'd tried:

let get2 : type s . s foo -> s = fun attr ->
  let x : type t . (t -> s) * t bar =
    match attr with
      A -> (int_of_string, Z)
    | B -> (string_of_float, Y)
    | C -> ((=) 1, X)
  in
    let (f, retr) = x
    in
      f (g retr)

But I get an error with int_of_string being of type string -> int instead of
type t -> s.

(Incidentally, the notation I expected to be able to use of [(let ((f, retr)
: type t . (t -> s) * t bar)] resulted in a syntax error although looking at
7.13 in the manual, I think that's probably correct?)

Is there a type annotation which will allow this to work? Any help (or a
statement that this happens to be impossible!) much appreciated...


David