Luca Cardelli introduced bounded universal quantification, which was later followed by many research works. Cook, Hill, and Canning suggested F-bounded polymorphism, in which inheritance is characterized as an operation on a recursive definition. With this operational definition of inheritance, subclasses inherited are not always subtypes. They are merely new types gotten by augmenting and modifying the parent type.
Kim Bruce followed this work by introducing a series of statically-typed functional languages TOOPL, TOOPLE, and PolyTOIL where type checking is decidable.
To put it simple, the inherited types are not subtypes of their parent if there is a covariant redefinition of the method interface in the inherited type. Therefore, Cow is not a subtype of Animal if Cow redefines its food type to plant food. If we have a polymorphic variable:
Assigning a Cow instance to the variable is then invalid.
Though using a notion of matching, which is weaker than subtyping, allows more polymorphism in the presence of self type (the type of the enclosing object), the flexibility achieved seems very limited. Self type is only a specific case that deals with an argument of the same type as the type of the enclosing object. In most cases, we have to deal with types other than self type. The food type in an animal class is an example.
If a cow cannot be an animal only because it does not eat all kinds of food, what can be animals then?