On Thu, 31 Mar 2005 17:32:23 +0900 (JST), Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> From: Yaron Minsky <yminsky@gmail.com>
> 
> > Interesting.  I guess this is best understood as a limitation of the
> > type-checking algorithm.  Does anyone know if there are any plans to
> > remove this limitation?  Are there fundamental reasons why it would be
> > difficult to do so?
> 
> This is not a limitation of the type checking algorithm per se.
> Rather, the type checking algorithm prefers not to use
> exhaustiveness information when this can be avoided, to keep it
> predictable.
> (Exhaustiveness is only used for polymorphic variants, but for
> a deeper reason.)

I guess I'm somewhat out of my depth.  I don't quite understand what
you mean by exhaustiveness information, and I don't see why avoiding
it improves predictability.  Do you have an example in mind?

> Is it so difficult to make the extra constructors explicit?

I'd say there are two issues.  The first is that it really can be a
pain for large variant types, particularly when the contents of those
types are changing during development, and you don't want the function
in question to depend on anything other than the particular variants
being modified.

The second issue is that it just seems like a violation of the
principle of least surprise.  The fact that this fails to compile:

# function Some x -> Some (float x) | x -> x;;
This expression has type int option but is here used with type float option

but that this does compile:

# function Some x -> Some (float x) | None as x -> x;;

was quite unexpected, at least by me.  That said, it's not all that
bad.  It just seems confusing, and since I don't see the downside of
accepting both functions as type-safe, I don't understand why it's not
done.

y