I think this is the right approach and in the meantime you can put that extension code in your package as well to be able to continue your work without too much hassle. Yes this is type piracy, but you are aware of it and it only a temporary bandaid. The moment your PR is merged, you remove the type piracy from your package and everything is fine (and if the compat bounds are configured correctly even every valid combination of the two packages is fine).
I think “don’t do type piracy” is a bit too dogmatic. It should at least have an asteric saying “unless there is currently no other way and you are aware of the consequences” or so.