suggested changes on #9309

unstaged.diff

diff --git a/typing/typecore.ml b/typing/typecore.ml
index c2cd2653e..d2bb6de46 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -1056,7 +1056,7 @@ and counter_example_checking_info = {
     of the original names.
  *)
 
-(** Due to GADT constraints, an or-pattern produced within
+(** Due to empty types and GADT constraints, an or-pattern produced within
     a counter-example may have ill-typed branches. Consider for example
 
       type _ tag = Int : int tag | Bool : bool tag
@@ -1105,13 +1105,14 @@ and splitting_mode =
 
      Instead of always splitting each or-pattern, It first attempts to
      find branches that do not introduce new constraints (because they
-     do not contain GADT constructors). Those branches are such that,
-     if they fail, all other branches will fail.
+     do not contain GADT constructors), and are not matching on an empty
+     type. Those branches are such that, if they fail, all other branches
+     will fail.
 
      If we find one such branch, we attempt to complete the subpattern
      (checking what's outside the or-pattern), ignoring other
-     branches -- we never consider another branch choice again. If all
-     branches are constrained, it falls back to splitting the
+     branches -- we never consider another branch choice again. If no
+     branch match these criteria, it falls back to splitting the
      or-pattern.
 
      We use this mode when checking exhaustivity of pattern matching.
@@ -1261,7 +1262,7 @@ and type_pat_aux
   and rvp k x = k (rp (pure category x))
   and rcp k x = k (rp (only_impure category x)) in
   let construction_not_used_in_counterexamples = (mode = Normal) in
-  let must_backtrack_on_gadt = match get_splitting_mode mode with
+  let must_backtrack_on_gadt_and_empty_type = match get_splitting_mode mode with
     | None -> false
     | Some Backtrack_or -> false
     | Some (Refine_or {inside_nonsplit_or}) -> inside_nonsplit_or
@@ -1289,7 +1290,8 @@ and type_pat_aux
               match explosion with
               | PE_single -> explosion_fuel - 1
               | PE_gadt_cases ->
-                  if must_backtrack_on_gadt then raise Need_backtrack;
+                  if must_backtrack_on_gadt_and_empty_type then
+                    raise Need_backtrack;
                   explosion_fuel - 5
             in
             let mode =
@@ -1437,7 +1439,7 @@ and type_pat_aux
           (mk_expected expected_ty)
           (Constructor.disambiguate Env.Pattern lid !env opath) candidates
       in
-      if constr.cstr_generalized && must_backtrack_on_gadt then
+      if constr.cstr_generalized && must_backtrack_on_gadt_and_empty_type then
         raise Need_backtrack;
       begin match no_existentials, constr.cstr_existentials with
       | None, _ | _, [] -> ()