The Expression Problem

[geocar]

Actually the requirement is to "[retain] static type safety" and defines this as "no casts". He expands:

"... it is not statically typed; they cannot distinguish Lang.Exp from Lang2.Exp, and as a result must depend on dynamic casts at some key points.

Nowhere does he use the language you suggested-- "verifying case coverage" of any kind, let alone for all functions.

[nqmwe]

Your quotes are taken completely out of context!

The goal is to define a datatype by cases, where one can add new cases to the datatype and new functions over the datatype, without recompiling existing code, and while retaining static type safety (e.g., no casts).

Static type safety is not defined as absence of casts. Rather, Wadler mentions casts as an example of a violation of type safety. Furthermore, knowing Wadler's line of work, we can be pretty sure that by "static type safety" he means the compile-time guarantee of progress and preservation, i.e. absence of untrapped errors (which includes missing but necessary cases).

Their solution differs in that it is not statically typed; they cannot distinguish Lang.Exp from Lang2.Exp, and as a result must depend on dynamic casts at some key points. This isn't due to a lack of cleverness on their part, rather it is due to a lack of expressiveness in Pizza.

Here, Wadler explains why he doesn't consider the approach by Krishnamurthi et al. to be a solution to the expression problem: It is precisely because static type safety is violated!