How to use menhir to parse into a GADT expression?

I have just learned something about GADT in OCaml through Real World OCaml, and want to try to transfer the first little language there into a interpreter, thus using menhir.

The ast definition is totally the same as the example.Here is it:

type _ value =
  | Int : int -> int value
  | Bool : bool -> bool value

type _ expr = 
  | Value: 'a value -> 'a expr
  | Eq : int expr * int expr -> bool expr
  | Plus : int expr * int expr -> int expr
  | If : bool expr * 'a expr * 'a expr -> 'a expr
  

let eval_value : type a. a value -> a = function
  | Int x -> x
  | Bool x -> x ;;
  
let rec eval: type a. a expr -> a = function
  | Value v -> eval_value v
  | If (c, t, e) -> if eval c then eval t else eval e
  | Eq (x, y) -> eval x = eval y
  | Plus (x, y) -> eval x + eval y;

And here is my lexer and parser specification

{
    open Parser
    exception Error of string
}

rule token = parse
| [' ' '\t'] {token lexbuf}
| '\n' {Lexing.new_line lexbuf; token lexbuf}
| "if" {IF}
| "then" {THEN}
| "else" {ELSE}
| '=' {EQ}
| '+' {PLUS}
| "true" {BOOL (true)}
| "FALSE" {BOOL (false)}
| ['0'-'9']+ as i {NUM (int_of_string i)}
| '-'['0'-'9']+ as i { NUM (int_of_string i) }
| eof {EOF}
| _ { raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }

%{
    open Ast
%}

%token <int> NUM
%token <bool> BOOL
%token PLUS
%token IF
%token THEN
%token ELSE
%token EQ
%token EOF

%left PLUS

%start <'a Ast.expr> expr_toplevel

%%

expr_toplevel:
| e = expr EOF {e}

expr:
| x = expr PLUS y = expr {Plus (x, y)} 
| IF c = expr THEN x = expr ELSE y = expr {If (c, x, y)}
| x = expr EQ y = expr {EQ (x, y)}
| b = BOOL {Value (Bool b)}
| n = NUM {Value (Int n)}

That's all, and the code above failed to build, the error it got is:

File "bin/parser.mly", line 27, characters 18-26:
Error: This expression has type bool value
       but an expression was expected of type int value
       Type bool is not compatible with type int

which is referring to

| b = BOOL {Value (Bool b)}

This error is totally the same as the one we get in the first code block in Chapter GADT, Locally Abstract Types, and Polymorphic Recursion in Real World OCaml, where the author try to treat GADT as ordinary variance. Is this the same problem here? If yes, how could I fix this to make it work.

There is nothing much about GADT in menhir manual. It is mentioned in a flag named --inspection. I have tried that and nothing changes.

Solution

The root issue is that you are trying to write a function of type

val parse: (x:string) -> f(x) Ast.expr

where the type of the parsed ast depends on the value of the input. This is only possible in dependently typed language, and OCaml is not dependently typed.

One solution to make it work is to make the parser return a type that represents any Ast.expr, which can be defined with an existential quantification:

type any_expr = Any: 'a Ast.expr -> any_expr [@@unboxed]

Then the expr parsing function will have the type:

val parse: string -> any_expr

and it is still possible to have subparsers that returns a specific type of expr.