Jacques Garrigue wrote:

> Your intuition is correct that it would theoretically be possible to
> try subtyping in place of unification in some cases. The trouble is
> that thoses cases are not easy to specify (so that it would be hard
> for the programmer to known when he can remove a coercion), 

Does the compiler really get any information from an explicit cast that
it can't figure out already?  I can't come up with any example.

> and that
> subtyping is potentially very costly (structural subtyping is much
> harder to check than the nominal subtyping you have in Java.)

As the compiler needs to check that explicit casts are valid, I don't
see any performance difference between explicit and implicit subtype casts.

> So the current approach is to completely separate subtyping and type
> inference, and require coercions everywhere subtyping is needed.
> 
Would it be particularly difficult to, in the cases where type [x] is
found but type [y] is expected, to try a (foo : x :> y) cast?

> You can also compare that to the situation between int and float.
> For most uses, int can be viewed as a subtype of float. However ocaml
> separates the two, and requires coercion functions whenever you want
> to use an int as a float.
> 
Code isn't produced by a :> cast.  As the internal representation of int
and float differs, a coercion function isn't required.  The internal
representation of [private int] and [int] is the same, not to mention
one is exactly the [private] of the other.

> Cheers,
> 
> Jacques Garrigue

Merci,
E.