Support multiple trait implementations for the same outer type

[jaybosamiya]

@utaal's note: originally reported as a bug by @jaybosamiya:

---

Previous discussion on traits here: #73

---

Consider:

use vstd::prelude::*;

verus! {

    trait Foo {
        spec fn foo(&self) -> bool;
    }

    impl Foo for Option<u8> {
        spec fn foo(&self) -> bool { true }
    }

    impl Foo for Option<u64> {
        spec fn foo(&self) -> bool { false }
    }

}

fn main() {}

We get (at least on latest main_new c81e6dc, I haven't tested on other branches):

$ rust-verify.sh a.rs
error: not supported: multiple definitions of same function
  --> a.rs:14:14
   |
10 |         spec fn foo(&self) -> bool { true }
   |              ---------------------
...
14 |         spec fn foo(&self) -> bool { false }
   |              ^^^^^^^^^^^^^^^^^^^^^

error: aborting due to previous error

My guess is that it is keying based on the Option rather than on the specific types Option<u8> and Option<u64>?

[utaal]

Unfortunately, this is a currently known limitation, and the fix requires a partial redesign of some of the encoding (with fairly far-reaching implications). We have candidate designs, but it will take some time before we get around to it.

I'm going to consider this a "feature request" at this stage, and turn it into a discussion.

[jaybosamiya]

Personally I don't see how this is a feature request when this breaks a fairly important usage of traits (to the point where Verus is actually lying about there being multiple definitions, when there aren't). If this is a known limitation, then either it should have a better error message when it is hit, or should be fixed (just because it might take time to get around to it and requires redesigning things doesn't make it a non-bug is all I'm saying)

Anyways, I defer to you in deciding what to do with it.

[utaal]

You're welcome to go ahead and improve the error message in the meantime. We are catching up, but there are still many situations where the error messages are suboptimal (and adding a precise error for all these can also result in a bunch of complexity if not done carefully). I've added this to the tracking discussion for suboptimal or confusing error messages: #387 (comment)

[tjhance]

This came up recently when I brought up the possibility of using the same AIR type to represent both slices and arrays. utaal pointed out that, because of this existing limitation, it wouldn't be possible to do this while also allowing us to implement traits on them. I think there are workarounds there, but we have to be careful about it.

The limitation also makes it hard to support size_of::<T> as elegantly as I'd like to, since size_of::<T>() needs to be different from size_of::<&T>() or size_of::<Box<T>>(). Or size_of::<u8>() is different than size_of::<u32>() (and so on).

[tjhance]

What are the candidate designs, by the way?

Right now the only idea I see is to do it similar to coq encoding of type classes: make AIR objects for trait implementations, and pass them as arguments to generic functions, rather than just passing arguments representing the types.

[utaal]

I don't have all that state in mind right now, but IIRC we were thinking it is mostly a naming issue: we need to be able to encode all of those different implementations as separate functions with distinct names (and currently function names are based on the path of Self). Generic functions with trait bounds would still just see the trait definition, not a concrete implementation.

make AIR objects for trait implementations, and pass them as arguments to generic functions, rather than just passing arguments representing the types.

I don't yet understand where this is useful, which may mean that I'm not seeing part of the problem yet.

[utaal-b]

This is now supported:

use vstd::prelude::*;

verus! {
    trait Foo {
        spec fn foo(&self) -> bool;
    }

    impl Foo for Option<u8> {
        spec fn foo(&self) -> bool { true }
    }

    impl Foo for Option<u64> {
        spec fn foo(&self) -> bool { false }
    }

    fn main() {
        let a: Option<u8> = None;
        let b: Option<u64> = None;
        
        assert(a.foo());
        assert(!b.foo());
    }
}