check that no ambiguous pattern type escapes its scope earlier on.

This gives more stable error messages.

testsuite/tests/typing-gadts/ambiguity.ml

@@ -113,13 +113,13 @@ let f (type a b) (x : (a, b) eq) =
   | _, [(_ : a)] -> []
 ;;
 [%%expect{|
-Line _, characters 4-16:
-    | _, [(_ : a)] -> []
-      ^^^^^^^^^^^^
-Error: This pattern matches values of type (a, b) eq * a list
-       but a pattern was expected which matches values of type
-         (a, b) eq * b list
-       Type a is not compatible with type b
+Line _, characters 4-29:
+    | Refl, [(_ : a) | (_ : b)] -> []
+      ^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This pattern matches values of type (a, b) eq * b list
+       but a pattern was expected which matches values of type 'a
+       This instance of b is ambiguous:
+       it would escape the scope of its equation
 |}]
 
 let g1 (type a b) (x : (a, b) eq) =
@@ -128,10 +128,9 @@ let g1 (type a b) (x : (a, b) eq) =
   | _, [(_ : b)] -> []
 ;;
 [%%expect{|
-Line _, characters 2-77:
-  ..match x, [] with
+Line _, characters 4-29:
     | Refl, [(_ : a) | (_ : b)] -> []
-    | _, [(_ : b)] -> []
+      ^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This pattern matches values of type (a, b) eq * b list
        but a pattern was expected which matches values of type 'a
        This instance of b is ambiguous:
@@ -144,13 +143,13 @@ let g2 (type a b) (x : (a, b) eq) =
   | _, [(_ : a)] -> []
 ;;
 [%%expect{|
-Line _, characters 4-16:
-    | _, [(_ : a)] -> []
-      ^^^^^^^^^^^^
-Error: This pattern matches values of type (a, b) eq * a list
-       but a pattern was expected which matches values of type
-         (a, b) eq * b list
-       Type a is not compatible with type b
+Line _, characters 4-29:
+    | Refl, [(_ : b) | (_ : a)] -> []
+      ^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This pattern matches values of type (a, b) eq * b list
+       but a pattern was expected which matches values of type 'a
+       This instance of b is ambiguous:
+       it would escape the scope of its equation
 |}]
 
 let h1 (type a b) (x : (a, b) eq) =
@@ -163,9 +162,9 @@ Line _, characters 4-29:
     | Refl, [(_ : a) | (_ : b)] -> []
       ^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This pattern matches values of type (a, b) eq * b list
-       but a pattern was expected which matches values of type
-         (a, b) eq * a list
-       Type b is not compatible with type a
+       but a pattern was expected which matches values of type 'a
+       This instance of b is ambiguous:
+       it would escape the scope of its equation
 |}]
 
 let h2 (type a b) (x : (a, b) eq) =
@@ -174,10 +173,9 @@ let h2 (type a b) (x : (a, b) eq) =
   | Refl, [(_ : a) | (_ : b)] -> []
 ;;
 [%%expect{|
-Line _, characters 2-77:
-  ..match x, [] with
-    | _, [(_ : b)] -> []
+Line _, characters 4-29:
     | Refl, [(_ : a) | (_ : b)] -> []
+      ^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This pattern matches values of type (a, b) eq * b list
        but a pattern was expected which matches values of type 'a
        This instance of b is ambiguous:
@@ -194,7 +192,7 @@ Line _, characters 4-29:
     | Refl, [(_ : b) | (_ : a)] -> []
       ^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This pattern matches values of type (a, b) eq * b list
-       but a pattern was expected which matches values of type
-         (a, b) eq * a list
-       Type b is not compatible with type a
+       but a pattern was expected which matches values of type 'a
+       This instance of b is ambiguous:
+       it would escape the scope of its equation
 |}]

testsuite/tests/typing-gadts/pr7618.ml

