Jacques Garrigue wrote:
> If we limit ourselves to the case where both [x] and [y] contrain no
> type variables, this si not particularly difficult. However whether
> they will contain type variables or not depends heavily on how the
> type inference algorithm proceeds.
> 
> If they contain type variables, then the situation becomes much more
> muddled, as these type variables may get instantiated by the subtyping
> check, and not necessarily as expected. So typing becomes rather
> unpredictable...
> 
>      Jacques Garrigue

We've reached the end of my intuition - I admit I get stuck thinking
about automatic casts with type variables.  I can only point out that
for an appropriate definition of "expected" (as in "found type x but
expected type y"), one will always get the expected type.  :)

If the line in the sand has to be drawn somewhere (between
auto-subtyping and not), this seems a simple and effective place to do so.

E.