Downcast, or type refinement, is the assignment of an object reference to a subtype (more restricted) entity reference.
In Eiffel we can do that either with the (now obsolete) reverse assignment attempt, or with an object test expression.
The external dispatch mechanism provides another alternative. In fact, a possible may of looking at it, is that it is a static safe mechanism to "downcast" the dispatch tuple object(s) to Current alike attributes in external classes. In each of those classes there will exist downcasted safe non-Void references to those objects. The compiler is able to statically ensure a successful downcast (to whatever effective external dispatch classes defined). Thus, no exception will ever arise from an unsuccessful downcast.
Note: This downcast operation is not local (as the existing ones), but externalized to external dispatch classes.
External dispatch solution:
(Source code) (Compiled Eiffel code)
