Another work around is to give m an empty body in T, but that only works for (some) methods (not functions), so it's not satisfactory:

trait T {
  method {:extern} m() returns (res: int) {}
}

class C extends T {
  method n() returns (res: int)  {
    var v := m();
    return v;
  }
}

After looking at this with @RustanLeino and @fabiomadge , we came up with the following proposal:

Current rule: *When a class is checked to make sure that it overrides the definitions of each trait that it extends, it has to override any definition in the trait that does not have a body.

New rule: When a class is checked to make sure that it overrides the definitions (functions or methods) of each trait that it extends, it has to override any definition in the trait that

0. Does not have a body,
1. Does not have an :axiom attribute,
2. Does not have an :compile false attribute.

In other words, definitions with :axiom or :compile false in the trait are treated the same as definitions with bodies in the trait; in particular, they cannot have a body in the class.

With these rules, if a trait has a bodyless definition without an :axiom or :compile false attribute, then the class must redeclare that definition, and the redeclaration must either have a body or have the :axiom or :compile false attribute.

Note that :extern is not used to make that decision; that is because :extern "name" can be used to indicate the name under which a trait method should be exposed to the world — even for methods that are implemented in Dafny.

@txiang61 , could you check whether this proposal would fulfill your use case? Thanks!