Are there any recommendations on how to use function contracts on generic functions? Consider this unsound contract:

#[kani::ensures(|r| r == 0)]
fn foo<T>() -> usize {
    1 / mem::size_of::<T>()
}

#[kani::proof_for_contract(foo)]
fn prove_foo() {
    foo::<u8>();
}

foo will divide by zero when size_of::<T>() == 0. However, to my knowledge, Kani has no way of proving statements of the form "for all T, ...". Thus, there's no way to exhaustively cover the space of possible invocations of foo - we can only test with a representative set of types, which is not truly exhaustive, and thus doesn't 100% convince us that our contract is sound.

Is there a way to handle this problem, or should we just avoid using contracts (or at least avoid using ensures - requires are still fine) on generic functions?