I don’t know if you read further in the Wikipedia article on Unification, but they have a section Order-sorted unification which looks a lot like your problem and links to Many-sorted logic.
However the reason I am noting this is that IIRC one of the proof systems has the concept of a sort built-in, but I can not find which one. I never really understood why they called the concept sort even though they explained it, but in reading about your problem it makes more sense.
Perhaps the examples in Many-sorted logic could serve as test cases.