@@ -19,15 +19,9 @@ let ok (type a b) (x : (a, b) eq) =
 ;;
 [%%expect{|
 type ('a, 'b) eq = Refl : ('a, 'a) eq
-Line _, characters 2-54:
-  ..match x, [] with
-    | Refl, [(_ : a) | (_ : b)] -> []
-Warning 8: this pattern-matching is not exhaustive.
-Here is an example of a case that is not matched:
-(Refl, _::_::_)
-Line _, characters 2-54:
-  ..match x, [] with
+Line _, characters 4-29:
     | Refl, [(_ : a) | (_ : b)] -> []
+      ^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This pattern matches values of type (a, b) eq * b list
        but a pattern was expected which matches values of type 'a
        This instance of b is ambiguous:
@@ -39,17 +33,9 @@ let fails (type a b) (x : (a, b) eq) =
   | Refl, [(_ : b) | (_ : a)] -> []
 ;;
 [%%expect{|
-Line _, characters 2-90:
-  ..match x, [] with
+Line _, characters 4-29:
     | Refl, [(_ : a) | (_ : b)] -> []
-    | Refl, [(_ : b) | (_ : a)] -> []
-Warning 8: this pattern-matching is not exhaustive.
-Here is an example of a case that is not matched:
-(Refl, _::_::_)
-Line _, characters 2-90:
-  ..match x, [] with
-    | Refl, [(_ : a) | (_ : b)] -> []
-    | Refl, [(_ : b) | (_ : a)] -> []
+      ^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This pattern matches values of type (a, b) eq * b list
        but a pattern was expected which matches values of type 'a
        This instance of b is ambiguous:

typing/ctype.ml

@@ -702,6 +702,27 @@ let rec normalize_package_path env p =
           normalize_package_path env (Path.Pdot (p1', s, n))
       | _ -> p
 
+let check_scope_escape level ty =
+  let rec aux ty =
+    let ty = repr ty in
+    if ty.level >= lowest_level then begin
+      ty.level <- pivot_level - ty.level;
+      begin match ty.scope with
+        Some lv ->
+        let var = newvar2 level in
+        if level < lv then raise (Unify [(ty,ty); (var, var)])
+      | None -> ()
+      end;
+      iter_type_expr aux ty
+    end
+  in
+  try
+    aux ty;
+    unmark_type ty
+  with Unify trace ->
+    let var = newvar2 level in
+    raise (Unify ((ty, ty) :: (var, var) :: trace))
+
 let update_scope scope ty =
   match scope with
   | None -> ()

typing/ctype.mli

@@ -109,6 +109,11 @@ val limited_generalize: type_expr -> type_expr -> unit
         (* Only generalize some part of the type
            Make the remaining of the type non-generalizable *)
 
+val check_scope_escape : int -> type_expr -> unit
+        (* [check_scope_escape lvl ty] ensures that [ty] could be raised
+           to the level [lvl] without any scope escape.
+           Raises [Unify] otherwise *)
+
 val instance: ?partial:bool -> type_expr -> type_expr
         (* Take an instance of a type scheme *)
         (* partial=None  -> normal

typing/typecore.ml

@@ -4536,6 +4536,10 @@ and type_statement ?explanation env sexp =
   end
 
 (* Typing of match cases *)
+and check_scope_escape loc env level ty =
+  try Ctype.check_scope_escape level ty
+  with Unify trace ->
+    raise(Error(loc, env, Pattern_type_clash(trace)))
 
 and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
   (* ty_arg is _fully_ generalized *)
@@ -4563,6 +4567,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
     | [{pc_lhs}] when is_var pc_lhs -> false
     | _ -> true
   in
+  let outer_level = get_current_level () in
   let init_env () =
     (* raise level for existentials *)
     begin_def ();
@@ -4617,6 +4622,8 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
             { pat with pat_type = instance pat.pat_type }
           end else pat
         in
+        (* Ensure that no ambivalent pattern type escapes its branch *)
+        check_scope_escape pat.pat_loc env outer_level ty_arg;
         (pat, ty_arg, (ext_env, unpacks)))
       caselist in
   (* Unify all cases (delayed to keep it order-free) *)
@@ -4717,8 +4724,6 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
     end_def ();
     (* Ensure that existential types do not escape *)
     unify_exp_types loc env (instance ty_res) (newvar ()) ;
-    (* Ensure that no ambivalent pattern type escapes its branch *)
-    unify_pat_types loc env ty_arg' (newvar ()) ;
   end;
   cases, partial