Do not use instance ~partial for principality when typing case bodies

Changes

@@ -328,8 +328,8 @@ Working version
   when the systhreads library is loaded.
   (David Allsopp, report by Anton Bachin, review by Xavier Leroy)
 
-- #8575, #10362: Surprising interaction between polymorphic variants and
-  constructor disambiguation.
+- #8575, #10362, #10364: Surprising interaction between polymorphic variants
+  and constructor disambiguation.
   (Jacques Garrigue, report and review by Thomas Refis)
 
 - #9936: Make sure that `List.([1;2;3])` is printed `[1;2;3]` in the toplevel

testsuite/tests/typing-gadts/didier.ml

@@ -52,7 +52,10 @@ val f : 't -> 't ty -> bool = <fun>
 Line 4, characters 12-13:
 4 |   | Bool -> x
                 ^
-Error: This expression has type t but an expression was expected of type bool
+Error: This expression has type t = bool
+       but an expression was expected of type bool
+       This instance of bool is ambiguous:
+       it would escape the scope of its equation
 |}];;
 (* val f : 'a -> 'a ty -> bool = <fun> *)
 
@@ -72,7 +75,10 @@ Error: This expression has type bool but an expression was expected of type
 Line 4, characters 11-16:
 4 |   | Int -> x > 0
                ^^^^^
-Error: This expression has type bool but an expression was expected of type t
+Error: This expression has type bool but an expression was expected of type
+         t = int
+       This instance of int is ambiguous:
+       it would escape the scope of its equation
 |}];;
 (* Error: This expression has type bool but an expression was expected of type
 t = int *)

testsuite/tests/typing-gadts/test.ml

@@ -370,7 +370,10 @@ module Propagation :
 Line 13, characters 19-20:
 13 |     | BoolLit b -> b
                         ^
-Error: This expression has type bool but an expression was expected of type s
+Error: This expression has type bool but an expression was expected of type
+         s = bool
+       This instance of bool is ambiguous:
+       it would escape the scope of its equation
 |}];;
 
 module Normal_constrs = struct
@@ -782,13 +785,6 @@ Error: This expression has type [> `A of a ]
        Type a is not compatible with type b = a
        This instance of a is ambiguous:
        it would escape the scope of its equation
-|}, Principal{|
-Line 2, characters 9-15:
-2 |   fun Eq o -> o ;; (* fail *)
-             ^^^^^^
-Error: This expression has type ([> `A of b ] as 'a) -> 'a
-       but an expression was expected of type [> `A of a ] -> [> `A of b ]
-       Types for tag `A are incompatible
 |}];;
 
 let f (type a b) (eq : (a,b) eq) (v : [> `A of a]) : [> `A of b] =

testsuite/tests/typing-misc/pr7937.ml

@@ -13,14 +13,6 @@ Line 3, characters 35-39:
 Error: This expression has type bool but an expression was expected of type
          ([< `X of int & 'a ] as 'a) r
        Types for tag `X are incompatible
-|}, Principal{|
-type 'a r = 'a constraint 'a = [< `X of int & 'a ]
-Line 3, characters 35-39:
-3 | let f: 'a. 'a r -> 'a r = fun x -> true;;
-                                       ^^^^
-Error: This expression has type bool but an expression was expected of type
-         ([< `X of 'b & 'a & 'c ] as 'a) r
-       Types for tag `X are incompatible
 |}]
 
 let g: 'a. 'a r -> 'a r = fun x -> { contents = 0 };;
@@ -31,14 +23,6 @@ Line 1, characters 35-51:
 Error: This expression has type int ref
        but an expression was expected of type ([< `X of int & 'a ] as 'a) r
        Types for tag `X are incompatible
-|}, Principal{|
-Line 1, characters 35-51:
-1 | let g: 'a. 'a r -> 'a r = fun x -> { contents = 0 };;
-                                       ^^^^^^^^^^^^^^^^
-Error: This expression has type int ref
-       but an expression was expected of type
-         ([< `X of 'b & 'a & 'c ] as 'a) r
-       Types for tag `X are incompatible
 |}]
 
 let h: 'a. 'a r -> _ = function true | false -> ();;

testsuite/tests/typing-polyvariants-bugs/pr8575.ml

@@ -18,7 +18,8 @@ val test : unit -> [> `A_t of A.t | `Onoes ] = <fun>
 Line 5, characters 49-50:
 5 |   | B -> if Random.bool () then `Onoes else `A_t B;;
                                                      ^
-Error: Unbound constructor B
+Warning 18 [not-principal]: this type-based constructor disambiguation is not principal.
+val test : unit -> [> `A_t of A.t | `Onoes ] = <fun>
 |}]
 
 let test () =
