Assertion in `register` always fails

[jstolarek]

When I uncomment assertion in register it causes every single example to fail:

let register state v =
  (* assert (U.rank v = no_rank); *)
  U.set_rank v state.young;
  register_at_rank state v

I remember commenting it temporarily because it tripped some examples. When did some turn into all?

[jstolarek]

Bisect says that an overwhelming majority of examples were broken by 806742e and all the remaining ones were broken by d769f02. Both are part of attempted hacky solution for #2.

[jstolarek]

List of examples that survived past 806742e and were only broken by d769f02: A1, A1∘, A2, A2∘, E3, bad5, bad6, inst_1, id_annot_1, id_annot_4, id_annot_5, mono_binder_constraint_1, mono_binder_constraint_2, id_annot_1.

[jstolarek]

d769f02 breaks behaviour of lift. In particular this definition of fresh:

let fresh t =
  match t with
  | None -> U.fresh t G.no_rank   false
  | _    -> U.fresh t G.signature false

will cause every variable created via lift (read: every function application) to be considered coming from a signature. Reverting.

[jstolarek]

The assertion needs to be extended to:

assert (U.rank v = no_rank || U.rank v = signature);

because we now also register variables from signatures. Not sure whether this will be the final design to deal with signatures but that's what the assertion needs to be for now.