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