Fix #8550: Soundness issue with class generalization (#8552)

* also rename generalize_expansive -> lower_contravariant

5 files changed, 47 insertions, 26 deletions

diff --git a/Changes b/Changes
index f155ccac40..a2585cf73c 100644
--- a/Changes
+++ b/Changes
@@ -854,6 +854,10 @@ OCaml 4.08.0
   (Thomas Refis, review by Gabriel Scherer and Jacques Garrigue,
   report by Daniel Bünzli and Jon Ludlam)
 
+- #8550, #8552: Soundness issue with class generalization
+  (Jacques Garrigue, review by Leo White and Thomas Refis,
+  report by Jeremy Yallop)
+
 OCaml 4.07.1 (4 October 2018)
 -----------------------------
 
diff --git a/testsuite/tests/typing-poly/poly.ml b/testsuite/tests/typing-poly/poly.ml
index 24b5b4a123..c8f050c164 100644
--- a/testsuite/tests/typing-poly/poly.ml
+++ b/testsuite/tests/typing-poly/poly.ml
@@ -1722,3 +1722,15 @@ module M :
       val i : 'a -> 'a
     end
 |}]
+
+(* #8550 *)
+class ['a] r = let r : 'a = ref [] in object method get = r end;;
+[%%expect{|
+Line 1, characters 0-63:
+1 | class ['a] r = let r : 'a = ref [] in object method get = r end;;
+    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: The type of this class,
+       class ['a] r :
+         object constraint 'a = '_weak2 list ref method get : 'a end,
+       contains type variables that cannot be generalized
+|}]
diff --git a/typing/ctype.ml b/typing/ctype.ml
index c3d24f5256..fb8f4c1051 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -711,9 +711,9 @@ let rec generalize_structure var_level ty =
     end
   end
 
-let generalize_structure var_level ty =
+let generalize_structure ty =
   simple_abbrevs := Mnil;
-  generalize_structure var_level ty
+  generalize_structure !current_level ty
 
 (* Generalize the spine of a function, if the level >= !current_level *)
 
@@ -868,15 +868,22 @@ let update_level env level ty =
       update_level env level true ty
   end
 
-(* Generalize and lower levels of contravariant branches simultaneously *)
+(* Lower level of type variables inside contravariant branches *)
 
-let rec generalize_expansive env var_level visited ty =
+let rec lower_contravariant env var_level visited contra ty =
   let ty = repr ty in
-  if ty.level = generic_level || ty.level <= var_level then () else
-  if not (Hashtbl.mem visited ty.id) then begin
-    Hashtbl.add visited ty.id ();
+  let must_visit =
+    ty.level > var_level &&
+    match Hashtbl.find visited ty.id with
+    | done_contra -> contra && not done_contra
+    | exception Not_found -> true
+  in
+  if must_visit then begin
+    Hashtbl.add visited ty.id contra;
+    let generalize_rec = lower_contravariant env var_level visited in
     match ty.desc with
-      Tconstr (path, tyl, abbrev) ->
+      Tvar _ -> if contra then set_level ty var_level
+    | Tconstr (path, tyl, abbrev) ->
         let variance =
           try (Env.find_type path env).type_variance
           with Not_found ->
@@ -887,23 +894,21 @@ let rec generalize_expansive env var_level visited ty =
         List.iter2
           (fun v t ->
             if Variance.(mem May_weak v)
-            then generalize_structure var_level t
-            else generalize_expansive env var_level visited t)
+            then generalize_rec true t
+            else generalize_rec contra t)
           variance tyl
     | Tpackage (_, _, tyl) ->
-        List.iter (generalize_structure var_level) tyl
+        List.iter (generalize_rec true) tyl
     | Tarrow (_, t1, t2, _) ->
-        generalize_structure var_level t1;
-        generalize_expansive env var_level visited t2
+        generalize_rec true t1;
+        generalize_rec contra t2
     | _ ->
-        iter_type_expr (generalize_expansive env var_level visited) ty
+        iter_type_expr (generalize_rec contra) ty
   end
 
-let generalize_expansive env ty =
+let lower_contravariant env ty =
   simple_abbrevs := Mnil;
-  generalize_expansive env !nongen_level (Hashtbl.create 7) ty
-
-let generalize_structure ty = generalize_structure !current_level ty
+  lower_contravariant env !nongen_level (Hashtbl.create 7) false ty
 
 (* Correct the levels of type [ty]. *)
 let correct_levels ty =
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 190df0cc67..15e70c991e 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -146,9 +146,9 @@ val filter_row_fields:
 
 val generalize: type_expr -> unit
         (* Generalize in-place the given type *)
-val generalize_expansive: Env.t -> type_expr -> unit
-        (* Generalize the covariant part of a type, making
-           contravariant branches non-generalizable *)
+val lower_contravariant: Env.t -> type_expr -> unit
+        (* Lower level of type variables inside contravariant branches;
+           to be used before generalize for expansive expressions *)
 val generalize_structure: type_expr -> unit
         (* Same, but variables are only lowered to !current_level *)
 val generalize_spine: type_expr -> unit
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 089654dfa8..e87169aeac 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -1990,7 +1990,7 @@ let list_labels env ty =
 (* Check that all univars are safe in a type *)
 let check_univars env expans kind exp ty_expected vars =
   if expans && not (is_nonexpansive exp) then
-    generalize_expansive env exp.exp_type;
+    lower_contravariant env exp.exp_type;
   (* need to expand twice? cf. Ctype.unify2 *)
   let vars = List.map (expand_head env) vars in
   let vars = List.map (expand_head env) vars in
@@ -2481,7 +2481,7 @@ and type_expect_
       begin_def ();
       let arg = type_exp env sarg in
       end_def ();
-      if not (is_nonexpansive arg) then generalize_expansive env arg.exp_type;
+      if not (is_nonexpansive arg) then lower_contravariant env arg.exp_type;
       generalize arg.exp_type;
       let cases, partial =
         type_cases ~exception_allowed:true env arg.exp_type ty_expected true loc
@@ -3831,7 +3831,7 @@ and type_label_exp create env loc ty_expected
       begin_def ();
       let arg = type_exp env sarg in
       end_def ();
-      generalize_expansive env arg.exp_type;
+      lower_contravariant env arg.exp_type;
       unify_exp env arg ty_arg;
       check_univars env false "field value" arg label.lbl_arg vars;
       arg
@@ -4654,7 +4654,7 @@ and type_let
   List.iter2
     (fun pat exp ->
        if not (is_nonexpansive exp) then
-         generalize_expansive env pat.pat_type)
+         lower_contravariant env pat.pat_type)
     pat_list exp_list;
   iter_pattern_variables_type generalize pvs;
   (* The next line changes the toplevel experience from:
@@ -4762,7 +4762,7 @@ let type_expression env sexp =
   begin_def();
   let exp = type_exp env sexp in
   end_def();
-  if not (is_nonexpansive exp) then generalize_expansive env exp.exp_type;
+  if not (is_nonexpansive exp) then lower_contravariant env exp.exp_type;
   generalize exp.exp_type;
   match sexp.pexp_desc with
     Pexp_ident lid ->