Merge pull request #10364 from COCTI/principal_cases

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

Changes

@@ -807,6 +807,9 @@ OCaml 4.14.0
   (Xavier Leroy, report by Rehan Malak, review by Gabriel Scherer and
    Vincent Laviron)
 
+- #10364: Improve detection of ambiguity in case bodies.
+  (Jacques Garrigue, review by Thomas Refis)
+
 - #10473: Add CFI directives to RISC-V runtime and asmcomp.
   This allows stacktraces to work in gdb through C and OCaml calls.
   (Edwin Török, review by Nicolás Ojeda Bär and Xavier Leroy)
@@ -1443,8 +1446,8 @@ OCaml 4.13.0 (24 September 2021)
   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: Surprising interaction between polymorphic variants
+  and constructor disambiguation.
   (Jacques Garrigue, report and review by Thomas Refis)
 
 - #8917, #8929, #9889, #10219: fix printing of nested recursive definitions

testsuite/tests/typing-gadts/ambivalent_apply.ml

@@ -11,6 +11,8 @@ type (_, _) eq = Refl : ('a, 'a) eq
 let f (type a b) (w1 : (a, b -> b) eq) (w2 : (a, int -> int) eq) (g : a) =
    let Refl = w1 in let Refl = w2 in g 3;;
 [%%expect{|
+val f : ('a, 'b -> 'b) eq -> ('a, int -> int) eq -> 'a -> 'b = <fun>
+|}, Principal{|
 Line 2, characters 37-40:
 2 |    let Refl = w1 in let Refl = w2 in g 3;;
                                          ^^^

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

@@ -12,13 +12,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
-|}, 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
 |}]
 
 let g: 'a. 'a r -> 'a r = fun x -> { contents = 0 };;
@@ -28,13 +21,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
-|}, 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
 |}]
 
 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

@@ -300,13 +300,19 @@ let extract_option_type env ty =
     Tconstr(path, [ty], _) when Path.same path Predef.path_option -> ty
   | _ -> assert false
 
+let protect_expansion env ty =
+  if Env.has_local_constraints env then generic_instance ty else ty
+
 type record_extraction_result =
   | Record_type of Path.t * Path.t * Types.label_declaration list
   | Not_a_record_type
   | Maybe_a_record_type
 
+let extract_concrete_typedecl_protected env ty =
+  extract_concrete_typedecl env (protect_expansion env ty)
+
 let extract_concrete_record env ty =
-  match extract_concrete_typedecl env ty with
+  match extract_concrete_typedecl_protected env ty with
   | Typedecl(p0, p, {type_kind=Type_record (fields, _)}) ->
     Record_type (p0, p, fields)
   | Has_no_typedecl | Typedecl(_, _, _) -> Not_a_record_type
@@ -318,7 +324,7 @@ type variant_extraction_result =
   | Maybe_a_variant_type
 
 let extract_concrete_variant env ty =
-  match extract_concrete_typedecl env ty with
+  match extract_concrete_typedecl_protected env ty with
   | Typedecl(p0, p, {type_kind=Type_variant (cstrs, _)}) ->
     Variant_type (p0, p, cstrs)
   | Typedecl(p0, p, {type_kind=Type_open}) ->
