Stubbing non-overridden default trait methods fails with type mismatch

[feliperodri]

When a trait defines a default method and the implementing type does not override it, attempting to stub that method via #[kani::stub(<Type as Trait>::default_method, stub_fn)] fails during stub validation with a type mismatch error.

Steps to reproduce

trait HasDefault {
    fn default_method(&self) -> u32 {
        0
    }
}

struct MyType;
impl HasDefault for MyType {}

fn stub_default(_x: &MyType) -> u32 { 42 }

#[kani::proof]
#[kani::stub(<MyType as HasDefault>::default_method, stub_default)]
fn check() {
    let x = MyType;
    assert_eq!(x.default_method(), 42);
}

Expected behavior

The stub replaces MyType's inherited default_method with stub_default.

Actual behavior

Compilation fails with a type mismatch error. The default method body uses Self as a placeholder type rather than the concrete implementing type (MyType), causing stub signature validation to fail.

Root cause

When a trait method has a default implementation and the impl block does not override it, Instance::resolve returns the trait's own default body, which uses Self as the receiver type. Kani's stub validation then compares the stub signature (&MyType) against the default body signature (&Self), which don't match.

Workaround

Override the default method in the impl block (even if the body is identical):

impl HasDefault for MyType {
    fn default_method(&self) -> u32 {
        0 // same as default
    }
}

This gives the method a concrete &MyType receiver, allowing stub validation to succeed.