All I really need right now is a trivial subset of what's called ACU-unification, where ACU stands for "associative, commutative, unit". This arises from the fact that world labels are relatively first-class things, and type-checking for the elimination of a forall quantifier over worlds postpones the choice of world as an existential variable to be later unified:
Γ |- S : [X/w]A > C
------------------------------
Γ |- S : ∀w.A > C
so what I wind up with is some equations where both sides are lists (delimited by "world concatenation", an operator that's essentially linear logic's tensor) of existential variables and world parameters.
General ACU-unification talks about terms built out of other function symbols and stuff, and here I have only constants and the AC function symbol — so I figure it should be ultra-efficient to do it, but I don't yet know how to adapt the stuff that claims to be ultra-efficient in the general case. I do know a stupid way of reducing the problem to linear diophantine equations, but them's nasty.