Bug: incorrect generics when implemented method has more specific signature

[Nadrieril]

While working on https://github.com/AeneasVerif/charon/pull/512, I discovered that there are two ways that an implemented method may have a different signature than expected from the trait:

• the implemented method fn<..> A -> B type (including late-bound vars) may be a subtype of that of the declared method;
• the implemented method may have less strict trait bounds.

trait Trait: Sized {
    fn method1(self, other: &'static u32);
    fn method2<T: Copy>(self, other: T); 
}

impl Trait for () {
    // This implementation is more general because it works for non-static refs.
    fn method1(self, _other: &u32) {}
    // This implementation is more general because it works for non-`Copy` `T`s.
    fn method2<T>(self, _other: T) {}
}

fn main() {
    let _ = ().method1(&1u32);
    // Error: we pass incorrect predicates
    // let _ = ().method2(false);
}

In both cases our translation is incorrect. Once https://github.com/AeneasVerif/charon/pull/512 lands we'll be able to fix this by using the method binders to convert between the trait-declared method generics and the actually-implemented method generics.

[Nadrieril]

https://github.com/hacspec/hax/pull/1215 fixes some of the first kind of error but not yet all. I left a hack that we'll be able to remove after #127.

[Nadrieril]

This happens in particular in the stdlib, for the Iterator::fold impl of slice::Iter.