Weird trait resolution issue with bounds

[xldenis]

When a function has explicit trait bounds it can interfere with trait resolution in weird ways, consider the following example:

trait X {
    #[logic]
    fn dummy(self);
}

impl<F> X for F {
    #[logic]
    fn dummy(self) {}
}

#[requires(f.dummy() == ())]
fn test<F, I>(f: F, i: I)
where
    F: X,
{
}

In the context of the requires we expect dummy to resolve to the impl provided above but it actually won't resolve at all. Rust reports it as being provided by the parameter because we have the F: X bound. If we remove that bound, then it will correctly select the right version of dummy. This may just be a case of rustc not optimizing for the same thing as creusot since coherence guarantees that this difference should disappear at monomorphization time.

I don't quite know what we can do to solve this (Chalk?).

Another example which motivated this bug hunt:

#[requires(forall<i : _> (*f).precondition(i))]
#[ensures(f.postcondition_mut((i,), result))]
fn test<F, I>(f : &mut F, i : I)
where F : FnMut(I),
{
    (f)(i)
}

[xldenis]

This is actually known and documented behavior of Rust, bounds are considered separate from impls and take precedence.