If that's your definition, I believe no one actually follows that definition because there are a lot of ways for abstractions to leak their implementation detai

If that's your definition, I believe no one actually follows that definition because there are a lot of ways for abstractions to leak their implementation details, which might not be fully captured by interfaces. A good example is the performance. If you need a fast enough implementation with the same interface, you are not doing the abstraction in your definition because the "fast enough" implementation is an implicit coupling factor. More commonly, and in my opinion, more reasonably, any abstraction involves a trade-off. Some abstractions can be quite leaky but darn easy to use. Others may be less leaky but difficult to use (or misuse, depending on your view). There is no non-leaky abstraction here. Once you've chosen a trade-off and thus abstraction, you are still not entirely free from coupling for the aforementioned reason, but can enjoy some level of freedom thanks to the trade-off made. Unison is no different from other conventional languages in this sense.