Add support for `dyn Trait`

[Nadrieril]

I investigated a bit. The issue is that we need to handle ExistentialPredicate which isn't quite a TraitRef. If I understand, after https://github.com/AeneasVerif/charon/issues/127 we might be able to use a TraitRef there.

[sonmarcho]

What do you mean by "we might be able to use a TraitRef there?

[Nadrieril]

dyn Trait refers to a trait with an ExistentialPredicate, which seems to be a mapping from Self to a list of clauses. E.g. dyn Iterator<Item=u32> would be represented as lambda Self -> Self: Iterator, Self::Item = u8. If we do #127, I think this simplifies to just a list of trait clauses on Self, which we can represent as a list TraitRefs.

[sonmarcho]

I think a dyn trait really existentially quantifies a type, and we need to represent that: lambda Self -> Self: Iterator, Self::Item = u8 is a predicate over some type Self, but must itself be quantified. If you have a function fn foo(...) -> dyn Trait in Lean we would generate something of the shape:

def foo ... : exists T, Trait T

or, written with a dependent tuple (we return a pair of a type T and the fact that it satisfies Trait T):

def foo ... : (T:Type, Trait T)

[Nadrieril]

Yes, but with #127 the existentially quantified predicate will always be of the form lambda Self -> Self: Trait1, Self: Trait2, which we can represent as a list [Trait1, Trait2].

[Nadrieril]

By which I mean, the TypeKind::Dyn variant will contain Vec<TraitRef> instead of having to define a new ExistentialPredicate thing and having to deal with substitution.

[Nadrieril]

I was wrong about that: a TraitRef looks like T: Into<u64>, but what we need for dyn is just the Into<u64> part. In other words, it's a TraitRef where the Self argument is not supplied. In yet other words, it's an existentially quantified TraitRef.

[Nadrieril]

Partial support here: https://github.com/AeneasVerif/charon/pull/276. Needs more work to support fully.