Fix #10907: Wrong type inferred from existential types

Changes

@@ -451,6 +451,9 @@ OCaml 4.14.0
   operation in `NO_SHARING` mode.
   (Xavier Leroy, report by Anil Madhavapeddy, review by Alain Frisch)
 
+- #10907, #10959: Wrong type inferred from existential types
+  (Jacques Garrigue and Gabriel Scherer, report by @dyzsr, review by Leo White)
+
 
 OCaml 4.13 maintenance branch
 -----------------------------

testsuite/tests/typing-gadts/pr10189.ml

@@ -111,24 +111,6 @@ Warning 8 [partial-match]: this pattern-matching is not exhaustive.
 Here is an example of a case that is not matched:
 Some A
 val g : 'a M.j t option -> unit = <fun>
-|}, Principal{|
-module M :
-  sig
-    type 'a d
-    type i = < m : 'c. 'c -> 'c d >
-    type 'a j = < m : 'c. 'c -> 'a >
-  end
-type _ t = A : M.i t
-File "_none_", line 1:
-Warning 18 [not-principal]: typing this pattern requires considering $0 and 'c M.d as equal.
-But the knowledge of these types is not principal.
-Line 9, characters 2-20:
-9 |   let None = y in () ;;
-      ^^^^^^^^^^^^^^^^^^
-Warning 8 [partial-match]: this pattern-matching is not exhaustive.
-Here is an example of a case that is not matched:
-Some A
-val g : 'a M.j t option -> unit = <fun>
 |}]
 
 (* more examples by @lpw25 *)

testsuite/tests/typing-gadts/pr10907.ml

@@ -0,0 +1,53 @@
+(* TEST
+   * expect
+*)
+
+(* from @dyzsr *)
+type 'a t = T : ('a -> 'b) * ('b -> 'a) -> 'a t;;
+[%%expect{|
+type 'a t = T : ('a -> 'b) * ('b -> 'a) -> 'a t
+|}]
+
+let t = T ((fun x -> x), (fun x -> x));;
+[%%expect{|
+val t : 'a t = T (<fun>, <fun>)
+|}]
+
+let t1 = let T (g, h) = t in h (g 1);;
+[%%expect{|
+val t1 : int = 1
+|}]
+
+let f x = let T (g, h) = t in h (g x);;
+[%%expect{|
+val f : 'a -> 'a = <fun>
+|}]
+
+(* reformulation by @gasche *)
+
+(* an isomorphism between 'a and 'b *)
+type ('a, 'b) iso = ('a -> 'b) * ('b -> 'a)
+
+(* exists 'b. ('a, 'b) iso *)
+type 'a some_iso = Iso : ('a, 'b) iso -> 'a some_iso
+[%%expect{|
+type ('a, 'b) iso = ('a -> 'b) * ('b -> 'a)
+type 'a some_iso = Iso : ('a, 'b) iso -> 'a some_iso
+|}]
+
+(* forall 'a. exists 'b. ('a, 'b) iso *)
+let t : 'a . 'a some_iso =
+  Iso ((fun x -> x), (fun x -> x))
+[%%expect{|
+val t : 'a some_iso = Iso (<fun>, <fun>)
+|}]
+
+let unsound_cast : 'a 'b. 'a -> 'b = fun x ->
+  match t with Iso (g, h) -> h (g x)
+[%%expect{|
+Lines 1-2, characters 37-36:
+1 | .....................................fun x ->
+2 |   match t with Iso (g, h) -> h (g x)
+Error: This definition has type 'c. 'c -> 'c which is less general than
+         'a 'b. 'a -> 'b
+|}]

typing/ctype.ml

@@ -853,6 +853,10 @@ let rec lower_contravariant env var_level visited contra ty =
         iter_type_expr (lower_rec contra) ty
   end
 
+let lower_variables_only env level ty =
+  simple_abbrevs := Mnil;
+  lower_contravariant env level (Hashtbl.create 7) true ty
+
 let lower_contravariant env ty =
   simple_abbrevs := Mnil;
   lower_contravariant env !nongen_level (Hashtbl.create 7) false ty

typing/ctype.mli

@@ -113,6 +113,8 @@ val generalize: type_expr -> unit
 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 lower_variables_only: Env.t -> int -> type_expr -> unit
+        (* Lower all variables to the given level *)
 val generalize_structure: type_expr -> unit
         (* Generalize the structure of a type, lowering variables
            to !current_level *)

typing/typecore.ml

@@ -716,11 +716,14 @@ let solve_Ppat_construct ~refine env loc constr no_existentials
           solve_constructor_annotation env name_list sty ty_args ty_ex in
         ty_args, ty_res, equated_types, existential_ctyp
   in
+  if constr.cstr_existentials <> [] then
+    lower_variables_only !env expansion_scope ty_res;
   end_def ();
   generalize_structure expected_ty;
   generalize_structure ty_res;
   List.iter generalize_structure ty_args;
-  if !Clflags.principal then begin
+  if !Clflags.principal && refine = None then begin
+    (* Do not warn for couter examples *)
     let exception Warn_only_once in
     try
       TypePairs.iter