Fill omitted defaulted generic parameters during type resolution

kani-compiler/src/kani_middle/resolve/type_resolution.rs

@@ -6,10 +6,12 @@ use crate::kani_middle::resolve::{ResolveError, resolve_path, validate_kind};
 use quote::ToTokens;
 use rustc_hir::def::DefKind;
 use rustc_middle::ty::TyCtxt;
+use rustc_public::CrateDef;
 use rustc_public::mir::Mutability;
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
-    FloatTy, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy,
+    AdtDef, FloatTy, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind,
+    UintTy,
 };
 use rustc_span::def_id::LocalDefId;
 use std::str::FromStr;
@@ -102,26 +104,31 @@ pub fn resolve_ty<'tcx>(
 /// If `path`'s final segment carries angle-bracketed generic arguments, instantiate `ty`
 /// (the definition's identity type, e.g. `Wrap<T>`) with those arguments resolved to
 /// concrete types (e.g. `Wrap<u8>`), so trait-implementation lookups can match a concrete
-/// impl. Returns `ty` unchanged when there are no arguments or when any argument cannot
-/// be resolved — preserving the previous behavior for everything that resolved before.
+/// impl. An omitted trailing parameter with a declared default is filled from the
+/// default, also when the path has no generic arguments at all (`Wrapper` for
+/// `struct Wrapper<T = u8>`). Returns `ty` unchanged when any argument cannot be
+/// resolved or a parameter without a default is missing, preserving the previous
+/// behavior for everything that resolved before.
 fn instantiate_path_args<'tcx>(
     tcx: TyCtxt<'tcx>,
     current_module: LocalDefId,
     path: &syn::Path,
     ty: Ty,
 ) -> Ty {
-    let Some(syn::PathArguments::AngleBracketed(syn_args)) =
-        path.segments.last().map(|seg| &seg.arguments)
-    else {
-        return ty;
+    // No generic arguments (`Wrapper`) is an empty list; parenthesized args keep `ty`.
+    let syn_args: Vec<&syn::GenericArgument> = match path.segments.last().map(|seg| &seg.arguments)
+    {
+        Some(syn::PathArguments::AngleBracketed(args)) => args.args.iter().collect(),
+        Some(syn::PathArguments::None) => Vec::new(),
+        _ => return ty,
     };
     let TyKind::RigidTy(RigidTy::Adt(adt_def, identity_args)) = ty.kind() else {
         return ty;
     };
     // Resolve the user-written type arguments; lifetimes are erased below, and anything
     // else (const arguments, associated-type bindings) keeps the uninstantiated type.
     let mut user_tys = Vec::new();
-    for arg in &syn_args.args {
+    for arg in syn_args {
         match arg {
             syn::GenericArgument::Type(syn_ty) => match resolve_ty(tcx, current_module, syn_ty) {
                 Ok(t) => user_tys.push(t),
@@ -132,16 +139,22 @@ fn instantiate_path_args<'tcx>(
         }
     }
     // Substitute the definition's type parameters in declaration order; erase lifetime
-    // parameters. A count mismatch (e.g. defaulted parameters the user omitted) keeps
-    // the uninstantiated type.
+    // parameters; fill an omitted trailing parameter that has a declared default from
+    // that default, instantiated with the arguments so far — what rustc does for omitted
+    // arguments. A missing parameter without a default keeps the uninstantiated type.
     let mut user_iter = user_tys.into_iter();
     let mut new_args = Vec::new();
-    for arg in &identity_args.0 {
+    for (param_index, arg) in identity_args.0.iter().enumerate() {
         match arg {
-            GenericArgKind::Type(_) => match user_iter.next() {
-                Some(t) => new_args.push(GenericArgKind::Type(t)),
-                None => return ty,
-            },
+            GenericArgKind::Type(_) => {
+                let filled = user_iter
+                    .next()
+                    .or_else(|| default_type_arg(tcx, &adt_def, param_index, &new_args));
+                match filled {
+                    Some(t) => new_args.push(GenericArgKind::Type(t)),
+                    None => return ty,
+                }
+            }
             GenericArgKind::Lifetime(_) => {
                 new_args.push(GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased }))
             }
@@ -154,6 +167,31 @@ fn instantiate_path_args<'tcx>(
     Ty::from_rigid_kind(RigidTy::Adt(adt_def, GenericArgs(new_args)))
 }
 
+/// The declared default of `adt_def`'s `param_index`-th generic parameter, instantiated
+/// with the arguments already substituted before it — how rustc fills an omitted trailing
+/// argument (a default may only reference earlier parameters). `None` when the parameter
+/// has no default or the default is not a type; the caller then keeps the uninstantiated
+/// type.
+fn default_type_arg<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    adt_def: &AdtDef,
+    param_index: usize,
+    args_so_far: &[GenericArgKind],
+) -> Option<Ty> {
+    let def_id = rustc_internal::internal(tcx, adt_def.def_id());
+    let default = tcx.generics_of(def_id).own_params.get(param_index)?.default_value(tcx)?;
+    let internal_args: Vec<rustc_middle::ty::GenericArg<'tcx>> = args_so_far
+        .iter()
+        .map(|arg| match arg {
+            GenericArgKind::Type(t) => Some(rustc_internal::internal(tcx, *t).into()),
+            GenericArgKind::Lifetime(_) => Some(tcx.lifetimes.re_erased.into()),
+            GenericArgKind::Const(_) => None,
+        })
+        .collect::<Option<_>>()?;
+    let filled = default.instantiate(tcx, &internal_args[..]).skip_normalization().as_type()?;
+    Some(rustc_internal::stable(filled))
+}
+
 /// Enumeration of existing primitive types that are not parametric.
 #[derive(Copy, Clone, Debug, Eq, PartialEq, IntoStaticStr, EnumString)]
 #[strum(serialize_all = "lowercase")]

tests/expected/function-contract/generic_default_const_param.expected

@@ -0,0 +1 @@
+unable to find implementation of associated function `Probe::probe` for WithConst

tests/expected/function-contract/generic_default_const_param.rs

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// A `proof_for_contract` path that omits a generic parameter with a declared default keeps
+// the uninstantiated type when that parameter is a CONST parameter: only defaulted TYPE
+// parameters are filled (see tests/kani/FunctionContracts/generic_default_argument_fill.rs).
+// `WithConst<u8>` omits `N` (default 4); the const default is not filled, so the target
+// keeps the uninstantiated type and fails to resolve.
+
+struct WithConst<T, const N: usize = 4>([T; N]);
+
+trait Probe {
+    fn probe(&self) -> u32;
+}
+
+impl Probe for WithConst<u8> {
+    #[kani::ensures(|r| *r == 0)]
+    fn probe(&self) -> u32 {
+        0
+    }
+}
+
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(<WithConst<u8> as Probe>::probe)]
+    fn check_const_default_not_filled() {
+        let w = WithConst([0u8; 4]);
+        let _ = w.probe();
+    }
+}

tests/expected/function-contract/generic_default_missing_bare.expected

@@ -0,0 +1 @@
+unable to find implementation of associated function `Probe::probe` for NoDefaultBare

tests/expected/function-contract/generic_default_missing_bare.rs

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// A `proof_for_contract` path written with NO generic arguments (`NoDefaultBare`, not
+// `NoDefaultBare<..>`) keeps the uninstantiated type when a parameter has no default. The
+// no-arguments path is treated as an empty argument list, but the substitution loop still
+// returns the identity type at the first parameter it cannot fill (see
+// tests/kani/FunctionContracts/generic_default_argument_fill.rs).
+
+struct NoDefaultBare<T>(T);
+
+trait Probe {
+    fn probe(&self) -> u32;
+}
+
+impl Probe for NoDefaultBare<u8> {
+    #[kani::ensures(|r| *r == 2)]
+    fn probe(&self) -> u32 {
+        2
+    }
+}
+
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(<NoDefaultBare as Probe>::probe)]
+    fn check_missing_required_bare() {
+        let n = NoDefaultBare(1u8);
+        let _ = n.probe();
+    }
+}

