[TYPES] breaking abstraction with ML exceptions

[Gabriel Scherer]

While I cannot comment on how often this occurs in practice, I'd like to
point out that this ability to hide equalities between exceptions has
delicate implications for the compilation of pattern-matching (in
exception-handling clauses, or when matching on exceptions as values¹), and
we (Luc Maranget, Thomas Refis and myself) somewhat recently found and
fixed bugs in the OCaml pattern-matching compilation coming from them. (The
bug went unreported for a long time, suggesting that indeed these cases do
not occur terribly often in practice.)

The problem is that it is wrong to assume that two constructors with
distinct names are distinct, because one may be redefined to be equal to
the other in a way that is not visible from your type environment (so a
canonicalization strategy does not suffice). Remark that if you decide to
conservatively assume that all constructors of exception type may be equal,
and  you use a classic "matrix-based" algorithm for pattern-matching, you
can end up with ill-typed columns of patterns (containing patterns of
incompatible types), coming from "potentially-equal" constructors of
different argument types, so your pattern-matching processing has to be
robust against this. (Two types may be equal for reasons unknown to the
current typing environment, but you should also be ready to deal with
incompatible head constructors or take steps to prevent that in the check
of whether two constructors are surely equal, surely distinct, or may be
equal.)

¹: OCaml 4.02 (August 2014) introduced extensible algebraic datatypes
(variants), contributed by Leo White, which generalize the extensible-type
model of exceptions to arbitrary datatypes (including GADTs). It is more
natural to match on the value on those than on exceptions.

On Wed, Mar 28, 2018 at 11:49 AM, Sam Lindley <Sam.Lindley at ed.ac.uk> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> The following SML program
>
>   exception C;
>
>   structure M :> sig exception A end =
>   struct
>     exception A = C
>   end;
>
>   (raise M.A) handle C => 42
>
> returns the value 42 (according to SML/NJ and, I believe, the 1997
> definition of Standard ML).
>
> The signature ascription appears to assert that exception A is abstract in
> M, and yet we are able to raise the exception M.A and catch it as C outside
> the scope of M. It makes no difference whether the signature ascription is
> transparent or opaque. The equivalent OCaml program yields the same result.
>
> Does this kind of code occur in practice?
>
> Sam
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>