Relax the value restriction

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

8 files changed, 54 insertions, 39 deletions

diff --git a/Changes b/Changes
index 052a573a5a..fa6911c9a4 100644
--- a/Changes
+++ b/Changes
@@ -29,6 +29,8 @@
 
 - Fixed bug in ocamlopt -pack related to tracking of imported modules.
 
+- Allow polymorphism for covariant parts of expansive expressions
+
 
 Objective Caml 3.06:
 --------------------
diff --git a/stdlib/sys.ml b/stdlib/sys.ml
index 72332c2288..7099fa2f17 100644
--- a/stdlib/sys.ml
+++ b/stdlib/sys.ml
@@ -77,4 +77,4 @@ let catch_break on =
 
 (* OCaml version string, must be in the format described in sys.mli. *)
 
-let ocaml_version = "3.06+18 (2002-11-07)";;
+let ocaml_version = "3.06+19 (2002-12-03)";;
diff --git a/testlabl/poly.exp b/testlabl/poly.exp
index 61221d9ac2..93c682c629 100644
--- a/testlabl/poly.exp
+++ b/testlabl/poly.exp
@@ -1,4 +1,4 @@
-        Objective Caml version 3.06
+        Objective Caml version 3.06+19 (2002-12-03)
 
 #   * * *       #   type 'a t = { t : 'a; } 
 # type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; } 
@@ -118,7 +118,7 @@
 val p1 : point = <obj>
 val cp : color_point = <obj>
 val c : circle = <obj>
-val d : float = 11.4536240471
+val d : float = 11.45362404707371
 #   val f : < m : 'a. 'a -> 'a > -> < m : 'a. 'a -> 'a > = <fun>
 #   Characters 41-42:
 This expression has type < m : 'a. 'a -> 'a list > but is here used with type
diff --git a/testlabl/poly.exp2 b/testlabl/poly.exp2
index c2efef0c66..7021301a7d 100644
--- a/testlabl/poly.exp2
+++ b/testlabl/poly.exp2
@@ -1,4 +1,4 @@
-        Objective Caml version 3.06
+        Objective Caml version 3.06+19 (2002-12-03)
 
 #   * * *       #   type 'a t = { t : 'a; } 
 # type 'a fold = { fold : 'b. f:('b -> 'a -> 'b) -> init:'b -> 'b; } 
@@ -118,7 +118,7 @@
 val p1 : point = <obj>
 val cp : color_point = <obj>
 val c : circle = <obj>
-val d : float = 11.4536240471
+val d : float = 11.45362404707371
 #   val f : < m : 'a. 'a -> 'a > -> < m : 'b. 'b -> 'b > = <fun>
 #   Characters 41-42:
 This expression has type < m : 'a. 'a -> 'a list > but is here used with type
diff --git a/typing/btype.ml b/typing/btype.ml
index d7225ad3bc..9543a06a0e 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -402,15 +402,9 @@ let rec rev_log accu = function
     Unchanged -> accu
   | Invalid -> assert false
   | Change (ch, next) ->
-      rev_log (ch::accu) !next
-
-let rec invalidate_after = function
-    Unchanged -> ()
-  | Invalid -> assert false
-  | Change (_, next) ->
       let d = !next in
       next := Invalid;
-      invalidate_after d
+      rev_log (ch::accu) d
 
 let backtrack changes =
   match !changes with
@@ -420,5 +414,5 @@ let backtrack changes =
       cleanup_abbrev ();
       let backlog = rev_log [] change in
       List.iter undo_change backlog;
-      invalidate_after change;
-      changes := Unchanged
+      changes := Unchanged;
+      Weak.set trail 0 (Some changes)
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 8f30f2375c..17c3f6e4ce 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -535,8 +535,7 @@ let rec generalize_structure var_level ty =
     else if ty.level > !current_level then begin
       set_level ty generic_level;
       begin match ty.desc with
-        Tconstr (_, _, abbrev) ->
-          iter_abbrev (generalize_structure var_level) !abbrev
+        Tconstr (_, _, abbrev) -> abbrev := Mnil
       | _ -> ()
       end;
       iter_type_expr (generalize_structure var_level) ty
@@ -547,7 +546,7 @@ let generalize_structure var_level ty =
   simple_abbrevs := Mnil;
   generalize_structure var_level ty
 
-let generalize_expansive ty = generalize_structure !nongen_level ty
+(* let generalize_expansive ty = generalize_structure !nongen_level ty *)
 let generalize_global ty = generalize_structure !global_level ty
 let generalize_structure ty = generalize_structure !current_level ty
 
@@ -613,19 +612,41 @@ let rec update_level env level ty =
         iter_type_expr (update_level env level) ty
     | _ ->
         set_level ty level;
+        (* XXX what about abbreviations in Tconstr ? *)
         iter_type_expr (update_level env level) ty
     end
   end
 
