trait A {
fn to_boxed_b(self: Box<Self>) -> Box<B> where Self: 'static;
}
impl<T> A for T {
fn to_boxed_b(self: Box<Self>) -> Box<B> where Self: 'static {
Box::new(*self) as _
}
}
trait B {}
impl<T: A> B for T {}
fn boxed_a() -> Box<A> { unimplemented!() }
fn main() {
boxed_a().to_boxed_b();
}

This doesn't:

trait A {
fn to_boxed_b(self: Box<Self>) -> Box<B> where Self: 'static {
Box::new(*self) as _
}
}
trait B {}
impl<T: A> B for T {}
fn boxed_a() -> Box<A> { unimplemented!() }
fn main() {
boxed_a().to_boxed_b();
}

I've tried many variations. Is there any way to make the default fn work? If not, why not?

The difference is the bounds on T. In the first example, Self is the generic parameter T which thus defaults to T: Sized. This is necessary for the implementation to be valid.

In the second example example, since it is the body of a trait, we have a default of Self: ?Sized and the implementation fails. In other words, the current bounds on Self are too general for it to work.

If you try adding a where Self: Sized bound to A::to_boxed_b (as you've probably tried), the default impl now compiles (hooray!), but the call to to_boxed_b() fails (booo!). This is because, at the callsite, Self is the trait object A, which isn't Sized.

Thinking in terms of "types as proofs", I feel like this comes down to a disconnect between the proofs we provide to the type system, and what we obtain back from it.

Consider:

T: Trait as the proposition that T implements Trait

impl Trait for T as providing a proof that T implements Trait.

In this language, there is one very special proof we never need to write, which is the fact that Trait: Trait (the one on the left being the trait object type). The compiler does this for us, and that's what lets the first example work.

This comes down to how fat pointers are implemented. Or rather, how type erasure is done. If you have an erased type Box<Trait> you cannot go to Box<AnotherTrait> since there’s no way to find the vtbl for that underlying object’s AnotherTrait impl. Once you add Sized bound then you’re working with thin pointers and those aren’t type erased.