Instantiate path generic arguments during type resolution

[kasimte]

Contracts on a trait method whose type carries a concrete generic argument — <CStr as Index<RangeFrom<usize>>>::index, or a concrete instantiation of a generic self type — failed to resolve with MissingTraitImpl. resolve_ty returned the definition's identity type (RangeFrom<usize> came back as RangeFrom<Idx>), so the arguments written in the path were parsed but never applied.

This PR applies them, in resolve_ty's Type::Path arm, via the new instantiate_path_args.

Verification

The tests live in the standard tests/kani and tests/expected suites (CI runs them); each has a definite outcome:

test (-Zfunction-contracts)	expect
tests/kani/FunctionContracts/generic_argument_instantiation.rs	6 targets verify. A primitive argument resolved before (regression guard); the five generic shapes resolve only with this change — a generic argument, a generic self type (associated-type return, where-bounded method), a concrete DST self, a generic impl at a concrete instantiation, and a type with a lifetime parameter beside a type parameter (lifetime erased).
tests/expected/function-contract/generic_arg_unimplemented.rs	still fails MissingTraitImpl (expected-output test — this diagnostic is the pass) — <S as Generic<Wrap<u16>>>::generic is genuinely not implemented, so valid targets resolve without over-resolving invalid ones.
tests/expected/function-contract/generic_method_unimplemented.rs	still fails MissingTraitImpl (expected-output test — this diagnostic is the pass) — a trait method with its own generic parameter (fn compute<T>) is out of scope (see below).

Confirmed on nightly-2026-09-22 (Kani 0.68.0, CBMC 6.11.0): all six verify; with the fix reverted, the generic targets fail to resolve while the primitive resolves. The cross_module_multiple_impls (7/7), multiple_inherent_impls (3/3), and resolver unit (41/41) suites are unchanged.

Mechanism: this is the "trait functions with generic parameters" limitation described in #1997. The trait's arguments already reach trait-impl resolution, but each came back uninstantiated from resolve_ty, and full Instance::resolve cannot match a concrete impl from a free parameter. Making the arguments concrete fixes that; any shape that cannot be resolved (const-generic arguments, omitted defaulted parameters) keeps the old uninstantiated type, so nothing that resolved before changes. No partial-resolution machinery is needed — with concrete arguments, the existing full resolution matches.

These are not hypothetical. An iterator adapter's __iterator_get_unchecked (a generic self type) is another std-library method of this shape: the Challenge 16 and Challenge 24 submissions (model-checking/verify-rust-std#549, model-checking/verify-rust-std#689) disclose it and fall back to kani::assume mirror harnesses. What this change reaches there: closure-free adapters resolve (Cloned, Zip); Map/Filter do not, since fn/closure types aren't supported by resolve_ty. Challenge 24's <vec::IntoIter<u8> as Iterator>::__iterator_get_unchecked resolves only with the allocator written out (IntoIter<u8, std::alloc::Global>, which needs allocator_api): omitted trailing parameters with declared defaults are not filled and keep the uninstantiated type.

Related to #1997 — this handles a type carrying concrete generic arguments: a generic trait argument, or a generic self type instantiated to concrete types, against a concrete or generic impl. A trait method with its own generic parameter still fails to resolve — that parameter is not part of the path, so nothing here binds it.

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

[feliperodri]

Approving. On main, <CStr as Index<RangeFrom<usize>>>::index and your six targets fail to resolve; with this change they resolve and verify. The sibling impls with distinct postconditions show resolution lands on the right one. kani, expected and cargo-kani suites are green, and I found no change for paths that resolved before, including inherent impls on different instantiations.

The biggest remaining gap is defaulted type parameters, which the count check sends back to the uninstantiated type. It covers most std containers: <Vec<u8> as Trait>::m still fails, and so does the natural spelling of Challenge 24's target, <vec::IntoIter<u8> as Iterator>::__iterator_get_unchecked. It resolves only as IntoIter<u8, std::alloc::Global>, which needs allocator_api. Filling omitted trailing parameters from their declared defaults would cover all of these. Happy to see that as a follow-up rather than here.

On the description: Challenge 16 holds for closure-free adapters (Cloned, Zip resolve), but not for Map/Filter, since fn/closure types aren't supported by resolve_ty. Challenge 24 needs the allocator written out. Worth saying, so someone trying those targets knows what to expect.

[kasimte]

Thank you for the review and for measuring the adapter and container boundaries. Description updated to state what to expect per target: Cloned/Zip resolve; Map/Filter don't (fn/closure types unsupported in resolve_ty); Challenge 24's target needs the allocator written out.