Remove propagation from previous branches (#9811)

Changes

@@ -22,6 +22,15 @@ Working version
   (GitHub user @EduardoRFS, review by Xavier Leroy, Nicolás Ojeda Bär
    and Anil Madhavapeddy, additional testing by Michael Schmidt)
 
+### Type system:
+
+* #9811: remove propagation from previous branches
+  Type information inferred from previous branches was propagated in
+  non-principal mode. Revert this for better compatibility with
+  -principal mode.
+  For the time being, infringing code should result in a principality warning.
+  (Jacques Garrigue, review by Thomas Refis and Gabriel Scherer)
+
 ### Runtime system:
 
 - #9756: garbage collector colors change

testsuite/tests/typing-gadts/didier.ml

@@ -47,6 +47,13 @@ let f (type t) (x : t) (tag : t ty) =
   | Bool -> x
 ;;
 [%%expect{|
+Lines 2-4, characters 2-13:
+2 | ..match tag with
+3 |   | Int -> x > 0
+4 |   | Bool -> x
+Warning 18 [not-principal]:
+  The return type of this pattern-matching is ambiguous.
+  Please add a type annotation, as the choice of `bool' is not principal.
 val f : 't -> 't ty -> bool = <fun>
 |}, Principal{|
 Line 4, characters 12-13:

testsuite/tests/typing-gadts/test.ml

@@ -361,6 +361,13 @@ module Propagation = struct
 end
 ;;
 [%%expect{|
+Lines 11-13, characters 12-20:
+11 | ............match x with
+12 |     | IntLit n -> (n : s )
+13 |     | BoolLit b -> b
+Warning 18 [not-principal]:
+  The return type of this pattern-matching is ambiguous.
+  Please add a type annotation, as the choice of `s' is not principal.
 module Propagation :
   sig
     type _ t = IntLit : int -> int t | BoolLit : bool -> bool t

typing/typecore.ml

@@ -133,6 +133,18 @@ type error =
 exception Error of Location.t * Env.t * error
 exception Error_forward of Location.error
 
+let trace_of_error = function
+    Label_mismatch (_,tr)
+  | Pattern_type_clash (tr,_)
+  | Or_pattern_type_clash (_,tr)
+  | Expr_type_clash (tr,_,_)
+  | Coercion_failure (_,_,tr,_)
+  | Less_general (_,tr)
+  | Letop_type_clash (_,tr)
+  | Andop_type_clash (_,tr)
+  | Bindings_type_clash tr -> Some tr
+  | _ -> None
+
 (* Forward declaration, to be filled in by Typemod.type_module *)
 
 let type_module =
@@ -4687,7 +4699,7 @@ and type_cases
   ) half_typed_cases;
   (* type bodies *)
   let in_function = if List.length caselist = 1 then in_function else None in
-  let cases =
+  let mk_cases interbranch_propagation =
     List.map
       (fun { typed_pat = pat; branch_env = ext_env; pat_vars = pvs; unpacks;
              untyped_case = {pc_lhs = _; pc_guard; pc_rhs};
@@ -4715,8 +4727,7 @@ and type_cases
             end_def ();
             generalize_structure ty; ty
           end
-          else if contains_gadt then
-            (* allow propagation from preceding branches *)
+          else if contains_gadt && interbranch_propagation then
             correct_levels ty_res
           else ty_res in
         let guard =
@@ -4738,6 +4749,31 @@ and type_cases
       )
       half_typed_cases
   in
+  let cases =
+    let may_backtrack = does_contain_gadt && not !Clflags.principal in
+    if not may_backtrack then mk_cases false else
+    let snap = Btype.snapshot () in
+    let has_equation_escape err =
+      match trace_of_error err with
+        Some tr ->
+          List.exists Ctype.Unification_trace.
+            (function Escape {kind=Equation _} -> true | _ -> false) tr
+      | None -> false
+    in
+    try mk_cases false
+    with Error(_,_,err) when has_equation_escape err ->
+      Btype.backtrack snap;
+      let cases = mk_cases true in
+      let msg =
+        Format.asprintf
+          "@[<v2>@ @[<hov>The return type of this pattern-matching \
+           is ambiguous.@ \
+           Please add a type annotation,@ as the choice of `@[%a@]'@]@]"
+          Printtyp.type_expr ty_res
+      in
+      Location.prerr_warning loc (Warnings.Not_principal msg);
+      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