Improve trait resolution

[Nadrieril]

This continues my work in cleaning up trait resolution. Of particular importance is the clarification of "required" vs "implied" predicates: required predicates must be proven to mention an item (e.g. one must prove T: Sized to mention Option<T>) whereas implied predicates are implied by the item being present in a signature (e.g. T: Copy implies T: Clone).

So far we consider all predicates on a trait declaration to be implied, but that's not what rustc does. For example:

trait Foo<T: Clone>: ToString {}

Here (according to rustc) T: Clone is required to mention Foo, and Self: ToString is implied by Self: Foo. I don't know if considering T: Clone as implied (like we implicitly did today) could cause problems but at least now what's happening is clear.

[W95Psp]

Thanks! So if I understand correctly, while this notion of implied VS required predicates was sort of existing implicitly in hax, this PR makes them very explicit and clear, particularly with the traits::utils::implied_predicates and traits::utils::required_predicates?
That sounds pretty nice, and that makes the API of traits more clear!

The rest looks good to me, let's merge!

[Nadrieril]

Yep, this was implicit previously, for example we don't store impl exprs when we refer to a trait, but if we decided to represent required predicates for traits we'd have to do that.