Add support for mutually recursive trait declarations

[sonmarcho]

We need to add support for mutually recursive trait declarations in Aeneas. In the meantime, we should add a span to the error message.

[Nadrieril]

For example:

pub trait Trait1 {
    type T: Trait2;
}
pub trait Trait2: Trait1 {}

impl Trait1 for () {
    type T = ();
}
impl Trait2 for () {}

Even more to the point:

pub trait Trait {
    type T: Trait;
}
impl Trait for () {
    type T = ();
}

See also the rustc-internal docs on coinduction in the trait solver which could be related to this.

[sonmarcho]

Another (simply recursive) example of a different flavour, inspired by the mutual recursion between Iterator and IntoIterator:

pub trait Trait {
    fn f<T : Trait>(&self, other: &T);
}