Discusion on the CATcall proposal

In Object-Oriented Software Construction (second edition), B. Meyer proposed a "drastic" solution to the type violation risk well know by Eiffel programmers that slot (1,3) shows.
 
Table 7 : Eiffel
u
d
ud
cv(Top) Up Compilation error Down
cv(Middle) Up Down Down
cv(Bottom) Up Down Down
ctv(Top) Compilation error Compilation error Compilation error
ctv(Middle) Compilation error Compilation error Compilation error
ctv(Bottom) Up Up Up

This solution is called CATcall type rule. It says (p 637) "Polymorphic catcalls are invalid."

Polymorphic call is defined (p 638) by a call whose target is a polymorphic entity.

A polymorphic entity is (p 637) defined by: "An entity x of reference (non-expended) type is polymorphic if it satisfies any of the following properties:
    P1 . It appears in an assignment x:= y where y is of different type or (recusrsively) polymorphic.
    P2 . It appears in a creation instruction ! OTHER_TYPE ! x where OTHER_TYPE is not of the type declared for x.
    P3 . It is a formal routine argument.
    P4 . It is an external function."

In our testing procedure u and d are not polymorphic, but ud is polymorphic (applying P1 or P2) and could execute 6 polymorphic calls, column 3.

Then the CAT (Changing Availability or Type) is defined (p 638) by "A routine is a CAT if some redefinition changes its export status or the type of any of its arguments".

In our testing procedure both cv and ctv are CAT since they change the type of the single argument. ctv is forbidden because no contravariant redefinition is allowed in Eiffel. So cv is  the only accepted CAT. Remain slots (1,3) ; (2,3) ; (3,3).

The definition of a Catcall (p 638) is "A call is a catcall if some redefinition of the routine would make it invalid because of a change of export status or argument type."

This definition is ambiguous. Should we understand slot (1,3) is forbidden, or slots (1,3) ; (2,3) and (3,3) are forbidden, since only slot (1,3) is error prone ?

The final example of p 638 precises things saying "since share redefines its arguments covariantly,(...) and [calls] are polymorphic, they are prime examples of polymorphic catcalls and hence made invalid by the Catcall type rule."

Hence, if I correctly interpret definitions, next Eiffel Table would be (CATcall is not yet implemented):
 
Table 7 bis : Eiffel with CATcalls (hard interretation)
u
d
ud
cv(Top) Up Compilation error Compilation error (CATcall rule)
cv(Middle) Up Down Compilation error (CATcall rule)
cv(Bottom) Up Down Compilation error (CATcall rule)
ctv(Top) Compilation error Compilation error Compilation error
ctv(Middle) Compilation error Compilation error Compilation error
ctv(Bottom) Up Up Up

If my interpretation is too strong, it would be  (CATcall is not yet implemented):
 
Table 7 ter : Eiffel with CATcalls (soft interpretation)
u
d
ud
cv(Top) Up Compilation error Compilation error (CATcall rule)
cv(Middle) Up Down Down
cv(Bottom) Up Down Down
ctv(Top) Compilation error Compilation error Compilation error
ctv(Middle) Compilation error Compilation error Compilation error
ctv(Bottom) Up Up Up

This proposal removes the runtime error risk but introduces new constraints...

I argue that proposed tables are tools that can be used to better understand OO design decisions.