Contract targets that omit defaulted generic parameters fail to resolve #4914

Requested feature:

Fill omitted trailing generic parameters that have declared defaults during type resolution. resolve_ty's instantiate_path_args (added in #4865) resolves explicitly written type arguments, but returns the uninstantiated identity type on a count mismatch, so a path that omits a trailing parameter with a declared default fails to resolve. Filling the omitted parameter from its declared default, instantiated with the arguments so far (what rustc does), would resolve these.

Use case:

Writing proof_for_contract harnesses for standard-library methods whose natural spelling omits a defaulted parameter. Challenge 24 (model-checking/verify-rust-std#689) names <std::vec::IntoIter<u8> as Iterator>::__iterator_get_unchecked. IntoIter<T, A = Global> omits the allocator, so on the #4865 branch it resolves only with the allocator written out (IntoIter<u8, std::alloc::Global>, which needs #![feature(allocator_api)]). Filling the default lets the natural spelling resolve.

Test case:

Save as min_defaults.rs (self-contained, no standard library):

// `Pair<T, U = T>` at `Pair<u8>` should fill `U = u8`.
struct Pair<T, U = T>(T, U);

trait Probe {
    fn probe(&self) -> u32;
}

impl Probe for Pair<u8> {
    #[kani::ensures(|r| *r == 0)]
    fn probe(&self) -> u32 {
        0
    }
}

#[kani::proof_for_contract(<Pair<u8> as Probe>::probe)]
fn check() {
    let p = Pair(0u8, 0u8);
    let _ = p.probe();
}

Run with:

kani min_defaults.rs -Z function-contracts

Kani 0.68.0 fails to resolve (location lines elided):

error: failed to resolve `<Pair < u8 > as Probe>::probe`: unable to find implementation of associated function `Probe::probe` for Pair<T, U>
   = note: Kani does not currently support stubs or function contracts on generic functions in traits.
            See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.

for Pair<T, U> is the uninstantiated identity type: the omitted U leaves the parameter count short. On 0.68.0 this is the general #1997 failure; with #4865 it is the residual, since explicit arguments resolve while the omitted default does not. With the fill, Pair<u8> fills U = u8 and verifies. Only declared defaults are filled, so NoDefault<u8> (for NoDefault<T, U>) still fails.

Scope: type parameters only. A const parameter, or any argument that cannot be resolved, keeps the uninstantiated type.