Confusing error when checking trait impl against trait

[enjhnsn2]

When I try to check the following trait implementation (here):

    #[flux_rs::sig(
        fn(self: &strg Self, _) -> Option<_> ensures self: Self
    )]
    fn remove_first_matching<F>(&mut self, f: F) -> Option<T>
    where
        F: Fn(&T) -> bool,
    {...}

against the trait spec (here):

    #[flux_rs::sig(
        fn(self: &strg Self, _) -> Option<_> ensures self: Self
    )]
    fn remove_first_matching<F>(&mut self, f: F) -> Option<T>
    where
        F: Fn(&T) -> bool;

it fails with the error:

error[E0999]: internal flux error: crates/flux-infer/src/infer.rs:533:22
   --> kernel/src/collections/ring_buffer.rs:181:5
    |
181 | /     fn remove_first_matching<F>(&mut self, f: F) -> Option<T>
182 | |     where
183 | |         F: Fn(&T) -> bool,
    | |__________________________^
    |
    = note: incompatible types: `&'_ strg <self: RingBuffer<'_, λb0. T[b0]>[RingBuffer { a0, a1, a2 }]>` - `&'_ strg <?0e#8242: ∃b0. RingBuffer<'_, λb1. T[b1]>[b0]>`

I'm a little confused because the spec is token-for-token identical in both the trait and implementation, and only asserts that we need a &strg Self.

I also get a similar error when there is no spec on the trait at all. I don't fully understand the implementation for trait_impl checking, so I'm not sure if this is expected or not.

Any guidance?

[nilehmann]

The check is not implemented at all when strong references are involved so it just crashes.

Do you need the &strg? isn't the mut ref unfolding we implemented enough for this use case? I would like to know why not.

In any case, @ranjitjhala maybe you can take care of finishing the work on trait impl checking to consider strong references.

@enjhnsn2 in the mean time you can use #[flux::trusted_impl]

[enjhnsn2]

As requested, another implementation

    #[flux_rs::sig(
        fn(self: &strg RingBuffer<T>[@old]) ensures self: RingBuffer<T>[old.ring_len, 0, 0]
    )]
    fn empty(&mut self) {
        self.head = 0;
        self.tail = 0;
    }

and trait method

    /// Remove all elements from the ring buffer.
    fn empty(&mut self);

where the implementation has a non-trivial ensures clause.

[nilehmann]

@ranjitjhala your PR doesn't consider this case. We need the unfold_local_ptrs hack to handle this. I think it shouldn't be too hard to reuse it, right?

Also, I always thought that if you have an &mut in the trait definition you would never be able to make it an &strg in the impl, but now that we've implemented the check I see that in certain situations you can. In particular, if the trait definition is completely unrefined you can turn an &mut into an &strg as long as you don't put extra constraints in the input at the implementation. I'm quite happy about that.

[ranjitjhala]

on it!

[ranjitjhala]

I updated the PR to handle the above (I think!) can you lmk if it works now @enjhnsn2 (and of course reopen if not!)