Fix PR8701 by expanding types in lower_contravariant (#8725)

Changes

@@ -318,6 +318,9 @@ OCaml 4.09.0
   ocamldep. It used to turn some errors into successes
   (Jérémie Dimino)
 
+- #8701, #8725: Variance of constrained parameters causes principality issues
+  (Jacques Garrigue, report by Leo White, review by Gabriel Scherer)
+
 OCaml 4.08.0
 ------------
 

testsuite/tests/typing-poly/poly.ml

@@ -1734,3 +1734,22 @@ Error: The type of this class,
          object constraint 'a = '_weak2 list ref method get : 'a end,
        contains type variables that cannot be generalized
 |}]
+
+(* #8701 *)
+type 'a t = 'a constraint 'a = 'b list;;
+type 'a s = 'a list;;
+let id x = x;;
+[%%expect{|
+type 'a t = 'a constraint 'a = 'b list
+type 'a s = 'a list
+val id : 'a -> 'a = <fun>
+|}]
+
+let x : [ `Foo of _ s | `Foo of 'a t ] = id (`Foo []);;
+[%%expect{|
+val x : [ `Foo of 'a s ] = `Foo []
+|}]
+let x : [ `Foo of 'a t | `Foo of _ s ] = id (`Foo []);;
+[%%expect{|
+val x : [ `Foo of 'a list t ] = `Foo []
+|}]

typing/ctype.ml

@@ -890,30 +890,36 @@ let rec lower_contravariant env var_level visited contra ty =
   in
   if must_visit then begin
     Hashtbl.add visited ty.id contra;
-    let generalize_rec = lower_contravariant env var_level visited in
+    let lower_rec = lower_contravariant env var_level visited in
     match ty.desc with
       Tvar _ -> if contra then set_level ty var_level
-    | Tconstr (path, tyl, abbrev) ->
+    | Tconstr (_, [], _) -> ()
+    | Tconstr (path, tyl, _abbrev) ->
         let variance =
           try (Env.find_type path env).type_variance
           with Not_found ->
             (* See testsuite/tests/typing-missing-cmi-2 for an example *)
             List.map (fun _ -> Variance.may_inv) tyl
         in
-        abbrev := Mnil;
-        List.iter2
-          (fun v t ->
-            if Variance.(mem May_weak v)
-            then generalize_rec true t
-            else generalize_rec contra t)
-          variance tyl
+        if List.for_all ((=) Variance.null) variance then () else
+        begin match !forward_try_expand_once env ty with
+        | ty -> lower_rec contra ty
+        | exception Cannot_expand ->
+          List.iter2
+            (fun v t ->
+              if v = Variance.null then () else
+              if Variance.(mem May_weak v)
+              then lower_rec true t
+              else lower_rec contra t)
+            variance tyl
+        end
     | Tpackage (_, _, tyl) ->
-        List.iter (generalize_rec true) tyl
+        List.iter (lower_rec true) tyl
     | Tarrow (_, t1, t2, _) ->
-        generalize_rec true t1;
-        generalize_rec contra t2
+        lower_rec true t1;
+        lower_rec contra t2
     | _ ->
-        iter_type_expr (generalize_rec contra) ty
+        iter_type_expr (lower_rec contra) ty
   end
 
 let lower_contravariant env ty =