@@ -2893,7 +2899,7 @@ and type_expect_
   | Pexp_constant(Pconst_string (str, _, _) as cst) -> (
     let cst = constant_or_raise env loc cst in
     (* Terrible hack for format strings *)
-    let ty_exp = expand_head env ty_expected in
+    let ty_exp = expand_head env (protect_expansion env ty_expected) in
     let fmt6_path =
       Path.(Pdot (Pident (Ident.create_persistent "CamlinternalFormatBasics"),
                   "format6"))
@@ -3099,9 +3105,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_expansion env ty_expected in
       let ty_expected0 = instance ty_expected in
       begin try match
-        sarg, get_desc (expand_head env ty_expected),
+        sarg, get_desc (expand_head env ty_expected1),
         get_desc (expand_head env ty_expected0)
       with
       | Some sarg, Tvariant row, Tvariant row0 ->
@@ -3768,7 +3775,7 @@ and type_expect_
   | Pexp_poly(sbody, sty) ->
       if !Clflags.principal then begin_def ();
       let ty, cty =
-        match sty with None -> ty_expected, None
+        match sty with None -> protect_expansion env ty_expected, None
         | Some sty ->
             let sty = Ast_helper.Typ.force_poly sty in
             let cty = Typetexp.transl_simple_type env false sty in
@@ -3852,7 +3859,8 @@ and type_expect_
         match get_desc (Ctype.expand_head env (instance ty_expected)) with
           Tpackage (p, fl) ->
             if !Clflags.principal &&
-              get_level (Ctype.expand_head env ty_expected)
+              get_level (Ctype.expand_head env
+                           (protect_expansion env ty_expected))
                 < Btype.generic_level
             then
               Location.prerr_warning loc
@@ -4461,7 +4469,7 @@ and type_argument ?explanation ?recarg env sarg ty_expected' ty_expected =
         (lv <> generic_level || get_level ty_fun' <> generic_level)
       and ty_fun = instance ty_fun' in
       let ty_arg, ty_res =
-        match get_desc (expand_head env ty_expected') with
+        match get_desc (expand_head env ty_expected) with
           Tarrow(Nolabel,ty_arg,ty_res,_) -> ty_arg, ty_res
         | _ -> assert false
       in
@@ -4593,10 +4601,30 @@ and type_application env funct sargs =
   in
   let warned = ref false in
   let rec type_args args ty_fun ty_fun0 sargs =
+    let type_unknown_args () =
+      (* We're not looking at a *known* function type anymore, or there are no
+         arguments left. *)
+      let ty_fun, typed_args =
+        List.fold_left type_unknown_arg (ty_fun0, args) sargs
+      in
+      let args =
+        (* Force typing of arguments.
+           Careful: the order matters here. Using [List.rev_map] would be
+           incorrect. *)
+        List.map
+          (function
+            | l, None -> l, None
+            | l, Some f -> l, Some (f ()))
+          (List.rev typed_args)
+      in
+      let result_ty = instance (result_type !omitted_parameters ty_fun) in
+      args, result_ty
+    in
+    if sargs = [] then type_unknown_args () else
     let ty_fun' = expand_head env ty_fun in
     match get_desc ty_fun', get_desc (expand_head env ty_fun0) with
     | Tarrow (l, ty, ty_fun, com), Tarrow (_, ty0, ty_fun0, _)
-      when sargs <> [] && is_commu_ok com ->
+      when is_commu_ok com ->
         let lv = get_level ty_fun' in
         let may_warn loc w =
           if not !warned && !Clflags.principal && lv <> generic_level
@@ -4674,23 +4702,7 @@ and type_application env funct sargs =
         in
         type_args ((l,arg)::args) ty_fun ty_fun0 remaining_sargs
     | _ ->
-        (* We're not looking at a *known* function type anymore, or there are no
-           arguments left. *)
-        let ty_fun, typed_args =
-          List.fold_left type_unknown_arg (ty_fun0, args) sargs
-        in
-        let args =
-          (* Force typing of arguments.
-             Careful: the order matters here. Using [List.rev_map] would be
-             incorrect. *)
-          List.map
-            (function
-              | l, None -> l, None
-              | l, Some f -> l, Some (f ()))
-            (List.rev typed_args)
-        in
-        let result_ty = instance (result_type !omitted_parameters ty_fun) in
-        args, result_ty
+        type_unknown_args ()
   in
   let is_ignore funct =
     is_prim ~name:"%ignore" funct &&
@@ -4983,6 +4995,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;
@@ -5005,14 +5019,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
@@ -5026,20 +5034,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
@@ -5078,7 +5083,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