Fill omitted defaulted generic parameters during type resolution

[kasimte]

A proof_for_contract target that omits a trailing generic parameter with a declared default failed to resolve with MissingTraitImpl. For example <Vec<u8> as Trait>::m, or the natural spelling of <vec::IntoIter<u8> as Iterator>::__iterator_get_unchecked, a target in the Challenge 24 submission (model-checking/verify-rust-std#689); both omit the allocator parameter. The parameter-count check kept the uninstantiated type instead of filling the default.

This PR fills an omitted trailing parameter from its declared default, instantiated with the arguments so far, matching what rustc does for omitted arguments. The logic lives in default_type_arg, called from instantiate_path_args's substitution loop.

A path written with no generic arguments at all (a bare Wrapper for struct Wrapper<T = u8>) is treated as an empty argument list, so an all-defaulted type resolves too. Parenthesized arguments keep the uninstantiated type.

Verification

test (-Zfunction-contracts)	expect
tests/kani/FunctionContracts/generic_default_argument_fill.rs	5 targets verify. A std container default (Vec<u8> fills A = Global); a sibling impl with a distinct postcondition (Vec<u16>), so each harness only verifies if resolution picks its own impl; a default referencing an earlier parameter (Pair<T, U = T> at Pair<u8> fills U = u8); the explicit spelling (Vec<u16, std::alloc::Global>) unchanged; and an all-defaulted type written with no argument list (AllDefault for struct AllDefault<T = u8>) fills T = u8.
tests/expected/function-contract/generic_default_missing_required.rs	still fails MissingTraitImpl (expected-output test; this diagnostic is the pass). NoDefault<u8> omits a parameter with no default, so only declared defaults are filled.
tests/expected/function-contract/generic_default_missing_bare.rs	still fails MissingTraitImpl (expected-output test; this diagnostic is the pass). NoDefaultBare written with no argument list omits a parameter with no default, so the no-arguments path still keeps the uninstantiated type.
tests/expected/function-contract/generic_default_const_param.rs	still fails MissingTraitImpl (expected-output test; this diagnostic is the pass). WithConst<u8> omits a defaulted const parameter; only defaulted type parameters are filled, so the const default is not filled and the target keeps the uninstantiated type.

The four original targets were confirmed locally when this PR was first submitted (generic_default_argument_fill 4/4, the two negatives failing MissingTraitImpl, resolver suites unchanged at generic_argument_instantiation 6, cross_module_multiple_impls 7, multiple_inherent_impls 3). This revision adds the no-arguments case (check_all_parameters_defaulted) and the generic_default_missing_bare negative; CI runs the full suite on the pinned toolchain.

Scope: type parameters only. A const parameter (with or without a default), and any argument that cannot be resolved, keep the uninstantiated type, as before. Defaults are instantiated structurally (no normalization), matching how resolve_ty already hands tcx.type_of results forward.

Resolves #4914.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Copilot review overview

🟡 Changes recommended

Fully omitted generic argument lists still bypass default filling.

Review effort: Balanced
Findings: 1

Open (1)

• Apply default generic parameters when path arguments are omitted · New

What changed in this PR

Fills omitted trailing default type parameters during contract target resolution.

Changes:

• Instantiates omitted type defaults using prior generic arguments.
• Adds positive and negative regression coverage.
• Leaves const defaults unsupported.

File	Description
kani-compiler/​src/​kani_middle/​resolve/​type_resolution.rs	Adds default type argument resolution.
tests/​kani/​FunctionContracts/​generic_default_argument_fill.rs	Tests successful default filling.
tests/​expected/​function-contract/​generic_default_missing_required.rs	Tests missing required parameters.
tests/​expected/​function-contract/​generic_default_missing_required.expected	Records expected diagnostic.
tests/​expected/​function-contract/​generic_default_const_param.rs	Tests unsupported const defaults.
tests/​expected/​function-contract/​generic_default_const_param.expected	Records expected diagnostic.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.