tests/expected/function-contract/generic_default_missing_required.expected

@@ -0,0 +1 @@
+unable to find implementation of associated function `Probe::probe` for NoDefault

tests/expected/function-contract/generic_default_missing_required.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// A `proof_for_contract` path that omits a generic parameter WITHOUT a declared default
+// (`NoDefault<u8>` for `NoDefault<T, U>`) keeps the uninstantiated type and fails to
+// resolve. Only parameters with declared defaults are filled (see
+// tests/kani/FunctionContracts/generic_default_argument_fill.rs).
+
+struct NoDefault<T, U>(T, U);
+
+trait Probe {
+    fn probe(&self) -> u32;
+}
+
+impl Probe for NoDefault<u8, u16> {
+    #[kani::ensures(|r| *r == 1)]
+    fn probe(&self) -> u32 {
+        1
+    }
+}
+
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(<NoDefault<u8> as Probe>::probe)]
+    fn check_missing_required_param() {
+        let n = NoDefault(1u8, 2u16);
+        let _ = n.probe();
+    }
+}

tests/kani/FunctionContracts/generic_default_argument_fill.rs

@@ -0,0 +1,97 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// `proof_for_contract` on a target that omits trailing generic parameters with declared
+// defaults. An omitted trailing parameter is now filled from its declared default,
+// instantiated with the arguments so far — what rustc does for omitted arguments. These
+// all resolve and verify:
+//   * a std container default: `Vec<u8>` fills `A = Global`,
+//   * sibling discrimination under the fill: `Vec<u16>`'s impl has a distinct
+//     postcondition, so each harness only verifies if resolution picks its own impl,
+//   * a default referencing an earlier parameter: `Pair<u8>` fills `U = T` as `u8`,
+//   * the explicit spelling (`Vec<u16, std::alloc::Global>`) resolves unchanged,
+//   * an all-defaulted type written with no argument list: `AllDefault` fills `T = u8`.
+// `tests/expected/function-contract/generic_default_missing_required.rs` guards that a
+// missing parameter without a default still fails to resolve.
+
+#![feature(allocator_api)]
+
+trait Sum {
+    fn total(&self) -> usize;
+}
+
+impl Sum for Vec<u8> {
+    #[kani::requires(self.len() < 3)]
+    #[kani::ensures(|r| *r == self.len())]
+    fn total(&self) -> usize {
+        self.len()
+    }
+}
+
+// Distinct postcondition from the `Vec<u8>` impl, so a harness only verifies if
+// resolution lands on *this* impl rather than the sibling.
+impl Sum for Vec<u16> {
+    #[kani::requires(self.len() < 3)]
+    #[kani::ensures(|r| *r == self.len() + 1)]
+    fn total(&self) -> usize {
+        self.len() + 1
+    }
+}
+
+// `U`'s default references the earlier parameter, so `Pair<u8>` must fill `U = u8`.
+struct Pair<T, U = T>(T, U);
+
+impl Sum for Pair<u8> {
+    #[kani::ensures(|r| *r == 2)]
+    fn total(&self) -> usize {
+        2
+    }
+}
+
+// All parameters defaulted, written with no argument list at all (`AllDefault`, not
+// `AllDefault<..>`): the omitted list must still be filled from the default `T = u8`.
+struct AllDefault<T = u8>(T);
+
+impl Sum for AllDefault {
+    #[kani::ensures(|r| *r == 1)]
+    fn total(&self) -> usize {
+        1
+    }
+}
+
+mod verify {
+    use super::*;
+    // Kani's path resolver does not see the prelude; name `Vec` explicitly.
+    use std::vec::Vec;
+
+    #[kani::proof_for_contract(<Vec<u8> as Sum>::total)]
+    fn check_vec_default_filled() {
+        let v: Vec<u8> = vec![1, 2];
+        let _ = v.total();
+    }
+
+    #[kani::proof_for_contract(<Vec<u16> as Sum>::total)]
+    fn check_vec_sibling_discriminated() {
+        let v: Vec<u16> = vec![1];
+        let _ = v.total();
+    }
+
+    #[kani::proof_for_contract(<Pair<u8> as Sum>::total)]
+    fn check_default_from_earlier_param() {
+        let p = Pair(1u8, 2u8);
+        let _ = p.total();
+    }
+
+    #[kani::proof_for_contract(<Vec<u16, std::alloc::Global> as Sum>::total)]
+    fn check_explicit_spelling_unchanged() {
+        let v: Vec<u16> = vec![1];
+        let _ = v.total();
+    }
+
+    #[kani::proof_for_contract(<AllDefault as Sum>::total)]
+    fn check_all_parameters_defaulted() {
+        let a = AllDefault(0u8);
+        let _ = a.total();
+    }
+}