Cannot automatically convert ghost types

[witemap]

The following spec causes Gobra to crash:

ensures forall e int :: e in s1 ==> e in s2
pure func test(ghost s1 set[int]) (ghost s2 set[any])

The exception reported is:

An exception occurred during execution of Gobra: java.util.concurrent.ExecutionException: java.lang.AssertionError: assertion failed: Expected second operand e_V1@119@00 to be of sort Tuple2[Ref, Types], but found Int.

The same also happens if we use mset instead of set. As @jcp19 explains, this is likely due to a lack of an automatic type conversion due to different encodings of int and interface types at the Viper level.

The same problem does NOT happen if we compare the values of elements of sequences. E.g.

ensures len(s1) == len(s2)
ensures forall idx int :: (0 <= idx && idx < len(s1)) ==> s1[idx] == s2[idx]
pure func test(ghost s1 seq[int]) (ghost s2 seq[any])

works fine.