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"