如何用Menhir解析生成GADT表达式？OCaml编译报错求助

学习OCaml的GADT后，尝试基于《Real World OCaml》中的小型语言实现解释器，使用Menhir编写解析器。AST定义如下：

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;

词法分析器代码：

{
    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)}

编译时出现错误：

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

疑问：这是否和书中「GADT、局部抽象类型与多态递归」章节里将GADT当作普通变体时的错误一致？该如何修复？尝试了Menhir的--inspection flag但无效果。

这确实是同一类问题。Menhir默认会将expr非终结符的类型推断为单一具体类型，而你的GADT定义中expr是多态的（可以是int expr或bool expr等）。类型检查器会强制expr的所有分支返回同一类型，导致Value (Bool b)（返回bool expr）和其他分支（比如Plus返回int expr）类型冲突，从而报错。

需要明确告诉Menhir，expr非终结符是多态的，可以返回任意类型的'a expr。通过在解析器中使用局部抽象类型来标注expr的类型即可解决：

修改后的解析器代码：

%{
    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的多态性 *)
expr: 'a.
| 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)}

关键修改点：

• 在expr规则前添加'a.，表示该规则返回'a Ast.expr类型，且'a是局部抽象类型，允许每个分支返回不同的具体实例（比如int expr或bool expr）。
• 修复了小笔误：原解析器中EQ (x, y)对应AST中的Eq构造子（注意大小写）。

修改后重新编译解析器，错误会消失。可以测试以下输入：

• 1 + 2 会被解析为Plus (Value (Int 1), Value (Int 2))，求值结果为3。
• if 1 = 2 then true else false 会被解析为If (Eq (Value (Int 1), Value (Int 2)), Value (Bool true), Value (Bool false))，求值结果为false。

内容的提问来源于stack exchange，提问作者stormckey