Bad pattern-matching analysis for tuple

[n-osborne]

$ cat > foo.mli << EOF
> (*@ type m = A of unit | B of (unit * unit) *)
> 
> type t
> (*@ mutable model m : m *)
> 
> val f : t -> bool
> (*@ b = f t
>     ensures match t.m with | A _ -> true | B _ -> false *)
> EOF
$ gospel check foo.mli
File "foo.mli", line 8, characters 12-55:
8 |     ensures match t.m with | A _ -> true | B _ -> false *)
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The pattern-matching is redundant.
       Here is a case that is unused:
         B _.

The error message is confusing and this is syntax that OCaml compiler accepts.