Fix #8550: Soundness issue with class generalization

Changes

@@ -1000,6 +1000,9 @@ 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, report by Jeremy Yallop)
+
 OCaml 4.07.1 (4 October 2018)
 -----------------------------
 

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
+|}]

typing/ctype.ml

@@ -878,15 +878,17 @@ 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 generalize_expansive 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 ();
+  if try Hashtbl.find visited ty.id < contra with Not_found -> true then begin
+    Hashtbl.add visited ty.id contra;
+    let generalize_rec = generalize_expansive 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 ->
@@ -897,21 +899,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 =
   simple_abbrevs := Mnil;
-  generalize_expansive env !nongen_level (Hashtbl.create 7) ty
+  generalize_expansive env !nongen_level (Hashtbl.create 7) false ty
 
 let generalize_structure ty = generalize_structure !current_level ty