Function over GADT not "polymorphic enough"

type-system
gadt

#1

I’m trying to write a simple GADT-based evaluator for typed expressions, with the following expression variant:

type 'a expr =
  | Int  : int       -> int expr
  | Neg  : int expr  -> int expr
  | Bool : bool      -> bool expr
  | Not  : bool expr -> bool expr

I’d like to write a single eval : 'a expr -> 'a function that handles any expression type:

let rec eval (type a) (expr : a expr) : a =
  match expr with
  | Int n  -> n
  | Neg n  -> - eval n
  | Bool b -> b
  | Not b  -> not (eval b)
;;

This doesn’t compile, however. I get the following error (line 25 refers to the Not branch of the match):

File "main.ml", line 25, characters 24-25:
Error: This expression has type a expr but an expression was expected of type
         int expr
       Type a is not compatible with type int

Asking Merlin for the type of eval gives me int expr -> int, rather than 'a expr -> 'a, as I expected.

Is such an eval function even possible to write, or am I simply doing something wrong with type annotations or locally abstract types or something?

P.S. the following works fine, but is less satisfying:

let rec eval_bool (expr : bool expr) : bool =
  match expr with
  | Bool b -> b
  | Not b -> not (eval_bool b)
and eval_int (expr : int expr) : int =
  match expr with
  | Int n -> n
  | Neg n -> - eval_int n
;;

#2

I think you should use the syntax:

let rec eval : type a. a expr -> a = function
  | ...

as described in the manual


#3

Thanks, @zozozo. Looks like I missed that.