Type inference and abstraction for HLF seems to work on the entire set of examples from linear cut elimination and the substructural nominal business that I have coded up so far! This is pretty exciting, as it was a very close call for a while whether the unification problems arising from some of the commutative cases of cut elimination were even solvable in principle.