If we generalize on varible-by-variable basis, then the following
letrecs are not the same:

  let rec f (x:'a) y = (x = y) and g (z:int) = f z z  // typechecks
  let rec g (z:int) = f z z and f (x:'a) y = (x = y)  // does not

In the first case, we unify the type of y with 'a, and thus
f is fully generalized in the definition of g. In the second
case, we unify the non-generazled second argument of f with int,
and the definition of f does not typecheck.

Also: accept implicit type variables in programs.