@@ -32,5 +33,6 @@ val test : unit -> [> `A_t of A.t | `Onoes ] = <fun>
 Line 5, characters 49-50:
 5 |   | B -> if Random.bool () then `Onoes else `A_t B;;
                                                      ^
-Error: Unbound constructor B
+Warning 18 [not-principal]: this type-based constructor disambiguation is not principal.
+val test : unit -> [> `A_t of A.t | `Onoes ] = <fun>
 |}]

typing/typecore.ml

@@ -273,20 +273,24 @@ let extract_option_type env ty =
     when Path.same path Predef.path_option -> ty
   | _ -> assert false
 
+let protect_extraction env ty =
+  if Env.has_local_constraints env then generic_instance ty else ty
+
 let extract_concrete_record env ty =
-  match extract_concrete_typedecl env ty with
+  match extract_concrete_typedecl env (protect_extraction env ty) with
     (p0, p, {type_kind=Type_record (fields, _)}) -> (p0, p, fields)
   | _ -> raise Not_found
 
 let extract_concrete_variant env ty =
-  match extract_concrete_typedecl env ty with
+  match extract_concrete_typedecl env (protect_extraction env ty) with
     (p0, p, {type_kind=Type_variant cstrs}) -> (p0, p, cstrs)
   | (p0, p, {type_kind=Type_open}) -> (p0, p, [])
   | _ -> raise Not_found
 
 let extract_label_names env ty =
   try
-    let (_, _,fields) = extract_concrete_record env ty in
+    let (_, _,fields) =
+      extract_concrete_record env (protect_extraction env ty) in
     List.map (fun l -> l.Types.ld_id) fields
   with Not_found ->
     assert false
@@ -2992,9 +2996,10 @@ and type_expect_
       type_construct env loc lid sarg ty_expected_explained sexp.pexp_attributes
   | Pexp_variant(l, sarg) ->
       (* Keep sharing *)
+      let ty_expected1 = protect_extraction env ty_expected in
       let ty_expected0 = instance ty_expected in
       begin try match
-        sarg, expand_head env ty_expected, expand_head env ty_expected0 with
+        sarg, expand_head env ty_expected1, expand_head env ty_expected0 with
       | Some sarg, {desc = Tvariant row}, {desc = Tvariant row0} ->
           let row = row_repr row and row0 = row_repr row0 in
           begin match row_field_repr (List.assoc l row.row_fields),
@@ -4861,6 +4866,8 @@ and type_cases
   ) half_typed_cases;
   (* type bodies *)
   let in_function = if List.length caselist = 1 then in_function else None in
+  let ty_res' = instance ty_res in
+  if !Clflags.principal then begin_def ();
   let cases =
     List.map
       (fun { typed_pat = pat; branch_env = ext_env; pat_vars = pvs; unpacks;
@@ -4883,14 +4890,8 @@ and type_cases
              tu_uid = Uid.mk ~current_unit:(Env.get_unit_name ())}
           ) unpacks
         in
-        let ty_res' =
-          if !Clflags.principal then begin
-            begin_def ();
-            let ty = instance ~partial:true ty_res in
-            end_def ();
-            generalize_structure ty; ty
-          end
-          else if contains_gadt then
+        let ty_expected =
+          if contains_gadt && not !Clflags.principal then
             (* allow propagation from preceding branches *)
             correct_levels ty_res
           else ty_res in
@@ -4904,20 +4905,17 @@ and type_cases
         in
         let exp =
           type_unpacks ?in_function ext_env
-            unpacks pc_rhs (mk_expected ?explanation ty_res')
+            unpacks pc_rhs (mk_expected ?explanation ty_expected)
         in
         {
          c_lhs = pat;
          c_guard = guard;
-         c_rhs = {exp with exp_type = instance ty_res'}
+         c_rhs = {exp with exp_type = ty_res'}
         }
       )
       half_typed_cases
   in
-  if !Clflags.principal || does_contain_gadt then begin
-    let ty_res' = instance ty_res in
-    List.iter (fun c -> unify_exp env c.c_rhs ty_res') cases
-  end;
+  if !Clflags.principal then end_def ();
   let do_init = may_contain_gadts || needs_exhaust_check in
   let ty_arg_check =
     if do_init then
@@ -4956,7 +4954,7 @@ and type_cases
   if may_contain_gadts then begin
     end_def ();
     (* Ensure that existential types do not escape *)
-    unify_exp_types loc env (instance ty_res) (newvar ()) ;
+    unify_exp_types loc env ty_res' (newvar ()) ;
   end;
   cases, partial