Keep generalized structure from patterns when typing let

Author: lpw25

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-poly/poly.ml

@@ -1540,6 +1540,15 @@ Error: This expression has type < m : 'x. [< `Foo of 'x ] -> 'x >
        but an expression was expected of type
          < m : 'a. [< `Foo of int ] -> 'a >
        The universal variable 'x would escape its scope
+|}, Principal{|
+Line 2, characters 2-72:
+2 |   object method m : 'x. [< `Foo of 'x] -> 'x = fun x -> assert false end;;
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This expression has type < m : 'x. [< `Foo of 'x ] -> 'x >
+       but an expression was expected of type < m : 'a. 'b -> 'a >
+       The method m has type 'x. [< `Foo of 'x ] -> 'x,
+       but the expected method type was 'a. 'b -> 'a
+       The universal variable 'x would escape its scope
 |}];;
 (* ok *)
 let f (n : < m : 'a 'r. [< `Foo of 'a & int | `Bar] as 'r >) =

testsuite/tests/typing-poly/pr11544.ml

@@ -8,11 +8,4 @@ let poly3 : 'b. M.t -> 'b -> 'b =
 [%%expect {|
 module M : sig type t = T end
 val poly3 : M.t -> 'b -> 'b = <fun>
-|}, Principal{|
-module M : sig type t = T end
-Line 3, characters 6-7:
-3 |   fun T x -> x
-          ^
-Warning 18 [not-principal]: this type-based constructor disambiguation is not principal.
-val poly3 : M.t -> 'b -> 'b = <fun>
 |}];;

typing/typecore.ml

@@ -6304,11 +6304,13 @@ and type_let
       end_def ();
       iter_pattern_variables_type generalize_structure pvs;
       List.map (fun (m, pat) ->
-        generalize_structure pat.pat_type;
-        m, {pat with pat_type = instance pat.pat_type}
+        let ty = pat.pat_type in
+        generalize_structure ty;
+        m, {pat with pat_type = instance ty}, ty
       ) pat_list
-    end else
-      pat_list
+    end else begin
+      List.map (fun (m, pat) -> (m, pat, pat.pat_type)) pat_list
+    end
   in
   (* Only bind pattern variables after generalizing *)
   List.iter (fun f -> f()) force;
@@ -6342,7 +6344,7 @@ and type_let
            || (is_recursive && (Warnings.is_active Warnings.Unused_rec_flag))))
       attrs_list
   in
-  let mode_pat_slot_list =
+  let mode_typ_slot_list =
     (* Algorithm to detect unused declarations in recursive bindings:
        - During type checking of the definitions, we capture the 'value_used'
          events on the bound identifiers and record them in a slot corresponding
@@ -6360,9 +6362,9 @@ and type_let
        warning is 26, not 27.
      *)
     List.map2
-      (fun attrs (mode, pat) ->
+      (fun attrs (mode, pat, expected_ty) ->
          Builtin_attributes.warning_scope ~ppwarning:false attrs (fun () ->
-           if not warn_about_unused_bindings then mode, pat, None
+           if not warn_about_unused_bindings then mode, expected_ty, None
            else
              let some_used = ref false in
              (* has one of the identifier of this pattern been used? *)
@@ -6394,16 +6396,16 @@ and type_let
                     )
                )
                (Typedtree.pat_bound_idents pat);
-             mode, pat, Some slot
+             mode, expected_ty, Some slot
          ))
       attrs_list
       pat_list
   in
   let exp_list =
     List.map2
-      (fun {pvb_expr=sexp; pvb_attributes; _} (mode, pat, slot) ->
+      (fun {pvb_expr=sexp; pvb_attributes; _} (mode, expected_ty, slot) ->
         if is_recursive then current_slot := slot;
-        match get_desc pat.pat_type with
+        match get_desc expected_ty with
         | Tpoly (ty, tl) ->
             if !Clflags.principal then begin_def ();
             let vars, ty' = instance_poly ~keep_names:true true tl ty in
@@ -6427,13 +6429,13 @@ and type_let
               Builtin_attributes.warning_scope pvb_attributes (fun () ->
                   if rec_flag = Recursive then
                     type_unpacks exp_env mode
-                      unpacks sexp (mk_expected pat.pat_type)
+                      unpacks sexp (mk_expected expected_ty)
                   else
                     type_expect exp_env mode
-                      sexp (mk_expected pat.pat_type))
+                      sexp (mk_expected expected_ty))
             in
             exp, None)
-      spat_sexp_list mode_pat_slot_list in
+      spat_sexp_list mode_typ_slot_list in
   current_slot := None;
   if is_recursive && not !rec_needed then begin
     let {pvb_pat; pvb_attributes} = List.hd spat_sexp_list in
@@ -6444,7 +6446,7 @@ and type_let
       )
   end;
   List.iter2
-    (fun (_,pat) (attrs, exp) ->
+    (fun (_,pat,_) (attrs, exp) ->
        Builtin_attributes.warning_scope ~ppwarning:false attrs
          (fun () ->
             ignore(check_partial env pat.pat_type pat.pat_loc
@@ -6456,13 +6458,13 @@ and type_let
   let pvs = List.map (fun pv -> { pv with pv_type = instance pv.pv_type}) pvs in
   end_def();
   List.iter2
-    (fun (_,pat) (exp, _) ->
+    (fun (_,pat,_) (exp, _) ->
        if maybe_expansive exp then
          lower_contravariant env pat.pat_type)
     pat_list exp_list;
   iter_pattern_variables_type generalize pvs;
   List.iter2
-    (fun (_,pat) (exp, vars) ->
+    (fun (_,_,expected_ty) (exp, vars) ->
        match vars with
        | None ->
          (* We generalize expressions even if they are not bound to a variable
@@ -6478,12 +6480,12 @@ and type_let
        | Some vars ->
            if maybe_expansive exp then
              lower_contravariant env exp.exp_type;
-           generalize_and_check_univars env "definition" exp pat.pat_type vars)
+           generalize_and_check_univars env "definition" exp expected_ty vars)
     pat_list exp_list;
   let l = List.combine pat_list exp_list in
   let l =
     List.map2
-      (fun ((_,p), (e, _)) pvb ->
+      (fun ((_,p,_), (e, _)) pvb ->
         {vb_pat=p; vb_expr=e; vb_attributes=pvb.pvb_attributes;
          vb_loc=pvb.pvb_loc;
         })