-(* 
-   Function [update_level] will never try to expand an abbreviation in
-   this case ([current_level] is greater than the binding time of any
-   type constructor path). So, it can be called with the empty
-   environnement.
-*)
-let make_nongen ty =
+(* Generalize and lower levels of contravariant branches simultaneously *)
+
+let rec generalize_expansive env var_level ty =
+  let ty = repr ty in
+  if ty.level <> generic_level then begin
+    if ty.level > var_level then begin
+      set_level ty generic_level;
+      match ty.desc with
+        Tconstr (path, tyl, abbrev) ->
+          let variance =
+            try (Env.find_type path env).type_variance
+            with Not_found -> List.map (fun _ -> (true,true)) tyl in
+          abbrev := Mnil;
+          List.iter2
+            (fun (co,cn) t ->
+              if cn then update_level env var_level t
+              else generalize_expansive env var_level t)
+            variance tyl
+      | Tarrow (_, t1, t2, _) ->
+          update_level env var_level t1;
+          generalize_expansive env var_level t2
+      | _ ->
+          iter_type_expr (generalize_expansive env var_level) ty
+    end
+  end
+
+let generalize_expansive env ty =
+  simple_abbrevs := Mnil;
   try
-    update_level Env.empty !nongen_level ty
+    generalize_expansive env !nongen_level ty
   with Unify [_, ty'] ->
     raise (Unify [ty, ty'])
 
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 987f3ba2d4..e0da260fcb 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -85,17 +85,16 @@ val generalize: type_expr -> unit
         (* Generalize in-place the given type *)
 val iterative_generalization: int -> type_expr list -> type_expr list
         (* Efficient repeated generalization of a type *)
-val generalize_expansive: type_expr -> unit
-        (* Generalize the structure of a type, making variables
-           non-generalizable *)
+val generalize_expansive: Env.t -> type_expr -> unit
+        (* Generalize the covariant part of a type, making
+           contravariant branches non-generalizable *)
 val generalize_global: type_expr -> unit
-        (* Same, but variables are lowered to !global_level *)
+        (* Generalize the structure of a type, lowering variables
+           to !global_level *)
 val generalize_structure: type_expr -> unit
         (* Same, but variables are only lowered to !current_level *)
 val generalize_spine: type_expr -> unit
         (* Special function to generalize a method during inference *)
-val make_nongen: type_expr -> unit
-        (* Make non-generalizable the given type *)
 val correct_levels: type_expr -> type_expr
         (* Returns a copy with decreasing levels *)
 val limited_generalize: type_expr -> type_expr -> unit
diff --git a/typing/typecore.ml b/typing/typecore.ml
index b02deffab3..d6db977f2b 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -863,10 +863,11 @@ let rec type_exp env sexp =
         end;
         let arg = type_argument env sarg ty_arg in
         end_def ();
-        if not (is_nonexpansive arg) then List.iter make_nongen vars;
+        if vars <> [] && not (is_nonexpansive arg) then
+          generalize_expansive env arg.exp_type;
         check_univars env "field value" arg label.lbl_arg vars;
         num_fields := Array.length label.lbl_all;
-        (label, arg) in
+        (label, {arg with exp_type = instance arg.exp_type}) in
       let lbl_exp_list = List.map type_label_exp lid_sexp_list in
       let rec check_duplicates seen_pos lid_sexp lbl_exp =
         match (lid_sexp, lbl_exp) with
@@ -939,7 +940,8 @@ let rec type_exp env sexp =
       unify_exp env record ty_res;
       let newval = type_expect env snewval ty_arg in
       end_def ();
-      if not (is_nonexpansive newval) then List.iter make_nongen vars;
+      if vars <> [] && not (is_nonexpansive newval) then
+        generalize_expansive env newval.exp_type;
       check_univars env "field value" newval label.lbl_arg vars;
       { exp_desc = Texp_setfield(record, label, newval);
         exp_loc = sexp.pexp_loc;
@@ -1744,9 +1746,7 @@ and type_let env rec_flag spat_sexp_list =
   List.iter2
     (fun pat exp ->
        if not (is_nonexpansive exp) then
-         let f =
-           if !Clflags.principal then generalize_expansive else make_nongen in
-         iter_pattern (fun pat -> f pat.pat_type) pat)
+         iter_pattern (fun pat -> generalize_expansive env pat.pat_type) pat)
     pat_list exp_list;
   List.iter
     (fun pat -> iter_pattern (fun pat -> generalize pat.pat_type) pat)
@@ -1767,8 +1767,7 @@ let type_expression env sexp =
   let exp = type_exp env sexp in
   end_def();
   if is_nonexpansive exp then generalize exp.exp_type
-  else if !Clflags.principal then generalize_expansive exp.exp_type
-  else make_nongen exp.exp_type;
+  else generalize_expansive env exp.exp_type;
   exp
 
 (* Error report *)