Hello

I'm trying to learn a bit about GADTs, but I can't figure out how to
make them work with Menhir.

I have defined the following GADT:

(* foo.ml *)

type 'a t =
  | Int : int -> int t
  | Bool : bool -> bool t

With this definition I can write an "eval" function as

let eval (type t) (foo : t Foo.t) : t =
  match foo with
  | Foo.Int i -> i
  | Foo.Bool b -> b

Now considering the simple parser and lexer below,

(* parser.mly *)

%{ open Foo %}

%token <int> INTEGER
%token <bool> BOOL
%token EOF

%start <'a Foo.t> start
%%

start:
  | value; EOF { $1 }
  ;
value:
  | i = INTEGER  { Int i }
  | b = BOOL     { Bool b }
  ;

(* lexer.mll *)

{ open Parser }

let digit = ['0'-'9']
let boolean = "true" | "false"

rule token = parse
  | [' ' '\t']             { token lexbuf }
  | '\n'                   { Lexing.new_line lexbuf; token lexbuf }
  | digit+ as i            { INTEGER (int_of_string i) }
  | boolean as b           { BOOL (bool_of_string b) }
  | eof                    { EOF }

when I try to compile this I get the error below:

File "parser.mly", line 15, characters 43-52:
Error: This expression has type int Foo.t
       but an expression was expected of type bool Foo.t
       Type int is not compatible with type bool

This is the

  | b = BOOL     { Bool b }

line. I believe the error comes from not having the locally-abstract
type annotations in the code generated by Menhir.

Is there any way around this?

Thanks in advance,
Andre