Not independently invented again. Lionel is fully aware of the level tracking in the OCaml type-checker; in fact the OP is cited in the Simple-sub paper (section 3.5.1, page 15).