Method invocations of trait-bound generics need explicit upcasting

[amaurremi]

Summary

Dafny currently does not allow direct invocation of methods that are defined in a trait, if the invocation is on a generic type bound by that trait:

trait T {
  method foo()
}

method bar<U extends T>(t: U) {
  t.foo();
}

Compiling this code would yield the error member 'foo' does not exist in type parameter 'U'.

Background and Motivation

Even though U is a subtype of T, the compiler does not allow direct invocation of foo on t.

To work around this, we need an explicit cast:

method bar<U extends T>(t: U) {
  (t as T).foo();
}

This behavior is unintuitive and adds unnecessary verbosity.

Proposed Feature

Enhance Dafny's support for bounded polymorphism by allowing direct invocation of methods on trait-bound generics without requiring upcasting. For the example above, t.foo() should compile without errors.

Alternatives

Update the documentation to explain why explicit upcasting in this scenario is required. This would reduce confusion but not resolve the underlying issue of verbosity and usability.