Fix #10822: Bad interaction between ambivalent types and subtyping co…

…ercions (#10823)

Changes

@@ -411,6 +411,9 @@ OCaml 4.14.0
 - #10763, #10764: fix miscompilation of method delegation
   (Alain Frisch, review by Vincent Laviron and Jacques Garrigue)
 
+- #10822, #10823: Bad interaction between ambivalent types and subtyping
+  coercions (Jacques Garrigue, report and review by Frédéric Bour)
+
 
 OCaml 4.13 maintenance branch
 -----------------------------

testsuite/tests/typing-gadts/principality-and-gadts.ml

@@ -440,3 +440,19 @@ let bar x =
 [%%expect{|
 val bar : string foo -> string = <fun>
 |}]
+
+(* #10822 *)
+type t
+type u = private t
+type ('a, 'b) eq = Refl : ('a, 'a) eq
+[%%expect{|
+type t
+type u = private t
+type ('a, 'b) eq = Refl : ('a, 'a) eq
+|}]
+
+let foo (type s) x (Refl : (s, u) eq) =
+  (x : s :> t)
+[%%expect{|
+val foo : 's -> ('s, u) eq -> t = <fun>
+|}]

typing/typecore.ml

@@ -3459,15 +3459,15 @@ and type_expect_
             and (cty', ty', force') =
               Typetexp.transl_simple_type_delayed env sty'
             in
+            end_def ();
+            generalize_structure ty;
+            generalize_structure ty';
             begin try
-              let force'' = subtype env ty ty' in
+              let force'' = subtype env (instance ty) (instance ty') in
               force (); force' (); force'' ()
             with Subtype err ->
               raise (Error(loc, env, Not_subtype err))
             end;
-            end_def ();
-            generalize_structure ty;
-            generalize_structure ty';
             (type_argument env sarg ty (instance ty),
              instance ty', Some cty, cty')
       in