Unexpected inconsistency with (<>)
I stumbled across the following unexpected inconsistency in why3's handling of <>
.
The following program compiles:
type option 'a = Some 'a | None
let rec ghost function f (x y : option int) = x <> y
However, this one does not:
use int.Int
type option 'a = Some 'a | None
let rec ghost function f (x y : option int) = x <> y
Stating,
File "test.mlw", line 5, characters 46-47:
This expression has type Top.option int, but is expected to have type int
I believe this is due to how <>
is treated literally as not (a = b)
and since int.Int
furnishes a =
symbol this is used in the expansion, however its strange that if that module is not imported then we get the polymorphic mathematical equality instead.