[contravariant]

I'm somewhat curious why you'd want both (2) and (3) to hold. Isn't it somewhat contradictory to want types to not just merely denote the structure, while requiring that everything with the same structure satisfies the type?

Maybe it's because I'm influenced by C# but viewed from that perspective it would be like requiring you to explicitly declare that e.g. some value is a ProductID but when you're declaring a type you wouldn't need to declare it is a Person, provided it simply implements the right fields (in C# you would have to explicitly implementing some interface to clarify that first-name and last-name do indeed refer to a person and not, for example, the head and tail of a list of names). This does mean that any external code can't implement your interfaces though, which is a bit annoying, though fixable.

[jdmichal]

That's commonly called "duck-typing". And since you're discussing C#, I'll throw in that Typescript (another MS language) has duck-typing for interfaces. You can explicitly implement an interface, in which case the compiler will enforce that the interface is implemented. But you can also implicitly meet an interface.