Fixes: Rust supports overriding traits

[MikaelMayer]

Description

The PR #5940 defined a preliminary support for value traits.
This PR fixes everything that encompasses value traits and newtypes. Here is the list of fixes.

• Fix to support functions declared in a trait and implemented in another trait
• Fix to support for equality in type parameters and conditional equality support for datatypes.
• Fix to support constants in datatypes
• Fix to support constants in traits
• Fix to support back/forth conversions between &self and the underlying type
• Fix to ensure we don't support coercions where it's not possible (that caused compilation errors for Rust and it's behind the discovery of soundness issue Soundness issue: Map's range not inferred to require equality for datatype to support equality #5972)
• Fix support of equality for newtypes (that caused compilation errors for Rust and it's behind the discovery of soundness issue General newtypes not supporting equality in a sound way #5978)
• Fix to support type bounds in type parameters
• Fix to support newtypes on booleans
• Fix to support correct borrowing of type arguments in methods when the method instantiate a trait method which always borrows the arguments with the type parameter
• Fix to support static constants in datatypes, including type parameters
• Fix to support type parameters in static functions
• Fix to ensure type parameter equality is correctly generated
• Fix to support downcast from one value trait to another value trait of the same hierarchy (needed to change the resolver to record all such traits)
• Fix to support the enclosing module name in externs

Also some enhancements

• Unification of extern semantics: Remove the error message about {:extern} on types requiring a hint when it can simply take the Dafny name, like for modules and classes.
• DafnyCodeGenerator.GenType now caches its result to avoid exponential computations

I also updated the documentation regarding the use of externs

How has this been tested?

• All the tests of comp/rust/traits-datatypes.dfy and comp/rust/small/* were not passing before this PR, and now they are.
• The way to downcast traits from one to the other is tested in the test/mod.rs of the runtime.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[ssomayyajula]

Some high level comments:

I'm mainly just concerned about the soundness and implementation of trait downcasting. It looks like you do this in phases:

• At resolution time, determine the parents of a trait declaration
• In Dafny code generator, compute for which parents the subtype relation works both ways

I don't understand why the latter can't be done earlier - is there not a subtype check method in the type system refresh?

[MikaelMayer]

Thank you very much for reading the PR and trying to understand the underlying logic. That's already a lot of work.

• In Dafny code generator, compute for which parents the subtype relation works both ways

I don't understand why the latter can't be done earlier - is there not a subtype check method in the type system refresh?

You're right that there is an issue here. The problem is that in other backends, it's fine to do something like this:

trait X {}
trait Y<T> extends X {}
var x: X;
if x is Y<int> {
}

This is because other back-ends keep run-time information of the type and types are behind single references.
However, in Rust, unless we do a deeper embedding, traits are only represented as the fat part of a pointer that points the vtable for that trait.
Therefore, it is not possible to check at run-time if x is Y<int> like that. More precisely, the only thing we know from a x: X is a pointer to the data and all the methods of X, plus possibly other internal methods.
The only way to know what the type at run-time is is through the trait Any, that Dafny traits extend. However, there could be two traits implementations for concrete types in two separate modules, so traits are not inherently attached to concrete types like they are in Dafny.

The only sensible way to do trait downcast is to add special methods to the trait X {} so that we can test if it's a Y {} for some T. However, again, because of monomorphization, Rust prevents type parameters on functions that are in a trait with a function. Hence, the only way to do a downcast test and instantiation is if the type parameters of the subtrait can be obtained from the type parameters of X. This is what I am computing in CanDowncast().

This means indeed that users who try to downcast X to Y<int> will get a compiler error, but I do not consider this as a soundness issue, more a kind of unsupported issue. Still, let me document that if that would alleviate your concern.

One problem with doing it earlier is that the subtype check depends on whether the instantiated type parameters support

[ssomayyajula]

I see, you add the coercion methods at code generation time, which is why CanDowncast happens so "late" in the process

Approved

[ssomayyajula]

What if the child trait contains abstract members not in the parent trait?

[MikaelMayer]

That's ok, because if the underlying struct declares it can be downcasted to the trait by implementing the Downcast trait itself and returning true to the method _is, it also has to return an instance of the child trait in the method _as, and because it has nothing else than itself to return, it also needs to implement the abstract methods of the child, so at the end it's sound.
The structs that don't implement the child trait will return false on _is and panic on _as.

[ssomayyajula]

Nitpick, but InferEqualitySupport would be easier to read in functional style (you wouldn't have to exit a doubly-nested loop). No changes needed.

[ssomayyajula]

OK: now I see the connection to the population of the new field in TraitDecl. Why can't this computation be done at that time?

[ssomayyajula]

Is there not an existing mechanism to do a subtype check on two types/traits?

[MikaelMayer]

For your first question:
This method has the side-effect of not just checking if the traits can be downcasted, but also given a type of the parent trait (with instantiated type arguments), it gives the type of the sub-trait (with instantiated arguments using the type parameters of the parent trait). This can't be done at the time of gathering trait dependencies because type parameters are not known. We could, however and at resolution time, determine if that construction is possible and store a function that, given the instantiated type of the parent, returns the instantiated type for each sub-trait that is possible, using a map.
Would you prefer me to do this instead?

For your second question
For Rust (the main consumer of the DafnyCodeGenerator now), references have a virtual dispatch table pointer if they represent a trait. Since everything must be known at compile-time, the comment of CanDowncast explains exactly what is necessary for us to be able to even mention that a trait is downcastable to another trait; that is, they need to share type arguments so that the type of the sub-trait must be expressible with the arguments of the upper trait. That's a slight restriction, and I should probably move it to a resolution error if we know that the target compiler is Rust.
In practice, this restriction has been satisfied in the large scale projects that I was helping translate to Rust, that is, there is usually no downcast by adding a type parameter that was not present in the parent trait.
Would you prefer that than having a resolution error instead as described?

[ssomayyajula]

Yeah, I think I would prefer to have that (1) / a function that returns a delayed computation on the parent's concrete type into the concrete type for each child trait if it's not too difficult.

OTOH for (2) I think what you're doing currently is fine. Special casing the resolver depending on the backend seems morally incorrect

[MikaelMayer]

That's ok, because if the underlying struct declares it can be downcasted to the trait by implementing the Downcast trait itself and returning true to the method _is, it also has to return an instance of the child trait in the method _as, and because it has nothing else than itself to return, it also needs to implement the abstract methods of the child, so at the end it's sound.
The structs that don't implement the child trait will return false on _is and panic on _as.