Treat empty variants as GADTs for exhaustiveness check

Changes

@@ -210,6 +210,10 @@ Working version
 
 ### Bug fixes:
 
+- #9309: Treat the empty variant as a GADT in or-patterns, so that the
+  exhaustiveness check will examine all cases in the or pattern.
+  (Stefan Muenzel, report by Robert Head, review by ????)
+
 - #7683, #1499: Fixes one case where the evaluation order in native-code
   may not match the one in bytecode.
   (Nicolás Ojeda Bär, report by Pierre Chambart, review by Gabriel Scherer)

testsuite/tests/typing-misc/empty_variant.ml

@@ -55,5 +55,11 @@ let f () =
 type nothing = |
 type ('a, 'b, 'c) t = A of 'a | B of 'b | C of 'c
 module Runner : sig val ac : f:((unit, 'a, unit) t -> unit) -> unit end
+Lines 16-17, characters 8-18:
+16 | ........match abc with
+17 |         | A _ -> 1
+Warning 8: this pattern-matching is not exhaustive.
+Here is an example of a case that is not matched:
+C ()
 val f : unit -> unit = <fun>
 |}]

typing/typecore.ml

@@ -1282,7 +1282,9 @@ and type_pat_aux
       | Counter_example ({explosion_fuel; _} as info) ->
          let open Parmatch in
          begin match ppat_of_type !env expected_ty with
-         | PT_empty -> raise (Error (loc, !env, Empty_pattern))
+         | PT_empty ->
+            if must_backtrack_on_gadt then raise Need_backtrack;
+            raise (Error (loc, !env, Empty_pattern))
          | PT_any -> k' Tpat_any
          | PT_pattern (explosion, sp, constrs, labels) ->
             let explosion_fuel =