Falsely(?) triggered warning 56 [unreachable-case] starting with 5.3.0~beta1

[tleedjarv]

Trying out 5.3.0~beta1 with Unison, I see the following warning. This warning is not present with versions up to and including 5.3.0~alpha1.

ocamlopt -g -I lwt -I ubase -I system -I +unix -I +str -I system/generic -I lwt/generic -c copy.ml
File "/home/runner/work/unison/unison/src/copy.ml", line 218, characters 37-88:
218 |                                    | TransferNeedsDoubleCheckAgainstCurrentSource (a, b) -> I32 (a, b)
                                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 56 [unreachable-case]: this match case is unreachable.
Consider replacing it with a refutation case '<pat> -> .'

The source: https://github.com/bcpierce00/unison/blob/96e15a800bb0e619da6f7092ddefc47101c3092f/src/copy.ml#L202-L224

[Octachron]

A simpler example to reproduce the bug:

module NI = struct
  type _ ni
end open NI

type 'a cstr = { desc: 'a } constraint 'a = _ ni
type x = int ni cstr

type ab =
  | A of x
  | B of x

let test: ab -> (x,x) Either.t  = function
   | B a -> Left a
   | A a -> Right a

[yallop]

It's a soundness bug, of course:

bug.ml:

module NI : sig type _ ni val v : int ni end = struct
  type _ ni = int
  let v = 0
end open NI

type 'a cstr = { desc: 'a } constraint 'a = _ ni
type x = int ni cstr

type ab =
  | A of x
  | B of x * string

let test: ab -> x list * string = function
   | B (a,b) -> [a], b
   | A _ -> .
let () = print_endline (snd (test (A {desc=v})))

$ ocaml bug.ml 
Segmentation fault

[gasche]

I wonder if this issue is fixed by #13510.

[gasche]

Answer: nope, I can still reproduce the issue on top of #13510.

[garrigue]

Looking at the typechecker code, it looks like the culprit is expand_abbrev.
Indeed, it does unification for constraints in expression mode, even when it is called from unification in pattern mode.
It would be interesting to find a counter-example in 5.2