RE: [Caml-list] Private types

["David Allsopp" <dra-news@metastack.com>]

Edgar Friendly wrote:
> 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.

Polymorphic variants. Consider:

type t = [ `A of int ]

let f (x : t) =
  let `A n = x
  in
    if n mod 2 = 0
    then (x : t :> [> t ])
    else `B (2 * n)

Without the full coercion for x you'll get a type error because the type
checker infers that the type of the [if] expression is [t] from the [then]
branch and then fails to unify [> `B of int ] with [t] unless the type of
[x] is first coerced to [> t ]. If the compiler were to try (x : t : [> t ])
in all those instances I think that would render polymorphic variants pretty
unusable ... the type checker needs to know that you meant to do that or
everything will unify!

> > 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?

+1! With reference my previous comment that "the type checker needs to know
if you meant that", there's still the option of using fully abstract types
if you wanted to avoid this kind of automatic coercion and have, say,
positive integers totally distinct from all integers without an explicit
cast.

All said, I do see Jacques point of wanting to keep coercion and type
inference totally separate... though perhaps if coercions were only tried
during unification if at least one of the types in question is private that
would maintain a certain level of predictability about when they're used
automatically?


David