[Caml-list] Type inference curiosity

[Grumpy <grumpy@drno.eu>]

Hello,

I think there is an incoherency or a bug somewhere in the type inference
engine with the following code with version 4.02.3 (I have not tested in
previous versions). Both functions eval and eval2 are identical but the
inferred types are different, and the type inferred for eval2 is
actually wrong.

The function eval is typed correcly ('a exp -> 'a) while the type
inferred for funcion function eval2 is (int exp -> int), which is wrong
because of the Inc case returning ('a exp -> 'a).

It seems the syntax (type a) leads to this incorrect behaviour...


type _ exp =
  | Stop : int exp
  | Inc : (int exp -> int) exp

let rec eval : type a. a exp -> a = function
  | Stop -> 0
  | Inc -> (fun (p : int exp) -> 1 + eval p)

let rec eval2 (type a) (p : a exp) : a =
  match p with
  | Stop -> 0
  | Inc -> (fun (p : int exp) -> 1 + eval2 p)