Need information about subtraits in trait declarations

[sweirich]

If the rust code includes a trait inheritance

trait A {
    fn a(&self) -> u32;
}
trait B : A {
    fn b(&self) -> u32;
}

then mir-verifier needs to know that B is a subtrait of A.

The reason is that any constraint that mentions B

fn g<T>(x : T) -> u32 where T : B {
    x.a()
}

needs to also imply that a's methods are also available.

[sweirich]

A workaround is to write g as

fn g<T>(x : T) -> u32 where T : A + B {
    x.a()
}

so that the generated constraints include this information.

[atomb]

Commit ed9ea836f adds a supertraits field to each element of the traits list. It always includes the trait being defined as the first entry and any supertraits as later entries.