In #13076 (comment) @ncik-roberts proposed two further testcases:

type nothing = |
type t = A | B | C of nothing
let f : bool * t -> int = function
  | true, A -> 3
  | false, A -> 4
  | _, B -> 5
  | _, C _ -> .

and

    type t =
      | A of int
      | B of string
      | C of string
      | D of string

    let compare t1 t2 =
      match t1, t2 with
      | A i, A j -> Int.compare i j
      | B l1, B l2 -> String.compare l1 l2
      | C l1, C l2 -> String.compare l1 l2
      | D l1, D l2 -> String.compare l1 l2
      | A _, (B _ | C _ | D _ ) -> -1
      | (B _ | C _ | D _ ), A _ -> 1
      | B _, (C _ | D _) -> -1
      | (C _ | D _), B _ -> 1
      | C _, D _ -> -1
      | D _, C _ -> 1

My checks seem to indicate that both examples indeed are pessimized in the current trunk, and this pessimization is fixed by the present PR. Good news! But I'm not sure why the second example is affected, as it does not rely on type-checker totality information. (For the first example: knowing that empty types and not inhabited requires type-checker information similar to GADTs.) I think that what is going on in the second example is related to the way or-pattern compilation discards some parts of the default environment, as discussed in details in #13076 (comment) .

Actually I notice a few things with polymorphic variants. These get Match_failure cases where they didn't before:

let f x y =
 match x, y with
 | _, `Y1 -> 0
 | `X1, `Y2 -> 1
 | (`X2 | `X3), `Y3 -> 2
 | `X1, `Y3
 | `X2, `Y2
 | `X3, _  -> 3


let check_results r1 r2 =
  match r1 r2 with
  | (Ok _ as r), _ | _, (Ok _ as r) -> r
  | (Error `A as r), Error _
  | Error _, (Error `A as r) -> r
  | (Error `B as r), Error `B -> r

I haven't looked into why yet (sorry, I'm timing out for the day soon).

Thanks for the polymorphic-variants examples. I haven't looked at the root cause either, but my guess would be that it is similar to the situation analyzed in details in #13076 (comment) : or-patterns trim the default environment (instead of growing the context with negative information), and there are a few cases where, before #13076, the pattern-matching compiler could locally detect that a sub-matrix is Total because its default environment becomes empty.

Thinking it, it may be possible to imitate this behavior now (with the global/current partiality split), by strengthening the current partiality into Total when the global partiality is also Total.

The fix I had in mind appears to work. I pushed your examples in the testsuite, and the fix. This is an addition to the previous fix (there are now two separate fixes for two separate code-quality regressions in #13076), so it would need a re-review.

Thanks! Merged.