Let's be clear, I am not arguing for subtypes. Subtypes are a mess, that is why no type system supports them. I am arguing against any types at all. So type inference being harder is not a problem, because there won't be any type inference. I know, that is a tough pill to swallow, type inference is like a hard drug for computer scientists.

Subsets or subcollections, on the other hand, are fine. Of course you will have proof obligations, but that is not a problem, and automation can take care of most of this (note that automation is much more flexibel than hardcoded type inference).