Hi,

> 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), and that
> subtyping is potentially very costly (structural subtyping is much
> harder to check than the nominal subtyping you have in Java.)


Thanks for the explanation, Jacques.  If I understand correctly, by requiring
subtyping relations to be explicitly coerced, the "giant system of equations"
behind unification can be simplified because it doesn't need to worry about
all possible subtyping relations.  So in a sense this is also a matter of
computational tractability, right?

I have also been playing with 3.11's private types, and I would like to
share a problem I've come across.  Suppose I have a Foobar module defined
as follows (note the use of a type constraint):


module Foobar:
sig
	type foo_t = [ `A ]
	type bar_t = [ `B ]
	type foobar_t = [ foo_t | bar_t ]
	type 'a t = 'a constraint 'a = [< foobar_t ]

	val make_a: unit -> foo_t t
	val make_b: unit -> bar_t t
	val is_foo: [< foobar_t] t -> bool
	val is_bar: [< foobar_t] t -> bool
end =
struct
	type foo_t = [ `A ]
	type bar_t = [ `B ]
	type foobar_t = [ foo_t | bar_t ]
	type 'a t = 'a constraint 'a = [< foobar_t ]

	let make_a () = `A
	let make_b () = `B
	let is_foo = function `A -> true | `B -> false
	let is_bar = function `B -> true | `A -> false
end


Suppose also that I want to define a "is_foo" function in an external module.
This function only needs to pattern-match on Foobar.t values.  The following
code will work:

module Mymod:
sig
	open Foobar

	val is_foo2: [< foobar_t] t -> bool
end =
struct
	let is_foo2 = function `A -> true | `B -> false
end


But now consider that I want to enforce the creation of Foobar.t values only
via Foobar's constructor functions, but I would like to keep the possibility of
external modules to pattern-match on Foobar.t values.  In other words, change
Foobar but don't break Mymod.  The immediate (naïve) solution is to make
use of private types, thus changing the signature of Foobar to the following:


module Foobar:
sig
	type foo_t = [ `A ]
	type bar_t = [ `B ]
	type foobar_t = [ foo_t | bar_t ]
	type 'a t = private 'a constraint 'a = [< foobar_t ]

	val make_a: unit -> foo_t t
	val make_b: unit -> bar_t t
	val is_foo: [< foobar_t] t -> bool
	val is_bar: [< foobar_t] t -> bool
end = (...)


But this will break Mymod.  The compile will complain with the following error:

      Values do not match:
         val is_foo2 : [< `A | `B ] -> bool
       is not included in
         val is_foo2 : [< Foobar.foobar_t ] Foobar.t -> bool

Any ideas on how can I get around this problem?

Thanks!
Cheers,
Dario Teixeira