Invalid extraction of disjunction patterns
The extraction of the following program to OCaml contains a type error: cat pattern.mlw
module Pattern
type s = A
type t = B | C
let f x =
match x with
| A, (B | C) -> ()
end
end
In fact, the parentheses around the disjunction seem to be lost on the way, or different associativity is assumed with respect to the comma: why3 extract -D ocaml64 -o pattern.ml pattern.mlw
type s =
| A
type t =
| B
| C
let f (x: s * t) : unit = let (A, B | C) = x in ()
OCaml surely complains: ocamlc pattern.ml
File "pattern.ml", line 8, characters 38-39:
Error: This pattern matches values of type t
but a pattern was expected which matches values of type s * t