In Eiffel, you are allowed to restrict the the food type of a cow to PlantFood by its redefinition feature. The language will take care of the rest to prevent some one from breaking through the type safety.
Elffel allows covariant redefinition, i.e., the type of an argument in a method interface in a subtype can be redefined into a subtype.
Eiffel uses system level type checking to prevent a cow to be fed with meat. System level type check requires all the exact type of a polymorphic variable should be figured out before the system can run. If we have code like:
animal: Animal;
...
animal.eat (meat);
The exact type of animal must be statically known by a data-flow analysis of the code between the variable declaration and the variable is used. If the variable is an input argument of a function, say:
foo (animal: Animal) is
do
animal.eat (meat);
end; foo
The compiler cannot find the type error until some body use it, say
foo (cow);
The error will be detected at link time.
We fall into the same trap as we did in C++. The interface foo tells you that the function can accept any subtype of animal. So you present a cow as an actual parameter. But the linker says that you cannot do this because the implementation of foo hidden in a black box cannot accept a cow. How do you feel?
If the function foo is presented in a distributed system as a remote service, system level check no longer works, because the actual parameter to animal is given at run-time.
Bertrand Meyer proposed a set of new Eiffel type rules in his keynote speech at OOPSLA'95. The purpose of the proposal is to eliminate the necessity of system-level type checking. By the new Eiffel rules, you can either covariantly redefine the method interface in a subclass, or use a polymorphic variable to call the method, but not both.
If you redefine the food type of a cow to plant food, then you cannot use a polymorphic variable to call the eat method, the code:
animal: Animal;
...
animal.eat (meat);
is then invalid.
On the other hand, if you used a polymorphic animal variable to call the eat method, then you cannot redefine the food type of a cow to plant food.
The rules are perhaps too pessimistic to make a covariant redefinition useful. If there is a need to redefine a method interface, the method in the superclass is usually used polymorphically.