Finally implement the occurs check (and scope_level propagation)

* src/lexp.ml (ctx_length): Rename from scope_length.

* src/unification.ml (occurs_in): New function.
(_unify_metavar.unif): Use it to avoid circular types and
inconsistent generalization!