Improve the `type mismatch` message
When a type mismatch is met, Why3 only says type mismatch
. Could it be possible to print the two (fully qualified) types that do not match? That would be of immense help. I remember this has been also a long-standing beginner-repellent for OCaml. For example, I struggled for quite a long time before understanding my mistake in the following example, where I would have expected a message like type mismatch between Test.t and Ordering.t
.
module Ordering
type t = Eq | Lt | Gt
end
module PreOrder
type t
use Ordering
function cmp t t : Ordering.t
end
module Test
use int.Int
use Ordering
function cmp (x:int) (y:int) : Ordering.t =
if x < y then Lt else if x = y then Eq else Gt
clone PreOrder with
type t = int,
function cmp = cmp
end