subtyping private types

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@7022 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

4 files changed, 45 insertions, 11 deletions

diff --git a/testlabl/poly.exp b/testlabl/poly.exp
index bcb876d36..1d776980a 100644
--- a/testlabl/poly.exp
+++ b/testlabl/poly.exp
@@ -1,4 +1,4 @@
-        Objective Caml version 3.09+dev25 (2005-07-22)
+        Objective Caml version 3.09+dev27 (2005-08-13)
 
 #   * * *       #   type 'a t = { t : 'a; }
 # type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; }
@@ -370,7 +370,7 @@ This expression has type < m : 'b. 'b * ('b * 'a) > as 'a
 but is here used with type < m : 'b. 'b * ('b * < m : 'd. 'd * 'c > as 'c) >
 Types for method m are incompatible
 #     Characters 14-115:
-Type < m : 'a. 'a -> ('a * (< m : 'e. 'e -> 'b as 'd > as 'c) as 'b) >
+Type < m : 'a. 'a -> ('a * (< m : 'd. 'd -> 'b as 'e > as 'c) as 'b) >
 is not a subtype of type < m : 'a. 'a -> ('a * 'f as 'h) as 'g > as 'f 
 #       Characters 88-150:
 Signature mismatch:
@@ -398,4 +398,17 @@ is not included in
 #         val f :
   (< m : 'b. 'b -> (< m : 'b. 'b -> 'c * <  > > as 'c) * < .. >; .. > as 'a) ->
   'a -> bool = <fun>
+#   type t = [ `A | `B ]
+# type v = private [> t ]
+# - : t -> v = <fun>
+# type u = private [< t ]
+# - : u -> v = <fun>
+# Characters 9-21:
+Type v = [> `A | `B ] is not a subtype of type u = [< `A | `B ] 
+These two variant types have no intersection
+# type p = < x : p >
+# type q = private < x : p; .. >
+# - : q -> p = <fun>
+# Characters 9-21:
+Type p = < x : p > is not a subtype of type q = < x : p; .. > 
 # 
diff --git a/testlabl/poly.exp2 b/testlabl/poly.exp2
index 8381ac344..b6cf74901 100644
--- a/testlabl/poly.exp2
+++ b/testlabl/poly.exp2
@@ -1,4 +1,4 @@
-        Objective Caml version 3.09+dev25 (2005-07-22)
+        Objective Caml version 3.09+dev27 (2005-08-13)
 
 #   * * *       #   type 'a t = { t : 'a; }
 # type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; }
@@ -381,7 +381,7 @@ This expression has type < m : 'b. 'b * ('b * 'a) > as 'a
 but is here used with type < m : 'b. 'b * ('b * < m : 'd. 'd * 'c > as 'c) >
 Types for method m are incompatible
 #     Characters 14-115:
-Type < m : 'a. 'a -> ('a * (< m : 'e. 'e -> 'b as 'd > as 'c) as 'b) >
+Type < m : 'a. 'a -> ('a * (< m : 'd. 'd -> 'b as 'e > as 'c) as 'b) >
 is not a subtype of type < m : 'a. 'a -> ('a * 'f as 'h) as 'g > as 'f 
 #       Characters 88-150:
 Signature mismatch:
@@ -409,4 +409,17 @@ is not included in
 #         val f :
   (< m : 'b. 'b -> (< m : 'b. 'b -> 'c * <  > > as 'c) * < .. >; .. > as 'a) ->
   'a -> bool = <fun>
+#   type t = [ `A | `B ]
+# type v = private [> t ]
+# - : t -> v = <fun>
+# type u = private [< t ]
+# - : u -> v = <fun>
+# Characters 9-21:
+Type v = [> `A | `B ] is not a subtype of type u = [< `A | `B ] 
+These two variant types have no intersection
+# type p = < x : p >
+# type q = private < x : p; .. >
+# - : q -> p = <fun>
+# Characters 9-21:
+Type p = < x : p > is not a subtype of type q = < x : p; .. > 
 # 
diff --git a/testlabl/poly.ml b/testlabl/poly.ml
index f0053b930..e3c218161 100644
--- a/testlabl/poly.ml
+++ b/testlabl/poly.ml
@@ -523,3 +523,14 @@ let f x y =
   ignore (x :> <m:'a.'a -> 'c * < > > as 'c);
   ignore (y :> <m:'b.'b -> 'd * < > > as 'd);
   x = y;;
+
+type t = [`A|`B];;
+type v = private [> t];;
+fun x -> (x : t :> v);;
+type u = private [< t];;
+fun x -> (x : u :> v);;
+fun x -> (x : v :> u);;
+type p = <x:p>;;
+type q = private <x:p; ..>;;
+fun x -> (x : q :> p);;
+fun x -> (x : p :> q);;
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 955eefc46..758da495e 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -2847,11 +2847,9 @@ let rec subtype_rec env trace t1 t2 cstrs =
         subtype_list env trace tl1 tl2 cstrs
     | (Tconstr(p1, [], _), Tconstr(p2, [], _)) when Path.same p1 p2 ->
         cstrs
-    | (Tconstr(p1, tl1, abbrev1), _)
-      when generic_abbrev env p1 && not (has_constr_row' env t1) ->
+    | (Tconstr(p1, tl1, abbrev1), _) when generic_abbrev env p1 ->
         subtype_rec env trace (expand_abbrev env t1) t2 cstrs
-    | (_, Tconstr(p2, tl2, abbrev2))
-      when generic_abbrev env p2 && not (has_constr_row' env t2) ->
+    | (_, Tconstr(p2, tl2, abbrev2)) when generic_abbrev env p2 ->
         subtype_rec env trace t1 (expand_abbrev env t2) cstrs
     | (Tconstr(p1, tl1, _), Tconstr(p2, tl2, _)) when Path.same p1 p2 ->
         begin try
@@ -2871,7 +2869,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
           (trace, t1, t2, !univar_pairs)::cstrs
         end
     | (Tobject (f1, _), Tobject (f2, _))
-              when opened_object f1 && opened_object f2 ->
+      when opened_object f1 && opened_object f2 || has_constr_row t2 ->
         (* Same row variable implies same object. *)
         (trace, t1, t2, !univar_pairs)::cstrs
     | (Tobject (f1, _), Tobject (f2, _)) ->
@@ -2879,8 +2877,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
     | (Tvariant row1, Tvariant row2) ->
         let row1 = row_repr row1 and row2 = row_repr row2 in
         begin try
-          if not row1.row_closed || row1.row_more.desc <> Tvar
-          || row2.row_more.desc <> Tvar then raise Exit;
+          if not row1.row_closed then raise Exit;
           let r1, r2, pairs =
             merge_row_fields row1.row_fields row2.row_fields in
           if filter_row_fields false r1 <> [] then raise Exit;