I have another challenge for you. Without the redundant annotations (i.e. with only an annotation on let-rec) it type-checks nicely. I am providing more annotations as an option.

>>>

type _ term =

  | Lit : integer -> integer term

  | Plus : integer term * integer term -> integer term

  | IsZero : integer term -> boolean term

  | If : (*∀'a.*)boolean term * 'a term * 'a term -> 'a term

  | Pair : (*∀'a, 'b.*)'a term * 'b term -> (('a * 'b)) term

  | Fst : (*∀'a, 'b.*)(('a * 'b)) term -> 'a term

  | Snd : (*∀'a, 'b.*)(('a * 'b)) term -> 'b term

and integer

and boolean

  

external plus : (integer -> integer -> integer) = "plus"

external is_zero : (integer -> boolean) = "is_zero"

external if_then : (boolean -> 'a -> 'a -> 'a) = "if_then"

let rec eval : type a . (a term -> a) =

  ((function Lit i -> i | IsZero x -> is_zero (eval x)

    | Plus (x, y) -> plus (eval x) (eval y)

    | If (b, t, e) -> if_then (eval b) (eval t) (eval e)

    | Pair (x, y) -> (eval x, eval y)

    | Fst p -> let ((x, y): (a * 't47)) = eval p in x

    | Snd p -> let ((x, y): ('t59 * a)) = eval p in y): a term -> a)

<<<

We get at "eval p" to the right of "let ((x, y): (a * 't47))":

Error: This expression has type a * b#0

       but an expression was expected of type a * b#0

       The type constructor b#0 would escape its scope